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

refactor(metavar): implement metavar_env, and use unification_constraint and trace objects in the type_checker, light_checker

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-01 17:25:17 -07:00
parent 1f0eab7a14
commit 7cf83800c0
25 changed files with 649 additions and 614 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/kernel/context.h
View file

@ -39,6 +39,7 @@ public:
context_entry const & lookup(unsigned vidx) const;
std::pair<context_entry const &, context> lookup_ext(unsigned vidx) const;
bool empty() const { return is_nil(m_list); }
operator bool() const { return !empty(); }
unsigned size() const { return length(m_list); }
typedef list<context_entry>::iterator iterator;
iterator begin() const { return m_list.begin(); }

6
src/kernel/environment.cpp
View file

@ -235,7 +235,7 @@ struct environment::imp {
infer_universe and infer_type expect an environment instead of environment::imp.
*/
void check_type(name const & n, expr const & t, expr const & v, environment const & env) {
m_type_checker.infer_universe(t);
m_type_checker.check_type(t);
expr v_t = m_type_checker.infer_type(v);
if (!m_type_checker.is_convertible(v_t, t))
throw def_type_mismatch_exception(env, n, t, v, v_t);
@ -296,14 +296,14 @@ struct environment::imp {
/** \brief Add new axiom. */
void add_axiom(name const & n, expr const & t, environment const & env) {
check_name(n, env);
m_type_checker.infer_universe(t);
m_type_checker.check_type(t);
register_named_object(mk_axiom(n, t));
}
/** \brief Add new variable. */
void add_var(name const & n, expr const & t, environment const & env) {
check_name(n, env);
m_type_checker.infer_universe(t);
m_type_checker.check_type(t);
register_named_object(mk_var_decl(n, t));
}

17
src/kernel/expr.cpp
View file

@ -137,21 +137,10 @@ expr_value::expr_value(value & v):
expr_value::~expr_value() {
m_val.dec_ref();
}
expr_metavar::expr_metavar(name const & n, expr const & t, local_context const & lctx):
expr_metavar::expr_metavar(name const & n, local_context const & lctx):
expr_cell(expr_kind::MetaVar, n.hash(), true),
m_name(n), m_type(t), m_lctx(lctx) {}
m_name(n), m_lctx(lctx) {}
expr_metavar::~expr_metavar() {}
expr expr_metavar::get_type() const {
if (m_type && get_lctx()) {
if (is_metavar(m_type)) {
return update_metavar(m_type, append(get_lctx(), metavar_lctx(m_type)));
} else {
return apply_local_context(m_type, get_lctx());
}
} else {
return m_type;
}
}
void expr_cell::dealloc() {
switch (kind()) {
@ -192,7 +181,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_name(a), metavar_raw_type(a), metavar_lctx(a));
case expr_kind::MetaVar: return mk_metavar(metavar_name(a), metavar_lctx(a));
}
lean_unreachable();
}

28
src/kernel/expr.h
View file

@ -31,7 +31,7 @@ class value;
| Type universe
| Eq expr expr (heterogeneous equality)
| Let name expr expr expr
| Metavar name expr? local_context (the expression is the type of the metavariable)
| Metavar name local_context
local_context ::= [local_entry]
@ -121,7 +121,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(name const & n, expr const & t, local_context const & ctx);
friend expr mk_metavar(name const & n, local_context const & ctx);
friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; }
@ -314,15 +314,11 @@ inline local_entry mk_inst(unsigned s, expr const & v) { return local_entry(s, v
/** \brief Metavariables */
class expr_metavar : public expr_cell {
name m_name;
expr m_type;
local_context m_lctx;
public:
expr_metavar(name const & n, expr const & t, local_context const & lctx);
expr_metavar(name const & n, local_context const & lctx);
~expr_metavar();
name const & get_name() const { return m_name; }
expr const & get_raw_type() const { return m_type; }
/* \brief Return the type of the metavariable modulo the associated local context */
expr get_type() const;
local_context const & get_lctx() const { return m_lctx; }
};
// =======================================
@ -380,8 +376,8 @@ 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(name const & n, expr const & t = expr(), local_context const & ctx = local_context()) {
return expr(new expr_metavar(n, t, ctx));
inline expr mk_metavar(name const & n, local_context const & ctx = local_context()) {
return expr(new expr_metavar(n, ctx));
}
inline expr expr::operator()(expr const & a1) const { return mk_app({*this, a1}); }
@ -441,8 +437,6 @@ inline expr const & let_value(expr_cell * e) { return to_let(e)->get
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 name const & metavar_name(expr_cell * e) { return to_metavar(e)->get_name(); }
inline expr const & metavar_raw_type(expr_cell * e) { return to_metavar(e)->get_raw_type(); }
inline expr metavar_type(expr_cell * e) { return to_metavar(e)->get_type(); }
inline local_context const & metavar_lctx(expr_cell * e) { return to_metavar(e)->get_lctx(); }
/** \brief Return the reference counter of the given expression. */
@ -474,8 +468,6 @@ inline expr const & let_type(expr const & e) { return to_let(e)->ge
inline expr const & let_value(expr const & e) { return to_let(e)->get_value(); }
inline expr const & let_body(expr const & e) { return to_let(e)->get_body(); }
inline name const & metavar_name(expr const & e) { return to_metavar(e)->get_name(); }
inline expr const & metavar_raw_type(expr const & e) { return to_metavar(e)->get_raw_type(); }
inline expr metavar_type(expr const & e) { return to_metavar(e)->get_type(); }
inline local_context const & metavar_lctx(expr const & e) { return to_metavar(e)->get_lctx(); }
inline bool has_metavar(expr const & e) { return e.has_metavar(); }
@ -594,9 +586,9 @@ template<typename F> expr update_eq(expr const & e, F f) {
else
return e;
}
template<typename F> expr update_metavar(expr const & e, name const & n, expr const & t, F f) {
template<typename F> expr update_metavar(expr const & e, name const & n, F f) {
buffer<local_entry> new_entries;
bool modified = (n != metavar_name(e) || t != metavar_raw_type(e));
bool modified = n != metavar_name(e);
for (local_entry const & me : metavar_lctx(e)) {
local_entry new_me = f(me);
if (new_me.kind() != me.kind() || new_me.s() != me.s()) {
@ -610,16 +602,16 @@ template<typename F> expr update_metavar(expr const & e, name const & n, expr co
new_entries.push_back(new_me);
}
if (modified)
return mk_metavar(n, t, to_list(new_entries.begin(), new_entries.end()));
return mk_metavar(n, 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_name(e), metavar_raw_type(e), f);
return update_metavar(e, metavar_name(e), f);
}
inline expr update_metavar(expr const & e, local_context const & lctx) {
if (metavar_lctx(e) != lctx)
return mk_metavar(metavar_name(e), metavar_raw_type(e), lctx);
return mk_metavar(metavar_name(e), lctx);
else
return e;
}

1
src/kernel/expr_eq.h
View file

@ -60,7 +60,6 @@ class expr_eq_fn {
case expr_kind::MetaVar:
return
metavar_name(a) == metavar_name(b) &&
metavar_raw_type(a) == metavar_raw_type(b) &&
compare(metavar_lctx(a), metavar_lctx(b), [&](local_entry const & e1, local_entry const & e2) {
if (e1.kind() != e2.kind() || e1.s() != e2.s())
return false;

109
src/kernel/metavar.cpp
View file

@ -14,24 +14,8 @@ Author: Leonardo de Moura
#include "kernel/for_each.h"
namespace lean {
void substitution::inc_timestamp() {
if (m_timestamp == std::numeric_limits<unsigned>::max()) {
// This should not happen in real examples. We add it just to be safe.
throw exception("metavar_env timestamp overflow");
}
m_timestamp++;
}
substitution::substitution():
m_size(0),
m_timestamp(0) {
}
bool substitution::operator==(substitution const & s) const {
if (size() != s.size())
return false;
// TODO(Leo)
return true;
m_size(0) {
}
bool substitution::is_assigned(name const & m) const {
@ -45,7 +29,6 @@ bool substitution::is_assigned(expr const & m) const {
void substitution::assign(name const & m, expr const & t) {
lean_assert(!is_assigned(m));
m_subst.insert(m, t);
inc_timestamp();
m_size++;
}
@ -93,20 +76,94 @@ expr substitution::get_subst(expr const & m) const {
static name g_unique_name = name::mk_internal_unique_name();
metavar_generator::metavar_generator(name const & prefix):
m_gen(prefix) {
void metavar_env::inc_timestamp() {
if (m_timestamp == std::numeric_limits<unsigned>::max()) {
// This should not happen in real examples. We add it just to be safe.
throw exception("metavar_env timestamp overflow");
}
m_timestamp++;
}
metavar_generator::metavar_generator():
m_gen(g_unique_name) {
metavar_env::metavar_env(name const & prefix):
m_name_generator(prefix),
m_timestamp(0) {
}
expr metavar_generator::mk(expr const & t) {
return mk_metavar(m_gen.next(), t, local_context());
metavar_env::metavar_env():
metavar_env(g_unique_name) {
}
expr metavar_generator::mk() {
return mk(mk(expr()));
expr metavar_env::mk_metavar(context const & ctx, expr const & type) {
inc_timestamp();
name m = m_name_generator.next();
expr r = ::lean::mk_metavar(m);
if (ctx)
m_metavar_contexts.insert(m, ctx);
if (type)
m_metavar_types.insert(m, type);
return r;
}
context metavar_env::get_context(expr const & m) const {
lean_assert(is_metavar(m));
lean_assert(!has_local_context(m));
return get_context(metavar_name(m));
}
context metavar_env::get_context(name const & m) const {
auto e = const_cast<metavar_env*>(this)->m_metavar_contexts.splay_find(m);
if (e)
return e->second;
else
return context();
}
expr metavar_env::get_type(expr const & m) {
lean_assert(is_metavar(m));
expr t = get_type(metavar_name(m));
if (has_local_context(m)) {
if (is_metavar(t)) {
return update_metavar(t, append(metavar_lctx(m), metavar_lctx(t)));
} else {
return apply_local_context(t, metavar_lctx(m));
}
} else {
return t;
}
}
expr metavar_env::get_type(name const & m) {
auto e = const_cast<metavar_env*>(this)->m_metavar_types.splay_find(m);
if (e) {
return e->second;
} else {
expr t = mk_metavar(get_context(m));
m_metavar_types.insert(m, t);
return t;
}
}
bool metavar_env::is_assigned(name const & m) const {
return m_substitution.is_assigned(m);
}
bool metavar_env::is_assigned(expr const & m) const {
lean_assert(is_metavar(m));
return is_assigned(metavar_name(m));
}
void metavar_env::assign(name const & m, expr const & t, trace const & tr) {
lean_assert(!is_assigned(m));
inc_timestamp();
m_substitution.assign(m, t);
if (tr)
m_metavar_traces.insert(m, tr);
}
void metavar_env::assign(expr const & m, expr const & t, trace const & tr) {
lean_assert(is_metavar(m));
lean_assert(!has_local_context(m));
assign(metavar_name(m), t, tr);
}
expr instantiate_metavars(expr const & e, substitution const & s) {

84
src/kernel/metavar.h
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "util/name_generator.h"
#include "kernel/expr.h"
#include "kernel/context.h"
#include "kernel/trace.h"
namespace lean {
/**
@ -20,18 +21,9 @@ class substitution {
typedef splay_map<name, expr, name_cmp> name2expr;
name2expr m_subst;
unsigned m_size;
unsigned m_timestamp;
void inc_timestamp();
public:
substitution();
/**
\brief The timestamp is increased whenever the substitution is updated by
\c mk_metavar or \c assign.
*/
unsigned get_timestamp() const { return m_timestamp; }
/**
\brief Return the number of assigned metavariables in this substitution.
*/
@ -77,9 +69,6 @@ public:
*/
expr get_subst(expr const & m) const;
bool operator==(substitution const & s) const;
bool operator!=(substitution const & s) const { return !operator==(s); }
/**
\brief Apply f to each entry in this substitution.
*/
@ -98,15 +87,18 @@ public:
class metavar_env {
typedef splay_map<name, expr, name_cmp> name2expr;
typedef splay_map<name, context, name_cmp> name2context;
typedef splay_map<name, trace, name_cmp> name2trace;
name_generator m_name_generator;
substitution m_substitution;
name2expr m_metavar_types;
name2context m_metavar_contexts;
name2trace m_metavar_traces;
unsigned m_timestamp;
void inc_timestamp();
public:
metavar_env(name const & prefix);
metavar_env();
/**
@ -123,13 +115,19 @@ public:
/**
\brief Return the context where the given metavariable was created.
\pre is_metavar(m)
\pre !has_local_context(m)
*/
context get_context(expr const & m);
context get_context(name const & m);
context get_context(expr const & m) const;
context get_context(name const & m) const;
/**
\brief Return the type of the given metavariable.
\pre is_metavar(m)
\remark If \c m does not have a type associated with it, then a new
metavariable is created to represent the type of \c m.
\remark If \c m has a local context, then the local context is applied.
*/
expr get_type(expr const & m);
expr get_type(name const & m);
@ -152,7 +150,7 @@ public:
\pre !is_assigned(m)
*/
void assign(name const & m, expr const & t);
void assign(name const & m, expr const & t, trace const & tr = trace());
/**
\brief Assign metavariable \c m to \c t.
@ -161,12 +159,14 @@ public:
\pre !has_meta_context(m)
\pre !is_assigned(m)
*/
void assign(expr const & m, expr const & t);
void assign(expr const & m, expr const & t, trace const & tr = trace());
/**
\brief Return the set of substitutions.
*/
substitution const & get_substitutions() const;
substitution const & get_substitutions() const { return m_substitution; }
operator substitution const &() const { return get_substitutions(); }
/**
\brief Return the substitution associated with the given metavariable
@ -177,33 +177,7 @@ public:
\pre is_metavar(m)
*/
expr get_subst(expr const & m) const;
};
/**
\brief Metavar generator.
*/
class metavar_generator {
name_generator m_gen;
public:
metavar_generator(name const & prefix);
metavar_generator();
/**
\brief Return the prefix used to create metavariables in this generator.
*/
name const & prefix() const { return m_gen.prefix(); }
/**
\brief Create a metavariable with the given type.
*/
expr mk(expr const & t);
/**
\brief Create a metavariable where the type is another
metavariable. The type of the type is a null expression.
*/
expr mk();
expr get_subst(expr const & m) const { return m_substitution.get_subst(m); }
};
/**
@ -269,26 +243,4 @@ bool has_assigned_metavar(expr const & e, substitution const & s);
\brief is_metavar(m)
*/
bool has_metavar(expr const & e, expr const & m, substitution const & s = substitution());
/**
\brief Set of unification constraints that need to be solved.
It store two kinds of problems:
1. <tt>ctx |- lhs == rhs</tt>
2. <tt>ctx |- n : t</tt>
*/
class unification_constraints {
public:
virtual ~unification_constraints() {}
/**
\brief Add a new unification problem of the form <tt>ctx |- lhs == rhs</tt>
It means that rhs is convertible to lhs.
If rhs and lhs are not types, then this is just equality (modulo normalization).
*/
virtual void add(context const & ctx, expr const & lhs, expr const & rhs) = 0;
/**
\brief Add a new unification problem of the form <tt>ctx |- n : t</tt>
*/
virtual void add_type_of(context const & ctx, expr const & n, expr const & t) = 0;
};
}

38
src/kernel/normalizer.cpp
View file

@ -71,8 +71,8 @@ class normalizer::imp {
environment const & m_env;
context m_ctx;
substitution const * m_subst;
unsigned m_subst_timestamp;
metavar_env const * m_menv;
unsigned m_menv_timestamp;
cache m_cache;
unsigned m_max_depth;
unsigned m_depth;
@ -193,8 +193,8 @@ class normalizer::imp {
svalue r;
switch (a.kind()) {
case expr_kind::MetaVar:
if (m_subst && m_subst->is_assigned(a)) {
r = normalize(m_subst->get_subst(a), s, k);
if (m_menv && m_menv->is_assigned(a)) {
r = normalize(m_menv->get_subst(a), s, k);
} else {
r = svalue(updt_metavar(a, s, k));
}
@ -297,17 +297,17 @@ class normalizer::imp {
}
}
void set_subst(substitution const * subst) {
if (m_subst == subst) {
// Check whether m_subst has been updated since the last time the normalizer has been invoked
if (m_subst && m_subst->get_timestamp() > m_subst_timestamp) {
m_subst_timestamp = m_subst->get_timestamp();
void set_menv(metavar_env const * menv) {
if (m_menv == menv) {
// Check whether m_menv has been updated since the last time the normalizer has been invoked
if (m_menv && m_menv->get_timestamp() > m_menv_timestamp) {
m_menv_timestamp = m_menv->get_timestamp();
m_cache.clear();
}
} else {
m_subst = subst;
m_menv = menv;
m_cache.clear();
m_subst_timestamp = m_subst ? m_subst->get_timestamp() : 0;
m_menv_timestamp = m_menv ? m_menv->get_timestamp() : 0;
}
}
@ -317,18 +317,18 @@ public:
m_interrupted = false;
m_max_depth = max_depth;
m_depth = 0;
m_subst = nullptr;
m_subst_timestamp = 0;
m_menv = nullptr;
m_menv_timestamp = 0;
}
expr operator()(expr const & e, context const & ctx, substitution const * subst) {
expr operator()(expr const & e, context const & ctx, metavar_env const * menv) {
set_ctx(ctx);
set_subst(subst);
set_menv(menv);
unsigned k = m_ctx.size();
return reify(normalize(e, value_stack(), k), k);
}
void clear() { m_ctx = context(); m_cache.clear(); m_subst = nullptr; m_subst_timestamp = 0; }
void clear() { m_ctx = context(); m_cache.clear(); m_menv = nullptr; m_menv_timestamp = 0; }
void set_interrupt(bool flag) { m_interrupted = flag; }
};
@ -336,12 +336,12 @@ normalizer::normalizer(environment const & env, unsigned max_depth):m_ptr(new im
normalizer::normalizer(environment const & env):normalizer(env, std::numeric_limits<unsigned>::max()) {}
normalizer::normalizer(environment const & env, options const & opts):normalizer(env, get_normalizer_max_depth(opts)) {}
normalizer::~normalizer() {}
expr normalizer::operator()(expr const & e, context const & ctx, substitution const * subst) { return (*m_ptr)(e, ctx, subst); }
expr normalizer::operator()(expr const & e, context const & ctx, metavar_env const * menv) { return (*m_ptr)(e, ctx, menv); }
void normalizer::clear() { m_ptr->clear(); }
void normalizer::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
expr normalize(expr const & e, environment const & env, context const & ctx, substitution const * subst) {
return normalizer(env)(e, ctx, subst);
expr normalize(expr const & e, environment const & env, context const & ctx, metavar_env const * menv) {
return normalizer(env)(e, ctx, menv);
}
}

7
src/kernel/normalizer.h
View file

@ -13,8 +13,7 @@ Author: Leonardo de Moura
namespace lean {
class environment;
class options;
class substitution;
class unification_constraints;
class metavar_env;
/** \brief Functional object for normalizing expressions */
class normalizer {
class imp;
@ -25,7 +24,7 @@ public:
normalizer(environment const & env, options const & opts);
~normalizer();
expr operator()(expr const & e, context const & ctx = context(), substitution const * subst = nullptr);
expr operator()(expr const & e, context const & ctx = context(), metavar_env const * menv = nullptr);
void clear();
@ -34,5 +33,5 @@ public:
void reset_interrupt() { set_interrupt(false); }
};
/** \brief Normalize \c e using the environment \c env and context \c ctx */
expr normalize(expr const & e, environment const & env, context const & ctx = context(), substitution const * subst = nullptr);
expr normalize(expr const & e, environment const & env, context const & ctx = context(), metavar_env const * menv = nullptr);
}

200
src/kernel/type_checker.cpp
View file

@ -13,26 +13,26 @@ Author: Leonardo de Moura
#include "kernel/instantiate.h"
#include "kernel/builtin.h"
#include "kernel/free_vars.h"
#include "kernel/metavar.h"
#include "kernel/type_checker_trace.h"
namespace lean {
static name g_x_name("x");
/** \brief Auxiliary functional object used to implement infer_type. */
class type_checker::imp {
typedef scoped_map<expr, expr, expr_hash, expr_eqp> cache;
typedef buffer<unification_constraint> unification_constraints;
environment const & m_env;
cache m_cache;
normalizer m_normalizer;
context m_ctx;
substitution * m_subst;
unsigned m_subst_timestamp;
metavar_generator * m_mgen;
metavar_env * m_menv;
unsigned m_menv_timestamp;
unification_constraints * m_uc;
volatile bool m_interrupted;
expr normalize(expr const & e, context const & ctx) {
return m_normalizer(e, ctx, m_subst);
return m_normalizer(e, ctx, m_menv);
}
expr lookup(context const & c, unsigned i) {
@ -49,45 +49,35 @@ class type_checker::imp {
expr r = normalize(e, ctx);
if (is_pi(r))
return r;
if (has_metavar(r) && m_subst && m_uc && m_mgen) {
if (has_metavar(r) && m_menv) {
// Create two fresh variables A and B,
// and assign r == (Pi(x : A), B x)
expr A = m_mgen->mk();
expr B = m_mgen->mk();
expr A = m_menv->mk_metavar(ctx);
expr B = m_menv->mk_metavar(ctx);
expr p = mk_pi(g_x_name, A, B(Var(0)));
if (is_metavar(r) && !has_local_context(r)) {
// cheap case
m_subst->assign(r, p);
} else {
m_uc->add(ctx, r, p);
}
trace tr = mk_function_expected_trace(ctx, s);
m_uc->push_back(mk_eq_constraint(ctx, r, p, tr));
return p;
}
throw function_expected_exception(m_env, ctx, s);
}
level infer_universe_core(expr const & t, context const & ctx) {
expr u = normalize(infer_type_core(t, ctx), ctx);
expr check_type(expr const & e, expr const & s, context const & ctx) {
if (is_type(e))
return e;
if (e == Bool)
return Type();
expr u = normalize(e, ctx);
if (is_type(u))
return ty_level(u);
return u;
if (u == Bool)
return level();
if (has_metavar(u) && m_subst && m_uc) {
// Remark: in the current implementation we don't have level constraints and variables
// in the unification problem set. So, we assume the metavariable is in level 0.
// This is a crude approximation that works most of the time.
// A better solution is consists in creating a fresh universe level k and
// associate the constraint that u == Type k.
// Later the constraint must be solved in the elaborator.
if (is_metavar(u) && !has_local_context(u)) {
// cheap case
m_subst->assign(u, Type());
} else {
m_uc->add(ctx, u, Type());
return Type();
if (has_metavar(u) && m_menv) {
trace tr = mk_type_expected_trace(ctx, s);
m_uc->push_back(mk_convertible_constraint(ctx, u, TypeU, tr));
return u;
}
return level();
}
throw type_expected_exception(m_env, ctx, t);
throw type_expected_exception(m_env, ctx, s);
}
expr infer_type_core(expr const & e, context const & ctx) {
@ -103,9 +93,14 @@ class type_checker::imp {
expr r;
switch (e.kind()) {
case expr_kind::MetaVar:
r = metavar_type(e);
if (!r)
throw kernel_exception(m_env, "metavariable does not have a type associated with it");
if (m_menv) {
if (m_menv->is_assigned(e))
return infer_type_core(m_menv->get_subst(e), ctx);
else
return m_menv->get_type(e);
} else {
throw kernel_exception(m_env, "unexpected metavariable occurrence");
}
break;
case expr_kind::Constant:
r = m_env.get_object(const_name(e)).get_type();
@ -128,7 +123,8 @@ class type_checker::imp {
while (true) {
expr const & c = arg(e, i);
expr const & c_t = arg_types[i];
if (!is_convertible(c_t, abst_domain(f_t), ctx))
auto mk_trace = [&](){ return mk_app_type_match_trace(ctx, e, i); }; // thunk for creating trace object if needed
if (!is_convertible(c_t, abst_domain(f_t), ctx, mk_trace))
throw app_type_mismatch_exception(m_env, ctx, e, arg_types.size(), arg_types.data());
if (closed(abst_body(f_t)))
f_t = abst_body(f_t);
@ -151,7 +147,8 @@ class type_checker::imp {
r = mk_bool_type();
break;
case expr_kind::Lambda: {
infer_universe_core(abst_domain(e), ctx);
expr d = infer_type_core(abst_domain(e), ctx);
check_type(d, abst_domain(e), ctx);
expr t;
{
cache::mk_scope sc(m_cache);
@ -161,20 +158,30 @@ class type_checker::imp {
break;
}
case expr_kind::Pi: {
level l1 = infer_universe_core(abst_domain(e), ctx);
level l2;
expr t1 = check_type(infer_type_core(abst_domain(e), ctx), abst_domain(e), ctx);
expr t2;
{
cache::mk_scope sc(m_cache);
l2 = infer_universe_core(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)));
context new_ctx = extend(ctx, abst_name(e), abst_domain(e));
t2 = check_type(infer_type_core(abst_body(e), new_ctx), abst_body(e), new_ctx);
}
if (is_type(t1) && is_type(t2)) {
r = mk_type(max(ty_level(t1), ty_level(t2)));
} else {
lean_assert(m_uc);
trace tr = mk_max_type_trace(ctx, e);
r = m_menv->mk_metavar(ctx);
m_uc->push_back(mk_max_constraint(ctx, t1, t2, r, tr));
}
r = mk_type(max(l1, l2));
break;
}
case expr_kind::Let: {
expr lt = infer_type_core(let_value(e), ctx);
if (let_type(e)) {
infer_universe_core(let_type(e), ctx); // check if it is really a type
if (!is_convertible(lt, let_type(e), ctx))
expr ty = infer_type_core(let_type(e), ctx);
check_type(ty, let_type(e), ctx); // check if it is really a type
auto mk_trace = [&](){ return mk_def_type_match_trace(ctx, let_name(e), let_value(e)); }; // thunk for creating trace object if needed
if (!is_convertible(lt, let_type(e), ctx, mk_trace))
throw def_type_mismatch_exception(m_env, ctx, let_name(e), let_type(e), let_value(e), lt);
}
{
@ -228,34 +235,21 @@ class type_checker::imp {
}
}
bool is_convertible(expr const & given, expr const & expected, context const & ctx) {
template<typename MkTrace>
bool is_convertible(expr const & given, expr const & expected, context const & ctx, MkTrace const & mk_trace) {
if (is_convertible_core(given, expected))
return true;
expr new_given = given;
expr new_expected = expected;
if (has_metavar(new_given) || has_metavar(new_expected)) {
if (!m_subst)
return false;
new_given = instantiate_metavars(new_given, *m_subst);
new_expected = instantiate_metavars(new_expected, *m_subst);
expr new_given = normalize(given, ctx);
expr new_expected = normalize(expected, ctx);
if (is_convertible_core(new_given, new_expected))
return true;
if (has_metavar(new_given) || has_metavar(new_expected)) {
// Very conservative approach, just postpone the problem.
// We may also try to normalize new_given and new_expected even if
// they contain metavariables.
if (m_uc) {
m_uc->add(ctx, new_expected, new_given);
if (m_menv && (has_metavar(new_given) || has_metavar(new_expected))) {
m_uc->push_back(mk_convertible_constraint(ctx, new_given, new_expected, mk_trace()));
return true;
} else {
}
return false;
}
}
}
new_given = normalize(new_given, ctx);
new_expected = normalize(new_expected, ctx);
return is_convertible_core(new_given, new_expected);
}
void set_ctx(context const & ctx) {
if (!is_eqp(m_ctx, ctx)) {
@ -264,17 +258,17 @@ class type_checker::imp {
}
}
void set_subst(substitution * subst) {
if (m_subst == subst) {
// Check whether m_subst has been updated since the last time the normalizer has been invoked
if (m_subst && m_subst->get_timestamp() > m_subst_timestamp) {
void set_menv(metavar_env * menv) {
if (m_menv == menv) {
// Check whether m_menv has been updated since the last time the type checker has been invoked
if (m_menv && m_menv->get_timestamp() > m_menv_timestamp) {
clear();
m_subst_timestamp = m_subst->get_timestamp();
m_menv_timestamp = m_menv->get_timestamp();
}
} else {
clear();
m_subst = subst;
m_subst_timestamp = m_subst ? m_subst->get_timestamp() : 0;
m_menv = menv;
m_menv_timestamp = m_menv ? m_menv->get_timestamp() : 0;
}
}
@ -282,34 +276,31 @@ public:
imp(environment const & env):
m_env(env),
m_normalizer(env) {
m_subst = nullptr;
m_subst_timestamp = 0;
m_mgen = nullptr;
m_menv = nullptr;
m_menv_timestamp = 0;
m_uc = nullptr;
m_interrupted = false;
}
level infer_universe(expr const & t, context const & ctx, substitution * subst, metavar_generator * mgen, unification_constraints * uc) {
expr infer_type(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> & uc) {
set_ctx(ctx);
set_subst(subst);
flet<unification_constraints*> set_uc(m_uc, uc);
flet<metavar_generator*> set_mgen(m_mgen, mgen);
return infer_universe_core(t, ctx);
}
expr infer_type(expr const & e, context const & ctx, substitution * subst, metavar_generator * mgen, unification_constraints * uc) {
set_ctx(ctx);
set_subst(subst);
flet<unification_constraints*> set_uc(m_uc, uc);
flet<metavar_generator*> set_mgen(m_mgen, mgen);
set_menv(menv);
flet<unification_constraints*> set_uc(m_uc, &uc);
return infer_type_core(e, ctx);
}
bool is_convertible(expr const & t1, expr const & t2, context const & ctx, substitution * subst, unification_constraints * uc) {
bool is_convertible(expr const & t1, expr const & t2, context const & ctx) {
set_ctx(ctx);
set_subst(subst);
flet<unification_constraints*> set_uc(m_uc, uc);
return is_convertible(t1, t2, ctx);
set_menv(nullptr);
auto mk_trace = [](){ lean_unreachable(); return trace(); };
return is_convertible(t1, t2, ctx, mk_trace);
}
void check_type(expr const & e, context const & ctx) {
set_ctx(ctx);
set_menv(nullptr);
expr t = infer_type_core(e, ctx);
check_type(t, e, ctx);
}
void set_interrupt(bool flag) {
@ -321,8 +312,8 @@ public:
m_cache.clear();
m_normalizer.clear();
m_ctx = context();
m_subst = nullptr;
m_subst_timestamp = 0;
m_menv = nullptr;
m_menv_timestamp = 0;
}
normalizer & get_normalizer() {
@ -332,24 +323,27 @@ public:
type_checker::type_checker(environment const & env):m_ptr(new imp(env)) {}
type_checker::~type_checker() {}
expr type_checker::infer_type(expr const & e, context const & ctx, substitution * subst, metavar_generator * mgen, unification_constraints * uc) {
return m_ptr->infer_type(e, ctx, subst, mgen, uc);
expr type_checker::infer_type(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> & uc) {
return m_ptr->infer_type(e, ctx, menv, uc);
}
level type_checker::infer_universe(expr const & e, context const & ctx, substitution * subst, metavar_generator * mgen, unification_constraints * uc) {
return m_ptr->infer_universe(e, ctx, subst, mgen, uc);
expr type_checker::infer_type(expr const & e, context const & ctx) {
buffer<unification_constraint> uc;
return infer_type(e, ctx, nullptr, uc);
}
bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx) {
return m_ptr->is_convertible(t1, t2, ctx);
}
void type_checker::check_type(expr const & e, context const & ctx) {
m_ptr->check_type(e, ctx);
}
void type_checker::clear() { m_ptr->clear(); }
void type_checker::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx, substitution * subst, unification_constraints * uc) {
return m_ptr->is_convertible(t1, t2, ctx, subst, uc);
}
normalizer & type_checker::get_normalizer() { return m_ptr->get_normalizer(); }
expr infer_type(expr const & e, environment const & env, context const & ctx) {
return type_checker(env).infer_type(e, ctx);
}
bool is_convertible(expr const & given, expr const & expected, environment const & env, context const & ctx,
substitution * subst, unification_constraints * uc) {
return type_checker(env).is_convertible(given, expected, ctx, subst, uc);
bool is_convertible(expr const & given, expr const & expected, environment const & env, context const & ctx) {
return type_checker(env).is_convertible(given, expected, ctx);
}
}

57
src/kernel/type_checker.h
View file

@ -8,13 +8,12 @@ Author: Leonardo de Moura
#include <memory>
#include "kernel/expr.h"
#include "kernel/context.h"
#include "kernel/unification_constraint.h"
#include "kernel/metavar.h"
namespace lean {
class environment;
class normalizer;
class substitution;
class metavar_generator;
class unification_constraints;
/**
\brief Lean Type Checker. It can also be used to infer types, universes and check whether a
type \c A is convertible to a type \c B.
@ -26,42 +25,46 @@ public:
type_checker(environment const & env);
~type_checker();
expr infer_type(expr const & e,
context const & ctx = context(),
substitution * subst = nullptr,
metavar_generator * mgen = nullptr,
unification_constraints * uc = nullptr);
/**
\brief Return the type of \c e in the context \c ctx.
level infer_universe(expr const & e,
context const & ctx = context(),
substitution * subst = nullptr,
metavar_generator * mgen = nullptr,
unification_constraints * uc = nullptr);
\remark This method throws an exception if \c e is not type correct.
void check(expr const & e,
context const & ctx = context(),
substitution * subst = nullptr,
metavar_generator * mgen = nullptr,
unification_constraints * uc = nullptr) {
infer_type(e, ctx, subst, mgen, uc);
}
\remark If \c menv is not nullptr, then \c e may contain metavariables.
New metavariables and unification constraints may be created by the type checker.
The new unification constraints are stored in \c new_constraints.
*/
expr infer_type(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> & new_constraints);
bool is_convertible(expr const & t1,
expr const & t2,
context const & ctx = context(),
substitution * subst = nullptr,
unification_constraints * uc = nullptr);
/**
\brief Return the type of \c e in the context \c ctx.
\remark This method throws an exception if \c e is not type
correct, or if \c e contains metavariables.
*/
expr infer_type(expr const & e, context const & ctx = context());
/** \brief Throw an exception if \c e is not type correct in the context \c ctx. */
void check(expr const & e, context const & ctx = context()) { infer_type(e, ctx); }
/** \brief Throw an exception if \c e is not a type in the context \c ctx. */
void check_type(expr const & e, context const & ctx = context());
/** \brief Return true iff \c t1 is convertible to \c t2 in the context \c ctx. */
bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context());
/** \brief Reset internal caches */
void clear();
/** \brief Interrupt type checker */
void set_interrupt(bool flag);
void interrupt() { set_interrupt(true); }
void reset_interrupt() { set_interrupt(false); }
/** \brief Return reference to the normalizer used by this type checker. */
normalizer & get_normalizer();
};
expr infer_type(expr const & e, environment const & env, context const & ctx = context());
bool is_convertible(expr const & t1, expr const & t2, environment const & env, context const & ctx = context(),
substitution * subst = nullptr, unification_constraints * uc = nullptr);
bool is_convertible(expr const & t1, expr const & t2, environment const & env, context const & ctx = context());
}

98
src/kernel/unification_constraint.cpp
View file

@ -10,22 +10,37 @@ namespace lean {
unification_constraint_cell::unification_constraint_cell(unification_constraint_kind k, context const & c, trace const & t):
m_kind(k), m_ctx(c), m_trace(t), m_rc(1) {
}
void unification_constraint_cell::dealloc() {
switch (m_kind) {
case unification_constraint_kind::Eq:
delete static_cast<unification_constraint_eq*>(this);
break;
case unification_constraint_kind::Convertible:
delete static_cast<unification_constraint_convertible*>(this);
break;
case unification_constraint_kind::Max:
delete static_cast<unification_constraint_max*>(this);
break;
case unification_constraint_kind::Choice:
static_cast<unification_constraint_choice*>(this)->~unification_constraint_choice();
delete[] reinterpret_cast<char*>(this);
break;
unification_constraint_cell::~unification_constraint_cell() {
}
void unification_constraint_cell::dealloc() {
delete this;
}
static format add_context(formatter const & fmt, options const & opts, context const & ctx, format const & body) {
bool unicode = get_pp_unicode(opts);
format ctx_fmt = fmt(ctx, opts);
format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-");
return group(format{ctx_fmt, space(), turnstile, line(), body});
}
static format add_trace(formatter const & fmt, options const & opts, format const & body, trace const & tr, bool include_trace) {
if (include_trace) {
unsigned indent = get_pp_indent(opts);
return format{body, line(), format("Trace:"), nest(indent, compose(line(), tr.pp(fmt, opts)))};
} else {
return body;
}
}
static format mk_binary(formatter const & fmt, options const & opts, context const & ctx, expr const & lhs, expr const & rhs, format const & op) {
format lhs_fmt = fmt(ctx, lhs, false, opts);
format rhs_fmt = fmt(ctx, rhs, false, opts);
return group(format{lhs_fmt, space(), op, line(), rhs_fmt});
}
static format mk_unification_op(options const & opts) {
bool unicode = get_pp_unicode(opts);
return unicode ? format("\u2248") /* ≈ */ : format("=?=");
}
unification_constraint_eq::unification_constraint_eq(context const & c, expr const & lhs, expr const & rhs, trace const & t):
@ -34,12 +49,33 @@ unification_constraint_eq::unification_constraint_eq(context const & c, expr con
m_rhs(rhs) {
}
unification_constraint_eq::~unification_constraint_eq() {
}
format unification_constraint_eq::pp(formatter const & fmt, options const & opts, bool include_trace) const {
format op = mk_unification_op(opts);
format body = mk_binary(fmt, opts, m_ctx, m_lhs, m_rhs, op);
body = add_context(fmt, opts, m_ctx, body);
return add_trace(fmt, opts, body, m_trace, include_trace);
}
unification_constraint_convertible::unification_constraint_convertible(context const & c, expr const & from, expr const & to, trace const & t):
unification_constraint_cell(unification_constraint_kind::Convertible, c, t),
m_from(from),
m_to(to) {
}
unification_constraint_convertible::~unification_constraint_convertible() {
}
format unification_constraint_convertible::pp(formatter const & fmt, options const & opts, bool include_trace) const {
bool unicode = get_pp_unicode(opts);
format op = unicode ? format("\u227A") /* ≺ */ : format("<<");
format body = mk_binary(fmt, opts, m_ctx, m_from, m_to, op);
body = add_context(fmt, opts, m_ctx, body);
return add_trace(fmt, opts, body, m_trace, include_trace);
}
unification_constraint_max::unification_constraint_max(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t):
unification_constraint_cell(unification_constraint_kind::Max, c, t),
m_lhs1(lhs1),
@ -47,12 +83,44 @@ unification_constraint_max::unification_constraint_max(context const & c, expr c
m_rhs(rhs) {
}
unification_constraint_max::~unification_constraint_max() {
}
format unification_constraint_max::pp(formatter const & fmt, options const & opts, bool include_trace) const {
format op = mk_unification_op(opts);
format lhs1_fmt = fmt(m_ctx, m_lhs1, false, opts);
format lhs2_fmt = fmt(m_ctx, m_lhs2, false, opts);
format rhs_fmt = fmt(m_ctx, m_rhs, false, opts);
format body = group(format{format("max"), lp(), lhs1_fmt, comma(), nest(4, compose(line(), lhs2_fmt)), space(), op, line(), rhs_fmt});
body = add_context(fmt, opts, m_ctx, body);
return add_trace(fmt, opts, body, m_trace, include_trace);
}
unification_constraint_choice::unification_constraint_choice(context const & c, expr const & mvar, unsigned num, trace const & t):
unification_constraint_cell(unification_constraint_kind::Choice, c, t),
m_mvar(mvar),
m_num_choices(num) {
}
unification_constraint_choice::~unification_constraint_choice() {
}
format unification_constraint_choice::pp(formatter const & fmt, options const & opts, bool include_trace) const {
bool unicode = get_pp_unicode(opts);
format m_fmt = fmt(m_ctx, m_mvar, false, opts);
format eq_op = mk_unification_op(opts);
format or_op = unicode ? format("\u2295") : format("OR");
format body;
for (unsigned i = 0; i < m_num_choices; i++) {
body += format{m_fmt, eq_op, fmt(m_ctx, m_choices[i], false, opts)};
if (i + 1 < m_num_choices)
body += format{space(), or_op, line()};
}
body = group(body);
body = add_context(fmt, opts, m_ctx, body);
return add_trace(fmt, opts, body, m_trace, include_trace);
}
unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, trace const & t) {
return unification_constraint(new unification_constraint_eq(c, lhs, rhs, t));
}

40
src/kernel/unification_constraint.h
View file

@ -34,6 +34,7 @@ enum class unification_constraint_kind { Eq, Convertible, Max, Choice };
\brief Base class for all Lean unification constraints.
*/
class unification_constraint_cell {
protected:
unification_constraint_kind m_kind;
context m_ctx;
trace m_trace; //!< justification for this constraint
@ -41,9 +42,11 @@ class unification_constraint_cell {
void dealloc();
public:
unification_constraint_cell(unification_constraint_kind k, context const & c, trace const & t);
virtual ~unification_constraint_cell();
unification_constraint_kind kind() const { return m_kind; }
trace const & get_trace() const { return m_trace; }
context const & get_context() const { return m_ctx; }
virtual format pp(formatter const & fmt, options const & opts, bool include_trace = false) const = 0;
};
class unification_constraint {
@ -66,6 +69,11 @@ public:
operator bool() const { return m_ptr != nullptr; }
format pp(formatter const & fmt, options const & opts, bool include_trace = false) const {
lean_assert(m_ptr);
return m_ptr->pp(fmt, opts, include_trace);
}
friend unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, trace const & t);
friend unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, trace const & t);
friend unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t);
@ -80,8 +88,10 @@ class unification_constraint_eq : public unification_constraint_cell {
expr m_rhs;
public:
unification_constraint_eq(context const & c, expr const & lhs, expr const & rhs, trace const & t);
virtual ~unification_constraint_eq();
expr const & get_lhs() const { return m_lhs; }
expr const & get_rhs() const { return m_rhs; }
virtual format pp(formatter const & fmt, options const & opts, bool include_trace = false) const;
};
/**
@ -94,8 +104,10 @@ class unification_constraint_convertible : public unification_constraint_cell {
expr m_to;
public:
unification_constraint_convertible(context const & c, expr const & from, expr const & to, trace const & t);
virtual ~unification_constraint_convertible();
expr const & get_from() const { return m_from; }
expr const & get_to() const { return m_to; }
virtual format pp(formatter const & fmt, options const & opts, bool include_trace = false) const;
};
/**
@ -107,9 +119,11 @@ class unification_constraint_max : public unification_constraint_cell {
expr m_rhs;
public:
unification_constraint_max(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t);
virtual ~unification_constraint_max();
expr const & get_lhs1() const { return m_lhs1; }
expr const & get_lhs2() const { return m_lhs2; }
expr const & get_rhs() const { return m_rhs; }
virtual format pp(formatter const & fmt, options const & opts, bool include_trace = false) const;
};
/**
@ -122,11 +136,13 @@ class unification_constraint_choice : public unification_constraint_cell {
friend unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, trace const & t);
public:
unification_constraint_choice(context const & c, expr const & mvar, unsigned num, trace const & t);
virtual ~unification_constraint_choice();
expr const & get_mvar() const { return m_mvar; }
unsigned get_num_choices() const { return m_num_choices; }
expr const & get_choice(unsigned idx) const { lean_assert(idx < m_num_choices); return m_choices[idx]; }
expr const * begin_choices() const { return m_choices; }
expr const * end_choices() const { return m_choices + m_num_choices; }
virtual format pp(formatter const & fmt, options const & opts, bool include_trace = false) const;
};
unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, trace const & t);
@ -145,16 +161,16 @@ inline unification_constraint_convertible * to_convertible(unification_constrain
inline unification_constraint_max * to_max(unification_constraint const & c) { lean_assert(is_max(c)); return static_cast<unification_constraint_max*>(c.raw()); }
inline unification_constraint_choice * to_choice(unification_constraint const & c) { lean_assert(is_choice(c)); return static_cast<unification_constraint_choice*>(c.raw()); }
context const & get_context(unification_constraint const & c) { return c.raw()->get_context(); }
trace const & get_trace(unification_constraint const & c) { return c.raw()->get_trace(); }
expr const & eq_lhs(unification_constraint const & c) { return to_eq(c)->get_lhs(); }
expr const & eq_rhs(unification_constraint const & c) { return to_eq(c)->get_rhs(); }
expr const & convertible_from(unification_constraint const & c) { return to_convertible(c)->get_from(); }
expr const & convertible_to(unification_constraint const & c) { return to_convertible(c)->get_to(); }
expr const & max_lhs1(unification_constraint const & c) { return to_max(c)->get_lhs1(); }
expr const & max_lhs2(unification_constraint const & c) { return to_max(c)->get_lhs2(); }
expr const & max_rhs(unification_constraint const & c) { return to_max(c)->get_rhs(); }
expr const & choice_mvar(unification_constraint const & c) { return to_choice(c)->get_mvar(); }
unsigned choice_size(unification_constraint const & c) { return to_choice(c)->get_num_choices(); }
expr const & choice_ith(unification_constraint const & c, unsigned i) { return to_choice(c)->get_choice(i); }
inline context const & get_context(unification_constraint const & c) { return c.raw()->get_context(); }
inline trace const & get_trace(unification_constraint const & c) { return c.raw()->get_trace(); }
inline expr const & eq_lhs(unification_constraint const & c) { return to_eq(c)->get_lhs(); }
inline expr const & eq_rhs(unification_constraint const & c) { return to_eq(c)->get_rhs(); }
inline expr const & convertible_from(unification_constraint const & c) { return to_convertible(c)->get_from(); }
inline expr const & convertible_to(unification_constraint const & c) { return to_convertible(c)->get_to(); }
inline expr const & max_lhs1(unification_constraint const & c) { return to_max(c)->get_lhs1(); }
inline expr const & max_lhs2(unification_constraint const & c) { return to_max(c)->get_lhs2(); }
inline expr const & max_rhs(unification_constraint const & c) { return to_max(c)->get_rhs(); }
inline expr const & choice_mvar(unification_constraint const & c) { return to_choice(c)->get_mvar(); }
inline unsigned choice_size(unification_constraint const & c) { return to_choice(c)->get_num_choices(); }
inline expr const & choice_ith(unification_constraint const & c, unsigned i) { return to_choice(c)->get_choice(i); }
}

30
src/library/ho_unifier.cpp
View file

@ -327,25 +327,6 @@ class ho_unifier::imp {
return is_meta_app(a) && has_local_context(arg(a, 0));
}
/**
Auxiliary class for invoking m_type_infer.
If it creates a new unfication problem we mark m_failed to true.
add_eq can be easily supported, but we need to extend ho_unifier API to be able
to support add_type_of_eq and add_is_convertible.
The m_type_infer only invokes add_type_of_eq when it needs to ask for the type
of a metavariable that does not have a type yet.
One possible workaround it o make sure that every metavariable has an associated type
before invoking ho_unifier.
*/
class unification_constraints_wrapper : public unification_constraints {
bool m_failed;
public:
unification_constraints_wrapper():m_failed(false) {}
virtual void add(context const &, expr const &, expr const &) { m_failed = true; }
virtual void add_type_of(context const &, expr const &, expr const &) { m_failed = true; }
bool failed() const { return m_failed; }
};
expr mk_lambda(name const & n, expr const & d, expr const & b) {
return ::lean::mk_lambda(n, d, b);
}
@ -382,7 +363,9 @@ class ho_unifier::imp {
We perform a "case split" using "projection" or "imitation". See Huet&Lang's paper on higher order matching
for further details.
*/
bool process_meta_app(context const & ctx, expr const & a, expr const & b) {
bool process_meta_app(context const & /* ctx */, expr const & /* a */, expr const & /* b */) {
return true;
#if 0
lean_assert(is_meta_app(a));
lean_assert(!has_local_context(arg(a, 0)));
lean_assert(!is_meta_app(b));
@ -394,7 +377,7 @@ class ho_unifier::imp {
substitution s = subst_of(top_state);
name const & mname = metavar_name(f_a);
unsigned num_a = num_args(a);
unification_constraints_wrapper ucw;
// unification_constraints_wrapper ucw;
buffer<expr> arg_types;
for (unsigned i = 1; i < num_a; i++) {
arg_types.push_back(m_type_infer(arg(a, i), ctx, &s, &ucw));
@ -464,6 +447,7 @@ class ho_unifier::imp {
m_state_stack.push_back(mk_state(new_s, new_q));
reset_delayed();
return true;
#endif
}
/** \brief Return true if \c a is of the form ?m[inst:i t, ...] */
@ -621,8 +605,8 @@ class ho_unifier::imp {
return true;
}
expr norm_a = m_normalizer(a, ctx, &s);
expr norm_b = m_normalizer(b, ctx, &s);
expr norm_a; // = m_normalizer(a, ctx, &s);
expr norm_b; // = m_normalizer(b, ctx, &s);
if (norm_a.kind() != norm_b.kind())
return false;
if (is_app(norm_a)) {

58
src/library/light_checker.cpp
View file

@ -19,11 +19,12 @@ Author: Leonardo de Moura
namespace lean {
class light_checker::imp {
typedef scoped_map<expr, expr, expr_hash, expr_eqp> cache;
typedef buffer<unification_constraint> unification_constraints;
environment m_env;
context m_ctx;
substitution * m_subst;
unsigned m_subst_timestamp;
metavar_env * m_menv;
unsigned m_menv_timestamp;
unification_constraints * m_uc;
normalizer m_normalizer;
cache m_cache;
@ -31,11 +32,12 @@ class light_checker::imp {
level infer_universe(expr const & t, context const & ctx) {
expr u = m_normalizer(infer_type(t, ctx), ctx);
expr u = m_normalizer(infer_type(t, ctx), ctx, m_menv);
if (is_type(u))
return ty_level(u);
if (u == Bool)
return level();
// TODO(Leo): case when u has metavariables
throw type_expected_exception(m_env, ctx, t);
}
@ -50,6 +52,7 @@ class light_checker::imp {
if (is_pi(t)) {
t = abst_body(t);
} else {
// TODO(Leo): case when t has metavariables
throw function_expected_exception(m_env, ctx, e);
}
}
@ -60,28 +63,31 @@ class light_checker::imp {
return instantiate(t, num_args(e)-1, &arg(e, 1));
}
void set_subst(substitution * subst) {
if (m_subst == subst) {
// Check whether m_subst has been updated since the last time the normalizer has been invoked
if (m_subst && m_subst->get_timestamp() > m_subst_timestamp) {
m_subst_timestamp = m_subst->get_timestamp();
void set_menv(metavar_env * menv) {
if (m_menv == menv) {
// Check whether m_menv has been updated since the last time the checker has been invoked
if (m_menv && m_menv->get_timestamp() > m_menv_timestamp) {
m_menv_timestamp = m_menv->get_timestamp();
m_cache.clear();
}
} else {
m_subst = subst;
m_menv = menv;
m_cache.clear();
m_subst_timestamp = m_subst ? m_subst->get_timestamp() : 0;
m_menv_timestamp = m_menv ? m_menv->get_timestamp() : 0;
}
}
expr infer_type(expr const & e, context const & ctx) {
// cheap cases, we do not cache results
switch (e.kind()) {
case expr_kind::MetaVar: {
expr r = metavar_type(e);
if (!r)
throw kernel_exception(m_env, "metavariable does not have a type associated with it");
return r;
case expr_kind::MetaVar:
if (m_menv) {
if (m_menv->is_assigned(e))
return infer_type(m_menv->get_subst(e), ctx);
else
return m_menv->get_type(e);
} else {
throw kernel_exception(m_env, "unexpected metavariable occurrence");
}
case expr_kind::Constant: {
object const & obj = m_env.get_object(const_name(e));
@ -178,15 +184,15 @@ public:
m_env(env),
m_normalizer(env) {
m_interrupted = false;
m_subst = nullptr;
m_subst_timestamp = 0;
m_menv = nullptr;
m_menv_timestamp = 0;
m_uc = nullptr;
}
expr operator()(expr const & e, context const & ctx, substitution * subst, unification_constraints * uc) {
expr operator()(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> & uc) {
set_ctx(ctx);
set_subst(subst);
flet<unification_constraints*> set(m_uc, uc);
set_menv(menv);
flet<unification_constraints*> set(m_uc, &uc);
return infer_type(e, ctx);
}
@ -199,14 +205,18 @@ public:
m_cache.clear();
m_normalizer.clear();
m_ctx = context();
m_subst = nullptr;
m_subst_timestamp = 0;
m_menv = nullptr;
m_menv_timestamp = 0;
}
};
light_checker::light_checker(environment const & env):m_ptr(new imp(env)) {}
light_checker::~light_checker() {}
expr light_checker::operator()(expr const & e, context const & ctx, substitution * subst, unification_constraints * uc) {
return m_ptr->operator()(e, ctx, subst, uc);
expr light_checker::operator()(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> & uc) {
return m_ptr->operator()(e, ctx, menv, uc);
}
expr light_checker::operator()(expr const & e, context const & ctx) {
buffer<unification_constraint> uc;
return operator()(e, ctx, nullptr, uc);
}
void light_checker::clear() { m_ptr->clear(); }
void light_checker::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }

8
src/library/light_checker.h
View file

@ -6,13 +6,14 @@ Author: Leonardo de Moura
*/
#pragma once
#include <memory>
#include "util/buffer.h"
#include "kernel/expr.h"
#include "kernel/context.h"
#include "kernel/unification_constraint.h"
namespace lean {
class environment;
class substitution;
class unification_constraints;
class metavar_env;
/**
\brief Functional object for "quickly" inferring the type of expressions.
It does not check whether the input expression is type correct or not.
@ -30,7 +31,8 @@ public:
light_checker(environment const & env);
~light_checker();
expr operator()(expr const & e, context const & ctx = context(), substitution * subst = nullptr, unification_constraints * uc = nullptr);
expr operator()(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> & uc);
expr operator()(expr const & e, context const & ctx = context());
void clear();

14
src/library/placeholder.cpp
View file

@ -7,7 +7,7 @@ Author: Leonardo de Moura
#include "kernel/occurs.h"
#include "kernel/metavar.h"
#include "kernel/expr_maps.h"
#include "kernel/replace.h"
#include "library/replace_using_ctx.h"
#include "library/placeholder.h"
namespace lean {
@ -24,18 +24,18 @@ bool has_placeholder(expr const & e) {
return occurs(mk_placholder(), e);
}
expr replace_placeholders_with_metavars(expr const & e, metavar_generator & mgen, expr_map<expr> * trace) {
auto f = [&](expr const & e, unsigned) -> expr {
expr replace_placeholders_with_metavars(expr const & e, metavar_env & menv, expr_map<expr> * new2old) {
auto f = [&](expr const & e, context const & c, unsigned) -> expr {
if (is_placeholder(e)) {
return mgen.mk();
return menv.mk_metavar(c);
} else {
return e;
}
};
auto p = [&](expr const & s, expr const & t) {
if (trace)
(*trace)[t] = s;
if (new2old)
(*new2old)[t] = s;
};
return replace_fn<decltype(f), decltype(p)>(f, p)(e);
return replace_using_ctx_fn<decltype(f), decltype(p)>(f, p)(e);
}
}

11
src/library/placeholder.h
View file

@ -9,8 +9,7 @@ Author: Leonardo de Moura
#include "kernel/expr_maps.h"
namespace lean {
class substitution;
class metavar_generator;
class metavar_env;
/**
\brief Return a new placeholder expression. To be able to track location,
a new constant for each placeholder.
@ -28,9 +27,9 @@ bool is_placeholder(expr const & e);
bool has_placeholder(expr const & e);
/**
\brief Replace the placeholders in \c e with fresh metavariables from \c mgen.
if \c trace is not null, then for each new expression \c t created based on
\c s, we store <tt>(*trace)[t] = s</tt>. We say this is traceability information.
\brief Replace the placeholders in \c e with fresh metavariables from \c menv.
if \c new2old is not nullptr, then for each new expression \c t created based on
\c s, we store <tt>(*new2old)[t] = s</tt>.
*/
expr replace_placeholders_with_metavars(expr const & e, metavar_generator & mgen, expr_map<expr> * trace = nullptr);
expr replace_placeholders_with_metavars(expr const & e, metavar_env & menv, expr_map<expr> * new2old = nullptr);
}

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

@ -17,32 +17,13 @@ Author: Leonardo de Moura
#include "kernel/environment.h"
#include "kernel/type_checker.h"
#include "kernel/printer.h"
#include "kernel/kernel_exception.h"
#include "library/placeholder.h"
#include "library/state.h"
#include "library/arith/arith.h"
#include "library/all/all.h"
using namespace lean;
class unification_constraints_dbg : public unification_constraints {
typedef std::tuple<context, expr, expr> constraint;
typedef std::vector<constraint> constraints;
constraints m_eqs;
constraints m_type_of_eqs;
public:
unification_constraints_dbg() {}
virtual ~unification_constraints_dbg() {}
virtual void add(context const & ctx, expr const & lhs, expr const & rhs) { m_eqs.push_back(constraint(ctx, lhs, rhs)); }
virtual void add_type_of(context const & ctx, expr const & n, expr const & t) { m_type_of_eqs.push_back(constraint(ctx, n, t)); }
constraints const & eqs() const { return m_eqs; }
constraints const & type_of_eqs() const { return m_type_of_eqs; }
friend std::ostream & operator<<(std::ostream & out, unification_constraints_dbg const & uc) {
for (auto c : uc.m_eqs)
std::cout << std::get<0>(c) << " |- " << std::get<1>(c) << " == " << std::get<2>(c) << "\n";
for (auto c : uc.m_type_of_eqs)
std::cout << std::get<0>(c) << " |- " << std::get<1>(c) << " : " << std::get<2>(c) << "\n";
return out;
}
};
std::ostream & operator<<(std::ostream & out, substitution const & env) {
bool first = true;
env.for_each([&](name const & n, expr const & v) {
@ -52,82 +33,86 @@ std::ostream & operator<<(std::ostream & out, substitution const & env) {
return out;
}
std::ostream & operator<<(std::ostream & out, buffer<unification_constraint> const & uc) {
formatter fmt = mk_simple_formatter();
for (auto c : uc) {
out << c.pp(fmt, options(), true) << "\n";
}
return out;
}
static void tst1() {
substitution subst;
metavar_generator gen;
expr m1 = gen.mk();
lean_assert(!subst.is_assigned(m1));
expr t1 = metavar_type(m1);
metavar_env menv;
expr m1 = menv.mk_metavar();
lean_assert(!menv.is_assigned(m1));
expr t1 = menv.get_type(m1);
lean_assert(is_metavar(t1));
lean_assert(is_eqp(metavar_type(m1), t1));
lean_assert(is_eqp(metavar_type(m1), t1));
lean_assert(!subst.is_assigned(m1));
expr m2 = gen.mk();
lean_assert(!subst.is_assigned(m1));
expr t2 = metavar_type(m2);
lean_assert(is_eqp(menv.get_type(m1), t1));
lean_assert(is_eqp(menv.get_type(m1), t1));
lean_assert(!menv.is_assigned(m1));
expr m2 = menv.mk_metavar();
lean_assert(!menv.is_assigned(m1));
expr t2 = menv.get_type(m2);
lean_assert(is_metavar(m2));
lean_assert(!is_eqp(t1, t2));
lean_assert(t1 != t2);
expr f = Const("f");
expr a = Const("a");
subst.assign(m1, f(a));
lean_assert(subst.is_assigned(m1));
lean_assert(!subst.is_assigned(m2));
lean_assert(subst.get_subst(m1) == f(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() {
substitution subst;
metavar_generator gen;
metavar_env menv;
expr f = Const("f");
expr g = Const("g");
expr h = Const("h");
expr a = Const("a");
expr m1 = gen.mk();
expr m2 = gen.mk();
expr m1 = menv.mk_metavar();
expr m2 = menv.mk_metavar();
// move m1 to a different context, and store new metavariable + context in m11
std::cout << "---------------------\n";
expr m11 = add_inst(m1, 0, f(a, m2));
std::cout << m11 << "\n";
subst.assign(m1, f(Var(0)));
std::cout << instantiate_metavars(m11, subst) << "\n";
subst.assign(m2, g(a, Var(1)));
std::cout << instantiate_metavars(h(m11), subst) << "\n";
lean_assert(instantiate_metavars(h(m11), subst) == h(f(f(a, g(a, Var(1))))));
menv.assign(m1, f(Var(0)));
std::cout << instantiate_metavars(m11, menv) << "\n";
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(1))))));
}
static void tst3() {
substitution subst;
metavar_generator gen;
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 = gen.mk();
expr m1 = menv.mk_metavar();
expr F = Fun({x, T}, f(m1, x));
subst.assign(m1, h(Var(0), Var(2)));
menv.assign(m1, h(Var(0), Var(2)));
std::cout << instantiate(abst_body(F), g(a)) << "\n";
std::cout << instantiate_metavars(instantiate(abst_body(F), g(a)), subst) << "\n";
lean_assert(instantiate_metavars(instantiate(abst_body(F), g(a)), subst) == f(h(g(a), Var(1)), g(a)));
std::cout << instantiate(instantiate_metavars(abst_body(F), subst), g(a)) << "\n";
lean_assert(instantiate(instantiate_metavars(abst_body(F), subst), g(a)) ==
instantiate_metavars(instantiate(abst_body(F), g(a)), subst));
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() {
substitution subst;
metavar_generator gen;
metavar_env menv;
expr f = Const("f");
expr g = Const("g");
expr h = Const("h");
expr a = Const("a");
expr m1 = gen.mk();
expr m1 = menv.mk_metavar();
expr F = f(m1, Var(2));
subst.assign(m1, h(Var(1)));
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)}), subst) << "\n";
std::cout << instantiate_metavars(instantiate(F, {g(Var(0)), h(a)}), menv) << "\n";
}
static void tst5() {
@ -142,18 +127,17 @@ static void tst6() {
expr a = Const("a");
expr g = Const("g");
expr h = Const("h");
substitution subst;
metavar_generator gen;
expr m1 = gen.mk();
expr m2 = gen.mk();
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;
subst.assign(m2, Var(2));
r = instantiate_metavars(r, subst);
menv.assign(m2, Var(2));
r = instantiate_metavars(r, menv);
std::cout << r << std::endl;
subst.assign(m1, h(Var(3)));
r = instantiate_metavars(r, subst);
menv.assign(m1, 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))))));
}
@ -162,13 +146,12 @@ static void tst7() {
expr f = Const("f");
expr g = Const("g");
expr a = Const("a");
substitution subst;
metavar_generator gen;
expr m1 = gen.mk();
metavar_env menv;
expr m1 = menv.mk_metavar();
expr t = f(m1, Var(0));
expr r = instantiate(t, a);
subst.assign(m1, g(Var(0)));
r = instantiate_metavars(r, subst);
menv.assign(m1, g(Var(0)));
r = instantiate_metavars(r, menv);
std::cout << r << std::endl;
lean_assert(r == f(g(a), a));
}
@ -177,13 +160,12 @@ static void tst8() {
expr f = Const("f");
expr g = Const("g");
expr a = Const("a");
substitution subst;
metavar_generator gen;
expr m1 = gen.mk();
metavar_env menv;
expr m1 = menv.mk_metavar();
expr t = f(m1, Var(0), Var(2));
expr r = instantiate(t, a);
subst.assign(m1, g(Var(0), Var(1)));
r = instantiate_metavars(r, subst);
menv.assign(m1, 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)));
}
@ -192,16 +174,15 @@ static void tst9() {
expr f = Const("f");
expr g = Const("g");
expr a = Const("a");
substitution subst;
metavar_generator gen;
expr m1 = gen.mk();
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;
subst.assign(m1, g(Var(0), Var(1)));
r = instantiate_metavars(r, subst);
menv.assign(m1, 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)));
}
@ -214,39 +195,36 @@ static void tst10() {
expr a = Const("a");
expr g = Const("g");
expr h = Const("h");
substitution subst;
metavar_generator gen;
expr m1 = gen.mk();
expr m2 = gen.mk();
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;
subst.assign(m1, f(Var(0)));
subst.assign(m2, Var(2));
r = instantiate_metavars(r, subst);
menv.assign(m1, f(Var(0)));
menv.assign(m2, 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))))));
}
static void tst11() {
substitution subst;
unsigned t1 = subst.get_timestamp();
metavar_generator gen;
expr m = gen.mk();
unsigned t2 = subst.get_timestamp();
lean_assert(t2 == t1);
lean_assert(!subst.is_assigned(m));
lean_assert(subst.get_timestamp() == t2);
subst.assign(m, Const("a"));
lean_assert(subst.get_timestamp() > t2);
metavar_env menv;
unsigned t1 = menv.get_timestamp();
expr m = menv.mk_metavar();
unsigned t2 = menv.get_timestamp();
lean_assert(t2 > t1);
lean_assert(!menv.is_assigned(m));
lean_assert(menv.get_timestamp() == t2);
menv.assign(m, Const("a"));
lean_assert(menv.get_timestamp() > t2);
}
static void tst12() {
substitution subst;
metavar_generator gen;
expr m = gen.mk();
metavar_env menv;
expr m = menv.mk_metavar();
expr f = Const("f");
std::cout << instantiate(f(m), {Var(0), Var(1)}) << "\n";
std::cout << instantiate(f(m), {Var(1), Var(0)}) << "\n";
@ -254,9 +232,8 @@ static void tst12() {
static void tst13() {
environment env;
substitution subst;
metavar_generator gen;
expr m = gen.mk();
metavar_env menv;
expr m = menv.mk_metavar();
env.add_var("N", Type());
expr N = Const("N");
env.add_var("f", N >> N);
@ -267,18 +244,17 @@ static void tst13() {
expr F = Fun({x, N}, f(m))(a);
normalizer norm(env);
std::cout << norm(F) << "\n";
subst.assign(m, Var(0));
std::cout << norm(instantiate_metavars(F, subst)) << "\n";
lean_assert(norm(instantiate_metavars(F, subst)) ==
instantiate_metavars(norm(F), subst));
menv.assign(m, Var(0));
std::cout << norm(instantiate_metavars(F, menv)) << "\n";
lean_assert(norm(instantiate_metavars(F, menv)) ==
instantiate_metavars(norm(F), menv));
}
static void tst14() {
environment env;
substitution subst;
metavar_generator gen;
expr m1 = gen.mk();
expr m2 = gen.mk();
metavar_env menv;
expr m1 = menv.mk_metavar();
expr m2 = menv.mk_metavar();
expr N = Const("N");
expr f = Const("f");
expr h = Const("h");
@ -289,17 +265,17 @@ static void tst14() {
env.add_var("h", Pi({N, Type()}, N >> (N >> N)));
expr F1 = Fun({{N, Type()}, {a, N}, {f, N >> N}},
(Fun({{x, N}, {y, N}}, Eq(f(m1), y)))(a));
substitution subst2 = subst;
subst2.assign(m1, h(Var(4), Var(1), Var(3)));
metavar_env menv2 = menv;
menv2.assign(m1, h(Var(4), Var(1), Var(3)));
normalizer norm(env);
env.add_var("M", Type());
expr M = Const("M");
std::cout << norm(F1) << "\n";
std::cout << instantiate_metavars(norm(F1), subst2) << "\n";
std::cout << instantiate_metavars(F1, subst2) << "\n";
std::cout << norm(instantiate_metavars(F1, subst2)) << "\n";
lean_assert(instantiate_metavars(norm(F1), subst2) ==
norm(instantiate_metavars(F1, subst2)));
std::cout << instantiate_metavars(norm(F1), menv2) << "\n";
std::cout << instantiate_metavars(F1, menv2) << "\n";
std::cout << norm(instantiate_metavars(F1, menv2)) << "\n";
lean_assert(instantiate_metavars(norm(F1), menv2) ==
norm(instantiate_metavars(F1, menv2)));
expr F2 = (Fun({{N, Type()}, {f, N >> N}, {a, N}, {b, N}},
(Fun({{x, N}, {y, N}}, Eq(f(m1), y)))(a, m2)))(M);
std::cout << norm(F2) << "\n";
@ -310,10 +286,9 @@ static void tst14() {
static void tst15() {
environment env;
substitution subst;
metavar_env menv;
normalizer norm(env);
metavar_generator gen;
expr m1 = gen.mk();
expr m1 = menv.mk_metavar();
expr f = Const("f");
expr x = Const("x");
expr y = Const("y");
@ -322,22 +297,21 @@ static void tst15() {
env.add_var("N", Type());
env.add_var("f", Type() >> Type());
expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, f(m1))(N, N));
subst.assign(m1, Var(2));
menv.assign(m1, Var(2));
std::cout << norm(F) << "\n";
std::cout << instantiate_metavars(norm(F), subst) << "\n";
std::cout << norm(instantiate_metavars(F, subst)) << "\n";
lean_assert(instantiate_metavars(norm(F), subst) ==
norm(instantiate_metavars(F, subst)));
std::cout << instantiate_metavars(norm(F), menv) << "\n";
std::cout << norm(instantiate_metavars(F, menv)) << "\n";
lean_assert(instantiate_metavars(norm(F), menv) ==
norm(instantiate_metavars(F, menv)));
}
static void tst16() {
environment env;
substitution subst;
metavar_env menv;
normalizer norm(env);
context ctx;
ctx = extend(ctx, "w", Type());
metavar_generator gen;
expr m1 = gen.mk();
expr m1 = menv.mk_metavar();
expr f = Const("f");
expr x = Const("x");
expr y = Const("y");
@ -345,23 +319,22 @@ static void tst16() {
expr N = Const("N");
env.add_var("N", Type());
expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, m1)(N, N));
subst.assign(m1, Var(3));
menv.assign(m1, Var(3));
std::cout << norm(F, ctx) << "\n";
std::cout << instantiate_metavars(norm(F, ctx), subst) << "\n";
std::cout << norm(instantiate_metavars(F, subst), ctx) << "\n";
std::cout << instantiate_metavars(norm(F, ctx), menv) << "\n";
std::cout << norm(instantiate_metavars(F, menv), ctx) << "\n";
}
static void tst17() {
environment env;
substitution subst;
metavar_env menv;
normalizer norm(env);
context ctx;
ctx = extend(ctx, "w1", Type());
ctx = extend(ctx, "w2", Type());
ctx = extend(ctx, "w3", Type());
ctx = extend(ctx, "w4", Type());
metavar_generator gen;
expr m1 = gen.mk();
expr m1 = menv.mk_metavar();
expr f = Const("f");
expr x = Const("x");
expr y = Const("y");
@ -369,33 +342,32 @@ static void tst17() {
expr N = Const("N");
env.add_var("N", Type());
expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, m1)(N, N));
substitution subst2 = subst;
subst.assign(m1, Var(3));
metavar_env menv2 = menv;
menv.assign(m1, Var(3));
std::cout << norm(F, ctx) << "\n";
std::cout << instantiate_metavars(norm(F, ctx), subst) << "\n";
std::cout << norm(instantiate_metavars(F, subst), ctx) << "\n";
std::cout << instantiate_metavars(norm(F, ctx), menv) << "\n";
std::cout << norm(instantiate_metavars(F, menv), ctx) << "\n";
F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}, {x, Type()}, {y, Type()}, {x, Type()}}, m1)(N, N, N, N, N));
lean_assert(instantiate_metavars(norm(F, ctx), subst) ==
norm(instantiate_metavars(F, subst), ctx));
lean_assert(instantiate_metavars(norm(F, ctx), menv) ==
norm(instantiate_metavars(F, menv), ctx));
std::cout << "----------------------\n";
subst2.assign(m1, Var(8));
menv2.assign(m1, Var(8));
std::cout << norm(F, ctx) << "\n";
std::cout << instantiate_metavars(norm(F, ctx), subst2) << "\n";
std::cout << norm(instantiate_metavars(F, subst2), ctx) << "\n";
lean_assert(instantiate_metavars(norm(F, ctx), subst2) ==
norm(instantiate_metavars(F, subst2), ctx));
std::cout << instantiate_metavars(norm(F, ctx), menv2) << "\n";
std::cout << norm(instantiate_metavars(F, menv2), ctx) << "\n";
lean_assert(instantiate_metavars(norm(F, ctx), menv2) ==
norm(instantiate_metavars(F, menv2), ctx));
}
static void tst18() {
environment env;
substitution subst;
metavar_env menv;
normalizer norm(env);
context ctx;
ctx = extend(ctx, "w1", Type());
ctx = extend(ctx, "w2", Type());
metavar_generator gen;
expr m1 = gen.mk();
expr m2 = gen.mk();
expr m1 = menv.mk_metavar();
expr m2 = menv.mk_metavar();
expr f = Const("f");
expr g = Const("g");
expr h = Const("h");
@ -410,26 +382,25 @@ static void tst18() {
env.add_var("h", N >> (N >> N));
expr F = Fun({z, Type()}, Fun({{f, N >> N}, {y, Type()}}, m1)(Fun({x, N}, g(z, x, m2)), N));
std::cout << norm(F, ctx) << "\n";
substitution subst2 = subst;
subst2.assign(m1, Var(1));
subst2.assign(m2, h(Var(2), Var(1)));
std::cout << instantiate_metavars(norm(F, ctx), subst2) << "\n";
std::cout << instantiate_metavars(F, subst2) << "\n";
lean_assert(instantiate_metavars(norm(F, ctx), subst2) ==
norm(instantiate_metavars(F, subst2), ctx));
lean_assert(instantiate_metavars(norm(F, ctx), subst2) ==
metavar_env menv2 = menv;
menv2.assign(m1, Var(1));
menv2.assign(m2, h(Var(2), Var(1)));
std::cout << instantiate_metavars(norm(F, ctx), menv2) << "\n";
std::cout << instantiate_metavars(F, menv2) << "\n";
lean_assert(instantiate_metavars(norm(F, ctx), menv2) ==
norm(instantiate_metavars(F, menv2), ctx));
lean_assert(instantiate_metavars(norm(F, ctx), menv2) ==
Fun({{z, Type()}, {x, N}}, g(z, x, h(Var(2), z))));
}
static void tst19() {
environment env;
substitution subst;
metavar_env menv;
normalizer norm(env);
context ctx;
ctx = extend(ctx, "w1", Type());
ctx = extend(ctx, "w2", Type());
metavar_generator gen;
expr m1 = gen.mk();
expr m1 = menv.mk_metavar();
expr x = Const("x");
expr y = Const("y");
expr N = Const("N");
@ -442,13 +413,12 @@ static void tst19() {
static void tst20() {
environment env;
substitution subst;
metavar_env menv;
normalizer norm(env);
context ctx;
ctx = extend(ctx, "w1", Type());
ctx = extend(ctx, "w2", Type());
metavar_generator gen;
expr m1 = gen.mk();
expr m1 = menv.mk_metavar();
expr x = Const("x");
expr y = Const("y");
expr z = Const("z");
@ -464,12 +434,11 @@ static void tst20() {
}
static void tst21() {
substitution subst;
metavar_generator gen;
expr m1 = gen.mk();
metavar_env menv;
expr m1 = menv.mk_metavar();
expr l = add_lift(add_lift(m1, 0, 1), 1, 1);
expr r = add_lift(m1, 0, 2);
std::cout << metavar_type(l) << " " << metavar_type(r) << "\n";
std::cout << menv.get_type(l) << " " << menv.get_type(r) << "\n";
lean_assert_eq(l, r);
lean_assert_eq(add_lift(add_lift(m1, 1, 2), 3, 4),
add_lift(m1, 1, 6));
@ -480,21 +449,18 @@ static void tst21() {
#define _ mk_placholder()
static void tst22() {
substitution subst;
metavar_generator mgen;
metavar_env menv;
expr f = Const("f");
expr x = Const("x");
expr N = Const("N");
expr F = f(Fun({x, N}, f(_, x)), _);
std::cout << F << "\n";
std::cout << replace_placeholders_with_metavars(F, mgen) << "\n";
std::cout << replace_placeholders_with_metavars(F, menv) << "\n";
}
static void tst23() {
environment env;
substitution subst;
unification_constraints_dbg up;
metavar_generator mgen;
metavar_env menv;
type_checker checker(env);
expr N = Const("N");
expr f = Const("f");
@ -504,30 +470,35 @@ static void tst23() {
env.add_var("a", N);
expr x = Const("x");
expr F0 = f(Fun({x, N}, f(_, x))(a), _);
expr F1 = replace_placeholders_with_metavars(F0, mgen);
expr F1 = replace_placeholders_with_metavars(F0, menv);
buffer<unification_constraint> up;
std::cout << F1 << "\n";
std::cout << checker.infer_type(F1, context(), &subst, &mgen, &up) << "\n";
try {
std::cout << checker.infer_type(F1, context(), &menv, up) << "\n";
} catch (kernel_exception & ex) {
formatter fmt = mk_simple_formatter();
state st(options(), fmt);
regular(st) << ex << "\n";
}
std::cout << up << "\n";
}
static void tst24() {
substitution subst;
metavar_generator gen;
expr m1 = gen.mk();
expr m2 = gen.mk();
metavar_env menv;
expr m1 = menv.mk_metavar();
expr m2 = menv.mk_metavar();
expr f = Const("f");
expr a = Const("a");
subst.assign(m1, f(m2));
subst.assign(m2, a);
lean_assert(instantiate_metavars(f(m1), subst) == f(f(a)));
std::cout << instantiate_metavars(f(m1), subst) << "\n";
menv.assign(m1, f(m2));
menv.assign(m2, a);
lean_assert(instantiate_metavars(f(m1), menv) == f(f(a)));
std::cout << instantiate_metavars(f(m1), menv) << "\n";
}
static void tst25() {
environment env;
substitution subst;
unification_constraints_dbg up;
metavar_generator gen;
metavar_env menv;
buffer<unification_constraint> up;
type_checker checker(env);
expr N = Const("N");
expr a = Const("a");
@ -535,10 +506,10 @@ static void tst25() {
env.add_var("N", Type());
env.add_var("a", N);
env.add_var("b", N);
expr m = gen.mk();
expr m = menv.mk_metavar();
expr F = m(a, b);
std::cout << checker.infer_type(F, context(), &subst, &gen, &up) << "\n";
std::cout << subst << "\n";
std::cout << checker.infer_type(F, context(), &menv, up) << "\n";
std::cout << menv << "\n";
std::cout << up << "\n";
}
@ -556,9 +527,8 @@ static void tst26() {
std::cout << "\ntst26\n";
environment env;
import_all(env);
substitution subst;
unification_constraints_dbg up;
metavar_generator gen;
metavar_env menv;
buffer<unification_constraint> up;
type_checker checker(env);
expr list = Const("list");
expr nil = Const("nil");
@ -575,17 +545,17 @@ static void tst26() {
expr b = Const("b");
expr n = Const("n");
expr m = Const("m");
expr m1 = gen.mk();
expr m2 = gen.mk();
expr m3 = gen.mk();
expr A1 = gen.mk();
expr A2 = gen.mk();
expr A3 = gen.mk();
expr A4 = gen.mk();
expr m1 = menv.mk_metavar();
expr m2 = menv.mk_metavar();
expr m3 = menv.mk_metavar();
expr A1 = menv.mk_metavar();
expr A2 = menv.mk_metavar();
expr A3 = menv.mk_metavar();
expr A4 = menv.mk_metavar();
expr F = cons(A1, m1(a), cons(A2, m2(n), cons(A3, m3(b), nil(A4))));
std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &subst, &gen, &up) << "\n";
std::cout << subst << "\n";
std::cout << checker.infer_type(F, context(), &menv, up) << "\n";
std::cout << menv << "\n";
std::cout << up << "\n";
}
@ -599,9 +569,8 @@ static void tst27() {
std::cout << "\ntst27\n";
environment env;
import_all(env);
substitution subst;
unification_constraints_dbg up;
metavar_generator gen;
metavar_env menv;
buffer<unification_constraint> up;
type_checker checker(env);
expr A = Const("A");
expr f = Const("f");
@ -612,15 +581,15 @@ static void tst27() {
env.add_var("f", Pi({A, Type()}, A >> (A >> Bool)));
env.add_var("a", Int);
env.add_var("b", Real);
expr T1 = gen.mk();
expr T2 = gen.mk();
expr A1 = gen.mk();
expr m1 = gen.mk();
expr m2 = gen.mk();
expr T1 = menv.mk_metavar();
expr T2 = menv.mk_metavar();
expr A1 = menv.mk_metavar();
expr m1 = menv.mk_metavar();
expr m2 = menv.mk_metavar();
expr F = Fun({{x, T1}, {y, T2}}, f(A1, x, y))(m1(a), m2(b));
std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &subst, &gen, &up) << "\n";
std::cout << subst << "\n";
std::cout << checker.infer_type(F, context(), &menv, up) << "\n";
std::cout << menv << "\n";
std::cout << up << "\n";
}

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

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#include <iostream>
#include <thread>
#include <chrono>
#include <string>
#include "util/test.h"
#include "util/trace.h"
#include "util/exception.h"

2
src/tests/library/deep_copy.cpp
View file

@ -17,7 +17,7 @@ static void tst1() {
expr t = Type();
expr z = Const("z");
local_context lctx{mk_lift(0, 1), mk_inst(0, a)};
expr m = mk_metavar("a", expr(), lctx);
expr m = mk_metavar("a", lctx);
expr F = mk_let("z", Type(), Type(level()+1), mk_pi("y", t, mk_lambda("x", t, f(f(f(x, a), Const("10")), Eq(x, m)))));
expr G = deep_copy(F);
lean_assert(F == G);

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

@ -70,12 +70,12 @@ static void tst1() {
local_context lctx3{mk_lift(3, 1), mk_inst(0, Const("a"))};
local_context lctx4{mk_lift(0, 1), mk_inst(0, Const("a")), mk_inst(0, Const("b"))};
local_context lctx5{mk_inst(0, Const("a")), mk_inst(0, Const("a"))};
lt(mk_metavar("a", expr(), lctx1), mk_metavar("b", expr(), lctx1), true);
lt(mk_metavar("a", expr(), lctx1), mk_metavar("a", expr(), lctx2), true);
lt(mk_metavar("a", expr(), lctx1), mk_metavar("a", expr(), lctx3), true);
lt(mk_metavar("a", expr(), lctx1), mk_metavar("a", expr(), lctx4), true);
lt(mk_metavar("a", expr(), lctx1), mk_metavar("a", expr(), lctx5), true);
lt(mk_metavar("a", expr(), lctx1), mk_metavar("a", expr(), lctx1), false);
lt(mk_metavar("a", lctx1), mk_metavar("b", lctx1), true);
lt(mk_metavar("a", lctx1), mk_metavar("a", lctx2), true);
lt(mk_metavar("a", lctx1), mk_metavar("a", lctx3), true);
lt(mk_metavar("a", lctx1), mk_metavar("a", lctx4), true);
lt(mk_metavar("a", lctx1), mk_metavar("a", lctx5), true);
lt(mk_metavar("a", lctx1), mk_metavar("a", lctx1), false);
}
int main() {

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

@ -80,8 +80,8 @@ void tst3() {
expr m1; // = subst.mk_metavar();
expr m2; // = subst.mk_metavar();
expr m3; // = subst.mk_metavar();
expr t1 = metavar_type(m1);
expr t2 = metavar_type(m2);
expr t1; // = metavar_type(m1);
expr t2; // = metavar_type(m2);
expr f = Const("f");
expr a = Const("a");
expr b = Const("b");

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

@ -30,8 +30,8 @@ static void tst1() {
lean_assert(is_eqp(arg(F2, 1), arg(F2, 2)));
max_fn.clear();
local_context lctx{mk_lift(1, 1), mk_inst(0, a1)};
expr m1 = mk_metavar("m1", expr(), lctx);
expr m2 = mk_metavar("m1", expr(), lctx);
expr m1 = mk_metavar("m1", lctx);
expr m2 = mk_metavar("m1", lctx);
F1 = f(m1, m2);
lean_assert(!is_eqp(arg(F1, 1), arg(F1, 2)));
F2 = max_fn(F1);

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

@ -399,9 +399,9 @@ static void match_eq_tst3() {
static void match_metavar_tst1() {
cout << "--- match_metavar_tst1() ---" << endl;
metavar_generator gen;
expr m1 = gen.mk();
expr m2 = gen.mk();
metavar_env menv;
expr m1 = menv.mk_metavar();
expr m2 = menv.mk_metavar();
expr f = Const("f");
subst_map s;
bool result = test_match(m1, m1, 0, s);
@ -411,9 +411,9 @@ static void match_metavar_tst1() {
static void match_metavar_tst2() {
cout << "--- match_metavar_tst2() ---" << endl;
metavar_generator gen;
expr m1 = gen.mk();
expr m2 = gen.mk();
metavar_env menv;
expr m1 = menv.mk_metavar();
expr m2 = menv.mk_metavar();
expr f = Const("f");
subst_map s;
bool result = test_match(m1, m2, 0, s);
@ -423,8 +423,8 @@ static void match_metavar_tst2() {
static void match_metavar_tst3() {
cout << "--- match_metavar_tst3() ---" << endl;
metavar_generator gen;
expr m1 = gen.mk();
metavar_env menv;
expr m1 = menv.mk_metavar();
expr f = Const("f");
subst_map s;
bool result = test_match(m1, f, 0, s);