From cdab19b88c559ed4cf875965005d4e5e75f98ae9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 Aug 2013 20:39:38 -0700 Subject: [PATCH] Simplify the elaborator Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_parser.cpp | 20 +- src/library/elaborator.h | 2 +- src/library/metavar_env.cpp | 288 +++++++++------------------- src/library/metavar_env.h | 67 +++---- src/tests/library/implicit_args.cpp | 263 +++---------------------- 5 files changed, 149 insertions(+), 491 deletions(-) diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp index 51849971a..f1ab6e4d1 100644 --- a/src/frontends/lean/lean_parser.cpp +++ b/src/frontends/lean/lean_parser.cpp @@ -116,7 +116,6 @@ class parser::imp { bool m_found_errors; local_decls m_local_decls; unsigned m_num_local_decls; - context m_context; builtins m_builtins; expr_pos_info m_expr_pos_info; pos_info m_last_cmd_pos; @@ -143,16 +142,13 @@ class parser::imp { imp & m_fn; local_decls::mk_scope m_scope; unsigned m_old_num_local_decls; - context m_old_context; mk_scope(imp & fn): m_fn(fn), m_scope(fn.m_local_decls), - m_old_num_local_decls(fn.m_num_local_decls), - m_old_context(fn.m_context) { + m_old_num_local_decls(fn.m_num_local_decls) { } ~mk_scope() { m_fn.m_num_local_decls = m_old_num_local_decls; - m_fn.m_context = m_old_context; } }; @@ -661,7 +657,7 @@ class parser::imp { auto p = pos(); next(); mk_scope scope(*this); - register_binding(g_unused, expr()); + register_binding(g_unused); // The -1 is a trick to get right associativity in Pratt's parsers expr right = parse_expr(g_arrow_precedence-1); return save(mk_arrow(left, right), p); @@ -688,12 +684,8 @@ class parser::imp { } /** \brief Register the name \c n as a local declaration. */ - void register_binding(name const & n, expr const & type, expr const & val = expr()) { + void register_binding(name const & n) { unsigned lvl = m_num_local_decls; - if (val) - m_context = extend(m_context, n, expr(), val); - else - m_context = extend(m_context, n, type); m_local_decls.insert(n, lvl); m_num_local_decls++; lean_assert(m_local_decls.find(n)->second == lvl); @@ -710,7 +702,7 @@ class parser::imp { unsigned sz = result.size(); result.resize(sz + names.size()); expr type = parse_expr(); - for (std::pair const & n : names) register_binding(n.second, type); + for (std::pair const & n : names) register_binding(n.second); unsigned i = names.size(); while (i > 0) { --i; @@ -834,7 +826,7 @@ class parser::imp { name id = check_identifier_next("invalid let expression, identifier expected"); check_assign_next("invalid let expression, ':=' expected"); expr val = parse_expr(); - register_binding(id, expr(), val); + register_binding(id); bindings.push_back(std::make_tuple(p, id, val)); if (curr_is_in()) { next(); @@ -881,7 +873,7 @@ class parser::imp { /** \brief Create a fresh metavariable. */ expr mk_metavar() { - return m_elaborator.mk_metavar(m_context); + return m_elaborator.mk_metavar(m_num_local_decls); } /** \brief Parse \c _ a hole that must be filled by the elaborator. */ diff --git a/src/library/elaborator.h b/src/library/elaborator.h index ab25ff853..f4b21417e 100644 --- a/src/library/elaborator.h +++ b/src/library/elaborator.h @@ -30,7 +30,7 @@ public: metavar_env & menv() { return m_metaenv; } void clear() { m_metaenv.clear(); } - expr mk_metavar(context const & ctx) { return m_metaenv.mk_metavar(ctx); } + expr mk_metavar(unsigned ctx_sz) { return m_metaenv.mk_metavar(ctx_sz); } void set_interrupt(bool flag) { m_metaenv.set_interrupt(flag); } void interrupt() { set_interrupt(true); } diff --git a/src/library/metavar_env.cpp b/src/library/metavar_env.cpp index c965b7b5b..d2491a19c 100644 --- a/src/library/metavar_env.cpp +++ b/src/library/metavar_env.cpp @@ -48,9 +48,24 @@ bool has_metavar(expr const & e) { } } -metavar_env::cell::cell(expr const & e, context const & ctx, unsigned find): +/** \brief Return true iff \c e contains a metavariable with index midx */ +bool has_metavar(expr const & e, unsigned midx) { + auto f = [=](expr const & m, unsigned offset) { + if (is_metavar(m) && metavar_idx(m) == midx) + throw found_metavar(); + }; + try { + for_each_fn proc(f); + proc(e); + return false; + } catch (found_metavar) { + return true; + } +} + +metavar_env::cell::cell(expr const & e, unsigned ctx_size, unsigned find): m_expr(e), - m_context(ctx), + m_ctx_size(ctx_size), m_find(find), m_rank(0), m_state(state::Unprocessed) { @@ -100,85 +115,6 @@ unsigned metavar_env::new_rank(unsigned r1, unsigned r2) { else return std::max(r1, r2); } -/** - \brief Assign m <- s, where s is a term. - - \pre s contains only unassigned metavariables. - - The contexts of the unassigned metavariables occurring in s are - shortened to the length of the context associated with m. - - The assignment is valid if: - - 1) \c s does contain free variables outside of the context - associated with m. - - 2) \c s does not contain m. - - 3) The context of every metavariable in s is unifiable with the - context of m. -*/ -void metavar_env::assign_term(expr const & m, expr s, context const & ctx) { - lean_assert(is_metavar(m)); - lean_assert(!is_assigned(m)); - lean_assert(!is_metavar(s)); - cell & mc = root_cell(m); - unsigned len_mc = length(mc.m_context); - unsigned len_ctx = length(ctx); - if (len_ctx < len_mc) { - // mc is used in a context with len_mc variables, - // but s free variables are references to a smaller context. - // So, we must lift s free variables. - s = lift_free_vars(s, len_mc - len_ctx); - } else if (len_ctx > len_mc) { - // s must only contain free variables that are available in mc.m_context - if (has_free_var(s, 0, len_ctx - len_mc)) - failed_to_unify(); - s = lower_free_vars(s, len_ctx - len_mc); - } - unsigned fv_range = 0; - auto proc = [&](expr const & n, unsigned offset) { - if (is_var(n)) { - unsigned vidx = var_idx(n); - if (vidx >= offset) { - unsigned fv_idx = vidx - offset; - fv_range = std::max(fv_range, fv_idx+1); - } - } else if (is_metavar(n)) { - // Remark: before performing an assignment, we - // instantiate all assigned metavariables in s. - lean_assert(!is_assigned(n)); - cell & nc = root_cell(n); - if (mc.m_find == nc.m_find) - failed_to_unify(); // cycle detected - unsigned len_nc = length(nc.m_context); - // make sure nc is not bigger than mc - while (len_nc > len_mc) { nc.m_context = cdr(nc.m_context); len_nc--; } - - // Remark: By property 2 of metavariable contexts, we - // know that m can't occur in the reduced - // nc.m_context. - // - // Property 2: If a metavariable ?m1 occurs in context ctx2 of - // metavariable ?m2, then context ctx1 of ?m1 must be a prefix of ctx2. - // - - // make sure nc that prefix of mc - unify_ctx_prefix(nc.m_context, mc.m_context); - - fv_range = std::max(fv_range, len_nc); - } - }; - - for_each_fn visitor(proc); - visitor(s); - if (fv_range > length(mc.m_context)) { - // s has a free variable that is not in the context of mc - failed_to_unify(); - } - mc.m_expr = s; -} - [[noreturn]] void metavar_env::failed_to_unify() { throw exception("failed to unify"); } @@ -199,11 +135,11 @@ metavar_env::metavar_env(environment const & env, name_set const * available_def metavar_env::metavar_env(environment const & env):metavar_env(env, nullptr) { } -expr metavar_env::mk_metavar(context const & ctx) { +expr metavar_env::mk_metavar(unsigned ctx_sz) { m_modified = true; unsigned vidx = m_cells.size(); expr m = ::lean::mk_metavar(vidx); - m_cells.push_back(cell(m, ctx, vidx)); + m_cells.push_back(cell(m, ctx_sz, vidx)); return m; } @@ -217,20 +153,34 @@ expr metavar_env::root_at(expr const & e, unsigned ctx_size) const { if (is_metavar(c.m_expr)) { return c.m_expr; } else { - unsigned len_c = length(c.m_context); - lean_assert(len_c <= ctx_size); - if (len_c < ctx_size) { - return lift_free_vars(c.m_expr, ctx_size - len_c); - } else { - return c.m_expr; - } + lean_assert(c.m_ctx_size <= ctx_size); + return lift_free_vars(c.m_expr, ctx_size - c.m_ctx_size); } } else { return e; } } -void metavar_env::assign(expr const & m, expr const & s, context const & ctx) { +/** + \brief Make sure that the metavariables in \c s can only access + ctx_size free variables. + + \pre s does not contain assigned metavariables. +*/ +void metavar_env::reduce_metavars_ctx_size(expr const & s, unsigned ctx_size) { + auto proc = [&](expr const & m, unsigned offset) { + if (is_metavar(m)) { + lean_assert(!is_assigned(m)); + cell & mc = root_cell(m); + if (mc.m_ctx_size > ctx_size + offset) + mc.m_ctx_size = ctx_size + offset; + } + }; + for_each_fn visitor(proc); + visitor(s); +} + +void metavar_env::assign(expr const & m, expr const & s, unsigned ctx_size) { lean_assert(is_metavar(m)); lean_assert(!is_assigned(m)); if (m == s) @@ -239,14 +189,15 @@ void metavar_env::assign(expr const & m, expr const & s, context const & ctx) { cell & mc = root_cell(m); lean_assert(is_metavar(mc.m_expr)); lean_assert(metavar_idx(mc.m_expr) == mc.m_find); - expr _s = instantiate_metavars(s, length(ctx)); + expr _s = instantiate_metavars(s, ctx_size); if (is_metavar(_s)) { // both are unassigned meta-variables... lean_assert(!is_assigned(_s)); cell & sc = root_cell(_s); lean_assert(is_metavar(sc.m_expr)); - ensure_same_length(mc.m_context, sc.m_context); - unify_ctx_entries(mc.m_context, sc.m_context); + unsigned new_ctx_sz = std::min(mc.m_ctx_size, sc.m_ctx_size); + mc.m_ctx_size = new_ctx_sz; + sc.m_ctx_size = new_ctx_sz; if (mc.m_rank > sc.m_rank) { // we want to make mc the root of the equivalence class. mc.m_rank = new_rank(mc.m_rank, sc.m_rank); @@ -257,9 +208,26 @@ void metavar_env::assign(expr const & m, expr const & s, context const & ctx) { mc.m_find = sc.m_find; } } else { - assign_term(m, _s, ctx); + lean_assert(!is_metavar(_s)); + if (has_metavar(_s, mc.m_find)) { + failed_to_unify(); + } + reduce_metavars_ctx_size(_s, mc.m_ctx_size); + if (ctx_size < mc.m_ctx_size) { + // mc is used in a context with more free variables. + // but s free variables are references to a smaller context. + // So, we must lift _s free variables. + _s = lift_free_vars(_s, mc.m_ctx_size - ctx_size); + } else if (ctx_size > mc.m_ctx_size) { + // _s must only contain free variables that are available + // in the context of mc + if (has_free_var(_s, 0, ctx_size - mc.m_ctx_size)) { + failed_to_unify(); + } + _s = lower_free_vars(_s, ctx_size - mc.m_ctx_size); + } + mc.m_expr = _s; } - lean_assert(check_invariant()); } expr metavar_env::instantiate_metavars(expr const & e, unsigned outer_offset) { @@ -272,20 +240,16 @@ expr metavar_env::instantiate_metavars(expr const & e, unsigned outer_offset) { return rc.m_expr; } else { switch (rc.m_state) { - case state::Unprocessed: { + case state::Unprocessed: rc.m_state = state::Processing; - unsigned rc_len = length(rc.m_context); - rc.m_expr = instantiate_metavars(rc.m_expr, rc_len); + rc.m_expr = instantiate_metavars(rc.m_expr, rc.m_ctx_size); rc.m_state = state::Processed; - lean_assert(rc_len <= offset + outer_offset); - return lift_free_vars(rc.m_expr, offset + outer_offset - rc_len); - } + lean_assert(rc.m_ctx_size <= offset + outer_offset); + return lift_free_vars(rc.m_expr, offset + outer_offset - rc.m_ctx_size); case state::Processing: throw exception("cycle detected"); - case state::Processed: { - unsigned rc_len = length(rc.m_context); - lean_assert(rc_len <= offset + outer_offset); - return lift_free_vars(rc.m_expr, offset + outer_offset - rc_len); - } + case state::Processed: + lean_assert(rc.m_ctx_size <= offset + outer_offset); + return lift_free_vars(rc.m_expr, offset + outer_offset - rc.m_ctx_size); } } } @@ -316,73 +280,6 @@ expr const & metavar_env::get_definition(expr const & e) { return m_env.find_object(const_name(e)).get_value(); } -/** - \brief Ensure both contexts have the same length -*/ -void metavar_env::ensure_same_length(context & ctx1, context & ctx2) { - if (is_eqp(ctx1, ctx2)) { - return; - } else { - unsigned len1 = length(ctx1); - unsigned len2 = length(ctx2); - unsigned new_len = std::min(len1, len2); - while (len1 > new_len) { ctx1 = cdr(ctx1); --len1; } - while (len2 > new_len) { ctx2 = cdr(ctx2); --len2; } - } -} - -/** - \brief Check if ctx1 is a prefix of ctx2. That is, - 1- length(ctx1) <= length(ctx2) - 2- Every entry in ctxt1 is unifiable with the corresponding - entry in ctx2. -*/ -void metavar_env::unify_ctx_prefix(context const & ctx1, context const & ctx2) { - if (is_eqp(ctx1, ctx2)) { - return; - } else { - unsigned len1 = length(ctx1); - unsigned len2 = length(ctx2); - if (len1 > len2) - failed_to_unify(); - context _ctx2 = ctx2; - while (len2 > len1) { _ctx2 = cdr(_ctx2); --len2; } - unify_ctx_entries(ctx1, _ctx2); - } -} - -/** - \brief Unify the context entries of the given contexts. - - \pre length(ctx1) == length(ctx2) -*/ -void metavar_env::unify_ctx_entries(context const & ctx1, context const & ctx2) { - lean_assert(length(ctx1) == length(ctx2)); - auto it1 = ctx1.begin(); - auto end1 = ctx1.end(); - auto it2 = ctx2.begin(); - for (; it1 != end1; ++it1, ++it2) { - context_entry const & e1 = *it1; - context_entry const & e2 = *it2; - - if ((e1.get_domain()) && (e2.get_domain())) { - unify(e1.get_domain(), e2.get_domain()); - } else if (!(e1.get_domain()) && !(e2.get_domain())) { - // do nothing - } else { - failed_to_unify(); - } - - if ((e1.get_body()) && (e2.get_body())) { - unify(e1.get_body(), e2.get_body()); - } else if (!(e1.get_body()) && !(e2.get_body())) { - // do nothing - } else { - failed_to_unify(); - } - } -} - // Little hack for matching (?m #0) with t // TODO: implement some support for higher order unification. bool metavar_env::is_simple_ho_match(expr const & e1, expr const & e2, context const & ctx) { @@ -395,15 +292,15 @@ bool metavar_env::is_simple_ho_match(expr const & e1, expr const & e2, context c // Little hack for matching (?m #0) with t // TODO: implement some support for higher order unification. -void metavar_env::unify_simple_ho_match(expr const & e1, expr const & e2, context const & ctx) { - unify(arg(e1,0), mk_lambda(car(ctx).get_name(), car(ctx).get_domain(), e2), ctx); +void metavar_env::unify_simple_ho_match(expr const & e1, expr const & e2, unsigned ctx_size, context const & ctx) { + unify(arg(e1,0), mk_lambda(car(ctx).get_name(), car(ctx).get_domain(), e2), ctx_size, ctx); } /** \brief Auxiliary function for unifying expressions \c e1 and \c e2 when none of them are metavariables. */ -void metavar_env::unify_core(expr const & e1, expr const & e2, context const & ctx) { +void metavar_env::unify_core(expr const & e1, expr const & e2, unsigned ctx_size, context const & ctx) { check_interrupted(m_interrupted); lean_assert(!is_metavar(e1)); lean_assert(!is_metavar(e2)); @@ -412,51 +309,51 @@ void metavar_env::unify_core(expr const & e1, expr const & e2, context const & c } else if (is_type(e1) && is_type(e2)) { return; // ignoring type universe levels. We let the kernel check that } else if (is_abstraction(e1) && is_abstraction(e2)) { - unify(abst_domain(e1), abst_domain(e2), ctx); - unify(abst_body(e1), abst_body(e2), extend(ctx, abst_name(e1), abst_domain(e1))); + unify(abst_domain(e1), abst_domain(e2), ctx_size, ctx); + unify(abst_body(e1), abst_body(e2), ctx_size+1, extend(ctx, abst_name(e1), abst_domain(e1))); } else if (is_eq(e1) && is_eq(e2)) { - unify(eq_lhs(e1), eq_lhs(e2), ctx); - unify(eq_rhs(e1), eq_rhs(e2), ctx); + unify(eq_lhs(e1), eq_lhs(e2), ctx_size, ctx); + unify(eq_rhs(e1), eq_rhs(e2), ctx_size, ctx); } else { expr r1 = head_reduce(e1, m_env, m_available_definitions); expr r2 = head_reduce(e2, m_env, m_available_definitions); if (!is_eqp(e1, r1) || !is_eqp(e2, r2)) { - return unify(r1, r2, ctx); + return unify(r1, r2, ctx_size, ctx); } else if (is_app(e1) && is_app(e2) && num_args(e1) == num_args(e2)) { unsigned num = num_args(e1); for (unsigned i = 0; i < num; i++) { - unify(arg(e1, i), arg(e2, i), ctx); + unify(arg(e1, i), arg(e2, i), ctx_size, ctx); } } else if (is_simple_ho_match(e1, e2, ctx)) { - unify_simple_ho_match(e1, e2, ctx); + unify_simple_ho_match(e1, e2, ctx_size, ctx); } else if (is_simple_ho_match(e2, e1, ctx)) { - unify_simple_ho_match(e2, e1, ctx); + unify_simple_ho_match(e2, e1, ctx_size, ctx); } else { failed_to_unify(); } } } -void metavar_env::unify(expr const & e1, expr const & e2, context const & ctx) { +void metavar_env::unify(expr const & e1, expr const & e2, unsigned ctx_size, context const & ctx) { + lean_assert(ctx_size == length(ctx)); flet l(m_depth, m_depth+1); if (m_depth > m_max_depth) throw exception("unifier maximum recursion depth exceeded"); - expr const & r1 = root_at(e1, ctx); - expr const & r2 = root_at(e2, ctx); + expr const & r1 = root_at(e1, ctx_size); + expr const & r2 = root_at(e2, ctx_size); if (is_metavar(r1)) { - assign(r1, r2, ctx); + assign(r1, r2, ctx_size); } else { if (is_metavar(r2)) { - assign(r2, r1, ctx); + assign(r2, r1, ctx_size); } else { - unify_core(r1, r2, ctx); + unify_core(r1, r2, ctx_size, ctx); } } } -context const & metavar_env::get_context(expr const & m) { - lean_assert(is_metavar(m)); - return root_cell(m).m_context; +void metavar_env::unify(expr const & e1, expr const & e2, context const & ctx) { + unify(e1, e2, length(ctx), ctx); } void metavar_env::set_interrupt(bool flag) { @@ -477,8 +374,7 @@ void metavar_env::display(std::ostream & out) const { out << c.m_expr; else out << "[unassigned]"; - if (c.m_context) - out << ", " << c.m_context; + out << ", ctx_sz: " << c.m_ctx_size; out << "\n"; } } diff --git a/src/library/metavar_env.h b/src/library/metavar_env.h index 64d03ae2a..3e1d9319f 100644 --- a/src/library/metavar_env.h +++ b/src/library/metavar_env.h @@ -33,25 +33,11 @@ class metavar_env { enum class state { Unprocessed, Processing, Processed }; struct cell { expr m_expr; - context m_context; + unsigned m_ctx_size; // size of the context where the metavariable is defined unsigned m_find; unsigned m_rank; state m_state; - cell(expr const & e, context const & ctx, unsigned find); - /* - Basic properties for metavariable contexts: - 1) A metavariable does not occur in its own context. - - 2) If a metavariable ?m1 occurs in context ctx2 of - metavariable ?m2, then context ctx1 of ?m1 must be a prefix of ctx2. - This is by construction. - Here is an example: - (fun (A : Type) (?m1 : A) (?m2 : B), C) - The context of ?m1 is [A : Type] - The context of ?m2 is [A : Type, ?m1 : A] - - Remark: these conditions are not enforced by this module. - */ + cell(expr const & e, unsigned ctx_size, unsigned find); }; environment const & m_env; std::vector m_cells; @@ -70,22 +56,20 @@ class metavar_env { cell & root_cell(expr const & m); cell const & root_cell(expr const & m) const; unsigned new_rank(unsigned r1, unsigned r2); - void assign_term(expr const & m, expr s, context const & ctx); [[noreturn]] void failed_to_unify(); - void ensure_same_length(context & ctx1, context & ctx2); - void unify_ctx_prefix(context const & ctx1, context const & ctx2); - void unify_ctx_entries(context const & ctx1, context const & ctx2); bool is_simple_ho_match(expr const & e1, expr const & e2, context const & ctx); - void unify_simple_ho_match(expr const & e1, expr const & e2, context const & ctx); - void unify_core(expr const & e1, expr const & e2, context const & ctx); + void unify_simple_ho_match(expr const & e1, expr const & e2, unsigned ctx_size, context const & ctx); + void unify_core(expr const & e1, expr const & e2, unsigned ctx_size, context const & ctx); + void reduce_metavars_ctx_size(expr const & s, unsigned ctx_size); + void unify(expr const & e1, expr const & e2, unsigned ctx_size, context const & ctx); public: metavar_env(environment const & env, name_set const * available_defs, unsigned max_depth); metavar_env(environment const & env, name_set const * available_defs); metavar_env(environment const & env); - /** \brief Create a new meta-variable with the given context. */ - expr mk_metavar(context const & ctx = context()); + /** \brief Create a new meta-variable for a context of size ctx_sz. */ + expr mk_metavar(unsigned ctx_sz = 0); /** \brief Return true iff the given metavariable representative is @@ -102,28 +86,30 @@ public: If the the metavariable was defined in smaller context, we lift the free variables to match the size of the given context. */ - expr root_at(expr const & m, context const & ctx) const { return root_at(m, length(ctx)); } - /** - \brief Similar to the previous function, but the context is given. - */ expr root_at(expr const & m, unsigned ctx_size) const; - - /** - \brief If the given expression is a metavariable, then return the root - of the equivalence class. Otherwise, return itself. - */ - // expr const & root(expr const & e) const + expr root_at(expr const & m, context const & ctx) const { + return root_at(m, length(ctx)); + } /** \brief Assign m <- s + + \remark s is a term that occurs in a context of size \c + ctx_size. We need this information to adjust \c s to the + metavariable \c m, since \c m maybe was created in context of + different size, or was unified with another metavariable + created in a smaller context. + + \pre is_metavar(m) + */ - void assign(expr const & m, expr const & s, context const & ctx = context()); + void assign(expr const & m, expr const & s, unsigned ctx_size); /** \brief Replace the metavariables occurring in \c e with the substitutions in this metaenvironment. */ - expr instantiate_metavars(expr const & e, unsigned outer_offset = 0); + expr instantiate_metavars(expr const & e, unsigned ctx_size = 0); /** \brief Return true iff the given expression is an available @@ -145,14 +131,6 @@ public: */ void unify(expr const & e1, expr const & e2, context const & ctx = context()); - /** - \brief Return the context associated with the given - meta-variable. - - \pre is_metavar(m) - */ - context const & get_context(expr const & m); - /** \brief Clear/Reset the state. */ @@ -164,7 +142,6 @@ public: void set_interrupt(bool flag); void display(std::ostream & out) const; - bool check_invariant() const; }; } diff --git a/src/tests/library/implicit_args.cpp b/src/tests/library/implicit_args.cpp index d55bd0053..5c1c68e2c 100644 --- a/src/tests/library/implicit_args.cpp +++ b/src/tests/library/implicit_args.cpp @@ -44,7 +44,7 @@ static expr replace(expr const & e, context const & ctx, metavar_env & menv) { switch (e.kind()) { case expr_kind::Constant: if (is_placeholder(e)) { - return menv.mk_metavar(ctx); + return menv.mk_metavar(length(ctx)); } else { return e; } @@ -85,221 +85,6 @@ expr elaborate(expr const & e, environment const & env) { return elb(new_e); } -static void tst1() { - expr m1 = mk_metavar(0); - expr m2 = mk_metavar(1); - expr a = Const("a"); - expr f = Const("f"); - lean_assert(is_metavar(m1)); - lean_assert(!is_metavar(a)); - lean_assert(metavar_idx(m1) == 0); - lean_assert(metavar_idx(m2) == 1); - lean_assert(m1 != m2); - lean_assert(a != m1); - std::cout << m1 << " " << m2 << "\n"; - lean_assert(has_metavar(m1)); - lean_assert(has_metavar(f(f(f(m1))))); - lean_assert(!has_metavar(f(f(a)))); -} - -static void tst2() { - environment env; - metavar_env u(env); - expr m1 = u.mk_metavar(); - expr m2 = u.mk_metavar(); - expr m3 = u.mk_metavar(); - lean_assert(!u.is_assigned(m1)); - lean_assert(!u.is_assigned(m2)); - lean_assert(!u.is_assigned(m3)); - expr f = Const("f"); - expr t1 = f(m1, m2); - expr t2 = f(m1, m1); - lean_assert(t1 != t2); - // m1 <- m2 - u.assign(m1, m2); - std::cout << u << "\n"; - lean_assert(u.root_at(m2, 0) == m2); - lean_assert(u.root_at(m1, 0) == m2); - expr a = Const("a"); - expr b = Const("b"); - expr g = Const("g"); - expr t3 = f(a, m1); - expr t4 = f(m2, a); - expr t5 = f(a, a); - lean_assert(t3 != t4); - lean_assert(t4 != t5); - u.assign(m2, a); - u.assign(m3, b); - std::cout << u << "\n"; - expr m4 = u.mk_metavar(); - std::cout << u << "\n"; - u.assign(m4, m1); - std::cout << u << "\n"; - expr m5 = u.mk_metavar(); - expr m6 = u.mk_metavar(); - u.assign(m5, m6); - metavar_env u2(u); - u.assign(m5, m3); - std::cout << u << "\n"; - u2.assign(m5, m2); - std::cout << u2 << "\n"; -} - -static void tst3() { - environment env; - metavar_env uenv(env); - expr m1 = uenv.mk_metavar(); - expr f = Const("f"); - expr a = Const("a"); - expr b = Const("b"); - expr g = Const("g"); - expr m2 = uenv.mk_metavar(); - uenv.assign(m2, f(m1, a)); - uenv.assign(m1, b); - std::cout << uenv.instantiate_metavars(g(m2,b)) << "\n"; - lean_assert(uenv.instantiate_metavars(g(m2,b)) == g(f(b,a), b)); - lean_assert(uenv.instantiate_metavars(g(m2,f(a,m1))) == g(f(b,a),f(a,b))); - expr m3 = uenv.mk_metavar(); - expr m4 = uenv.mk_metavar(); - uenv.assign(m3, f(m4)); - try { - uenv.assign(m4, f(m3)); - lean_unreachable(); - } catch (exception) { - } -} - -static void tst4() { - environment env; - metavar_env uenv(env); - expr m1 = uenv.mk_metavar(); - expr m2 = uenv.mk_metavar(); - uenv.assign(m1, m2); - expr f = Const("f"); - expr a = Const("a"); - expr t = uenv.instantiate_metavars(f(m1,f(a, m1))); - std::cout << t << "\n"; - lean_assert(t == f(m2, f(a, m2))); -} - -static void tst5() { - environment env; - env.add_var("A", Type()); - env.add_var("B", Type()); - expr A = Const("A"); - expr B = Const("B"); - env.add_definition("F", Type(), A >> B); - env.add_definition("G", Type(), B >> B); - metavar_env uenv(env); - expr m1 = uenv.mk_metavar(); - expr m2 = uenv.mk_metavar(); - expr m3 = uenv.mk_metavar(); - expr m4 = uenv.mk_metavar(); - expr F = Const("F"); - expr G = Const("G"); - expr f = Const("f"); - expr g = Const("g"); - expr a = Const("a"); - expr b = Const("b"); - expr x = Const("x"); - expr Id = Fun({x, A}, x); - expr t1 = f(m1, g(a, F)); - expr t2 = f(g(a, b), Id(g(m2, m3 >> m4))); - metavar_env uenv2(uenv); - uenv2.unify(t1, t2); - std::cout << uenv2 << "\n"; - lean_assert(uenv2.root_at(m1,0) == g(a, b)); - lean_assert(uenv2.root_at(m2,0) == a); - lean_assert(uenv2.root_at(m3,0) == A); - lean_assert(uenv2.root_at(m4,0) == B); - lean_assert(uenv2.instantiate_metavars(t1) == f(g(a, b), g(a, F))); - lean_assert(uenv2.instantiate_metavars(t2) == f(g(a, b), Id(g(a, A >> B)))); - metavar_env uenv3(uenv); - expr t3 = f(m1, m1 >> m1); - expr t4 = f(m2 >> m2, m3); - uenv3.unify(t3, t4); - std::cout << uenv3 << "\n"; - uenv3.unify(m1, G); - std::cout << uenv3 << "\n"; - std::cout << uenv3.instantiate_metavars(t3) << "\n"; -} - -static void tst6() { - environment env; - env.add_var("A", Type()); - expr A = Const("A"); - expr f = Const("f"); - expr g = Const("g"); - expr a = Const("a"); - expr b = Const("b"); - context ctx1; - ctx1 = extend(extend(ctx1, "x", A >> A), "y", A); - metavar_env uenv(env); - expr m1 = uenv.mk_metavar(); - expr m2 = uenv.mk_metavar(ctx1); - context ctx2; - ctx2 = extend(ctx2, "x", m1); - expr m3 = uenv.mk_metavar(ctx2); - metavar_env uenv2(uenv); - expr t1 = f(m2, m3); - expr t2 = f(g(m3), Var(0)); - std::cout << "----------------\n"; - std::cout << uenv << "\n"; - uenv.unify(t1, t2, ctx2); - std::cout << uenv << "\n"; - std::cout << uenv.instantiate_metavars(t1,2) << "\n"; - std::cout << uenv.instantiate_metavars(t2,1) << "\n"; - lean_assert(uenv.instantiate_metavars(t1,2) == lift_free_vars(uenv.instantiate_metavars(t2,1),1)); - lean_assert(uenv.instantiate_metavars(t2,1) == f(g(Var(0)),Var(0))); - lean_assert(uenv.instantiate_metavars(m1) == A >> A); - expr t3 = f(m2); - expr t4 = f(m3); - uenv2.unify(t3, t4); - std::cout << "----------------\n"; - std::cout << uenv2 << "\n"; - lean_assert(uenv2.instantiate_metavars(m1) == A >> A); - lean_assert(length(uenv2.get_context(m2)) == length(uenv2.get_context(m3))); -} - -static void tst7() { - environment env; - env.add_var("A", Type()); - env.add_var("B", Type()); - expr A = Const("A"); - expr B = Const("B"); - env.add_definition("F", Type(), A >> B); - env.add_definition("G", Type(), B >> B); - name_set S; - S.insert("G"); - metavar_env uenv(env, &S); - expr m1 = uenv.mk_metavar(); - expr m2 = uenv.mk_metavar(); - expr m3 = uenv.mk_metavar(); - expr m4 = uenv.mk_metavar(); - expr F = Const("F"); - expr G = Const("G"); - expr f = Const("f"); - expr g = Const("g"); - expr a = Const("a"); - expr b = Const("b"); - expr x = Const("x"); - expr Id = Fun({x, A}, x); - expr t1 = f(m1, g(a, F)); - expr t2 = f(g(a, b), Id(g(m2, m3 >> m4))); - metavar_env uenv2(uenv); - try { - uenv2.unify(t1, t2); - lean_unreachable(); - } catch (exception) { - // It failed because "F" is not in the set of - // available definitions. - } - S.insert("F"); - uenv.unify(t1, t2); - std::cout << uenv.instantiate_metavars(t1) << "\n"; - std::cout << uenv.instantiate_metavars(t2) << "\n"; -} - // Check elaborator success static void success(expr const & e, expr const & expected, environment const & env) { std::cout << "\n" << e << "\n------>\n" << elaborate(e, env) << "\n"; @@ -322,7 +107,7 @@ static void unsolved(expr const & e, environment const & env) { lean_assert(has_metavar(elaborate(e, env))); } -static void tst8() { +static void tst1() { environment env; expr A = Const("A"); expr B = Const("B"); @@ -342,7 +127,7 @@ static void tst8() { success(F(_,_,Fun({a, Nat},a)), F(Nat,Nat,Fun({a,Nat},a)), env); } -static void tst9() { +static void tst2() { environment env = mk_toplevel(); expr a = Const("a"); expr b = Const("b"); @@ -367,7 +152,7 @@ static void tst9() { env); } -static void tst10() { +static void tst3() { environment env = mk_toplevel(); expr Nat = Const("Nat"); env.add_var("Nat", Type()); @@ -398,7 +183,7 @@ static void tst10() { success(Refl(_,a), Refl(Nat,a), env); } -static void tst11() { +static void tst4() { environment env; expr Nat = Const("Nat"); env.add_var("Nat", Type()); @@ -421,7 +206,7 @@ static void tst11() { Fun({{A,Type()},{x,Nat},{y,R >> Nat},{z,R >> Nat}}, Eq(f(x, y), f(x, z))), env); } -static void tst12() { +static void tst5() { environment env; expr A = Const("A"); expr B = Const("B"); @@ -438,7 +223,7 @@ static void tst12() { Fun({{a,Nat},{b,Nat}},g(f(Nat,a,b))), env); } -static void tst13() { +static void tst6() { environment env; expr lst = Const("list"); expr nil = Const("nil"); @@ -458,7 +243,7 @@ static void tst13() { Fun({a,N>>N}, f(cons(N>>N, a, cons(N>>N, a, nil(N>>N))))), env); } -static void tst14() { +static void tst7() { environment env; expr x = Const("x"); expr _ = mk_placholder(); @@ -466,7 +251,7 @@ static void tst14() { fails(omega, env); } -static void tst15() { +static void tst8() { environment env; expr B = Const("B"); expr A = Const("A"); @@ -474,13 +259,13 @@ static void tst15() { expr f = Const("f"); expr _ = mk_placholder(); env.add_var("f", Pi({B, Type()}, B >> B)); + success(Fun({{A,Type()}, {B,Type()}, {x,_}}, f(B, x)), + Fun({{A,Type()}, {B,Type()}, {x,B}}, f(B, x)), env); fails(Fun({{x,_}, {A,Type()}}, f(A, x)), env); success(Fun({{A,Type()}, {x,_}}, f(A, x)), Fun({{A,Type()}, {x,A}}, f(A, x)), env); success(Fun({{A,Type()}, {B,Type()}, {x,_}}, f(A, x)), Fun({{A,Type()}, {B,Type()}, {x,A}}, f(A, x)), env); - success(Fun({{A,Type()}, {B,Type()}, {x,_}}, f(B, x)), - Fun({{A,Type()}, {B,Type()}, {x,B}}, f(B, x)), env); success(Fun({{A,Type()}, {B,Type()}, {x,_}}, Eq(f(B, x), f(_,x))), Fun({{A,Type()}, {B,Type()}, {x,B}}, Eq(f(B, x), f(B,x))), env); success(Fun({{A,Type()}, {B,_}, {x,_}}, Eq(f(B, x), f(_,x))), @@ -488,7 +273,7 @@ static void tst15() { unsolved(Fun({{A,_}, {B,_}, {x,_}}, Eq(f(B, x), f(_,x))), env); } -static void tst16() { +static void tst9() { environment env = mk_toplevel(); expr A = Const("A"); expr B = Const("B"); @@ -528,7 +313,7 @@ static void tst16() { Fun({{x,N},{y,Bool}}, True))), env); } -static void tst17() { +static void tst10() { environment env = mk_toplevel(); expr A = Const("A"); expr B = Const("B"); @@ -554,7 +339,7 @@ static void tst17() { } -static void tst18() { +static void tst11() { environment env = mk_toplevel(); expr a = Const("a"); expr b = Const("b"); @@ -590,6 +375,20 @@ static void tst18() { env2); } +void tst12() { + environment env; + expr A = Const("A"); + expr B = Const("B"); + expr a = Const("a"); + expr b = Const("b"); + expr eq = Const("eq"); + expr _ = mk_placholder(); + env.add_var("eq", Pi({A, Type(level()+1)}, A >> (A >> Bool))); + success(eq(_, Fun({{A, Type()}, {a, _}}, a), Fun({{B, Type()}, {b, B}}, b)), + eq(Pi({A, Type()}, A >> A), Fun({{A, Type()}, {a, A}}, a), Fun({{B, Type()}, {b, B}}, b)), + env); +} + int main() { tst1(); tst2(); @@ -603,11 +402,5 @@ int main() { tst10(); tst11(); tst12(); - tst13(); - tst14(); - tst15(); - tst16(); - tst17(); - tst18(); return has_violations() ? 1 : 0; }