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

Move metavariables to the kernel. This is the first step for implementing the new elaborator.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-12 18:25:38 -07:00
parent dfd4b3b57f
commit 63e102055e
41 changed files with 1270 additions and 840 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

123
src/frontends/lean/elaborator.cpp
View file

@ -9,14 +9,18 @@ Author: Leonardo de Moura
#include <utility>
#include <vector>
#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)) {

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

@ -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"

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

@ -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) {

2
src/kernel/CMakeLists.txt
View file

@ -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})

4
src/kernel/context.h
View file

@ -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<context_entry const &, context> 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<context_entry>::iterator iterator;
iterator begin() const { return m_list.begin(); }
@ -58,5 +58,5 @@ inline std::pair<context_entry const &, context> 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(); }
}

35
src/kernel/expr.cpp
View file

@ -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<unsigned>(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<expr_type*>(this); break;
case expr_kind::Value: delete static_cast<expr_value*>(this); break;
case expr_kind::Let: delete static_cast<expr_let*>(this); break;
case expr_kind::MetaVar: delete static_cast<expr_metavar*>(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();

130
src/kernel/expr.h
View file

@ -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_entry> 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<expr_kind>(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:
<code>
| Lift s n
| Lower s n
| Subst s v
</code>
where \c s and \c n are unsigned integers, and
\c v is an expression
The meaning of <tt>Lift s n</tt> is: lift the free variables greater than or equal to \c s by \c n.
The meaning of <tt>Lower s n</tt> is: lower the free variables greater than or equal to \c s by \c n.
The meaning of <tt>Subst s v</tt> 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
<code>
[ Lower 1 1, Subst 0 a, Lift 1 2 ]
</code>
Now, assume we want to instantiate \c ?M with <tt>f #0 (g #2)</tt>.
Then, we apply the metavariable entries from right to left.
Thus, first we apply <tt>(Lift 1 2)</tt> and obtain the term
<code>
f #0 (g #4)
</code>
Then, we apply <tt>(Subst 0 a)</tt> and produce
<code>
f a (g #4)
</code>
Finally, we apply <tt>(Lower 1 1)</tt> and get the final result
<code>
f a (g #3)
</code>
*/
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<expr_pi*>(e); }
inline expr_type * to_type(expr_cell * e) { lean_assert(is_type(e)); return static_cast<expr_type*>(e); }
inline expr_let * to_let(expr_cell * e) { lean_assert(is_let(e)); return static_cast<expr_let*>(e); }
inline expr_metavar * to_metavar(expr_cell * e) { lean_assert(is_metavar(e)); return static_cast<expr_metavar*>(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<typename F> expr update_eq(expr const & e, F f) {
else
return e;
}
template<typename F> expr update_metavar(expr const & e, unsigned i, F f) {
buffer<meta_entry> 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<typename F> expr update_metavar(expr const & e, F f) {
return update_metavar(e, metavar_idx(e), f);
}
// =======================================
}

10
src/kernel/expr_eq.h
View file

@ -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

3
src/kernel/for_each.h
View file

@ -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); });

35
src/kernel/free_vars.cpp
View file

@ -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 <tt>[low, high)</tt> or not. */
/**
\brief Functional object for checking whether a kernel expression has a free variable in the range <tt>[low, high)</tt> 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<decltype(f)>(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;
}

11
src/kernel/free_vars.h
View file

@ -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 <tt>(var i)</tt> is mapped into <tt>(var i-d)</tt>.
\brief Lower the free variables >= s in \c e by d. That is, a free variable <tt>(var i)</tt> s.t.
<tt>i >= s</tt> is mapped into <tt>(var i-d)</tt>.
\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); }
}

41
src/kernel/instantiate.cpp
View file

@ -7,38 +7,55 @@ Author: Leonardo de Moura
#include <algorithm>
#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<decltype(f)>(f)(e);
return replace_fn<decltype(f)>(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<decltype(f)>(f)(e);
return replace_fn<decltype(f)>(f)(a);
}
}

4
src/kernel/instantiate.h
View file

@ -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<expr> 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<expr> const & l) { return instantiate(e, l.size(), l.begin()); }
inline expr instantiate(expr const & e, expr const & s) { return instantiate(e, 1, &s); }
}

229
src/kernel/metavar.cpp Normal file
View file

@ -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 <limits>
#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<decltype(f)>(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<decltype(f)>(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<unsigned>::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<unsigned>::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<decltype(f)> proc(f);
proc(e);
return false;
} catch (found_metavar) {
return true;
}
}
}

186
src/kernel/metavar.h Normal file
View file

@ -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 <utility>
#include <vector>
#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. <tt>lhs == rhs</tt>
2. <tt>typeof(n) == t</tt>
*/
class unification_problems {
std::vector<std::pair<expr, expr>> m_eqs;
std::vector<std::pair<expr, expr>> m_type_of_eqs;
public:
/**
\brief Add a new unification problem of the form <tt>lhs == rhs</tt>
*/
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 <tt>typeof(n) == t</tt>
*/
void add_type_of_eq(expr const & n, expr const & t) { m_type_of_eqs.push_back(mk_pair(n, t)); }
std::vector<std::pair<expr, expr>> const & eqs() const { return m_eqs; }
std::vector<std::pair<expr, expr>> 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<std::pair<expr, expr>> 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
<tt>midx -> (s, t)</tt>.
*/
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
<tt>typeof(m) = t</tt> 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());
}

5
src/kernel/normalizer.cpp
View file

@ -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;

3
src/kernel/replace.h
View file

@ -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); });

