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

refactor(kernel/metavar_env): use the same approach used in the class environment in the class metavar_env

Browse source 
This modification was motivated by a bug exposed by tst17 at tests/kernel/type_checker.
metavar_env is now a smart point to metavar_env_cell.
ro_metavar_env is a read-only smart pointer. It is useful to make sure we are using proof_state correctly.

example showing that the approach for caching metavar_env is broken in the type_checker

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-12 17:47:11 -08:00
parent 26afc6cf12
commit 51aee83b70
30 changed files with 793 additions and 600 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -147,7 +147,7 @@ class frontend_elaborator::imp {
virtual expr visit_constant(expr const & e, context const & ctx) { virtual expr visit_constant(expr const & e, context const & ctx) {
if (is_placeholder(e)) { if (is_placeholder(e)) {
expr m = m_ref.m_menv.mk_metavar(ctx, visit(const_type(e), ctx)); expr m = m_ref.m_menv->mk_metavar(ctx, visit(const_type(e), ctx));
m_ref.m_trace[m] = e; m_ref.m_trace[m] = e;
return m; return m;
} else { } else {
@ -186,7 +186,7 @@ class frontend_elaborator::imp {
expr add_coercion_mvar_app(list<expr_pair> const & l, expr const & a, expr const & a_t, expr add_coercion_mvar_app(list<expr_pair> const & l, expr const & a, expr const & a_t,
context const & ctx, expr const & original_a) { context const & ctx, expr const & original_a) {
buffer<expr> choices; buffer<expr> choices;
expr mvar = m_ref.m_menv.mk_metavar(ctx); expr mvar = m_ref.m_menv->mk_metavar(ctx);
for (auto p : l) { for (auto p : l) {
choices.push_back(p.second); choices.push_back(p.second);
} }
@ -292,7 +292,7 @@ class frontend_elaborator::imp {
*/ */
expr mk_overload_mvar(buffer<expr> & f_choices, context const & ctx, expr const & src) { expr mk_overload_mvar(buffer<expr> & f_choices, context const & ctx, expr const & src) {
std::reverse(f_choices.begin(), f_choices.end()); std::reverse(f_choices.begin(), f_choices.end());
expr mvar = m_ref.m_menv.mk_metavar(ctx); expr mvar = m_ref.m_menv->mk_metavar(ctx);
m_ref.m_ucs.push_back(mk_choice_constraint(ctx, mvar, f_choices.size(), f_choices.data(), m_ref.m_ucs.push_back(mk_choice_constraint(ctx, mvar, f_choices.size(), f_choices.data(),
mk_overload_justification(ctx, src))); mk_overload_justification(ctx, src)));
return mvar; return mvar;
@ -436,13 +436,13 @@ public:
expr new_e = preprocessor(*this)(e); expr new_e = preprocessor(*this)(e);
// std::cout << "After preprocessing\n" << new_e << "\n"; // std::cout << "After preprocessing\n" << new_e << "\n";
if (has_metavar(new_e)) { if (has_metavar(new_e)) {
m_type_checker.infer_type(new_e, context(), &m_menv, &m_ucs); m_type_checker.infer_type(new_e, context(), m_menv, m_ucs);
// for (auto c : m_ucs) { // for (auto c : m_ucs) {
// formatter fmt = mk_simple_formatter(); // formatter fmt = mk_simple_formatter();
// std::cout << c.pp(fmt, options(), nullptr, false) << "\n"; // std::cout << c.pp(fmt, options(), nullptr, false) << "\n";
// } // }
metavar_env new_menv = elaborate_core(); metavar_env new_menv = elaborate_core();
return instantiate_metavars(new_e, new_menv); return new_menv->instantiate_metavars(new_e);
} else { } else {
return new_e; return new_e;
} }
@ -455,8 +455,8 @@ public:
expr new_e = preprocessor(*this)(e); expr new_e = preprocessor(*this)(e);
// std::cout << "After preprocessing\n" << new_t << "\n" << new_e << "\n"; // std::cout << "After preprocessing\n" << new_t << "\n" << new_e << "\n";
if (has_metavar(new_e) || has_metavar(new_t)) { if (has_metavar(new_e) || has_metavar(new_t)) {
m_type_checker.infer_type(new_t, context(), &m_menv, &m_ucs); m_type_checker.infer_type(new_t, context(), m_menv, m_ucs);
expr new_e_t = m_type_checker.infer_type(new_e, context(), &m_menv, &m_ucs); expr new_e_t = m_type_checker.infer_type(new_e, context(), m_menv, m_ucs);
m_ucs.push_back(mk_convertible_constraint(context(), new_e_t, new_t, m_ucs.push_back(mk_convertible_constraint(context(), new_e_t, new_t,
mk_def_type_match_justification(context(), n, e))); mk_def_type_match_justification(context(), n, e)));
// for (auto c : m_ucs) { // for (auto c : m_ucs) {
@ -464,8 +464,8 @@ public:
// std::cout << c.pp(fmt, options(), nullptr, false) << "\n"; // std::cout << c.pp(fmt, options(), nullptr, false) << "\n";
// } // }
metavar_env new_menv = elaborate_core(); metavar_env new_menv = elaborate_core();
return std::make_tuple(instantiate_metavars(new_t, new_menv), return std::make_tuple(new_menv->instantiate_metavars(new_t),
instantiate_metavars(new_e, new_menv), new_menv->instantiate_metavars(new_e),
new_menv); new_menv);
} else { } else {
return std::make_tuple(new_t, new_e, metavar_env()); return std::make_tuple(new_t, new_e, metavar_env());

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

@ -1393,19 +1393,19 @@ class parser::imp {
*/ */
expr mk_proof_for(proof_state const & s, pos_info const & p, context const & ctx, expr const & expected_type) { expr mk_proof_for(proof_state const & s, pos_info const & p, context const & ctx, expr const & expected_type) {
if (s.is_proof_final_state()) { if (s.is_proof_final_state()) {
assignment a(s.get_menv()); assignment a(s.get_menv().copy());
proof_map m; proof_map m;
expr pr = s.get_proof_builder()(m, a); expr pr = s.get_proof_builder()(m, a);
if (has_metavar(pr)) { if (has_metavar(pr)) {
// Some tactics generate metavariables that can only be instantiated by type inference elaboration. // Some tactics generate metavariables that can only be instantiated by type inference elaboration.
// Example: apply_tactic. // Example: apply_tactic.
metavar_env menv = s.get_menv(); metavar_env menv = s.get_menv().copy();
buffer<unification_constraint> ucs; buffer<unification_constraint> ucs;
expr pr_type = type_checker(m_frontend.get_environment()).infer_type(pr, ctx, &menv, &ucs); expr pr_type = type_checker(m_frontend.get_environment()).infer_type(pr, ctx, menv, ucs);
ucs.push_back(mk_convertible_constraint(ctx, pr_type, expected_type, mk_type_match_justification(ctx, expected_type, pr))); ucs.push_back(mk_convertible_constraint(ctx, pr_type, expected_type, mk_type_match_justification(ctx, expected_type, pr)));
elaborator elb(m_frontend.get_environment(), s.get_menv(), ucs.size(), ucs.data(), m_frontend.get_options()); elaborator elb(m_frontend.get_environment(), menv, ucs.size(), ucs.data(), m_frontend.get_options());
metavar_env new_menv = elb.next(); metavar_env new_menv = elb.next();
pr = instantiate_metavars(pr, new_menv); pr = new_menv->instantiate_metavars(pr);
if (has_metavar(pr)) if (has_metavar(pr))
throw exception("synthesized proof object has unsolved metavars"); throw exception("synthesized proof object has unsolved metavars");
} }
@ -1585,15 +1585,15 @@ class parser::imp {
}); });
std::sort(mvars.begin(), mvars.end(), [](expr const & e1, expr const & e2) { return is_lt(e1, e2, false); }); std::sort(mvars.begin(), mvars.end(), [](expr const & e1, expr const & e2) { return is_lt(e1, e2, false); });
for (auto mvar : mvars) { for (auto mvar : mvars) {
expr mvar_type = instantiate_metavars(menv.get_type(mvar), menv); expr mvar_type = menv->instantiate_metavars(menv->get_type(mvar));
if (has_metavar(mvar_type)) if (has_metavar(mvar_type))
throw exception("failed to synthesize metavar, its type contains metavariables"); throw exception("failed to synthesize metavar, its type contains metavariables");
buffer<context_entry> new_entries; buffer<context_entry> new_entries;
for (auto e : menv.get_context(mvar)) { for (auto e : menv->get_context(mvar)) {
optional<expr> d = e.get_domain(); optional<expr> d = e.get_domain();
optional<expr> b = e.get_body(); optional<expr> b = e.get_body();
if (d) d = instantiate_metavars(*d, menv); if (d) d = menv->instantiate_metavars(*d);
if (b) b = instantiate_metavars(*b, menv); if (b) b = menv->instantiate_metavars(*b);
if (d) if (d)
new_entries.emplace_back(e.get_name(), *d, b); new_entries.emplace_back(e.get_name(), *d, b);
else else
@ -1607,7 +1607,7 @@ class parser::imp {
if (hint_and_pos.first) { if (hint_and_pos.first) {
// metavariable has an associated tactic hint // metavariable has an associated tactic hint
s = apply_tactic(s, *(hint_and_pos.first), hint_and_pos.second).first; s = apply_tactic(s, *(hint_and_pos.first), hint_and_pos.second).first;
menv.assign(mvar, mk_proof_for(s, hint_and_pos.second, mvar_ctx, mvar_type)); menv->assign(mvar, mk_proof_for(s, hint_and_pos.second, mvar_ctx, mvar_type));
} else { } else {
if (curr_is_period()) { if (curr_is_period()) {
display_proof_state_if_interactive(s); display_proof_state_if_interactive(s);
@ -1615,10 +1615,10 @@ class parser::imp {
next(); next();
} }
expr mvar_val = parse_tactic_cmds(s, mvar_ctx, mvar_type); expr mvar_val = parse_tactic_cmds(s, mvar_ctx, mvar_type);
menv.assign(mvar, mvar_val); menv->assign(mvar, mvar_val);
} }
} }
return instantiate_metavars(val, menv); return menv->instantiate_metavars(val);
} }
/** \brief Auxiliary method used for parsing definitions and theorems. */ /** \brief Auxiliary method used for parsing definitions and theorems. */

27
src/kernel/free_vars.cpp
View file

@ -128,7 +128,7 @@ class free_var_range_fn {
*/ */
unsigned process_metavar(expr const & m) { unsigned process_metavar(expr const & m) {
lean_assert(is_metavar(m)); lean_assert(is_metavar(m));
context ctx = m_menv.get_context(metavar_name(m)); context ctx = m_menv->get_context(metavar_name(m));
unsigned R = ctx.size(); unsigned R = ctx.size();
if (has_local_context(m)) { if (has_local_context(m)) {
local_context lctx = metavar_lctx(m); local_context lctx = metavar_lctx(m);
@ -316,7 +316,7 @@ protected:
return result; return result;
} }
public: public:
has_free_var_in_range_fn(unsigned low, unsigned high, metavar_env const * menv): has_free_var_in_range_fn(unsigned low, unsigned high, optional<metavar_env> const & menv):
m_low(low), m_low(low),
m_high(high) { m_high(high) {
lean_assert(low < high); lean_assert(low < high);
@ -326,11 +326,14 @@ public:
bool operator()(expr const & e) { return apply(e, 0); } bool operator()(expr const & e) { return apply(e, 0); }
}; };
bool has_free_var(expr const & e, unsigned low, unsigned high, metavar_env const * menv) { bool has_free_var(expr const & e, unsigned low, unsigned high, optional<metavar_env> const & menv) { return has_free_var_in_range_fn(low, high, menv)(e); }
return has_free_var_in_range_fn(low, high, menv)(e); bool has_free_var(expr const & e, unsigned low, unsigned high, metavar_env const & menv) { return has_free_var(e, low, high, some_menv(menv)); }
} bool has_free_var(expr const & e, unsigned low, unsigned high) { return has_free_var(e, low, high, none_menv()); }
bool has_free_var(expr const & e, unsigned i, optional<metavar_env> const & menv) { return has_free_var(e, i, i+1, menv); }
bool has_free_var(expr const & e, unsigned i, metavar_env const & menv) { return has_free_var(e, i, i+1, menv); }
bool has_free_var(expr const & e, unsigned i) { return has_free_var(e, i, i+1); }
expr lower_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const * DEBUG_CODE(menv)) { expr lower_free_vars(expr const & e, unsigned s, unsigned d, optional<metavar_env> const & DEBUG_CODE(menv)) {
lean_assert(s >= d); lean_assert(s >= d);
lean_assert(!has_free_var(e, s-d, s, menv)); lean_assert(!has_free_var(e, s-d, s, menv));
auto f = [=](expr const & e, unsigned offset) -> expr { auto f = [=](expr const & e, unsigned offset) -> expr {
@ -343,8 +346,13 @@ expr lower_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const *
}; };
return replace_fn<decltype(f)>(f)(e); return replace_fn<decltype(f)>(f)(e);
} }
expr lower_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const & menv) { return lower_free_vars(e, s, d, some_menv(menv)); }
expr lower_free_vars(expr const & e, unsigned s, unsigned d) { return lower_free_vars(e, s, d, none_menv()); }
expr lower_free_vars(expr const & e, unsigned d, optional<metavar_env> const & menv) { return lower_free_vars(e, d, d, menv); }
expr lower_free_vars(expr const & e, unsigned d, metavar_env const & menv) { return lower_free_vars(e, d, d, menv); }
expr lower_free_vars(expr const & e, unsigned d) { return lower_free_vars(e, d, d); }
expr lift_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const * menv) { expr lift_free_vars(expr const & e, unsigned s, unsigned d, optional<metavar_env> const & menv) {
if (d == 0) if (d == 0)
return e; return e;
auto f = [=](expr const & e, unsigned offset) -> expr { auto f = [=](expr const & e, unsigned offset) -> expr {
@ -358,4 +366,9 @@ expr lift_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const *
}; };
return replace_fn<decltype(f)>(f)(e); return replace_fn<decltype(f)>(f)(e);
} }
expr lift_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const & menv) { return lift_free_vars(e, s, d, some_menv(menv)); }
expr lift_free_vars(expr const & e, unsigned s, unsigned d) { return lift_free_vars(e, s, d, none_menv()); }
expr lift_free_vars(expr const & e, unsigned d, optional<metavar_env> const & menv) { return lift_free_vars(e, 0, d, menv); }
expr lift_free_vars(expr const & e, unsigned d) { return lift_free_vars(e, 0, d); }
expr lift_free_vars(expr const & e, unsigned d, metavar_env const & menv) { return lift_free_vars(e, 0, d, menv); }
} }

38
src/kernel/free_vars.h
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/ */
#pragma once #pragma once
#include "kernel/expr.h" #include "kernel/expr.h"
#include "kernel/metavar.h"
namespace lean { namespace lean {
/** /**
\brief Return true iff the given expression has free variables. \brief Return true iff the given expression has free variables.
@ -40,18 +41,18 @@ unsigned free_var_range(expr const & e, metavar_env const & menv);
\brief Return true iff \c e constains a free variable <tt>(var i)</tt> s.t. \c i in <tt>[low, high)</tt>. \brief Return true iff \c e constains a free variable <tt>(var i)</tt> s.t. \c i in <tt>[low, high)</tt>.
\pre low < high \pre low < high
\remark If menv != nullptr, then we use \c free_var_range to compute the free variables that may \remark If menv is not none, then we use \c free_var_range to compute the free variables that may
occur in a metavariable. occur in a metavariable.
*/ */
bool has_free_var(expr const & e, unsigned low, unsigned high, metavar_env const * menv = nullptr); bool has_free_var(expr const & e, unsigned low, unsigned high, optional<metavar_env> const & menv);
inline bool has_free_var(expr const & e, unsigned low, unsigned high, metavar_env const & menv) { bool has_free_var(expr const & e, unsigned low, unsigned high, metavar_env const & menv);
return has_free_var(e, low, high, &menv); bool has_free_var(expr const & e, unsigned low, unsigned high);
}
/** /**
\brief Return true iff \c e contains the free variable <tt>(var i)</tt>. \brief Return true iff \c e contains the free variable <tt>(var i)</tt>.
*/ */
inline bool has_free_var(expr const & e, unsigned i, metavar_env const * menv = nullptr) { return has_free_var(e, i, i+1, menv); } bool has_free_var(expr const & e, unsigned i, optional<metavar_env> const & menv);
inline bool has_free_var(expr const & e, unsigned i, metavar_env const & menv) { return has_free_var(e, i, i+1, &menv); } bool has_free_var(expr const & e, unsigned i, metavar_env const & menv);
bool has_free_var(expr const & e, unsigned i);
/** /**
\brief Lower the free variables >= s in \c e by \c d. That is, a free variable <tt>(var i)</tt> s.t. \brief Lower the free variables >= s in \c e by \c d. That is, a free variable <tt>(var i)</tt> s.t.
@ -62,20 +63,23 @@ inline bool has_free_var(expr const & e, unsigned i, metavar_env const & menv) {
\remark The parameter menv is only used for debugging purposes \remark The parameter menv is only used for debugging purposes
*/ */
expr lower_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const * menv = nullptr); expr lower_free_vars(expr const & e, unsigned s, unsigned d, optional<metavar_env> const & menv);
inline expr lower_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const & menv) { expr lower_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const & menv);
return lower_free_vars(e, s, d, &menv); expr lower_free_vars(expr const & e, unsigned s, unsigned d);
} expr lower_free_vars(expr const & e, unsigned d, optional<metavar_env> const & menv);
inline expr lower_free_vars(expr const & e, unsigned d, metavar_env const * menv = nullptr) { return lower_free_vars(e, d, d, menv); } expr lower_free_vars(expr const & e, unsigned d, metavar_env const & menv);
expr lower_free_vars(expr const & e, unsigned d);
/** /**
\brief Lift free variables >= s in \c e by d. \brief Lift free variables >= s in \c e by d.
\remark When the parameter menv != nullptr, this function will minimize the use \remark When the parameter menv is not none, this function will minimize the use
of the local entry lift in metavariables occurring in \c e. of the local entry lift in metavariables occurring in \c e.
*/ */
expr lift_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const * menv = nullptr); expr lift_free_vars(expr const & e, unsigned s, unsigned d, optional<metavar_env> const & menv);
inline expr lift_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const & menv) { return lift_free_vars(e, s, d, &menv); } expr lift_free_vars(expr const & e, unsigned s, unsigned d);
inline expr lift_free_vars(expr const & e, unsigned d, metavar_env const * menv = nullptr) { return lift_free_vars(e, 0, d, menv); } expr lift_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const & menv);
inline expr lift_free_vars(expr const & e, unsigned d, metavar_env const & menv) { return lift_free_vars(e, 0, d, &menv); } expr lift_free_vars(expr const & e, unsigned d, optional<metavar_env> const & menv);
expr lift_free_vars(expr const & e, unsigned d, metavar_env const & menv);
expr lift_free_vars(expr const & e, unsigned d);
} }

47
src/kernel/instantiate.cpp
View file

@ -12,7 +12,7 @@ Author: Leonardo de Moura
#include "kernel/instantiate.h" #include "kernel/instantiate.h"
namespace lean { namespace lean {
expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, metavar_env const * menv) { expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, optional<metavar_env> const & menv) {
auto f = [=](expr const & m, unsigned offset) -> expr { auto f = [=](expr const & m, unsigned offset) -> expr {
if (is_var(m)) { if (is_var(m)) {
unsigned vidx = var_idx(m); unsigned vidx = var_idx(m);
@ -35,13 +35,24 @@ expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s,
}; };
return replace_fn<decltype(f)>(f)(a); return replace_fn<decltype(f)>(f)(a);
} }
expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, metavar_env const & menv) {
expr instantiate_with_closed(expr const & a, unsigned n, expr const * s, metavar_env const * menv) { return instantiate_with_closed_relaxed(a, n, s, some_menv(menv));
}
expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s) {
return instantiate_with_closed_relaxed(a, n, s, none_menv());
}
expr instantiate_with_closed(expr const & a, unsigned n, expr const * s, optional<metavar_env> const & menv) {
lean_assert(std::all_of(s, s+n, [&](expr const & e) { return !has_free_var(e, 0, std::numeric_limits<unsigned>::max(), menv); })); lean_assert(std::all_of(s, s+n, [&](expr const & e) { return !has_free_var(e, 0, std::numeric_limits<unsigned>::max(), menv); }));
return instantiate_with_closed_relaxed(a, n, s, menv); return instantiate_with_closed_relaxed(a, n, s, menv);
} }
expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, metavar_env const & menv) { return instantiate_with_closed(e, n, s, some_menv(menv)); }
expr instantiate_with_closed(expr const & e, unsigned n, expr const * s) { return instantiate_with_closed(e, n, s, none_menv()); }
expr instantiate_with_closed(expr const & e, std::initializer_list<expr> const & l) { return instantiate_with_closed(e, l.size(), l.begin()); }
expr instantiate_with_closed(expr const & e, expr const & s, optional<metavar_env> const & menv) { return instantiate_with_closed(e, 1, &s, menv); }
expr instantiate_with_closed(expr const & e, expr const & s) { return instantiate_with_closed(e, 1, &s); }
expr instantiate_with_closed(expr const & e, expr const & s, metavar_env const & menv) { return instantiate_with_closed(e, s, some_menv(menv)); }
expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst, metavar_env const * menv) { expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst, optional<metavar_env> const & menv) {
auto f = [=](expr const & m, unsigned offset) -> expr { auto f = [=](expr const & m, unsigned offset) -> expr {
if (is_var(m)) { if (is_var(m)) {
unsigned vidx = var_idx(m); unsigned vidx = var_idx(m);
@ -64,18 +75,22 @@ expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst, met
}; };
return replace_fn<decltype(f)>(f)(a); return replace_fn<decltype(f)>(f)(a);
} }
expr instantiate(expr const & e, unsigned n, expr const * s, metavar_env const * menv) { expr instantiate(expr const & e, unsigned n, expr const * s, optional<metavar_env> const & menv) { return instantiate(e, 0, n, s, menv); }
return instantiate(e, 0, n, s, menv); expr instantiate(expr const & e, unsigned n, expr const * s, metavar_env const & menv) { return instantiate(e, n, s, some_menv(menv)); }
} expr instantiate(expr const & e, unsigned n, expr const * s) { return instantiate(e, n, s, none_menv()); }
expr instantiate(expr const & e, unsigned i, expr const & s, metavar_env const * menv) { expr instantiate(expr const & e, std::initializer_list<expr> const & l) { return instantiate(e, l.size(), l.begin()); }
return instantiate(e, i, 1, &s, menv); expr instantiate(expr const & e, unsigned i, expr const & s, optional<metavar_env> const & menv) { return instantiate(e, i, 1, &s, menv); }
} expr instantiate(expr const & e, unsigned i, expr const & s, metavar_env const & menv) { return instantiate(e, i, 1, &s, some_menv(menv)); }
expr instantiate(expr const & e, unsigned i, expr const & s) { return instantiate(e, i, 1, &s, none_menv()); }
expr instantiate(expr const & e, expr const & s, optional<metavar_env> const & menv) { return instantiate(e, 1, &s, menv); }
expr instantiate(expr const & e, expr const & s, metavar_env const & menv) { return instantiate(e, s, some_menv(menv)); }
expr instantiate(expr const & e, expr const & s) { return instantiate(e, s, none_menv()); }
bool is_head_beta(expr const & t) { bool is_head_beta(expr const & t) {
return is_app(t) && is_lambda(arg(t, 0)); return is_app(t) && is_lambda(arg(t, 0));
} }
expr apply_beta(expr f, unsigned num_args, expr const * args, metavar_env const * menv) { expr apply_beta(expr f, unsigned num_args, expr const * args, optional<metavar_env> const & menv) {
lean_assert(is_lambda(f)); lean_assert(is_lambda(f));
unsigned m = 1; unsigned m = 1;
while (is_lambda(abst_body(f)) && m < num_args) { while (is_lambda(abst_body(f)) && m < num_args) {
@ -94,16 +109,20 @@ expr apply_beta(expr f, unsigned num_args, expr const * args, metavar_env const
return mk_app(new_args); return mk_app(new_args);
} }
} }
expr apply_beta(expr f, unsigned num_args, expr const * args, metavar_env const & menv) { return apply_beta(f, num_args, args, some_menv(menv)); }
expr apply_beta(expr f, unsigned num_args, expr const * args) { return apply_beta(f, num_args, args, none_menv()); }
expr head_beta_reduce(expr const & t, metavar_env const * menv) { expr head_beta_reduce(expr const & t, optional<metavar_env> const & menv) {
if (!is_head_beta(t)) { if (!is_head_beta(t)) {
return t; return t;
} else { } else {
return apply_beta(arg(t, 0), num_args(t) - 1, &arg(t, 1), menv); return apply_beta(arg(t, 0), num_args(t) - 1, &arg(t, 1), menv);
} }
} }
expr head_beta_reduce(expr const & t) { return head_beta_reduce(t, none_menv()); }
expr head_beta_reduce(expr const & t, metavar_env const & menv) { return head_beta_reduce(t, some_menv(menv)); }
expr beta_reduce(expr t, metavar_env const * menv) { expr beta_reduce(expr t, optional<metavar_env> const & menv) {
auto f = [=](expr const & m, unsigned) -> expr { auto f = [=](expr const & m, unsigned) -> expr {
if (is_head_beta(m)) if (is_head_beta(m))
return head_beta_reduce(m, menv); return head_beta_reduce(m, menv);
@ -118,4 +137,6 @@ expr beta_reduce(expr t, metavar_env const * menv) {
t = new_t; t = new_t;
} }
} }
expr beta_reduce(expr t, metavar_env const & menv) { return beta_reduce(t, some_menv(menv)); }
expr beta_reduce(expr t) { return beta_reduce(t, none_menv()); }
} }

86
src/kernel/instantiate.h
View file

@ -14,70 +14,60 @@ class metavar_env;
\pre s[0], ..., s[n-1] must be closed expressions (i.e., no free variables). \pre s[0], ..., s[n-1] must be closed expressions (i.e., no free variables).
\remark When the parameter menv != nullptr, this function will minimize the use \remark When the parameter menv is not none, this function will minimize the use
of the local entry inst in metavariables occurring in \c e. of the local entry inst in metavariables occurring in \c e.
*/ */
expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, metavar_env const * menv = nullptr); expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, optional<metavar_env> const & menv);
inline expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, metavar_env const & menv) { expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, metavar_env const & menv);
return instantiate_with_closed(e, n, s, &menv); expr instantiate_with_closed(expr const & e, unsigned n, expr const * s);
} expr instantiate_with_closed(expr const & e, std::initializer_list<expr> const & l);
inline expr instantiate_with_closed(expr const & e, std::initializer_list<expr> const & l) { expr instantiate_with_closed(expr const & e, expr const & s, optional<metavar_env> const & menv);
return instantiate_with_closed(e, l.size(), l.begin()); expr instantiate_with_closed(expr const & e, expr const & s, metavar_env const & menv);
} expr instantiate_with_closed(expr const & e, expr const & s);
inline expr instantiate_with_closed(expr const & e, expr const & s, metavar_env const * menv = nullptr) {
return instantiate_with_closed(e, 1, &s, menv);
}
inline expr instantiate_with_closed(expr const & e, expr const & s, metavar_env const & menv) {
return instantiate_with_closed(e, s, &menv);
}
/** /**
\brief Similar to instantiate_with_closed, but does not use an assertion for \brief Similar to instantiate_with_closed, but does not use an assertion for
testing whether arguments are close or not. testing whether arguments are close or not.
This version is useful, for example, when we want to treat metavariables as closed terms. This version is useful, for example, when we want to treat metavariables as closed terms.
*/ */
expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, metavar_env const * menv = nullptr); expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, optional<metavar_env> const & menv);
inline expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, metavar_env const & menv) { expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, metavar_env const & menv);
return instantiate_with_closed_relaxed(a, n, s, menv); expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s);
}
/** /**
\brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e. \brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e.
\remark When the parameter menv != nullptr, this function will minimize the use \remark When the parameter menv is not none, this function will minimize the use
of the local entry inst in metavariables occurring in \c e. of the local entry inst in metavariables occurring in \c e.
*/ */
expr instantiate(expr const & e, unsigned n, expr const * s, metavar_env const * menv = nullptr); expr instantiate(expr const & e, unsigned n, expr const * s, optional<metavar_env> const & menv);
inline expr instantiate(expr const & e, unsigned n, expr const * s, metavar_env const & menv) { expr instantiate(expr const & e, unsigned n, expr const * s, metavar_env const & menv);
return instantiate(e, n, s, &menv); expr instantiate(expr const & e, unsigned n, expr const * s);
} expr instantiate(expr const & e, std::initializer_list<expr> const & l);
inline expr instantiate(expr const & e, std::initializer_list<expr> const & l) {
return instantiate(e, l.size(), l.begin());
}
inline expr instantiate(expr const & e, expr const & s, metavar_env const * menv = nullptr) {
return instantiate(e, 1, &s, menv);
}
inline expr instantiate(expr const & e, expr const & s, metavar_env const & menv) {
return instantiate(e, s, &menv);
}
/** /**
\brief Replace free variable \c i with \c s in \c e. \brief Replace free variable \c i with \c s in \c e.
*/ */
expr instantiate(expr const & e, unsigned i, expr const & s, metavar_env const * menv = nullptr); expr instantiate(expr const & e, unsigned i, expr const & s, optional<metavar_env> const & menv);
inline expr instantiate(expr const & e, unsigned i, expr const & s, metavar_env const & menv) { expr instantiate(expr const & e, unsigned i, expr const & s, metavar_env const & menv);
return instantiate(e, i, s, &menv); expr instantiate(expr const & e, unsigned i, expr const & s);
} /**
\brief Replace free variable \c 0 with \c s in \c e.
*/
expr instantiate(expr const & e, expr const & s, optional<metavar_env> const & menv);
expr instantiate(expr const & e, expr const & s, metavar_env const & menv);
expr instantiate(expr const & e, expr const & s);
expr apply_beta(expr f, unsigned num_args, expr const * args, optional<metavar_env> const & menv);
expr apply_beta(expr f, unsigned num_args, expr const * args, metavar_env const & menv);
expr apply_beta(expr f, unsigned num_args, expr const * args);
expr apply_beta(expr f, unsigned num_args, expr const * args, metavar_env const * menv = nullptr);
inline expr apply_beta(expr f, unsigned num_args, expr const * args, metavar_env const & menv) {
return apply_beta(f, num_args, args, &menv);
}
bool is_head_beta(expr const & t); bool is_head_beta(expr const & t);
expr head_beta_reduce(expr const & t, metavar_env const * menv = nullptr);
inline expr head_beta_reduce(expr const & t, metavar_env const & menv) { expr head_beta_reduce(expr const & t, optional<metavar_env> const & menv);
return head_beta_reduce(t, &menv); expr head_beta_reduce(expr const & t, metavar_env const & menv);
} expr head_beta_reduce(expr const & t);
expr beta_reduce(expr t, metavar_env const * menv = nullptr);
inline expr beta_reduce(expr t, metavar_env const & menv) { expr beta_reduce(expr t, optional<metavar_env> const & menv);
return beta_reduce(t, &menv); expr beta_reduce(expr t, metavar_env const & menv);
} expr beta_reduce(expr t);
} }

