michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(kernel/expr): remove 'null' expression, and operator bool for expression

Browse source 
After this commit, a value of type 'expr' cannot be a reference to nullptr.
This commit also fixes several bugs due to the use of 'null' expressions.

TODO: do the same for kernel objects, sexprs, etc.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-07 23:21:07 -08:00
parent e4dff52d7a
commit 3e1fd06903
77 changed files with 825 additions and 731 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/frontends/lean/frontend.cpp
View file

@ -315,16 +315,16 @@ struct lean_extension : public environment::extension {
env.add_neutral_object(new coercion_declaration(f));
}
expr get_coercion(expr const & from_type, expr const & to_type) const {
optional<expr> get_coercion(expr const & from_type, expr const & to_type) const {
expr_pair p(from_type, to_type);
auto it = m_coercion_map.find(p);
if (it != m_coercion_map.end())
return it->second;
return optional<expr>(it->second);
lean_extension const * parent = get_parent();
if (parent)
return parent->get_coercion(from_type, to_type);
else
return expr();
return optional<expr>();
}
list<expr_pair> get_coercions(expr const & from_type) const {
@ -444,7 +444,7 @@ bool frontend::is_explicit(name const & n) const {
void frontend::add_coercion(expr const & f) {
to_ext(m_env).add_coercion(f, m_env);
}
expr frontend::get_coercion(expr const & from_type, expr const & to_type) const {
optional<expr> frontend::get_coercion(expr const & from_type, expr const & to_type) const {
return to_ext(m_env).get_coercion(from_type, to_type);
}
list<expr_pair> frontend::get_coercions(expr const & from_type) const {

4
src/frontends/lean/frontend.h
View file

@ -157,10 +157,8 @@ public:
/**
\brief Return a coercion from given_type to expected_type if it exists.
Return the null expression if there is no coercion from \c from_type to
\c to_type.
*/
expr get_coercion(expr const & from_type, expr const & to_type) const;
optional<expr> get_coercion(expr const & from_type, expr const & to_type) const;
/**
\brief Return the list of coercions for the given type.

107
src/frontends/lean/frontend_elaborator.cpp
View file

@ -63,7 +63,7 @@ public:
return r;
}
virtual void get_children(buffer<justification_cell*> &) const {}
virtual expr const & get_main_expr() const { return m_src; }
virtual optional<expr> get_main_expr() const { return some(m_src); }
context const & get_context() const { return m_ctx; }
};
@ -82,7 +82,7 @@ public:
return r;
}
virtual void get_children(buffer<justification_cell*> &) const {}
virtual expr const & get_main_expr() const { return m_app; }
virtual optional<expr> get_main_expr() const { return some(m_app); }
context const & get_context() const { return m_ctx; }
expr const & get_app() const { return m_app; }
};
@ -133,30 +133,29 @@ class frontend_elaborator::imp {
/**
\brief Return the type of \c e if possible.
Return null expression if it was not possible to infer the type of \c e.
The idea is to use the type to catch the easy cases where we can solve
overloads (aka choices) and coercions during preprocessing.
*/
expr get_type(expr const & e, context const & ctx) {
optional<expr> get_type(expr const & e, context const & ctx) {
try {
return m_ref.m_type_inferer(e, ctx);
return some(m_ref.m_type_inferer(e, ctx));
} catch (exception &) {
return expr();
return optional<expr>();
}
}
/**
\brief Make sure f_t is a Pi, if it is not, then return the null expression.
\brief Make sure f_t is a Pi, if it is not, then return optional<expr>()
*/
expr check_pi(expr const & f_t, context const & ctx) {
if (!f_t || is_pi(f_t)) {
optional<expr> check_pi(optional<expr> const & f_t, context const & ctx) {
if (!f_t || is_pi(*f_t)) {
return f_t;
} else {
expr r = m_ref.m_normalizer(f_t, ctx);
expr r = m_ref.m_normalizer(*f_t, ctx);
if (is_pi(r))
return r;
return optional<expr>(r);
else
return expr();
return optional<expr>();
}
}
@ -174,20 +173,20 @@ class frontend_elaborator::imp {
return mk_app(mvar, a);
}
expr find_coercion(list<expr_pair> const & l, expr const & to_type) {
optional<expr> find_coercion(list<expr_pair> const & l, expr const & to_type) {
for (auto p : l) {
if (p.first == to_type) {
return p.second;
return optional<expr>(p.second);
}
}
return expr();
return optional<expr>();
}
/**
\brief Try to solve overload at preprocessing time.
*/
void choose(buffer<expr> & f_choices, buffer<expr> & f_choice_types,
buffer<expr> const & args, buffer<expr> const & arg_types,
void choose(buffer<expr> & f_choices, buffer<optional<expr>> & f_choice_types,
buffer<expr> const & args, buffer<optional<expr>> const & arg_types,
context const & ctx) {
unsigned best_num_coercions = std::numeric_limits<unsigned>::max();
unsigned num_choices = f_choices.size();
@ -196,7 +195,7 @@ class frontend_elaborator::imp {
buffer<unsigned> matched;
for (unsigned j = 0; j < num_choices; j++) {
expr f_t = f_choice_types[j];
optional<expr> f_t = f_choice_types[j];
unsigned num_coercions = 0; // number of coercions needed by current choice
unsigned num_skipped_args = 0;
unsigned i = 1;
@ -206,16 +205,16 @@ class frontend_elaborator::imp {
// can't process this choice at preprocessing time
delayed.push_back(j);
break;
}
expr expected = abst_domain(f_t);
expr given = arg_types[i];
} else {
expr expected = abst_domain(*f_t);
optional<expr> given = arg_types[i];
if (!given) {
num_skipped_args++;
} else {
if (!has_metavar(expected) && !has_metavar(given)) {
if (m_ref.m_type_checker.is_convertible(given, expected, ctx)) {
if (!has_metavar(expected) && !has_metavar(*given)) {
if (m_ref.m_type_checker.is_convertible(*given, expected, ctx)) {
// compatible
} else if (m_ref.m_frontend.get_coercion(given, expected)) {
} else if (m_ref.m_frontend.get_coercion(*given, expected)) {
// compatible if using coercion
num_coercions++;
} else {
@ -226,7 +225,8 @@ class frontend_elaborator::imp {
num_skipped_args++;
}
}
f_t = ::lean::instantiate(abst_body(f_t), args[i]);
f_t = some(::lean::instantiate(abst_body(*f_t), args[i]));
}
}
if (i == num_args) {
if (num_skipped_args > 0) {
@ -250,7 +250,7 @@ class frontend_elaborator::imp {
// We currently do nothing, and let the elaborator to sign the error
} else {
buffer<expr> to_keep;
buffer<expr> to_keep_types;
buffer<optional<expr>> to_keep_types;
for (unsigned i : matched) {
to_keep.push_back(f_choices[i]);
to_keep_types.push_back(f_choice_types[i]);
@ -275,27 +275,27 @@ class frontend_elaborator::imp {
virtual expr visit_app(expr const & e, context const & ctx) {
expr f = arg(e, 0);
expr f_t;
optional<expr> f_t;
buffer<expr> args;
buffer<expr> arg_types;
buffer<optional<expr>> arg_types;
args.push_back(expr()); // placeholder
arg_types.push_back(expr()); // placeholder
arg_types.push_back(optional<expr>()); // placeholder
for (unsigned i = 1; i < num_args(e); i++) {
expr a = arg(e, i);
expr new_a = visit(a, ctx);
expr new_a_t = get_type(new_a, ctx);
optional<expr> new_a_t = get_type(new_a, ctx);
args.push_back(new_a);
arg_types.push_back(new_a_t);
}
if (is_choice(f)) {
buffer<expr> f_choices;
buffer<expr> f_choice_types;
buffer<optional<expr>> f_choice_types;
unsigned num_alts = get_num_choices(f);
for (unsigned i = 0; i < num_alts; i++) {
expr c = get_choice(f, i);
expr new_c = visit(c, ctx);
expr new_c_t = get_type(new_c, ctx);
optional<expr> new_c_t = get_type(new_c, ctx);
f_choices.push_back(new_c);
f_choice_types.push_back(new_c_t);
}
@ -304,9 +304,9 @@ class frontend_elaborator::imp {
args[0] = mk_overload_mvar(f_choices, ctx, e);
for (unsigned i = 1; i < args.size(); i++) {
if (arg_types[i]) {
list<expr_pair> coercions = m_ref.m_frontend.get_coercions(arg_types[i]);
list<expr_pair> coercions = m_ref.m_frontend.get_coercions(*(arg_types[i]));
if (coercions)
args[i] = add_coercion_mvar_app(coercions, args[i], arg_types[i], ctx, arg(e, i));
args[i] = add_coercion_mvar_app(coercions, args[i], *(arg_types[i]), ctx, arg(e, i));
}
}
return mk_app(args);
@ -326,20 +326,20 @@ class frontend_elaborator::imp {
f_t = check_pi(f_t, ctx);
expr a = arg(e, i);
expr new_a = args[i];
expr new_a_t = arg_types[i];
optional<expr> new_a_t = arg_types[i];
if (new_a_t) {
list<expr_pair> coercions = m_ref.m_frontend.get_coercions(new_a_t);
list<expr_pair> coercions = m_ref.m_frontend.get_coercions(*new_a_t);
if (coercions) {
if (!f_t) {
new_a = add_coercion_mvar_app(coercions, new_a, new_a_t, ctx, a);
new_a = add_coercion_mvar_app(coercions, new_a, *new_a_t, ctx, a);
} else {
expr expected = abst_domain(f_t);
if (expected != new_a_t) {
expr c = find_coercion(coercions, expected);
expr expected = abst_domain(*f_t);
if (expected != *new_a_t) {
optional<expr> c = find_coercion(coercions, expected);
if (c) {
new_a = mk_app(c, new_a); // apply coercion
new_a = mk_app(*c, new_a); // apply coercion
} else {
new_a = add_coercion_mvar_app(coercions, new_a, new_a_t, ctx, a);
new_a = add_coercion_mvar_app(coercions, new_a, *new_a_t, ctx, a);
}
}
}
@ -347,34 +347,37 @@ class frontend_elaborator::imp {
}
new_args.push_back(new_a);
if (f_t)
f_t = ::lean::instantiate(abst_body(f_t), new_a);
f_t = some(::lean::instantiate(abst_body(*f_t), new_a));
}
return mk_app(new_args);
}
virtual expr visit_let(expr const & e, context const & ctx) {
lean_assert(is_let(e));
return update_let(e, [&](expr const & t, expr const & v, expr const & b) {
expr new_t = t ? visit(t, ctx) : expr();
return update_let(e, [&](optional<expr> const & t, expr const & v, expr const & b) {
optional<expr> new_t = visit(t, ctx);
expr new_v = visit(v, ctx);
if (new_t) {
expr new_v_t = get_type(new_v, ctx);
if (new_v_t && new_t != new_v_t) {
list<expr_pair> coercions = m_ref.m_frontend.get_coercions(new_v_t);
optional<expr> new_v_t = get_type(new_v, ctx);
if (new_v_t && *new_t != *new_v_t) {
list<expr_pair> coercions = m_ref.m_frontend.get_coercions(*new_v_t);
if (coercions) {
new_v = add_coercion_mvar_app(coercions, new_v, new_v_t, ctx, v);
new_v = add_coercion_mvar_app(coercions, new_v, *new_v_t, ctx, v);
}
}
}
expr new_b;
{
cache::mk_scope sc(m_cache);
new_b = visit(b, extend(ctx, let_name(e), new_t, new_v));
}
expr new_b = visit(b, extend(ctx, let_name(e), new_t, new_v));
return std::make_tuple(new_t, new_v, new_b);
}
});
}
optional<expr> visit(optional<expr> const & e, context const & ctx) {
return replace_visitor::visit(e, ctx);
}
virtual expr visit(expr const & e, context const & ctx) {
check_interrupted();
expr r = replace_visitor::visit(e, ctx);

36
src/frontends/lean/parser.cpp
View file

@ -324,9 +324,9 @@ class parser::imp {
void display_error_pos(pos_info const & p) { display_error_pos(p.first, p.second); }
void display_error_pos(expr const & e) {
void display_error_pos(optional<expr> const & e) {
if (e) {
auto it = m_expr_pos_info.find(e);
auto it = m_expr_pos_info.find(*e);
if (it == m_expr_pos_info.end())
return display_error_pos(m_last_cmd_pos);
else
@ -346,7 +346,11 @@ class parser::imp {
}
void display_error(kernel_exception const & ex) {
display_error_pos(m_elaborator.get_original(ex.get_main_expr()));
optional<expr> main_expr = ex.get_main_expr();
if (main_expr)
display_error_pos(some(m_elaborator.get_original(*main_expr)));
else
display_error_pos(main_expr);
regular(m_frontend) << " " << ex << endl;
}
@ -912,7 +916,7 @@ class parser::imp {
void parse_simple_bindings(bindings_buffer & result, bool implicit_decl, bool suppress_type) {
buffer<std::pair<pos_info, name>> names;
parse_names(names);
expr type;
optional<expr> type;
if (!suppress_type) {
check_colon_next("invalid binder, ':' expected");
type = parse_expr();
@ -928,7 +932,7 @@ class parser::imp {
--i;
expr arg_type;
if (type)
arg_type = lift_free_vars(type, i);
arg_type = lift_free_vars(*type, i);
else
arg_type = save(mk_placeholder(), names[i].first);
result[sz + i] = std::make_tuple(names[i].first, names[i].second, arg_type, implicit_decl);
@ -1063,11 +1067,11 @@ class parser::imp {
expr parse_let() {
next();
mk_scope scope(*this);
buffer<std::tuple<pos_info, name, expr, expr>> bindings;
buffer<std::tuple<pos_info, name, optional<expr>, expr>> bindings;
while (true) {
auto p = pos();
name id = check_identifier_next("invalid let expression, identifier expected");
expr type;
optional<expr> type;
if (curr_is_colon()) {
next();
type = parse_expr();
@ -1181,7 +1185,7 @@ class parser::imp {
expr t = parse_expr();
check_next(scanner::token::By, "invalid 'show _ by _' expression, 'by' expected");
tactic tac = parse_tactic_expr();
expr r = mk_placeholder(t);
expr r = mk_placeholder(optional<expr>(t));
m_tactic_hints[r] = tac;
return save(r, p);
}
@ -1440,7 +1444,7 @@ class parser::imp {
*/
expr parse_tactic_cmds(proof_state s, context const & ctx, expr const & expected_type) {
proof_state_seq_stack stack;
expr pr;
optional<expr> pr;
enum class status { Continue, Done, Eof, Abort };
status st = status::Continue;
while (st == status::Continue) {
@ -1497,7 +1501,7 @@ class parser::imp {
});
}
switch (st) {
case status::Done: return pr;
case status::Done: return *pr;
case status::Eof: throw parser_error("invalid tactic command, unexpected end of file", pos());
case status::Abort: throw parser_error("failed to prove theorem, proof has been aborted", pos());
default: lean_unreachable(); // LCOV_EXCL_LINE
@ -1542,9 +1546,14 @@ class parser::imp {
throw exception("failed to synthesize metavar, its type contains metavariables");
buffer<context_entry> new_entries;
for (auto e : menv.get_context(mvar)) {
new_entries.emplace_back(e.get_name(),
instantiate_metavars(e.get_domain(), menv),
instantiate_metavars(e.get_body(), menv));
optional<expr> d = e.get_domain();
optional<expr> b = e.get_body();
if (d) d = instantiate_metavars(*d, menv);
if (b) b = instantiate_metavars(*b, menv);
if (d)
new_entries.emplace_back(e.get_name(), *d, b);
else
new_entries.emplace_back(e.get_name(), d, *b);
}
context mvar_ctx(to_list(new_entries.begin(), new_entries.end()));
if (!m_type_inferer.is_proposition(mvar_type, mvar_ctx))
@ -1562,7 +1571,6 @@ class parser::imp {
next();
}
expr mvar_val = parse_tactic_cmds(s, mvar_ctx, mvar_type);
if (mvar_val)
menv.assign(mvar, mvar_val);
}
}

34
src/frontends/lean/pp.cpp
View file

@ -725,14 +725,14 @@ class pp_fn {
\remark The argument B is only relevant when processing
condensed definitions. \see pp_abstraction_core.
*/
std::pair<expr, expr> collect_nested(expr const & e, expr T, expr_kind k, buffer<std::pair<name, expr>> & r) {
if (e.kind() == k && (!T || is_abstraction(T))) {
std::pair<expr, optional<expr>> collect_nested(expr const & e, optional<expr> T, expr_kind k, buffer<std::pair<name, expr>> & r) {
if (e.kind() == k && (!T || is_abstraction(*T))) {
name n1 = get_unused_name(e);
m_local_names.insert(n1);
r.emplace_back(n1, abst_domain(e));
expr b = replace_var_with_name(abst_body(e), n1);
if (T)
T = replace_var_with_name(abst_body(T), n1);
T = some(replace_var_with_name(abst_body(*T), n1));
return collect_nested(b, T, k, r);
} else {
return mk_pair(e, T);
@ -849,7 +849,7 @@ class pp_fn {
\remark if T != 0, then T is Pi(x : A), B
*/
result pp_abstraction_core(expr const & e, unsigned depth, expr T, std::vector<bool> const * implicit_args = nullptr) {
result pp_abstraction_core(expr const & e, unsigned depth, optional<expr> T, std::vector<bool> const * implicit_args = nullptr) {
local_names::mk_scope mk(m_local_names);
if (is_arrow(e) && !implicit_args) {
lean_assert(!T);
@ -876,7 +876,7 @@ class pp_fn {
}
format body_sep;
if (T) {
format T_f = pp(T, 0).first;
format T_f = pp(*T, 0).first;
body_sep = format{space(), colon(), space(), T_f, space(), g_assign_fmt};
} else if (implicit_args) {
// This is a little hack to pretty print Variable and
@ -957,10 +957,10 @@ class pp_fn {
}
result pp_abstraction(expr const & e, unsigned depth) {
return pp_abstraction_core(e, depth, expr());
return pp_abstraction_core(e, depth, optional<expr>());
}
expr collect_nested_let(expr const & e, buffer<std::tuple<name, expr, expr>> & bindings) {
expr collect_nested_let(expr const & e, buffer<std::tuple<name, optional<expr>, expr>> & bindings) {
if (is_let(e)) {
name n1 = get_unused_name(e);
m_local_names.insert(n1);
@ -974,7 +974,7 @@ class pp_fn {
result pp_let(expr const & e, unsigned depth) {
local_names::mk_scope mk(m_local_names);
buffer<std::tuple<name, expr, expr>> bindings;
buffer<std::tuple<name, optional<expr>, expr>> bindings;
expr body = collect_nested_let(e, bindings);
unsigned r_weight = 2;
format r_format = g_let_fmt;
@ -985,9 +985,9 @@ class pp_fn {
format beg = i == 0 ? space() : line();
format sep = i < sz - 1 ? comma() : format();
result p_def = pp_scoped_child(std::get<2>(b), depth+1);
expr type = std::get<1>(b);
optional<expr> const & type = std::get<1>(b);
if (type) {
result p_type = pp_scoped_child(type, depth+1);
result p_type = pp_scoped_child(*type, depth+1);
r_format += nest(3 + 1, compose(beg, group(format{format(n), space(),
colon(), nest(n.size() + 1 + 1 + 1, compose(space(), p_type.first)), space(), g_assign_fmt,
nest(m_indent, format{line(), p_def.first, sep})})));
@ -1166,13 +1166,12 @@ public:
format pp_definition(expr const & v, expr const & t, std::vector<bool> const * implicit_args) {
init(mk_app(v, t));
expr T(t);
return pp_abstraction_core(v, 0, T, implicit_args).first;
return pp_abstraction_core(v, 0, optional<expr>(t), implicit_args).first;
}
format pp_pi_with_implicit_args(expr const & e, std::vector<bool> const & implicit_args) {
init(e);
return pp_abstraction_core(e, 0, expr(), &implicit_args).first;
return pp_abstraction_core(e, 0, optional<expr>(), &implicit_args).first;
}
void register_local(name const & n) {
@ -1198,10 +1197,13 @@ class pp_formatter_cell : public formatter_cell {
check_interrupted();
name n1 = get_unused_name(c2);
fn.register_local(n1);
format entry = format{format(n1), space(), colon(), space(), fn(fake_context_domain(c2))};
expr val = fake_context_value(c2);
format entry = format(n1);
optional<expr> domain = fake_context_domain(c2);
optional<expr> val = fake_context_value(c2);
if (domain)
entry += format{space(), colon(), space(), fn(*domain)};
if (val)
entry += format{space(), g_assign_fmt, nest(indent, format{line(), fn(val)})};
entry += format{space(), g_assign_fmt, nest(indent, format{line(), fn(*val)})};
if (first) {
r = group(entry);
first = false;

4
src/kernel/abstract.h
View file

@ -48,8 +48,8 @@ inline expr Pi(std::pair<expr const &, expr const &> const & p, expr const & b)
/**
\brief Create a Let expression (Let x := v in b), the term b is abstracted using abstract(b, x).
*/
inline expr Let(name const & x, expr const & v, expr const & b) { return mk_let(x, expr(), v, abstract(b, mk_constant(x))); }
inline expr Let(expr const & x, expr const & v, expr const & b) { return mk_let(const_name(x), expr(), v, abstract(b, x)); }
inline expr Let(name const & x, expr const & v, expr const & b) { return mk_let(x, v, abstract(b, mk_constant(x))); }
inline expr Let(expr const & x, expr const & v, expr const & b) { return mk_let(const_name(x), v, abstract(b, x)); }
inline expr Let(std::pair<expr const &, expr const &> const & p, expr const & b) { return Let(p.first, p.second, b); }
expr Let(std::initializer_list<std::pair<expr const &, expr const &>> const & l, expr const & b);
/**

19
src/kernel/builtin.cpp
View file

@ -126,27 +126,26 @@ static format g_if_fmt(g_if_name);
*/
class if_fn_value : public value {
expr m_type;
public:
if_fn_value() {
static expr mk_type() {
expr A = Const("A");
// Pi (A: Type), bool -> A -> A -> A
m_type = Pi({A, TypeU}, Bool >> (A >> (A >> A)));
return Pi({A, TypeU}, Bool >> (A >> (A >> A)));
}
public:
if_fn_value():m_type(mk_type()) {}
virtual ~if_fn_value() {}
virtual expr get_type() const { return m_type; }
virtual name get_name() const { return g_if_name; }
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
if (num_args == 5 && is_bool_value(args[2])) {
if (to_bool(args[2]))
r = args[3]; // if A true a b --> a
return some(args[3]); // if A true a b --> a
else
r = args[4]; // if A false a b --> b
return true;
return some(args[4]); // if A false a b --> b
} else if (num_args == 5 && args[3] == args[4]) {
r = args[3]; // if A c a a --> a
return true;
return some(args[3]); // if A c a a --> a
} else {
return false;
return optional<expr>();
}
}
};

18
src/kernel/context.h
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#pragma once
#include <utility>
#include "util/list.h"
#include "util/optional.h"
#include "kernel/expr.h"
namespace lean {
@ -16,14 +17,16 @@ namespace lean {
*/
class context_entry {
name m_name;
expr m_domain;
expr m_body;
optional<expr> m_domain;
optional<expr> m_body;
public:
context_entry(name const & n, optional<expr> const & d, expr const & b):m_name(n), m_domain(d), m_body(b) {}
context_entry(name const & n, expr const & d, optional<expr> const & b):m_name(n), m_domain(d), m_body(b) {}
context_entry(name const & n, expr const & d, expr const & b):m_name(n), m_domain(d), m_body(b) {}
context_entry(name const & n, expr const & d):m_name(n), m_domain(d) {}
name const & get_name() const { return m_name; }
expr const & get_domain() const { return m_domain; }
expr const & get_body() const { return m_body; }
optional<expr> const & get_domain() const { return m_domain; }
optional<expr> const & get_body() const { return m_body; }
};
/**
@ -33,8 +36,11 @@ class context {
list<context_entry> m_list;
public:
context() {}
context(context const & c, name const & n, expr const & d):m_list(context_entry(n, d), c.m_list) {}
context(context const & c, name const & n, optional<expr> const & d, expr const & b):m_list(context_entry(n, d, b), c.m_list) {}
context(context const & c, name const & n, expr const & d, optional<expr> const & b):m_list(context_entry(n, d, b), c.m_list) {}
context(context const & c, name const & n, expr const & d, expr const & b):m_list(context_entry(n, d, b), c.m_list) {}
context(context const & c, name const & n, expr const & d):m_list(context_entry(n, d), c.m_list) {}
context(context const & c, context_entry const & e):m_list(e, c.m_list) {}
explicit context(list<context_entry> const & l):m_list(l) {}
context_entry const & lookup(unsigned vidx) const;
std::pair<context_entry const &, context> lookup_ext(unsigned vidx) const;
@ -69,6 +75,8 @@ inline std::pair<context_entry const &, context> lookup_ext(context const & c, u
Bruijn index \c i.
*/
inline context_entry const & lookup(context const & c, unsigned i) { return c.lookup(i); }
inline context extend(context const & c, name const & n, optional<expr> const & d, expr const & b) { return context(c, n, d, b); }
inline context extend(context const & c, name const & n, expr const & d, optional<expr> const & b) { return context(c, n, d, b); }
inline context extend(context const & c, name const & n, expr const & d, expr const & b) { return context(c, n, d, b); }
inline context extend(context const & c, name const & n, expr const & d) { return context(c, n, d); }
inline bool empty(context const & c) { return c.empty(); }

5
src/kernel/environment.cpp
View file

@ -159,11 +159,12 @@ struct environment::imp {
object const & get_object(name const & n, environment const & env) const {
object const & obj = get_object_core(n);
if (obj)
if (obj) {
return obj;
else
} else {
throw unknown_object_exception(env, n);
}
}
/**
\brief Return true if u >= v + k is implied by constraints

32
src/kernel/expr.cpp
View file

@ -15,6 +15,9 @@ Author: Leonardo de Moura
#include "kernel/metavar.h"
namespace lean {
static expr g_dummy(mk_var(0));
expr::expr():expr(g_dummy) {}
local_entry::local_entry(unsigned s, unsigned n):m_kind(local_entry_kind::Lift), m_s(s), m_n(n) {}
local_entry::local_entry(unsigned s, expr const & v):m_kind(local_entry_kind::Inst), m_s(s), m_v(v) {}
local_entry::~local_entry() {}
@ -31,13 +34,6 @@ unsigned hash_args(unsigned size, expr const * args) {
return hash(size, [&args](unsigned i){ return args[i].hash(); });
}
static expr g_null;
expr const & expr::null() {
lean_assert(!g_null);
return g_null;
}
expr_cell::expr_cell(expr_kind k, unsigned h, bool has_mv):
m_kind(static_cast<unsigned>(k)),
m_flags(has_mv ? 4 : 0),
@ -55,20 +51,25 @@ expr_cell::expr_cell(expr_kind k, unsigned h, bool has_mv):
}
void expr_cell::dec_ref(expr & e, buffer<expr_cell*> & todelete) {
if (e) {
if (e.m_ptr) {
expr_cell * c = e.steal_ptr();
lean_assert(!e);
lean_assert(!(e.m_ptr));
if (c->dec_ref_core())
todelete.push_back(c);
}
}
void expr_cell::dec_ref(optional<expr> & c, buffer<expr_cell*> & todelete) {
if (c)
dec_ref(*c, todelete);
}
expr_var::expr_var(unsigned idx):
expr_cell(expr_kind::Var, idx, false),
m_vidx(idx) {}
expr_const::expr_const(name const & n, expr const & t):
expr_cell(expr_kind::Constant, n.hash(), t && t.has_metavar()),
expr_const::expr_const(name const & n, optional<expr> const & t):
expr_cell(expr_kind::Constant, n.hash(), t && t->has_metavar()),
m_name(n),
m_type(t) {}
void expr_const::dealloc(buffer<expr_cell*> & todelete) {
@ -86,7 +87,6 @@ void expr_app::dealloc(buffer<expr_cell*> & todelete) {
while (i > 0) {
--i;
dec_ref(m_args[i], todelete);
lean_assert(!m_args[i]);
}
delete[] reinterpret_cast<char*>(this);
}
@ -140,8 +140,6 @@ expr_abstraction::expr_abstraction(expr_kind k, name const & n, expr const & t,
void expr_abstraction::dealloc(buffer<expr_cell*> & todelete) {
dec_ref(m_body, todelete);
dec_ref(m_domain, todelete);
lean_assert(!m_body);
lean_assert(!m_domain);
delete(this);
}
expr_lambda::expr_lambda(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Lambda, n, t, e) {}
@ -151,8 +149,8 @@ expr_type::expr_type(level const & l):
m_level(l) {
}
expr_type::~expr_type() {}
expr_let::expr_let(name const & n, expr const & t, expr const & v, expr const & b):
expr_cell(expr_kind::Let, ::lean::hash(v.hash(), b.hash()), v.has_metavar() || b.has_metavar() || (t && t.has_metavar())),
expr_let::expr_let(name const & n, optional<expr> const & t, expr const & v, expr const & b):
expr_cell(expr_kind::Let, ::lean::hash(v.hash(), b.hash()), v.has_metavar() || b.has_metavar() || (t && t->has_metavar())),
m_name(n),
m_type(t),
m_value(v),
@ -166,7 +164,7 @@ void expr_let::dealloc(buffer<expr_cell*> & todelete) {
}
expr_let::~expr_let() {}
name value::get_unicode_name() const { return get_name(); }
bool value::normalize(unsigned, expr const *, expr &) const { return false; }
optional<expr> value::normalize(unsigned, expr const *) const { return optional<expr>(); }
void value::display(std::ostream & out) const { out << get_name(); }
bool value::operator==(value const & other) const { return typeid(*this) == typeid(other); }
bool value::operator<(value const & other) const {

65
src/kernel/expr.h
View file

@ -17,6 +17,7 @@ Author: Leonardo de Moura
#include "util/hash.h"
#include "util/buffer.h"
#include "util/list_fn.h"
#include "util/optional.h"
#include "util/sexpr/format.h"
#include "kernel/level.h"
@ -85,6 +86,7 @@ protected:
void set_closed() { m_flags |= 2; }
friend class has_free_var_fn;
static void dec_ref(expr & c, buffer<expr_cell*> & todelete);
static void dec_ref(optional<expr> & c, buffer<expr_cell*> & todelete);
public:
expr_cell(expr_kind k, unsigned h, bool has_mv);
expr_kind kind() const { return static_cast<expr_kind>(m_kind); }
@ -102,13 +104,11 @@ private:
friend class expr_cell;
expr_cell * steal_ptr() { expr_cell * r = m_ptr; m_ptr = nullptr; return r; }
public:
expr():m_ptr(nullptr) {}
expr();
expr(expr const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
expr(expr && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
~expr() { if (m_ptr) m_ptr->dec_ref(); }
static expr const & null();
friend void swap(expr & a, expr & b) { std::swap(a.m_ptr, b.m_ptr); }
void release() { if (m_ptr) m_ptr->dec_ref(); m_ptr = nullptr; }
@ -123,20 +123,21 @@ public:
expr_cell * raw() const { return m_ptr; }
explicit operator bool() const { return m_ptr != nullptr; }
friend expr mk_var(unsigned idx);
friend expr mk_constant(name const & n, expr const & t);
friend expr mk_constant(name const & n, optional<expr> const & t);
friend expr mk_value(value & v);
friend expr mk_app(unsigned num_args, expr const * args);
friend expr mk_eq(expr const & l, expr const & r);
friend expr mk_lambda(name const & n, expr const & t, expr const & e);
friend expr mk_pi(name const & n, expr const & t, expr const & e);
friend expr mk_type(level const & l);
friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & e);
friend expr mk_let(name const & n, optional<expr> const & t, expr const & v, expr const & e);
friend expr mk_metavar(name const & n, local_context const & ctx);
friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; }
friend bool is_eqp(optional<expr> const & a, optional<expr> const & b) {
return static_cast<bool>(a) == static_cast<bool>(b) && (!a || is_eqp(*a, *b));
}
// Overloaded operator() can be used to create applications
expr operator()(expr const & a1) const;
@ -161,15 +162,15 @@ public:
/** \brief Constants. */
class expr_const : public expr_cell {
name m_name;
expr m_type; // (optional) cached type
optional<expr> m_type;
// Remark: we do *not* perform destructive updates on m_type
// This field is used to efficiently implement the tactic framework
friend class expr_cell;
void dealloc(buffer<expr_cell*> & to_delete);
public:
expr_const(name const & n, expr const & type);
expr_const(name const & n, optional<expr> const & type);
name const & get_name() const { return m_name; }
expr const & get_type() const { return m_type; }
optional<expr> const & get_type() const { return m_type; }
};
/** \brief Function Applications */
class expr_app : public expr_cell {
@ -224,16 +225,16 @@ public:
/** \brief Let expressions */
class expr_let : public expr_cell {
name m_name;
expr m_type;
optional<expr> m_type;
expr m_value;
expr m_body;
friend class expr_cell;
void dealloc(buffer<expr_cell*> & todelete);
public:
expr_let(name const & n, expr const & t, expr const & v, expr const & b);
expr_let(name const & n, optional<expr> const & t, expr const & v, expr const & b);
~expr_let();
name const & get_name() const { return m_name; }
expr const & get_type() const { return m_type; }
optional<expr> const & get_type() const { return m_type; }
expr const & get_value() const { return m_value; }
expr const & get_body() const { return m_body; }
};
@ -262,7 +263,7 @@ public:
virtual expr get_type() const = 0;
virtual name get_name() const = 0;
virtual name get_unicode_name() const;
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const;
virtual optional<expr> normalize(unsigned num_args, expr const * args) const;
virtual bool operator==(value const & other) const;
bool operator<(value const & other) const;
virtual void display(std::ostream & out) const;
@ -320,7 +321,7 @@ class local_entry {
local_entry_kind m_kind;
unsigned m_s;
unsigned m_n;
expr m_v;
optional<expr> m_v;
local_entry(unsigned s, unsigned n);
local_entry(unsigned s, expr const & v);
public:
@ -334,7 +335,7 @@ public:
unsigned n() const { lean_assert(is_lift()); return m_n; }
bool operator==(local_entry const & e) const;
bool operator!=(local_entry const & e) const { return !operator==(e); }
expr const & v() const { lean_assert(is_inst()); return m_v; }
expr const & v() const { lean_assert(is_inst()); return *m_v; }
};
inline local_entry mk_lift(unsigned s, unsigned n) { return local_entry(s, n); }
inline local_entry mk_inst(unsigned s, expr const & v) { return local_entry(s, v); }
@ -383,7 +384,9 @@ inline bool is_abstraction(expr const & e) { return is_lambda(e) || is_pi(e); }
// Constructors
inline expr mk_var(unsigned idx) { return expr(new expr_var(idx)); }
inline expr Var(unsigned idx) { return mk_var(idx); }
inline expr mk_constant(name const & n, expr const & t = expr()) { return expr(new expr_const(n, t)); }
inline expr mk_constant(name const & n, optional<expr> const & t) { return expr(new expr_const(n, t)); }
inline expr mk_constant(name const & n, expr const & t) { return mk_constant(n, optional<expr>(t)); }
inline expr mk_constant(name const & n) { return mk_constant(n, optional<expr>()); }
inline expr Const(name const & n) { return mk_constant(n); }
inline expr mk_value(value & v) { return expr(new expr_value(v)); }
inline expr to_expr(value & v) { return mk_value(v); }
@ -400,7 +403,9 @@ inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return e
inline expr mk_pi(name const & n, expr const & t, expr const & e) { return expr(new expr_pi(n, t, e)); }
inline expr mk_arrow(expr const & t, expr const & e) { return mk_pi(name("_"), t, e); }
inline expr operator>>(expr const & t, expr const & e) { return mk_arrow(t, e); }
inline expr mk_let(name const & n, expr const & t, expr const & v, expr const & e) { return expr(new expr_let(n, t, v, e)); }
inline expr mk_let(name const & n, optional<expr> const & t, expr const & v, expr const & e) { return expr(new expr_let(n, t, v, e)); }
inline expr mk_let(name const & n, expr const & t, expr const & v, expr const & e) { return mk_let(n, optional<expr>(t), v, e); }
inline expr mk_let(name const & n, expr const & v, expr const & e) { return mk_let(n, optional<expr>(), v, e); }
inline expr mk_type(level const & l) { return expr(new expr_type(l)); }
expr mk_type();
inline expr Type(level const & l) { return mk_type(l); }
@ -453,7 +458,7 @@ inline unsigned var_idx(expr_cell * e) { return to_var(e)->get
inline bool is_var(expr_cell * e, unsigned i) { return is_var(e) && var_idx(e) == i; }
inline name const & const_name(expr_cell * e) { return to_constant(e)->get_name(); }
// Remark: the following function should not be exposed in the internal API.
inline expr const & const_type(expr_cell * e) { return to_constant(e)->get_type(); }
inline optional<expr> const & const_type(expr_cell * e) { return to_constant(e)->get_type(); }
inline value const & to_value(expr_cell * e) { lean_assert(is_value(e)); return static_cast<expr_value*>(e)->get_value(); }
inline unsigned num_args(expr_cell * e) { return to_app(e)->get_num_args(); }
inline expr const & arg(expr_cell * e, unsigned idx) { return to_app(e)->get_arg(idx); }
@ -465,7 +470,7 @@ inline expr const & abst_body(expr_cell * e) { return to_abstraction
inline level const & ty_level(expr_cell * e) { return to_type(e)->get_level(); }
inline name const & let_name(expr_cell * e) { return to_let(e)->get_name(); }
inline expr const & let_value(expr_cell * e) { return to_let(e)->get_value(); }
inline expr const & let_type(expr_cell * e) { return to_let(e)->get_type(); }
inline optional<expr> const & let_type(expr_cell * e) { return to_let(e)->get_type(); }
inline expr const & let_body(expr_cell * e) { return to_let(e)->get_body(); }
inline name const & metavar_name(expr_cell * e) { return to_metavar(e)->get_name(); }
inline local_context const & metavar_lctx(expr_cell * e) { return to_metavar(e)->get_lctx(); }
@ -480,7 +485,7 @@ inline unsigned var_idx(expr const & e) { return to_var(e)->ge
inline bool is_var(expr const & e, unsigned i) { return is_var(e) && var_idx(e) == i; }
inline name const & const_name(expr const & e) { return to_constant(e)->get_name(); }
// Remark: the following function should not be exposed in the internal API.
inline expr const & const_type(expr const & e) { return to_constant(e)->get_type(); }
inline optional<expr> const & const_type(expr const & e) { return to_constant(e)->get_type(); }
/** \brief Return true iff the given expression is a constant with name \c n. */
inline bool is_constant(expr const & e, name const & n) {
return is_constant(e) && const_name(e) == n;
@ -497,7 +502,7 @@ inline expr const & abst_domain(expr const & e) { return to_abstractio
inline expr const & abst_body(expr const & e) { return to_abstraction(e)->get_body(); }
inline level const & ty_level(expr const & e) { return to_type(e)->get_level(); }
inline name const & let_name(expr const & e) { return to_let(e)->get_name(); }
inline expr const & let_type(expr const & e) { return to_let(e)->get_type(); }
inline optional<expr> const & let_type(expr const & e) { return to_let(e)->get_type(); }
inline expr const & let_value(expr const & e) { return to_let(e)->get_value(); }
inline expr const & let_body(expr const & e) { return to_let(e)->get_body(); }
inline name const & metavar_name(expr const & e) { return to_metavar(e)->get_name(); }
@ -604,15 +609,15 @@ template<typename F> expr update_abst(expr const & e, F f) {
}
}
template<typename F> expr update_let(expr const & e, F f) {
static_assert(std::is_same<typename std::result_of<F(expr const &, expr const &, expr const &)>::type,
std::tuple<expr, expr, expr>>::value,
"update_let: return type of f is not pair<expr, expr>");
expr const & old_t = let_type(e);
static_assert(std::is_same<typename std::result_of<F(optional<expr> const &, expr const &, expr const &)>::type,
std::tuple<optional<expr>, expr, expr>>::value,
"update_let: return type of f is not tuple<optional<expr>, expr, expr>");
optional<expr> const & old_t = let_type(e);
expr const & old_v = let_value(e);
expr const & old_b = let_body(e);
std::tuple<expr, expr, expr> t = f(old_t, old_v, old_b);
if (!is_eqp(std::get<0>(t), old_t) || !is_eqp(std::get<1>(t), old_v) || !is_eqp(std::get<2>(t), old_b))
return mk_let(let_name(e), std::get<0>(t), std::get<1>(t), std::get<2>(t));
std::tuple<optional<expr>, expr, expr> r = f(old_t, old_v, old_b);
if (!is_eqp(std::get<0>(r), old_t) || !is_eqp(std::get<1>(r), old_v) || !is_eqp(std::get<2>(r), old_b))
return mk_let(let_name(e), std::get<0>(r), std::get<1>(r), std::get<2>(r));
else
return e;
}
@ -661,7 +666,7 @@ inline expr update_metavar(expr const & e, local_context const & lctx) {
else
return e;
}
inline expr update_const(expr const & e, expr const & t) {
inline expr update_const(expr const & e, optional<expr> const & t) {
if (!is_eqp(const_type(e), t))
return mk_constant(const_name(e), t);
else

10
src/kernel/expr_eq.h
View file

@ -29,10 +29,18 @@ class expr_eq_fn {
std::unique_ptr<expr_cell_pair_set> m_eq_visited;
N m_norm;
bool apply(optional<expr> const & a0, optional<expr> const & b0) {
if (is_eqp(a0, b0))
return true;
else if (!a0 || !b0)
return false;
else
return apply(*a0, *b0);
}
bool apply(expr const & a0, expr const & b0) {
check_system("expression equality test");
if (is_eqp(a0, b0)) return true;
if (!a0 || !b0) return false;
if (UseHash && a0.hash() != b0.hash()) return false;
expr const & a = m_norm(a0);
expr const & b = m_norm(b0);

27
src/kernel/find_fn.h
View file

@ -12,9 +12,9 @@ namespace lean {
template<typename P>
class find_fn {
struct pred_fn {
expr & m_result;
optional<expr> & m_result;
P m_p;
pred_fn(expr & result, P const & p):m_result(result), m_p(p) {}
pred_fn(optional<expr> & result, P const & p):m_result(result), m_p(p) {}
bool operator()(expr const & e, unsigned) {
if (m_result) {
return false; // already found result, stop the search
@ -26,19 +26,18 @@ class find_fn {
}
}
};
expr m_result;
optional<expr> m_result;
for_each_fn<pred_fn> m_proc;
public:
find_fn(P const & p):m_proc(pred_fn(m_result, p)) {}
expr operator()(expr const & e) { m_proc(e); return m_result; }
optional<expr> operator()(expr const & e) { m_proc(e); return m_result; }
};
/**
\brief Return a subexpression of \c e that satisfies the predicate \c p.
If there is none, then return the null expression.
*/
template<typename P>
expr find(expr const & e, P p) {
optional<expr> find(expr const & e, P p) {
return find_fn<P>(p)(e);
}
@ -46,22 +45,26 @@ expr find(expr const & e, P p) {
\brief Return an expression \c e that satisfies \c p and occurs in \c c or \c es.
*/
template<typename P>
expr find(context const * c, unsigned sz, expr const * es, P p) {
optional<expr> find(context const * c, unsigned sz, expr const * es, P p) {
find_fn<P> finder(p);
if (c) {
for (auto const & e : *c) {
if (expr r = finder(e.get_domain())) {
auto const & d = e.get_domain();
if (d) {
if (optional<expr> r = finder(*d))
return r;
} else if (e.get_body()) {
if (expr r = finder(e.get_body()))
}
auto const & b = e.get_body();
if (b) {
if (optional<expr> r = finder(*b))
return r;
}
}
}
for (unsigned i = 0; i < sz; i++) {
if (expr r = finder(es[i]))
if (optional<expr> r = finder(es[i]))
return r;
}
return expr();
return optional<expr>();
}
}

4
src/kernel/for_each_fn.h
View file

@ -71,7 +71,7 @@ class for_each_fn {
switch (e.kind()) {
case expr_kind::Constant:
if (const_type(e))
todo.emplace_back(const_type(e), offset);
todo.emplace_back(*const_type(e), offset);
goto begin_loop;
case expr_kind::Type: case expr_kind::Value:
case expr_kind::Var: case expr_kind::MetaVar:
@ -98,7 +98,7 @@ class for_each_fn {
todo.emplace_back(let_body(e), offset + 1);
todo.emplace_back(let_value(e), offset);
if (let_type(e))
todo.emplace_back(let_type(e), offset);
todo.emplace_back(*let_type(e), offset);
goto begin_loop;
}
}

14
src/kernel/free_vars.cpp
View file

@ -21,6 +21,10 @@ class has_free_vars_fn {
protected:
expr_cell_offset_set m_cached;
bool apply(optional<expr> const & e, unsigned offset) {
return e && apply(*e, offset);
}
bool apply(expr const & e, unsigned offset) {
// handle easy cases
switch (e.kind()) {
@ -80,7 +84,7 @@ protected:
result = apply(abst_domain(e), offset) || apply(abst_body(e), offset + 1);
break;
case expr_kind::Let:
result = (let_type(e) && apply(let_type(e), offset)) || apply(let_value(e), offset) || apply(let_body(e), offset + 1);
result = apply(let_type(e), offset) || apply(let_value(e), offset) || apply(let_body(e), offset + 1);
break;
}
@ -99,7 +103,7 @@ public:
};
bool has_free_vars(expr const & e) {
return e && has_free_vars_fn()(e);
return has_free_vars_fn()(e);
}
/**
@ -114,6 +118,10 @@ protected:
unsigned m_high;
expr_cell_offset_set m_cached;
bool apply(optional<expr> const & e, unsigned offset) {
return e && apply(*e, offset);
}
bool apply(expr const & e, unsigned offset) {
// handle easy cases
switch (e.kind()) {
@ -163,7 +171,7 @@ protected:
result = apply(abst_domain(e), offset) || apply(abst_body(e), offset + 1);
break;
case expr_kind::Let:
result = (let_type(e) && apply(let_type(e), offset)) || apply(let_value(e), offset) || apply(let_body(e), offset + 1);
result = apply(let_type(e), offset) || apply(let_value(e), offset) || apply(let_body(e), offset + 1);
break;
}

6
src/kernel/justification.cpp
View file

@ -9,10 +9,10 @@ Author: Leonardo de Moura
#include "kernel/justification.h"
namespace lean {
void justification_cell::add_pos_info(format & r, expr const & e, pos_info_provider const * p) {
void justification_cell::add_pos_info(format & r, optional<expr> const & e, pos_info_provider const * p) {
if (!p || !e)
return;
format f = p->pp(e);
format f = p->pp(*e);
if (!f)
return;
r += f;
@ -42,7 +42,7 @@ bool justification::has_children() const {
assumption_justification::assumption_justification(unsigned idx):m_idx(idx) {}
void assumption_justification::get_children(buffer<justification_cell*> &) const {}
expr const & assumption_justification::get_main_expr() const { return expr::null(); }
optional<expr> assumption_justification::get_main_expr() const { return optional<expr>(); }
format assumption_justification::pp_header(formatter const &, options const &) const {
return format{format("Assumption"), space(), format(m_idx)};
}

8
src/kernel/justification.h
View file

@ -26,14 +26,14 @@ class justification_cell {
MK_LEAN_RC();
void dealloc() { delete this; }
protected:
static void add_pos_info(format & r, expr const & e, pos_info_provider const * p);
static void add_pos_info(format & r, optional<expr> const & e, pos_info_provider const * p);
public:
justification_cell():m_rc(0) {}
virtual ~justification_cell() {}
virtual format pp_header(formatter const & fmt, options const & opts) const = 0;
virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const;
virtual void get_children(buffer<justification_cell*> & r) const = 0;
virtual expr const & get_main_expr() const { return expr::null(); }
virtual optional<expr> get_main_expr() const { return optional<expr>(); }
bool is_shared() const { return get_rc() > 1; }
};
@ -45,7 +45,7 @@ class assumption_justification : public justification_cell {
public:
assumption_justification(unsigned idx);
virtual void get_children(buffer<justification_cell*> &) const;
virtual expr const & get_main_expr() const;
virtual optional<expr> get_main_expr() const;
virtual format pp_header(formatter const &, options const &) const;
};
@ -73,7 +73,7 @@ public:
lean_assert(m_ptr);
return m_ptr->pp(fmt, opts, p, display_children);
}
expr const & get_main_expr() const { return m_ptr ? m_ptr->get_main_expr() : expr::null(); }
optional<expr> get_main_expr() const { return m_ptr ? m_ptr->get_main_expr() : optional<expr>(); }
void get_children(buffer<justification_cell*> & r) const { if (m_ptr) m_ptr->get_children(r); }
bool has_children() const;
};

23
src/kernel/kernel_exception.h
View file

@ -24,11 +24,10 @@ public:
virtual ~kernel_exception() noexcept {}
environment const & get_environment() const { return m_env; }
/**
\brief Return a reference to the main expression associated with this exception.
Return the null expression if there is none. This information is used to provide
better error messages.
\brief Return a reference (if available) to the main expression associated with this exception.
This information is used to provide better error messages.
*/
virtual expr const & get_main_expr() const { return expr::null(); }
virtual optional<expr> get_main_expr() const { return optional<expr>(); }
virtual format pp(formatter const & fmt, options const & opts) const;
virtual exception * clone() const { return new kernel_exception(m_env, m_msg.c_str()); }
virtual void rethrow() const { throw *this; }
@ -107,7 +106,7 @@ class has_no_type_exception : public type_checker_exception {
public:
has_no_type_exception(environment const & env, expr const & c):type_checker_exception(env), m_const(c) {}
virtual ~has_no_type_exception() {}
virtual expr const & get_main_expr() const { return m_const; }
virtual optional<expr> get_main_expr() const { return some(m_const); }
virtual char const * what() const noexcept { return "object does not have a type associated with it"; }
virtual format pp(formatter const & fmt, options const & opts) const;
virtual exception * clone() const { return new has_no_type_exception(m_env, m_const); }
@ -134,7 +133,7 @@ public:
virtual ~app_type_mismatch_exception() {}
context const & get_context() const { return m_context; }
expr const & get_application() const { return m_app; }
virtual expr const & get_main_expr() const { return get_application(); }
virtual optional<expr> get_main_expr() const { return some(get_application()); }
std::vector<expr> const & get_arg_types() const { return m_arg_types; }
virtual char const * what() const noexcept { return "application argument type mismatch"; }
virtual format pp(formatter const & fmt, options const & opts) const;
@ -159,7 +158,7 @@ public:
virtual ~function_expected_exception() {}
context const & get_context() const { return m_context; }
expr const & get_expr() const { return m_expr; }
virtual expr const & get_main_expr() const { return get_expr(); }
virtual optional<expr> get_main_expr() const { return some(get_expr()); }
virtual char const * what() const noexcept { return "function expected"; }
virtual format pp(formatter const & fmt, options const & opts) const;
virtual exception * clone() const { return new function_expected_exception(m_env, m_context, m_expr); }
@ -183,7 +182,7 @@ public:
virtual ~type_expected_exception() {}
context const & get_context() const { return m_context; }
expr const & get_expr() const { return m_expr; }
virtual expr const & get_main_expr() const { return get_expr(); }
virtual optional<expr> get_main_expr() const { return some(get_expr()); }
virtual char const * what() const noexcept { return "type expected"; }
virtual format pp(formatter const & fmt, options const & opts) const;
virtual exception * clone() const { return new type_expected_exception(m_env, m_context, m_expr); }
@ -219,7 +218,7 @@ public:
expr const & get_type() const { return m_type; }
expr const & get_value() const { return m_value; }
expr const & get_value_type() const { return m_value_type; }
virtual expr const & get_main_expr() const { return m_value; }
virtual optional<expr> get_main_expr() const { return some(m_value); }
virtual char const * what() const noexcept { return "definition type mismatch"; }
virtual format pp(formatter const & fmt, options const & opts) const;
virtual exception * clone() const { return new def_type_mismatch_exception(m_env, m_context, m_name, m_type, m_value, m_value_type); }
@ -235,7 +234,7 @@ public:
invalid_builtin_value_declaration(environment const & env, expr const & e):kernel_exception(env), m_expr(e) {}
virtual ~invalid_builtin_value_declaration() {}
virtual char const * what() const noexcept { return "invalid builtin value declaration, expression is not a builtin value"; }
virtual expr const & get_main_expr() const { return m_expr; }
virtual optional<expr> get_main_expr() const { return some(m_expr); }
virtual exception * clone() const { return new invalid_builtin_value_declaration(m_env, m_expr); }
virtual void rethrow() const { throw *this; }
};
@ -250,7 +249,7 @@ public:
invalid_builtin_value_reference(environment const & env, expr const & e):kernel_exception(env), m_expr(e) {}
virtual ~invalid_builtin_value_reference() {}
virtual char const * what() const noexcept { return "invalid builtin value reference, this kind of builtin value was not declared in the environment"; }
virtual expr const & get_main_expr() const { return m_expr; }
virtual optional<expr> get_main_expr() const { return some(m_expr); }
virtual exception * clone() const { return new invalid_builtin_value_reference(m_env, m_expr); }
virtual void rethrow() const { throw *this; }
};
@ -264,7 +263,7 @@ public:
unexpected_metavar_occurrence(environment const & env, expr const & e):kernel_exception(env), m_expr(e) {}
virtual ~unexpected_metavar_occurrence() {}
virtual char const * what() const noexcept { return "unexpected metavariable occurrence"; }
virtual expr const & get_main_expr() const { return m_expr; }
virtual optional<expr> get_main_expr() const { return some(m_expr); }
virtual exception * clone() const { return new unexpected_metavar_occurrence(m_env, m_expr); }
virtual void rethrow() const { throw *this; }
};

62
src/kernel/metavar.cpp
View file

@ -48,7 +48,7 @@ public:
append(r, m_jsts);
}
virtual expr const & get_main_expr() const { return m_expr; }
virtual optional<expr> get_main_expr() const { return some(m_expr); }
};
void swap(metavar_env & a, metavar_env & b) {
@ -77,7 +77,7 @@ metavar_env::metavar_env():
metavar_env(g_default_name) {
}
expr metavar_env::mk_metavar(context const & ctx, expr const & type) {
expr metavar_env::mk_metavar(context const & ctx, optional<expr> const & type) {
inc_timestamp();
name m = m_name_generator.next();
expr r = ::lean::mk_metavar(m);
@ -115,7 +115,7 @@ expr metavar_env::get_type(name const & m) {
auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
lean_assert(it);
if (it->m_type) {
return it->m_type;
return *(it->m_type);
} else {
expr t = mk_metavar(get_context(m));
it->m_type = t;
@ -134,13 +134,17 @@ bool metavar_env::has_type(expr const & m) const {
return has_type(metavar_name(m));
}
justification metavar_env::get_justification(expr const & m) const {
optional<justification> metavar_env::get_justification(expr const & m) const {
lean_assert(is_metavar(m));
return get_justification(metavar_name(m));
}
justification metavar_env::get_justification(name const & m) const {
return get_subst_jst(m).second;
optional<justification> metavar_env::get_justification(name const & m) const {
auto r = get_subst_jst(m);
if (r)
return optional<justification>(r->second);
else
return optional<justification>();
}
bool metavar_env::is_assigned(name const & m) const {
@ -187,44 +191,53 @@ expr apply_local_context(expr const & a, local_context const & lctx) {
}
}
std::pair<expr, justification> metavar_env::get_subst_jst(expr const & m) const {
optional<std::pair<expr, justification>> metavar_env::get_subst_jst(expr const & m) const {
lean_assert(is_metavar(m));
auto p = get_subst_jst(metavar_name(m));
expr r = p.first;
if (p.first) {
if (p) {
expr r = p->first;
local_context const & lctx = metavar_lctx(m);
if (lctx)
r = apply_local_context(r, lctx);
return mk_pair(r, p.second);
return some(mk_pair(r, p->second));
} else {
return p;
}
}
std::pair<expr, justification> metavar_env::get_subst_jst(name const & m) const {
optional<std::pair<expr, justification>> metavar_env::get_subst_jst(name const & m) const {
auto it = const_cast<metavar_env*>(this)->m_metavar_data.splay_find(m);
if (it->m_subst) {
if (has_assigned_metavar(it->m_subst, *this)) {
expr s = *(it->m_subst);
if (has_assigned_metavar(s, *this)) {
buffer<justification> jsts;
expr new_subst = instantiate_metavars(it->m_subst, *this, jsts);
expr new_subst = instantiate_metavars(s, *this, jsts);
if (!jsts.empty()) {
it->m_justification = justification(new normalize_assignment_justification(it->m_context, it->m_subst, it->m_justification,
it->m_justification = justification(new normalize_assignment_justification(it->m_context, s, it->m_justification,
jsts.size(), jsts.data()));
it->m_subst = new_subst;
}
}
return mk_pair(it->m_subst, it->m_justification);
return optional<std::pair<expr, justification>>(std::pair<expr, justification>(*(it->m_subst), it->m_justification));
} else {
return mk_pair(expr(), justification());
return optional<std::pair<expr, justification>>();
}
}
expr metavar_env::get_subst(name const & m) const {
return get_subst_jst(m).first;
optional<expr> metavar_env::get_subst(name const & m) const {
auto r = get_subst_jst(m);
if (r)
return optional<expr>(r->first);
else
return optional<expr>();
}
expr metavar_env::get_subst(expr const & m) const {
return get_subst_jst(m).first;
optional<expr> metavar_env::get_subst(expr const & m) const {
auto r = get_subst_jst(m);
if (r)
return optional<expr>(r->first);
else
return optional<expr>();
}
class instantiate_metavars_proc : public replace_visitor {
@ -240,8 +253,9 @@ protected:
virtual expr visit_metavar(expr const & m, context const & ctx) {
if (is_metavar(m) && m_menv.is_assigned(m)) {
auto p = m_menv.get_subst_jst(m);
expr r = p.first;
push_back(p.second);
lean_assert(p);
expr r = p->first;
push_back(p->second);
if (has_assigned_metavar(r, m_menv)) {
return visit(r, ctx);
} else {
@ -275,7 +289,7 @@ public:
};
expr instantiate_metavars(expr const & e, metavar_env const & menv, buffer<justification> & jsts) {
if (!e || !has_metavar(e)) {
if (!has_metavar(e)) {
return e;
} else {
return instantiate_metavars_proc(menv, jsts)(e);
@ -365,7 +379,7 @@ bool has_metavar(expr const & e, expr const & m, metavar_env const & menv) {
return
is_metavar(m2) &&
((metavar_name(m) == metavar_name(m2)) ||
(menv.is_assigned(m2) && has_metavar(menv.get_subst(m2), m, menv)));
(menv.is_assigned(m2) && has_metavar(*menv.get_subst(m2), m, menv)));
}));
} else {
return false;

30
src/kernel/metavar.h
View file

@ -25,11 +25,11 @@ namespace lean {
*/
class metavar_env {
struct data {
expr m_subst; // substitution
expr m_type; // type of the metavariable
optional<expr> m_subst; // substitution
optional<expr> m_type; // type of the metavariable
context m_context; // context where the metavariable was defined
justification m_justification; // justification for assigned metavariables.
data(expr const & t = expr(), context const & ctx = context()):m_type(t), m_context(ctx) {}
data(optional<expr> const & t = optional<expr>(), context const & ctx = context()):m_type(t), m_context(ctx) {}
};
typedef splay_map<name, data, name_quick_cmp> name2data;
@ -62,7 +62,7 @@ public:
/**
\brief Create a new metavariable in the given context and with the given type.
*/
expr mk_metavar(context const & ctx = context(), expr const & type = expr());
expr mk_metavar(context const & ctx = context(), optional<expr> const & type = optional<expr>());
/**
\brief Return the context where the given metavariable was created.
@ -93,21 +93,16 @@ public:
/**
\brief Return the substitution and justification for the given metavariable.
If the metavariable is not assigned in this substitution, then it returns the null
expression.
*/
std::pair<expr, justification> get_subst_jst(name const & m) const;
std::pair<expr, justification> get_subst_jst(expr const & m) const;
optional<std::pair<expr, justification>> get_subst_jst(name const & m) const;
optional<std::pair<expr, justification>> get_subst_jst(expr const & m) const;
/**
\brief Return the justification for an assigned metavariable.
\pre is_metavar(m)
\pre is_assigned(m)
*/
justification get_justification(expr const & m) const;
justification get_justification(name const & m) const;
optional<justification> get_justification(expr const & m) const;
optional<justification> get_justification(name const & m) const;
/**
\brief Return true iff the metavariable named \c m is assigned in this substitution.
@ -142,13 +137,10 @@ public:
\brief Return the substitution associated with the given metavariable
in this substitution.
If the metavariable is not assigned in this substitution, then it returns the null
expression.
\pre is_metavar(m)
*/
expr get_subst(expr const & m) const;
expr get_subst(name const & m) const;
optional<expr> get_subst(expr const & m) const;
optional<expr> get_subst(name const & m) const;
/**
\brief Apply f to each substitution in the metavariable environment.
@ -157,7 +149,7 @@ public:
void for_each_subst(F f) const {
m_metavar_data.for_each([&](name const & k, data const & d) {
if (d.m_subst)
f(k, d.m_subst);
f(k, *(d.m_subst));
});
}
};

21
src/kernel/normalizer.cpp
View file

@ -40,7 +40,7 @@ enum class svalue_kind { Expr, Closure, BoundedVar };
class svalue {
svalue_kind m_kind;
unsigned m_bvar;
expr m_expr;
optional<expr> m_expr;
value_stack m_ctx;
public:
svalue() {}
@ -54,7 +54,7 @@ public:
bool is_closure() const { return kind() == svalue_kind::Closure; }
bool is_bounded_var() const { return kind() == svalue_kind::BoundedVar; }
expr const & get_expr() const { lean_assert(is_expr() || is_closure()); return m_expr; }
expr const & get_expr() const { lean_assert(is_expr() || is_closure()); return *m_expr; }
value_stack const & get_ctx() const { lean_assert(is_closure()); return m_ctx; }
unsigned get_var_idx() const { lean_assert(is_bounded_var()); return m_bvar; }
};
@ -113,7 +113,7 @@ class normalizer::imp {
save_context save(*this); // it restores the context and cache
m_ctx = entry_c;
unsigned k = m_ctx.size();
return svalue(reify(normalize(entry.get_body(), value_stack(), k), k));
return svalue(reify(normalize(*(entry.get_body()), value_stack(), k), k));
} else {
return svalue(entry_c.size());
}
@ -123,12 +123,10 @@ class normalizer::imp {
expr reify_closure(expr const & a, value_stack const & s, unsigned k) {
lean_assert(is_lambda(a));
expr new_t = reify(normalize(abst_domain(a), s, k), k);
expr new_b;
{
cache::mk_scope sc(m_cache);
new_b = reify(normalize(abst_body(a), extend(s, svalue(k)), k+1), k+1);
return mk_lambda(abst_name(a), new_t, reify(normalize(abst_body(a), extend(s, svalue(k)), k+1), k+1));
}
return mk_lambda(abst_name(a), new_t, new_b);
}
/** \brief Convert the value \c v back into an expression in a context that contains \c k binders. */
@ -236,9 +234,9 @@ class normalizer::imp {
for (; i < n; i++)
new_args.push_back(reify(normalize(arg(a, i), s, k), k));
if (is_value(new_f)) {
expr m;
if (to_value(new_f).normalize(new_args.size(), new_args.data(), m)) {
r = normalize(m, s, k);
optional<expr> m = to_value(new_f).normalize(new_args.size(), new_args.data());
if (m) {
r = normalize(*m, s, k);
break;
}
}
@ -263,12 +261,11 @@ class normalizer::imp {
break;
case expr_kind::Pi: {
expr new_t = reify(normalize(abst_domain(a), s, k), k);
expr new_b;
{
cache::mk_scope sc(m_cache);
new_b = reify(normalize(abst_body(a), extend(s, svalue(k)), k+1), k+1);
}
expr new_b = reify(normalize(abst_body(a), extend(s, svalue(k)), k+1), k+1);
r = svalue(mk_pi(abst_name(a), new_t, new_b));
}
break;
}
case expr_kind::Let: {

10
src/kernel/printer.cpp
View file

@ -138,7 +138,7 @@ struct print_expr_fn {
out() << "let " << let_name(a);
if (let_type(a)) {
out() << " : ";
print(let_type(a), c);
print(*let_type(a), c);
}
out() << " := ";
print(let_value(a), c);
@ -182,10 +182,10 @@ static void display_context_core(std::ostream & out, context const & ctx) {
if (!empty(tail_ctx))
out << "; ";
out << head.get_name();
if (head.get_domain())
out << " : " << mk_pair(head.get_domain(), tail_ctx);
if (head.get_body()) {
out << " := " << mk_pair(head.get_body(), tail_ctx);
if (optional<expr> const & d = head.get_domain())
out << " : " << mk_pair(*d, tail_ctx);
if (optional<expr> const & b = head.get_body()) {
out << " := " << mk_pair(*b, tail_ctx);
}
}
}

14
src/kernel/replace_fn.h
View file

@ -47,10 +47,15 @@ class replace_fn {
F m_f;
P m_post;
optional<expr> apply(optional<expr> const & e, unsigned offset) {
if (e)
return optional<expr>(apply(*e, offset));
else
return optional<expr>();
}
expr apply(expr const & e, unsigned offset) {
check_system("expression replacer");
if (!e)
return e;
bool sh = false;
if (is_shared(e)) {
expr_cell_offset p(e.raw(), offset);
@ -81,9 +86,8 @@ class replace_fn {
r = update_abst(e, [=](expr const & t, expr const & b) { return std::make_pair(apply(t, offset), apply(b, offset+1)); });
break;
case expr_kind::Let:
r = update_let(e, [=](expr const & t, expr const & v, expr const & b) {
expr new_t = t ? apply(t, offset) : expr();
return std::make_tuple(new_t, apply(v, offset), apply(b, offset+1));
r = update_let(e, [=](optional<expr> const & t, expr const & v, expr const & b) {
return std::make_tuple(apply(t, offset), apply(v, offset), apply(b, offset+1));
});
break;
}

58
src/kernel/replace_visitor.cpp
View file

@ -15,11 +15,7 @@ expr replace_visitor::visit_var(expr const & e, context const &) { lean_assert(i
expr replace_visitor::visit_metavar(expr const & e, context const &) { lean_assert(is_metavar(e)); return e; }
expr replace_visitor::visit_constant(expr const & e, context const & ctx) {
lean_assert(is_constant(e));
if (const_type(e)) {
return update_const(e, visit(const_type(e), ctx));
} else {
return e;
}
}
expr replace_visitor::visit_app(expr const & e, context const & ctx) {
lean_assert(is_app(e));
@ -33,12 +29,11 @@ expr replace_visitor::visit_abst(expr const & e, context const & ctx) {
lean_assert(is_abstraction(e));
return update_abst(e, [&](expr const & t, expr const & b) {
expr new_t = visit(t, ctx);
expr new_b;
{
cache::mk_scope sc(m_cache);
new_b = visit(b, extend(ctx, abst_name(e), new_t));
}
expr new_b = visit(b, extend(ctx, abst_name(e), new_t));
return std::make_pair(new_t, new_b);
}
});
}
expr replace_visitor::visit_lambda(expr const & e, context const & ctx) {
@ -49,23 +44,26 @@ expr replace_visitor::visit_pi(expr const & e, context const & ctx) {
lean_assert(is_pi(e));
return visit_abst(e, ctx);
}
expr replace_visitor::visit_let(expr const & e, context const & ctx) {
lean_assert(is_let(e));
return update_let(e, [&](expr const & t, expr const & v, expr const & b) {
expr new_t = visit(t, ctx);
return update_let(e, [&](optional<expr> const & t, expr const & v, expr const & b) {
optional<expr> new_t = visit(t, ctx);
expr new_v = visit(v, ctx);
expr new_b;
{
cache::mk_scope sc(m_cache);
new_b = visit(b, extend(ctx, let_name(e), new_t, new_v));
}
expr new_b = visit(b, extend(ctx, let_name(e), new_t, new_v));
return std::make_tuple(new_t, new_v, new_b);
}
});
}
expr replace_visitor::save_result(expr const & e, expr && r, bool shared) {
if (shared)
m_cache.insert(std::make_pair(e, r));
return r;
}
expr replace_visitor::visit(expr const & e, context const & ctx) {
check_system("expression replacer");
if (!e)
return e;
bool shared = false;
if (is_shared(e)) {
shared = true;
@ -74,23 +72,25 @@ expr replace_visitor::visit(expr const & e, context const & ctx) {
return it->second;
}
expr r;
switch (e.kind()) {
case expr_kind::Type: r = visit_type(e, ctx); break;
case expr_kind::Value: r = visit_value(e, ctx); break;
case expr_kind::Constant: r = visit_constant(e, ctx); break;
case expr_kind::Var: r = visit_var(e, ctx); break;
case expr_kind::MetaVar: r = visit_metavar(e, ctx); break;
case expr_kind::App: r = visit_app(e, ctx); break;
case expr_kind::Eq: r = visit_eq(e, ctx); break;
case expr_kind::Lambda: r = visit_lambda(e, ctx); break;
case expr_kind::Pi: r = visit_pi(e, ctx); break;
case expr_kind::Let: r = visit_let(e, ctx); break;
case expr_kind::Type: return save_result(e, visit_type(e, ctx), shared);
case expr_kind::Value: return save_result(e, visit_value(e, ctx), shared);
case expr_kind::Constant: return save_result(e, visit_constant(e, ctx), shared);
case expr_kind::Var: return save_result(e, visit_var(e, ctx), shared);
case expr_kind::MetaVar: return save_result(e, visit_metavar(e, ctx), shared);
case expr_kind::App: return save_result(e, visit_app(e, ctx), shared);
case expr_kind::Eq: return save_result(e, visit_eq(e, ctx), shared);
case expr_kind::Lambda: return save_result(e, visit_lambda(e, ctx), shared);
case expr_kind::Pi: return save_result(e, visit_pi(e, ctx), shared);
case expr_kind::Let: return save_result(e, visit_let(e, ctx), shared);
}
if (shared)
m_cache.insert(std::make_pair(e, r));
return r;
lean_unreachable(); // LCOV_EXCL_LINE
}
optional<expr> replace_visitor::visit(optional<expr> const & e, context const & ctx) {
if (e)
return some(visit(*e, ctx));
else
return optional<expr>();
}
}

3
src/kernel/replace_visitor.h
View file

@ -24,7 +24,7 @@ protected:
typedef scoped_map<expr, expr, expr_hash_alloc, expr_eqp> cache;
cache m_cache;
context m_ctx;
expr save_result(expr const & e, expr && r, bool shared);
virtual expr visit_type(expr const &, context const &);
virtual expr visit_value(expr const &, context const &);
virtual expr visit_constant(expr const &, context const &);
@ -37,6 +37,7 @@ protected:
virtual expr visit_pi(expr const &, context const &);
virtual expr visit_let(expr const &, context const &);
virtual expr visit(expr const &, context const &);
optional<expr> visit(optional<expr> const &, context const &);
void set_ctx(context const & ctx) {
if (!is_eqp(m_ctx, ctx)) {

96
src/kernel/type_checker.cpp
View file

@ -39,14 +39,6 @@ class type_checker::imp {
return m_normalizer(e, ctx);
}
expr lookup(context const & c, unsigned i) {
auto p = lookup_ext(c, i);
context_entry const & def = p.first;
context const & def_c = p.second;
lean_assert(c.size() > def_c.size());
return lift_free_vars(def.get_domain(), c.size() - def_c.size());
}
expr check_pi(expr const & e, expr const & s, context const & ctx) {
if (is_pi(e))
return e;
@ -84,6 +76,12 @@ class type_checker::imp {
throw type_expected_exception(env(), ctx, s);
}
expr save_result(expr const & e, expr const & r, bool shared) {
if (shared)
m_cache.insert(e, r);
return r;
}
expr infer_type_core(expr const & e, context const & ctx) {
check_system("type checker");
bool shared = false;
@ -94,36 +92,44 @@ class type_checker::imp {
return it->second;
}
expr r;
switch (e.kind()) {
case expr_kind::MetaVar:
if (m_menv) {
if (m_menv->is_assigned(e))
return infer_type_core(m_menv->get_subst(e), ctx);
return infer_type_core(*(m_menv->get_subst(e)), ctx);
else
return m_menv->get_type(e);
} else {
throw unexpected_metavar_occurrence(env(), e);
}
break;
case expr_kind::Constant: {
if (const_type(e)) {
r = const_type(e);
return save_result(e, *const_type(e), shared);
} else {
object const & obj = env().get_object(const_name(e));
if (obj.has_type())
r = obj.get_type();
return save_result(e, obj.get_type(), shared);
else
throw has_no_type_exception(env(), e);
}
break;
}
case expr_kind::Var:
r = lookup(ctx, var_idx(e));
break;
case expr_kind::Var: {
unsigned i = var_idx(e);
auto p = lookup_ext(ctx, i);
context_entry const & def = p.first;
context const & def_ctx = p.second;
lean_assert(ctx.size() > def_ctx.size());
if (optional<expr> const & d = def.get_domain()) {
return save_result(e, lift_free_vars(*d, ctx.size() - def_ctx.size()), shared);
} else {
optional<expr> const & b = def.get_body();
lean_assert(b);
expr t = infer_type_core(*b, def_ctx);
return save_result(e, lift_free_vars(t, ctx.size() - def_ctx.size()), shared);
}
}
case expr_kind::Type:
r = mk_type(ty_level(e) + 1);
break;
return save_result(e, mk_type(ty_level(e) + 1), shared);
case expr_kind::App: {
unsigned num = num_args(e);
lean_assert(num >= 2);
@ -146,81 +152,71 @@ class type_checker::imp {
else
f_t = instantiate(abst_body(f_t), c);
i++;
if (i == num) {
r = f_t;
break;
}
if (i == num)
return save_result(e, f_t, shared);
f_t = check_pi(f_t, e, ctx);
}
break;
}
case expr_kind::Eq:
infer_type_core(eq_lhs(e), ctx);
infer_type_core(eq_rhs(e), ctx);
r = mk_bool_type();
break;
return save_result(e, mk_bool_type(), shared);
case expr_kind::Lambda: {
expr d = infer_type_core(abst_domain(e), ctx);
check_type(d, abst_domain(e), ctx);
expr t;
{
cache::mk_scope sc(m_cache);
t = infer_type_core(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)));
return save_result(e,
mk_pi(abst_name(e), abst_domain(e), infer_type_core(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)))),
shared);
}
r = mk_pi(abst_name(e), abst_domain(e), t);
break;
}
case expr_kind::Pi: {
expr t1 = check_type(infer_type_core(abst_domain(e), ctx), abst_domain(e), ctx);
expr t2;
optional<expr> t2;
context new_ctx = extend(ctx, abst_name(e), abst_domain(e));
{
cache::mk_scope sc(m_cache);
t2 = check_type(infer_type_core(abst_body(e), new_ctx), abst_body(e), new_ctx);
}
if (is_type(t1) && is_type(t2)) {
r = mk_type(max(ty_level(t1), ty_level(t2)));
if (is_type(t1) && is_type(*t2)) {
return save_result(e, mk_type(max(ty_level(t1), ty_level(*t2))), shared);
} else {
lean_assert(m_uc);
justification jst = mk_max_type_justification(ctx, e);
r = m_menv->mk_metavar(ctx);
m_uc->push_back(mk_max_constraint(new_ctx, lift_free_vars(t1, 0, 1), t2, r, jst));
expr r = m_menv->mk_metavar(ctx);
m_uc->push_back(mk_max_constraint(new_ctx, lift_free_vars(t1, 0, 1), *t2, r, jst));
return save_result(e, r, shared);
}
break;
}
case expr_kind::Let: {
expr lt = infer_type_core(let_value(e), ctx);
if (let_type(e)) {
expr ty = infer_type_core(let_type(e), ctx);
check_type(ty, let_type(e), ctx); // check if it is really a type
auto mk_justification = [&](){ return mk_def_type_match_justification(ctx, let_name(e), let_value(e)); }; // thunk for creating justification object if needed
if (!is_convertible(lt, let_type(e), ctx, mk_justification))
throw def_type_mismatch_exception(env(), ctx, let_name(e), let_type(e), let_value(e), lt);
expr ty = infer_type_core(*let_type(e), ctx);
check_type(ty, *let_type(e), ctx); // check if it is really a type
// thunk for creating justification object if needed
auto mk_justification = [&](){ return mk_def_type_match_justification(ctx, let_name(e), let_value(e)); };
if (!is_convertible(lt, *let_type(e), ctx, mk_justification))
throw def_type_mismatch_exception(env(), ctx, let_name(e), *let_type(e), let_value(e), lt);
}
{
cache::mk_scope sc(m_cache);
expr t = infer_type_core(let_body(e), extend(ctx, let_name(e), lt, let_value(e)));
r = instantiate(t, let_value(e));
return save_result(e, instantiate(t, let_value(e)), shared);
}
break;
}
case expr_kind::Value: {
// Check if the builtin value (or its set) is declared in the environment.
name const & n = to_value(e).get_name();
object const & obj = env().get_object(n);
if (obj && ((obj.is_builtin() && obj.get_value() == e) || (obj.is_builtin_set() && obj.in_builtin_set(e)))) {
r = to_value(e).get_type();
return save_result(e, to_value(e).get_type(), shared);
} else {
throw invalid_builtin_value_reference(env(), e);
}
break;
}
}
if (shared) {
m_cache.insert(e, r);
}
return r;
lean_unreachable(); // LCOV_EXCL_LINE
}
bool is_convertible_core(expr const & given, expr const & expected) {

20
src/kernel/type_checker_justification.cpp
View file

@ -23,8 +23,8 @@ format function_expected_justification_cell::pp_header(formatter const & fmt, op
void function_expected_justification_cell::get_children(buffer<justification_cell*> &) const {
}
expr const & function_expected_justification_cell::get_main_expr() const {
return m_app;
optional<expr> function_expected_justification_cell::get_main_expr() const {
return some(m_app);
}
app_type_match_justification_cell::~app_type_match_justification_cell() {
@ -51,8 +51,8 @@ format app_type_match_justification_cell::pp_header(formatter const & fmt, optio
void app_type_match_justification_cell::get_children(buffer<justification_cell*> &) const {
}
expr const & app_type_match_justification_cell::get_main_expr() const {
return m_app;
optional<expr> app_type_match_justification_cell::get_main_expr() const {
return some(m_app);
}
type_expected_justification_cell::~type_expected_justification_cell() {
@ -70,8 +70,8 @@ format type_expected_justification_cell::pp_header(formatter const & fmt, option
void type_expected_justification_cell::get_children(buffer<justification_cell*> &) const {
}
expr const & type_expected_justification_cell::get_main_expr() const {
return m_type;
optional<expr> type_expected_justification_cell::get_main_expr() const {
return some(m_type);
}
def_type_match_justification_cell::~def_type_match_justification_cell() {
@ -88,8 +88,8 @@ format def_type_match_justification_cell::pp_header(formatter const &, options c
void def_type_match_justification_cell::get_children(buffer<justification_cell*> &) const {
}
expr const & def_type_match_justification_cell::get_main_expr() const {
return m_value;
optional<expr> def_type_match_justification_cell::get_main_expr() const {
return some(m_value);
}
type_match_justification_cell::~type_match_justification_cell() {
@ -102,7 +102,7 @@ format type_match_justification_cell::pp_header(formatter const &, options const
void type_match_justification_cell::get_children(buffer<justification_cell*> &) const {
}
expr const & type_match_justification_cell::get_main_expr() const {
return m_value;
optional<expr> type_match_justification_cell::get_main_expr() const {
return some(m_value);
}
}

10
src/kernel/type_checker_justification.h
View file

@ -29,7 +29,7 @@ public:
virtual ~function_expected_justification_cell();
virtual format pp_header(formatter const & fmt, options const & opts) const;
virtual void get_children(buffer<justification_cell*> &) const;
virtual expr const & get_main_expr() const;
virtual optional<expr> get_main_expr() const;
context const & get_context() const { return m_ctx; }
expr const & get_app() const { return m_app; }
};
@ -54,7 +54,7 @@ public:
virtual ~app_type_match_justification_cell();
virtual format pp_header(formatter const & fmt, options const & opts) const;
virtual void get_children(buffer<justification_cell*> &) const;
virtual expr const & get_main_expr() const;
virtual optional<expr> get_main_expr() const;
context const & get_context() const { return m_ctx; }
expr const & get_app() const { return m_app; }
unsigned get_arg_pos() const { return m_i; }
@ -77,7 +77,7 @@ public:
virtual ~type_expected_justification_cell();
virtual format pp_header(formatter const & fmt, options const & opts) const;
virtual void get_children(buffer<justification_cell*> &) const;
virtual expr const & get_main_expr() const;
virtual optional<expr> get_main_expr() const;
context const & get_context() const { return m_ctx; }
expr const & get_type() const { return m_type; }
};
@ -114,7 +114,7 @@ public:
virtual ~def_type_match_justification_cell();
virtual format pp_header(formatter const & fmt, options const & opts) const;
virtual void get_children(buffer<justification_cell*> &) const;
virtual expr const & get_main_expr() const;
virtual optional<expr> get_main_expr() const;
context const & get_context() const { return m_ctx; }
name const & get_name() const { return m_name; }
expr const & get_value() const { return m_value; }
@ -133,7 +133,7 @@ public:
virtual ~type_match_justification_cell();
virtual format pp_header(formatter const & fmt, options const & opts) const;
virtual void get_children(buffer<justification_cell*> &) const;
virtual expr const & get_main_expr() const;
virtual optional<expr> get_main_expr() const;
context const & get_context() const { return m_ctx; }
expr const & get_type() const { return m_type; }
expr const & get_value() const { return m_value; }

21
src/library/arith/int.cpp
View file

@ -72,12 +72,11 @@ template<char const * Name, typename F>
class int_bin_op : public const_value {
public:
int_bin_op():const_value(name("Int", Name), Int >> (Int >> Int)) {}
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
r = mk_int_value(F()(int_value_numeral(args[1]), int_value_numeral(args[2])));
return true;
return some(mk_int_value(F()(int_value_numeral(args[1]), int_value_numeral(args[2]))));
} else {
return false;
return optional<expr>();
}
}
};
@ -107,12 +106,11 @@ MK_BUILTIN(int_div_fn, int_div_value);
class int_le_value : public const_value {
public:
int_le_value():const_value(name{"Int", "le"}, Int >> (Int >> Bool)) {}
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
r = mk_bool_value(int_value_numeral(args[1]) <= int_value_numeral(args[2]));
return true;
return some(mk_bool_value(int_value_numeral(args[1]) <= int_value_numeral(args[2])));
} else {
return false;
return optional<expr>();
}
}
};
@ -133,12 +131,11 @@ MK_CONSTANT(int_gt_fn, name({"Int", "gt"}));
class nat_to_int_value : public const_value {
public:
nat_to_int_value():const_value("nat_to_int", Nat >> Int) {}
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
if (num_args == 2 && is_nat_value(args[1])) {
r = mk_int_value(nat_value_numeral(args[1]));
return true;
return some(mk_int_value(nat_value_numeral(args[1])));
} else {
return false;
return optional<expr>();
}
}
};

14
src/library/arith/nat.cpp
View file

@ -66,12 +66,11 @@ template<char const * Name, typename F>
class nat_bin_op : public const_value {
public:
nat_bin_op():const_value(name("Nat", Name), Nat >> (Nat >> Nat)) {}
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) {
r = mk_nat_value(F()(nat_value_numeral(args[1]), nat_value_numeral(args[2])));
return true;
return some(mk_nat_value(F()(nat_value_numeral(args[1]), nat_value_numeral(args[2]))));
} else {
return false;
return optional<expr>();
}
}
};
@ -95,12 +94,11 @@ MK_BUILTIN(nat_mul_fn, nat_mul_value);
class nat_le_value : public const_value {
public:
nat_le_value():const_value(name{"Nat", "le"}, Nat >> (Nat >> Bool)) {}
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) {
r = mk_bool_value(nat_value_numeral(args[1]) <= nat_value_numeral(args[2]));
return true;
return some(mk_bool_value(nat_value_numeral(args[1]) <= nat_value_numeral(args[2])));
} else {
return false;
return optional<expr>();
}
}
};

21
src/library/arith/real.cpp
View file

@ -75,12 +75,11 @@ template<char const * Name, typename F>
class real_bin_op : public const_value {
public:
real_bin_op():const_value(name("Real", Name), Real >> (Real >> Real)) {}
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
r = mk_real_value(F()(real_value_numeral(args[1]), real_value_numeral(args[2])));
return true;
return some(mk_real_value(F()(real_value_numeral(args[1]), real_value_numeral(args[2]))));
} else {
return false;
return optional<expr>();
}
}
};
@ -117,12 +116,11 @@ MK_BUILTIN(real_div_fn, real_div_value);
class real_le_value : public const_value {
public:
real_le_value():const_value(name{"Real", "le"}, Real >> (Real >> Bool)) {}
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
r = mk_bool_value(real_value_numeral(args[1]) <= real_value_numeral(args[2]));
return true;
return some(mk_bool_value(real_value_numeral(args[1]) <= real_value_numeral(args[2])));
} else {
return false;
return optional<expr>();
}
}
};
@ -167,12 +165,11 @@ void import_real(environment & env) {
class int_to_real_value : public const_value {
public:
int_to_real_value():const_value("int_to_real", Int >> Real) {}
virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
if (num_args == 2 && is_int_value(args[1])) {
r = mk_real_value(mpq(int_value_numeral(args[1])));
return true;
return some(mk_real_value(mpq(int_value_numeral(args[1]))));
} else {
return false;
return optional<expr>();
}
}
};

19
src/library/cast/cast.cpp
View file

@ -27,14 +27,13 @@ public:
virtual ~cast_fn_value() {}
virtual expr get_type() const { return m_type; }
virtual name get_name() const { return g_cast_name; }
virtual bool normalize(unsigned num_as, expr const * as, expr & r) const {
virtual optional<expr> normalize(unsigned num_as, expr const * as) const {
if (num_as > 4 && as[1] == as[2]) {
// Cast T T H a == a
if (num_as == 5)
r = as[4];
return some(as[4]);
else
r = mk_app(num_as - 4, as + 4);
return true;
return some(mk_app(num_as - 4, as + 4));
} else if (is_app(as[4]) &&
arg(as[4], 0) == mk_Cast_fn() &&
num_args(as[4]) == 5 &&
@ -49,14 +48,13 @@ public:
expr const & a = arg(nested, 4);
expr c = Cast(T3, T2, Trans(TypeU, T3, T1, T2, H1, H2), a);
if (num_as == 5) {
r = c;
return optional<expr>(c);
} else {
buffer<expr> new_as;
new_as.push_back(c);
new_as.append(num_as - 5, as + 5);
r = mk_app(new_as);
return optional<expr>(mk_app(new_as));
}
return true;
} else if (num_as > 5 && is_pi(as[1]) && is_pi(as[2])) {
// cast T1 T2 H f a_1 ... a_k
// Propagate application over cast.
@ -86,16 +84,15 @@ public:
expr B1_eq_B2_at_a_1p = RanInj(A1, A2, B1f, B2f, H, a_1p);
expr fa_1_B2 = Cast(B1, B2, B1_eq_B2_at_a_1p, fa_1);
if (num_as == 6) {
r = fa_1_B2;
return optional<expr>(fa_1_B2);
} else {
buffer<expr> new_as;
new_as.push_back(fa_1_B2);
new_as.append(num_as - 6, as + 6);
r = mk_app(new_as);
return optional<expr>(mk_app(new_as));
}
return true;
} else {
return false;
return optional<expr>();
}
}
};

37
src/library/context_to_lambda.cpp
View file

@ -13,12 +13,18 @@ expr context_to_lambda(context::iterator it, context::iterator const & end, expr
return e;
} else {
context_entry const & entry = *it;
expr t;
if (entry.get_body())
t = mk_app(g_fake, entry.get_domain(), entry.get_body());
optional<expr> t;
optional<expr> const & d = entry.get_domain();
optional<expr> const & b = entry.get_body();
lean_assert(b || d);
if (b && d)
t = mk_app(g_fake, *d, *b);
else if (d)
t = mk_app(g_fake, *d, g_fake);
else
t = mk_app(g_fake, entry.get_domain());
return context_to_lambda(++it, end, mk_lambda(entry.get_name(), t, e));
t = mk_app(g_fake, g_fake, *b);
lean_assert(t);
return context_to_lambda(++it, end, mk_lambda(entry.get_name(), *t, e));
}
}
expr context_to_lambda(context const & c, expr const & e) {
@ -31,16 +37,21 @@ name const & fake_context_name(expr const & e) {
lean_assert(is_fake_context(e));
return abst_name(e);
}
expr const & fake_context_domain(expr const & e) {
optional<expr> fake_context_domain(expr const & e) {
lean_assert(is_fake_context(e));
return arg(abst_domain(e), 1);
}
expr const & fake_context_value(expr const & e) {
lean_assert(is_fake_context(e));
if (num_args(abst_domain(e)) > 2)
return arg(abst_domain(e), 2);
expr r = arg(abst_domain(e), 1);
if (!is_eqp(r, g_fake))
return optional<expr>(r);
else
return expr::null();
return optional<expr>();
}
optional<expr> fake_context_value(expr const & e) {
lean_assert(is_fake_context(e));
expr r = arg(abst_domain(e), 2);
if (!is_eqp(r, g_fake))
return optional<expr>(r);
else
return optional<expr>();
}
expr const & fake_context_rest(expr const & e) {
return abst_body(e);

7
src/library/context_to_lambda.h
View file

@ -42,15 +42,14 @@ name const & fake_context_name(expr const & e);
\pre is_fake_context(e)
*/
expr const & fake_context_domain(expr const & e);
optional<expr> fake_context_domain(expr const & e);
/**
\brief Return the value V_1 of the head of the (fake) context
\brief Return (if available) the value V_1 of the head of the (fake) context
(lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
\pre is_fake_context(e)
\remark If the head does not have a value, then return a null expression
*/
expr const & fake_context_value(expr const & e);
optional<expr> fake_context_value(expr const & e);
/**
\brief Return the rest (lambda (n_2 : (fake T_2 V_2)) ... (lambda (n_k : (fake T_k V_k)) e)) of the fake context
(lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))

39
src/library/deep_copy.cpp
View file

@ -13,8 +13,20 @@ namespace lean {
class deep_copy_fn {
expr_cell_map<expr> m_cache;
expr save_result(expr const & a, expr && r, bool shared) {
if (shared)
m_cache.insert(std::make_pair(a.raw(), r));
return r;
}
optional<expr> apply(optional<expr> const & a) {
if (a)
return some(apply(*a));
else
return a;
}
expr apply(expr const & a) {
if (!a) return a;
bool sh = false;
if (is_shared(a)) {
auto r = m_cache.find(a.raw());
@ -22,33 +34,30 @@ class deep_copy_fn {
return r->second;
sh = true;
}
expr r;
switch (a.kind()) {
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
r = copy(a); break; // shallow copy is equivalent to deep copy for these ones.
return save_result(a, copy(a), sh);
case expr_kind::App: {
buffer<expr> new_args;
for (expr const & old_arg : args(a))
new_args.push_back(apply(old_arg));
r = mk_app(new_args);
break;
return save_result(a, mk_app(new_args), sh);
}
case expr_kind::Eq: r = mk_eq(apply(eq_lhs(a)), apply(eq_rhs(a))); break;
case expr_kind::Lambda: r = mk_lambda(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))); break;
case expr_kind::Pi: r = mk_pi(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))); break;
case expr_kind::Let: r = mk_let(let_name(a), apply(let_type(a)), apply(let_value(a)), apply(let_body(a))); break;
case expr_kind::Eq: return save_result(a, mk_eq(apply(eq_lhs(a)), apply(eq_rhs(a))), sh);
case expr_kind::Lambda: return save_result(a, mk_lambda(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))), sh);
case expr_kind::Pi: return save_result(a, mk_pi(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))), sh);
case expr_kind::Let: return save_result(a, mk_let(let_name(a), apply(let_type(a)), apply(let_value(a)), apply(let_body(a))), sh);
case expr_kind::MetaVar:
r = update_metavar(a, [&](local_entry const & e) -> local_entry {
return save_result(a,
update_metavar(a, [&](local_entry const & e) -> local_entry {
if (e.is_inst())
return mk_inst(e.s(), apply(e.v()));
else
return e;
});
break;
}),
sh);
}
if (sh)
m_cache.insert(std::make_pair(a.raw(), r));
return r;
lean_unreachable(); // LCOV_EXCL_LINE
}
public:
/**

22
src/library/elaborator/elaborator.cpp
View file

@ -187,7 +187,7 @@ class elaborator::imp {
std::pair<expr, justification> get_subst_jst(expr const & m) const {
lean_assert(is_metavar(m));
lean_assert(is_assigned(m));
return m_state.m_menv.get_subst_jst(m);
return *(m_state.m_menv.get_subst_jst(m));
}
/** \brief Return the type of an metavariable */
@ -523,7 +523,7 @@ class elaborator::imp {
try {
context_entry const & e = lookup(ctx, var_idx(a));
if (e.get_body())
a = e.get_body();
a = *(e.get_body());
} catch (exception&) {
}
}
@ -549,14 +549,14 @@ class elaborator::imp {
if (curr != new_curr) {
modified = true;
new_args[i] = new_curr;
if (to_value(f).normalize(new_args.size(), new_args.data(), r)) {
a = r;
if (optional<expr> r = to_value(f).normalize(new_args.size(), new_args.data())) {
a = *r;
return;
}
}
}
if (to_value(f).normalize(new_args.size(), new_args.data(), r)) {
a = r;
if (optional<expr> r = to_value(f).normalize(new_args.size(), new_args.data())) {
a = *r;
return;
}
if (modified) {
@ -720,8 +720,13 @@ class elaborator::imp {
if (is_simple_ho_match(ctx, a, b, is_lhs, c)) {
expr m = arg(a, 0);
buffer<expr> types;
for (unsigned i = 1; i < num_args(a); i++)
types.push_back(lookup(ctx, var_idx(arg(a, i))).get_domain());
for (unsigned i = 1; i < num_args(a); i++) {
optional<expr> d = lookup(ctx, var_idx(arg(a, i))).get_domain();
if (d)
types.push_back(*d);
else
return false;
}
justification new_jst(new destruct_justification(c));
expr s = mk_lambda(types, b);
if (!is_lhs)
@ -811,7 +816,6 @@ class elaborator::imp {
// Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), b
imitation = mk_lambda(arg_types, lift_free_vars(b, 0, num_a - 1));
}
lean_assert(imitation);
push_new_eq_constraint(new_state.m_queue, ctx, f_a, imitation, new_assumption);
new_cs->push_back(new_state, new_assumption);
}

12
src/library/elaborator/elaborator_justification.cpp
View file

@ -18,8 +18,8 @@ propagation_justification::~propagation_justification() {
void propagation_justification::get_children(buffer<justification_cell*> & r) const {
push_back(r, m_constraint.get_justification());
}
expr const & propagation_justification::get_main_expr() const {
return expr::null();
optional<expr> propagation_justification::get_main_expr() const {
return optional<expr>();
}
format propagation_justification::pp_header(formatter const & fmt, options const & opts) const {
format r;
@ -120,8 +120,8 @@ format synthesis_justification::pp_header(formatter const & fmt, options const &
void synthesis_justification::get_children(buffer<justification_cell*> & r) const {
append(r, m_substitution_justifications);
}
expr const & synthesis_justification::get_main_expr() const {
return m_mvar;
optional<expr> synthesis_justification::get_main_expr() const {
return some(m_mvar);
}
char const * synthesis_failure_justification::get_label() const {
@ -156,7 +156,7 @@ format next_solution_justification::pp_header(formatter const &, options const &
void next_solution_justification::get_children(buffer<justification_cell*> & r) const {
append(r, m_assumptions);
}
expr const & next_solution_justification::get_main_expr() const {
return expr::null();
optional<expr> next_solution_justification::get_main_expr() const {
return optional<expr>();
}
}

6
src/library/elaborator/elaborator_justification.h
View file

@ -21,7 +21,7 @@ public:
propagation_justification(unification_constraint const & c);
virtual ~propagation_justification();
virtual void get_children(buffer<justification_cell*> & r) const;
virtual expr const & get_main_expr() const;
virtual optional<expr> get_main_expr() const;
virtual format pp_header(formatter const &, options const &) const;
unification_constraint const & get_constraint() const { return m_constraint; }
};
@ -168,7 +168,7 @@ public:
virtual ~synthesis_justification();
virtual format pp_header(formatter const &, options const &) const;
virtual void get_children(buffer<justification_cell*> & r) const;
virtual expr const & get_main_expr() const;
virtual optional<expr> get_main_expr() const;
};
/**
@ -212,6 +212,6 @@ public:
virtual ~next_solution_justification();
virtual format pp_header(formatter const &, options const &) const;
virtual void get_children(buffer<justification_cell*> & r) const;
virtual expr const & get_main_expr() const;
virtual optional<expr> get_main_expr() const;
};
};

10
src/library/expr_lt.cpp
View file

@ -7,10 +7,16 @@ Author: Leonardo de Moura
#include "kernel/expr.h"
namespace lean {
bool is_lt(expr const & a, expr const & b, bool use_hash);
static bool is_lt(optional<expr> const & a, optional<expr> const & b, bool use_hash) {
if (is_eqp(a, b)) return false;
else if (!a && b) return true;
else if (a && !b) return false;
else return is_lt(*a, *b, use_hash);
}
bool is_lt(expr const & a, expr const & b, bool use_hash) {
if (is_eqp(a, b)) return false;
if (!a && b) return true; // the null expression is the smallest one
if (a && !b) return false;
if (a.kind() != b.kind()) return a.kind() < b.kind();
if (use_hash) {
if (a.hash() < b.hash()) return true;

27
src/library/fo_unify.cpp
View file

@ -20,16 +20,21 @@ static bool is_metavar_wo_local_context(expr const & e) {
return is_metavar(e) && !metavar_lctx(e);
}
static bool is_eq_heq(expr const & e, expr & lhs, expr & rhs) {
return is_eq(e, lhs, rhs) || is_homo_eq(e, lhs, rhs);
static bool is_eq_heq(expr const & e) {
return is_eq(e) || is_homo_eq(e);
}
static expr_pair eq_heq_args(expr const & e) {
lean_assert(is_eq(e) || is_homo_eq(e));
if (is_eq(e))
return expr_pair(eq_lhs(e), eq_rhs(e));
else
return expr_pair(arg(e, 1), arg(e, 2));
}
optional<substitution> fo_unify(expr e1, expr e2) {
lean_assert(e1);
lean_assert(e2);
substitution s;
unsigned i1, i2;
expr lhs1, rhs1, lhs2, rhs2;
buffer<expr_pair> todo;
todo.emplace_back(e1, e2);
while (!todo.empty()) {
@ -42,9 +47,11 @@ optional<substitution> fo_unify(expr e1, expr e2) {
assign(s, e1, e2);
} else if (is_metavar_wo_local_context(e2)) {
assign(s, e2, e1);
} else if (is_eq_heq(e1, lhs1, rhs1) && is_eq_heq(e2, lhs2, rhs2)) {
todo.emplace_back(lhs1, lhs2);
todo.emplace_back(rhs1, rhs2);
} else if (is_eq_heq(e1) && is_eq_heq(e2)) {
expr_pair p1 = eq_heq_args(e1);
expr_pair p2 = eq_heq_args(e2);
todo.emplace_back(p1.second, p2.second);
todo.emplace_back(p1.first, p2.first);
} else {
if (e1.kind() != e2.kind())
return optional<substitution>();
@ -79,7 +86,7 @@ optional<substitution> fo_unify(expr e1, expr e2) {
return optional<substitution>();
if (let_type(e1)) {
lean_assert(let_type(e2));
todo.emplace_back(let_type(e1), let_type(e2));
todo.emplace_back(*let_type(e1), *let_type(e2));
}
break;
}
@ -91,7 +98,7 @@ optional<substitution> fo_unify(expr e1, expr e2) {
static int fo_unify(lua_State * L) {
optional<substitution> r = fo_unify(to_nonnull_expr(L, 1), to_nonnull_expr(L, 2));
optional<substitution> r = fo_unify(to_expr(L, 1), to_expr(L, 2));
if (!r) {
lua_pushnil(L);
return 1;

147
src/library/kernel_bindings.cpp
View file

@ -162,7 +162,7 @@ static int local_entry_mk_lift(lua_State * L) {
}
static int local_entry_mk_inst(lua_State * L) {
return push_local_entry(L, mk_inst(luaL_checkinteger(L, 1), to_nonnull_expr(L, 2)));
return push_local_entry(L, mk_inst(luaL_checkinteger(L, 1), to_expr(L, 2)));
}
static int local_entry_is_lift(lua_State * L) {
@ -268,15 +268,16 @@ static void open_local_context(lua_State * L) {
DECL_UDATA(expr)
expr & to_nonnull_expr(lua_State * L, int idx) {
expr & r = to_expr(L, idx);
if (!r)
throw exception("non-null Lean expression expected");
return r;
int push_optional_expr(lua_State * L, optional<expr> const & e) {
if (e)
push_expr(L, *e);
else
lua_pushnil(L);
return 1;
}
expr & to_app(lua_State * L, int idx) {
expr & r = to_nonnull_expr(L, idx);
expr & r = to_expr(L, idx);
if (!is_app(r))
throw exception("Lean application expression expected");
return r;
@ -284,14 +285,9 @@ expr & to_app(lua_State * L, int idx) {
static int expr_tostring(lua_State * L) {
std::ostringstream out;
expr & e = to_expr(L, 1);
if (e) {
formatter fmt = get_global_formatter(L);
options opts = get_global_options(L);
out << mk_pair(fmt(to_expr(L, 1), opts), opts);
} else {
out << "<null-expr>";
}
lua_pushstring(L, out.str().c_str());
return 1;
}
@ -320,39 +316,39 @@ static int expr_mk_app(lua_State * L) {
throw exception("application must have at least two arguments");
buffer<expr> args;
for (int i = 1; i <= nargs; i++)
args.push_back(to_nonnull_expr(L, i));
args.push_back(to_expr(L, i));
return push_expr(L, mk_app(args));
}
static int expr_mk_eq(lua_State * L) {
return push_expr(L, mk_eq(to_nonnull_expr(L, 1), to_nonnull_expr(L, 2)));
return push_expr(L, mk_eq(to_expr(L, 1), to_expr(L, 2)));
}
static int expr_mk_lambda(lua_State * L) {
return push_expr(L, mk_lambda(to_name_ext(L, 1), to_nonnull_expr(L, 2), to_nonnull_expr(L, 3)));
return push_expr(L, mk_lambda(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3)));
}
static int expr_mk_pi(lua_State * L) {
return push_expr(L, mk_pi(to_name_ext(L, 1), to_nonnull_expr(L, 2), to_nonnull_expr(L, 3)));
return push_expr(L, mk_pi(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3)));
}
static int expr_mk_arrow(lua_State * L) {
return push_expr(L, mk_arrow(to_nonnull_expr(L, 1), to_nonnull_expr(L, 2)));
return push_expr(L, mk_arrow(to_expr(L, 1), to_expr(L, 2)));
}
static int expr_mk_let(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 3)
return push_expr(L, mk_let(to_name_ext(L, 1), expr(), to_nonnull_expr(L, 2), to_nonnull_expr(L, 3)));
return push_expr(L, mk_let(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3)));
else
return push_expr(L, mk_let(to_name_ext(L, 1), to_nonnull_expr(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4)));
return push_expr(L, mk_let(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3), to_expr(L, 4)));
}
static expr get_expr_from_table(lua_State * L, int t, int i) {
lua_pushvalue(L, t); // push table to the top
lua_pushinteger(L, i);
lua_gettable(L, -2);
expr r = to_nonnull_expr(L, -1);
expr r = to_expr(L, -1);
lua_pop(L, 2); // remove table and value
return r;
}
@ -385,7 +381,7 @@ int expr_abst(lua_State * L) {
int len = objlen(L, 1);
if (len == 0)
throw exception("function expects arg #1 to be a non-empty table");
expr r = to_nonnull_expr(L, 2);
expr r = to_expr(L, 2);
for (int i = len; i >= 1; i--) {
auto p = get_expr_pair_from_table(L, 1, i);
r = F1(p.first, p.second, r);
@ -394,12 +390,12 @@ int expr_abst(lua_State * L) {
} else {
if (nargs % 2 == 0)
throw exception("function must have an odd number of arguments");
expr r = to_nonnull_expr(L, nargs);
expr r = to_expr(L, nargs);
for (int i = nargs - 1; i >= 1; i-=2) {
if (is_expr(L, i - 1))
r = F1(to_nonnull_expr(L, i - 1), to_nonnull_expr(L, i), r);
r = F1(to_expr(L, i - 1), to_expr(L, i), r);
else
r = F2(to_name_ext(L, i - 1), to_nonnull_expr(L, i), r);
r = F2(to_name_ext(L, i - 1), to_expr(L, i), r);
}
return push_expr(L, r);
}
@ -425,19 +421,14 @@ static int expr_mk_metavar(lua_State * L) {
return push_expr(L, mk_metavar(to_name_ext(L, 1), to_local_context(L, 2)));
}
static int expr_is_null(lua_State * L) {
lua_pushboolean(L, !to_expr(L, 1));
return 1;
}
static int expr_get_kind(lua_State * L) {
lua_pushinteger(L, static_cast<int>(to_nonnull_expr(L, 1).kind()));
lua_pushinteger(L, static_cast<int>(to_expr(L, 1).kind()));
return 1;
}
#define EXPR_PRED(P) \
static int expr_ ## P(lua_State * L) { \
lua_pushboolean(L, P(to_nonnull_expr(L, 1))); \
lua_pushboolean(L, P(to_expr(L, 1))); \
return 1; \
}
@ -502,7 +493,7 @@ static int expr_arg(lua_State * L) {
}
static int expr_fields(lua_State * L) {
expr & e = to_nonnull_expr(L, 1);
expr & e = to_expr(L, 1);
switch (e.kind()) {
case expr_kind::Var: lua_pushinteger(L, var_idx(e)); return 1;
case expr_kind::Constant: return push_name(L, const_name(e));
@ -511,8 +502,10 @@ static int expr_fields(lua_State * L) {
case expr_kind::App: lua_pushinteger(L, num_args(e)); expr_args(L); return 2;
case expr_kind::Eq: push_expr(L, eq_lhs(e)); push_expr(L, eq_rhs(e)); return 2;
case expr_kind::Lambda:
case expr_kind::Pi: push_name(L, abst_name(e)); push_expr(L, abst_domain(e)); push_expr(L, abst_body(e)); return 3;
case expr_kind::Let: push_name(L, let_name(e)); push_expr(L, let_type(e)); push_expr(L, let_value(e)); push_expr(L, let_body(e)); return 4;
case expr_kind::Pi:
push_name(L, abst_name(e)); push_expr(L, abst_domain(e)); push_expr(L, abst_body(e)); return 3;
case expr_kind::Let:
push_name(L, let_name(e)); push_optional_expr(L, let_type(e)); push_expr(L, let_value(e)); push_expr(L, let_body(e)); return 4;
case expr_kind::MetaVar: push_name(L, metavar_name(e)); push_local_context(L, metavar_lctx(e)); return 2;
}
lean_unreachable(); // LCOV_EXCL_LINE
@ -520,7 +513,7 @@ static int expr_fields(lua_State * L) {
}
static int expr_for_each(lua_State * L) {
expr & e = to_nonnull_expr(L, 1); // expr
expr & e = to_expr(L, 1); // expr
luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun
auto f = [&](expr const & a, unsigned offset) {
lua_pushvalue(L, 2); // push user-fun
@ -619,7 +612,6 @@ static const struct luaL_Reg expr_m[] = {
{"__lt", safe_function<expr_lt>},
{"__call", safe_function<expr_mk_app>},
{"kind", safe_function<expr_get_kind>},
{"is_null", safe_function<expr_is_null>},
{"is_var", safe_function<expr_is_var>},
{"is_constant", safe_function<expr_is_constant>},
{"is_app", safe_function<expr_is_app>},
@ -709,14 +701,14 @@ DECL_UDATA(context_entry)
static int mk_context_entry(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 2)
return push_context_entry(L, context_entry(to_name_ext(L, 1), to_nonnull_expr(L, 2)));
return push_context_entry(L, context_entry(to_name_ext(L, 1), to_expr(L, 2)));
else
return push_context_entry(L, context_entry(to_name_ext(L, 1), to_nonnull_expr(L, 2), to_nonnull_expr(L, 3)));
return push_context_entry(L, context_entry(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3)));
}
static int context_entry_get_name(lua_State * L) { return push_name(L, to_context_entry(L, 1).get_name()); }
static int context_entry_get_domain(lua_State * L) { return push_expr(L, to_context_entry(L, 1).get_domain()); }
static int context_entry_get_body(lua_State * L) { return push_expr(L, to_context_entry(L, 1).get_body()); }
static int context_entry_get_domain(lua_State * L) { return push_optional_expr(L, to_context_entry(L, 1).get_domain()); }
static int context_entry_get_body(lua_State * L) { return push_optional_expr(L, to_context_entry(L, 1).get_body()); }
static const struct luaL_Reg context_entry_m[] = {
{"__gc", context_entry_gc}, // never throws
@ -743,11 +735,14 @@ static int mk_context(lua_State * L) {
return push_context(L, context());
} else if (nargs == 2) {
context_entry & e = to_context_entry(L, 2);
return push_context(L, context(to_context(L, 1), e.get_name(), e.get_domain(), e.get_body()));
return push_context(L, context(to_context(L, 1), e));
} else if (nargs == 3) {
return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), to_nonnull_expr(L, 3)));
return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), to_expr(L, 3)));
} else {
return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), to_expr(L, 3), to_nonnull_expr(L, 4)));
if (lua_isnil(L, 3))
return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), optional<expr>(), to_expr(L, 4)));
else
return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), to_expr(L, 3), to_expr(L, 4)));
}
}
@ -979,33 +974,33 @@ static int environment_add_definition(lua_State * L) {
rw_environment env(L, 1);
int nargs = lua_gettop(L);
if (nargs == 3) {
env->add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3));
env->add_definition(to_name_ext(L, 2), to_expr(L, 3));
} else if (nargs == 4) {
if (is_expr(L, 4))
env->add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4));
env->add_definition(to_name_ext(L, 2), to_expr(L, 3), to_expr(L, 4));
else
env->add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3), lua_toboolean(L, 4));
env->add_definition(to_name_ext(L, 2), to_expr(L, 3), lua_toboolean(L, 4));
} else {
env->add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4), lua_toboolean(L, 5));
env->add_definition(to_name_ext(L, 2), to_expr(L, 3), to_expr(L, 4), lua_toboolean(L, 5));
}
return 0;
}
static int environment_add_theorem(lua_State * L) {
rw_environment env(L, 1);
env->add_theorem(to_name_ext(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4));
env->add_theorem(to_name_ext(L, 2), to_expr(L, 3), to_expr(L, 4));
return 0;
}
static int environment_add_var(lua_State * L) {
rw_environment env(L, 1);
env->add_var(to_name_ext(L, 2), to_nonnull_expr(L, 3));
env->add_var(to_name_ext(L, 2), to_expr(L, 3));
return 0;
}
static int environment_add_axiom(lua_State * L) {
rw_environment env(L, 1);
env->add_axiom(to_name_ext(L, 2), to_nonnull_expr(L, 3));
env->add_axiom(to_name_ext(L, 2), to_expr(L, 3));
return 0;
}
@ -1024,18 +1019,18 @@ static int environment_check_type(lua_State * L) {
ro_environment env(L, 1);
int nargs = lua_gettop(L);
if (nargs == 2)
return push_expr(L, env->infer_type(to_nonnull_expr(L, 2)));
return push_expr(L, env->infer_type(to_expr(L, 2)));
else
return push_expr(L, env->infer_type(to_nonnull_expr(L, 2), to_context(L, 3)));
return push_expr(L, env->infer_type(to_expr(L, 2), to_context(L, 3)));
}
static int environment_normalize(lua_State * L) {
ro_environment env(L, 1);
int nargs = lua_gettop(L);
if (nargs == 2)
return push_expr(L, env->normalize(to_nonnull_expr(L, 2)));
return push_expr(L, env->normalize(to_expr(L, 2)));
else
return push_expr(L, env->normalize(to_nonnull_expr(L, 2), to_context(L, 3)));
return push_expr(L, env->normalize(to_expr(L, 2), to_context(L, 3)));
}
/**
@ -1081,9 +1076,9 @@ static int environment_infer_type(lua_State * L) {
int nargs = lua_gettop(L);
type_inferer inferer(to_environment(L, 1));
if (nargs == 2)
return push_expr(L, inferer(to_nonnull_expr(L, 2)));
return push_expr(L, inferer(to_expr(L, 2)));
else
return push_expr(L, inferer(to_nonnull_expr(L, 2), to_context(L, 3)));
return push_expr(L, inferer(to_expr(L, 2), to_context(L, 3)));
}
static int environment_tostring(lua_State * L) {
@ -1303,6 +1298,14 @@ static void open_object(lua_State * L) {
DECL_UDATA(justification)
int push_optional_justification(lua_State * L, optional<justification> const & j) {
if (j)
push_justification(L, *j);
else
lua_pushnil(L);
return 1;
}
static int justification_tostring(lua_State * L) {
std::ostringstream out;
justification & jst = to_justification(L, 1);
@ -1359,7 +1362,12 @@ static int justification_children(lua_State * L) {
}
static int justification_get_main_expr(lua_State * L) {
return push_expr(L, to_justification(L, 1).get_main_expr());
optional<expr> r = to_justification(L, 1).get_main_expr();
if (r)
push_expr(L, *r);
else
lua_pushnil(L);
return 1;
}
static int justification_pp(lua_State * L) {
@ -1437,7 +1445,7 @@ static int menv_mk_metavar(lua_State * L) {
} else if (nargs == 2) {
return push_expr(L, to_metavar_env(L, 1).mk_metavar(to_context(L, 2)));
} else {
return push_expr(L, to_metavar_env(L, 1).mk_metavar(to_context(L, 2), to_expr(L, 3)));
return push_expr(L, to_metavar_env(L, 1).mk_metavar(to_context(L, 2), optional<expr>(to_expr(L, 3))));
}
}
@ -1500,29 +1508,32 @@ static int menv_assign(lua_State * L) {
static int menv_get_subst(lua_State * L) {
if (is_expr(L, 2))
return push_expr(L, to_metavar_env(L, 1).get_subst(to_metavar(L, 2)));
return push_optional_expr(L, to_metavar_env(L, 1).get_subst(to_metavar(L, 2)));
else
return push_expr(L, to_metavar_env(L, 1).get_subst(to_name_ext(L, 2)));
return push_optional_expr(L, to_metavar_env(L, 1).get_subst(to_name_ext(L, 2)));
}
static int menv_get_justification(lua_State * L) {
if (is_expr(L, 2))
return push_justification(L, to_metavar_env(L, 1).get_justification(to_metavar(L, 2)));
return push_optional_justification(L, to_metavar_env(L, 1).get_justification(to_metavar(L, 2)));
else
return push_justification(L, to_metavar_env(L, 1).get_justification(to_name_ext(L, 2)));
return push_optional_justification(L, to_metavar_env(L, 1).get_justification(to_name_ext(L, 2)));
}
static int menv_get_subst_jst(lua_State * L) {
optional<std::pair<expr, justification>> r;
if (is_expr(L, 2)) {
auto p = to_metavar_env(L, 1).get_subst_jst(to_metavar(L, 2));
push_expr(L, p.first);
push_justification(L, p.second);
r = to_metavar_env(L, 1).get_subst_jst(to_metavar(L, 2));
} else {
auto p = to_metavar_env(L, 1).get_subst_jst(to_name_ext(L, 2));
push_expr(L, p.first);
push_justification(L, p.second);
r = to_metavar_env(L, 1).get_subst_jst(to_name_ext(L, 2));
}
if (r) {
push_expr(L, r->first);
push_justification(L, r->second);
return 2;
} else {
return 0;
}
}
static int menv_for_each_subst(lua_State * L) {

3
src/library/kernel_bindings.h
View file

@ -21,7 +21,8 @@ UDATA_DEFS(object)
UDATA_DEFS(environment)
UDATA_DEFS(justification)
UDATA_DEFS(metavar_env)
expr & to_nonnull_expr(lua_State * L, int idx);
int push_optional_expr(lua_State * L, optional<expr> const & e);
int push_optional_justification(lua_State * L, optional<justification> const & j);
/**
\brief Return the formatter object associated with the given Lua State.
This procedure checks for options at:

22
src/library/max_sharing.cpp
View file

@ -25,6 +25,13 @@ struct max_sharing_fn::imp {
m_cache.insert(a);
}
optional<expr> apply(optional<expr> const & a) {
if (a)
return some(apply(*a));
else
return a;
}
expr apply(expr const & a) {
auto r = m_cache.find(a);
if (r != m_cache.end()) {
@ -36,25 +43,21 @@ struct max_sharing_fn::imp {
return a;
}
switch (a.kind()) {
case expr_kind::Constant:
if (const_type(a)) {
case expr_kind::Constant: {
expr r = update_const(a, apply(const_type(a)));
cache(r);
return r;
} else {
cache(a);
return a;
}
case expr_kind::Var: case expr_kind::Type: case expr_kind::Value:
cache(a);
return a;
case expr_kind::App: {
expr r = update_app(a, [=](expr const & c){ return apply(c); });
expr r = update_app(a, [=](expr const & c) { return apply(c); });
cache(r);
return r;
}
case expr_kind::Eq : {
expr r = update_eq(a, [=](expr const & l, expr const & r){ return std::make_pair(apply(l), apply(r)); });
expr r = update_eq(a, [=](expr const & l, expr const & r) { return std::make_pair(apply(l), apply(r)); });
cache(r);
return r;
}
@ -65,9 +68,8 @@ struct max_sharing_fn::imp {
return r;
}
case expr_kind::Let: {
expr r = update_let(a, [=](expr const & t, expr const & v, expr const & b) {
expr new_t = t ? apply(t) : expr();
return std::make_tuple(new_t, apply(v), apply(b));
expr r = update_let(a, [=](optional<expr> const & t, expr const & v, expr const & b) {
return std::make_tuple(apply(t), apply(v), apply(b));
});
cache(r);
return r;

5
src/library/placeholder.cpp
View file

@ -8,11 +8,12 @@ Author: Leonardo de Moura
#include "kernel/metavar.h"
#include "kernel/expr_maps.h"
#include "kernel/replace_visitor.h"
#include "library/expr_pair.h"
#include "library/placeholder.h"
namespace lean {
static name g_placeholder_name("_");
expr mk_placeholder(expr const & t) {
expr mk_placeholder(optional<expr> const & t) {
return mk_constant(g_placeholder_name, t);
}
@ -39,7 +40,7 @@ protected:
expr visit(expr const & e, context const & c) {
expr r = replace_visitor::visit(e, c);
if (!is_eqp(r, e) && m_new2old)
(*m_new2old)[r] = e;
m_new2old->insert(expr_pair(r, e));
return r;
}
public:

2
src/library/placeholder.h
View file

@ -15,7 +15,7 @@ class metavar_env;
type). To be able to track location, a new constant for each
placeholder.
*/
expr mk_placeholder(expr const & t = expr());
expr mk_placeholder(optional<expr> const & t = optional<expr>());
/**
\brief Return true iff the given expression is a placeholder.

7
src/library/rewriter/fo_match.cpp
View file

@ -153,6 +153,13 @@ bool fo_match::match_metavar(expr const & p, expr const & t, unsigned, subst_map
return p == t;
}
bool fo_match::match_main(optional<expr> const & p, optional<expr> const & t, unsigned o, subst_map & s) {
if (p && t)
return match_main(*p, *t, o, s);
else
return !p && !t;
}
bool fo_match::match_main(expr const & p, expr const & t, unsigned o, subst_map & s) {
lean_trace("fo_match", tout << "match : (" << p << ", " << t << ", " << o << ", " << s << ")" << endl;); // LCOV_EXCL_LINE
switch (p.kind()) {

1
src/library/rewriter/fo_match.h
View file

@ -26,6 +26,7 @@ private:
bool match_let(expr const & p, expr const & t, unsigned o, subst_map & s);
bool match_metavar(expr const & p, expr const & t, unsigned o, subst_map & s);
bool match_main(expr const & p, expr const & t, unsigned o, subst_map & s);
bool match_main(optional<expr> const & p, optional<expr> const & t, unsigned o, subst_map & s);
public:
bool match(expr const & p, expr const & t, unsigned o, subst_map & s);

19
src/library/rewriter/rewriter.cpp
View file

@ -370,8 +370,9 @@ pair<expr, expr> rewrite_eq(environment const & env, context & ctx, expr const &
pair<expr, expr> rewrite_let_type(environment const & env, context & ctx, expr const & v, pair<expr, expr> const & result_ty) {
lean_assert(is_let(v));
type_inferer ti(env);
if (!let_type(v)) {
name const & n = let_name(v);
expr const & ty = let_type(v);
expr const & ty = *let_type(v);
expr const & val = let_value(v);
expr const & body = let_body(v);
expr const & new_ty = result_ty.first;
@ -385,6 +386,9 @@ pair<expr, expr> rewrite_let_type(environment const & env, context & ctx, expr c
Refl(ty_v, v),
pf);
return make_pair(new_v, proof);
} else {
throw rewriter_exception();
}
}
/**
@ -403,7 +407,7 @@ pair<expr, expr> rewrite_let_value(environment const & env, context & ctx, expr
lean_assert(is_let(v));
type_inferer ti(env);
name const & n = let_name(v);
expr const & ty = let_type(v);
optional<expr> const & ty = let_type(v);
expr const & val = let_value(v);
expr const & body = let_body(v);
expr const & new_val = result_value.first;
@ -436,7 +440,7 @@ pair<expr, expr> rewrite_let_body(environment const & env, context & ctx, expr c
lean_assert(is_let(v));
type_inferer ti(env);
name const & n = let_name(v);
expr const & ty = let_type(v);
optional<expr> const & ty = let_type(v);
expr const & val = let_value(v);
expr const & body = let_body(v);
expr const & new_body = result_body.first;
@ -828,10 +832,11 @@ let_type_rewriter_cell::let_type_rewriter_cell(rewriter const & rw)
:rewriter_cell(rewriter_kind::LetType), m_rw(rw) { }
let_type_rewriter_cell::~let_type_rewriter_cell() { }
pair<expr, expr> let_type_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
if (!is_let(v))
if (!is_let(v) || !let_type(v))
throw rewriter_exception();
expr const & ty = let_type(v);
expr const & ty = *let_type(v);
pair<expr, expr> result_ty = m_rw(env, ctx, ty);
if (ty != result_ty.first) {
// ty changed
@ -878,9 +883,9 @@ pair<expr, expr> let_body_rewriter_cell::operator()(environment const & env, con
throw rewriter_exception();
name const & n = let_name(v);
expr const & ty = let_type(v);
optional<expr> const & ty = let_type(v);
expr const & body = let_body(v);
context new_ctx = extend(ctx, n, ty);
context new_ctx = extend(ctx, n, ty, let_value(v));
pair<expr, expr> result_body = m_rw(env, new_ctx, body);
if (body != result_body.first) {
return rewrite_let_body(env, ctx, v, result_body);

10
src/library/rewriter/rewriter.h
View file

@ -483,7 +483,7 @@ class apply_rewriter_fn {
break;
case expr_kind::Let: {
name const & n = let_name(v);
expr const & ty = let_type(v);
optional<expr> const & ty = let_type(v);
expr const & val = let_value(v);
expr const & body = let_body(v);
@ -492,14 +492,16 @@ class apply_rewriter_fn {
expr pf = Refl(ty_v, v);
bool changed = false;
std::pair<expr, expr> result_ty = apply(env, ctx, ty);
if (ty != result_ty.first) {
if (ty) {
std::pair<expr, expr> result_ty = apply(env, ctx, *ty);
if (*ty != result_ty.first) {
// ty changed
result = rewrite_let_type(env, ctx, new_v, result_ty);
new_v = result.first;
pf = result.second;
changed = true;
}
}
std::pair<expr, expr> result_val = apply(env, ctx, val);
if (val != result_val.first) {
@ -513,7 +515,7 @@ class apply_rewriter_fn {
changed = true;
}
context new_ctx = extend(ctx, n, ty);
context new_ctx = extend(ctx, n, ty, val);
std::pair<expr, expr> result_body = apply(env, new_ctx, body);
if (body != result_body.first) {
result = rewrite_let_body(env, ctx, new_v, result_body);

4
src/library/substitution.cpp
View file

@ -59,7 +59,7 @@ static int substitution_find(lua_State * L) {
substitution & s = to_substitution(L, 1);
expr * it;
if (is_expr(L, 2)) {
expr const & e = to_nonnull_expr(L, 2);
expr const & e = to_expr(L, 2);
if (is_metavar(e))
it = s.splay_find(metavar_name(e));
else
@ -75,7 +75,7 @@ static int substitution_find(lua_State * L) {
}
static int substitution_apply(lua_State * L) {
return push_expr(L, apply(to_substitution(L, 1), to_nonnull_expr(L, 2)));
return push_expr(L, apply(to_substitution(L, 1), to_expr(L, 2)));
}
static const struct luaL_Reg substitution_m[] = {

14
src/library/tactic/apply_tactic.cpp
View file

@ -44,7 +44,7 @@ static optional<proof_state> apply_tactic(environment const & env, proof_state c
// 1) regular arguments computed using unification.
// 2) propostions that generate new subgoals.
// We use a pair to simulate this "union" type.
typedef list<std::pair<expr, name>> arg_list;
typedef list<std::pair<optional<expr>, name>> arg_list;
// We may solve more than one goal.
// We store the solved goals using a list of pairs
// name, args. Where the 'name' is the name of the solved goal.
@ -66,21 +66,21 @@ static optional<proof_state> apply_tactic(environment const & env, proof_state c
for (auto const & mvar : mvars) {
expr mvar_sol = apply(*subst, mvar);
if (mvar_sol != mvar) {
l.emplace_front(mvar_sol, name());
l = cons(mk_pair(optional<expr>(mvar_sol), name()), l);
th_type_c = instantiate(abst_body(th_type_c), mvar_sol);
} else {
if (inferer.is_proposition(abst_domain(th_type_c), context(), &new_menv)) {
name new_gname(gname, new_goal_idx);
new_goal_idx++;
l.emplace_front(expr(), new_gname);
l = cons(mk_pair(optional<expr>(), new_gname), l);
new_goals_buf.emplace_back(new_gname, update(g, abst_domain(th_type_c)));
th_type_c = instantiate(abst_body(th_type_c), mk_constant(new_gname, abst_domain(th_type_c)));
} else {
// we have to create a new metavar in menv
// since we do not have a substitution for mvar, and
// it is not a proposition
expr new_m = new_menv.mk_metavar(context(), abst_domain(th_type_c));
l.emplace_front(new_m, name());
expr new_m = new_menv.mk_metavar(context(), optional<expr>(abst_domain(th_type_c)));
l = cons(mk_pair(optional<expr>(new_m), name()), l);
// we use instantiate_with_closed_relaxed because we do not want
// to introduce a lift operator in the new_m
th_type_c = instantiate_with_closed_relaxed(abst_body(th_type_c), 1, &new_m);
@ -105,10 +105,10 @@ static optional<proof_state> apply_tactic(environment const & env, proof_state c
buffer<expr> args;
args.push_back(th);
for (auto const & p2 : l) {
expr const & arg = p2.first;
optional<expr> const & arg = p2.first;
if (arg) {
// TODO(Leo): decide if we instantiate the metavars in the end or not.
args.push_back(arg);
args.push_back(*arg);
} else {
name const & subgoal_name = p2.second;
args.push_back(find(m, subgoal_name));

2
src/library/tactic/assignment.h
View file

@ -15,6 +15,6 @@ class assignment {
metavar_env m_menv;
public:
assignment(metavar_env const & menv):m_menv(menv) {}
expr operator()(name const & mvar) const { return m_menv.get_subst(mvar); }
optional<expr> operator()(name const & mvar) const { return m_menv.get_subst(mvar); }
};
}

41
src/library/tactic/boolean_tactics.cpp
View file

@ -62,16 +62,16 @@ tactic imp_tactic(name const & H_name, bool all) {
expr impfn = mk_implies_fn();
bool found = false;
list<std::tuple<name, name, expr>> proof_info;
goals new_goals = map_goals(s, [&](name const & g_name, goal const & g) -> goal {
goals new_goals = map_goals(s, [&](name const & g_name, goal const & g) -> optional<goal> {
expr const & c = g.get_conclusion();
expr new_h, new_c;
if ((all || !found) && is_implies(c, new_h, new_c)) {
found = true;
name new_h_name = g.mk_unique_hypothesis_name(H_name);
proof_info.emplace_front(g_name, new_h_name, c);
return goal(add_hypothesis(new_h_name, new_h, g.get_hypotheses()), new_c);
return optional<goal>(goal(add_hypothesis(new_h_name, new_h, g.get_hypotheses()), new_c));
} else {
return g;
return optional<goal>(g);
}
});
if (found) {
@ -100,7 +100,7 @@ tactic conj_hyp_tactic(bool all) {
return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
bool found = false;
list<std::pair<name, hypotheses>> proof_info; // goal name -> expanded hypotheses
goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal {
goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> optional<goal> {
if (all || !found) {
buffer<hypothesis> new_hyp_buf;
hypotheses proof_info_data;
@ -119,12 +119,12 @@ tactic conj_hyp_tactic(bool all) {
}
if (proof_info_data) {
proof_info.emplace_front(ng, proof_info_data);
return update(g, new_hyp_buf);
return some(update(g, new_hyp_buf));
} else {
return g;
return some(g);
}
} else {
return g;
return some(g);
}
});
if (found) {
@ -158,7 +158,7 @@ tactic conj_hyp_tactic(bool all) {
optional<proof_state> disj_hyp_tactic_core(name const & goal_name, name const & hyp_name, proof_state const & s) {
buffer<std::pair<name, goal>> new_goals_buf;
expr H;
optional<expr> H;
expr conclusion;
for (auto const & p1 : s.get_goals()) {
check_interrupted();
@ -170,10 +170,10 @@ optional<proof_state> disj_hyp_tactic_core(name const & goal_name, name const &
for (auto const & p2 : g.get_hypotheses()) {
if (p2.first == hyp_name) {
H = p2.second;
if (!is_or(H))
if (!is_or(*H))
return none_proof_state(); // tactic failed
new_hyp_buf1.emplace_back(p2.first, arg(H, 1));
new_hyp_buf2.emplace_back(p2.first, arg(H, 2));
new_hyp_buf1.emplace_back(p2.first, arg(*H, 1));
new_hyp_buf2.emplace_back(p2.first, arg(*H, 2));
} else {
new_hyp_buf1.push_back(p2);
new_hyp_buf2.push_back(p2);
@ -191,13 +191,14 @@ optional<proof_state> disj_hyp_tactic_core(name const & goal_name, name const &
return none_proof_state(); // tactic failed
goals new_gs = to_list(new_goals_buf.begin(), new_goals_buf.end());
proof_builder pb = s.get_proof_builder();
expr Href = *H;
proof_builder new_pb = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
proof_map new_m(m);
expr pr1 = find(m, name(goal_name, 1));
expr pr2 = find(m, name(goal_name, 2));
pr1 = Fun(hyp_name, arg(H, 1), pr1);
pr2 = Fun(hyp_name, arg(H, 2), pr2);
new_m.insert(goal_name, DisjCases(arg(H, 1), arg(H, 2), conclusion, mk_constant(hyp_name), pr1, pr2));
pr1 = Fun(hyp_name, arg(Href, 1), pr1);
pr2 = Fun(hyp_name, arg(Href, 2), pr2);
new_m.insert(goal_name, DisjCases(arg(Href, 1), arg(Href, 2), conclusion, mk_constant(hyp_name), pr1, pr2));
new_m.erase(name(goal_name, 1));
new_m.erase(name(goal_name, 2));
return pb(new_m, a);
@ -248,7 +249,7 @@ optional<proof_state_pair> disj_tactic(proof_state const & s, name gname) {
optional<proof_state_pair>();
}
buffer<std::pair<name, goal>> new_goals_buf1, new_goals_buf2;
expr conclusion;
optional<expr> conclusion;
for (auto const & p : s.get_goals()) {
check_interrupted();
goal const & g = p.second;
@ -276,12 +277,12 @@ optional<proof_state_pair> disj_tactic(proof_state const & s, name gname) {
proof_builder pb = s.get_proof_builder();
proof_builder new_pb1 = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
proof_map new_m(m);
new_m.insert(gname, Disj1(arg(conclusion, 1), arg(conclusion, 2), find(m, gname)));
new_m.insert(gname, Disj1(arg(*conclusion, 1), arg(*conclusion, 2), find(m, gname)));
return pb(new_m, a);
});
proof_builder new_pb2 = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
proof_map new_m(m);
new_m.insert(gname, Disj2(arg(conclusion, 2), arg(conclusion, 1), find(m, gname)));
new_m.insert(gname, Disj2(arg(*conclusion, 2), arg(*conclusion, 1), find(m, gname)));
return pb(new_m, a);
});
proof_state s1(precision::Over, new_gs1, s.get_menv(), new_pb1, s.get_cex_builder());
@ -323,7 +324,7 @@ tactic disj_tactic(unsigned i) {
tactic absurd_tactic() {
return mk_tactic01([](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
list<std::pair<name, expr>> proofs;
goals new_gs = map_goals(s, [&](name const & gname, goal const & g) -> goal {
goals new_gs = map_goals(s, [&](name const & gname, goal const & g) -> optional<goal> {
expr const & c = g.get_conclusion();
for (auto const & p1 : g.get_hypotheses()) {
check_interrupted();
@ -333,12 +334,12 @@ tactic absurd_tactic() {
if (p2.second == a) {
expr pr = AbsurdImpAny(a, c, mk_constant(p2.first), mk_constant(p1.first));
proofs.emplace_front(gname, pr);
return goal(); // remove goal
return optional<goal>(); // remove goal
}
}
}
}
return g; // keep goal
return some(g); // keep goal
});
if (empty(proofs))
return none_proof_state(); // tactic failed

48
src/library/tactic/goal.cpp
View file

@ -76,10 +76,10 @@ static name_set collect_used_names(context const & ctx, expr const & t) {
auto f = [&r](expr const & e, unsigned) { if (is_constant(e)) r.insert(const_name(e)); return true; };
for_each_fn<decltype(f)> visitor(f);
for (auto const & e : ctx) {
if (expr const & d = e.get_domain())
visitor(d);
if (expr const & b = e.get_body())
visitor(b);
if (optional<expr> const & d = e.get_domain())
visitor(*d);
if (optional<expr> const & b = e.get_body())
visitor(*b);
}
visitor(t);
return r;
@ -109,7 +109,7 @@ std::pair<goal, goal_proof_fn> to_goal(environment const & env, context const &
entries.push_back(e);
std::reverse(entries.begin(), entries.end());
buffer<hypothesis> hypotheses; // normalized names and types of the entries processed so far
buffer<expr> bodies; // normalized bodies of the entries processed so far
buffer<optional<expr>> bodies; // normalized bodies of the entries processed so far
std::vector<expr> consts; // cached consts[i] == mk_constant(names[i], hypotheses[i])
auto replace_vars = [&](expr const & e, unsigned offset) -> expr {
if (is_var(e)) {
@ -121,7 +121,7 @@ std::pair<goal, goal_proof_fn> to_goal(environment const & env, context const &
throw exception("to_goal failed, unknown free variable");
unsigned lvl = nfv - nvidx - 1;
if (bodies[lvl])
return bodies[lvl];
return *(bodies[lvl]);
else
return consts[lvl];
}
@ -134,20 +134,22 @@ std::pair<goal, goal_proof_fn> to_goal(environment const & env, context const &
for (; it != end; ++it) {
auto const & e = *it;
name n = mk_unique_name(used_names, e.get_name());
expr d = replacer(e.get_domain());
expr b = replacer(e.get_body());
optional<expr> d = e.get_domain();
optional<expr> b = e.get_body();
if (d) d = some(replacer(*d));
if (b) b = some(replacer(*b));
if (b && !d) {
d = inferer(b);
d = some(inferer(*b));
}
replacer.clear();
if (b && !inferer.is_proposition(d)) {
if (b && !inferer.is_proposition(*d)) {
bodies.push_back(b);
consts.push_back(expr());
} else {
lean_assert(d);
hypotheses.emplace_back(n, d);
bodies.push_back(expr());
consts.push_back(mk_constant(n, d));
hypotheses.emplace_back(n, *d);
bodies.push_back(optional<expr>());
consts.push_back(mk_constant(n, *d));
}
}
expr conclusion = replacer(t);
@ -162,9 +164,9 @@ static int mk_hypotheses(lua_State * L) {
if (nargs == 0) {
return push_hypotheses(L, hypotheses());
} else if (nargs == 2) {
return push_hypotheses(L, hypotheses(mk_pair(to_name_ext(L, 1), to_nonnull_expr(L, 2)), hypotheses()));
return push_hypotheses(L, hypotheses(mk_pair(to_name_ext(L, 1), to_expr(L, 2)), hypotheses()));
} else if (nargs == 3) {
return push_hypotheses(L, hypotheses(mk_pair(to_name_ext(L, 1), to_nonnull_expr(L, 2)), to_hypotheses(L, 3)));
return push_hypotheses(L, hypotheses(mk_pair(to_name_ext(L, 1), to_expr(L, 2)), to_hypotheses(L, 3)));
} else {
throw exception("hypotheses functions expects 0 (empty list), 2 (name & expr for singleton hypotheses list), or 3 (name & expr & hypotheses list) arguments");
}
@ -233,12 +235,7 @@ static const struct luaL_Reg hypotheses_m[] = {
DECL_UDATA(goal)
static int mk_goal(lua_State * L) {
return push_goal(L, goal(to_hypotheses(L, 1), to_nonnull_expr(L, 2)));
}
static int goal_is_null(lua_State * L) {
lua_pushboolean(L, !to_goal(L, 1));
return 1;
return push_goal(L, goal(to_hypotheses(L, 1), to_expr(L, 2)));
}
static int goal_hypotheses(lua_State * L) {
@ -256,13 +253,9 @@ static int goal_unique_name(lua_State * L) {
static int goal_tostring(lua_State * L) {
std::ostringstream out;
goal & g = to_goal(L, 1);
if (g) {
formatter fmt = get_global_formatter(L);
options opts = get_global_options(L);
out << mk_pair(g.pp(fmt, opts), opts);
} else {
out << "<null-goal>";
}
lua_pushstring(L, out.str().c_str());
return 1;
}
@ -270,9 +263,7 @@ static int goal_tostring(lua_State * L) {
static int goal_pp(lua_State * L) {
int nargs = lua_gettop(L);
goal & g = to_goal(L, 1);
if (!g) {
return push_format(L, format());
} else if (nargs == 1) {
if (nargs == 1) {
return push_format(L, g.pp(get_global_formatter(L), get_global_options(L)));
} else if (nargs == 2) {
if (is_formatter(L, 2))
@ -287,7 +278,6 @@ static int goal_pp(lua_State * L) {
static const struct luaL_Reg goal_m[] = {
{"__gc", goal_gc}, // never throws
{"__tostring", safe_function<goal_tostring>},
{"is_null", safe_function<goal_is_null>},
{"hypotheses", safe_function<goal_hypotheses>},
{"hyps", safe_function<goal_hypotheses>},
{"conclusion", safe_function<goal_conclusion>},

1
src/library/tactic/goal.h
View file

@ -26,7 +26,6 @@ public:
goal(hypotheses const & hs, expr const & c);
hypotheses const & get_hypotheses() const { return m_hypotheses; }
expr const & get_conclusion() const { return m_conclusion; }
explicit operator bool() const { return static_cast<bool>(m_conclusion); }
format pp(formatter const & fmt, options const & opts) const;
name mk_unique_hypothesis_name(name const & suggestion) const;
};

6
src/library/tactic/proof_builder.cpp
View file

@ -50,7 +50,7 @@ static int proof_map_find(lua_State * L) {
}
static int proof_map_insert(lua_State * L) {
to_proof_map(L, 1).insert(to_name_ext(L, 2), to_nonnull_expr(L, 3));
to_proof_map(L, 1).insert(to_name_ext(L, 2), to_expr(L, 3));
return 0;
}
@ -80,7 +80,7 @@ static int mk_assignment(lua_State * L) {
}
static int assignment_call(lua_State * L) {
return push_expr(L, to_assignment(L, 1)(to_name_ext(L, 2)));
return push_optional_expr(L, to_assignment(L, 1)(to_name_ext(L, 2)));
}
static const struct luaL_Reg assignment_m[] = {
@ -104,7 +104,7 @@ static int mk_proof_builder(lua_State * L) {
push_proof_map(L, m);
push_assignment(L, a);
pcall(L, 2, 1, 0);
r = to_nonnull_expr(L, -1);
r = to_expr(L, -1);
lua_pop(L, 1);
});
return r;

2
src/library/tactic/proof_state.cpp
View file

@ -223,7 +223,7 @@ static int mk_proof_state(lua_State * L) {
}
static int to_proof_state(lua_State * L) {
return push_proof_state(L, to_proof_state(to_environment(L, 1), to_context(L, 2), to_nonnull_expr(L, 3)));
return push_proof_state(L, to_proof_state(to_environment(L, 1), to_context(L, 2), to_expr(L, 3)));
}
static int proof_state_tostring(lua_State * L) {

4
src/library/tactic/proof_state.h
View file

@ -107,10 +107,10 @@ template<typename F>
goals map_goals(proof_state const & s, F && f) {
return map_filter(s.get_goals(), [=](std::pair<name, goal> const & in, std::pair<name, goal> & out) -> bool {
check_interrupted();
goal new_goal = f(in.first, in.second);
optional<goal> new_goal = f(in.first, in.second);
if (new_goal) {
out.first = in.first;
out.second = new_goal;
out.second = *new_goal;
return true;
} else {
return false;

26
src/library/tactic/tactic.cpp
View file

@ -184,9 +184,9 @@ tactic suppress_trace(tactic const & t) {
tactic assumption_tactic() {
return mk_tactic01([](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
list<std::pair<name, expr>> proofs;
goals new_gs = map_goals(s, [&](name const & gname, goal const & g) -> goal {
goals new_gs = map_goals(s, [&](name const & gname, goal const & g) -> optional<goal> {
expr const & c = g.get_conclusion();
expr pr;
optional<expr> pr;
for (auto const & p : g.get_hypotheses()) {
check_interrupted();
if (p.second == c) {
@ -195,10 +195,10 @@ tactic assumption_tactic() {
}
}
if (pr) {
proofs.emplace_front(gname, pr);
return goal();
proofs.emplace_front(gname, *pr);
return optional<goal>();
} else {
return g;
return some(g);
}
});
if (empty(proofs))
@ -410,13 +410,13 @@ public:
};
optional<proof_state> unfold_tactic_core(unfold_core_fn & fn, proof_state const & s) {
goals new_gs = map_goals(s, [&](name const &, goal const & g) -> goal {
goals new_gs = map_goals(s, [&](name const &, goal const & g) -> optional<goal> {
hypotheses new_hs = map(g.get_hypotheses(), [&](hypothesis const & h) { return hypothesis(h.first, fn(h.second)); });
expr new_c = fn(g.get_conclusion());
return goal(new_hs, new_c);
return some(goal(new_hs, new_c));
});
if (fn.unfolded()) {
return proof_state(s, new_gs);
return some(proof_state(s, new_gs));
} else {
return none_proof_state();
}
@ -464,13 +464,13 @@ public:
tactic beta_tactic() {
return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
beta_fn fn;
goals new_gs = map_goals(s, [&](name const &, goal const & g) -> goal {
goals new_gs = map_goals(s, [&](name const &, goal const & g) -> optional<goal> {
hypotheses new_hs = map(g.get_hypotheses(), [&](hypothesis const & h) { return hypothesis(h.first, fn(h.second)); });
expr new_c = fn(g.get_conclusion());
return goal(new_hs, new_c);
return some(goal(new_hs, new_c));
});
if (fn.reduced()) {
return proof_state(s, new_gs);
return some(proof_state(s, new_gs));
} else {
return none_proof_state();
}
@ -660,10 +660,10 @@ static int tactic_solve(lua_State * L) {
} else {
io_state * ios = get_io_state(L);
check_ios(ios);
return tactic_solve_core(L, t, env, *ios, to_context(L, 3), to_nonnull_expr(L, 4));
return tactic_solve_core(L, t, env, *ios, to_context(L, 3), to_expr(L, 4));
}
} else {
return tactic_solve_core(L, t, env, to_io_state(L, 3), to_context(L, 4), to_nonnull_expr(L, 5));
return tactic_solve_core(L, t, env, to_io_state(L, 3), to_context(L, 4), to_expr(L, 5));
}
}

12
src/library/type_inferer.cpp
View file

@ -104,7 +104,7 @@ class type_inferer::imp {
case expr_kind::MetaVar:
if (m_menv) {
if (m_menv->is_assigned(e))
return infer_type(m_menv->get_subst(e), ctx);
return infer_type(*(m_menv->get_subst(e)), ctx);
else
return m_menv->get_type(e);
} else {
@ -112,7 +112,7 @@ class type_inferer::imp {
}
case expr_kind::Constant: {
if (const_type(e)) {
return const_type(e);
return *const_type(e);
} else {
object const & obj = m_env.get_object(const_name(e));
if (obj.has_type())
@ -127,7 +127,7 @@ class type_inferer::imp {
context_entry const & ce = p.first;
if (ce.get_domain()) {
context const & ce_ctx = p.second;
return lift_free_vars(ce.get_domain(), ctx.size() - ce_ctx.size());
return lift_free_vars(*(ce.get_domain()), ctx.size() - ce_ctx.size());
}
// Remark: the case where ce.get_domain() is not
// available is not considered cheap.
@ -164,7 +164,7 @@ class type_inferer::imp {
context_entry const & ce = p.first;
context const & ce_ctx = p.second;
lean_assert(!ce.get_domain());
r = lift_free_vars(infer_type(ce.get_body(), ce_ctx), ctx.size() - ce_ctx.size());
r = lift_free_vars(infer_type(*(ce.get_body()), ce_ctx), ctx.size() - ce_ctx.size());
break;
}
case expr_kind::App: {
@ -269,9 +269,9 @@ static int type_inferer_call(lua_State * L) {
int nargs = lua_gettop(L);
type_inferer & inferer = to_type_inferer(L, 1);
if (nargs == 2)
return push_expr(L, inferer(to_nonnull_expr(L, 2)));
return push_expr(L, inferer(to_expr(L, 2)));
else
return push_expr(L, inferer(to_nonnull_expr(L, 2), to_context(L, 3)));
return push_expr(L, inferer(to_expr(L, 2), to_context(L, 3)));
}
static int type_inferer_clear(lua_State * L) {

2
src/library/update_expr.cpp
View file

@ -60,7 +60,7 @@ expr update_abstraction(expr const & abst, expr const & d, expr const & b) {
return update_pi(abst, d, b);
}
expr update_let(expr const & let, expr const & t, expr const & v, expr const & b) {
expr update_let(expr const & let, optional<expr> const & t, expr const & v, expr const & b) {
if (is_eqp(let_type(let), t) && is_eqp(let_value(let), v) && is_eqp(let_body(let), b))
return let;
else

2
src/library/update_expr.h
View file

@ -37,7 +37,7 @@ expr update_abstraction(expr const & abst, expr const & d, expr const & b);
\remark Return \c let if the given value and body are (pointer) equal to the ones in \c let.
*/
expr update_let(expr const & let, expr const & t, expr const & v, expr const & b);
expr update_let(expr const & let, optional<expr> const & t, expr const & v, expr const & b);
/**
\brief Return a new equality with lhs \c l and rhs \c r.

4
src/tests/kernel/expr.cpp
View file

@ -278,7 +278,7 @@ static void tst13() {
static void tst14() {
expr t = Eq(Const("a"), Const("b"));
std::cout << t << "\n";
expr l = mk_let("a", expr(), Const("b"), Var(0));
expr l = mk_let("a", optional<expr>(), Const("b"), Var(0));
std::cout << l << "\n";
lean_assert(closed(l));
}
@ -327,7 +327,7 @@ static void tst16() {
check_copy(mk_metavar("M"));
check_copy(mk_lambda("x", a, Var(0)));
check_copy(mk_pi("x", a, Var(0)));
check_copy(mk_let("x", expr(), a, Var(0)));
check_copy(mk_let("x", optional<expr>(), a, Var(0)));
}
static void tst17() {

2
src/tests/kernel/metavar.cpp
View file

@ -61,7 +61,7 @@ static void tst1() {
menv.assign(m1, f(a));
lean_assert(menv.is_assigned(m1));
lean_assert(!menv.is_assigned(m2));
lean_assert(menv.get_subst(m1) == f(a));
lean_assert(*(menv.get_subst(m1)) == f(a));
}
static void tst2() {

2
src/tests/kernel/normalizer.cpp
View file

@ -200,7 +200,7 @@ static void tst3() {
static void tst4() {
environment env;
env.add_var("b", Type());
expr t1 = mk_let("a", expr(), Const("b"), mk_lambda("c", Type(), Var(1)(Var(0))));
expr t1 = mk_let("a", optional<expr>(), Const("b"), mk_lambda("c", Type(), Var(1)(Var(0))));
std::cout << t1 << " --> " << normalize(t1, env) << "\n";
lean_assert(normalize(t1, env) == mk_lambda("c", Type(), Const("b")(Var(0))));
}

4
src/tests/kernel/type_checker.cpp
View file

@ -82,7 +82,7 @@ static void tst3() {
expr f = Fun("a", Bool, Eq(Const("a"), True));
std::cout << infer_type(f, env) << "\n";
lean_assert(infer_type(f, env) == mk_arrow(Bool, Bool));
expr t = mk_let("a", expr(), True, Var(0));
expr t = mk_let("a", optional<expr>(), True, Var(0));
std::cout << infer_type(t, env) << "\n";
}
@ -205,7 +205,7 @@ static void tst11() {
expr t3 = f(b, b);
for (unsigned i = 0; i < n; i++) {
t1 = f(t1, t1);
t2 = mk_let("x", expr(), t2, f(Var(0), Var(0)));
t2 = mk_let("x", optional<expr>(), t2, f(Var(0), Var(0)));
t3 = f(t3, t3);
}
lean_assert(t1 != t2);

12
src/tests/library/elaborator/elaborator.cpp
View file

@ -652,7 +652,7 @@ void tst20() {
while (true) {
try {
auto sol = elb.next();
std::cout << m1 << " -> " << sol.get_subst(m1) << "\n";
std::cout << m1 << " -> " << *(sol.get_subst(m1)) << "\n";
std::cout << instantiate_metavars(l, sol) << "\n";
lean_assert(instantiate_metavars(l, sol) == r);
std::cout << "--------------\n";
@ -684,7 +684,7 @@ void tst21() {
while (true) {
try {
auto sol = elb.next();
std::cout << m1 << " -> " << sol.get_subst(m1) << "\n";
std::cout << m1 << " -> " << *(sol.get_subst(m1)) << "\n";
std::cout << instantiate_metavars(l, sol) << "\n";
lean_assert(instantiate_metavars(l, sol) == r);
std::cout << "--------------\n";
@ -718,8 +718,8 @@ void tst22() {
while (true) {
try {
auto sol = elb.next();
std::cout << m3 << " -> " << sol.get_subst(m3) << "\n";
lean_assert(sol.get_subst(m3) == iVal(1));
std::cout << m3 << " -> " << *(sol.get_subst(m3)) << "\n";
lean_assert(*(sol.get_subst(m3)) == iVal(1));
std::cout << instantiate_metavars(l, sol) << "\n";
std::cout << instantiate_metavars(r, sol) << "\n";
std::cout << "--------------\n";
@ -748,7 +748,7 @@ void tst23() {
while (true) {
try {
auto sol = elb.next();
std::cout << m1 << " -> " << sol.get_subst(m1) << "\n";
std::cout << m1 << " -> " << *(sol.get_subst(m1)) << "\n";
std::cout << instantiate_metavars(l, sol) << "\n";
lean_assert_eq(instantiate_metavars(l, sol),
instantiate_metavars(r, sol));
@ -797,7 +797,7 @@ void tst25() {
while (true) {
try {
auto sol = elb.next();
std::cout << m1 << " -> " << sol.get_subst(m1) << "\n";
std::cout << m1 << " -> " << *(sol.get_subst(m1)) << "\n";
std::cout << instantiate_metavars(l, sol) << "\n";
lean_assert_eq(beta_reduce(instantiate_metavars(l, sol)),
beta_reduce(instantiate_metavars(r, sol)));

1
src/tests/library/expr_lt.cpp
View file

@ -34,7 +34,6 @@ static void tst1() {
lt(Const("a"), Const("b"), true);
lt(Const("a"), Const("a"), false);
lt(Var(1), Const("a"), true);
lt(expr(), Var(0), true);
lt(Eq(Var(0), Var(1)), Eq(Var(1), Var(1)), true);
lt(Eq(Var(1), Var(0)), Eq(Var(1), Var(1)), true);
lt(Eq(Var(1), Var(1)), Eq(Var(1), Var(1)), false);

4
src/tests/library/update_expr.cpp
View file

@ -40,9 +40,9 @@ void tst3() {
expr b = Const("b");
expr f = Const("f");
expr t1 = Let(a, b, f(a));
expr t2 = update_let(t1, expr(), b, let_body(t1));
expr t2 = update_let(t1, optional<expr>(), b, let_body(t1));
lean_assert(is_eqp(t1, t2));
t2 = update_let(t1, expr(), a, let_body(t1));
t2 = update_let(t1, optional<expr>(), a, let_body(t1));
lean_assert(!is_eqp(t1, t2));
lean_assert(t2 == Let(a, a, f(a)));
}

19
src/util/optional.h
View file

@ -20,8 +20,9 @@ class optional {
};
public:
optional():m_some(false) {}
optional(T const & v):m_some(true) {
new (&m_value) T(v);
optional(optional & other):m_some(other.m_some) {
if (m_some)
new (&m_value) T(other.m_value);
}
optional(optional const & other):m_some(other.m_some) {
if (m_some)
@ -31,9 +32,15 @@ public:
if (m_some)
new (&m_value) T(std::forward<T>(other.m_value));
}
explicit optional(T const & v):m_some(true) {
new (&m_value) T(v);
}
explicit optional(T && v):m_some(true) {
new (&m_value) T(std::forward<T>(v));
}
template<typename... Args>
optional(Args&&... args):m_some(true) {
new (&m_value) T(args...);
explicit optional(Args&&... args):m_some(true) {
new (&m_value) T(std::forward<Args>(args)...);
}
~optional() {
if (m_some)
@ -95,6 +102,10 @@ public:
else
return !o1.m_some || o1.m_value == o2.m_value;
}
friend bool operator!=(optional const & o1, optional const & o2) {
return !operator==(o1, o2);
}
};
template<typename T> optional<T> some(T const & t) { return optional<T>(t); }

2
src/util/scoped_map.h
View file

@ -108,7 +108,7 @@ public:
auto it = m_map.find(k);
if (it == m_map.end()) {
if (!at_base_lvl())
m_actions.emplace_back(action_kind::Insert, value_type(k, T()));
m_actions.emplace_back(action_kind::Insert, value_type(k, v /* dummy */));
m_map.insert(value_type(k, v));
} else {
if (!at_base_lvl())

2
tests/lua/context1.lua
View file

@ -4,7 +4,7 @@ print(c)
e = context_entry("x", Const("N"))
assert(e:get_name() == name("x"))
assert(e:get_domain() == Const("N"))
assert(e:get_body():is_null())
assert(not e:get_body())
print(e:get_body())
c = context(c, e)
print(c)

2
tests/lua/env2.lua
View file

@ -6,7 +6,7 @@ for v in env:objects() do
print(v:get_name())
end
end
assert(not env:find_object("N"):is_null())
assert(env:find_object("N"))
assert(env:find_object("Z"):is_null())
assert(env:find_object("N"):is_var_decl())
assert(env:find_object("N"):has_type())

2
tests/lua/env4.lua
View file

@ -11,7 +11,7 @@ for o in child:local_objects() do
print(o)
end
local eenv = empty_environment()
assert(eenv:find_object("Int"):is_null())
print(eenv:find_object("Int"):is_null())
assert(not pcall(function() env:parent() end))
local p = child:parent()
assert(p:has_children())

6
tests/lua/expr6.lua
View file

@ -1,6 +1,5 @@
function print_leaves(e, ctx)
if e:is_null() then
if (not e) then
return
end
local k = e:kind()
@ -46,6 +45,3 @@ local F = fun(h, mk_arrow(N, N),
Let(x, h(a), Eq(f(x), h(x))))
print(F)
print_leaves(F, context())

1
tests/lua/goal1.lua
View file

@ -21,7 +21,6 @@ assert(is_goal(g))
print(g)
assert(#(g:hypotheses()) == 2)
assert(g:conclusion() == Const("p1"))
assert(not g:is_null())
assert(g:unique_name("H") == name("H"))
assert(g:unique_name("H1") == name("H1", 1))
print(g:pp())

2
tests/lua/jst1.lua
View file

@ -8,4 +8,4 @@ for c in j1:children() do
end
assert(not j2:has_children())
print(j1)
assert(j1:get_main_expr():is_null())
assert(not j1:get_main_expr())