5
src/kernel/type_checker.cpp
View file

@ -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;

4
src/library/CMakeLists.txt
View file

@ -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})

11
src/library/deep_copy.cpp
View file

@ -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));

6
src/library/light_checker.cpp
View file

@ -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: {

10
src/library/max_sharing.cpp
View file

@ -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;

357
src/library/metavar.cpp
View file

@ -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<decltype(f)> 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<decltype(f)> 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<decltype(f)>(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<decltype(f)>(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<decltype(f)>(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<decltype(f)>(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<decltype(f)>(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<expr> 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;
}
}

154
src/library/metavar.h
View file

@ -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 <tt>idx >=
s</tt>.
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 <tt>idx > i</tt> 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 <tt>idx >= s</tt>.
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);
}

23
src/library/placeholder.cpp Normal file
View file

@ -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);
}
}

26
src/library/placeholder.h Normal file
View file

@ -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);
}

137
src/library/printer.cpp
View file

@ -8,15 +8,16 @@ Author: Leonardo de Moura
#include <utility>
#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<expr const &, context co
}
static void display_context_core(std::ostream & out, context const & ctx) {
if (!is_empty(ctx)) {
if (!empty(ctx)) {
auto p = lookup_ext(ctx, 0);
context_entry const & head = p.first;
context const & tail_ctx = p.second;
display_context_core(out, tail_ctx);
if (!is_empty(tail_ctx))
if (!empty(tail_ctx))
out << "; ";
out << head.get_name() << " : " << head.get_domain();
if (head.get_body()) {

2
src/tests/frontends/lean/implicit_args.cpp
View file

@ -10,7 +10,7 @@ Author: Leonardo de Moura
#include "kernel/occurs.h"
#include "kernel/abstract.h"
#include "kernel/free_vars.h"
#include "library/metavar.h"
#include "library/placeholder.h"
#include "library/printer.h"
#include "library/basic_thms.h"
#include "library/all/all.h"

9
src/tests/kernel/CMakeLists.txt
View file

@ -1,6 +1,6 @@
add_executable(expr_tst expr.cpp)
target_link_libraries(expr_tst ${EXTRA_LIBS})
add_test(expr ${CMAKE_CURRENT_BINARY_DIR}/expr_tst)
add_executable(expr expr.cpp)
target_link_libraries(expr ${EXTRA_LIBS})
add_test(expr ${CMAKE_CURRENT_BINARY_DIR}/expr)
add_executable(normalizer normalizer.cpp)
target_link_libraries(normalizer ${EXTRA_LIBS})
add_test(normalizer ${CMAKE_CURRENT_BINARY_DIR}/normalizer)
@ -28,3 +28,6 @@ add_test(environment ${CMAKE_CURRENT_BINARY_DIR}/environment)
add_executable(occurs occurs.cpp)
target_link_libraries(occurs ${EXTRA_LIBS})
add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs)
add_executable(metavar_kernel metavar.cpp)
target_link_libraries(metavar_kernel ${EXTRA_LIBS})
add_test(metavar_kernel ${CMAKE_CURRENT_BINARY_DIR}/metavar_kernel)

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

@ -53,7 +53,8 @@ expr mk_dag(unsigned depth, bool _closed = false) {
unsigned depth1(expr const & e) {
switch (e.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: {
unsigned m = 0;
@ -74,7 +75,8 @@ unsigned depth1(expr const & e) {
// This is the fastest depth implementation in this file.
unsigned depth2(expr const & e) {
switch (e.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
@ -102,7 +104,8 @@ unsigned depth3(expr const & e) {
unsigned c = p.second + 1;
todo.pop_back();
switch (e.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:
m = std::max(c, m);
break;
case expr_kind::App: {
@ -171,7 +174,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,
@ -352,6 +356,35 @@ void tst15() {
lean_assert(closed(l));
}
void tst16() {
expr f = Const("f");
expr x = Var(0);
expr a = Const("a");
expr m = mk_metavar(0);
lean_assert(has_metavar(m));
lean_assert(has_metavar(f(m)));
lean_assert(!has_metavar(f(a)));
lean_assert(!has_metavar(f(x)));
lean_assert(!has_metavar(Pi({a, Type()}, a)));
lean_assert(!has_metavar(Type()));
lean_assert(!has_metavar(Fun({a, Type()}, a)));
lean_assert(has_metavar(Pi({a, Type()}, m)));
lean_assert(has_metavar(Pi({a, m}, a)));
lean_assert(has_metavar(Fun({a, Type()}, m)));
lean_assert(has_metavar(Fun({a, m}, a)));
lean_assert(!has_metavar(Let({a, Type()}, a)));
lean_assert(!has_metavar(mk_let(name("a"), Type(), f(x), f(f(x)))));
lean_assert(has_metavar(mk_let(name("a"), m, f(x), f(f(x)))));
lean_assert(has_metavar(mk_let(name("a"), Type(), f(m), f(f(x)))));
lean_assert(has_metavar(mk_let(name("a"), Type(), f(x), f(f(m)))));
lean_assert(has_metavar(f(a, a, m)));
lean_assert(has_metavar(f(a, m, a, a)));
lean_assert(!has_metavar(f(a, a, a, a)));
lean_assert(!has_metavar(Eq(a, f(a))));
lean_assert(has_metavar(Eq(m, f(a))));
lean_assert(has_metavar(Eq(a, f(m))));
}
int main() {
std::cout << "sizeof(expr): " << sizeof(expr) << "\n";
std::cout << "sizeof(expr_app): " << sizeof(expr_app) << "\n";
@ -371,6 +404,7 @@ int main() {
tst13();
tst14();
tst15();
tst16();
std::cout << "done" << "\n";
return has_violations() ? 1 : 0;
}

235
src/tests/kernel/metavar.cpp Normal file
View file

@ -0,0 +1,235 @@
/*
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 <algorithm>
#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;
}

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

@ -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,

3
src/tests/library/CMakeLists.txt
View file

@ -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)

120
src/tests/library/metavar.cpp
View file

@ -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;
}

28
src/util/list_fn.h
View file

@ -91,4 +91,32 @@ list<T> append(list<T> const & l1, list<T> const & l2) {
to_buffer(l2, tmp);
return to_list(tmp.begin(), tmp.end());
}
/**
\brief Given list <tt>(a_0, ..., a_k)</tt>, return list <tt>(f(a_0), ..., f(a_k))</tt>.
*/
template<typename T, typename F>
list<T> map(list<T> const & l, F f) {
if (is_nil(l)) {
return l;
} else {
return list<T>(f(head(l)), map(tail(l), f));
}
}
/**
\brief Compare two lists using the binary predicate p.
*/
template<typename T, typename P>
bool compare(list<T> const & l1, list<T> 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;
}
}

1
src/util/pvector.h
View file

@ -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); }

9
src/util/sexpr/format.cpp
View file

@ -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()}));

2
src/util/sexpr/format.h
View file

@ -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();

14
tests/lean/elab1.lean.expected.out
View file

@ -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

8
tests/lean/implicit1.lean.expected.out
View file

@ -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

4
tests/lean/tst7.lean.expected.out
View file

@ -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