189
src/kernel/metavar.cpp
View file

@ -51,26 +51,35 @@ public:
virtual optional<expr> get_main_expr() const { return some_expr(m_expr); } virtual optional<expr> get_main_expr() const { return some_expr(m_expr); }
}; };
void metavar_env::inc_timestamp() { void metavar_env_cell::inc_timestamp() {
if (m_timestamp == std::numeric_limits<unsigned>::max()) { if (m_timestamp == std::numeric_limits<unsigned>::max()) {
// This should not happen in real examples. We add it just to be safe. // This should not happen in real examples. We add it just to be safe.
throw exception("metavar_env timestamp overflow"); throw exception("metavar_env_cell timestamp overflow");
} }
m_timestamp++; m_timestamp++;
} }
metavar_env::metavar_env(name const & prefix): metavar_env_cell::metavar_env_cell(name const & prefix):
m_name_generator(prefix), m_name_generator(prefix),
m_beta_reduce_mv(true), m_beta_reduce_mv(true),
m_timestamp(0) { m_timestamp(1),
m_rc(0) {
} }
static name g_default_name("M"); static name g_default_name("M");
metavar_env::metavar_env(): metavar_env_cell::metavar_env_cell():
metavar_env(g_default_name) { metavar_env_cell(g_default_name) {
} }
expr metavar_env::mk_metavar(context const & ctx, optional<expr> const & type) { metavar_env_cell::metavar_env_cell(metavar_env_cell const & other):
m_name_generator(other.m_name_generator),
m_metavar_data(other.m_metavar_data),
m_beta_reduce_mv(other.m_beta_reduce_mv),
m_timestamp(0),
m_rc(0) {
}
expr metavar_env_cell::mk_metavar(context const & ctx, optional<expr> const & type) {
inc_timestamp(); inc_timestamp();
name m = m_name_generator.next(); name m = m_name_generator.next();
expr r = ::lean::mk_metavar(m); expr r = ::lean::mk_metavar(m);
@ -78,33 +87,33 @@ expr metavar_env::mk_metavar(context const & ctx, optional<expr> const & type) {
return r; return r;
} }
context metavar_env::get_context(expr const & m) const { context metavar_env_cell::get_context(expr const & m) const {
lean_assert(is_metavar(m)); lean_assert(is_metavar(m));
lean_assert(!has_local_context(m)); lean_assert(!has_local_context(m));
return get_context(metavar_name(m)); return get_context(metavar_name(m));
} }
context metavar_env::get_context(name const & m) const { context metavar_env_cell::get_context(name const & m) const {
auto it = m_metavar_data.find(m); auto it = m_metavar_data.find(m);
lean_assert(it); lean_assert(it);
return it->m_context; return it->m_context;
} }
expr metavar_env::get_type(expr const & m) { expr metavar_env_cell::get_type(expr const & m) {
lean_assert(is_metavar(m)); lean_assert(is_metavar(m));
expr t = get_type(metavar_name(m)); expr t = get_type(metavar_name(m));
if (has_local_context(m)) { if (has_local_context(m)) {
if (is_metavar(t)) { if (is_metavar(t)) {
return update_metavar(t, append(metavar_lctx(m), metavar_lctx(t))); return update_metavar(t, append(metavar_lctx(m), metavar_lctx(t)));
} else { } else {
return apply_local_context(t, metavar_lctx(m)); return apply_local_context(t, metavar_lctx(m), metavar_env(this));
} }
} else { } else {
return t; return t;
} }
} }
expr metavar_env::get_type(name const & m) { expr metavar_env_cell::get_type(name const & m) {
auto it = m_metavar_data.find(m); auto it = m_metavar_data.find(m);
lean_assert(it); lean_assert(it);
if (it->m_type) { if (it->m_type) {
@ -116,23 +125,23 @@ expr metavar_env::get_type(name const & m) {
} }
} }
bool metavar_env::has_type(name const & m) const { bool metavar_env_cell::has_type(name const & m) const {
auto it = m_metavar_data.find(m); auto it = m_metavar_data.find(m);
lean_assert(it); lean_assert(it);
return static_cast<bool>(it->m_type); return static_cast<bool>(it->m_type);
} }
bool metavar_env::has_type(expr const & m) const { bool metavar_env_cell::has_type(expr const & m) const {
lean_assert(is_metavar(m)); lean_assert(is_metavar(m));
return has_type(metavar_name(m)); return has_type(metavar_name(m));
} }
optional<justification> metavar_env::get_justification(expr const & m) const { optional<justification> metavar_env_cell::get_justification(expr const & m) const {
lean_assert(is_metavar(m)); lean_assert(is_metavar(m));
return get_justification(metavar_name(m)); return get_justification(metavar_name(m));
} }
optional<justification> metavar_env::get_justification(name const & m) const { optional<justification> metavar_env_cell::get_justification(name const & m) const {
auto r = get_subst_jst(m); auto r = get_subst_jst(m);
if (r) if (r)
return optional<justification>(r->second); return optional<justification>(r->second);
@ -140,17 +149,17 @@ optional<justification> metavar_env::get_justification(name const & m) const {
return optional<justification>(); return optional<justification>();
} }
bool metavar_env::is_assigned(name const & m) const { bool metavar_env_cell::is_assigned(name const & m) const {
auto it = m_metavar_data.find(m); auto it = m_metavar_data.find(m);
return it && it->m_subst; return it && it->m_subst;
} }
bool metavar_env::is_assigned(expr const & m) const { bool metavar_env_cell::is_assigned(expr const & m) const {
lean_assert(is_metavar(m)); lean_assert(is_metavar(m));
return is_assigned(metavar_name(m)); return is_assigned(metavar_name(m));
} }
void metavar_env::assign(name const & m, expr const & t, justification const & jst) { void metavar_env_cell::assign(name const & m, expr const & t, justification const & jst) {
lean_assert(!is_assigned(m)); lean_assert(!is_assigned(m));
inc_timestamp(); inc_timestamp();
auto it = m_metavar_data.find(m); auto it = m_metavar_data.find(m);
@ -159,24 +168,24 @@ void metavar_env::assign(name const & m, expr const & t, justification const & j
it->m_justification = jst; it->m_justification = jst;
} }
void metavar_env::assign(expr const & m, expr const & t, justification const & j) { void metavar_env_cell::assign(expr const & m, expr const & t, justification const & j) {
lean_assert(is_metavar(m)); lean_assert(is_metavar(m));
lean_assert(!has_local_context(m)); lean_assert(!has_local_context(m));
assign(metavar_name(m), t, j); assign(metavar_name(m), t, j);
} }
expr apply_local_context(expr const & a, local_context const & lctx) { expr apply_local_context(expr const & a, local_context const & lctx, optional<metavar_env> const & menv) {
if (lctx) { if (lctx) {
if (is_metavar(a)) { if (is_metavar(a)) {
return mk_metavar(metavar_name(a), append(lctx, metavar_lctx(a))); return mk_metavar(metavar_name(a), append(lctx, metavar_lctx(a)));
} else { } else {
expr r = apply_local_context(a, tail(lctx)); expr r = apply_local_context(a, tail(lctx), menv);
local_entry const & e = head(lctx); local_entry const & e = head(lctx);
if (e.is_lift()) { if (e.is_lift()) {
return lift_free_vars(r, e.s(), e.n()); return lift_free_vars(r, e.s(), e.n(), menv);
} else { } else {
lean_assert(e.is_inst()); lean_assert(e.is_inst());
return instantiate(r, e.s(), e.v()); return instantiate(r, e.s(), e.v(), menv);
} }
} }
} else { } else {
@ -184,30 +193,31 @@ expr apply_local_context(expr const & a, local_context const & lctx) {
} }
} }
optional<std::pair<expr, justification>> metavar_env::get_subst_jst(expr const & m) const { optional<std::pair<expr, justification>> metavar_env_cell::get_subst_jst(expr const & m) const {
lean_assert(is_metavar(m)); lean_assert(is_metavar(m));
auto p = get_subst_jst(metavar_name(m)); auto p = get_subst_jst(metavar_name(m));
if (p) { if (p) {
expr r = p->first; expr r = p->first;
local_context const & lctx = metavar_lctx(m); local_context const & lctx = metavar_lctx(m);
if (lctx) if (lctx)
r = apply_local_context(r, lctx); r = apply_local_context(r, lctx, metavar_env(const_cast<metavar_env_cell*>(this)));
return some(mk_pair(r, p->second)); return some(mk_pair(r, p->second));
} else { } else {
return p; return p;
} }
} }
optional<std::pair<expr, justification>> metavar_env::get_subst_jst(name const & m) const { optional<std::pair<expr, justification>> metavar_env_cell::get_subst_jst(name const & m) const {
auto it = const_cast<metavar_env*>(this)->m_metavar_data.find(m); auto it = const_cast<metavar_env_cell*>(this)->m_metavar_data.find(m);
if (it->m_subst) { if (it->m_subst) {
expr s = *(it->m_subst); expr s = *(it->m_subst);
if (has_assigned_metavar(s, *this)) { if (has_assigned_metavar(s)) {
buffer<justification> jsts; buffer<justification> jsts;
expr new_subst = instantiate_metavars(s, *this, jsts); expr new_subst = instantiate_metavars(s, jsts);
if (!jsts.empty()) { if (!jsts.empty()) {
it->m_justification = justification(new normalize_assignment_justification(it->m_context, s, it->m_justification, justification new_jst(new normalize_assignment_justification(it->m_context, s, it->m_justification,
jsts.size(), jsts.data())); jsts.size(), jsts.data()));
it->m_justification = new_jst;
it->m_subst = new_subst; it->m_subst = new_subst;
} }
} }
@ -217,7 +227,7 @@ optional<std::pair<expr, justification>> metavar_env::get_subst_jst(name const &
} }
} }
optional<expr> metavar_env::get_subst(name const & m) const { optional<expr> metavar_env_cell::get_subst(name const & m) const {
auto r = get_subst_jst(m); auto r = get_subst_jst(m);
if (r) if (r)
return some_expr(r->first); return some_expr(r->first);
@ -225,7 +235,7 @@ optional<expr> metavar_env::get_subst(name const & m) const {
return none_expr(); return none_expr();
} }
optional<expr> metavar_env::get_subst(expr const & m) const { optional<expr> metavar_env_cell::get_subst(expr const & m) const {
auto r = get_subst_jst(m); auto r = get_subst_jst(m);
if (r) if (r)
return some_expr(r->first); return some_expr(r->first);
@ -233,10 +243,45 @@ optional<expr> metavar_env::get_subst(expr const & m) const {
return none_expr(); return none_expr();
} }
bool metavar_env_cell::has_assigned_metavar(expr const & e) const {
if (!has_metavar(e)) {
return false;
} else {
bool result = false;
for_each(e, [&](expr const & n, unsigned) {
if (result)
return false;
if (!has_metavar(n))
return false;
if (is_metavar(n) && is_assigned(n)) {
result = true;
return false;
}
return true;
});
return result;
}
}
bool metavar_env_cell::has_metavar(expr const & e, expr const & m) const {
if (has_metavar(e)) {
lean_assert(is_metavar(m));
lean_assert(!is_assigned(m));
return static_cast<bool>(find(e, [&](expr const & m2) {
return
is_metavar(m2) &&
((metavar_name(m) == metavar_name(m2)) ||
(is_assigned(m2) && has_metavar(*get_subst(m2), m)));
}));
} else {
return false;
}
}
class instantiate_metavars_proc : public replace_visitor { class instantiate_metavars_proc : public replace_visitor {
protected: protected:
metavar_env const & m_menv; metavar_env_cell const * m_menv;
buffer<justification> & m_jsts; buffer<justification> & m_jsts;
void push_back(justification const & jst) { void push_back(justification const & jst) {
if (jst) if (jst)
@ -244,12 +289,12 @@ protected:
} }
virtual expr visit_metavar(expr const & m, context const & ctx) { virtual expr visit_metavar(expr const & m, context const & ctx) {
if (is_metavar(m) && m_menv.is_assigned(m)) { if (is_metavar(m) && m_menv->is_assigned(m)) {
auto p = m_menv.get_subst_jst(m); auto p = m_menv->get_subst_jst(m);
lean_assert(p); lean_assert(p);
expr r = p->first; expr r = p->first;
push_back(p->second); push_back(p->second);
if (has_assigned_metavar(r, m_menv)) { if (m_menv->has_assigned_metavar(r)) {
return visit(r, ctx); return visit(r, ctx);
} else { } else {
return r; return r;
@ -261,7 +306,7 @@ protected:
virtual expr visit_app(expr const & e, context const & ctx) { virtual expr visit_app(expr const & e, context const & ctx) {
expr const & f = arg(e, 0); expr const & f = arg(e, 0);
if (m_menv.beta_reduce_metavar_application() && is_metavar(f) && m_menv.is_assigned(f)) { if (m_menv->beta_reduce_metavar_application() && is_metavar(f) && m_menv->is_assigned(f)) {
buffer<expr> new_args; buffer<expr> new_args;
for (unsigned i = 0; i < num_args(e); i++) for (unsigned i = 0; i < num_args(e); i++)
new_args.push_back(visit(arg(e, i), ctx)); new_args.push_back(visit(arg(e, i), ctx));
@ -275,37 +320,38 @@ protected:
} }
public: public:
instantiate_metavars_proc(metavar_env const & menv, buffer<justification> & jsts): instantiate_metavars_proc(metavar_env_cell const * menv, buffer<justification> & jsts):
m_menv(menv), m_menv(menv),
m_jsts(jsts) { m_jsts(jsts) {
} }
}; };
expr instantiate_metavars(expr const & e, metavar_env const & menv, buffer<justification> & jsts) { expr metavar_env_cell::instantiate_metavars(expr const & e, buffer<justification> & jsts) const {
if (!has_metavar(e)) { if (!has_metavar(e)) {
return e; return e;
} else { } else {
return instantiate_metavars_proc(menv, jsts)(e); return instantiate_metavars_proc(this, jsts)(e);
} }
} }
bool has_assigned_metavar(expr const & e, metavar_env const & menv) { bool cached_metavar_env::update(optional<metavar_env> const & menv) {
if (!has_metavar(e)) { if (!menv) {
return false; if (m_timestamp != 0) {
m_menv = none_menv();
m_timestamp = 0;
return true;
} else {
return false;
}
} else { } else {
bool result = false; unsigned new_timestamp = (*menv)->get_timestamp();
for_each(e, [&](expr const & n, unsigned) { if (m_menv != menv || m_timestamp != new_timestamp) {
if (result) m_menv = menv;
return false; m_timestamp = new_timestamp;
if (!has_metavar(n)) return true;
return false; } else {
if (is_metavar(n) && menv.is_assigned(n)) { return false;
result = true; }
return false;
}
return true;
});
return result;
} }
} }
@ -323,7 +369,7 @@ local_context add_lift(local_context const & lctx, unsigned s, unsigned n) {
return cons(mk_lift(s, n), lctx); return cons(mk_lift(s, n), lctx);
} }
expr add_lift(expr const & m, unsigned s, unsigned n, metavar_env const * menv) { expr add_lift(expr const & m, unsigned s, unsigned n, optional<metavar_env> const & menv) {
if (menv && s >= free_var_range(m, *menv)) if (menv && s >= free_var_range(m, *menv))
return m; return m;
return update_metavar(m, add_lift(metavar_lctx(m), s, n)); return update_metavar(m, add_lift(metavar_lctx(m), s, n));
@ -347,7 +393,7 @@ local_context add_inst(local_context const & lctx, unsigned s, expr const & v) {
return cons(mk_inst(s, v), lctx); return cons(mk_inst(s, v), lctx);
} }
expr add_inst(expr const & m, unsigned s, expr const & v, metavar_env const * menv) { expr add_inst(expr const & m, unsigned s, expr const & v, optional<metavar_env> const & menv) {
if (menv && s >= free_var_range(m, *menv)) if (menv && s >= free_var_range(m, *menv))
return m; return m;
return update_metavar(m, add_inst(metavar_lctx(m), s, v)); return update_metavar(m, add_inst(metavar_lctx(m), s, v));
@ -361,25 +407,4 @@ expr pop_meta_context(expr const & m) {
lean_assert(has_local_context(m)); lean_assert(has_local_context(m));
return update_metavar(m, tail(metavar_lctx(m))); return update_metavar(m, tail(metavar_lctx(m)));
} }
/**
\brief Auxiliary exception used to sign that a metavariable was
found in an expression.
*/
struct found_metavar {};
bool has_metavar(expr const & e, expr const & m, metavar_env const & menv) {
if (has_metavar(e)) {
lean_assert(is_metavar(m));
lean_assert(!menv.is_assigned(m));
return static_cast<bool>(find(e, [&](expr const & m2) {
return
is_metavar(m2) &&
((metavar_name(m) == metavar_name(m2)) ||
(menv.is_assigned(m2) && has_metavar(*menv.get_subst(m2), m, menv)));
}));
} else {
return false;
}
}
} }

150
src/kernel/metavar.h
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/ */
#pragma once #pragma once
#include <utility> #include <utility>
#include "util/rc.h"
#include "util/pair.h" #include "util/pair.h"
#include "util/splay_map.h" #include "util/splay_map.h"
#include "util/name_generator.h" #include "util/name_generator.h"
@ -16,14 +17,14 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
/** /**
\brief Metavar environment. It is an auxiliary datastructure used for: \brief Metavar environment (cell). It is an auxiliary datastructure used for:
1- Creating metavariables. 1- Creating metavariables.
2- Storing their types and the contexts where they were created. 2- Storing their types and the contexts where they were created.
3- Storing substitutions. 3- Storing substitutions.
4- Collecting constraints
*/ */
class metavar_env { class metavar_env_cell {
friend class metavar_env;
struct data { struct data {
optional<expr> m_subst; // substitution optional<expr> m_subst; // substitution
optional<expr> m_type; // type of the metavariable optional<expr> m_type; // type of the metavariable
@ -42,20 +43,24 @@ class metavar_env {
// bunch of assignments of the form ?m <- fun (x : T), ... // bunch of assignments of the form ?m <- fun (x : T), ...
bool m_beta_reduce_mv; bool m_beta_reduce_mv;
unsigned m_timestamp; unsigned m_timestamp;
MK_LEAN_RC();
static bool has_metavar(expr const & e) { return ::lean::has_metavar(e); }
void dealloc() { delete this; }
void inc_timestamp(); void inc_timestamp();
public: public:
metavar_env(name const & prefix); metavar_env_cell();
metavar_env(); metavar_env_cell(name const & prefix);
metavar_env_cell(metavar_env_cell const & other);
bool beta_reduce_metavar_application() const { return m_beta_reduce_mv; } bool beta_reduce_metavar_application() const { return m_beta_reduce_mv; }
void set_beta_reduce_metavar_application(bool f) { m_beta_reduce_mv = f; } void set_beta_reduce_metavar_application(bool f) { m_beta_reduce_mv = f; }
friend void swap(metavar_env & a, metavar_env & b);
/** /**
\brief The timestamp is increased whenever this environment is \brief The timestamp is increased whenever this environment is
updated. updated.
\remark The result is always greater than 0.
*/ */
unsigned get_timestamp() const { return m_timestamp; } unsigned get_timestamp() const { return m_timestamp; }
@ -152,22 +157,107 @@ public:
f(k, *(d.m_subst)); f(k, *(d.m_subst));
}); });
} }
/**
\brief Return true iff \c e has a metavariable that is assigned in \c menv.
*/
bool has_assigned_metavar(expr const & e) const;
/**
\brief Return true iff \c e contains the metavariable \c m.
The substitutions in this metavar environment are taken into account.
\brief is_metavar(m)
*/
bool has_metavar(expr const & e, expr const & m) const;
/**
\brief Instantiate the metavariables occurring in \c e with the substitutions
provided by \c menv. Store the justification of replace variables in jsts.
*/
expr instantiate_metavars(expr const & e, buffer<justification> & jsts) const;
inline expr instantiate_metavars(expr const & e) const {
buffer<justification> tmp;
return instantiate_metavars(e, tmp);
}
};
/**
\brief Reference to metavariable environment (cell).
*/
class metavar_env {
friend class optional<metavar_env>;
friend class ro_metavar_env;
friend class metavar_env_cell;
metavar_env_cell * m_ptr;
explicit metavar_env(metavar_env_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
public:
metavar_env():m_ptr(new metavar_env_cell()) { m_ptr->inc_ref(); }
metavar_env(name const & prefix):m_ptr(new metavar_env_cell(prefix)) { m_ptr->inc_ref(); }
metavar_env(metavar_env const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
metavar_env(metavar_env && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
~metavar_env() { if (m_ptr) m_ptr->dec_ref(); }
metavar_env & operator=(metavar_env const & s) { LEAN_COPY_REF(s); }
metavar_env & operator=(metavar_env && s) { LEAN_MOVE_REF(s); }
metavar_env_cell * operator->() const { return m_ptr; }
metavar_env_cell & operator*() const { return *m_ptr; }
metavar_env copy() const { return metavar_env(new metavar_env_cell(*m_ptr)); }
friend bool is_eqp(metavar_env const & menv1, metavar_env const & menv2) { return menv1.m_ptr == menv2.m_ptr; }
friend bool operator==(metavar_env const & menv1, metavar_env const & menv2) { return is_eqp(menv1, menv2); }
};
SPECIALIZE_OPTIONAL_FOR_SMART_PTR(metavar_env)
inline optional<metavar_env> none_menv() { return optional<metavar_env>(); }
inline optional<metavar_env> some_menv(metavar_env const & e) { return optional<metavar_env>(e); }
inline optional<metavar_env> some_menv(metavar_env && e) { return optional<metavar_env>(std::forward<metavar_env>(e)); }
/**
\brief Read-only reference to metavariable environment (cell).
*/
class ro_metavar_env {
metavar_env_cell * m_ptr;
public:
ro_metavar_env():m_ptr(new metavar_env_cell()) { m_ptr->inc_ref(); }
ro_metavar_env(metavar_env const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
ro_metavar_env(ro_metavar_env const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
ro_metavar_env(ro_metavar_env && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
~ro_metavar_env() { if (m_ptr) m_ptr->dec_ref(); }
ro_metavar_env & operator=(ro_metavar_env const & s) { LEAN_COPY_REF(s); }
ro_metavar_env & operator=(ro_metavar_env && s) { LEAN_MOVE_REF(s); }
metavar_env_cell const * operator->() const { return m_ptr; }
metavar_env_cell const & operator*() const { return *m_ptr; }
metavar_env copy() const { return metavar_env(new metavar_env_cell(*m_ptr)); }
};
/**
\brief A cached weak reference to a metavariable environment + timestamp at the time of
the caching. This object may also cache optional references.
*/
class cached_metavar_env {
optional<metavar_env> m_menv;
unsigned m_timestamp;
public:
cached_metavar_env():m_timestamp(0) {}
void clear() { m_menv = none_menv(); m_timestamp = 0; }
/**
\brief Updated the cached value with menv.
Return true if menv is different from the the cached metavar_env, or if
the timestamp is different.
*/
bool update(optional<metavar_env> const & menv);
bool update(metavar_env const & menv) { return update(some(menv)); }
explicit operator bool() const { return static_cast<bool>(m_menv); }
optional<metavar_env> const & to_some_menv() const { return m_menv; }
metavar_env operator*() const { return *m_menv; }
metavar_env_cell * operator->() const { lean_assert(m_menv); return (*m_menv).operator->(); }
}; };
/** /**
\brief Apply the changes in \c lctx to \c a. \brief Apply the changes in \c lctx to \c a.
*/ */
expr apply_local_context(expr const & a, local_context const & lctx); expr apply_local_context(expr const & a, local_context const & lctx, optional<metavar_env> const & menv);
inline expr apply_local_context(expr const & a, local_context const & lctx, metavar_env const & menv) { return apply_local_context(a, lctx, some_menv(menv)); }
/** inline expr apply_local_context(expr const & a, local_context const & lctx) { return apply_local_context(a, lctx, none_menv()); }
\brief Instantiate the metavariables occurring in \c e with the substitutions
provided by \c menv. Store the justification of replace variables in jsts.
*/
expr instantiate_metavars(expr const & e, metavar_env const & menv, buffer<justification> & jsts);
inline expr instantiate_metavars(expr const & e, metavar_env const & menv) {
buffer<justification> tmp;
return instantiate_metavars(e, menv, tmp);
}
/** /**
\brief Extend the local context \c lctx with the entry <tt>lift:s:n</tt> \brief Extend the local context \c lctx with the entry <tt>lift:s:n</tt>
@ -179,29 +269,31 @@ local_context add_lift(local_context const & lctx, unsigned s, unsigned n);
\pre is_metavar(m) \pre is_metavar(m)
\remark If menv != nullptr, then we use \c free_var_range to compute the free variables that may \remark If menv is not none, then we use \c free_var_range to compute the free variables that may
occur in \c m. If s > the maximum free variable that occurs in \c m, then occur in \c m. If s > the maximum free variable that occurs in \c m, then
we do not add a lift local entry to the local context. we do not add a lift local entry to the local context.
*/ */
expr add_lift(expr const & m, unsigned s, unsigned n, metavar_env const * menv = nullptr); expr add_lift(expr const & m, unsigned s, unsigned n, optional<metavar_env> const & menv);
inline expr add_lift(expr const & m, unsigned s, unsigned n, metavar_env const & menv) { return add_lift(m, s, n, &menv); } inline expr add_lift(expr const & m, unsigned s, unsigned n) { return add_lift(m, s, n, none_menv()); }
inline expr add_lift(expr const & m, unsigned s, unsigned n, metavar_env const & menv) { return add_lift(m, s, n, some_menv(menv)); }
/**
\brief Extend the local context \c lctx with the entry <tt>inst:s v</tt>
*/
local_context add_inst(local_context const & lctx, unsigned s, expr const & v);
/** /**
\brief Add an inst:s:v operation to the context of the given metavariable. \brief Add an inst:s:v operation to the context of the given metavariable.
\pre is_metavar(m) \pre is_metavar(m)
\remark If menv != nullptr, then we use \c free_var_range to compute the free variables that may \remark If menv is not none, then we use \c free_var_range to compute the free variables that may
occur in \c m. If s > the maximum free variable that occurs in \c m, then occur in \c m. If s > the maximum free variable that occurs in \c m, then
we do not add an inst local entry to the local context. we do not add an inst local entry to the local context.
*/ */
expr add_inst(expr const & m, unsigned s, expr const & v, metavar_env const * menv = nullptr); expr add_inst(expr const & m, unsigned s, expr const & v, optional<metavar_env> const & menv);
inline expr add_inst(expr const & m, unsigned s, expr const & v, metavar_env const & menv) { return add_inst(m, s, v, &menv); } inline expr add_inst(expr const & m, unsigned s, expr const & v) { return add_inst(m, s, v, none_menv()); }
inline expr add_inst(expr const & m, unsigned s, expr const & v, metavar_env const & menv) { return add_inst(m, s, v, some_menv(menv)); }
/**
\brief Extend the local context \c lctx with the entry <tt>inst:s v</tt>
*/
local_context add_inst(local_context const & lctx, unsigned s, expr const & v);
/** /**
\brief Return true iff the given metavariable has a non-empty \brief Return true iff the given metavariable has a non-empty

67
src/kernel/type_checker.cpp
View file

@ -27,8 +27,7 @@ class type_checker::imp {
cache m_cache; cache m_cache;
normalizer m_normalizer; normalizer m_normalizer;
context m_ctx; context m_ctx;
metavar_env * m_menv; cached_metavar_env m_menv;
unsigned m_menv_timestamp;
unification_constraints * m_uc; unification_constraints * m_uc;
ro_environment env() const { ro_environment env() const {
@ -95,10 +94,13 @@ class type_checker::imp {
switch (e.kind()) { switch (e.kind()) {
case expr_kind::MetaVar: case expr_kind::MetaVar:
if (m_menv) { if (m_menv) {
if (m_menv->is_assigned(e)) if (m_menv->is_assigned(e)) {
return infer_type_core(*(m_menv->get_subst(e)), ctx); optional<expr> s = m_menv->get_subst(e);
else lean_assert(s);
return infer_type_core(*s, ctx);
} else {
return m_menv->get_type(e); return m_menv->get_type(e);
}
} else { } else {
throw unexpected_metavar_occurrence(env(), e); throw unexpected_metavar_occurrence(env(), e);
} }
@ -148,9 +150,9 @@ class type_checker::imp {
if (closed(abst_body(f_t))) if (closed(abst_body(f_t)))
f_t = abst_body(f_t); f_t = abst_body(f_t);
else if (closed(c)) else if (closed(c))
f_t = instantiate_with_closed(abst_body(f_t), c); f_t = instantiate_with_closed(abst_body(f_t), c); // TODO(Leo): m_menv.to_some_menv());
else else
f_t = instantiate(abst_body(f_t), c); f_t = instantiate(abst_body(f_t), c); // TODO(Leo): m_menv.to_some_menv());
i++; i++;
if (i == num) if (i == num)
return save_result(e, f_t, shared); return save_result(e, f_t, shared);
@ -202,7 +204,9 @@ class type_checker::imp {
{ {
cache::mk_scope sc(m_cache); cache::mk_scope sc(m_cache);
expr t = infer_type_core(let_body(e), extend(ctx, let_name(e), lt, let_value(e))); expr t = infer_type_core(let_body(e), extend(ctx, let_name(e), lt, let_value(e)));
return save_result(e, instantiate(t, let_value(e)), shared); return save_result(e,
instantiate(t, let_value(e)), // TODO(Leo): m_menv.to_some_menv()),
shared);
} }
} }
case expr_kind::Value: { case expr_kind::Value: {
@ -267,40 +271,28 @@ class type_checker::imp {
} }
} }
void set_menv(metavar_env * menv) { void update_menv(optional<metavar_env> const & menv) {
if (m_menv == menv) { if (m_menv.update(menv))
// Check whether m_menv has been updated since the last time the type checker has been invoked clear_cache();
if (m_menv && m_menv->get_timestamp() > m_menv_timestamp) {
clear();
m_menv = menv;
m_menv_timestamp = m_menv->get_timestamp();
}
} else {
clear();
m_menv = menv;
m_menv_timestamp = m_menv ? m_menv->get_timestamp() : 0;
}
} }
public: public:
imp(ro_environment const & env): imp(ro_environment const & env):
m_env(env), m_env(env),
m_normalizer(env) { m_normalizer(env) {
m_menv = nullptr;
m_menv_timestamp = 0;
m_uc = nullptr; m_uc = nullptr;
} }
expr infer_type(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> * uc) { expr infer_type(expr const & e, context const & ctx, optional<metavar_env> const & menv, buffer<unification_constraint> * uc) {
set_ctx(ctx); set_ctx(ctx);
set_menv(menv); update_menv(menv);
flet<unification_constraints*> set_uc(m_uc, uc); flet<unification_constraints*> set_uc(m_uc, uc);
return infer_type_core(e, ctx); return infer_type_core(e, ctx);
} }
bool is_convertible(expr const & t1, expr const & t2, context const & ctx) { bool is_convertible(expr const & t1, expr const & t2, context const & ctx) {
set_ctx(ctx); set_ctx(ctx);
set_menv(nullptr); update_menv(none_menv());
auto mk_justification = [](){ auto mk_justification = [](){
lean_unreachable(); return justification(); // LCOV_EXCL_LINE lean_unreachable(); return justification(); // LCOV_EXCL_LINE
}; };
@ -309,17 +301,20 @@ public:
void check_type(expr const & e, context const & ctx) { void check_type(expr const & e, context const & ctx) {
set_ctx(ctx); set_ctx(ctx);
set_menv(nullptr); update_menv(none_menv());
expr t = infer_type_core(e, ctx); expr t = infer_type_core(e, ctx);
check_type(t, e, ctx); check_type(t, e, ctx);
} }
void clear() { void clear_cache() {
m_cache.clear(); m_cache.clear();
m_normalizer.clear(); m_normalizer.clear();
m_ctx = context(); }
m_menv = nullptr;
m_menv_timestamp = 0; void clear() {
clear_cache();
m_menv.clear();
m_ctx = context();
} }
normalizer & get_normalizer() { normalizer & get_normalizer() {
@ -329,11 +324,17 @@ public:
type_checker::type_checker(ro_environment const & env):m_ptr(new imp(env)) {} type_checker::type_checker(ro_environment const & env):m_ptr(new imp(env)) {}
type_checker::~type_checker() {} type_checker::~type_checker() {}
expr type_checker::infer_type(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> * uc) { expr type_checker::infer_type(expr const & e, context const & ctx, optional<metavar_env> const & menv, buffer<unification_constraint> * uc) {
return m_ptr->infer_type(e, ctx, menv, uc); return m_ptr->infer_type(e, ctx, menv, uc);
} }
expr type_checker::infer_type(expr const & e, context const & ctx, metavar_env const & menv, buffer<unification_constraint> & uc) {
return m_ptr->infer_type(e, ctx, some_menv(menv), &uc);
}
expr type_checker::infer_type(expr const & e, context const & ctx, metavar_env const & menv) {
return m_ptr->infer_type(e, ctx, some_menv(menv), nullptr);
}
expr type_checker::infer_type(expr const & e, context const & ctx) { expr type_checker::infer_type(expr const & e, context const & ctx) {
return infer_type(e, ctx, nullptr, nullptr); return infer_type(e, ctx, none_menv(), nullptr);
} }
bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx) { bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx) {
return m_ptr->is_convertible(t1, t2, ctx); return m_ptr->is_convertible(t1, t2, ctx);

6
src/kernel/type_checker.h
View file

@ -30,11 +30,13 @@ public:
\remark This method throws an exception if \c e is not type correct. \remark This method throws an exception if \c e is not type correct.
\remark If \c menv is not nullptr, then \c e may contain metavariables. \remark If \c menv is not none, then \c e may contain metavariables.
New metavariables and unification constraints may be created by the type checker. New metavariables and unification constraints may be created by the type checker.
The new unification constraints are stored in \c new_constraints. The new unification constraints are stored in \c new_constraints.
*/ */
expr infer_type(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> * new_constraints); expr infer_type(expr const & e, context const & ctx, optional<metavar_env> const & menv, buffer<unification_constraint> * new_constraints);
expr infer_type(expr const & e, context const & ctx, metavar_env const & menv, buffer<unification_constraint> & new_constraints);
expr infer_type(expr const & e, context const & ctx, metavar_env const & menv);
/** /**
\brief Return the type of \c e in the context \c ctx. \brief Return the type of \c e in the context \c ctx.

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

@ -31,15 +31,26 @@ class elaborator::imp {
cnstr_queue m_queue; cnstr_queue m_queue;
state(metavar_env const & menv, unsigned num_cnstrs, unification_constraint const * cnstrs): state(metavar_env const & menv, unsigned num_cnstrs, unification_constraint const * cnstrs):
m_menv(menv) { m_menv(menv.copy()) {
for (unsigned i = 0; i < num_cnstrs; i++) for (unsigned i = 0; i < num_cnstrs; i++)
m_queue.push_back(cnstrs[i]); m_queue.push_back(cnstrs[i]);
} }
state(metavar_env const & menv, cnstr_queue const & q): state(metavar_env const & menv, cnstr_queue const & q):
m_menv(menv), m_menv(menv.copy()),
m_queue(q) { m_queue(q) {
} }
state(state const & other):
m_menv(other.m_menv.copy()),
m_queue(other.m_queue) {
}
state & operator=(state const & other) {
m_menv = other.m_menv.copy();
m_queue = other.m_queue;
return *this;
}
}; };
/** /**
@ -166,14 +177,14 @@ class elaborator::imp {
/** \brief Return true iff \c m is an assigned metavariable in the current state */ /** \brief Return true iff \c m is an assigned metavariable in the current state */
bool is_assigned(expr const & m) const { bool is_assigned(expr const & m) const {
lean_assert(is_metavar(m)); lean_assert(is_metavar(m));
return m_state.m_menv.is_assigned(m); return m_state.m_menv->is_assigned(m);
} }
/** \brief Return the substitution (and justification) for an assigned metavariable */ /** \brief Return the substitution (and justification) for an assigned metavariable */
std::pair<expr, justification> get_subst_jst(expr const & m) const { std::pair<expr, justification> get_subst_jst(expr const & m) const {
lean_assert(is_metavar(m)); lean_assert(is_metavar(m));
lean_assert(is_assigned(m)); lean_assert(is_assigned(m));
return *(m_state.m_menv.get_subst_jst(m)); return *(m_state.m_menv->get_subst_jst(m));
} }
/** /**
@ -181,7 +192,7 @@ class elaborator::imp {
The substitutions in the current state are taken into account. The substitutions in the current state are taken into account.
*/ */
bool has_metavar(expr const & e, expr const & m) const { bool has_metavar(expr const & e, expr const & m) const {
return ::lean::has_metavar(e, m, m_state.m_menv); return m_state.m_menv->has_metavar(e, m);
} }
static bool has_metavar(expr const & e) { static bool has_metavar(expr const & e) {
@ -193,7 +204,7 @@ class elaborator::imp {
the current state. the current state.
*/ */
bool has_assigned_metavar(expr const & e) const { bool has_assigned_metavar(expr const & e) const {
return ::lean::has_assigned_metavar(e, m_state.m_menv); return m_state.m_menv->has_assigned_metavar(e);
} }
/** \brief Return true if \c a is of the form <tt>(?m ...)</tt> */ /** \brief Return true if \c a is of the form <tt>(?m ...)</tt> */
@ -343,15 +354,15 @@ class elaborator::imp {
reset_quota(); reset_quota();
context const & ctx = get_context(c); context const & ctx = get_context(c);
justification jst(new assignment_justification(c)); justification jst(new assignment_justification(c));
metavar_env & menv = m_state.m_menv; metavar_env const & menv = m_state.m_menv;
m_state.m_menv.assign(m, v, jst); menv->assign(m, v, jst);
if (menv.has_type(m)) { if (menv->has_type(m)) {
buffer<unification_constraint> ucs; buffer<unification_constraint> ucs;
expr tv = m_type_inferer(v, ctx, &menv, &ucs); expr tv = m_type_inferer(v, ctx, menv, ucs);
for (auto c : ucs) for (auto c : ucs)
push_front(c); push_front(c);
justification new_jst(new typeof_mvar_justification(ctx, m, menv.get_type(m), tv, jst)); justification new_jst(new typeof_mvar_justification(ctx, m, menv->get_type(m), tv, jst));
push_front(mk_convertible_constraint(ctx, tv, menv.get_type(m), new_jst)); push_front(mk_convertible_constraint(ctx, tv, menv->get_type(m), new_jst));
} }
} }
@ -449,7 +460,7 @@ class elaborator::imp {
justification new_jst(new substitution_justification(c, s_j.second)); justification new_jst(new substitution_justification(c, s_j.second));
expr new_f = s_j.first; expr new_f = s_j.first;
expr new_a = update_app(a, 0, new_f); expr new_a = update_app(a, 0, new_f);
if (m_state.m_menv.beta_reduce_metavar_application()) if (m_state.m_menv->beta_reduce_metavar_application())
new_a = head_beta_reduce(new_a); new_a = head_beta_reduce(new_a);
push_updated_constraint(c, is_lhs, new_a, new_jst); push_updated_constraint(c, is_lhs, new_a, new_jst);
return Processed; return Processed;
@ -471,7 +482,7 @@ class elaborator::imp {
*/ */
expr instantiate_metavars(expr const & a, buffer<justification> & jsts) { expr instantiate_metavars(expr const & a, buffer<justification> & jsts) {
lean_assert(has_assigned_metavar(a)); lean_assert(has_assigned_metavar(a));
return ::lean::instantiate_metavars(a, m_state.m_menv, jsts); return m_state.m_menv->instantiate_metavars(a, jsts);
} }
/** /**
@ -733,7 +744,7 @@ class elaborator::imp {
buffer<unification_constraint> ucs; buffer<unification_constraint> ucs;
context h_ctx = ctx; // context for new fresh metavariables used in the imitation step context h_ctx = ctx; // context for new fresh metavariables used in the imitation step
for (unsigned i = 1; i < num_a; i++) { for (unsigned i = 1; i < num_a; i++) {
arg_types.push_back(m_type_inferer(arg(a, i), ctx, &menv, &ucs)); arg_types.push_back(m_type_inferer(arg(a, i), ctx, menv, ucs));
for (auto uc : ucs) for (auto uc : ucs)
push_front(uc); push_front(uc);
h_ctx = extend(h_ctx, name(g_x_name, i), arg_types.back()); h_ctx = extend(h_ctx, name(g_x_name, i), arg_types.back());
@ -767,7 +778,7 @@ class elaborator::imp {
imitation_args.push_back(lift_free_vars(f_b, 0, num_a - 1)); imitation_args.push_back(lift_free_vars(f_b, 0, num_a - 1));
for (unsigned i = 1; i < num_b; i++) { for (unsigned i = 1; i < num_b; i++) {
// Remark: h_ctx is "ctx, (x_{num_a} : T_{num_a}) ... (x_1 : T_1)" because h_i is inside of the lambda // Remark: h_ctx is "ctx, (x_{num_a} : T_{num_a}) ... (x_1 : T_1)" because h_i is inside of the lambda
expr h_i = new_state.m_menv.mk_metavar(h_ctx); expr h_i = new_state.m_menv->mk_metavar(h_ctx);
imitation_args.push_back(mk_app_vars(h_i, num_a - 1)); imitation_args.push_back(mk_app_vars(h_i, num_a - 1));
push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_i), arg(b, i), new_assumption); push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_i), arg(b, i), new_assumption);
} }
@ -777,8 +788,8 @@ class elaborator::imp {
// Assign f_a <- fun (x_1 : T_1) ... (x_{num_a} : T_{num_a}), (h_1 x_1 ... x_{num_a}) = (h_2 x_1 ... x_{num_a}) // Assign f_a <- fun (x_1 : T_1) ... (x_{num_a} : T_{num_a}), (h_1 x_1 ... x_{num_a}) = (h_2 x_1 ... x_{num_a})
// New constraints (h_1 a_1 ... a_{num_a}) == eq_lhs(b) // New constraints (h_1 a_1 ... a_{num_a}) == eq_lhs(b)
// (h_2 a_1 ... a_{num_a}) == eq_rhs(b) // (h_2 a_1 ... a_{num_a}) == eq_rhs(b)
expr h_1 = new_state.m_menv.mk_metavar(h_ctx); expr h_1 = new_state.m_menv->mk_metavar(h_ctx);
expr h_2 = new_state.m_menv.mk_metavar(h_ctx); expr h_2 = new_state.m_menv->mk_metavar(h_ctx);
push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_1), eq_lhs(b), new_assumption); push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_1), eq_lhs(b), new_assumption);
push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_2), eq_rhs(b), new_assumption); push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_2), eq_rhs(b), new_assumption);
imitation = mk_lambda(arg_types, mk_eq(mk_app_vars(h_1, num_a - 1), mk_app_vars(h_2, num_a - 1))); imitation = mk_lambda(arg_types, mk_eq(mk_app_vars(h_1, num_a - 1), mk_app_vars(h_2, num_a - 1)));
@ -788,9 +799,9 @@ class elaborator::imp {
// fun (x_b : (?h_1 x_1 ... x_{num_a})), (?h_2 x_1 ... x_{num_a} x_b) // fun (x_b : (?h_1 x_1 ... x_{num_a})), (?h_2 x_1 ... x_{num_a} x_b)
// New constraints (h_1 a_1 ... a_{num_a}) == abst_domain(b) // New constraints (h_1 a_1 ... a_{num_a}) == abst_domain(b)
// (h_2 a_1 ... a_{num_a} x_b) == abst_body(b) // (h_2 a_1 ... a_{num_a} x_b) == abst_body(b)
expr h_1 = new_state.m_menv.mk_metavar(h_ctx); expr h_1 = new_state.m_menv->mk_metavar(h_ctx);
context new_ctx = extend(ctx, abst_name(b), abst_domain(b)); context new_ctx = extend(ctx, abst_name(b), abst_domain(b));
expr h_2 = new_state.m_menv.mk_metavar(extend(h_ctx, abst_name(b), abst_domain(b))); expr h_2 = new_state.m_menv->mk_metavar(extend(h_ctx, abst_name(b), abst_domain(b)));
push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_1), abst_domain(b), new_assumption); push_new_eq_constraint(new_state.m_queue, ctx, update_app(a, 0, h_1), abst_domain(b), new_assumption);
push_new_eq_constraint(new_state.m_queue, new_ctx, push_new_eq_constraint(new_state.m_queue, new_ctx,
mk_app(update_app(a, 0, h_2), mk_var(0)), abst_body(b), new_assumption); mk_app(update_app(a, 0, h_2), mk_var(0)), abst_body(b), new_assumption);
@ -850,7 +861,7 @@ class elaborator::imp {
metavar_env & menv = m_state.m_menv; metavar_env & menv = m_state.m_menv;
buffer<unification_constraint> ucs; buffer<unification_constraint> ucs;
expr b_type = m_type_inferer(b, ctx, &menv, &ucs); expr b_type = m_type_inferer(b, ctx, menv, ucs);
for (auto uc : ucs) for (auto uc : ucs)
push_front(uc); push_front(uc);
context ctx_with_i = ctx.insert_at(i, g_x_name, b_type); // must add entry for variable #i in the context context ctx_with_i = ctx.insert_at(i, g_x_name, b_type); // must add entry for variable #i in the context
@ -883,7 +894,7 @@ class elaborator::imp {
buffer<expr> imitation_args; buffer<expr> imitation_args;
imitation_args.push_back(f_b); imitation_args.push_back(f_b);
for (unsigned j = 1; j < num_b; j++) { for (unsigned j = 1; j < num_b; j++) {
expr h_j = new_state.m_menv.mk_metavar(ctx); expr h_j = new_state.m_menv->mk_metavar(ctx);
imitation_args.push_back(h_j); imitation_args.push_back(h_j);
push_new_eq_constraint(new_state.m_queue, ctx, h_j, lift_free_vars(arg(b, j), i, 1), new_assumption); push_new_eq_constraint(new_state.m_queue, ctx, h_j, lift_free_vars(arg(b, j), i, 1), new_assumption);
} }
@ -891,8 +902,8 @@ class elaborator::imp {
} else if (is_eq(b)) { } else if (is_eq(b)) {
// Imitation for equality b == Eq(s1, s2) // Imitation for equality b == Eq(s1, s2)
// mname <- Eq(?h_1, ?h_2) // mname <- Eq(?h_1, ?h_2)
expr h_1 = new_state.m_menv.mk_metavar(ctx); expr h_1 = new_state.m_menv->mk_metavar(ctx);
expr h_2 = new_state.m_menv.mk_metavar(ctx); expr h_2 = new_state.m_menv->mk_metavar(ctx);
imitation = mk_eq(h_1, h_2); imitation = mk_eq(h_1, h_2);
push_new_eq_constraint(new_state.m_queue, ctx, h_1, lift_free_vars(eq_lhs(b), i, 1), new_assumption); push_new_eq_constraint(new_state.m_queue, ctx, h_1, lift_free_vars(eq_lhs(b), i, 1), new_assumption);
push_new_eq_constraint(new_state.m_queue, ctx, h_2, lift_free_vars(eq_rhs(b), i, 1), new_assumption); push_new_eq_constraint(new_state.m_queue, ctx, h_2, lift_free_vars(eq_rhs(b), i, 1), new_assumption);
@ -900,10 +911,10 @@ class elaborator::imp {
// Lambdas and Pis // Lambdas and Pis
// Imitation for Lambdas and Pis, b == Fun(x:T) B // Imitation for Lambdas and Pis, b == Fun(x:T) B
// mname <- Fun (x:?h_1) ?h_2 // mname <- Fun (x:?h_1) ?h_2
expr h_1 = new_state.m_menv.mk_metavar(ctx); expr h_1 = new_state.m_menv->mk_metavar(ctx);
push_new_eq_constraint(new_state.m_queue, ctx, h_1, lift_free_vars(abst_domain(b), i, 1), new_assumption); push_new_eq_constraint(new_state.m_queue, ctx, h_1, lift_free_vars(abst_domain(b), i, 1), new_assumption);
context new_ctx = extend(ctx, abst_name(b), abst_domain(b)); context new_ctx = extend(ctx, abst_name(b), abst_domain(b));
expr h_2 = new_state.m_menv.mk_metavar(new_ctx); expr h_2 = new_state.m_menv->mk_metavar(new_ctx);
imitation = update_abstraction(b, h_1, h_2); imitation = update_abstraction(b, h_1, h_2);
push_new_eq_constraint(new_state.m_queue, new_ctx, h_2, lift_free_vars(abst_body(b), i+1, 1), new_assumption); push_new_eq_constraint(new_state.m_queue, new_ctx, h_2, lift_free_vars(abst_body(b), i+1, 1), new_assumption);
} else { } else {
@ -933,9 +944,9 @@ class elaborator::imp {
// a <- (fun x : ?h1, ?h2) or (Pi x : ?h1, ?h2) // a <- (fun x : ?h1, ?h2) or (Pi x : ?h1, ?h2)
// ?h1 is in the same context where 'a' was defined // ?h1 is in the same context where 'a' was defined
// ?h2 is in the context of 'a' + domain of b // ?h2 is in the context of 'a' + domain of b
context ctx_a = m_state.m_menv.get_context(metavar_name(a)); context ctx_a = m_state.m_menv->get_context(metavar_name(a));
expr h_1 = m_state.m_menv.mk_metavar(ctx_a); expr h_1 = m_state.m_menv->mk_metavar(ctx_a);
expr h_2 = m_state.m_menv.mk_metavar(extend(ctx_a, abst_name(b), abst_domain(b))); expr h_2 = m_state.m_menv->mk_metavar(extend(ctx_a, abst_name(b), abst_domain(b)));
expr imitation = update_abstraction(b, h_1, h_2); expr imitation = update_abstraction(b, h_1, h_2);
expr ma = mk_metavar(metavar_name(a)); expr ma = mk_metavar(metavar_name(a));
justification new_jst(new imitation_justification(c)); justification new_jst(new imitation_justification(c));
@ -1441,7 +1452,7 @@ public:
} }
void display(std::ostream & out) const { void display(std::ostream & out) const {
m_state.m_menv.for_each_subst([&](name const & m, expr const & e) { m_state.m_menv->for_each_subst([&](name const & m, expr const & e) {
out << m << " <- " << e << "\n"; out << m << " <- " << e << "\n";
}); });
for (auto c : m_state.m_queue) for (auto c : m_state.m_queue)

46
src/library/kernel_bindings.cpp
View file

@ -1462,11 +1462,11 @@ DECL_UDATA(metavar_env)
static int menv_mk_metavar(lua_State * L) { static int menv_mk_metavar(lua_State * L) {
int nargs = lua_gettop(L); int nargs = lua_gettop(L);
if (nargs == 1) { if (nargs == 1) {
return push_expr(L, to_metavar_env(L, 1).mk_metavar()); return push_expr(L, to_metavar_env(L, 1)->mk_metavar());
} else if (nargs == 2) { } else if (nargs == 2) {
return push_expr(L, to_metavar_env(L, 1).mk_metavar(to_context(L, 2))); return push_expr(L, to_metavar_env(L, 1)->mk_metavar(to_context(L, 2)));
} else { } else {
return push_expr(L, to_metavar_env(L, 1).mk_metavar(to_context(L, 2), some_expr(to_expr(L, 3)))); return push_expr(L, to_metavar_env(L, 1)->mk_metavar(to_context(L, 2), some_expr(to_expr(L, 3))));
} }
} }
@ -1481,37 +1481,37 @@ static expr & to_metavar(lua_State * L, int i, bool lctx = true) {
} }
static int menv_get_timestamp(lua_State * L) { static int menv_get_timestamp(lua_State * L) {
lua_pushinteger(L, to_metavar_env(L, 1).get_timestamp()); lua_pushinteger(L, to_metavar_env(L, 1)->get_timestamp());
return 1; return 1;
} }
static int menv_get_context(lua_State * L) { static int menv_get_context(lua_State * L) {
if (is_expr(L, 2)) if (is_expr(L, 2))
return push_context(L, to_metavar_env(L, 1).get_context(to_metavar(L, 2, false))); return push_context(L, to_metavar_env(L, 1)->get_context(to_metavar(L, 2, false)));
else else
return push_context(L, to_metavar_env(L, 1).get_context(to_name_ext(L, 2))); return push_context(L, to_metavar_env(L, 1)->get_context(to_name_ext(L, 2)));
} }
static int menv_has_type(lua_State * L) { static int menv_has_type(lua_State * L) {
if (is_expr(L, 2)) if (is_expr(L, 2))
lua_pushboolean(L, to_metavar_env(L, 1).has_type(to_metavar(L, 2))); lua_pushboolean(L, to_metavar_env(L, 1)->has_type(to_metavar(L, 2)));
else else
lua_pushboolean(L, to_metavar_env(L, 1).has_type(to_name_ext(L, 2))); lua_pushboolean(L, to_metavar_env(L, 1)->has_type(to_name_ext(L, 2)));
return 1; return 1;
} }
static int menv_get_type(lua_State * L) { static int menv_get_type(lua_State * L) {
if (is_expr(L, 2)) if (is_expr(L, 2))
return push_expr(L, to_metavar_env(L, 1).get_type(to_metavar(L, 2))); return push_expr(L, to_metavar_env(L, 1)->get_type(to_metavar(L, 2)));
else else
return push_expr(L, to_metavar_env(L, 1).get_type(to_name_ext(L, 2))); return push_expr(L, to_metavar_env(L, 1)->get_type(to_name_ext(L, 2)));
} }
static int menv_is_assigned(lua_State * L) { static int menv_is_assigned(lua_State * L) {
if (is_expr(L, 2)) if (is_expr(L, 2))
lua_pushboolean(L, to_metavar_env(L, 1).is_assigned(to_metavar(L, 2))); lua_pushboolean(L, to_metavar_env(L, 1)->is_assigned(to_metavar(L, 2)));
else else
lua_pushboolean(L, to_metavar_env(L, 1).is_assigned(to_name_ext(L, 2))); lua_pushboolean(L, to_metavar_env(L, 1)->is_assigned(to_name_ext(L, 2)));
return 1; return 1;
} }
@ -1521,32 +1521,32 @@ static int menv_assign(lua_State * L) {
if (nargs == 4) if (nargs == 4)
jst = to_justification(L, 4); jst = to_justification(L, 4);
if (is_expr(L, 2)) if (is_expr(L, 2))
to_metavar_env(L, 1).assign(to_metavar(L, 2, false), to_expr(L, 3), jst); to_metavar_env(L, 1)->assign(to_metavar(L, 2, false), to_expr(L, 3), jst);
else else
to_metavar_env(L, 1).assign(to_name_ext(L, 2), to_expr(L, 3), jst); to_metavar_env(L, 1)->assign(to_name_ext(L, 2), to_expr(L, 3), jst);
return 0; return 0;
} }
static int menv_get_subst(lua_State * L) { static int menv_get_subst(lua_State * L) {
if (is_expr(L, 2)) if (is_expr(L, 2))
return push_optional_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 else
return push_optional_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) { static int menv_get_justification(lua_State * L) {
if (is_expr(L, 2)) if (is_expr(L, 2))
return push_optional_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 else
return push_optional_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) { static int menv_get_subst_jst(lua_State * L) {
optional<std::pair<expr, justification>> r; optional<std::pair<expr, justification>> r;
if (is_expr(L, 2)) { if (is_expr(L, 2)) {
r = to_metavar_env(L, 1).get_subst_jst(to_metavar(L, 2)); r = to_metavar_env(L, 1)->get_subst_jst(to_metavar(L, 2));
} else { } else {
r = to_metavar_env(L, 1).get_subst_jst(to_name_ext(L, 2)); r = to_metavar_env(L, 1)->get_subst_jst(to_name_ext(L, 2));
} }
if (r) { if (r) {
push_expr(L, r->first); push_expr(L, r->first);
@ -1559,7 +1559,7 @@ static int menv_get_subst_jst(lua_State * L) {
static int menv_for_each_subst(lua_State * L) { static int menv_for_each_subst(lua_State * L) {
luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun
to_metavar_env(L, 1).for_each_subst([&](name const & n, expr const & e) { to_metavar_env(L, 1)->for_each_subst([&](name const & n, expr const & e) {
lua_pushvalue(L, 2); // push user-fun lua_pushvalue(L, 2); // push user-fun
push_name(L, n); push_name(L, n);
push_expr(L, e); push_expr(L, e);
@ -1576,11 +1576,11 @@ static int mk_metavar_env(lua_State * L) {
} }
static int menv_copy(lua_State * L) { static int menv_copy(lua_State * L) {
return push_metavar_env(L, metavar_env(to_metavar_env(L, 1))); return push_metavar_env(L, metavar_env(to_metavar_env(L, 1).copy()));
} }
static int instantiate_metavars(lua_State * L) { static int instantiate_metavars(lua_State * L) {
return push_expr(L, instantiate_metavars(to_expr(L, 1), to_metavar_env(L, 2))); return push_expr(L, to_metavar_env(L, 2)->instantiate_metavars(to_expr(L, 1)));
} }
static const struct luaL_Reg metavar_env_m[] = { static const struct luaL_Reg metavar_env_m[] = {

10
src/library/placeholder.cpp
View file

@ -26,12 +26,12 @@ bool has_placeholder(expr const & e) {
} }
class replace_placeholders_with_metavars_proc : public replace_visitor { class replace_placeholders_with_metavars_proc : public replace_visitor {
metavar_env & m_menv; metavar_env const & m_menv;
expr_map<expr> * m_new2old; expr_map<expr> * m_new2old;
protected: protected:
expr visit_constant(expr const & e, context const & c) { expr visit_constant(expr const & e, context const & c) {
if (is_placeholder(e)) { if (is_placeholder(e)) {
return m_menv.mk_metavar(c, const_type(e)); return m_menv->mk_metavar(c, const_type(e));
} else { } else {
return e; return e;
} }
@ -44,13 +44,13 @@ protected:
return r; return r;
} }
public: public:
replace_placeholders_with_metavars_proc(metavar_env & menv, expr_map<expr> * new2old): replace_placeholders_with_metavars_proc(metavar_env const & menv, expr_map<expr> * new2old):
m_menv(menv), m_menv(menv),
m_new2old(new2old) { m_new2old(new2old) {
} }
}; };
expr replace_placeholders_with_metavars(expr const & e, metavar_env & menv, expr_map<expr> * new2old) { expr replace_placeholders_with_metavars(expr const & e, metavar_env const & menv, expr_map<expr> * new2old) {
replace_placeholders_with_metavars_proc proc(menv, new2old); replace_placeholders_with_metavars_proc proc(menv, new2old);
return proc(e); return proc(e);
} }

2
src/library/placeholder.h
View file

@ -32,5 +32,5 @@ bool has_placeholder(expr const & e);
if \c new2old is not nullptr, then for each new expression \c t created based on if \c new2old is not nullptr, then for each new expression \c t created based on
\c s, we store <tt>(*new2old)[t] = s</tt>. \c s, we store <tt>(*new2old)[t] = s</tt>.
*/ */
expr replace_placeholders_with_metavars(expr const & e, metavar_env & menv, expr_map<expr> * new2old = nullptr); expr replace_placeholders_with_metavars(expr const & e, metavar_env const & menv, expr_map<expr> * new2old = nullptr);
} }

4
src/library/substitution.cpp
View file

@ -23,7 +23,7 @@ expr find(substitution & s, expr e) {
} }
} }
expr apply(substitution & s, expr const & e) { expr apply(substitution & s, expr const & e, optional<metavar_env> const & menv) {
auto f = [&](expr const & e, unsigned) -> expr { auto f = [&](expr const & e, unsigned) -> expr {
if (is_metavar(e)) { if (is_metavar(e)) {
expr r = find(s, e); expr r = find(s, e);
@ -32,7 +32,7 @@ expr apply(substitution & s, expr const & e) {
r = apply(s, r); r = apply(s, r);
s.insert(metavar_name(e), r); s.insert(metavar_name(e), r);
} }
return apply_local_context(r, metavar_lctx(e)); return apply_local_context(r, metavar_lctx(e), menv);
} else { } else {
return e; return e;
} }

5
src/library/substitution.h
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include "util/splay_map.h" #include "util/splay_map.h"
#include "util/name.h" #include "util/name.h"
#include "kernel/expr.h" #include "kernel/expr.h"
#include "kernel/metavar.h"
namespace lean { namespace lean {
/** /**
@ -19,7 +20,9 @@ typedef splay_map<name, expr, name_quick_cmp> substitution;
/** /**
\brief Apply substitution \c s to \c e \brief Apply substitution \c s to \c e
*/ */
expr apply(substitution & s, expr const & e); expr apply(substitution & s, expr const & e, optional<metavar_env> const & menv = none_menv());
inline expr apply(substitution & s, expr const & e, metavar_env const & menv) { return apply(s, e, some_menv(menv)); }
expr find(substitution & s, expr e); expr find(substitution & s, expr e);
UDATA_DEFS_CORE(substitution) UDATA_DEFS_CORE(substitution)
void open_substitution(lua_State * L); void open_substitution(lua_State * L);

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

@ -49,7 +49,7 @@ static optional<proof_state> apply_tactic(ro_environment const & env, proof_stat
// We store the solved goals using a list of pairs // We store the solved goals using a list of pairs
// name, args. Where the 'name' is the name of the solved goal. // name, args. Where the 'name' is the name of the solved goal.
type_inferer inferer(env); type_inferer inferer(env);
metavar_env new_menv = s.get_menv(); metavar_env new_menv = s.get_menv().copy();
list<std::pair<name, arg_list>> proof_info; list<std::pair<name, arg_list>> proof_info;
for (auto const & p : s.get_goals()) { for (auto const & p : s.get_goals()) {
check_interrupted(); check_interrupted();
@ -69,7 +69,7 @@ static optional<proof_state> apply_tactic(ro_environment const & env, proof_stat
l = cons(mk_pair(some_expr(mvar_sol), name()), l); l = cons(mk_pair(some_expr(mvar_sol), name()), l);
th_type_c = instantiate(abst_body(th_type_c), mvar_sol); th_type_c = instantiate(abst_body(th_type_c), mvar_sol);
} else { } else {
if (inferer.is_proposition(abst_domain(th_type_c), context(), &new_menv)) { if (inferer.is_proposition(abst_domain(th_type_c), context(), new_menv)) {
name new_gname(gname, new_goal_idx); name new_gname(gname, new_goal_idx);
new_goal_idx++; new_goal_idx++;
l = cons(mk_pair(none_expr(), new_gname), l); l = cons(mk_pair(none_expr(), new_gname), l);
@ -79,7 +79,7 @@ static optional<proof_state> apply_tactic(ro_environment const & env, proof_stat
// we have to create a new metavar in menv // we have to create a new metavar in menv
// since we do not have a substitution for mvar, and // since we do not have a substitution for mvar, and
// it is not a proposition // it is not a proposition
expr new_m = new_menv.mk_metavar(context(), some_expr(abst_domain(th_type_c))); expr new_m = new_menv->mk_metavar(context(), some_expr(abst_domain(th_type_c)));
l = cons(mk_pair(some_expr(new_m), name()), l); l = cons(mk_pair(some_expr(new_m), name()), l);
// we use instantiate_with_closed_relaxed because we do not want // we use instantiate_with_closed_relaxed because we do not want
// to introduce a lift operator in the new_m // to introduce a lift operator in the new_m

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

@ -15,6 +15,6 @@ class assignment {
metavar_env m_menv; metavar_env m_menv;
public: public:
assignment(metavar_env const & menv):m_menv(menv) {} assignment(metavar_env const & menv):m_menv(menv) {}
optional<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); }
}; };
} }

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

@ -240,7 +240,8 @@ static int proof_state_get_goals(lua_State * L) {
} }
static int proof_state_get_menv(lua_State * L) { static int proof_state_get_menv(lua_State * L) {
return push_metavar_env(L, to_proof_state(L, 1).get_menv()); // Remark: I use copy to make sure Lua code cannot change the metavar_env in the proof_state
return push_metavar_env(L, to_proof_state(L, 1).get_menv().copy());
} }
static int proof_state_get_proof_builder(lua_State * L) { static int proof_state_get_proof_builder(lua_State * L) {

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

@ -42,14 +42,14 @@ class proof_state {
MK_LEAN_RC(); MK_LEAN_RC();
precision m_precision; precision m_precision;
goals m_goals; goals m_goals;
metavar_env m_menv; ro_metavar_env m_menv;
proof_builder m_proof_builder; proof_builder m_proof_builder;
cex_builder m_cex_builder; cex_builder m_cex_builder;
void dealloc() { delete this; } void dealloc() { delete this; }
cell():m_rc(1) {} cell():m_rc(1) {}
cell(precision prec, goals const & gs, metavar_env const & menv, proof_builder const & p, cex_builder const & c): cell(precision prec, goals const & gs, ro_metavar_env const & menv, proof_builder const & p, cex_builder const & c):
m_rc(1), m_precision(prec), m_goals(gs), m_menv(menv), m_proof_builder(p), m_cex_builder(c) {} m_rc(1), m_precision(prec), m_goals(gs), m_menv(menv), m_proof_builder(p), m_cex_builder(c) {}
cell(goals const & gs, metavar_env const & menv, proof_builder const & p, cex_builder const & c): cell(goals const & gs, ro_metavar_env const & menv, proof_builder const & p, cex_builder const & c):
m_rc(1), m_precision(precision::Precise), m_goals(gs), m_menv(menv), m_proof_builder(p), m_cex_builder(c) {} m_rc(1), m_precision(precision::Precise), m_goals(gs), m_menv(menv), m_proof_builder(p), m_cex_builder(c) {}
}; };
cell * m_ptr; cell * m_ptr;
@ -57,23 +57,23 @@ public:
proof_state():m_ptr(new cell()) {} proof_state():m_ptr(new cell()) {}
proof_state(proof_state const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } proof_state(proof_state const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
proof_state(proof_state && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } proof_state(proof_state && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
proof_state(goals const & gs, metavar_env const & menv, proof_builder const & p, cex_builder const & c): proof_state(goals const & gs, ro_metavar_env const & menv, proof_builder const & p, cex_builder const & c):
m_ptr(new cell(gs, menv, p, c)) {} m_ptr(new cell(gs, menv, p, c)) {}
proof_state(precision prec, goals const & gs, metavar_env const & menv, proof_builder const & p, cex_builder const & c): proof_state(precision prec, goals const & gs, ro_metavar_env const & menv, proof_builder const & p, cex_builder const & c):
m_ptr(new cell(prec, gs, menv, p, c)) {} m_ptr(new cell(prec, gs, menv, p, c)) {}
proof_state(proof_state const & s, goals const & gs, proof_builder const & p): proof_state(proof_state const & s, goals const & gs, proof_builder const & p):
m_ptr(new cell(s.get_precision(), gs, s.get_menv(), p, s.get_cex_builder())) {} m_ptr(new cell(s.get_precision(), gs, s.m_ptr->m_menv, p, s.get_cex_builder())) {}
proof_state(proof_state const & s, goals const & gs): proof_state(proof_state const & s, goals const & gs):
m_ptr(new cell(s.get_precision(), gs, s.get_menv(), s.get_proof_builder(), s.get_cex_builder())) {} m_ptr(new cell(s.get_precision(), gs, s.m_ptr->m_menv, s.get_proof_builder(), s.get_cex_builder())) {}
proof_state(proof_state const & s, goals const & gs, proof_builder const & p, cex_builder const & c): proof_state(proof_state const & s, goals const & gs, proof_builder const & p, cex_builder const & c):
m_ptr(new cell(s.get_precision(), gs, s.get_menv(), p, c)) {} m_ptr(new cell(s.get_precision(), gs, s.m_ptr->m_menv, p, c)) {}
~proof_state() { if (m_ptr) m_ptr->dec_ref(); } ~proof_state() { if (m_ptr) m_ptr->dec_ref(); }
friend void swap(proof_state & a, proof_state & b) { std::swap(a.m_ptr, b.m_ptr); } friend void swap(proof_state & a, proof_state & b) { std::swap(a.m_ptr, b.m_ptr); }
proof_state & operator=(proof_state const & s) { LEAN_COPY_REF(s); } proof_state & operator=(proof_state const & s) { LEAN_COPY_REF(s); }
proof_state & operator=(proof_state && s) { LEAN_MOVE_REF(s); } proof_state & operator=(proof_state && s) { LEAN_MOVE_REF(s); }
precision get_precision() const { lean_assert(m_ptr); return m_ptr->m_precision; } precision get_precision() const { lean_assert(m_ptr); return m_ptr->m_precision; }
goals const & get_goals() const { lean_assert(m_ptr); return m_ptr->m_goals; } goals const & get_goals() const { lean_assert(m_ptr); return m_ptr->m_goals; }
metavar_env const & get_menv() const { lean_assert(m_ptr); return m_ptr->m_menv; } ro_metavar_env const & get_menv() const { lean_assert(m_ptr); return m_ptr->m_menv; }
proof_builder const & get_proof_builder() const { lean_assert(m_ptr); return m_ptr->m_proof_builder; } proof_builder const & get_proof_builder() const { lean_assert(m_ptr); return m_ptr->m_proof_builder; }
cex_builder const & get_cex_builder() const { lean_assert(m_ptr); return m_ptr->m_cex_builder; } cex_builder const & get_cex_builder() const { lean_assert(m_ptr); return m_ptr->m_cex_builder; }
/** /**

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

@ -74,7 +74,7 @@ tactic & tactic::operator=(tactic && s) {
optional<expr> to_proof(proof_state const & s) { optional<expr> to_proof(proof_state const & s) {
if (s.is_proof_final_state()) { if (s.is_proof_final_state()) {
try { try {
assignment a(s.get_menv()); assignment a(s.get_menv().copy());
proof_map m; proof_map m;
return some_expr(s.get_proof_builder()(m, a)); return some_expr(s.get_proof_builder()(m, a));
} catch (...) { } catch (...) {
@ -88,7 +88,7 @@ optional<expr> to_proof(proof_state const & s) {
*/ */
optional<counterexample> to_counterexample(proof_state const & s) { optional<counterexample> to_counterexample(proof_state const & s) {
if (s.is_cex_final_state()) { if (s.is_cex_final_state()) {
assignment a(s.get_menv()); assignment a(s.get_menv().copy());
name goal_name(head(s.get_goals()).first); name goal_name(head(s.get_goals()).first);
try { try {
return some(s.get_cex_builder()(goal_name, optional<counterexample>(), a)); return some(s.get_cex_builder()(goal_name, optional<counterexample>(), a));

56
src/library/type_inferer.cpp
View file

@ -26,8 +26,7 @@ class type_inferer::imp {
ro_environment m_env; ro_environment m_env;
context m_ctx; context m_ctx;
metavar_env * m_menv; cached_metavar_env m_menv;
unsigned m_menv_timestamp;
unification_constraints * m_uc; unification_constraints * m_uc;
normalizer m_normalizer; normalizer m_normalizer;
cache m_cache; cache m_cache;
@ -84,20 +83,6 @@ class type_inferer::imp {
return instantiate(t, num_args(e)-1, &arg(e, 1)); return instantiate(t, num_args(e)-1, &arg(e, 1));
} }
void set_menv(metavar_env * menv) {
if (m_menv == menv) {
// Check whether m_menv has been updated since the last time the checker has been invoked
if (m_menv && m_menv->get_timestamp() > m_menv_timestamp) {
m_menv_timestamp = m_menv->get_timestamp();
m_cache.clear();
}
} else {
m_menv = menv;
m_cache.clear();
m_menv_timestamp = m_menv ? m_menv->get_timestamp() : 0;
}
}
expr infer_type(expr const & e, context const & ctx) { expr infer_type(expr const & e, context const & ctx) {
// cheap cases, we do not cache results // cheap cases, we do not cache results
switch (e.kind()) { switch (e.kind()) {
@ -219,27 +204,29 @@ public:
imp(ro_environment const & env): imp(ro_environment const & env):
m_env(env), m_env(env),
m_normalizer(env) { m_normalizer(env) {
m_menv = nullptr; m_uc = nullptr;
m_menv_timestamp = 0;
m_uc = nullptr;
} }
expr operator()(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> * uc) { expr operator()(expr const & e, context const & ctx, optional<metavar_env> const & menv, buffer<unification_constraint> * uc) {
set_ctx(ctx); set_ctx(ctx);
set_menv(menv); if (m_menv.update(menv))
clear_cache();
flet<unification_constraints*> set(m_uc, uc); flet<unification_constraints*> set(m_uc, uc);
return infer_type(e, ctx); return infer_type(e, ctx);
} }
void clear() { void clear_cache() {
m_cache.clear(); m_cache.clear();
m_normalizer.clear(); m_normalizer.clear();
m_ctx = context();
m_menv = nullptr;
m_menv_timestamp = 0;
} }
bool is_proposition(expr const & e, context const & ctx, metavar_env * menv) { void clear() {
clear_cache();
m_menv.clear();
m_ctx = context();
}
bool is_proposition(expr const & e, context const & ctx, optional<metavar_env> const & menv) {
// Catch easy cases // Catch easy cases
switch (e.kind()) { switch (e.kind()) {
case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Type: return false; case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Type: return false;
@ -255,15 +242,24 @@ public:
}; };
type_inferer::type_inferer(ro_environment const & env):m_ptr(new imp(env)) {} type_inferer::type_inferer(ro_environment const & env):m_ptr(new imp(env)) {}
type_inferer::~type_inferer() {} type_inferer::~type_inferer() {}
expr type_inferer::operator()(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> * uc) { expr type_inferer::operator()(expr const & e, context const & ctx, optional<metavar_env> const & menv, buffer<unification_constraint> * uc) {
return m_ptr->operator()(e, ctx, menv, uc); return m_ptr->operator()(e, ctx, menv, uc);
} }
expr type_inferer::operator()(expr const & e, context const & ctx) { expr type_inferer::operator()(expr const & e, context const & ctx, metavar_env const & menv, buffer<unification_constraint> & uc) {
return operator()(e, ctx, nullptr, nullptr); return m_ptr->operator()(e, ctx, some_menv(menv), &uc);
} }
bool type_inferer::is_proposition(expr const & e, context const & ctx, metavar_env * menv) { expr type_inferer::operator()(expr const & e, context const & ctx) {
return operator()(e, ctx, none_menv(), nullptr);
}
bool type_inferer::is_proposition(expr const & e, context const & ctx, optional<metavar_env> const & menv) {
return m_ptr->is_proposition(e, ctx, menv); return m_ptr->is_proposition(e, ctx, menv);
} }
bool type_inferer::is_proposition(expr const & e, context const & ctx) {
return is_proposition(e, ctx, none_menv());
}
bool type_inferer::is_proposition(expr const & e, context const & ctx, metavar_env const & menv) {
return is_proposition(e, ctx, some_menv(menv));
}
void type_inferer::clear() { m_ptr->clear(); } void type_inferer::clear() { m_ptr->clear(); }
constexpr char const * type_inferer_mt = "type_inferer"; constexpr char const * type_inferer_mt = "type_inferer";

8
src/library/type_inferer.h
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#pragma once #pragma once
#include <memory> #include <memory>
#include "util/buffer.h" #include "util/buffer.h"
#include "util/optional.h"
#include "kernel/expr.h" #include "kernel/expr.h"
#include "kernel/context.h" #include "kernel/context.h"
#include "kernel/unification_constraint.h" #include "kernel/unification_constraint.h"
@ -31,9 +32,12 @@ public:
type_inferer(ro_environment const & env); type_inferer(ro_environment const & env);
~type_inferer(); ~type_inferer();
expr operator()(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> * uc); expr operator()(expr const & e, context const & ctx, optional<metavar_env> const & menv, buffer<unification_constraint> * uc);
expr operator()(expr const & e, context const & ctx, metavar_env const & menv, buffer<unification_constraint> & uc);
expr operator()(expr const & e, context const & ctx = context()); expr operator()(expr const & e, context const & ctx = context());
bool is_proposition(expr const & e, context const & ctx = context(), metavar_env * menv = nullptr); bool is_proposition(expr const & e, context const & ctx, optional<metavar_env> const & menv);
bool is_proposition(expr const & e, context const & ctx, metavar_env const & menv);
bool is_proposition(expr const & e, context const & ctx = context());
void clear(); void clear();
}; };

14
src/tests/kernel/free_vars.cpp
View file

@ -66,7 +66,7 @@ static void tst4() {
expr a = Const("a"); expr a = Const("a");
expr b = Const("b"); expr b = Const("b");
expr x = Const("x"); expr x = Const("x");
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
lean_assert(fn(m1) == 0); lean_assert(fn(m1) == 0);
lean_assert(fn(Var(0)) == 1); lean_assert(fn(Var(0)) == 1);
lean_assert(fn(Var(0)(Var(2), Var(1))) == 3); lean_assert(fn(Var(0)(Var(2), Var(1))) == 3);
@ -83,7 +83,7 @@ static void tst4() {
context ctx; context ctx;
ctx = extend(ctx, name("x"), Bool); ctx = extend(ctx, name("x"), Bool);
ctx = extend(ctx, name("y"), Bool); ctx = extend(ctx, name("y"), Bool);
expr m2 = menv.mk_metavar(ctx); expr m2 = menv->mk_metavar(ctx);
lean_assert_eq(fn(m2), 2); lean_assert_eq(fn(m2), 2);
lean_assert_eq(fn(add_lift(m2, 3, 5)), 2); lean_assert_eq(fn(add_lift(m2, 3, 5)), 2);
lean_assert_eq(fn(add_lift(m2, 2, 5)), 2); lean_assert_eq(fn(add_lift(m2, 2, 5)), 2);
@ -96,7 +96,7 @@ static void tst4() {
lean_assert_eq(fn(add_lift(add_inst(m2, 1, f(Var(2))), 2, 2)), 5); lean_assert_eq(fn(add_lift(add_inst(m2, 1, f(Var(2))), 2, 2)), 5);
ctx = extend(ctx, name("w"), Bool); ctx = extend(ctx, name("w"), Bool);
ctx = extend(ctx, name("z"), Bool); ctx = extend(ctx, name("z"), Bool);
expr m3 = menv.mk_metavar(ctx); expr m3 = menv->mk_metavar(ctx);
lean_assert_eq(fn(m3), 4); lean_assert_eq(fn(m3), 4);
lean_assert_eq(fn(add_lift(add_inst(m3, 1, f(Var(0))), 1, 1)), 4); lean_assert_eq(fn(add_lift(add_inst(m3, 1, f(Var(0))), 1, 1)), 4);
lean_assert_eq(fn(add_lift(add_inst(m3, 1, f(Var(3))), 1, 1)), 5); lean_assert_eq(fn(add_lift(add_inst(m3, 1, f(Var(3))), 1, 1)), 5);
@ -108,7 +108,7 @@ static void tst4() {
static void tst5() { static void tst5() {
metavar_env menv; metavar_env menv;
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr f = Const("f"); expr f = Const("f");
expr a = Const("a"); expr a = Const("a");
expr b = Const("b"); expr b = Const("b");
@ -119,7 +119,7 @@ static void tst5() {
lean_assert(!has_free_var(m1, 0, menv)); lean_assert(!has_free_var(m1, 0, menv));
lean_assert(!has_free_var(m1, 1, menv)); lean_assert(!has_free_var(m1, 1, menv));
context ctx({{"x", Bool}, {"y", Bool}}); context ctx({{"x", Bool}, {"y", Bool}});
expr m2 = menv.mk_metavar(ctx); expr m2 = menv->mk_metavar(ctx);
lean_assert(has_free_var(m2, 0, menv)); lean_assert(has_free_var(m2, 0, menv));
lean_assert(has_free_var(m2, 1, menv)); lean_assert(has_free_var(m2, 1, menv));
lean_assert(!has_free_var(m2, 2, menv)); lean_assert(!has_free_var(m2, 2, menv));
@ -139,8 +139,8 @@ static void tst5() {
static void tst6() { static void tst6() {
metavar_env menv; metavar_env menv;
expr f = Const("f"); expr f = Const("f");
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(context({{"x", Bool}, {"y", Bool}})); expr m2 = menv->mk_metavar(context({{"x", Bool}, {"y", Bool}}));
lean_assert(lift_free_vars(m1, 0, 1, menv) == m1); lean_assert(lift_free_vars(m1, 0, 1, menv) == m1);
lean_assert(lift_free_vars(m2, 0, 1, menv) != m2); lean_assert(lift_free_vars(m2, 0, 1, menv) != m2);
lean_assert(lift_free_vars(m2, 0, 1, menv) == add_lift(m2, 0, 1)); lean_assert(lift_free_vars(m2, 0, 1, menv) == add_lift(m2, 0, 1));

10
src/tests/kernel/instantiate.cpp
View file

@ -50,8 +50,8 @@ static void tst3() {
expr f = Const("f"); expr f = Const("f");
expr a = Const("a"); expr a = Const("a");
expr T = Const("T"); expr T = Const("T");
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(context({{"x", T}, {"y", T}})); expr m2 = menv->mk_metavar(context({{"x", T}, {"y", T}}));
lean_assert_eq(instantiate(f(m1, Var(0)), 0, a, menv), f(m1, a)); lean_assert_eq(instantiate(f(m1, Var(0)), 0, a, menv), f(m1, a));
lean_assert_ne(instantiate(f(m1, Var(0)), 0, a, menv), instantiate(f(m1, Var(0)), 0, a)); lean_assert_ne(instantiate(f(m1, Var(0)), 0, a, menv), instantiate(f(m1, Var(0)), 0, a));
lean_assert_ne(instantiate(f(m2, Var(0)), 0, a, menv), f(m2, a)); lean_assert_ne(instantiate(f(m2, Var(0)), 0, a, menv), f(m2, a));
@ -67,7 +67,7 @@ static void tst3() {
Fun({x, T}, f(m1, f(Var(1)), Var(0)))); Fun({x, T}, f(m1, f(Var(1)), Var(0))));
lean_assert_eq(instantiate(Fun({x, T}, f(m2, Var(3), Var(0))), 1, f(Var(0)), menv), lean_assert_eq(instantiate(Fun({x, T}, f(m2, Var(3), Var(0))), 1, f(Var(0)), menv),
Fun({x, T}, f(m2, Var(2), Var(0)))); Fun({x, T}, f(m2, Var(2), Var(0))));
expr m3 = menv.mk_metavar(context({{"x", T}, {"y", T}, {"z", T}})); expr m3 = menv->mk_metavar(context({{"x", T}, {"y", T}, {"z", T}}));
lean_assert_eq(instantiate(Fun({x, T}, f(m3, Var(3), Var(0))), 1, f(Var(0)), menv), lean_assert_eq(instantiate(Fun({x, T}, f(m3, Var(3), Var(0))), 1, f(Var(0)), menv),
Fun({x, T}, f(add_inst(m3, 2, f(Var(1))), Var(2), Var(0)))); Fun({x, T}, f(add_inst(m3, 2, f(Var(1))), Var(2), Var(0))));
} }
@ -75,8 +75,8 @@ static void tst3() {
static void tst4() { static void tst4() {
metavar_env menv; metavar_env menv;
expr T = Const("T"); expr T = Const("T");
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(context({{"x", T}, {"y", T}})); expr m2 = menv->mk_metavar(context({{"x", T}, {"y", T}}));
expr f = Const("f"); expr f = Const("f");
expr g = Const("f"); expr g = Const("f");
expr x = Const("x"); expr x = Const("x");

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

@ -27,7 +27,7 @@ using namespace lean;
static std::ostream & operator<<(std::ostream & out, metavar_env const & menv) { static std::ostream & operator<<(std::ostream & out, metavar_env const & menv) {
bool first = true; bool first = true;
menv.for_each_subst([&](name const & n, expr const & v) { menv->for_each_subst([&](name const & n, expr const & v) {
if (first) first = false; else out << "\n"; if (first) first = false; else out << "\n";
out << "?" << n << " <- " << v; out << "?" << n << " <- " << v;
}); });
@ -44,25 +44,25 @@ static std::ostream & operator<<(std::ostream & out, buffer<unification_constrai
static void tst1() { static void tst1() {
metavar_env menv; metavar_env menv;
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
lean_assert(!menv.is_assigned(m1)); lean_assert(!menv->is_assigned(m1));
expr t1 = menv.get_type(m1); expr t1 = menv->get_type(m1);
lean_assert(is_metavar(t1)); lean_assert(is_metavar(t1));
lean_assert(is_eqp(menv.get_type(m1), t1)); lean_assert(is_eqp(menv->get_type(m1), t1));
lean_assert(is_eqp(menv.get_type(m1), t1)); lean_assert(is_eqp(menv->get_type(m1), t1));
lean_assert(!menv.is_assigned(m1)); lean_assert(!menv->is_assigned(m1));
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
lean_assert(!menv.is_assigned(m1)); lean_assert(!menv->is_assigned(m1));
expr t2 = menv.get_type(m2); expr t2 = menv->get_type(m2);
lean_assert(is_metavar(m2)); lean_assert(is_metavar(m2));
lean_assert(!is_eqp(t1, t2)); lean_assert(!is_eqp(t1, t2));
lean_assert(t1 != t2); lean_assert(t1 != t2);
expr f = Const("f"); expr f = Const("f");
expr a = Const("a"); expr a = Const("a");
menv.assign(m1, f(a)); menv->assign(m1, f(a));
lean_assert(menv.is_assigned(m1)); lean_assert(menv->is_assigned(m1));
lean_assert(!menv.is_assigned(m2)); 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() { static void tst2() {
@ -71,17 +71,17 @@ static void tst2() {
expr g = Const("g"); expr g = Const("g");
expr h = Const("h"); expr h = Const("h");
expr a = Const("a"); expr a = Const("a");
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
// move m1 to a different context, and store new metavariable + context in m11 // move m1 to a different context, and store new metavariable + context in m11
std::cout << "---------------------\n"; std::cout << "---------------------\n";
expr m11 = add_inst(m1, 0, f(a, m2)); expr m11 = add_inst(m1, 0, f(a, m2));
std::cout << m11 << "\n"; std::cout << m11 << "\n";
menv.assign(m1, f(Var(0))); menv->assign(m1, f(Var(0)));
std::cout << instantiate_metavars(m11, menv) << "\n"; std::cout << menv->instantiate_metavars(m11) << "\n";
menv.assign(m2, g(a, Var(1))); menv->assign(m2, g(a, Var(1)));
std::cout << instantiate_metavars(h(m11), menv) << "\n"; std::cout << menv->instantiate_metavars(h(m11)) << "\n";
lean_assert_eq(instantiate_metavars(h(m11), menv), h(f(f(a, g(a, Var(1)))))); lean_assert_eq(menv->instantiate_metavars(h(m11)), h(f(f(a, g(a, Var(1))))));
} }
static void tst3() { static void tst3() {
@ -92,15 +92,14 @@ static void tst3() {
expr a = Const("a"); expr a = Const("a");
expr x = Const("x"); expr x = Const("x");
expr T = Const("T"); expr T = Const("T");
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr F = Fun({x, T}, f(m1, x)); expr F = Fun({x, T}, f(m1, x));
menv.assign(m1, h(Var(0), Var(2))); menv->assign(m1, h(Var(0), Var(2)));
std::cout << instantiate(abst_body(F), g(a)) << "\n"; std::cout << instantiate(abst_body(F), g(a)) << "\n";
std::cout << instantiate_metavars(instantiate(abst_body(F), g(a)), menv) << "\n"; lean_assert(menv->instantiate_metavars(instantiate(abst_body(F), g(a))) == f(h(g(a), Var(1)), g(a)));
lean_assert(instantiate_metavars(instantiate(abst_body(F), g(a)), menv) == f(h(g(a), Var(1)), g(a))); std::cout << instantiate(menv->instantiate_metavars(abst_body(F)), g(a)) << "\n";
std::cout << instantiate(instantiate_metavars(abst_body(F), menv), g(a)) << "\n"; lean_assert(instantiate(menv->instantiate_metavars(abst_body(F)), g(a)) ==
lean_assert(instantiate(instantiate_metavars(abst_body(F), menv), g(a)) == menv->instantiate_metavars(instantiate(abst_body(F), g(a))));
instantiate_metavars(instantiate(abst_body(F), g(a)), menv));
} }
static void tst4() { static void tst4() {
@ -109,11 +108,11 @@ static void tst4() {
expr g = Const("g"); expr g = Const("g");
expr h = Const("h"); expr h = Const("h");
expr a = Const("a"); expr a = Const("a");
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr F = f(m1, Var(2)); expr F = f(m1, Var(2));
menv.assign(m1, h(Var(1))); menv->assign(m1, h(Var(1)));
std::cout << instantiate(F, {g(Var(0)), h(a)}) << "\n"; std::cout << instantiate(F, {g(Var(0)), h(a)}) << "\n";
std::cout << instantiate_metavars(instantiate(F, {g(Var(0)), h(a)}), menv) << "\n"; std::cout << menv->instantiate_metavars(instantiate(F, {g(Var(0)), h(a)})) << "\n";
} }
static void tst5() { static void tst5() {
@ -129,16 +128,16 @@ static void tst6() {
expr g = Const("g"); expr g = Const("g");
expr h = Const("h"); expr h = Const("h");
metavar_env menv; metavar_env menv;
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
expr t = f(Var(0), Fun({x, N}, f(Var(1), x, Fun({y, N}, f(Var(2), x, y))))); expr t = f(Var(0), Fun({x, N}, f(Var(1), x, Fun({y, N}, f(Var(2), x, y)))));
expr r = instantiate(t, g(m1, m2)); expr r = instantiate(t, g(m1, m2));
std::cout << r << std::endl; std::cout << r << std::endl;
menv.assign(m2, Var(2)); menv->assign(m2, Var(2));
r = instantiate_metavars(r, menv); r = menv->instantiate_metavars(r);
std::cout << r << std::endl; std::cout << r << std::endl;
menv.assign(m1, h(Var(3))); menv->assign(m1, h(Var(3)));
r = instantiate_metavars(r, menv); r = menv->instantiate_metavars(r);
std::cout << r << std::endl; std::cout << r << std::endl;
lean_assert(r == f(g(h(Var(3)), Var(2)), Fun({x, N}, f(g(h(Var(4)), Var(3)), x, Fun({y, N}, f(g(h(Var(5)), Var(4)), x, y)))))); lean_assert(r == f(g(h(Var(3)), Var(2)), Fun({x, N}, f(g(h(Var(4)), Var(3)), x, Fun({y, N}, f(g(h(Var(5)), Var(4)), x, y))))));
} }
@ -148,11 +147,11 @@ static void tst7() {
expr g = Const("g"); expr g = Const("g");
expr a = Const("a"); expr a = Const("a");
metavar_env menv; metavar_env menv;
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr t = f(m1, Var(0)); expr t = f(m1, Var(0));
expr r = instantiate(t, a); expr r = instantiate(t, a);
menv.assign(m1, g(Var(0))); menv->assign(m1, g(Var(0)));
r = instantiate_metavars(r, menv); r = menv->instantiate_metavars(r);
std::cout << r << std::endl; std::cout << r << std::endl;
lean_assert(r == f(g(a), a)); lean_assert(r == f(g(a), a));
} }
@ -162,11 +161,11 @@ static void tst8() {
expr g = Const("g"); expr g = Const("g");
expr a = Const("a"); expr a = Const("a");
metavar_env menv; metavar_env menv;
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr t = f(m1, Var(0), Var(2)); expr t = f(m1, Var(0), Var(2));
expr r = instantiate(t, a); expr r = instantiate(t, a);
menv.assign(m1, g(Var(0), Var(1))); menv->assign(m1, g(Var(0), Var(1)));
r = instantiate_metavars(r, menv); r = menv->instantiate_metavars(r);
std::cout << r << std::endl; std::cout << r << std::endl;
lean_assert(r == f(g(a, Var(0)), a, Var(1))); lean_assert(r == f(g(a, Var(0)), a, Var(1)));
} }
@ -176,14 +175,14 @@ static void tst9() {
expr g = Const("g"); expr g = Const("g");
expr a = Const("a"); expr a = Const("a");
metavar_env menv; metavar_env menv;
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr t = f(m1, Var(1), Var(2)); expr t = f(m1, Var(1), Var(2));
expr r = lift_free_vars(t, 1, 2); expr r = lift_free_vars(t, 1, 2);
std::cout << r << std::endl; std::cout << r << std::endl;
r = instantiate(r, a); r = instantiate(r, a);
std::cout << r << std::endl; std::cout << r << std::endl;
menv.assign(m1, g(Var(0), Var(1))); menv->assign(m1, g(Var(0), Var(1)));
r = instantiate_metavars(r, menv); r = menv->instantiate_metavars(r);
std::cout << r << std::endl; std::cout << r << std::endl;
lean_assert(r == f(g(a, Var(2)), Var(2), Var(3))); lean_assert(r == f(g(a, Var(2)), Var(2), Var(3)));
} }
@ -197,35 +196,35 @@ static void tst10() {
expr g = Const("g"); expr g = Const("g");
expr h = Const("h"); expr h = Const("h");
metavar_env menv; metavar_env menv;
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
expr t = f(Var(0), Fun({x, N}, f(Var(1), Var(2), x, Fun({y, N}, f(Var(2), x, y))))); expr t = f(Var(0), Fun({x, N}, f(Var(1), Var(2), x, Fun({y, N}, f(Var(2), x, y)))));
expr r = instantiate(t, g(m1)); expr r = instantiate(t, g(m1));
std::cout << r << std::endl; std::cout << r << std::endl;
r = instantiate(r, h(m2)); r = instantiate(r, h(m2));
std::cout << r << std::endl; std::cout << r << std::endl;
menv.assign(m1, f(Var(0))); menv->assign(m1, f(Var(0)));
menv.assign(m2, Var(2)); menv->assign(m2, Var(2));
r = instantiate_metavars(r, menv); r = menv->instantiate_metavars(r);
std::cout << r << std::endl; std::cout << r << std::endl;
lean_assert(r == f(g(f(h(Var(2)))), Fun({x, N}, f(g(f(h(Var(3)))), h(Var(3)), x, Fun({y, N}, f(g(f(h(Var(4)))), x, y)))))); lean_assert(r == f(g(f(h(Var(2)))), Fun({x, N}, f(g(f(h(Var(3)))), h(Var(3)), x, Fun({y, N}, f(g(f(h(Var(4)))), x, y))))));
} }
static void tst11() { static void tst11() {
metavar_env menv; metavar_env menv;
unsigned t1 = menv.get_timestamp(); unsigned t1 = menv->get_timestamp();
expr m = menv.mk_metavar(); expr m = menv->mk_metavar();
unsigned t2 = menv.get_timestamp(); unsigned t2 = menv->get_timestamp();
lean_assert(t2 > t1); lean_assert(t2 > t1);
lean_assert(!menv.is_assigned(m)); lean_assert(!menv->is_assigned(m));
lean_assert(menv.get_timestamp() == t2); lean_assert(menv->get_timestamp() == t2);
menv.assign(m, Const("a")); menv->assign(m, Const("a"));
lean_assert(menv.get_timestamp() > t2); lean_assert(menv->get_timestamp() > t2);
} }
static void tst12() { static void tst12() {
metavar_env menv; metavar_env menv;
expr m = menv.mk_metavar(); expr m = menv->mk_metavar();
expr f = Const("f"); expr f = Const("f");
std::cout << instantiate(f(m), {Var(0), Var(1)}) << "\n"; std::cout << instantiate(f(m), {Var(0), Var(1)}) << "\n";
std::cout << instantiate(f(m), {Var(1), Var(0)}) << "\n"; std::cout << instantiate(f(m), {Var(1), Var(0)}) << "\n";
@ -234,7 +233,7 @@ static void tst12() {
static void tst13() { static void tst13() {
environment env; environment env;
metavar_env menv; metavar_env menv;
expr m = menv.mk_metavar(); expr m = menv->mk_metavar();
env->add_var("N", Type()); env->add_var("N", Type());
expr N = Const("N"); expr N = Const("N");
env->add_var("f", N >> N); env->add_var("f", N >> N);
@ -245,17 +244,17 @@ static void tst13() {
expr F = Fun({x, N}, f(m))(a); expr F = Fun({x, N}, f(m))(a);
normalizer norm(env); normalizer norm(env);
std::cout << norm(F) << "\n"; std::cout << norm(F) << "\n";
menv.assign(m, Var(0)); menv->assign(m, Var(0));
std::cout << norm(instantiate_metavars(F, menv)) << "\n"; std::cout << norm(menv->instantiate_metavars(F)) << "\n";
lean_assert(norm(instantiate_metavars(F, menv)) == lean_assert(norm(menv->instantiate_metavars(F)) ==
instantiate_metavars(norm(F), menv)); menv->instantiate_metavars(norm(F)));
} }
static void tst14() { static void tst14() {
environment env; environment env;
metavar_env menv; metavar_env menv;
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
expr N = Const("N"); expr N = Const("N");
expr f = Const("f"); expr f = Const("f");
expr h = Const("h"); expr h = Const("h");
@ -266,17 +265,17 @@ static void tst14() {
env->add_var("h", Pi({N, Type()}, N >> (N >> N))); env->add_var("h", Pi({N, Type()}, N >> (N >> N)));
expr F1 = Fun({{N, Type()}, {a, N}, {f, N >> N}}, expr F1 = Fun({{N, Type()}, {a, N}, {f, N >> N}},
(Fun({{x, N}, {y, N}}, Eq(f(m1), y)))(a)); (Fun({{x, N}, {y, N}}, Eq(f(m1), y)))(a));
metavar_env menv2 = menv; metavar_env menv2 = menv.copy();
menv2.assign(m1, h(Var(4), Var(1), Var(3))); menv2->assign(m1, h(Var(4), Var(1), Var(3)));
normalizer norm(env); normalizer norm(env);
env->add_var("M", Type()); env->add_var("M", Type());
expr M = Const("M"); expr M = Const("M");
std::cout << norm(F1) << "\n"; std::cout << norm(F1) << "\n";
std::cout << instantiate_metavars(norm(F1), menv2) << "\n"; std::cout << menv2->instantiate_metavars(norm(F1)) << "\n";
std::cout << instantiate_metavars(F1, menv2) << "\n"; std::cout << menv2->instantiate_metavars(F1) << "\n";
std::cout << norm(instantiate_metavars(F1, menv2)) << "\n"; std::cout << norm(menv2->instantiate_metavars(F1)) << "\n";
lean_assert(instantiate_metavars(norm(F1), menv2) == lean_assert(menv2->instantiate_metavars(norm(F1)) ==
norm(instantiate_metavars(F1, menv2))); norm(menv2->instantiate_metavars(F1)));
expr F2 = (Fun({{N, Type()}, {f, N >> N}, {a, N}, {b, N}}, expr F2 = (Fun({{N, Type()}, {f, N >> N}, {a, N}, {b, N}},
(Fun({{x, N}, {y, N}}, Eq(f(m1), y)))(a, m2)))(M); (Fun({{x, N}, {y, N}}, Eq(f(m1), y)))(a, m2)))(M);
std::cout << norm(F2) << "\n"; std::cout << norm(F2) << "\n";
@ -289,7 +288,7 @@ static void tst15() {
environment env; environment env;
metavar_env menv; metavar_env menv;
normalizer norm(env); normalizer norm(env);
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr f = Const("f"); expr f = Const("f");
expr x = Const("x"); expr x = Const("x");
expr y = Const("y"); expr y = Const("y");
@ -298,12 +297,12 @@ static void tst15() {
env->add_var("N", Type()); env->add_var("N", Type());
env->add_var("f", Type() >> Type()); env->add_var("f", Type() >> Type());
expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, f(m1))(N, N)); expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, f(m1))(N, N));
menv.assign(m1, Var(2)); menv->assign(m1, Var(2));
std::cout << norm(F) << "\n"; std::cout << norm(F) << "\n";
std::cout << instantiate_metavars(norm(F), menv) << "\n"; std::cout << menv->instantiate_metavars(norm(F)) << "\n";
std::cout << norm(instantiate_metavars(F, menv)) << "\n"; std::cout << norm(menv->instantiate_metavars(F)) << "\n";
lean_assert(instantiate_metavars(norm(F), menv) == lean_assert(menv->instantiate_metavars(norm(F)) ==
norm(instantiate_metavars(F, menv))); norm(menv->instantiate_metavars(F)));
} }
static void tst16() { static void tst16() {
@ -312,7 +311,7 @@ static void tst16() {
normalizer norm(env); normalizer norm(env);
context ctx; context ctx;
ctx = extend(ctx, "w", Type()); ctx = extend(ctx, "w", Type());
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr f = Const("f"); expr f = Const("f");
expr x = Const("x"); expr x = Const("x");
expr y = Const("y"); expr y = Const("y");
@ -320,10 +319,10 @@ static void tst16() {
expr N = Const("N"); expr N = Const("N");
env->add_var("N", Type()); env->add_var("N", Type());
expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, m1)(N, N)); expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, m1)(N, N));
menv.assign(m1, Var(3)); menv->assign(m1, Var(3));
std::cout << norm(F, ctx) << "\n"; std::cout << norm(F, ctx) << "\n";
std::cout << instantiate_metavars(norm(F, ctx), menv) << "\n"; std::cout << menv->instantiate_metavars(norm(F, ctx)) << "\n";
std::cout << norm(instantiate_metavars(F, menv), ctx) << "\n"; std::cout << norm(menv->instantiate_metavars(F), ctx) << "\n";
} }
static void tst17() { static void tst17() {
@ -335,7 +334,7 @@ static void tst17() {
ctx = extend(ctx, "w2", Type()); ctx = extend(ctx, "w2", Type());
ctx = extend(ctx, "w3", Type()); ctx = extend(ctx, "w3", Type());
ctx = extend(ctx, "w4", Type()); ctx = extend(ctx, "w4", Type());
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr f = Const("f"); expr f = Const("f");
expr x = Const("x"); expr x = Const("x");
expr y = Const("y"); expr y = Const("y");
@ -343,21 +342,21 @@ static void tst17() {
expr N = Const("N"); expr N = Const("N");
env->add_var("N", Type()); env->add_var("N", Type());
expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, m1)(N, N)); expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, m1)(N, N));
metavar_env menv2 = menv; metavar_env menv2 = menv.copy();
menv.assign(m1, Var(3)); menv->assign(m1, Var(3));
std::cout << norm(F, ctx) << "\n"; std::cout << norm(F, ctx) << "\n";
std::cout << instantiate_metavars(norm(F, ctx), menv) << "\n"; std::cout << menv->instantiate_metavars(norm(F, ctx)) << "\n";
std::cout << norm(instantiate_metavars(F, menv), ctx) << "\n"; std::cout << norm(menv->instantiate_metavars(F), ctx) << "\n";
F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}, {x, Type()}, {y, Type()}, {x, Type()}}, m1)(N, N, N, N, N)); F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}, {x, Type()}, {y, Type()}, {x, Type()}}, m1)(N, N, N, N, N));
lean_assert(instantiate_metavars(norm(F, ctx), menv) == lean_assert(menv->instantiate_metavars(norm(F, ctx)) ==
norm(instantiate_metavars(F, menv), ctx)); norm(menv->instantiate_metavars(F), ctx));
std::cout << "----------------------\n"; std::cout << "----------------------\n";
menv2.assign(m1, Var(8)); menv2->assign(m1, Var(8));
std::cout << norm(F, ctx) << "\n"; std::cout << norm(F, ctx) << "\n";
std::cout << instantiate_metavars(norm(F, ctx), menv2) << "\n"; std::cout << menv2->instantiate_metavars(norm(F, ctx)) << "\n";
std::cout << norm(instantiate_metavars(F, menv2), ctx) << "\n"; std::cout << norm(menv2->instantiate_metavars(F), ctx) << "\n";
lean_assert(instantiate_metavars(norm(F, ctx), menv2) == lean_assert(menv2->instantiate_metavars(norm(F, ctx)) ==
norm(instantiate_metavars(F, menv2), ctx)); norm(menv2->instantiate_metavars(F), ctx));
} }
static void tst18() { static void tst18() {
@ -367,8 +366,6 @@ static void tst18() {
context ctx; context ctx;
ctx = extend(ctx, "w1", Type()); ctx = extend(ctx, "w1", Type());
ctx = extend(ctx, "w2", Type()); ctx = extend(ctx, "w2", Type());
expr m1 = menv.mk_metavar();
expr m2 = menv.mk_metavar();
expr f = Const("f"); expr f = Const("f");
expr g = Const("g"); expr g = Const("g");
expr h = Const("h"); expr h = Const("h");
@ -381,17 +378,19 @@ static void tst18() {
env->add_var("a", N); env->add_var("a", N);
env->add_var("g", N >> N); env->add_var("g", N >> N);
env->add_var("h", N >> (N >> N)); env->add_var("h", N >> (N >> N));
expr m1 = menv->mk_metavar(context({{"z", Type()}, {"f", N >> N}, {"y", Type()}}));
expr m2 = menv->mk_metavar(context({{"z", Type()}, {"x", N}}));
expr F = Fun({z, Type()}, Fun({{f, N >> N}, {y, Type()}}, m1)(Fun({x, N}, g(z, x, m2)), N)); expr F = Fun({z, Type()}, Fun({{f, N >> N}, {y, Type()}}, m1)(Fun({x, N}, g(z, x, m2)), N));
std::cout << norm(F, ctx) << "\n"; std::cout << norm(F, ctx) << "\n";
metavar_env menv2 = menv; metavar_env menv2 = menv.copy();
menv2.assign(m1, Var(1)); menv2->assign(m1, Var(1));
menv2.assign(m2, h(Var(2), Var(1))); menv2->assign(m2, h(Var(2), Var(1)));
std::cout << instantiate_metavars(norm(F, ctx), menv2) << "\n"; std::cout << menv2->instantiate_metavars(norm(F, ctx)) << "\n";
std::cout << instantiate_metavars(F, menv2) << "\n"; std::cout << menv2->instantiate_metavars(F) << "\n";
lean_assert(instantiate_metavars(norm(F, ctx), menv2) == lean_assert_eq(menv2->instantiate_metavars(norm(F, ctx)),
norm(instantiate_metavars(F, menv2), ctx)); norm(menv2->instantiate_metavars(F), ctx));
lean_assert(instantiate_metavars(norm(F, ctx), menv2) == lean_assert_eq(menv2->instantiate_metavars(norm(F, ctx)),
Fun({{z, Type()}, {x, N}}, g(z, x, h(Var(2), z)))); Fun({{z, Type()}, {x, N}}, g(z, x, h(Var(2), z))));
} }
static void tst19() { static void tst19() {
@ -401,7 +400,7 @@ static void tst19() {
context ctx; context ctx;
ctx = extend(ctx, "w1", Type()); ctx = extend(ctx, "w1", Type());
ctx = extend(ctx, "w2", Type()); ctx = extend(ctx, "w2", Type());
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr x = Const("x"); expr x = Const("x");
expr y = Const("y"); expr y = Const("y");
expr N = Const("N"); expr N = Const("N");
@ -419,7 +418,7 @@ static void tst20() {
context ctx; context ctx;
ctx = extend(ctx, "w1", Type()); ctx = extend(ctx, "w1", Type());
ctx = extend(ctx, "w2", Type()); ctx = extend(ctx, "w2", Type());
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr x = Const("x"); expr x = Const("x");
expr y = Const("y"); expr y = Const("y");
expr z = Const("z"); expr z = Const("z");
@ -436,10 +435,10 @@ static void tst20() {
static void tst21() { static void tst21() {
metavar_env menv; metavar_env menv;
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr l = add_lift(add_lift(m1, 0, 1), 1, 1); expr l = add_lift(add_lift(m1, 0, 1), 1, 1);
expr r = add_lift(m1, 0, 2); expr r = add_lift(m1, 0, 2);
std::cout << menv.get_type(l) << " " << menv.get_type(r) << "\n"; std::cout << menv->get_type(l) << " " << menv->get_type(r) << "\n";
#if 0 #if 0
// Leo: I disabled the lift over lift optimization since it was // Leo: I disabled the lift over lift optimization since it was
// negatively impacting the heuristics // negatively impacting the heuristics
@ -481,7 +480,7 @@ static void tst23() {
buffer<unification_constraint> up; buffer<unification_constraint> up;
std::cout << F1 << "\n"; std::cout << F1 << "\n";
try { try {
std::cout << checker.infer_type(F1, context(), &menv, &up) << "\n"; std::cout << checker.infer_type(F1, context(), menv, up) << "\n";
} catch (kernel_exception & ex) { } catch (kernel_exception & ex) {
formatter fmt = mk_simple_formatter(); formatter fmt = mk_simple_formatter();
io_state st(options(), fmt); io_state st(options(), fmt);
@ -492,14 +491,14 @@ static void tst23() {
static void tst24() { static void tst24() {
metavar_env menv; metavar_env menv;
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
expr f = Const("f"); expr f = Const("f");
expr a = Const("a"); expr a = Const("a");
menv.assign(m1, f(m2)); menv->assign(m1, f(m2));
menv.assign(m2, a); menv->assign(m2, a);
lean_assert(instantiate_metavars(f(m1), menv) == f(f(a))); lean_assert(menv->instantiate_metavars(f(m1)) == f(f(a)));
std::cout << instantiate_metavars(f(m1), menv) << "\n"; std::cout << menv->instantiate_metavars(f(m1)) << "\n";
} }
static void tst25() { static void tst25() {
@ -513,9 +512,9 @@ static void tst25() {
env->add_var("N", Type()); env->add_var("N", Type());
env->add_var("a", N); env->add_var("a", N);
env->add_var("b", N); env->add_var("b", N);
expr m = menv.mk_metavar(); expr m = menv->mk_metavar();
expr F = m(a, b); expr F = m(a, b);
std::cout << checker.infer_type(F, context(), &menv, &up) << "\n"; std::cout << checker.infer_type(F, context(), menv, up) << "\n";
std::cout << menv << "\n"; std::cout << menv << "\n";
std::cout << up << "\n"; std::cout << up << "\n";
} }
@ -552,16 +551,16 @@ static void tst26() {
expr b = Const("b"); expr b = Const("b");
expr n = Const("n"); expr n = Const("n");
expr m = Const("m"); expr m = Const("m");
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
expr m3 = menv.mk_metavar(); expr m3 = menv->mk_metavar();
expr A1 = menv.mk_metavar(); expr A1 = menv->mk_metavar();
expr A2 = menv.mk_metavar(); expr A2 = menv->mk_metavar();
expr A3 = menv.mk_metavar(); expr A3 = menv->mk_metavar();
expr A4 = menv.mk_metavar(); expr A4 = menv->mk_metavar();
expr F = cons(A1, m1(a), cons(A2, m2(n), cons(A3, m3(b), nil(A4)))); expr F = cons(A1, m1(a), cons(A2, m2(n), cons(A3, m3(b), nil(A4))));
std::cout << F << "\n"; std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, &up) << "\n"; std::cout << checker.infer_type(F, context(), menv, up) << "\n";
std::cout << menv << "\n"; std::cout << menv << "\n";
std::cout << up << "\n"; std::cout << up << "\n";
} }
@ -588,14 +587,14 @@ static void tst27() {
env->add_var("f", Pi({A, Type()}, A >> (A >> Bool))); env->add_var("f", Pi({A, Type()}, A >> (A >> Bool)));
env->add_var("a", Int); env->add_var("a", Int);
env->add_var("b", Real); env->add_var("b", Real);
expr T1 = menv.mk_metavar(); expr T1 = menv->mk_metavar();
expr T2 = menv.mk_metavar(); expr T2 = menv->mk_metavar();
expr A1 = menv.mk_metavar(); expr A1 = menv->mk_metavar();
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
expr F = Fun({{x, T1}, {y, T2}}, f(A1, x, y))(m1(a), m2(b)); expr F = Fun({{x, T1}, {y, T2}}, f(A1, x, y))(m1(a), m2(b));
std::cout << F << "\n"; std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, &up) << "\n"; std::cout << checker.infer_type(F, context(), menv, up) << "\n";
std::cout << menv << "\n"; std::cout << menv << "\n";
std::cout << up << "\n"; std::cout << up << "\n";
} }
@ -604,12 +603,12 @@ static void tst28() {
metavar_env menv; metavar_env menv;
expr f = Const("f"); expr f = Const("f");
expr a = Const("a"); expr a = Const("a");
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
lean_assert(add_inst(m1, 0, f(a), menv) == m1); lean_assert(add_inst(m1, 0, f(a), menv) == m1);
lean_assert(add_inst(m1, 1, f(a), menv) == m1); lean_assert(add_inst(m1, 1, f(a), menv) == m1);
lean_assert(add_lift(m1, 0, 2, menv) == m1); lean_assert(add_lift(m1, 0, 2, menv) == m1);
lean_assert(add_lift(m1, 1, 2, menv) == m1); lean_assert(add_lift(m1, 1, 2, menv) == m1);
expr m2 = menv.mk_metavar(context({{"x", Bool}, {"y", Bool}})); expr m2 = menv->mk_metavar(context({{"x", Bool}, {"y", Bool}}));
lean_assert(add_inst(m2, 0, f(a), menv) != m2); lean_assert(add_inst(m2, 0, f(a), menv) != m2);
lean_assert(add_inst(m2, 0, f(a), menv) == add_inst(m2, 0, f(a))); lean_assert(add_inst(m2, 0, f(a), menv) == add_inst(m2, 0, f(a)));
lean_assert(add_inst(m2, 1, f(a), menv) != m2); lean_assert(add_inst(m2, 1, f(a), menv) != m2);

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

@ -323,6 +323,36 @@ static void tst16() {
check_justification_msg(mk_def_type_match_justification(ctx, "foo", f(a, x)), "Type of definition 'foo' must be convertible to expected type."); check_justification_msg(mk_def_type_match_justification(ctx, "foo", f(a, x)), "Type of definition 'foo' must be convertible to expected type.");
} }
static void f1(type_checker & tc, expr const & F) {
metavar_env menv;
expr m1 = menv->mk_metavar(context(), some_expr(Bool >> Int));
expr r = tc.infer_type(F, context(), menv);
lean_assert_eq(r, Int);
}
static void f2(type_checker & tc, expr const & F) {
metavar_env menv;
expr m1 = menv->mk_metavar(context(), some_expr(Bool >> Bool));
expr r = tc.infer_type(F, context(), menv);
lean_assert_eq(r, Bool);
}
static void tst17() {
environment env;
import_all(env);
type_checker tc(env);
expr A = Const("A");
expr F;
{
metavar_env menv;
expr m1 = menv->mk_metavar();
F = m1(True);
}
expr F2 = F;
f1(tc, F);
f2(tc, F);
}
int main() { int main() {
save_stack_info(); save_stack_info();
tst1(); tst1();
@ -341,5 +371,6 @@ int main() {
tst14(); tst14();
tst15(); tst15();
tst16(); tst16();
tst17();
return has_violations() ? 1 : 0; return has_violations() ? 1 : 0;
} }

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

@ -39,16 +39,16 @@ static void tst1() {
expr b = Const("b"); expr b = Const("b");
expr n = Const("n"); expr n = Const("n");
expr m = Const("m"); expr m = Const("m");
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
expr m3 = menv.mk_metavar(); expr m3 = menv->mk_metavar();
expr A1 = menv.mk_metavar(); expr A1 = menv->mk_metavar();
expr A2 = menv.mk_metavar(); expr A2 = menv->mk_metavar();
expr A3 = menv.mk_metavar(); expr A3 = menv->mk_metavar();
expr A4 = menv.mk_metavar(); expr A4 = menv->mk_metavar();
expr F = cons(A1, m1(a), cons(A2, m2(n), cons(A3, m3(b), nil(A4)))); expr F = cons(A1, m1(a), cons(A2, m2(n), cons(A3, m3(b), nil(A4))));
std::cout << F << "\n"; std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, &ucs) << "\n"; std::cout << checker.infer_type(F, context(), menv, ucs) << "\n";
expr int_id = Fun({a, Int}, a); expr int_id = Fun({a, Int}, a);
expr nat_id = Fun({a, Nat}, a); expr nat_id = Fun({a, Nat}, a);
ucs.push_back(mk_choice_constraint(context(), m1, { int_id, mk_int_to_real_fn() }, justification())); ucs.push_back(mk_choice_constraint(context(), m1, { int_id, mk_int_to_real_fn() }, justification()));
@ -84,15 +84,15 @@ static void tst2() {
env->add_var("g", Pi({A, Type()}, A >> A)); env->add_var("g", Pi({A, Type()}, A >> A));
expr a = Const("a"); expr a = Const("a");
env->add_var("a", Int); env->add_var("a", Int);
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
expr m3 = menv.mk_metavar(); expr m3 = menv->mk_metavar();
expr m4 = menv.mk_metavar(); expr m4 = menv->mk_metavar();
expr int_id = Fun({a, Int}, a); expr int_id = Fun({a, Int}, a);
expr nat_id = Fun({a, Nat}, a); expr nat_id = Fun({a, Nat}, a);
expr F = m1(g(m2, m3(a)), m4(nVal(0))); expr F = m1(g(m2, m3(a)), m4(nVal(0)));
std::cout << F << "\n"; std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, &ucs) << "\n"; std::cout << checker.infer_type(F, context(), menv, ucs) << "\n";
ucs.push_back(mk_choice_constraint(context(), m1, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification())); ucs.push_back(mk_choice_constraint(context(), m1, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m3, { int_id, mk_int_to_real_fn() }, justification())); ucs.push_back(mk_choice_constraint(context(), m3, { int_id, mk_int_to_real_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification())); ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification()));
@ -125,17 +125,17 @@ static void tst3() {
env->add_var("f", Pi({A, Type()}, A >> A)); env->add_var("f", Pi({A, Type()}, A >> A));
expr a = Const("a"); expr a = Const("a");
env->add_var("a", Int); env->add_var("a", Int);
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
expr m3 = menv.mk_metavar(); expr m3 = menv->mk_metavar();
expr m4 = menv.mk_metavar(); expr m4 = menv->mk_metavar();
expr m5 = menv.mk_metavar(); expr m5 = menv->mk_metavar();
expr int_id = Fun({a, Int}, a); expr int_id = Fun({a, Int}, a);
expr nat_id = Fun({a, Nat}, a); expr nat_id = Fun({a, Nat}, a);
expr x = Const("x"); expr x = Const("x");
expr F = Fun({x, m1}, m2(f(m3, x), m4(nVal(10))))(m5(a)); expr F = Fun({x, m1}, m2(f(m3, x), m4(nVal(10))))(m5(a));
std::cout << F << "\n"; std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, &ucs) << "\n"; std::cout << checker.infer_type(F, context(), menv, ucs) << "\n";
ucs.push_back(mk_choice_constraint(context(), m2, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification())); ucs.push_back(mk_choice_constraint(context(), m2, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification())); ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m5, { int_id, mk_int_to_real_fn() }, justification())); ucs.push_back(mk_choice_constraint(context(), m5, { int_id, mk_int_to_real_fn() }, justification()));
@ -169,18 +169,18 @@ static void tst4() {
expr b = Const("b"); expr b = Const("b");
env->add_var("a", Int); env->add_var("a", Int);
env->add_var("b", Real); env->add_var("b", Real);
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
expr m3 = menv.mk_metavar(); expr m3 = menv->mk_metavar();
expr m4 = menv.mk_metavar(); expr m4 = menv->mk_metavar();
expr m5 = menv.mk_metavar(); expr m5 = menv->mk_metavar();
expr m6 = menv.mk_metavar(); expr m6 = menv->mk_metavar();
expr x = Const("x"); expr x = Const("x");
expr y = Const("y"); expr y = Const("y");
expr int_id = Fun({a, Int}, a); expr int_id = Fun({a, Int}, a);
expr F = Fun({{x, m1}, {y, m2}}, m3(f(m4, x), f(m5, y)))(m6(a), b); expr F = Fun({{x, m1}, {y, m2}}, m3(f(m4, x), f(m5, y)))(m6(a), b);
std::cout << F << "\n"; std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, &ucs) << "\n"; std::cout << checker.infer_type(F, context(), menv, ucs) << "\n";
ucs.push_back(mk_choice_constraint(context(), m3, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification())); ucs.push_back(mk_choice_constraint(context(), m3, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m6, { int_id, mk_int_to_real_fn() }, justification())); ucs.push_back(mk_choice_constraint(context(), m6, { int_id, mk_int_to_real_fn() }, justification()));
elaborator elb(env, menv, ucs.size(), ucs.data()); elaborator elb(env, menv, ucs.size(), ucs.data());
@ -213,16 +213,16 @@ static void tst5() {
expr b = Const("b"); expr b = Const("b");
env->add_var("a", Int); env->add_var("a", Int);
env->add_var("b", Real); env->add_var("b", Real);
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
expr m3 = menv.mk_metavar(); expr m3 = menv->mk_metavar();
expr m4 = menv.mk_metavar(); expr m4 = menv->mk_metavar();
expr x = Const("x"); expr x = Const("x");
expr y = Const("y"); expr y = Const("y");
expr int_id = Fun({a, Int}, a); expr int_id = Fun({a, Int}, a);
expr F = Fun({{x, m1}, {y, m2}}, f(m3, x, y))(m4(a), b); expr F = Fun({{x, m1}, {y, m2}}, f(m3, x, y))(m4(a), b);
std::cout << F << "\n"; std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, &ucs) << "\n"; std::cout << checker.infer_type(F, context(), menv, ucs) << "\n";
ucs.push_back(mk_choice_constraint(context(), m4, { int_id, mk_int_to_real_fn() }, justification())); ucs.push_back(mk_choice_constraint(context(), m4, { int_id, mk_int_to_real_fn() }, justification()));
elaborator elb(env, menv, ucs.size(), ucs.data()); elaborator elb(env, menv, ucs.size(), ucs.data());
elb.next(); elb.next();
@ -248,10 +248,10 @@ static void tst6() {
expr b = Const("b"); expr b = Const("b");
expr H1 = Const("H1"); expr H1 = Const("H1");
expr H2 = Const("H2"); expr H2 = Const("H2");
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
expr m3 = menv.mk_metavar(); expr m3 = menv->mk_metavar();
expr m4 = menv.mk_metavar(); expr m4 = menv->mk_metavar();
env->add_var("f", Int >> (Int >> Int)); env->add_var("f", Int >> (Int >> Int));
env->add_var("a", Int); env->add_var("a", Int);
env->add_var("b", Int); env->add_var("b", Int);
@ -259,11 +259,11 @@ static void tst6() {
env->add_axiom("H2", Eq(a, b)); env->add_axiom("H2", Eq(a, b));
expr V = Subst(m1, m2, m3, m4, H1, H2); expr V = Subst(m1, m2, m3, m4, H1, H2);
expr expected = Eq(f(a, f(b, b)), a); expr expected = Eq(f(a, f(b, b)), a);
expr given = checker.infer_type(V, context(), &menv, &ucs); expr given = checker.infer_type(V, context(), menv, ucs);
ucs.push_back(mk_eq_constraint(context(), expected, given, justification())); ucs.push_back(mk_eq_constraint(context(), expected, given, justification()));
elaborator elb(env, menv, ucs.size(), ucs.data()); elaborator elb(env, menv, ucs.size(), ucs.data());
metavar_env s = elb.next(); metavar_env s = elb.next();
std::cout << instantiate_metavars(V, s) << "\n"; std::cout << s->instantiate_metavars(V) << "\n";
} }
#define _ mk_placeholder() #define _ mk_placeholder()
@ -273,10 +273,10 @@ static expr elaborate(expr const & e, environment const & env) {
buffer<unification_constraint> ucs; buffer<unification_constraint> ucs;
type_checker checker(env); type_checker checker(env);
expr e2 = replace_placeholders_with_metavars(e, menv); expr e2 = replace_placeholders_with_metavars(e, menv);
checker.infer_type(e2, context(), &menv, &ucs); checker.infer_type(e2, context(), menv, ucs);
elaborator elb(env, menv, ucs.size(), ucs.data()); elaborator elb(env, menv, ucs.size(), ucs.data());
metavar_env s = elb.next(); metavar_env s = elb.next();
return instantiate_metavars(e2, s); return s->instantiate_metavars(e2);
} }
// Check elaborator success // Check elaborator success
@ -645,16 +645,16 @@ void tst20() {
expr x = Const("x"); expr x = Const("x");
expr a = Const("a"); expr a = Const("a");
expr b = Const("b"); expr b = Const("b");
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr l = m1(b, a); expr l = m1(b, a);
expr r = f(b, f(a, b)); expr r = f(b, f(a, b));
elaborator elb(env, menv, context(), l, r); elaborator elb(env, menv, context(), l, r);
while (true) { while (true) {
try { try {
auto sol = elb.next(); 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"; std::cout << sol->instantiate_metavars(l) << "\n";
lean_assert(instantiate_metavars(l, sol) == r); lean_assert(sol->instantiate_metavars(l) == r);
std::cout << "--------------\n"; std::cout << "--------------\n";
} catch (elaborator_exception & ex) { } catch (elaborator_exception & ex) {
break; break;
@ -677,16 +677,16 @@ void tst21() {
expr x = Const("x"); expr x = Const("x");
expr a = Const("a"); expr a = Const("a");
expr b = Const("b"); expr b = Const("b");
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr l = m1(b, a); expr l = m1(b, a);
expr r = Fun({x, N}, f(x, Eq(a, b))); expr r = Fun({x, N}, f(x, Eq(a, b)));
elaborator elb(env, menv, context(), l, r); elaborator elb(env, menv, context(), l, r);
while (true) { while (true) {
try { try {
auto sol = elb.next(); 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"; std::cout << sol->instantiate_metavars(l) << "\n";
lean_assert(instantiate_metavars(l, sol) == r); lean_assert(sol->instantiate_metavars(l) == r);
std::cout << "--------------\n"; std::cout << "--------------\n";
} catch (elaborator_exception & ex) { } catch (elaborator_exception & ex) {
break; break;
@ -704,11 +704,11 @@ void tst22() {
env->add_var("f", N >> (Int >> N)); env->add_var("f", N >> (Int >> N));
env->add_var("a", N); env->add_var("a", N);
env->add_var("b", N); env->add_var("b", N);
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
expr m3 = menv.mk_metavar(); expr m3 = menv->mk_metavar();
expr t1 = menv.get_type(m1); expr t1 = menv->get_type(m1);
expr t2 = menv.get_type(m2); expr t2 = menv->get_type(m2);
expr f = Const("f"); expr f = Const("f");
expr a = Const("a"); expr a = Const("a");
expr b = Const("b"); expr b = Const("b");
@ -718,10 +718,10 @@ void tst22() {
while (true) { while (true) {
try { try {
auto sol = elb.next(); auto sol = elb.next();
std::cout << m3 << " -> " << *(sol.get_subst(m3)) << "\n"; std::cout << m3 << " -> " << *(sol->get_subst(m3)) << "\n";
lean_assert(*(sol.get_subst(m3)) == iVal(1)); lean_assert(*(sol->get_subst(m3)) == iVal(1));
std::cout << instantiate_metavars(l, sol) << "\n"; std::cout << sol->instantiate_metavars(l) << "\n";
std::cout << instantiate_metavars(r, sol) << "\n"; std::cout << sol->instantiate_metavars(r) << "\n";
std::cout << "--------------\n"; std::cout << "--------------\n";
} catch (elaborator_exception & ex) { } catch (elaborator_exception & ex) {
break; break;
@ -740,18 +740,18 @@ void tst23() {
expr x = Const("x"); expr x = Const("x");
expr y = Const("y"); expr y = Const("y");
expr f = Const("f"); expr f = Const("f");
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
expr l = Fun({{x, N}, {y, N}}, Eq(y, f(x, m1))); expr l = Fun({{x, N}, {y, N}}, Eq(y, f(x, m1)));
expr r = Fun({{x, N}, {y, N}}, Eq(m2, f(m1, x))); expr r = Fun({{x, N}, {y, N}}, Eq(m2, f(m1, x)));
elaborator elb(env, menv, context(), l, r); elaborator elb(env, menv, context(), l, r);
while (true) { while (true) {
try { try {
auto sol = elb.next(); 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"; std::cout << sol->instantiate_metavars(l) << "\n";
lean_assert_eq(instantiate_metavars(l, sol), lean_assert_eq(sol->instantiate_metavars(l),
instantiate_metavars(r, sol)); sol->instantiate_metavars(r));
std::cout << "--------------\n"; std::cout << "--------------\n";
} catch (elaborator_exception & ex) { } catch (elaborator_exception & ex) {
break; break;
@ -768,7 +768,7 @@ void tst24() {
env->add_var("N", Type()); env->add_var("N", Type());
env->add_var("f", N >> (N >> N)); env->add_var("f", N >> (N >> N));
expr f = Const("f"); expr f = Const("f");
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr l = f(f(m1)); expr l = f(f(m1));
expr r = f(m1); expr r = f(m1);
elaborator elb(env, menv, context(), l, r); elaborator elb(env, menv, context(), l, r);
@ -790,17 +790,17 @@ void tst25() {
expr x = Const("x"); expr x = Const("x");
expr y = Const("y"); expr y = Const("y");
expr f = Const("f"); expr f = Const("f");
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr l = Fun({x, N}, Fun({y, N}, f(m1, y))(x)); expr l = Fun({x, N}, Fun({y, N}, f(m1, y))(x));
expr r = Fun({x, N}, f(x, x)); expr r = Fun({x, N}, f(x, x));
elaborator elb(env, menv, context(), l, r); elaborator elb(env, menv, context(), l, r);
while (true) { while (true) {
try { try {
auto sol = elb.next(); 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"; std::cout << sol->instantiate_metavars(l) << "\n";
lean_assert_eq(beta_reduce(instantiate_metavars(l, sol)), lean_assert_eq(beta_reduce(sol->instantiate_metavars(l)),
beta_reduce(instantiate_metavars(r, sol))); beta_reduce(sol->instantiate_metavars(r)));
std::cout << "--------------\n"; std::cout << "--------------\n";
} catch (elaborator_exception & ex) { } catch (elaborator_exception & ex) {
break; break;
@ -827,14 +827,14 @@ void tst26() {
env->add_var("g", Pi({A, TypeU}, A >> A)); env->add_var("g", Pi({A, TypeU}, A >> A));
expr a = Const("a"); expr a = Const("a");
env->add_var("a", Type(level()+1)); env->add_var("a", Type(level()+1));
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr F = Eq(g(m1, a), a); expr F = Eq(g(m1, a), a);
std::cout << F << "\n"; std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, &ucs) << "\n"; std::cout << checker.infer_type(F, context(), menv, ucs) << "\n";
elaborator elb(env, menv, ucs.size(), ucs.data()); elaborator elb(env, menv, ucs.size(), ucs.data());
metavar_env s = elb.next(); metavar_env s = elb.next();
std::cout << instantiate_metavars(F, s) << "\n"; std::cout << s->instantiate_metavars(F) << "\n";
lean_assert_eq(instantiate_metavars(F, s), Eq(g(Type(level()+1), a), a)); lean_assert_eq(s->instantiate_metavars(F), Eq(g(Type(level()+1), a), a));
} }
void tst27() { void tst27() {
@ -860,16 +860,16 @@ void tst27() {
env->add_var("my_eq", Pi({A, TypeU}, A >> (A >> Bool))); env->add_var("my_eq", Pi({A, TypeU}, A >> (A >> Bool)));
env->add_var("g", Pi({A, TypeU}, A >> A)); env->add_var("g", Pi({A, TypeU}, A >> A));
env->add_var("a", TypeM); env->add_var("a", TypeM);
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
expr m3 = menv.mk_metavar(); expr m3 = menv->mk_metavar();
expr F = Fun({f, m1}, eq(m2, g(m3, f)(a), a)); expr F = Fun({f, m1}, eq(m2, g(m3, f)(a), a));
std::cout << F << "\n"; std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, &ucs) << "\n"; std::cout << checker.infer_type(F, context(), menv, ucs) << "\n";
elaborator elb(env, menv, ucs.size(), ucs.data()); elaborator elb(env, menv, ucs.size(), ucs.data());
metavar_env s = elb.next(); metavar_env s = elb.next();
std::cout << instantiate_metavars(F, s) << "\n"; std::cout << s->instantiate_metavars(F) << "\n";
lean_assert_eq(instantiate_metavars(F, s), lean_assert_eq(s->instantiate_metavars(F),
Fun({f, TypeM >> TypeM}, eq(TypeM, g(TypeM >> TypeM, f)(a), a))); Fun({f, TypeM >> TypeM}, eq(TypeM, g(TypeM >> TypeM, f)(a), a)));
} }

10
src/tests/library/rewriter/fo_match.cpp
View file

@ -400,8 +400,8 @@ static void match_eq_tst3() {
static void match_metavar_tst1() { static void match_metavar_tst1() {
cout << "--- match_metavar_tst1() ---" << endl; cout << "--- match_metavar_tst1() ---" << endl;
metavar_env menv; metavar_env menv;
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
expr f = Const("f"); expr f = Const("f");
subst_map s; subst_map s;
bool result = test_match(m1, m1, 0, s); bool result = test_match(m1, m1, 0, s);
@ -412,8 +412,8 @@ static void match_metavar_tst1() {
static void match_metavar_tst2() { static void match_metavar_tst2() {
cout << "--- match_metavar_tst2() ---" << endl; cout << "--- match_metavar_tst2() ---" << endl;
metavar_env menv; metavar_env menv;
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
expr f = Const("f"); expr f = Const("f");
subst_map s; subst_map s;
bool result = test_match(m1, m2, 0, s); bool result = test_match(m1, m2, 0, s);
@ -424,7 +424,7 @@ static void match_metavar_tst2() {
static void match_metavar_tst3() { static void match_metavar_tst3() {
cout << "--- match_metavar_tst3() ---" << endl; cout << "--- match_metavar_tst3() ---" << endl;
metavar_env menv; metavar_env menv;
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr f = Const("f"); expr f = Const("f");
subst_map s; subst_map s;
bool result = test_match(m1, f, 0, s); bool result = test_match(m1, f, 0, s);

16
src/tests/library/type_inferer.cpp
View file

@ -124,16 +124,16 @@ static void tst4() {
expr b = Const("b"); expr b = Const("b");
expr n = Const("n"); expr n = Const("n");
expr m = Const("m"); expr m = Const("m");
expr m1 = menv.mk_metavar(); expr m1 = menv->mk_metavar();
expr m2 = menv.mk_metavar(); expr m2 = menv->mk_metavar();
expr m3 = menv.mk_metavar(); expr m3 = menv->mk_metavar();
expr A1 = menv.mk_metavar(); expr A1 = menv->mk_metavar();
expr A2 = menv.mk_metavar(); expr A2 = menv->mk_metavar();
expr A3 = menv.mk_metavar(); expr A3 = menv->mk_metavar();
expr A4 = menv.mk_metavar(); expr A4 = menv->mk_metavar();
expr F = cons(A1, m1(a), cons(A2, m2(n), cons(A3, m3(b), nil(A4)))); expr F = cons(A1, m1(a), cons(A2, m2(n), cons(A3, m3(b), nil(A4))));
std::cout << F << "\n"; std::cout << F << "\n";
std::cout << inferer(F, context(), &menv, &uc) << "\n"; std::cout << inferer(F, context(), menv, uc) << "\n";
std::cout << uc << "\n"; std::cout << uc << "\n";
} }