From 63e102055efb6dff83a3ee5b39c63b2d2f76c2d1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Sep 2013 18:25:38 -0700 Subject: [PATCH] Move metavariables to the kernel. This is the first step for implementing the new elaborator. Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 123 +++++-- src/frontends/lean/parser.cpp | 2 +- src/frontends/lean/pp.cpp | 74 +++-- src/kernel/CMakeLists.txt | 2 +- src/kernel/context.h | 4 +- src/kernel/expr.cpp | 35 +- src/kernel/expr.h | 130 +++++++- src/kernel/expr_eq.h | 10 + src/kernel/for_each.h | 3 +- src/kernel/free_vars.cpp | 35 +- src/kernel/free_vars.h | 11 +- src/kernel/instantiate.cpp | 41 ++- src/kernel/instantiate.h | 4 + src/kernel/metavar.cpp | 229 +++++++++++++ src/kernel/metavar.h | 186 +++++++++++ src/kernel/normalizer.cpp | 5 + src/kernel/replace.h | 3 +- src/kernel/type_checker.cpp | 5 + src/library/CMakeLists.txt | 4 +- src/library/deep_copy.cpp | 11 +- src/library/light_checker.cpp | 6 + src/library/max_sharing.cpp | 10 + src/library/metavar.cpp | 357 --------------------- src/library/metavar.h | 154 --------- src/library/placeholder.cpp | 23 ++ src/library/placeholder.h | 26 ++ src/library/printer.cpp | 137 ++++---- src/tests/frontends/lean/implicit_args.cpp | 2 +- src/tests/kernel/CMakeLists.txt | 9 +- src/tests/kernel/expr.cpp | 42 ++- src/tests/kernel/metavar.cpp | 235 ++++++++++++++ src/tests/kernel/normalizer.cpp | 3 +- src/tests/library/CMakeLists.txt | 3 - src/tests/library/metavar.cpp | 120 ------- src/util/list_fn.h | 28 ++ src/util/pvector.h | 1 + src/util/sexpr/format.cpp | 9 +- src/util/sexpr/format.h | 2 + tests/lean/elab1.lean.expected.out | 14 +- tests/lean/implicit1.lean.expected.out | 8 +- tests/lean/tst7.lean.expected.out | 4 +- 41 files changed, 1270 insertions(+), 840 deletions(-) create mode 100644 src/kernel/metavar.cpp create mode 100644 src/kernel/metavar.h delete mode 100644 src/library/metavar.cpp delete mode 100644 src/library/metavar.h create mode 100644 src/library/placeholder.cpp create mode 100644 src/library/placeholder.h create mode 100644 src/tests/kernel/metavar.cpp delete mode 100644 src/tests/library/metavar.cpp diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 1c28808726..cb5f66c11c 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -9,14 +9,18 @@ Author: Leonardo de Moura #include #include #include "util/flet.h" +#include "util/name_set.h" #include "kernel/normalizer.h" #include "kernel/context.h" #include "kernel/builtin.h" #include "kernel/free_vars.h" #include "kernel/for_each.h" #include "kernel/replace.h" -#include "library/metavar.h" +#include "kernel/instantiate.h" +#include "kernel/metavar.h" #include "library/printer.h" +#include "library/placeholder.h" +#include "library/reduce.h" #include "library/update_expr.h" #include "library/expr_pair.h" #include "frontends/lean/frontend.h" @@ -182,7 +186,7 @@ class elaborator::imp { context_entry const & def = p.first; context const & def_c = p.second; lean_assert(c.size() > def_c.size()); - return lift_free_vars_mmv(def.get_domain(), 0, c.size() - def_c.size()); + return lift_free_vars(def.get_domain(), 0, c.size() - def_c.size()); } expr check_pi(expr const & e, context const & ctx, expr const & s, context const & s_ctx) { @@ -190,7 +194,7 @@ class elaborator::imp { if (is_pi(e)) { return e; } else { - expr r = head_reduce_mmv(e, m_env, m_available_defs); + expr r = head_reduce(e, m_env, ctx, m_available_defs); if (!is_eqp(r, e)) { return check_pi(r, ctx, s, s_ctx); } else if (is_var(e)) { @@ -199,7 +203,7 @@ class elaborator::imp { context_entry const & entry = p.first; context const & entry_ctx = p.second; if (entry.get_body()) { - return lift_free_vars_mmv(check_pi(entry.get_body(), entry_ctx, s, s_ctx), 0, ctx.size() - entry_ctx.size()); + return lift_free_vars(check_pi(entry.get_body(), entry_ctx, s, s_ctx), 0, ctx.size() - entry_ctx.size()); } } catch (exception&) { // this can happen if we access a variable out of scope @@ -207,7 +211,7 @@ class elaborator::imp { } } else if (has_assigned_metavar(e)) { return check_pi(instantiate(e), ctx, s, s_ctx); - } else if (is_metavar(e)) { + } else if (is_metavar(e) && !has_context(e)) { // e is a unassigned metavariable that must be a Pi, // then we can assign it to (Pi x : A, B x), where // A and B are fresh metavariables @@ -234,7 +238,7 @@ class elaborator::imp { } else if (e == Bool) { return level(); } else { - expr r = head_reduce_mmv(e, m_env, m_available_defs); + expr r = head_reduce(e, m_env, ctx, m_available_defs); if (!is_eqp(r, e)) { return check_universe(r, ctx, s, s_ctx); } else if (is_var(e)) { @@ -288,7 +292,7 @@ class elaborator::imp { break; // failed } } - f_t = instantiate_free_var_mmv(abst_body(f_t), 0, args[i]); + f_t = ::lean::instantiate(abst_body(f_t), args[i]); } if (i == num_args) { if (num_coercions < best_num_coercions) { @@ -338,13 +342,13 @@ class elaborator::imp { expr_pair process(expr const & e, context const & ctx) { check_interrupted(m_interrupted); switch (e.kind()) { + case expr_kind::MetaVar: + return expr_pair(e, metavar_type(e)); case expr_kind::Constant: if (is_placeholder(e)) { expr m = mk_metavar(ctx); m_trace[m] = e; return expr_pair(m, metavar_type(m)); - } else if (is_metavar(e)) { - return expr_pair(e, metavar_type(e)); } else { return expr_pair(e, m_env.get_object(const_name(e)).get_type()); } @@ -410,7 +414,7 @@ class elaborator::imp { } } } - f_t = instantiate_free_var_mmv(abst_body(f_t), 0, args[i]); + f_t = ::lean::instantiate(abst_body(f_t), args[i]); } if (modified) { expr new_e = mk_app(args.size(), args.data()); @@ -466,7 +470,7 @@ class elaborator::imp { } } auto b_p = process(let_body(e), extend(ctx, let_name(e), t_p.first ? t_p.first : v_p.second, v_p.first)); - expr t = instantiate_free_var_mmv(b_p.second, 0, v_p.first); + expr t = ::lean::instantiate(b_p.second, v_p.first); expr new_e = update_let(e, t_p.first, v_p.first, b_p.first); add_trace(e, new_e); return expr_pair(new_e, t); @@ -480,7 +484,7 @@ class elaborator::imp { } bool is_simple_ho_match(expr const & e1, expr const & e2, context const & ctx) { - if (is_app(e1) && is_meta(arg(e1, 0)) && is_var(arg(e1, 1), 0) && num_args(e1) == 2 && !is_empty(ctx)) { + if (is_app(e1) && is_metavar(arg(e1, 0)) && is_var(arg(e1, 1), 0) && num_args(e1) == 2 && !empty(ctx)) { return true; } else { return false; @@ -491,8 +495,8 @@ class elaborator::imp { context const & ctx = c.m_ctx; context_entry const & head = ::lean::lookup(ctx, 0); m_constraints.push_back(constraint(arg(e1, 0), mk_lambda(head.get_name(), - lift_free_vars_mmv(head.get_domain(), 1, 1), - lift_free_vars_mmv(e2, 1, 1)), c)); + lift_free_vars(head.get_domain(), 1, 1), + lift_free_vars(e2, 1, 1)), c)); } struct cycle_detected {}; @@ -547,7 +551,7 @@ class elaborator::imp { } void solve_mvar(expr const & m, expr const & t, constraint const & c) { - lean_assert(is_metavar(m)); + lean_assert(is_metavar(m) && !has_context(m)); unsigned midx = metavar_idx(m); if (m_metavars[midx].m_assignment) { m_constraints.push_back(constraint(m_metavars[midx].m_assignment, t, c)); @@ -558,9 +562,72 @@ class elaborator::imp { } } + /** + \brief Temporary hack until we build the new elaborator. + */ + expr instantiate_metavar(expr const & e, unsigned midx, expr const & v) { + metavar_env menv; + while (!menv.contains(midx)) + menv.mk_metavar(); + menv.assign(midx, v); + return instantiate_metavars(e, menv); + } + + /** + \brief Temporary hack until we build the new elaborator. + */ + bool is_lower_lift_core(meta_entry_kind k, expr const & e, expr & c, unsigned & s, unsigned & n) { + if (!is_metavar(e) || !has_context(e)) + return false; + meta_ctx const & ctx = metavar_ctx(e); + meta_entry const & entry = head(ctx); + if (entry.kind() == k) { + c = ::lean::mk_metavar(metavar_idx(e), tail(ctx)); + add_trace(e, c); + s = entry.s(); + n = entry.n(); + return true; + } else { + return false; + } + } + + /** + \brief Temporary hack until we build the new elaborator. + */ + bool is_lower(expr const & e, expr & c, unsigned & s, unsigned & n) { + return is_lower_lift_core(meta_entry_kind::Lower, e, c, s, n); + } + + /** + \brief Temporary hack until we build the new elaborator. + */ + bool is_lift(expr const & e, expr & c, unsigned & s, unsigned & n) { + return is_lower_lift_core(meta_entry_kind::Lift, e, c, s, n); + } + + /** + \brief Temporary hack until we build the new elaborator. + */ + bool is_subst(expr const & e, expr & c, unsigned & s, expr & v) { + if (!is_metavar(e) || !has_context(e)) + return false; + meta_ctx const & ctx = metavar_ctx(e); + meta_entry const & entry = head(ctx); + if (entry.kind() == meta_entry_kind::Subst) { + c = ::lean::mk_metavar(metavar_idx(e), tail(ctx)); + add_trace(e, c); + s = entry.s(); + v = entry.v(); + return true; + } else { + return false; + } + } + bool solve_meta(expr const & e, expr const & t, constraint const & c) { - lean_assert(!is_metavar(e)); - expr const & m = get_metavar(e); + lean_assert(has_context(e)); + expr const & m = e; unsigned midx = metavar_idx(m); unsigned i, s, n; expr v, a, b; @@ -573,13 +640,13 @@ class elaborator::imp { if (!has_metavar(t)) { if (is_lower(e, a, s, n)) { - m_constraints.push_back(constraint(a, lift_free_vars_mmv(t, s-n, n), c)); + m_constraints.push_back(constraint(a, lift_free_vars(t, s-n, n), c)); return true; } if (is_lift(e, a, s, n)) { if (!has_free_var(t, s, s+n)) { - m_constraints.push_back(constraint(a, lower_free_vars_mmv(t, s+n, n), c)); + m_constraints.push_back(constraint(a, lower_free_vars(t, s+n, n), c)); return true; } else { // display(std::cout); @@ -620,16 +687,16 @@ class elaborator::imp { if (lhs == rhs || (!has_metavar(lhs) && !has_metavar(rhs))) { // do nothing delayed = 0; - } else if (is_metavar(lhs)) { + } else if (is_metavar(lhs) && !has_context(lhs)) { delayed = 0; solve_mvar(lhs, rhs, c); - } else if (is_metavar(rhs)) { + } else if (is_metavar(rhs) && !has_context(rhs)) { delayed = 0; solve_mvar(rhs, lhs, c); - } else if (is_meta(lhs) || is_meta(rhs)) { - if (is_meta(lhs) && solve_meta(lhs, rhs, c)) { + } else if (is_metavar(lhs) || is_metavar(rhs)) { + if (is_metavar(lhs) && solve_meta(lhs, rhs, c)) { delayed = 0; - } else if (is_meta(rhs) && solve_meta(rhs, lhs, c)) { + } else if (is_metavar(rhs) && solve_meta(rhs, lhs, c)) { delayed = 0; } else { m_constraints.push_back(c); @@ -654,8 +721,8 @@ class elaborator::imp { m_constraints.push_back(constraint(eq_lhs(lhs), eq_lhs(rhs), c)); m_constraints.push_back(constraint(eq_rhs(lhs), eq_rhs(rhs), c)); } else { - expr new_lhs = head_reduce_mmv(lhs, m_env, m_available_defs); - expr new_rhs = head_reduce_mmv(rhs, m_env, m_available_defs); + expr new_lhs = head_reduce(lhs, m_env, c.m_ctx, m_available_defs); + expr new_rhs = head_reduce(rhs, m_env, c.m_ctx, m_available_defs); if (!is_eqp(lhs, new_lhs) || !is_eqp(rhs, new_rhs)) { delayed = 0; m_constraints.push_back(constraint(new_lhs, new_rhs, c)); @@ -712,8 +779,8 @@ class elaborator::imp { expr instantiate(expr const & e) { auto proc = [&](expr const & n, unsigned offset) -> expr { - if (is_meta(n)) { - expr const & m = get_metavar(n); + if (is_metavar(n)) { + expr const & m = n; unsigned midx = metavar_idx(m); if (m_metavars[midx].m_assignment) { if (has_assigned_metavar(m_metavars[midx].m_assignment)) { diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 7b63311da4..baa66f9a0f 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -29,7 +29,7 @@ Author: Leonardo de Moura #include "library/printer.h" #include "library/state.h" #include "library/kernel_exception_formatter.h" -#include "library/metavar.h" +#include "library/placeholder.h" #include "frontends/lean/frontend.h" #include "frontends/lean/elaborator.h" #include "frontends/lean/elaborator_exception.h" diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index e567c99336..dd5faa171b 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -20,7 +20,7 @@ Author: Leonardo de Moura #include "kernel/builtin.h" #include "kernel/free_vars.h" #include "library/context_to_lambda.h" -#include "library/metavar.h" +#include "library/placeholder.h" #include "frontends/lean/notation.h" #include "frontends/lean/pp.h" #include "frontends/lean/frontend.h" @@ -78,7 +78,6 @@ static format g_lift_fmt = highlight_keyword(format("lift")); static format g_lower_fmt = highlight_keyword(format("lower")); static format g_subst_fmt = highlight_keyword(format("subst")); - static name g_pp_max_depth {"lean", "pp", "max_depth"}; static name g_pp_max_steps {"lean", "pp", "max_steps"}; static name g_pp_implicit {"lean", "pp", "implicit"}; @@ -184,6 +183,8 @@ class pp_fn { switch (e.kind()) { case expr_kind::Var: case expr_kind::Constant: case expr_kind::Value: case expr_kind::Type: return true; + case expr_kind::MetaVar: + return !metavar_ctx(e); case expr_kind::App: if (!m_coercion && is_coercion(e)) return is_atomic(arg(e, 1)); @@ -216,8 +217,6 @@ class pp_fn { name const & n = const_name(e); if (is_placeholder(e)) { return mk_result(format("_"), 1); - } else if (is_metavar(e)) { - return mk_result(format{format("?M"), format(metavar_idx(e))}, 1); } else if (has_implicit_arguments(n)) { return mk_result(format(m_frontend.get_explicit_version(n)), 1); } else { @@ -668,8 +667,8 @@ class pp_fn { } else { // standard function application expr const & f = app.get_function(); - result p = is_constant(f) && !is_metavar(f) ? mk_result(format(const_name(f)), 1) : pp_child(f, depth); - bool simple = is_constant(f) && !is_metavar(f) && const_name(f).size() <= m_indent + 4; + result p = is_constant(f) ? mk_result(format(const_name(f)), 1) : pp_child(f, depth); + bool simple = is_constant(f) && const_name(f).size() <= m_indent + 4; unsigned indent = simple ? const_name(f).size()+1 : m_indent; format r_format = p.first; unsigned r_weight = p.second; @@ -992,32 +991,6 @@ class pp_fn { return mk_result(r_format, p_arg1.second + p_arg2.second + 1); } - result pp_lower(expr const & e, unsigned depth) { - expr arg; unsigned s, n; - is_lower(e, arg, s, n); - result p_arg = pp_child(arg, depth); - format r_format = format{g_lower_fmt, colon(), format(s), colon(), format(n), nest(m_indent, compose(line(), p_arg.first))}; - return mk_result(r_format, p_arg.second + 1); - } - - result pp_lift(expr const & e, unsigned depth) { - expr arg; unsigned s, n; - is_lift(e, arg, s, n); - result p_arg = pp_child(arg, depth); - format r_format = format{g_lift_fmt, colon(), format(s), colon(), format(n), nest(m_indent, compose(line(), p_arg.first))}; - return mk_result(r_format, p_arg.second + 1); - } - - result pp_subst(expr const & e, unsigned depth) { - expr arg, v; unsigned i; - is_subst(e, arg, i, v); - result p_arg = pp_child(arg, depth); - result p_v = pp_child(v, depth); - format r_format = format{g_subst_fmt, colon(), format(i), - nest(m_indent, format{line(), p_arg.first, line(), p_v.first})}; - return mk_result(r_format, p_arg.second + p_v.second + 1); - } - result pp_choice(expr const & e, unsigned depth) { lean_assert(is_choice(e)); unsigned num = get_num_choices(e); @@ -1034,6 +1007,36 @@ class pp_fn { return mk_result(r_format, r_weight+1); } + result pp_metavar(expr const & a, unsigned depth) { + format mv_fmt = compose(format("?M"), format(metavar_idx(a))); + if (metavar_ctx(a)) { + format ctx_fmt; + bool first = true; + unsigned r_weight = 1; + for (meta_entry const & e : metavar_ctx(a)) { + format e_fmt; + switch (e.kind()) { + case meta_entry_kind::Lift: e_fmt = format{g_lift_fmt, colon(), format(e.s()), colon(), format(e.n())}; break; + case meta_entry_kind::Lower: e_fmt = format{g_lower_fmt, colon(), format(e.s()), colon(), format(e.n())}; break; + case meta_entry_kind::Subst: { + auto p_e = pp_child_with_paren(e.v(), depth); + r_weight += p_e.second; + e_fmt = format{g_subst_fmt, colon(), format(e.s()), space(), nest(m_indent, p_e.first)}; + break; + }} + if (first) { + ctx_fmt = e_fmt; + first = false; + } else { + ctx_fmt += compose(line(), e_fmt); + } + } + return mk_result(group(compose(mv_fmt, nest(m_indent, format{lsb(), ctx_fmt, rsb()}))), r_weight); + } else { + return mk_result(mv_fmt, 1); + } + } + result pp(expr const & e, unsigned depth, bool main = false) { check_interrupted(m_interrupted); if (!is_atomic(e) && (m_num_steps > m_max_steps || depth > m_max_depth)) { @@ -1048,12 +1051,6 @@ class pp_fn { result r; if (is_choice(e)) { return pp_choice(e, depth); - } else if (is_lower(e)) { - r = pp_lower(e, depth); - } else if (is_lift(e)) { - r = pp_lift(e, depth); - } else if (is_subst(e)) { - r = pp_subst(e, depth); } else { switch (e.kind()) { case expr_kind::Var: r = pp_var(e); break; @@ -1065,6 +1062,7 @@ class pp_fn { case expr_kind::Type: r = pp_type(e); break; case expr_kind::Eq: r = pp_eq(e, depth); break; case expr_kind::Let: r = pp_let(e, depth); break; + case expr_kind::MetaVar: r = pp_metavar(e, depth); break; } } if (!main && m_extra_lets && is_shared(e) && r.second > m_alias_min_weight) { diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index a9e9402cb1..41b3f4d8c2 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -1,5 +1,5 @@ add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp normalizer.cpp context.cpp level.cpp object.cpp environment.cpp - type_checker.cpp builtin.cpp occurs.cpp) + type_checker.cpp builtin.cpp occurs.cpp metavar.cpp) target_link_libraries(kernel ${LEAN_LIBS}) diff --git a/src/kernel/context.h b/src/kernel/context.h index cbca17583d..9f492ee31c 100644 --- a/src/kernel/context.h +++ b/src/kernel/context.h @@ -38,7 +38,7 @@ public: context(context const & c, name const & n, expr const & d, expr const & b):m_list(context_entry(n, d, b), c.m_list) {} context_entry const & lookup(unsigned vidx) const; std::pair lookup_ext(unsigned vidx) const; - bool is_empty() const { return is_nil(m_list); } + bool empty() const { return is_nil(m_list); } unsigned size() const { return length(m_list); } typedef list::iterator iterator; iterator begin() const { return m_list.begin(); } @@ -58,5 +58,5 @@ inline std::pair lookup_ext(context const & c, u inline context_entry const & lookup(context const & c, unsigned i) { return c.lookup(i); } inline context extend(context const & c, name const & n, expr const & d, expr const & b) { return context(c, n, d, b); } inline context extend(context const & c, name const & n, expr const & d) { return context(c, n, d); } -inline bool is_empty(context const & c) { return c.is_empty(); } +inline bool empty(context const & c) { return c.empty(); } } diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 507d1bfb05..53dd8b5dcf 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -13,6 +13,10 @@ Author: Leonardo de Moura #include "kernel/expr_eq.h" namespace lean { +meta_entry::meta_entry(meta_entry_kind k, unsigned s, unsigned n):m_kind(k), m_s(s), m_n(n) {} +meta_entry::meta_entry(unsigned s, expr const & v):m_kind(meta_entry_kind::Subst), m_s(s), m_v(v) {} +meta_entry::~meta_entry() {} + unsigned hash_args(unsigned size, expr const * args) { return hash(size, [&args](unsigned i){ return args[i].hash(); }); } @@ -24,22 +28,22 @@ expr const & expr::null() { return g_null; } -expr_cell::expr_cell(expr_kind k, unsigned h): +expr_cell::expr_cell(expr_kind k, unsigned h, bool has_mv): m_kind(static_cast(k)), - m_flags(0), + m_flags(has_mv ? 4 : 0), m_hash(h), m_rc(1) {} expr_var::expr_var(unsigned idx): - expr_cell(expr_kind::Var, idx), + expr_cell(expr_kind::Var, idx, false), m_vidx(idx) {} expr_const::expr_const(name const & n): - expr_cell(expr_kind::Constant, n.hash()), + expr_cell(expr_kind::Constant, n.hash(), false), m_name(n) {} -expr_app::expr_app(unsigned num_args): - expr_cell(expr_kind::App, 0), +expr_app::expr_app(unsigned num_args, bool has_mv): + expr_cell(expr_kind::App, 0, has_mv), m_num_args(num_args) { } expr_app::~expr_app() { @@ -51,6 +55,7 @@ expr mk_app(unsigned n, expr const * as) { unsigned new_n; unsigned n0 = 0; expr const & arg0 = as[0]; + bool has_mv = std::any_of(as, as + n, [](expr const & c) { return c.has_metavar(); }); // Remark: we represent ((app a b) c) as (app a b c) if (is_app(arg0)) { n0 = num_args(arg0); @@ -59,7 +64,7 @@ expr mk_app(unsigned n, expr const * as) { new_n = n; } char * mem = new char[sizeof(expr_app) + new_n*sizeof(expr)]; - expr r(new (mem) expr_app(new_n)); + expr r(new (mem) expr_app(new_n, has_mv)); expr * m_args = to_app(r)->m_args; unsigned i = 0; unsigned j = 0; @@ -76,13 +81,13 @@ expr mk_app(unsigned n, expr const * as) { return r; } expr_eq::expr_eq(expr const & lhs, expr const & rhs): - expr_cell(expr_kind::Eq, ::lean::hash(lhs.hash(), rhs.hash())), + expr_cell(expr_kind::Eq, ::lean::hash(lhs.hash(), rhs.hash()), lhs.has_metavar() || rhs.has_metavar()), m_lhs(lhs), m_rhs(rhs) { } expr_eq::~expr_eq() {} expr_abstraction::expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & b): - expr_cell(k, ::lean::hash(t.hash(), b.hash())), + expr_cell(k, ::lean::hash(t.hash(), b.hash()), t.has_metavar() || b.has_metavar()), m_name(n), m_domain(t), m_body(b) { @@ -90,12 +95,12 @@ expr_abstraction::expr_abstraction(expr_kind k, name const & n, expr const & t, expr_lambda::expr_lambda(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Lambda, n, t, e) {} expr_pi::expr_pi(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Pi, n, t, e) {} expr_type::expr_type(level const & l): - expr_cell(expr_kind::Type, l.hash()), + expr_cell(expr_kind::Type, l.hash(), false), m_level(l) { } expr_type::~expr_type() {} expr_let::expr_let(name const & n, expr const & t, expr const & v, expr const & b): - expr_cell(expr_kind::Let, ::lean::hash(v.hash(), b.hash())), + expr_cell(expr_kind::Let, ::lean::hash(v.hash(), b.hash()), v.has_metavar() || b.has_metavar() || (t && t.has_metavar())), m_name(n), m_type(t), m_value(v), @@ -110,13 +115,17 @@ format value::pp() const { return format(get_name()); } format value::pp(bool unicode) const { return unicode ? format(get_unicode_name()) : pp(); } unsigned value::hash() const { return get_name().hash(); } expr_value::expr_value(value & v): - expr_cell(expr_kind::Value, v.hash()), + expr_cell(expr_kind::Value, v.hash(), false), m_val(v) { m_val.inc_ref(); } expr_value::~expr_value() { m_val.dec_ref(); } +expr_metavar::expr_metavar(unsigned i, meta_ctx const & c): + expr_cell(expr_kind::MetaVar, i, true), + m_midx(i), m_ctx(c) {} +expr_metavar::~expr_metavar() {} void expr_cell::dealloc() { switch (kind()) { @@ -129,6 +138,7 @@ void expr_cell::dealloc() { case expr_kind::Type: delete static_cast(this); break; case expr_kind::Value: delete static_cast(this); break; case expr_kind::Let: delete static_cast(this); break; + case expr_kind::MetaVar: delete static_cast(this); break; } } @@ -156,6 +166,7 @@ expr copy(expr const & a) { case expr_kind::Lambda: return mk_lambda(abst_name(a), abst_domain(a), abst_body(a)); case expr_kind::Pi: return mk_pi(abst_name(a), abst_domain(a), abst_body(a)); case expr_kind::Let: return mk_let(let_name(a), let_type(a), let_value(a), let_body(a)); + case expr_kind::MetaVar: return mk_metavar(metavar_idx(a), metavar_ctx(a)); } lean_unreachable(); return expr(); diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 88fcb9027e..ac3d2fd513 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "util/name.h" #include "util/hash.h" #include "util/buffer.h" +#include "util/list_fn.h" #include "util/sexpr/format.h" #include "kernel/level.h" @@ -30,6 +31,13 @@ class value; | Type universe | Eq expr expr (heterogeneous equality) | Let name expr expr expr + | Metavar idx meta_ctx + + meta_ctx ::= [meta_entry] + + meta_entry ::= lift idx idx + | lower idx idx + | subst idx expr TODO(Leo): match expressions. @@ -39,7 +47,13 @@ The main API is divided in the following sections - Accessors - Miscellaneous ======================================= */ -enum class expr_kind { Var, Constant, Value, App, Lambda, Pi, Type, Eq, Let }; +enum class expr_kind { Var, Constant, Value, App, Lambda, Pi, Type, Eq, Let, MetaVar }; +class meta_entry; +/** + \brief A metavariable context is just a list of meta_entries. + \see meta_entry +*/ +typedef list meta_ctx; /** \brief Base class used to represent expressions. @@ -64,9 +78,10 @@ protected: void set_closed() { m_flags |= 2; } friend class has_free_var_fn; public: - expr_cell(expr_kind k, unsigned h); + expr_cell(expr_kind k, unsigned h, bool has_mv); expr_kind kind() const { return static_cast(m_kind); } unsigned hash() const { return m_hash; } + bool has_metavar() const { return (m_flags & 4) != 0; } }; /** \brief Exprs for encoding formulas/expressions, types and proofs. @@ -92,6 +107,7 @@ public: expr_kind kind() const { return m_ptr->kind(); } unsigned hash() const { return m_ptr ? m_ptr->hash() : 23; } + bool has_metavar() const { return m_ptr->has_metavar(); } expr_cell * raw() const { return m_ptr; } @@ -106,6 +122,7 @@ public: friend expr mk_pi(name const & n, expr const & t, expr const & e); friend expr mk_type(level const & l); friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & e); + friend expr mk_metavar(unsigned idx, meta_ctx const & ctx); friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; } @@ -141,7 +158,7 @@ class expr_app : public expr_cell { expr m_args[0]; friend expr mk_app(unsigned num_args, expr const * args); public: - expr_app(unsigned size); + expr_app(unsigned size, bool has_mv); ~expr_app(); unsigned get_num_args() const { return m_num_args; } expr const & get_arg(unsigned idx) const { lean_assert(idx < m_num_args); return m_args[idx]; } @@ -228,6 +245,78 @@ public: value const & get_value() const { return m_val; } }; +/** + \see meta_entry +*/ +enum class meta_entry_kind { Lift, Lower, Subst }; +/** + \brief An entry in a metavariable context. + It represents objects of the form: + + | Lift s n + | Lower s n + | Subst s v + + where \c s and \c n are unsigned integers, and + \c v is an expression + + The meaning of Lift s n is: lift the free variables greater than or equal to \c s by \c n. + The meaning of Lower s n is: lower the free variables greater than or equal to \c s by \c n. + The meaning of Subst s v is: substitute the free variable \c s with the expression \c v. + + The metavariable context records operations that must be applied + whenever we substitute a metavariable with an actual expression. + For example, let ?M be a metavariable with context + + [ Lower 1 1, Subst 0 a, Lift 1 2 ] + + Now, assume we want to instantiate \c ?M with f #0 (g #2). + Then, we apply the metavariable entries from right to left. + Thus, first we apply (Lift 1 2) and obtain the term + + f #0 (g #4) + + Then, we apply (Subst 0 a) and produce + + f a (g #4) + + Finally, we apply (Lower 1 1) and get the final result + + f a (g #3) + +*/ +class meta_entry { + meta_entry_kind m_kind; + unsigned m_s; + unsigned m_n; + expr m_v; + meta_entry(meta_entry_kind k, unsigned s, unsigned n); + meta_entry(unsigned s, expr const & v); +public: + ~meta_entry(); + friend meta_entry mk_lift(unsigned s, unsigned n); + friend meta_entry mk_lower(unsigned s, unsigned n); + friend meta_entry mk_subst(unsigned s, expr const & v); + meta_entry_kind kind() const { return m_kind; } + bool is_subst() const { return kind() == meta_entry_kind::Subst; } + unsigned s() const { return m_s; } + unsigned n() const { lean_assert(kind() != meta_entry_kind::Subst); return m_n; } + expr const & v() const { lean_assert(kind() == meta_entry_kind::Subst); return m_v; } +}; +inline meta_entry mk_lift(unsigned s, unsigned n) { return meta_entry(meta_entry_kind::Lift, s, n); } +inline meta_entry mk_lower(unsigned s, unsigned n) { return meta_entry(meta_entry_kind::Lower, s, n); } +inline meta_entry mk_subst(unsigned s, expr const & v) { return meta_entry(s, v); } + +/** \brief Metavariables */ +class expr_metavar : public expr_cell { + unsigned m_midx; + meta_ctx m_ctx; +public: + expr_metavar(unsigned i, meta_ctx const & c); + ~expr_metavar(); + unsigned get_midx() const { return m_midx; } + meta_ctx const & get_ctx() const { return m_ctx; } +}; // ======================================= // ======================================= @@ -241,6 +330,7 @@ inline bool is_lambda(expr_cell * e) { return e->kind() == expr_kind::Lambd inline bool is_pi(expr_cell * e) { return e->kind() == expr_kind::Pi; } inline bool is_type(expr_cell * e) { return e->kind() == expr_kind::Type; } inline bool is_let(expr_cell * e) { return e->kind() == expr_kind::Let; } +inline bool is_metavar(expr_cell * e) { return e->kind() == expr_kind::MetaVar; } inline bool is_abstraction(expr_cell * e) { return is_lambda(e) || is_pi(e); } inline bool is_var(expr const & e) { return e.kind() == expr_kind::Var; } @@ -253,6 +343,7 @@ inline bool is_pi(expr const & e) { return e.kind() == expr_kind::Pi; } bool is_arrow(expr const & e); inline bool is_type(expr const & e) { return e.kind() == expr_kind::Type; } inline bool is_let(expr const & e) { return e.kind() == expr_kind::Let; } +inline bool is_metavar(expr const & e) { return e.kind() == expr_kind::MetaVar; } inline bool is_abstraction(expr const & e) { return is_lambda(e) || is_pi(e); } // ======================================= @@ -281,6 +372,7 @@ inline expr mk_type(level const & l) { return expr(new expr_type(l)); } expr mk_type(); inline expr Type(level const & l) { return mk_type(l); } inline expr Type() { return mk_type(); } +inline expr mk_metavar(unsigned idx, meta_ctx const & ctx = meta_ctx()) { return expr(new expr_metavar(idx, ctx)); } inline expr expr::operator()(expr const & a1) const { return mk_app({*this, a1}); } inline expr expr::operator()(expr const & a1, expr const & a2) const { return mk_app({*this, a1, a2}); } @@ -302,6 +394,7 @@ inline expr_lambda * to_lambda(expr_cell * e) { lean_assert(is_lambda( inline expr_pi * to_pi(expr_cell * e) { lean_assert(is_pi(e)); return static_cast(e); } inline expr_type * to_type(expr_cell * e) { lean_assert(is_type(e)); return static_cast(e); } inline expr_let * to_let(expr_cell * e) { lean_assert(is_let(e)); return static_cast(e); } +inline expr_metavar * to_metavar(expr_cell * e) { lean_assert(is_metavar(e)); return static_cast(e); } inline expr_var * to_var(expr const & e) { return to_var(e.raw()); } inline expr_const * to_constant(expr const & e) { return to_constant(e.raw()); } @@ -312,6 +405,8 @@ inline expr_lambda * to_lambda(expr const & e) { return to_lambda(e.ra inline expr_pi * to_pi(expr const & e) { return to_pi(e.raw()); } inline expr_let * to_let(expr const & e) { return to_let(e.raw()); } inline expr_type * to_type(expr const & e) { return to_type(e.raw()); } +inline expr_metavar * to_metavar(expr const & e) { return to_metavar(e.raw()); } + // ======================================= // ======================================= @@ -334,6 +429,8 @@ inline name const & let_name(expr_cell * e) { return to_let(e)->get inline expr const & let_value(expr_cell * e) { return to_let(e)->get_value(); } inline expr const & let_type(expr_cell * e) { return to_let(e)->get_type(); } inline expr const & let_body(expr_cell * e) { return to_let(e)->get_body(); } +inline unsigned metavar_idx(expr_cell * e) { return to_metavar(e)->get_midx(); } +inline meta_ctx const & metavar_ctx(expr_cell * e) { return to_metavar(e)->get_ctx(); } /** \brief Return the reference counter of the given expression. */ inline unsigned get_rc(expr const & e) { return e.raw()->get_rc(); } @@ -363,6 +460,10 @@ inline name const & let_name(expr const & e) { return to_let(e)->ge inline expr const & let_type(expr const & e) { return to_let(e)->get_type(); } inline expr const & let_value(expr const & e) { return to_let(e)->get_value(); } inline expr const & let_body(expr const & e) { return to_let(e)->get_body(); } +inline unsigned metavar_idx(expr const & e) { return to_metavar(e)->get_midx(); } +inline meta_ctx const & metavar_ctx(expr const & e) { return to_metavar(e)->get_ctx(); } + +inline bool has_metavar(expr const & e) { return e.has_metavar(); } // ======================================= // ======================================= @@ -478,5 +579,28 @@ template expr update_eq(expr const & e, F f) { else return e; } +template expr update_metavar(expr const & e, unsigned i, F f) { + buffer new_entries; + bool modified = (i != metavar_idx(e)); + for (meta_entry const & me : metavar_ctx(e)) { + meta_entry new_me = f(me); + if (new_me.kind() != me.kind() || new_me.s() != me.s()) { + modified = true; + } else if (new_me.is_subst()) { + if (!is_eqp(new_me.v(), me.v())) + modified = true; + } else if (new_me.n() != me.n()) { + modified = true; + } + new_entries.push_back(new_me); + } + if (modified) + return mk_metavar(i, to_list(new_entries.begin(), new_entries.end())); + else + return e; +} +template expr update_metavar(expr const & e, F f) { + return update_metavar(e, metavar_idx(e), f); +} // ======================================= } diff --git a/src/kernel/expr_eq.h b/src/kernel/expr_eq.h index b7327a852d..27fdec5b0f 100644 --- a/src/kernel/expr_eq.h +++ b/src/kernel/expr_eq.h @@ -63,6 +63,16 @@ class expr_eq_fn { return false; } return apply(let_value(a), let_value(b)) && apply(let_body(a), let_body(b)); + case expr_kind::MetaVar: + return metavar_idx(a) == metavar_idx(b) && + compare(metavar_ctx(a), metavar_ctx(b), [&](meta_entry const & e1, meta_entry const & e2) { + if (e1.kind() != e2.kind() || e1.s() != e2.s()) + return false; + if (e1.is_subst()) + return apply(e1.v(), e2.v()); + else + return e1.n() == e2.n(); + }); } lean_unreachable(); // LCOV_EXCL_LINE return false; // LCOV_EXCL_LINE diff --git a/src/kernel/for_each.h b/src/kernel/for_each.h index adc0573d90..15dbfb83a2 100644 --- a/src/kernel/for_each.h +++ b/src/kernel/for_each.h @@ -35,7 +35,8 @@ class for_each_fn { m_f(e, offset); switch (e.kind()) { - case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: + case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: + case expr_kind::Var: case expr_kind::MetaVar: return; case expr_kind::App: std::for_each(begin_args(e), end_args(e), [=](expr const & arg){ return apply(arg, offset); }); diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp index 3ab732ec32..e072bd6f2e 100644 --- a/src/kernel/free_vars.cpp +++ b/src/kernel/free_vars.cpp @@ -8,10 +8,15 @@ Author: Leonardo de Moura #include "kernel/free_vars.h" #include "kernel/expr_sets.h" #include "kernel/replace.h" +#include "kernel/metavar.h" namespace lean { +/** + \brief Functional object for checking whether a kernel expression has free variables or not. -/** \brief Functional object for checking whether a kernel expression has free variables or not. */ + \remark We assume that a metavariable contains free variables. + This is an approximation, since we don't know how the metavariable will be instantiated. +*/ class has_free_vars_fn { protected: expr_cell_offset_set m_cached; @@ -21,6 +26,8 @@ protected: switch (e.kind()) { case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: return false; + case expr_kind::MetaVar: + return true; case expr_kind::Var: return var_idx(e) >= offset; case expr_kind::App: case expr_kind::Eq: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: @@ -51,7 +58,7 @@ protected: bool result = false; switch (e.kind()) { - case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: + case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar: // easy cases were already handled lean_unreachable(); return false; case expr_kind::App: @@ -87,7 +94,12 @@ bool has_free_vars(expr const & e) { return has_free_vars_fn()(e); } -/** \brief Functional object for checking whether a kernel expression has a free variable in the range [low, high) or not. */ +/** + \brief Functional object for checking whether a kernel expression has a free variable in the range [low, high) or not. + + \remark We assume that a metavariable contains free variables. + This is an approximation, since we don't know how the metavariable will be instantiated. +*/ class has_free_var_in_range_fn { protected: unsigned m_low; @@ -99,6 +111,8 @@ protected: switch (e.kind()) { case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: return false; + case expr_kind::MetaVar: + return true; case expr_kind::Var: return var_idx(e) >= offset + m_low && var_idx(e) < offset + m_high; case expr_kind::App: case expr_kind::Eq: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: @@ -119,7 +133,7 @@ protected: bool result = false; switch (e.kind()) { - case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: + case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar: // easy cases were already handled lean_unreachable(); return false; case expr_kind::App: @@ -160,13 +174,14 @@ bool has_free_var(expr const & e, unsigned low, unsigned high) { return has_free_var_in_range_fn(low, high)(e); } -expr lower_free_vars(expr const & e, unsigned d) { +expr lower_free_vars(expr const & e, unsigned s, unsigned d) { lean_assert(d > 0); - lean_assert(!has_free_var(e, 0, d)); auto f = [=](expr const & e, unsigned offset) -> expr { - if (is_var(e) && var_idx(e) >= offset) { + if (is_var(e) && var_idx(e) >= s + offset) { lean_assert(var_idx(e) >= offset + d); return mk_var(var_idx(e) - d); + } else if (is_metavar(e)) { + return add_lower(e, s + offset, d); } else { return e; } @@ -174,12 +189,14 @@ expr lower_free_vars(expr const & e, unsigned d) { return replace_fn(f)(e); } -expr lift_free_vars(expr const & e, unsigned d) { +expr lift_free_vars(expr const & e, unsigned s, unsigned d) { if (d == 0) return e; auto f = [=](expr const & e, unsigned offset) -> expr { - if (is_var(e) && var_idx(e) >= offset) { + if (is_var(e) && var_idx(e) >= s + offset) { return mk_var(var_idx(e) + d); + } else if (is_metavar(e)) { + return add_lift(e, s + offset, d); } else { return e; } diff --git a/src/kernel/free_vars.h b/src/kernel/free_vars.h index 95471fdbfe..14bd3d64ca 100644 --- a/src/kernel/free_vars.h +++ b/src/kernel/free_vars.h @@ -28,15 +28,18 @@ bool has_free_var(expr const & e, unsigned i); bool has_free_var(expr const & e, unsigned low, unsigned high); /** - \brief Lower the free variables in \c e by d. That is, a free variable (var i) is mapped into (var i-d). + \brief Lower the free variables >= s in \c e by d. That is, a free variable (var i) s.t. + i >= s is mapped into (var i-d). \pre d > 0 \pre !has_free_var(e, 0, d) */ -expr lower_free_vars(expr const & e, unsigned d); +expr lower_free_vars(expr const & e, unsigned s, unsigned d); +inline expr lower_free_vars(expr const & e, unsigned d) { return lower_free_vars(e, 0, d); } /** - \brief Lift free variables in \c e by d. + \brief Lift free variables >= s in \c e by d. */ -expr lift_free_vars(expr const & e, unsigned d); +expr lift_free_vars(expr const & e, unsigned s, unsigned d); +inline expr lift_free_vars(expr const & e, unsigned d) { return lift_free_vars(e, 0, d); } } diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index 3ab414fd27..5d8f5e3dd7 100644 --- a/src/kernel/instantiate.cpp +++ b/src/kernel/instantiate.cpp @@ -7,38 +7,55 @@ Author: Leonardo de Moura #include #include "kernel/free_vars.h" #include "kernel/replace.h" +#include "kernel/metavar.h" namespace lean { -expr instantiate_with_closed(expr const & e, unsigned n, expr const * s) { +expr instantiate_with_closed(expr const & a, unsigned n, expr const * s) { lean_assert(std::all_of(s, s+n, closed)); - auto f = [=](expr const & e, unsigned offset) -> expr { - if (is_var(e)) { - unsigned vidx = var_idx(e); + auto f = [=](expr const & m, unsigned offset) -> expr { + if (is_var(m)) { + unsigned vidx = var_idx(m); if (vidx >= offset) { if (vidx < offset + n) return s[n - (vidx - offset) - 1]; else return mk_var(vidx - n); + } else { + return m; } + } else if (is_metavar(m)) { + expr r = m; + for (unsigned i = 0; i < n; i++) + r = add_subst(r, offset + i, s[n - i - 1]); + return add_lower(r, offset + n, n); + } else { + return m; } - return e; }; - return replace_fn(f)(e); + return replace_fn(f)(a); } -expr instantiate(expr const & e, unsigned n, expr const * s) { - auto f = [=](expr const & e, unsigned offset) -> expr { - if (is_var(e)) { - unsigned vidx = var_idx(e); +expr instantiate(expr const & a, unsigned n, expr const * s) { + auto f = [=](expr const & m, unsigned offset) -> expr { + if (is_var(m)) { + unsigned vidx = var_idx(m); if (vidx >= offset) { if (vidx < offset + n) return lift_free_vars(s[n - (vidx - offset) - 1], offset); else return mk_var(vidx - n); + } else { + return m; } + } else if (is_metavar(m)) { + expr r = m; + for (unsigned i = 0; i < n; i++) + r = add_subst(r, offset + i, lift_free_vars(s[n - i - 1], offset + n)); + return add_lower(r, offset + n, n); + } else { + return m; } - return e; }; - return replace_fn(f)(e); + return replace_fn(f)(a); } } diff --git a/src/kernel/instantiate.h b/src/kernel/instantiate.h index 0ac9a20a4b..ba031bf1c6 100644 --- a/src/kernel/instantiate.h +++ b/src/kernel/instantiate.h @@ -14,11 +14,15 @@ namespace lean { \pre s[0], ..., s[n-1] must be closed expressions (i.e., no free variables). */ expr instantiate_with_closed(expr const & e, unsigned n, expr const * s); +inline expr instantiate_with_closed(expr const & e, std::initializer_list const & l) { + return instantiate_with_closed(e, l.size(), l.begin()); +} inline expr instantiate_with_closed(expr const & e, expr const & s) { return instantiate_with_closed(e, 1, &s); } /** \brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e. */ expr instantiate(expr const & e, unsigned n, expr const * s); +inline expr instantiate(expr const & e, std::initializer_list const & l) { return instantiate(e, l.size(), l.begin()); } inline expr instantiate(expr const & e, expr const & s) { return instantiate(e, 1, &s); } } diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp new file mode 100644 index 0000000000..cc2aac3848 --- /dev/null +++ b/src/kernel/metavar.cpp @@ -0,0 +1,229 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "kernel/metavar.h" +#include "kernel/replace.h" +#include "kernel/free_vars.h" +#include "kernel/occurs.h" +#include "kernel/for_each.h" + +namespace lean { +expr metavar_env::mk_metavar() { + unsigned midx = m_env.size(); + m_env.push_back(mk_pair(expr(), expr())); + return ::lean::mk_metavar(midx); +} + +bool metavar_env::contains(unsigned midx) const { + return midx < m_env.size(); +} + +bool metavar_env::is_assigned(unsigned midx) const { + return m_env[midx].first; +} + +expr metavar_env::get_subst(unsigned midx) const { + return m_env[midx].first; +} + +expr metavar_env::get_type(unsigned midx, unification_problems & up) { + auto p = m_env[midx]; + expr t = p->second; + if (t) { + return t; + } else { + t = mk_metavar(); + expr s = p->first; + m_env[midx] = mk_pair(s, t); + if (s) + up.add_type_of_eq(s, t); + else + up.add_type_of_eq(::lean::mk_metavar(midx), t); + return t; + } +} + +void metavar_env::assign(unsigned midx, expr const & t) { + lean_assert(!is_assigned(midx)); + auto p = m_env[midx]; + m_env[midx] = mk_pair(t, p->second); +} + +expr subst(expr const & a, unsigned i, expr const & c) { + auto f = [&](expr const & e, unsigned offset) -> expr { + if (is_var(e)) { + unsigned vidx = var_idx(e); + if (vidx == offset + i) + return lift_free_vars(c, 0, offset); + else + return e; + } else if (is_metavar(e)) { + return add_subst(e, offset, lift_free_vars(c, 0, offset)); + } else { + return e; + } + }; + return replace_fn(f)(a); +} + +expr instantiate(expr const & s, meta_ctx const & ctx, metavar_env const & env) { + if (ctx) { + expr r = instantiate(s, tail(ctx), env); + meta_entry const & e = head(ctx); + switch (e.kind()) { + case meta_entry_kind::Lift: return lift_free_vars(r, e.s(), e.n()); + case meta_entry_kind::Lower: return lower_free_vars(r, e.s(), e.n()); + case meta_entry_kind::Subst: return subst(r, e.s(), instantiate_metavars(e.v(), env)); + } + lean_unreachable(); + return s; + } else { + return s; + } +} + +expr metavar_env::get_subst(expr const & m) const { + expr s = get_subst(metavar_idx(m)); + if (s) + return instantiate(s, metavar_ctx(m), *this); + else + return s; +} + +expr metavar_env::get_type(expr const & m, unification_problems & up) { + expr s = get_type(metavar_idx(m), up); + lean_assert(is_metavar(s)); + lean_assert(!metavar_ctx(s)); + meta_ctx const & ctx = metavar_ctx(m); + if (ctx) + return ::lean::mk_metavar(metavar_idx(s), ctx); + else + return s; +} + +void metavar_env::assign(expr const & m, expr const & t) { + lean_assert(!metavar_ctx(m)); + assign(metavar_idx(m), t); +} + +expr instantiate_metavars(expr const & e, metavar_env const & env) { + auto f = [=](expr const & m, unsigned offset) -> expr { + if (is_metavar(m) && env.contains(m)) { + expr s = env.get_subst(m); + return s ? s : m; + } else { + return m; + } + }; + return replace_fn(f)(e); +} + +expr add_lift(expr const & m, unsigned s, unsigned n) { + return mk_metavar(metavar_idx(m), cons(mk_lift(s, n), metavar_ctx(m))); +} + +meta_ctx add_lower(meta_ctx const & ctx, unsigned s2, unsigned n2) { + if (ctx) { + meta_entry e = head(ctx); + unsigned s1, n1; + switch (e.kind()) { + case meta_entry_kind::Lift: + s1 = e.s(); + n1 = e.n(); + if (s1 <= s2 && s2 <= s1 + n1) { + if (n1 == n2) + return tail(ctx); + else if (n1 > n2) + return cons(mk_lift(s1, n1 - n2), tail(ctx)); + } + break; + case meta_entry_kind::Lower: + s1 = e.s(); + n1 = e.n(); + if (s2 == s1 - n1) + return add_lower(tail(ctx), s1, n1 + n2); + break; + case meta_entry_kind::Subst: + break; + } + } + return cons(mk_lower(s2, n2), ctx); +} + +expr add_lower(expr const & m, unsigned s, unsigned n) { + return mk_metavar(metavar_idx(m), add_lower(metavar_ctx(m), s, n)); +} + +meta_ctx add_subst(meta_ctx const & ctx, unsigned s, expr const & v) { + if (ctx) { + meta_entry e = head(ctx); + switch (e.kind()) { + case meta_entry_kind::Subst: + return cons(mk_subst(s, v), ctx); + case meta_entry_kind::Lower: + if (s >= e.s()) + return cons(e, add_subst(tail(ctx), s + e.n(), lift_free_vars(v, e.s(), e.n()))); + else + return cons(e, add_subst(tail(ctx), s, lift_free_vars(v, e.s(), e.n()))); + case meta_entry_kind::Lift: + if (e.s() <= s && s < e.s() + e.n()) { + return ctx; + } else if (s < e.s() && !has_free_var(v, e.s(), std::numeric_limits::max())) { + return cons(e, add_subst(tail(ctx), s, v)); + } else if (s >= e.s() + e.n() && !has_free_var(v, e.s(), std::numeric_limits::max())) { + return cons(e, add_subst(tail(ctx), s - e.n(), v)); + } else { + return cons(mk_subst(s, v), ctx); + } + } + lean_unreachable(); + return ctx; + } else { + return cons(mk_subst(s, v), ctx); + } +} + +expr add_subst(expr const & m, unsigned s, expr const & v) { + return mk_metavar(metavar_idx(m), add_subst(metavar_ctx(m), s, v)); +} + +bool has_context(expr const & m) { + return metavar_ctx(m); +} + +expr pop_context(expr const & m) { + lean_assert(has_context(m)); + return mk_metavar(metavar_idx(m), tail(metavar_ctx(m))); +} + +/** + \brief Auxiliary exception used to sign that a metavariable was + found in an expression. +*/ +struct found_metavar {}; + +bool has_metavar(expr const & e, unsigned midx, metavar_env const & menv) { + auto f = [&](expr const & m, unsigned offset) { + if (is_metavar(m)) { + unsigned midx2 = metavar_idx(m); + if (midx2 == midx) + throw found_metavar(); + if (menv.contains(midx2) && + menv.is_assigned(midx2) && + has_metavar(menv.get_subst(midx2), midx, menv)) + throw found_metavar(); + } + }; + try { + for_each_fn proc(f); + proc(e); + return false; + } catch (found_metavar) { + return true; + } +} +} diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h new file mode 100644 index 0000000000..b7b508d3ad --- /dev/null +++ b/src/kernel/metavar.h @@ -0,0 +1,186 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include +#include "util/pair.h" +#include "util/pvector.h" +#include "kernel/expr.h" + +namespace lean { +/** + \brief Set of unification problems that need to be solved. + It store two kinds of problems: + 1. lhs == rhs + 2. typeof(n) == t +*/ +class unification_problems { + std::vector> m_eqs; + std::vector> m_type_of_eqs; +public: + /** + \brief Add a new unification problem of the form lhs == rhs + */ + void add_eq(expr const & lhs, expr const & rhs) { m_eqs.push_back(mk_pair(lhs, rhs)); } + + /** + \brief Add a new unification problem of the form typeof(n) == t + */ + void add_type_of_eq(expr const & n, expr const & t) { m_type_of_eqs.push_back(mk_pair(n, t)); } + + std::vector> const & eqs() const { return m_eqs; } + std::vector> const & type_of_eqs() const { return m_type_of_eqs; } +}; + +/** + \brief Metavariable environment. It is essentially a mapping + from metavariables to assignments and types. +*/ +class metavar_env { + pvector> m_env; +public: + /** + \brief Create new metavariable in this environment. + */ + expr mk_metavar(); + + /** + \brief Return true if this environment contains a metavariable + with id \c midx. That is, it has an entry of the form + midx -> (s, t). + */ + bool contains(unsigned midx) const; + + /** + \brief Return true if the metavariable with id \c midx is assigned in + this environment. + + \pre contains(midx) + */ + bool is_assigned(unsigned midx) const; + + /** + \brief Return the substitution associated with the metavariable with id \c midx + in this environment. + If the metavariable is not assigned in this environment, then it returns the null + expression. + + \pre contains(midx) + */ + expr get_subst(unsigned midx) const; + + /** + \brief Return the type of the metavariable with id \c midx in this environment. + + \remark A new metavariable may be created to represent the type of the input + metavariable. When this happens, a new unification problem of the form + typeof(m) = t is added to \c up, where \c m is the metavariable + with id \c midx, and \c t is the result of this method. + + \pre contains(midx) + */ + expr get_type(unsigned midx, unification_problems & up); + + /** + \brief Assign the metavariable with id \c midx to the term \c t. + + \pre !is_assigned(midx) + */ + void assign(unsigned midx, expr const & t); + + /** + \brief Return true if this environment contains the given metavariable + + \pre is_metavar(m) + */ + bool contains(expr const & m) const { return contains(metavar_idx(m)); } + + /** + \pre contains(m) + */ + bool is_assigned(expr const & m) const { return is_assigned(metavar_idx(m)); } + + /** + \brief Return the substitution associated with the metavariable \c m. + If \c m has a context ctx associated with it, then the substitution is + 'moved' to ctx. + + \pre contains(m) + */ + expr get_subst(expr const & m) const; + + /** + \brief Return the type of the given metavariable. + If \c m has a context ctx associated with it, then the type is + 'moved' to ctx. + + \pre contains(m) + */ + expr get_type(expr const & m, unification_problems & up); + + /** + \brief Assign the metavariable \c m to \c t. + The metavariable must not have a context associated with it. + + \pre contains(m) + \pre !metavar_ctx(m) + \pre !is_assigned(m) + */ + void assign(expr const & m, expr const & t); +}; + +/** + \brief Instantiate the metavariables occurring in \c e with the substitutions + provided by \c env. +*/ +expr instantiate_metavars(expr const & e, metavar_env const & env); + +/** + \brief Add a lift:s:n operation to the context of the given metavariable. + + \pre is_metavar(m) +*/ +expr add_lift(expr const & m, unsigned s, unsigned n); + +/** + \brief Add a lower:s:n operation to the context of the given metavariable. + + \pre is_metavar(m) + \pre n <= s +*/ +expr add_lower(expr const & m, unsigned s, unsigned n); + +/** + \brief Add a subst:s:v operation to the context of the given metavariable. + + \pre is_metavar(m) + \pre !occurs(m, v) +*/ +expr add_subst(expr const & m, unsigned s, expr const & v); + +/** + \brief Return true iff the given metavariable has a non-empty + context associated with it. + + \pre is_metavar(m) +*/ +bool has_context(expr const & m); + +/** + \brief Return the same metavariable, but the head of the context is removed. + + \pre is_metavar(m) + \pre has_context(m) +*/ +expr pop_context(expr const & m); + +/** + \brief Return true iff \c e contains the metavariable with index \c midx. + The substitutions in \c menv are taken into account. +*/ +bool has_metavar(expr const & e, unsigned midx, metavar_env const & menv = metavar_env()); +} diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index f4ffab6500..d26b5990fc 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -142,6 +142,11 @@ class normalizer::imp { svalue r; switch (a.kind()) { + case expr_kind::MetaVar: + // TODO(Leo) The following code should be unreachable in the current implementation. + // It will be needed when we implement the new elaborator. + lean_unreachable(); + return svalue(a); case expr_kind::Var: r = lookup(s, var_idx(a), k); break; diff --git a/src/kernel/replace.h b/src/kernel/replace.h index 3e66e68a59..b64d37f7fc 100644 --- a/src/kernel/replace.h +++ b/src/kernel/replace.h @@ -53,7 +53,8 @@ class replace_fn { expr r = m_f(e, offset); if (is_eqp(e, r)) { switch (e.kind()) { - case expr_kind::Type: case expr_kind::Value: case expr_kind::Constant: case expr_kind::Var: + case expr_kind::Type: case expr_kind::Value: case expr_kind::Constant: + case expr_kind::Var: case expr_kind::MetaVar: break; case expr_kind::App: r = update_app(e, [=](expr const & c) { return apply(c, offset); }); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 0f8e5dcc54..589585dbe9 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -68,6 +68,11 @@ public: expr r; switch (e.kind()) { + case expr_kind::MetaVar: + // TODO(Leo) The following code should be unreachable in the current implementation. + // It will be needed when we implement the new elaborator. + lean_unreachable(); + return e; case expr_kind::Constant: r = m_env.get_object(const_name(e)).get_type(); break; diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 2d93a17858..dd3aeabba4 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -1,5 +1,5 @@ add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp printer.cpp formatter.cpp context_to_lambda.cpp - state.cpp metavar.cpp update_expr.cpp kernel_exception_formatter.cpp - reduce.cpp light_checker.cpp) + state.cpp update_expr.cpp kernel_exception_formatter.cpp + reduce.cpp light_checker.cpp placeholder.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/deep_copy.cpp b/src/library/deep_copy.cpp index c787293d73..cdfc944db1 100644 --- a/src/library/deep_copy.cpp +++ b/src/library/deep_copy.cpp @@ -37,8 +37,17 @@ class deep_copy_fn { case expr_kind::Pi: r = mk_pi(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))); break; case expr_kind::Let: { expr new_t = let_type(a) ? apply(let_type(a)) : expr(); - r = mk_let(let_name(a), new_t, apply(let_value(a)), apply(let_body(a))); break; + r = mk_let(let_name(a), new_t, apply(let_value(a)), apply(let_body(a))); + break; } + case expr_kind::MetaVar: + r = update_metavar(a, [&](meta_entry const & e) -> meta_entry { + if (e.is_subst()) + return mk_subst(e.s(), apply(e.v())); + else + return e; + }); + break; } if (sh) m_cache.insert(std::make_pair(a.raw(), r)); diff --git a/src/library/light_checker.cpp b/src/library/light_checker.cpp index 385366fdf3..9ff028e754 100644 --- a/src/library/light_checker.cpp +++ b/src/library/light_checker.cpp @@ -63,6 +63,11 @@ public: expr infer_type(expr const & e, context const & ctx) { // cheap cases, we do not cache results switch (e.kind()) { + case expr_kind::MetaVar: + // TODO(Leo) The following code should be unreachable in the current implementation. + // It will be needed when we implement the new elaborator. + lean_unreachable(); + return e; case expr_kind::Constant: { object const & obj = m_env.get_object(const_name(e)); if (obj.has_type()) @@ -103,6 +108,7 @@ public: switch (e.kind()) { case expr_kind::Constant: case expr_kind::Eq: case expr_kind::Value: case expr_kind::Type: + case expr_kind::MetaVar: lean_unreachable(); break; case expr_kind::Var: { diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp index 212bdbc473..e68361a5fd 100644 --- a/src/library/max_sharing.cpp +++ b/src/library/max_sharing.cpp @@ -61,6 +61,16 @@ struct max_sharing_fn::imp { }); cache(r); return r; + } + case expr_kind::MetaVar: { + expr r = update_metavar(a, [=](meta_entry const & e) -> meta_entry { + if (e.is_subst()) + return mk_subst(e.s(), apply(e.v())); + else + return e; + }); + cache(r); + return r; }} lean_unreachable(); return a; diff --git a/src/library/metavar.cpp b/src/library/metavar.cpp deleted file mode 100644 index 9ec570f846..0000000000 --- a/src/library/metavar.cpp +++ /dev/null @@ -1,357 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "kernel/replace.h" -#include "kernel/for_each.h" -#include "kernel/environment.h" -#include "kernel/occurs.h" -#include "library/update_expr.h" -#include "library/printer.h" -#include "library/metavar.h" - -namespace lean { -static name g_placeholder_name("_"); -static name g_metavar_prefix(name(name(name(0u), "library"), "metavar")); -static name g_subst_prefix(name(name(name(0u), "library"), "subst")); -static name g_lift_prefix(name(name(name(0u), "library"), "lift")); -static name g_lower_prefix(name(name(name(0u), "library"), "lower")); - -expr mk_placholder() { - return mk_constant(g_placeholder_name); -} - -bool is_placeholder(expr const & e) { - return is_constant(e) && const_name(e) == g_placeholder_name; -} - -bool has_placeholder(expr const & e) { - return occurs(mk_placholder(), e); -} - -expr mk_metavar(unsigned idx) { - return mk_constant(name(g_metavar_prefix, idx)); -} - -bool is_metavar(expr const & n) { - return is_constant(n) && !const_name(n).is_atomic() && const_name(n).get_prefix() == g_metavar_prefix; -} - -unsigned metavar_idx(expr const & n) { - lean_assert(is_metavar(n)); - return const_name(n).get_numeral(); -} - -/** - \brief Auxiliary exception used to sign that a metavariable was - found in an expression. -*/ -struct found_metavar {}; - -bool has_metavar(expr const & e) { - auto f = [](expr const & c, unsigned offset) { - if (is_metavar(c)) - throw found_metavar(); - }; - try { - for_each_fn proc(f); - proc(e); - return false; - } catch (found_metavar) { - return true; - } -} - -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; - } -} - -expr mk_subst_fn(unsigned idx) { - return mk_constant(name(g_subst_prefix, idx)); -} - -bool is_subst_fn(expr const & n) { - return is_constant(n) && !const_name(n).is_atomic() && const_name(n).get_prefix() == g_subst_prefix; -} - -expr mk_subst(expr const & e, unsigned i, expr const & c) { - unsigned s, n; - expr a; - if (is_lift(e, a, s, n) && s <= i && i < s+n) { - return e; - } else { - return mk_eq(mk_subst_fn(i), mk_eq(e, c)); - } -} - -bool is_subst(expr const & e, expr & c, unsigned & i, expr & v) { - if (is_eq(e) && is_subst_fn(eq_lhs(e))) { - i = const_name(eq_lhs(e)).get_numeral(); - c = eq_lhs(eq_rhs(e)); - v = eq_rhs(eq_rhs(e)); - return true; - } else { - return false; - } -} - -bool is_subst(expr const & e) { - return is_eq(e) && is_subst_fn(eq_lhs(e)); -} - -expr mk_lift_fn(unsigned s, unsigned n) { - lean_assert(n > 0); - return mk_constant(name(name(g_lift_prefix, s), n)); -} - -bool is_lift_fn(expr const & n) { - return - is_constant(n) && - !const_name(n).is_atomic() && - !const_name(n).get_prefix().is_atomic() && - const_name(n).get_prefix().get_prefix() == g_lift_prefix; -} - -expr mk_lift(expr const & e, unsigned s, unsigned n) { - return mk_eq(mk_lift_fn(s, n), e); -} - -bool is_lift(expr const & e, expr & c, unsigned & s, unsigned & n) { - if (is_eq(e) && is_lift_fn(eq_lhs(e))) { - name const & l = const_name(eq_lhs(e)); - c = eq_rhs(e); - n = l.get_numeral(); - s = l.get_prefix().get_numeral(); - return true; - } else { - return false; - } -} - -bool is_lift(expr const & e) { - return is_eq(e) && is_lift_fn(eq_lhs(e)); -} - -expr mk_lower_fn(unsigned s, unsigned n) { - return mk_constant(name(name(g_lower_prefix, s), n)); -} - -bool is_lower_fn(expr const & n) { - return - is_constant(n) && - !const_name(n).is_atomic() && - !const_name(n).get_prefix().is_atomic() && - const_name(n).get_prefix().get_prefix() == g_lower_prefix; -} - -expr mk_lower(expr const & e, unsigned s2, unsigned n2) { - unsigned s1, n1; - expr c; - if (is_lift(e, c, s1, n1) && s1 <= s2 - n2 && s2 <= s1 + n1) { - n1 -= n2; - if (n1 == 0) - return c; - else - return mk_lift(c, s1, n1); - } else { - return mk_eq(mk_lower_fn(s2, n2), e); - } -} - -bool is_lower(expr const & e, expr & c, unsigned & s, unsigned & n) { - if (is_eq(e) && is_lower_fn(eq_lhs(e))) { - name const & l = const_name(eq_lhs(e)); - c = eq_rhs(e); - n = l.get_numeral(); - s = l.get_prefix().get_numeral(); - return true; - } else { - return false; - } -} - -bool is_lower(expr const & e) { - return is_eq(e) && is_lower_fn(eq_lhs(e)); -} - -bool is_meta(expr const & e) { - return is_metavar(e) || is_subst(e) || is_lift(e) || is_lower(e); -} - -expr lower_free_vars_mmv(expr const & a, unsigned s, unsigned n) { - if (n == 0) - return a; - lean_assert(s >= n); - auto f = [=](expr const & e, unsigned offset) -> expr { - if (is_var(e) && var_idx(e) >= s + offset) { - return mk_var(var_idx(e) - n); - } else if (is_meta(e)) { - return mk_lower(e, s + offset, n); - } else { - return e; - } - }; - return replace_fn(f)(a); -} - -expr lift_free_vars_mmv(expr const & a, unsigned s, unsigned n) { - if (n == 0) - return a; - auto f = [=](expr const & e, unsigned offset) -> expr { - if (is_var(e) && var_idx(e) >= s + offset) { - return mk_var(var_idx(e) + n); - } else if (is_meta(e)) { - return mk_lift(e, s + offset, n); - } else { - return e; - } - }; - return replace_fn(f)(a); -} - -expr instantiate_free_var_mmv(expr const & a, unsigned i, expr const & c) { - auto f = [&](expr const & e, unsigned offset) -> expr { - if (is_var(e)) { - unsigned vidx = var_idx(e); - if (vidx == offset + i) - return lift_free_vars_mmv(c, 0, offset); - else if (vidx > offset + i) - return mk_var(vidx - 1); - else - return e; - } else if (is_meta(e)) { - return mk_lower(mk_subst(e, offset, lift_free_vars_mmv(c, 0, offset+1)), offset+1, 1); - } else { - return e; - } - }; - return replace_fn(f)(a); -} - -expr subst_mmv(expr const & a, unsigned i, expr const & c) { - auto f = [&](expr const & e, unsigned offset) -> expr { - if (is_var(e)) { - unsigned vidx = var_idx(e); - if (vidx == offset + i) - return lift_free_vars_mmv(c, 0, offset); - else - return e; - } else if (is_meta(e)) { - return mk_subst(e, offset, lift_free_vars_mmv(c, 0, offset)); - } else { - return e; - } - }; - return replace_fn(f)(a); -} - -expr get_metavar(expr const & e) { - lean_assert(is_meta(e)); - if (is_metavar(e)) { - return e; - } else { - unsigned i, s, n; - expr c, v; - if (is_lift(e, c, s, n)) { - return get_metavar(c); - } else if (is_lower(e, c, s, n)) { - return get_metavar(c); - } else if (is_subst(e, c, i, v)) { - return get_metavar(c); - } else { - lean_unreachable(); - return e; - } - } -} - -expr instantiate_metavar_core(expr const & e, expr const & v) { - lean_assert(is_meta(e)); - unsigned i, s, n; - expr c, a; - if (is_metavar(e)) { - return v; - } else if (is_subst(e, c, i, a)) { - return subst_mmv(instantiate_metavar_core(c, v), i, a); - } else if (is_lift(e, c, s, n)) { - return lift_free_vars_mmv(instantiate_metavar_core(c, v), s, n); - } else if (is_lower(e, c, s, n)) { - return lower_free_vars_mmv(instantiate_metavar_core(c, v), s, n); - } else { - lean_unreachable(); - return e; - } -} - -expr instantiate_metavar(expr const & a, unsigned midx, expr const & v) { - auto f = [=](expr const & e, unsigned offset) -> expr { - if (is_meta(e)) { - expr m = get_metavar(e); - lean_assert(is_metavar(m)); - if (metavar_idx(m) == midx) { - return instantiate_metavar_core(e, v); - } else { - return e; - } - } else { - return e; - } - }; - return replace_fn(f)(a); -} - -static expr get_def_value(name const & n, environment const & env, name_set const * defs) { - if (defs == nullptr || defs->find(n) != defs->end()) { - object const & obj = env.find_object(n); - if (obj && obj.is_definition() && !obj.is_opaque()) - return obj.get_value(); - } - return expr(); -} - -expr head_reduce_mmv(expr const & e, environment const & env, name_set const * defs) { - if (is_app(e) && is_lambda(arg(e, 0))) { - expr r = arg(e, 0); - unsigned num = num_args(e); - unsigned i = 1; - while (i < num) { - r = instantiate_free_var_mmv(abst_body(r), 0, arg(e, i)); - i = i + 1; - if (!is_lambda(r)) - break; - } - if (i < num) { - buffer args; - args.push_back(r); - for (; i < num; i++) - args.push_back(arg(e, i)); - r = mk_app(args.size(), args.data()); - } - return r; - } else if (is_app(e) && is_constant(arg(e, 0))) { - expr def = get_def_value(const_name(arg(e, 0)), env, defs); - if (def) - return update_app(e, 0, def); - } else if (is_let(e)) { - return instantiate_free_var_mmv(let_body(e), 0, let_value(e)); - } else if (is_constant(e)) { - expr def = get_def_value(const_name(e), env, defs); - if (def) - return def; - } - return e; -} - -} diff --git a/src/library/metavar.h b/src/library/metavar.h deleted file mode 100644 index 2a7cc64c50..0000000000 --- a/src/library/metavar.h +++ /dev/null @@ -1,154 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "util/name_set.h" -#include "kernel/expr.h" -#include "kernel/environment.h" - -namespace lean { -/** - \brief Return a new placeholder expression. To be able to track location, - a new constant for each placeholder. -*/ -expr mk_placholder(); - -/** - \brief Return true iff the given expression is a placeholder. -*/ -bool is_placeholder(expr const & e); - -/** - \brief Return true iff the given expression contains placeholders. -*/ -bool has_placeholder(expr const & e); - -/** - \brief Create a new metavariable with index \c idx. -*/ -expr mk_metavar(unsigned idx); - -/** - \brief Return true iff \c n is a metavariable. -*/ -bool is_metavar(expr const & n); - -/** - \brief Return the index of the given metavariable. - \pre is_metavar(n); -*/ -unsigned metavar_idx(expr const & n); - -/** - \brief Return true iff the given expression contains a - metavariable -*/ -bool has_metavar(expr const & e); - -/** - \brief Return true iff \c e contains a metavariable with index - \c midx -*/ -bool has_metavar(expr const & e, unsigned midx); - -/** - \brief Version of lift_free_vars for expressions containing - metavariables. It will return a new expression such that the - index idx of free variables is increased by \c n when idx >= - s. - - The suffix mmv stands for "modulo metavariables". -*/ -expr lift_free_vars_mmv(expr const & e, unsigned s, unsigned n); - -/** - \brief Version of instantiate for expressions containing - metavariables. It will return a new expression such that the free - variables with index \c i are replaced with the expression \c v. - Moreover, the index \c idx of the free variables with idx > i is - lowered by 1. - - The suffix mmv stands for "modulo metavariables". -*/ -expr instantiate_free_var_mmv(expr const & e, unsigned i, expr const & v); - -/** - \brief Version of lower_free_vars for expressions containing - metavariables. It will return a new expression such that the - index \c idx of free variables is lowered by \c n when idx >= s. - - The suffix mmv stands for "modulo metavariables". -*/ -expr lower_free_vars_mmv(expr const & e, unsigned s, unsigned n); - -/** - \brief Instantiate the metavariable with index \c midx in \c e with - the expression \c v. -*/ -expr instantiate_metavar(expr const & e, unsigned midx, expr const & v); - -/** - \brief Try to reduce the head of the given expression. - The following reductions are tried: - 1- Beta reduction - 2- Constant unfolding (if constant is defined in env, and defs == - nullptr or it contains constant). - 3- Let expansion - - \remark The expression \c e may contain metavariables. -*/ -expr head_reduce_mmv(expr const & e, environment const & env, name_set const * defs = nullptr); - -/** - \brief Return true iff \c e is a delayed substitution expression - of the form (subst:i c v). The meaning of the expression is - substitute free variable \c i in \c c with expression \c v. -*/ -bool is_subst(expr const & e, expr & c, unsigned & i, expr & v); - -/** - \brief Return true iff \c e is a delayed substitution expression. -*/ -bool is_subst(expr const & e); - -/** - \brief Return true iff \c e is a delayed lift expression of the - form (lift:s:n c). The meaning of the expression is lift the free - variables >= \c s by \c n in \c c. -*/ -bool is_lift(expr const & e, expr & c, unsigned & s, unsigned & n); - -/** - \brief Return true iff \c e is a delayed lift expression. -*/ -bool is_lift(expr const & e); - -/** - \brief Return true iff \c e is a delayed lower expression of the - form (lower:s:n c). The meaning of the expression is lower the free - variables >= \c s by \c n in \c c. -*/ -bool is_lower(expr const & e, expr & c, unsigned & s, unsigned & n); - -/** - \brief Return true iff \c e is a delayed lower expression. -*/ -bool is_lower(expr const & e); - -/** - \brief Return true iff \c e is a meta-variable, or a delayed - instantiation expression, or a delayed lift expression, or a - delayed lower expression. -*/ -bool is_meta(expr const & e); - -/** - \brief Return nested metavar in \c e - - \pre is_meta(e) -*/ -expr get_metavar(expr const & e); -} diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp new file mode 100644 index 0000000000..2df1401a32 --- /dev/null +++ b/src/library/placeholder.cpp @@ -0,0 +1,23 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/occurs.h" +#include "library/placeholder.h" + +namespace lean { +static name g_placeholder_name("_"); +expr mk_placholder() { + return mk_constant(g_placeholder_name); +} + +bool is_placeholder(expr const & e) { + return is_constant(e) && const_name(e) == g_placeholder_name; +} + +bool has_placeholder(expr const & e) { + return occurs(mk_placholder(), e); +} +} diff --git a/src/library/placeholder.h b/src/library/placeholder.h new file mode 100644 index 0000000000..28ec542e90 --- /dev/null +++ b/src/library/placeholder.h @@ -0,0 +1,26 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/expr.h" + +namespace lean { +/** + \brief Return a new placeholder expression. To be able to track location, + a new constant for each placeholder. +*/ +expr mk_placholder(); + +/** + \brief Return true iff the given expression is a placeholder. +*/ +bool is_placeholder(expr const & e); + +/** + \brief Return true iff the given expression contains placeholders. +*/ +bool has_placeholder(expr const & e); +} diff --git a/src/library/printer.cpp b/src/library/printer.cpp index 99a606699d..d6665c2b39 100644 --- a/src/library/printer.cpp +++ b/src/library/printer.cpp @@ -8,15 +8,16 @@ Author: Leonardo de Moura #include #include "util/exception.h" #include "library/printer.h" -#include "library/metavar.h" #include "kernel/environment.h" namespace lean { bool is_atomic(expr const & e) { switch (e.kind()) { - case expr_kind::Var: case expr_kind::Constant: case expr_kind::Value: case expr_kind::Type: + case expr_kind::Var: case expr_kind::Constant: case expr_kind::Value: + case expr_kind::Type: case expr_kind::MetaVar: return true; - case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Eq: case expr_kind::Let: + case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: + case expr_kind::Eq: case expr_kind::Let: return false; } return false; @@ -74,72 +75,78 @@ struct print_expr_fn { return print_child(a, c); } + void print_metavar(expr const & a, context const & c) { + out() << "?M" << metavar_idx(a); + if (metavar_ctx(a)) { + out() << "["; + bool first = true; + for (meta_entry const & e : metavar_ctx(a)) { + if (first) first = false; else out() << ", "; + switch (e.kind()) { + case meta_entry_kind::Lift: out() << "lift:" << e.s() << ":" << e.n(); break; + case meta_entry_kind::Lower: out() << "lower:" << e.s() << ":" << e.n(); break; + case meta_entry_kind::Subst: out() << "subst:" << e.s() << " "; print_child(e.v(), c); break; + } + } + out() << "]"; + } + } + void print(expr const & a, context const & c) { - unsigned i, s, n; - expr v, ch; - if (is_lower(a, ch, s, n)) { - out() << "lower:" << s << ":" << n << " "; print_child(ch, c); - } else if (is_lift(a, ch, s, n)) { - out() << "lift:" << s << ":" << n << " "; print_child(ch, c); - } else if (is_subst(a, ch, i, v)) { - out() << "subst:" << i << " "; print_child(ch, c); out() << " "; print_child(v, context()); - } else { - switch (a.kind()) { - case expr_kind::Var: - try { - out() << lookup(c, var_idx(a)).get_name(); - } catch (exception & ex) { - out() << "#" << var_idx(a); - } - break; - case expr_kind::Constant: - if (is_metavar(a)) { - out() << "?M:" << metavar_idx(a); - } else { - out() << const_name(a); - } - break; - case expr_kind::App: - print_app(a, c); - break; - case expr_kind::Eq: - print_eq(a, c); - break; - case expr_kind::Lambda: - out() << "fun " << abst_name(a) << " : "; + switch (a.kind()) { + case expr_kind::MetaVar: + print_metavar(a, c); + break; + case expr_kind::Var: + try { + out() << lookup(c, var_idx(a)).get_name(); + } catch (exception & ex) { + out() << "#" << var_idx(a); + } + break; + case expr_kind::Constant: + out() << const_name(a); + break; + case expr_kind::App: + print_app(a, c); + break; + case expr_kind::Eq: + print_eq(a, c); + break; + case expr_kind::Lambda: + out() << "fun " << abst_name(a) << " : "; + print_child(abst_domain(a), c); + out() << ", "; + print_child(abst_body(a), extend(c, abst_name(a), abst_domain(a))); + break; + case expr_kind::Pi: + if (!is_arrow(a)) { + out() << "Pi " << abst_name(a) << " : "; print_child(abst_domain(a), c); out() << ", "; print_child(abst_body(a), extend(c, abst_name(a), abst_domain(a))); break; - case expr_kind::Pi: - if (!is_arrow(a)) { - out() << "Pi " << abst_name(a) << " : "; - print_child(abst_domain(a), c); - out() << ", "; - print_child(abst_body(a), extend(c, abst_name(a), abst_domain(a))); - break; - } else { - print_child(abst_domain(a), c); - out() << " -> "; - print_arrow_body(abst_body(a), extend(c, abst_name(a), abst_domain(a))); - } - break; - case expr_kind::Let: - out() << "let " << let_name(a); - if (let_type(a)) - out() << " : " << let_type(a); - out() << " := "; - print(let_value(a), c); - out() << " in "; - print_child(let_body(a), extend(c, let_name(a), let_value(a))); - break; - case expr_kind::Type: - print_type(a); - break; - case expr_kind::Value: - print_value(a); - break; + } else { + print_child(abst_domain(a), c); + out() << " -> "; + print_arrow_body(abst_body(a), extend(c, abst_name(a), abst_domain(a))); } + break; + case expr_kind::Let: + out() << "let " << let_name(a); + if (let_type(a)) + out() << " : " << let_type(a); + out() << " := "; + print(let_value(a), c); + out() << " in "; + print_child(let_body(a), extend(c, let_name(a), let_value(a))); + break; + case expr_kind::Type: + print_type(a); + break; + case expr_kind::Value: + print_value(a); + break; } } @@ -163,12 +170,12 @@ std::ostream & operator<<(std::ostream & out, std::pair +#include "util/test.h" +#include "kernel/metavar.h" +#include "kernel/instantiate.h" +#include "kernel/abstract.h" +#include "kernel/free_vars.h" +#include "library/printer.h" +using namespace lean; + +static void tst1() { + unification_problems u; + metavar_env menv; + expr m1 = menv.mk_metavar(); + lean_assert(!menv.is_assigned(m1)); + lean_assert(menv.contains(m1)); + lean_assert(!menv.contains(2)); + expr t1 = menv.get_type(m1, u); + lean_assert(is_metavar(t1)); + lean_assert(menv.contains(t1)); + lean_assert(is_eqp(menv.get_type(m1, u), t1)); + lean_assert(is_eqp(menv.get_type(m1, u), t1)); + lean_assert(!menv.is_assigned(m1)); + expr m2 = menv.mk_metavar(); + lean_assert(!menv.is_assigned(m1)); + lean_assert(menv.contains(m1)); + expr t2 = menv.get_type(m2, u); + lean_assert(is_metavar(m2)); + lean_assert(menv.contains(m2)); + lean_assert(!is_eqp(t1, t2)); + lean_assert(t1 != t2); + lean_assert(u.eqs().empty()); + lean_assert(u.type_of_eqs().size() == 2); + for (auto p : u.type_of_eqs()) { + std::cout << "typeof(" << p.first << ") == " << p.second << "\n"; + } + expr f = Const("f"); + expr a = Const("a"); + menv.assign(m1, f(a)); + lean_assert(menv.is_assigned(m1)); + lean_assert(!menv.is_assigned(m2)); + lean_assert(menv.get_subst(m1) == f(a)); +} + +static void tst2() { + metavar_env menv; + expr f = Const("f"); + expr g = Const("g"); + expr h = Const("h"); + expr a = Const("a"); + expr m1 = menv.mk_metavar(); + expr m2 = menv.mk_metavar(); + // move m1 to a different context, and store new metavariable + context in m11 + expr m11 = add_lower(add_subst(m1, 0, f(a, m2)), 1, 1); + std::cout << m11 << "\n"; + menv.assign(m1, f(Var(0))); + std::cout << instantiate_metavars(m11, menv) << "\n"; + lean_assert(instantiate_metavars(m11, menv) == f(f(a, add_lower(m2, 1, 1)))); + menv.assign(m2, g(a, Var(1))); + std::cout << instantiate_metavars(h(m11), menv) << "\n"; + lean_assert(instantiate_metavars(h(m11), menv) == h(f(f(a, g(a, Var(0)))))); +} + +static void tst3() { + metavar_env menv; + expr f = Const("f"); + expr g = Const("g"); + expr h = Const("h"); + expr a = Const("a"); + expr x = Const("x"); + expr T = Const("T"); + expr m1 = menv.mk_metavar(); + expr F = Fun({x, T}, f(m1, x)); + menv.assign(m1, h(Var(0), Var(2))); + std::cout << instantiate(abst_body(F), g(a)) << "\n"; + std::cout << instantiate_metavars(instantiate(abst_body(F), g(a)), menv) << "\n"; + lean_assert(instantiate_metavars(instantiate(abst_body(F), g(a)), menv) == f(h(g(a), Var(1)), g(a))); + std::cout << instantiate(instantiate_metavars(abst_body(F), menv), g(a)) << "\n"; + lean_assert(instantiate(instantiate_metavars(abst_body(F), menv), g(a)) == + instantiate_metavars(instantiate(abst_body(F), g(a)), menv)); +} + +static void tst4() { + metavar_env menv; + expr f = Const("f"); + expr g = Const("g"); + expr h = Const("h"); + expr a = Const("a"); + expr m1 = menv.mk_metavar(); + expr F = f(m1, Var(2)); + menv.assign(m1, h(Var(1))); + std::cout << instantiate(F, {g(Var(0)), h(a)}) << "\n"; + std::cout << instantiate_metavars(instantiate(F, {g(Var(0)), h(a)}), menv) << "\n"; +} + +static void tst5() { + metavar_env menv; + expr m1 = menv.mk_metavar(); + expr f = Const("f"); + expr m11 = add_lower(m1, 2, 1); + std::cout << add_subst(add_lower(m1, 2, 1), 1, f(Var(0))) << "\n"; + std::cout << add_subst(add_lower(m1, 2, 1), 1, f(Var(3))) << "\n"; + std::cout << add_subst(add_lower(m1, 2, 1), 3, f(Var(0))) << "\n"; + std::cout << add_subst(add_lower(add_lower(m1, 2, 1), 3, 1), 3, f(Var(0))) << "\n"; + std::cout << add_lower(add_lift(m1, 1, 1), 1, 1) << "\n"; + std::cout << add_lower(add_lift(m1, 1, 1), 2, 1) << "\n"; + std::cout << add_lower(add_lift(m1, 1, 1), 2, 2) << "\n"; + std::cout << add_lower(add_lift(m1, 1, 3), 2, 2) << "\n"; + std::cout << add_subst(add_lift(m1, 1, 1), 0, f(Var(0))) << "\n"; + std::cout << add_subst(add_lift(m1, 1, 1), 1, f(Var(0))) << "\n"; + lean_assert(add_subst(add_lower(m1, 2, 1), 1, f(Var(0))) == + add_lower(add_subst(m1, 1, f(Var(0))), 2, 1)); + lean_assert(add_subst(add_lower(m1, 2, 1), 1, f(Var(3))) == + add_lower(add_subst(m1, 1, f(Var(4))), 2, 1)); + lean_assert(add_subst(add_lower(m1, 2, 1), 2, f(Var(0))) == + add_lower(add_subst(m1, 3, f(Var(0))), 2, 1)); + lean_assert(add_subst(add_lower(add_lower(m1, 2, 1), 3, 1), 3, f(Var(0))) == + add_lower(add_lower(add_subst(m1, 5, f(Var(0))), 2, 1), 3, 1)); + lean_assert(add_lower(add_lift(m1, 1, 1), 2, 1) == m1); + lean_assert(add_lower(add_lift(m1, 1, 3), 2, 2) == add_lift(m1, 1, 1)); + lean_assert(add_subst(add_lift(m1, 1, 1), 0, f(Var(0))) == + add_lift(add_subst(m1, 0, f(Var(0))), 1, 1)); + lean_assert(add_subst(add_lift(m1, 1, 1), 1, f(Var(0))) == + add_lift(m1, 1, 1)); +} + +static void tst6() { + expr N = Const("N"); + expr f = Const("f"); + expr x = Const("x"); + expr y = Const("y"); + expr a = Const("a"); + expr g = Const("g"); + expr h = Const("h"); + metavar_env menv; + expr m1 = 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 r = instantiate(t, g(m1, m2)); + std::cout << r << std::endl; + menv.assign(1, Var(2)); + r = instantiate_metavars(r, menv); + std::cout << r << std::endl; + menv.assign(0, h(Var(3))); + r = instantiate_metavars(r, menv); + 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)))))); +} + +static void tst7() { + expr f = Const("f"); + expr g = Const("g"); + expr a = Const("a"); + metavar_env menv; + expr m1 = menv.mk_metavar(); + expr t = f(m1, Var(0)); + expr r = instantiate(t, a); + menv.assign(0, g(Var(0))); + r = instantiate_metavars(r, menv); + std::cout << r << std::endl; + lean_assert(r == f(g(a), a)); +} + +static void tst8() { + expr f = Const("f"); + expr g = Const("g"); + expr a = Const("a"); + metavar_env menv; + expr m1 = menv.mk_metavar(); + expr t = f(m1, Var(0), Var(2)); + expr r = instantiate(t, a); + menv.assign(0, g(Var(0), Var(1))); + r = instantiate_metavars(r, menv); + std::cout << r << std::endl; + lean_assert(r == f(g(a, Var(0)), a, Var(1))); +} + +static void tst9() { + expr f = Const("f"); + expr g = Const("g"); + expr a = Const("a"); + metavar_env menv; + expr m1 = menv.mk_metavar(); + expr t = f(m1, Var(1), Var(2)); + expr r = lift_free_vars(t, 1, 2); + std::cout << r << std::endl; + r = instantiate(r, a); + std::cout << r << std::endl; + menv.assign(0, g(Var(0), Var(1))); + r = instantiate_metavars(r, menv); + std::cout << r << std::endl; + lean_assert(r == f(g(a, Var(2)), Var(2), Var(3))); +} + +static void tst10() { + expr N = Const("N"); + expr f = Const("f"); + expr x = Const("x"); + expr y = Const("y"); + expr a = Const("a"); + expr g = Const("g"); + expr h = Const("h"); + metavar_env menv; + expr m1 = 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 r = instantiate(t, g(m1)); + std::cout << r << std::endl; + r = instantiate(r, h(m2)); + std::cout << r << std::endl; + menv.assign(0, f(Var(0))); + menv.assign(1, Var(2)); + r = instantiate_metavars(r, menv); + 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)))))); +} + +int main() { + tst1(); + tst2(); + tst3(); + tst4(); + tst5(); + tst6(); + tst7(); + tst8(); + tst9(); + tst10(); + return has_violations() ? 1 : 0; +} diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp index 421a5c2b0a..8aede2dcc1 100644 --- a/src/tests/kernel/normalizer.cpp +++ b/src/tests/kernel/normalizer.cpp @@ -65,7 +65,8 @@ unsigned count_core(expr const & a, expr_set & s) { return 0; s.insert(a); switch (a.kind()) { - case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: + case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: + case expr_kind::Value: case expr_kind::MetaVar: return 1; case expr_kind::App: return std::accumulate(begin_args(a), end_args(a), 1, diff --git a/src/tests/library/CMakeLists.txt b/src/tests/library/CMakeLists.txt index 26e57af5f2..1302291b32 100644 --- a/src/tests/library/CMakeLists.txt +++ b/src/tests/library/CMakeLists.txt @@ -1,6 +1,3 @@ -add_executable(metavar metavar.cpp) -target_link_libraries(metavar ${EXTRA_LIBS}) -add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar) add_executable(light_checker light_checker.cpp) target_link_libraries(light_checker ${EXTRA_LIBS}) add_test(light_checker ${CMAKE_CURRENT_BINARY_DIR}/light_checker) diff --git a/src/tests/library/metavar.cpp b/src/tests/library/metavar.cpp deleted file mode 100644 index 51a74402b1..0000000000 --- a/src/tests/library/metavar.cpp +++ /dev/null @@ -1,120 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "util/test.h" -#include "kernel/abstract.h" -#include "library/metavar.h" -#include "library/printer.h" -using namespace lean; - -static void tst1() { - expr N = Const("N"); - expr f = Const("f"); - expr x = Const("x"); - expr y = Const("y"); - expr a = Const("a"); - expr g = Const("g"); - expr h = Const("h"); - expr m1 = mk_metavar(1); - expr m2 = mk_metavar(2); - expr t = f(Var(0), Fun({x, N}, f(Var(1), x, Fun({y, N}, f(Var(2), x, y))))); - expr r = instantiate_free_var_mmv(t, 0, g(m1, m2)); - std::cout << r << std::endl; - r = instantiate_metavar(r, 2, Var(2)); - std::cout << r << std::endl; - r = instantiate_metavar(r, 1, h(Var(3))); - 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)))))); -} - -static void tst2() { - expr f = Const("f"); - expr g = Const("g"); - expr a = Const("a"); - expr m1 = mk_metavar(1); - expr t = f(m1, Var(0)); - expr r = instantiate_free_var_mmv(t, 0, a); - r = instantiate_metavar(r, 1, g(Var(0))); - std::cout << r << std::endl; - lean_assert(r == f(g(a), a)); -} - -static void tst3() { - expr f = Const("f"); - expr g = Const("g"); - expr a = Const("a"); - expr m1 = mk_metavar(1); - expr t = f(m1, Var(0), Var(2)); - expr r = instantiate_free_var_mmv(t, 0, a); - r = instantiate_metavar(r, 1, g(Var(0), Var(1))); - std::cout << r << std::endl; - lean_assert(r == f(g(a, Var(0)), a, Var(1))); -} - -static void tst4() { - expr f = Const("f"); - expr g = Const("g"); - expr a = Const("a"); - expr m1 = mk_metavar(1); - expr t = f(m1, Var(1), Var(2)); - expr r = lift_free_vars_mmv(t, 1, 2); - std::cout << r << std::endl; - r = instantiate_free_var_mmv(r, 0, a); - std::cout << r << std::endl; - r = instantiate_metavar(r, 1, g(Var(0), Var(1))); - std::cout << r << std::endl; - lean_assert(r == f(g(a, Var(2)), Var(2), Var(3))); -} - -static void tst5() { - expr N = Const("N"); - expr f = Const("f"); - expr x = Const("x"); - expr y = Const("y"); - expr a = Const("a"); - expr g = Const("g"); - expr h = Const("h"); - expr m1 = mk_metavar(1); - expr m2 = mk_metavar(2); - 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_free_var_mmv(t, 0, g(m1)); - std::cout << r << std::endl; - r = instantiate_free_var_mmv(r, 0, h(m2)); - std::cout << r << std::endl; - r = instantiate_metavar(r, 1, f(Var(0))); - std::cout << r << std::endl; - r = instantiate_metavar(r, 2, Var(2)); - 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)))))); -} - -static void tst6() { - environment env; - expr N = Const("N"); - expr f = Const("f"); - expr a = Const("a"); - expr x = Const("x"); - expr m1 = mk_metavar(1); - expr t = mk_app(Fun({x, N}, m1), a); - expr s1 = instantiate_metavar(head_reduce_mmv(t, env), 1, Var(0)); - expr s2 = head_reduce_mmv(instantiate_metavar(t, 1, Var(0)), env); - std::cout << instantiate_metavar(t, 1, Var(0)) << "\n"; - std::cout << s1 << "\n"; - std::cout << s2 << "\n"; - lean_assert(s1 == s2); -} - -int main() { - tst1(); - tst2(); - tst3(); - tst4(); - tst5(); - tst6(); - return has_violations() ? 1 : 0; -} - - diff --git a/src/util/list_fn.h b/src/util/list_fn.h index 2909dbfca2..ccbd3b8708 100644 --- a/src/util/list_fn.h +++ b/src/util/list_fn.h @@ -91,4 +91,32 @@ list append(list const & l1, list const & l2) { to_buffer(l2, tmp); return to_list(tmp.begin(), tmp.end()); } + +/** + \brief Given list (a_0, ..., a_k), return list (f(a_0), ..., f(a_k)). +*/ +template +list map(list const & l, F f) { + if (is_nil(l)) { + return l; + } else { + return list(f(head(l)), map(tail(l), f)); + } +} + +/** + \brief Compare two lists using the binary predicate p. +*/ +template +bool compare(list const & l1, list const & l2, P p) { + auto it1 = l1.begin(); + auto it2 = l2.begin(); + auto end1 = l1.end(); + auto end2 = l2.end(); + for (; it1 != end1 && it2 != end2; ++it1, ++it2) { + if (!p(*it1, *it2)) + return false; + } + return it1 == end1 && it2 == end2; +} } diff --git a/src/util/pvector.h b/src/util/pvector.h index 4bc8b15393..c6f229212a 100644 --- a/src/util/pvector.h +++ b/src/util/pvector.h @@ -351,6 +351,7 @@ public: ref(pvector & v, unsigned i):m_vector(v), m_idx(i) {} ref & operator=(T const & a) { m_vector.set(m_idx, a); return *this; } operator T const &() const { return m_vector.get(m_idx); } + T const * operator->() const { return &(m_vector.get(m_idx)); } }; T const & operator[](unsigned i) const { return get(i); } diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp index 8108bacbd9..776467867a 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/sexpr/format.cpp @@ -145,6 +145,8 @@ static format g_line(mk_line()); static format g_space(" "); static format g_lp("("); static format g_rp(")"); +static format g_lsb("["); +static format g_rsb("]"); static format g_lcurly("{"); static format g_rcurly("}"); static format g_comma(","); @@ -154,6 +156,8 @@ format const & line() { return g_line; } format const & space() { return g_space; } format const & lp() { return g_lp; } format const & rp() { return g_rp; } +format const & lsb() { return g_lsb; } +format const & rsb() { return g_rsb; } format const & lcurly() { return g_lcurly; } format const & rcurly() { return g_rcurly; } format const & comma() { return g_comma; } @@ -212,10 +216,7 @@ format above(format const & f1, format const & f2) { return format{f1, line(), f2}; } format bracket(std::string const l, format const & x, std::string const r) { - return group(format{format(l), - nest(2, format(line(), x)), - line(), - format(r)}); + return group(nest(l.size(), format{format(l), x, format(r)})); } format paren(format const & x) { return group(nest(1, format{lp(), x, rp()})); diff --git a/src/util/sexpr/format.h b/src/util/sexpr/format.h index 9e3910ed19..ea50ab9802 100644 --- a/src/util/sexpr/format.h +++ b/src/util/sexpr/format.h @@ -232,6 +232,8 @@ format const & line(); format const & space(); format const & lp(); format const & rp(); +format const & lsb(); +format const & rsb(); format const & lcurly(); format const & rcurly(); format const & comma(); diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out index 0dc2014c3b..9e3dfe78fa 100644 --- a/tests/lean/elab1.lean.expected.out +++ b/tests/lean/elab1.lean.expected.out @@ -19,9 +19,9 @@ Function type: Π (A : Type), A → A Arguments types: A : Type - x : lift:0:2 ?M0 + x : ?M0 Elaborator state - #0 ≈ lift:0:2 ?M0 + #0 ≈ ?M0[lift:0:2] Assumed: eq Error (line: 15, pos: 51) application type mismatch during term elaboration eq C a b @@ -29,11 +29,11 @@ Function type: Π (A : Type), A → A → Bool Arguments types: C : Type - a : lift:0:3 ?M0 - b : lift:0:2 ?M2 + a : ?M0[lower:5:5 lift:0:3 subst:0 B subst:1 A] + b : ?M2[lower:5:5 lift:0:2 subst:0 a subst:1 B subst:2 A] Elaborator state - #0 ≈ lift:0:2 ?M2 - #0 ≈ lift:0:3 ?M0 + #0 ≈ ?M2[lift:0:2] + #0 ≈ ?M0[lift:0:3] Assumed: a Assumed: b Assumed: H @@ -46,7 +46,7 @@ Expected type: Got: ?M4 ⇒ ?M2 Elaborator state - lift:0:1 ?M2 ≈ lift:0:1 ?M4 ∧ a + ?M2[lift:0:1] ≈ (?M4[lift:0:1]) ∧ a b ≈ if Bool ?M4 ?M2 ⊤ b ≈ if Bool ?M4 ?M2 ⊤ Error (line: 22, pos: 22) type mismatch at application diff --git a/tests/lean/implicit1.lean.expected.out b/tests/lean/implicit1.lean.expected.out index 8238c267ea..f0b01530b8 100644 --- a/tests/lean/implicit1.lean.expected.out +++ b/tests/lean/implicit1.lean.expected.out @@ -15,8 +15,8 @@ Candidates: Int::add : ℤ → ℤ → ℤ Nat::add : ℕ → ℕ → ℕ Arguments: - a : lift:0:2 ?M0 - b : lift:0:1 ?M2 + a : ?M0 + b : ?M2[lower:2:2 lift:0:1 subst:0 a] λ a b c : ℤ, a + c + b Error (line: 17, pos: 19) ambiguous overloads Candidates: @@ -24,7 +24,7 @@ Candidates: Int::add : ℤ → ℤ → ℤ Nat::add : ℕ → ℕ → ℕ Arguments: - a : lift:0:2 ?M0 - b : lift:0:1 ?M2 + a : ?M0 + b : ?M2[lower:2:2 lift:0:1 subst:0 a] Assumed: x λ a b : ℤ, a + x + b diff --git a/tests/lean/tst7.lean.expected.out b/tests/lean/tst7.lean.expected.out index 142a2f9f46..5a3f41a038 100644 --- a/tests/lean/tst7.lean.expected.out +++ b/tests/lean/tst7.lean.expected.out @@ -8,9 +8,9 @@ Function type: Π (A : Type), A → Bool Arguments types: B : Type - a : lift:0:2 ?M0 + a : ?M0[lower:3:3 lift:0:2 subst:0 A] Elaborator state - #0 ≈ lift:0:2 ?M0 + #0 ≈ ?M0[lift:0:2] Assumed: myeq myeq (Π (A : Type), A → A) (λ (A : Type) (a : A), a) (λ (B : Type) (b : B), b) myeq (Π (A : Type), A → A) (λ (A : Type) (a : A), a) (λ (B : Type) (b : B), b) : Bool