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

refactor(kernel): improve names

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-16 11:13:50 -07:00
parent d6d72ba80e
commit 40b3129e7b
34 changed files with 249 additions and 247 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/kernel/context.cpp
View file

@ -9,7 +9,7 @@ Author: Leonardo de Moura
#include "kernel/context.h"
namespace lean {
std::pair<name, expr> const & lookup(context const & c, unsigned i) {
binder const & lookup(context const & c, unsigned i) {
auto const * it = &c;
while (*it) {
if (i == 0)
@ -19,11 +19,11 @@ std::pair<name, expr> const & lookup(context const & c, unsigned i) {
}
throw exception("unknown free variable");
}
optional<std::pair<name, expr>> find(context const & c, unsigned i) {
optional<binder> find(context const & c, unsigned i) {
try {
return optional<std::pair<name, expr>>(lookup(c, i));
return optional<binder>(lookup(c, i));
} catch (exception &) {
return optional<std::pair<name, expr>>();
return optional<binder>();
}
}
}

10
src/kernel/context.h
View file

@ -11,8 +11,10 @@ Author: Leonardo de Moura
#include "kernel/expr.h"
namespace lean {
typedef list<std::pair<name, expr>> context;
inline context extend(context const & c, name const & n, expr const & t) { return cons(mk_pair(n, t), c); }
std::pair<name, expr> const & lookup(context const & c, unsigned i);
optional<std::pair<name, expr>> find(context const & c, unsigned i);
typedef list<binder> context;
typedef context telescope;
inline context extend(context const & c, name const & n, expr const & t) { return cons(binder(n, t), c); }
inline context extend(context const & c, binder const & b) { return cons(b, c); }
binder const & lookup(context const & c, unsigned i);
optional<binder> find(context const & c, unsigned i);
}

22
src/kernel/converter.cpp
View file

@ -66,7 +66,7 @@ struct default_converter : public converter {
/** \brief Try to apply eta-reduction to \c e. */
expr try_eta(expr const & e) {
lean_assert(is_lambda(e));
expr const & b = binder_body(e);
expr const & b = binding_body(e);
if (is_lambda(b)) {
expr new_b = try_eta(b);
if (is_eqp(b, new_b)) {
@ -74,7 +74,7 @@ struct default_converter : public converter {
} else if (is_app(new_b) && is_var(app_arg(new_b), 0) && !has_free_var(app_fn(new_b), 0)) {
return lower_free_vars(app_fn(new_b), 1);
} else {
return update_binder(e, binder_domain(e), new_b);
return update_binder(e, binding_domain(e), new_b);
}
} else if (is_app(b) && is_var(app_arg(b), 0) && !has_free_var(app_fn(b), 0)) {
return lower_free_vars(app_fn(b), 1);
@ -132,12 +132,12 @@ struct default_converter : public converter {
if (is_lambda(f)) {
unsigned m = 1;
unsigned num_args = args.size();
while (is_lambda(binder_body(f)) && m < num_args) {
f = binder_body(f);
while (is_lambda(binding_body(f)) && m < num_args) {
f = binding_body(f);
m++;
}
lean_assert(m <= num_args);
r = whnf_core(mk_rev_app(instantiate(binder_body(f), m, args.data() + (num_args - m)), num_args - m, args.data()), c);
r = whnf_core(mk_rev_app(instantiate(binding_body(f), m, args.data() + (num_args - m)), num_args - m, args.data()), c);
} else {
r = is_eqp(f, *it) ? e : mk_rev_app(f, args.size(), args.data());
}
@ -183,7 +183,7 @@ struct default_converter : public converter {
if (is_constant(e)) {
if (auto d = m_env.find(const_name(e))) {
if (d->is_definition() && !is_opaque(*d) && d->get_weight() >= w)
return unfold_name_core(instantiate_params(d->get_value(), d->get_params(), const_level_params(e)), w);
return unfold_name_core(instantiate_params(d->get_value(), d->get_params(), const_levels(e)), w);
}
}
return e;
@ -300,13 +300,13 @@ struct default_converter : public converter {
expr_kind k = t.kind();
buffer<expr> subst;
do {
expr var_t_type = instantiate(binder_domain(t), subst.size(), subst.data());
expr var_s_type = instantiate(binder_domain(s), subst.size(), subst.data());
expr var_t_type = instantiate(binding_domain(t), subst.size(), subst.data());
expr var_s_type = instantiate(binding_domain(s), subst.size(), subst.data());
if (!is_def_eq(var_t_type, var_s_type, c, jst))
return false;
subst.push_back(mk_local(c.mk_fresh_name() + binder_name(s), var_s_type));
t = binder_body(t);
s = binder_body(s);
subst.push_back(mk_local(c.mk_fresh_name() + binding_name(s), var_s_type));
t = binding_body(t);
s = binding_body(s);
} while (t.kind() == k && s.kind() == k);
return is_def_eq(instantiate(t, subst.size(), subst.data()), instantiate(s, subst.size(), subst.data()), c, jst);
}

36
src/kernel/definition.cpp
View file

@ -11,34 +11,34 @@ Author: Leonardo de Moura
namespace lean {
struct definition::cell {
MK_LEAN_RC();
name m_name;
param_names m_params;
expr m_type;
bool m_theorem;
optional<expr> m_value; // if none, then definition is actually a postulate
name m_name;
level_param_names m_params;
expr m_type;
bool m_theorem;
optional<expr> m_value; // if none, then definition is actually a postulate
// The following fields are only meaningful for definitions (which are not theorems)
unsigned m_weight;
unsigned m_module_idx; // module idx where it was defined
bool m_opaque;
unsigned m_weight;
unsigned m_module_idx; // module idx where it was defined
bool m_opaque;
// The following field affects the convertability checker.
// Let f be this definition, then if the following field is true,
// then whenever we are checking whether
// (f a) is convertible to (f b)
// we will first check whether a is convertible to b.
// If the test fails, then we perform the full check.
bool m_use_conv_opt;
bool m_use_conv_opt;
void dealloc() { delete this; }
cell(name const & n, param_names const & params, expr const & t, bool is_axiom):
cell(name const & n, level_param_names const & params, expr const & t, bool is_axiom):
m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_axiom),
m_weight(0), m_module_idx(0), m_opaque(true), m_use_conv_opt(false) {}
cell(name const & n, param_names const & params, expr const & t, bool is_thm, expr const & v,
cell(name const & n, level_param_names const & params, expr const & t, bool is_thm, expr const & v,
bool opaque, unsigned w, module_idx mod_idx, bool use_conv_opt):
m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_thm),
m_value(v), m_weight(w), m_module_idx(mod_idx), m_opaque(opaque), m_use_conv_opt(use_conv_opt) {}
};
definition g_dummy = mk_axiom(name(), param_names(), expr());
definition g_dummy = mk_axiom(name(), level_param_names(), expr());
definition::definition():definition(g_dummy) {}
definition::definition(cell * ptr):m_ptr(ptr) {}
@ -55,7 +55,7 @@ bool definition::is_axiom() const { return is_var_decl() && m_ptr->m_theore
bool definition::is_theorem() const { return is_definition() && m_ptr->m_theorem; }
name definition::get_name() const { return m_ptr->m_name; }
param_names const & definition::get_params() const { return m_ptr->m_params; }
level_param_names const & definition::get_params() const { return m_ptr->m_params; }
expr definition::get_type() const { return m_ptr->m_type; }
bool definition::is_opaque() const { return m_ptr->m_opaque; }
@ -64,11 +64,11 @@ unsigned definition::get_weight() const { return m_ptr->m_weight; }
module_idx definition::get_module_idx() const { return m_ptr->m_module_idx; }
bool definition::use_conv_opt() const { return m_ptr->m_use_conv_opt; }
definition mk_definition(name const & n, param_names const & params, expr const & t, expr const & v,
definition mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque, unsigned weight, module_idx mod_idx, bool use_conv_opt) {
return definition(new definition::cell(n, params, t, false, v, opaque, weight, mod_idx, use_conv_opt));
}
definition mk_definition(environment const & env, name const & n, param_names const & params, expr const & t, expr const & v,
definition mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque, module_idx mod_idx, bool use_conv_opt) {
unsigned w = 0;
for_each(v, [&](expr const & e, unsigned) {
@ -81,13 +81,13 @@ definition mk_definition(environment const & env, name const & n, param_names co
});
return mk_definition(n, params, t, v, opaque, w+1, mod_idx, use_conv_opt);
}
definition mk_theorem(name const & n, param_names const & params, expr const & t, expr const & v) {
definition mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v) {
return definition(new definition::cell(n, params, t, true, v, true, 0, 0, false));
}
definition mk_axiom(name const & n, param_names const & params, expr const & t) {
definition mk_axiom(name const & n, level_param_names const & params, expr const & t) {
return definition(new definition::cell(n, params, t, true));
}
definition mk_var_decl(name const & n, param_names const & params, expr const & t) {
definition mk_var_decl(name const & n, level_param_names const & params, expr const & t) {
return definition(new definition::cell(n, params, t, false));
}
}

22
src/kernel/definition.h
View file

@ -58,7 +58,7 @@ public:
bool is_var_decl() const;
name get_name() const;
param_names const & get_params() const;
level_param_names const & get_params() const;
expr get_type() const;
expr get_value() const;
@ -67,24 +67,24 @@ public:
module_idx get_module_idx() const;
bool use_conv_opt() const;
friend definition mk_definition(environment const & env, name const & n, param_names const & params, expr const & t,
friend definition mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t,
expr const & v, bool opaque, module_idx mod_idx, bool use_conv_opt);
friend definition mk_definition(name const & n, param_names const & params, expr const & t, expr const & v, bool opaque,
friend definition mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, bool opaque,
unsigned weight, module_idx mod_idx, bool use_conv_opt);
friend definition mk_theorem(name const & n, param_names const & params, expr const & t, expr const & v);
friend definition mk_axiom(name const & n, param_names const & params, expr const & t);
friend definition mk_var_decl(name const & n, param_names const & params, expr const & t);
friend definition mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
friend definition mk_axiom(name const & n, level_param_names const & params, expr const & t);
friend definition mk_var_decl(name const & n, level_param_names const & params, expr const & t);
};
inline optional<definition> none_definition() { return optional<definition>(); }
inline optional<definition> some_definition(definition const & o) { return optional<definition>(o); }
inline optional<definition> some_definition(definition && o) { return optional<definition>(std::forward<definition>(o)); }
definition mk_definition(name const & n, param_names const & params, expr const & t, expr const & v,
definition mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque = false, unsigned weight = 0, module_idx mod_idx = 0, bool use_conv_opt = true);
definition mk_definition(environment const & env, name const & n, param_names const & params, expr const & t, expr const & v,
definition mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque = false, module_idx mod_idx = 0, bool use_conv_opt = true);
definition mk_theorem(name const & n, param_names const & params, expr const & t, expr const & v);
definition mk_axiom(name const & n, param_names const & params, expr const & t);
definition mk_var_decl(name const & n, param_names const & params, expr const & t);
definition mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
definition mk_axiom(name const & n, level_param_names const & params, expr const & t);
definition mk_var_decl(name const & n, level_param_names const & params, expr const & t);
}

22
src/kernel/expr.cpp
View file

@ -137,12 +137,12 @@ void expr_app::dealloc(buffer<expr_cell*> & todelete) {
static unsigned dec(unsigned k) { return k == 0 ? 0 : k - 1; }
bool operator==(expr_binder_info const & i1, expr_binder_info const & i2) {
bool operator==(binder_info const & i1, binder_info const & i2) {
return i1.is_implicit() == i2.is_implicit() && i1.is_cast() == i2.is_cast() && i1.is_contextual() == i2.is_contextual();
}
// Expr binders (Lambda, Pi)
expr_binder::expr_binder(expr_kind k, name const & n, expr const & t, expr const & b, expr_binder_info const & i):
expr_binding::expr_binding(expr_kind k, name const & n, expr const & t, expr const & b, binder_info const & i):
expr_composite(k, ::lean::hash(t.hash(), b.hash()),
t.has_metavar() || b.has_metavar(),
t.has_local() || b.has_local(),
@ -153,7 +153,7 @@ expr_binder::expr_binder(expr_kind k, name const & n, expr const & t, expr const
m_body(b) {
lean_assert(k == expr_kind::Lambda || k == expr_kind::Pi);
}
void expr_binder::dealloc(buffer<expr_cell*> & todelete) {
void expr_binding::dealloc(buffer<expr_cell*> & todelete) {
dec_ref(m_body, todelete);
dec_ref(m_binder.m_type, todelete);
delete(this);
@ -269,7 +269,7 @@ void expr_cell::dealloc() {
case expr_kind::Sort: delete static_cast<expr_sort*>(it); break;
case expr_kind::App: static_cast<expr_app*>(it)->dealloc(todo); break;
case expr_kind::Lambda:
case expr_kind::Pi: static_cast<expr_binder*>(it)->dealloc(todo); break;
case expr_kind::Pi: static_cast<expr_binding*>(it)->dealloc(todo); break;
case expr_kind::Let: static_cast<expr_let*>(it)->dealloc(todo); break;
}
}
@ -400,8 +400,8 @@ expr update_rev_app(expr const & e, unsigned num, expr const * new_args) {
}
expr update_binder(expr const & e, expr const & new_domain, expr const & new_body) {
if (!is_eqp(binder_domain(e), new_domain) || !is_eqp(binder_body(e), new_body))
return copy_tag(e, mk_binder(e.kind(), binder_name(e), new_domain, new_body, binder_info(e)));
if (!is_eqp(binding_domain(e), new_domain) || !is_eqp(binding_body(e), new_body))
return copy_tag(e, mk_binder(e.kind(), binding_name(e), new_domain, new_body, binding_info(e)));
else
return e;
}
@ -428,7 +428,7 @@ expr update_sort(expr const & e, level const & new_level) {
}
expr update_constant(expr const & e, levels const & new_levels) {
if (!is_eqp(const_level_params(e), new_levels))
if (!is_eqp(const_levels(e), new_levels))
return copy_tag(e, mk_constant(const_name(e), new_levels));
else
return e;
@ -467,7 +467,7 @@ bool is_arrow(expr const & t) {
if (r) {
return *r;
} else {
bool res = is_pi(t) && !has_free_var(binder_body(t), 0);
bool res = is_pi(t) && !has_free_var(binding_body(t), 0);
t.raw()->set_is_arrow(res);
return res;
}
@ -476,12 +476,12 @@ bool is_arrow(expr const & t) {
expr copy(expr const & a) {
switch (a.kind()) {
case expr_kind::Var: return mk_var(var_idx(a));
case expr_kind::Constant: return mk_constant(const_name(a), const_level_params(a));
case expr_kind::Constant: return mk_constant(const_name(a), const_levels(a));
case expr_kind::Sort: return mk_sort(sort_level(a));
case expr_kind::Macro: return mk_macro(to_macro(a)->m_definition, macro_num_args(a), macro_args(a));
case expr_kind::App: return mk_app(app_fn(a), app_arg(a));
case expr_kind::Lambda: return mk_lambda(binder_name(a), binder_domain(a), binder_body(a), binder_info(a));
case expr_kind::Pi: return mk_pi(binder_name(a), binder_domain(a), binder_body(a), binder_info(a));
case expr_kind::Lambda: return mk_lambda(binding_name(a), binding_domain(a), binding_body(a), binding_info(a));
case expr_kind::Pi: return mk_pi(binding_name(a), binding_domain(a), binding_body(a), binding_info(a));
case expr_kind::Let: return mk_let(let_name(a), let_type(a), let_value(a), let_body(a));
case expr_kind::Meta: return mk_metavar(mlocal_name(a), mlocal_type(a));
case expr_kind::Local: return mk_local(mlocal_name(a), mlocal_type(a));

67
src/kernel/expr.h
View file

@ -79,7 +79,7 @@ public:
};
class macro_definition;
class expr_binder_info;
class binder_info;
/**
\brief Exprs for encoding formulas/expressions, types and proofs.
@ -130,7 +130,7 @@ public:
friend expr mk_app(expr const & f, expr const & a);
friend expr mk_pair(expr const & f, expr const & s, expr const & t);
friend expr mk_proj(bool fst, expr const & p);
friend expr mk_binder(expr_kind k, name const & n, expr const & t, expr const & e, expr_binder_info const & i);
friend expr mk_binder(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i);
friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & e);
friend expr mk_macro(macro_definition const & m, unsigned num, expr const * args);
@ -182,7 +182,7 @@ class expr_const : public expr_cell {
public:
expr_const(name const & n, levels const & ls);
name const & get_name() const { return m_name; }
levels const & get_level_params() const { return m_levels; }
levels const & get_levels() const { return m_levels; }
};
/** \brief Metavariables and local constants */
@ -223,48 +223,47 @@ public:
\brief Auxiliary annotation for binders (Lambda and Pi). This information
is only used for elaboration.
*/
class expr_binder_info {
class binder_info {
unsigned m_implicit:1; //! if true, binder argument is an implicit argument
unsigned m_cast:1; //! if true, binder argument is a target for using cast
unsigned m_contextual:1; //! if true, binder argument is assumed to be part of the context, and may be argument for metavariables.
public:
expr_binder_info(bool implicit = false, bool cast = false, bool contextual = true):
binder_info(bool implicit = false, bool cast = false, bool contextual = true):
m_implicit(implicit), m_cast(cast), m_contextual(contextual) {}
bool is_implicit() const { return m_implicit; }
bool is_cast() const { return m_cast; }
bool is_contextual() const { return m_contextual; }
};
bool operator==(expr_binder_info const & i1, expr_binder_info const & i2);
inline bool operator!=(expr_binder_info const & i1, expr_binder_info const & i2) { return !(i1 == i2); }
bool operator==(binder_info const & i1, binder_info const & i2);
inline bool operator!=(binder_info const & i1, binder_info const & i2) { return !(i1 == i2); }
class binder {
friend class expr_binder;
friend class expr_binding;
name m_name;
expr m_type;
expr_binder_info m_info;
binder_info m_info;
public:
binder(name const & n, expr const & t, expr_binder_info const & bi):
binder(name const & n, expr const & t, binder_info const & bi = binder_info()):
m_name(n), m_type(t), m_info(bi) {}
name const & get_name() const { return m_name; }
expr const & get_type() const { return m_type; }
expr_binder_info const & get_info() const { return m_info; }
binder_info const & get_info() const { return m_info; }
};
typedef list<binder> telescope;
/** \brief Super class for lambda and pi */
class expr_binder : public expr_composite {
/** \brief Lambda and Pi expressions */
class expr_binding : public expr_composite {
binder m_binder;
expr m_body;
friend class expr_cell;
void dealloc(buffer<expr_cell*> & todelete);
public:
expr_binder(expr_kind k, name const & n, expr const & t, expr const & e, expr_binder_info const & i = expr_binder_info());
expr_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i = binder_info());
name const & get_name() const { return m_binder.get_name(); }
expr const & get_domain() const { return m_binder.get_type(); }
expr const & get_body() const { return m_body; }
expr_binder_info const & get_info() const { return m_binder.get_info(); }
binder_info const & get_info() const { return m_binder.get_info(); }
binder const & get_binder() const { return m_binder; }
};
/** \brief Let expressions */
@ -424,13 +423,13 @@ template<typename T> expr mk_app(T const & args) { return mk_app(args.size(), ar
expr mk_rev_app(unsigned num_args, expr const * args);
template<typename T> expr mk_rev_app(T const & args) { return mk_rev_app(args.size(), args.data()); }
template<typename T> expr mk_rev_app(expr const & f, T const & args) { return mk_rev_app(f, args.size(), args.data()); }
inline expr mk_binder(expr_kind k, name const & n, expr const & t, expr const & e, expr_binder_info const & i = expr_binder_info()) {
return expr(new expr_binder(k, n, t, e, i));
inline expr mk_binder(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i = binder_info()) {
return expr(new expr_binding(k, n, t, e, i));
}
inline expr mk_lambda(name const & n, expr const & t, expr const & e, expr_binder_info const & i = expr_binder_info()) {
inline expr mk_lambda(name const & n, expr const & t, expr const & e, binder_info const & i = binder_info()) {
return mk_binder(expr_kind::Lambda, n, t, e, i);
}
inline expr mk_pi(name const & n, expr const & t, expr const & e, expr_binder_info const & i = expr_binder_info()) {
inline expr mk_pi(name const & n, expr const & t, expr const & e, binder_info const & i = binder_info()) {
return mk_binder(expr_kind::Pi, n, t, e, i);
}
inline expr mk_let(name const & n, expr const & t, expr const & v, expr const & e) { return expr(new expr_let(n, t, v, e)); }
@ -486,7 +485,7 @@ expr mk_app_vars(expr const & f, unsigned n);
inline expr_var * to_var(expr_cell * e) { lean_assert(is_var(e)); return static_cast<expr_var*>(e); }
inline expr_const * to_constant(expr_cell * e) { lean_assert(is_constant(e)); return static_cast<expr_const*>(e); }
inline expr_app * to_app(expr_cell * e) { lean_assert(is_app(e)); return static_cast<expr_app*>(e); }
inline expr_binder * to_binder(expr_cell * e) { lean_assert(is_binder(e)); return static_cast<expr_binder*>(e); }
inline expr_binding * to_binding(expr_cell * e) { lean_assert(is_binder(e)); return static_cast<expr_binding*>(e); }
inline expr_let * to_let(expr_cell * e) { lean_assert(is_let(e)); return static_cast<expr_let*>(e); }
inline expr_sort * to_sort(expr_cell * e) { lean_assert(is_sort(e)); return static_cast<expr_sort*>(e); }
inline expr_mlocal * to_mlocal(expr_cell * e) { lean_assert(is_mlocal(e)); return static_cast<expr_mlocal*>(e); }
@ -497,7 +496,7 @@ inline expr_macro * to_macro(expr_cell * e) { lean_assert(is_macro(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()); }
inline expr_app * to_app(expr const & e) { return to_app(e.raw()); }
inline expr_binder * to_binder(expr const & e) { return to_binder(e.raw()); }
inline expr_binding * to_binding(expr const & e) { return to_binding(e.raw()); }
inline expr_let * to_let(expr const & e) { return to_let(e.raw()); }
inline expr_sort * to_sort(expr const & e) { return to_sort(e.raw()); }
inline expr_mlocal * to_mlocal(expr const & e) { return to_mlocal(e.raw()); }
@ -514,17 +513,18 @@ inline bool is_shared(expr_cell * e) { return get_rc(e) >
inline unsigned var_idx(expr_cell * e) { return to_var(e)->get_vidx(); }
inline bool is_var(expr_cell * e, unsigned i) { return is_var(e) && var_idx(e) == i; }
inline name const & const_name(expr_cell * e) { return to_constant(e)->get_name(); }
inline levels const & const_level_params(expr_cell * e) { return to_constant(e)->get_level_params(); }
inline levels const & const_levels(expr_cell * e) { return to_constant(e)->get_levels(); }
inline macro_definition const & macro_def(expr_cell * e) { return to_macro(e)->get_def(); }
inline expr const * macro_args(expr_cell * e) { return to_macro(e)->get_args(); }
inline expr const & macro_arg(expr_cell * e, unsigned i) { return to_macro(e)->get_arg(i); }
inline unsigned macro_num_args(expr_cell * e) { return to_macro(e)->get_num_args(); }
inline expr const & app_fn(expr_cell * e) { return to_app(e)->get_fn(); }
inline expr const & app_arg(expr_cell * e) { return to_app(e)->get_arg(); }
inline name const & binder_name(expr_cell * e) { return to_binder(e)->get_name(); }
inline expr const & binder_domain(expr_cell * e) { return to_binder(e)->get_domain(); }
inline expr const & binder_body(expr_cell * e) { return to_binder(e)->get_body(); }
inline expr_binder_info const & binder_info(expr_cell * e) { return to_binder(e)->get_info(); }
inline name const & binding_name(expr_cell * e) { return to_binding(e)->get_name(); }
inline expr const & binding_domain(expr_cell * e) { return to_binding(e)->get_domain(); }
inline expr const & binding_body(expr_cell * e) { return to_binding(e)->get_body(); }
inline binder_info const & binding_info(expr_cell * e) { return to_binding(e)->get_info(); }
inline binder const & binding_binder(expr_cell * e) { return to_binding(e)->get_binder(); }
inline level const & sort_level(expr_cell * e) { return to_sort(e)->get_level(); }
inline name const & let_name(expr_cell * e) { return to_let(e)->get_name(); }
inline expr const & let_value(expr_cell * e) { return to_let(e)->get_value(); }
@ -538,17 +538,18 @@ inline bool is_shared(expr const & e) { return get_rc(e) >
inline unsigned var_idx(expr const & e) { return to_var(e)->get_vidx(); }
inline bool is_var(expr const & e, unsigned i) { return is_var(e) && var_idx(e) == i; }
inline name const & const_name(expr const & e) { return to_constant(e)->get_name(); }
inline levels const & const_level_params(expr const & e) { return to_constant(e)->get_level_params(); }
inline levels const & const_levels(expr const & e) { return to_constant(e)->get_levels(); }
inline macro_definition const & macro_def(expr const & e) { return to_macro(e)->get_def(); }
inline expr const * macro_args(expr const & e) { return to_macro(e)->get_args(); }
inline expr const & macro_arg(expr const & e, unsigned i) { return to_macro(e)->get_arg(i); }
inline unsigned macro_num_args(expr const & e) { return to_macro(e)->get_num_args(); }
inline expr const & app_fn(expr const & e) { return to_app(e)->get_fn(); }
inline expr const & app_arg(expr const & e) { return to_app(e)->get_arg(); }
inline name const & binder_name(expr const & e) { return to_binder(e)->get_name(); }
inline expr const & binder_domain(expr const & e) { return to_binder(e)->get_domain(); }
inline expr const & binder_body(expr const & e) { return to_binder(e)->get_body(); }
inline expr_binder_info const & binder_info(expr const & e) { return to_binder(e)->get_info(); }
inline name const & binding_name(expr const & e) { return to_binding(e)->get_name(); }
inline expr const & binding_domain(expr const & e) { return to_binding(e)->get_domain(); }
inline expr const & binding_body(expr const & e) { return to_binding(e)->get_body(); }
inline binder_info const & binding_info(expr const & e) { return to_binding(e)->get_info(); }
inline binder const & binding_binder(expr const & e) { return to_binding(e)->get_binder(); }
inline level const & sort_level(expr const & e) { return to_sort(e)->get_level(); }
inline name const & let_name(expr const & e) { return to_let(e)->get_name(); }
inline expr const & let_value(expr const & e) { return to_let(e)->get_value(); }

8
src/kernel/expr_eq_fn.cpp
View file

@ -27,7 +27,7 @@ bool expr_eq_fn::apply(expr const & a, expr const & b) {
case expr_kind::Constant:
return
const_name(a) == const_name(b) &&
compare(const_level_params(a), const_level_params(b), [](level const & l1, level const & l2) { return l1 == l2; });
compare(const_levels(a), const_levels(b), [](level const & l1, level const & l2) { return l1 == l2; });
case expr_kind::Local: case expr_kind::Meta:
return
mlocal_name(a) == mlocal_name(b) &&
@ -38,9 +38,9 @@ bool expr_eq_fn::apply(expr const & a, expr const & b) {
apply(app_arg(a), app_arg(b));
case expr_kind::Lambda: case expr_kind::Pi:
return
apply(binder_domain(a), binder_domain(b)) &&
apply(binder_body(a), binder_body(b)) &&
(!m_compare_binder_info || binder_info(a) == binder_info(b));
apply(binding_domain(a), binding_domain(b)) &&
apply(binding_body(a), binding_body(b)) &&
(!m_compare_binder_info || binding_info(a) == binding_info(b));
case expr_kind::Sort:
return sort_level(a) == sort_level(b);
case expr_kind::Macro:

4
src/kernel/for_each_fn.cpp
View file

@ -61,8 +61,8 @@ void for_each_fn::apply(expr const & e, unsigned offset) {
todo.emplace_back(app_fn(e), offset);
goto begin_loop;
case expr_kind::Lambda: case expr_kind::Pi:
todo.emplace_back(binder_body(e), offset + 1);
todo.emplace_back(binder_domain(e), offset);
todo.emplace_back(binding_body(e), offset + 1);
todo.emplace_back(binding_domain(e), offset);
goto begin_loop;
case expr_kind::Let:
todo.emplace_back(let_body(e), offset + 1);

22
src/kernel/formatter.cpp
View file

@ -65,22 +65,22 @@ struct print_expr_fn {
void print_binder(char const * bname, expr const & e, context const & c) {
out() << bname << " ";
if (binder_info(e).is_implicit())
if (binding_info(e).is_implicit())
out() << "{";
else if (binder_info(e).is_cast())
else if (binding_info(e).is_cast())
out() << "[";
out() << binder_name(e) << " : ";
print_child(binder_domain(e), c);
if (binder_info(e).is_implicit())
out() << binding_name(e) << " : ";
print_child(binding_domain(e), c);
if (binding_info(e).is_implicit())
out() << "}";
else if (binder_info(e).is_cast())
else if (binding_info(e).is_cast())
out() << "]";
out() << ", ";
print_child(binder_body(e), extend(c, binder_name(e), binder_domain(e)));
print_child(binding_body(e), extend(c, binding_name(e), binding_domain(e)));
}
void print_const(expr const & a) {
list<level> const & ls = const_level_params(a);
list<level> const & ls = const_levels(a);
out() << const_name(a);
if (!is_nil(ls)) {
out() << ".{";
@ -104,7 +104,7 @@ struct print_expr_fn {
case expr_kind::Var: {
auto e = find(c, var_idx(a));
if (e)
out() << e->first << "#" << var_idx(a);
out() << e->get_name() << "#" << var_idx(a);
else
out() << "#" << var_idx(a);
break;
@ -122,9 +122,9 @@ struct print_expr_fn {
if (!is_arrow(a)) {
print_binder("Pi", a, c);
} else {
print_child(binder_domain(a), c);
print_child(binding_domain(a), c);
out() << " -> ";
print_arrow_body(binder_body(a), extend(c, binder_name(a), binder_domain(a)));
print_arrow_body(binding_body(a), extend(c, binding_binder(a)));
}
break;
case expr_kind::Let:

2
src/kernel/free_vars.cpp
View file

@ -67,7 +67,7 @@ protected:
result = apply(app_fn(e), offset) || apply(app_arg(e), offset);
break;
case expr_kind::Lambda: case expr_kind::Pi:
result = apply(binder_domain(e), offset) || apply(binder_body(e), offset + 1);
result = apply(binding_domain(e), offset) || apply(binding_body(e), offset + 1);
break;
case expr_kind::Let:
result = apply(let_type(e), offset) || apply(let_value(e), offset) || apply(let_body(e), offset + 1);

4
src/kernel/inductive/inductive.cpp
View file

@ -8,14 +8,14 @@ Author: Leonardo de Moura
namespace lean {
namespace inductive {
environment add_inductive(environment const & env, name const & ind_name, level_params const & level_params,
environment add_inductive(environment const & env, name const & ind_name, level_param_names const & level_params,
telescope const & params, telescope const & indices, list<intro_rule> const & intro_rules,
optional<unsigned> const & univ_offset) {
return add_inductive(env, level_params, params, list<inductive_decl>(std::make_tuple(ind_name, indices, intro_rules)), univ_offset);
}
environment add_inductive(environment const & env,
level_params const & level_params,
level_param_names const & level_params,
telescope const & params,
list<inductive_decl> const & decls,
optional<unsigned> const & univ_offset) {

7
src/kernel/inductive/inductive.h
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include <tuple>
#include "util/list.h"
#include "kernel/environment.h"
#include "kernel/context.h"
namespace lean {
namespace inductive {
@ -22,8 +23,6 @@ typedef std::tuple<name, // introduction rule name
expr // result type
> intro_rule;
typedef param_names level_params;
/** \brief Inductive datatype */
typedef std::tuple<name, // datatype name
telescope, // indices
@ -32,7 +31,7 @@ typedef std::tuple<name, // datatype name
/** \brief Declare a finite set of mutually dependent inductive datatypes. */
environment add_inductive(environment const & env,
level_params const & level_params,
level_param_names const & level_params,
telescope const & params,
list<inductive_decl> const & decls,
// By default the resultant inductive datatypes live in max(level_params),
@ -43,7 +42,7 @@ environment add_inductive(environment const & env,
/** \brief Declare a single inductive datatype. */
environment add_inductive(environment const & env,
name const & ind_name, // name of new inductive datatype
level_params const & level_params, // level parameters
level_param_names const & level_params, // level parameters
telescope const & params, // parameters
telescope const & indices, // indices
list<intro_rule> const & intro_rules, // introduction rules

10
src/kernel/instantiate.cpp
View file

@ -61,12 +61,12 @@ expr apply_beta(expr f, unsigned num_args, expr const * args) {
return mk_rev_app(f, num_args, args);
} else {
unsigned m = 1;
while (is_lambda(binder_body(f)) && m < num_args) {
f = binder_body(f);
while (is_lambda(binding_body(f)) && m < num_args) {
f = binding_body(f);
m++;
}
lean_assert(m <= num_args);
return mk_rev_app(instantiate(binder_body(f), m, args + (num_args - m)), num_args - m, args);
return mk_rev_app(instantiate(binding_body(f), m, args + (num_args - m)), num_args - m, args);
}
}
@ -106,14 +106,14 @@ expr beta_reduce(expr t) {
}
}
expr instantiate_params(expr const & e, param_names const & ps, levels const & ls) {
expr instantiate_params(expr const & e, level_param_names const & ps, levels const & ls) {
if (!has_param_univ(e))
return e;
return replace(e, [&](expr const & e, unsigned) -> optional<expr> {
if (!has_param_univ(e))
return some_expr(e);
if (is_constant(e)) {
return some_expr(update_constant(e, map_reuse(const_level_params(e),
return some_expr(update_constant(e, map_reuse(const_levels(e),
[&](level const & l) { return instantiate(l, ps, ls); },
[](level const & l1, level const & l2) { return is_eqp(l1, l2); })));
} else if (is_sort(e)) {

2
src/kernel/instantiate.h
View file

@ -28,5 +28,5 @@ expr beta_reduce(expr t);
\pre length(ps) == length(ls)
*/
expr instantiate_params(expr const & e, param_names const & ps, levels const & ls);
expr instantiate_params(expr const & e, level_param_names const & ps, levels const & ls);
}

4
src/kernel/level.cpp
View file

@ -380,7 +380,7 @@ level replace_level_fn::apply(level const & l) {
lean_unreachable(); // LCOV_EXCL_LINE
}
optional<name> get_undef_param(level const & l, param_names const & ps) {
optional<name> get_undef_param(level const & l, level_param_names const & ps) {
optional<name> r;
for_each(l, [&](level const & l) {
if (!has_param(l) || r)
@ -420,7 +420,7 @@ level update_max(level const & l, level const & new_lhs, level const & new_rhs)
return mk_imax(new_lhs, new_rhs);
}
level instantiate(level const & l, param_names const & ps, levels const & ls) {
level instantiate(level const & l, level_param_names const & ps, levels const & ls) {
lean_assert(length(ps) == length(ls));
return replace(l, [=](level const & l) {
if (!has_param(l)) {

6
src/kernel/level.h
View file

@ -174,19 +174,19 @@ public:
};
template<typename F> level replace(level const & l, F const & f) { return replace_level_fn(f)(l); }
typedef list<name> param_names;
typedef list<name> level_param_names;
/** \brief If \c l contains a global that is not in \c env, then return it. Otherwise, return none. */
optional<name> get_undef_global(level const & l, environment const & env);
/** \brief If \c l contains a parameter that is not in \c ps, then return it. Otherwise, return none. */
optional<name> get_undef_param(level const & l, param_names const & ps);
optional<name> get_undef_param(level const & l, level_param_names const & ps);
/**
\brief Instantiate the universe level parameters \c ps occurring in \c l with the levels \c ls.
\pre length(ps) == length(ls)
*/
level instantiate(level const & l, param_names const & ps, levels const & ls);
level instantiate(level const & l, level_param_names const & ps, levels const & ls);
/** \brief Printer for debugging purposes */
std::ostream & operator<<(std::ostream & out, level const & l);

2
src/kernel/max_sharing.cpp
View file

@ -36,7 +36,7 @@ struct max_sharing_fn::imp {
res = update_app(a, apply(app_fn(a)), apply(app_arg(a)));
break;
case expr_kind::Lambda: case expr_kind::Pi:
res = update_binder(a, apply(binder_domain(a)), apply(binder_body(a)));
res = update_binder(a, apply(binding_domain(a)), apply(binding_body(a)));
break;
case expr_kind::Let:
res = update_let(a, apply(let_type(a)), apply(let_value(a)), apply(let_body(a)));

2
src/kernel/metavar.cpp
View file

@ -146,7 +146,7 @@ protected:
}
virtual expr visit_constant(expr const & c) {
return update_constant(c, visit_levels(const_level_params(c)));
return update_constant(c, visit_levels(const_levels(c)));
}
virtual expr visit_meta(expr const & m) {

4
src/kernel/replace_fn.cpp
View file

@ -94,9 +94,9 @@ expr replace_fn::operator()(expr const & e) {
pop_rs(2);
break;
case expr_kind::Pi: case expr_kind::Lambda:
if (check_index(f, 0) && !visit(binder_domain(e), offset))
if (check_index(f, 0) && !visit(binding_domain(e), offset))
goto begin_loop;
if (check_index(f, 1) && !visit(binder_body(e), offset + 1))
if (check_index(f, 1) && !visit(binding_body(e), offset + 1))
goto begin_loop;
r = update_binder(e, rs(-2), rs(-1));
pop_rs(2);

4
src/kernel/replace_visitor.cpp
View file

@ -24,8 +24,8 @@ expr replace_visitor::visit_app(expr const & e) {
}
expr replace_visitor::visit_binder(expr const & e) {
lean_assert(is_binder(e));
expr new_d = visit(binder_domain(e));
expr new_b = visit(binder_body(e));
expr new_d = visit(binding_domain(e));
expr new_b = visit(binding_body(e));
return update_binder(e, new_d, new_b);
}
expr replace_visitor::visit_lambda(expr const & e) { return visit_binder(e); }

38
src/kernel/type_checker.cpp
View file

@ -69,7 +69,7 @@ struct type_checker::imp {
type_checker_context m_tc_ctx;
bool m_memoize;
// temp flag
param_names m_params;
level_param_names m_params;
imp(environment const & env, name_generator const & g, constraint_handler & h, std::unique_ptr<converter> && conv, bool memoize):
m_env(env), m_gen(g), m_chandler(h), m_conv(std::move(conv)), m_conv_ctx(*this), m_tc_ctx(*this),
@ -84,9 +84,9 @@ struct type_checker::imp {
\brief Return the body of the given binder, where the free variable #0 is replaced with a fresh local constant.
It also returns the fresh local constant.
*/
std::pair<expr, expr> open_binder_body(expr const & e) {
expr local = mk_local(m_gen.next() + binder_name(e), binder_domain(e));
return mk_pair(instantiate(binder_body(e), local), local);
std::pair<expr, expr> open_binding_body(expr const & e) {
expr local = mk_local(m_gen.next() + binding_name(e), binding_domain(e));
return mk_pair(instantiate(binding_body(e), local), local);
}
/** \brief Add given constraint to the constraint handler m_chandler. */
@ -235,7 +235,7 @@ struct type_checker::imp {
[=](formatter const & fmt, options const & o, substitution const & subst) {
return pp_app_type_mismatch(fmt, m_env, o,
subst.instantiate_metavars_wo_jst(e),
subst.instantiate_metavars_wo_jst(binder_domain(fn_type)),
subst.instantiate_metavars_wo_jst(binding_domain(fn_type)),
subst.instantiate_metavars_wo_jst(arg_type));
});
}
@ -303,7 +303,7 @@ struct type_checker::imp {
case expr_kind::Constant: {
definition d = m_env.get(const_name(e));
auto const & ps = d.get_params();
auto const & ls = const_level_params(e);
auto const & ls = const_levels(e);
if (length(ps) != length(ls))
throw_kernel_exception(m_env, sstream() << "incorrect number of universe levels parameters for '" << const_name(e) << "', #"
<< length(ps) << " expected, #" << length(ls) << " provided");
@ -332,17 +332,17 @@ struct type_checker::imp {
}
case expr_kind::Lambda: {
if (!infer_only) {
expr t = infer_type_core(binder_domain(e), infer_only);
ensure_sort(t, binder_domain(e));
expr t = infer_type_core(binding_domain(e), infer_only);
ensure_sort(t, binding_domain(e));
}
auto b = open_binder_body(e);
r = mk_pi(binder_name(e), binder_domain(e), abstract_p(infer_type_core(b.first, infer_only), b.second), binder_info(e));
auto b = open_binding_body(e);
r = mk_pi(binding_name(e), binding_domain(e), abstract_p(infer_type_core(b.first, infer_only), b.second), binding_info(e));
break;
}
case expr_kind::Pi: {
expr t1 = ensure_sort(infer_type_core(binder_domain(e), infer_only), binder_domain(e));
auto b = open_binder_body(e);
expr t2 = ensure_sort(infer_type_core(b.first, infer_only), binder_body(e));
expr t1 = ensure_sort(infer_type_core(binding_domain(e), infer_only), binding_domain(e));
auto b = open_binding_body(e);
expr t2 = ensure_sort(infer_type_core(b.first, infer_only), binding_body(e));
if (m_env.impredicative())
r = mk_sort(mk_imax(sort_level(t1), sort_level(t2)));
else
@ -354,14 +354,14 @@ struct type_checker::imp {
if (!infer_only) {
expr a_type = infer_type_core(app_arg(e), infer_only);
delayed_justification jst([=]() { return mk_app_mismatch_jst(e, f_type, a_type); });
if (!is_def_eq(a_type, binder_domain(f_type), jst)) {
if (!is_def_eq(a_type, binding_domain(f_type), jst)) {
throw_kernel_exception(m_env, e,
[=](formatter const & fmt, options const & o) {
return pp_app_type_mismatch(fmt, m_env, o, e, binder_domain(f_type), a_type);
return pp_app_type_mismatch(fmt, m_env, o, e, binding_domain(f_type), a_type);
});
}
}
r = instantiate(binder_body(f_type), app_arg(e));
r = instantiate(binding_body(f_type), app_arg(e));
break;
}
case expr_kind::Let:
@ -387,8 +387,8 @@ struct type_checker::imp {
}
expr infer_type(expr const & e) { return infer_type_core(e, true); }
expr check(expr const & e, param_names const & ps) {
flet<param_names> updt(m_params, ps);
expr check(expr const & e, level_param_names const & ps) {
flet<level_param_names> updt(m_params, ps);
return infer_type_core(e, false);
}
bool is_def_eq(expr const & t, expr const & s) { return m_conv->is_def_eq(t, s, m_conv_ctx); }
@ -410,7 +410,7 @@ type_checker::type_checker(environment const & env):
type_checker::~type_checker() {}
expr type_checker::infer(expr const & t) { return m_ptr->infer_type(t); }
expr type_checker::check(expr const & t, param_names const & ps) { return m_ptr->check(t, ps); }
expr type_checker::check(expr const & t, level_param_names const & ps) { return m_ptr->check(t, ps); }
bool type_checker::is_def_eq(expr const & t, expr const & s) { return m_ptr->is_def_eq(t, s); }
bool type_checker::is_prop(expr const & t) { return m_ptr->is_prop(t); }
expr type_checker::whnf(expr const & t) { return m_ptr->whnf(t); }

2
src/kernel/type_checker.h
View file

@ -84,7 +84,7 @@ public:
The result is meaningful only if the constraints sent to the
constraint handler can be solved.
*/
expr check(expr const & t, param_names const & ps = param_names());
expr check(expr const & t, level_param_names const & ps = level_param_names());
/** \brief Return true iff t is definitionally equal to s. */
bool is_def_eq(expr const & t, expr const & s);
/** \brief Return true iff t is a proposition. */

4
src/library/deep_copy.cpp
View file

@ -28,8 +28,8 @@ class deep_copy_fn {
case expr_kind::Sort:
case expr_kind::Macro: r = copy(a); break;
case expr_kind::App: r = mk_app(apply(app_fn(a)), apply(app_arg(a))); break;
case expr_kind::Lambda: r = mk_lambda(binder_name(a), apply(binder_domain(a)), apply(binder_body(a))); break;
case expr_kind::Pi: r = mk_pi(binder_name(a), apply(binder_domain(a)), apply(binder_body(a))); break;
case expr_kind::Lambda: r = mk_lambda(binding_name(a), apply(binding_domain(a)), apply(binding_body(a))); break;
case expr_kind::Pi: r = mk_pi(binding_name(a), apply(binding_domain(a)), apply(binding_body(a))); break;
case expr_kind::Let: r = mk_let(let_name(a), apply(let_type(a)), apply(let_value(a)), apply(let_body(a))); break;
case expr_kind::Meta: r = mk_metavar(mlocal_name(a), apply(mlocal_type(a))); break;
case expr_kind::Local: r = mk_local(mlocal_name(a), apply(mlocal_type(a))); break;

8
src/library/expr_lt.cpp
View file

@ -27,17 +27,17 @@ bool is_lt(expr const & a, expr const & b, bool use_hash) {
if (const_name(a) != const_name(b))
return const_name(a) < const_name(b);
else
return is_lt(const_level_params(a), const_level_params(b), use_hash);
return is_lt(const_levels(a), const_levels(b), use_hash);
case expr_kind::App:
if (app_fn(a) != app_fn(b))
return is_lt(app_fn(a), app_fn(b), use_hash);
else
return is_lt(app_arg(a), app_arg(b), use_hash);
case expr_kind::Lambda: case expr_kind::Pi:
if (binder_domain(a) != binder_domain(b))
return is_lt(binder_domain(a), binder_domain(b), use_hash);
if (binding_domain(a) != binding_domain(b))
return is_lt(binding_domain(a), binding_domain(b), use_hash);
else
return is_lt(binder_body(a), binder_body(b), use_hash);
return is_lt(binding_body(a), binding_body(b), use_hash);
case expr_kind::Sort:
return is_lt(sort_level(a), sort_level(b), use_hash);
case expr_kind::Let:

70
src/library/kernel_bindings.cpp
View file

@ -172,36 +172,36 @@ static void open_level(lua_State * L) {
}
// Expr_binder_info
DECL_UDATA(expr_binder_info)
DECL_UDATA(binder_info)
static int mk_binder_info(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 0)
return push_expr_binder_info(L, expr_binder_info());
return push_binder_info(L, binder_info());
else if (nargs == 1)
return push_expr_binder_info(L, expr_binder_info(lua_toboolean(L, 1)));
return push_binder_info(L, binder_info(lua_toboolean(L, 1)));
else if (nargs == 2)
return push_expr_binder_info(L, expr_binder_info(lua_toboolean(L, 1), lua_toboolean(L, 2)));
return push_binder_info(L, binder_info(lua_toboolean(L, 1), lua_toboolean(L, 2)));
else
return push_expr_binder_info(L, expr_binder_info(lua_toboolean(L, 1), lua_toboolean(L, 2), lua_toboolean(L, 3)));
return push_binder_info(L, binder_info(lua_toboolean(L, 1), lua_toboolean(L, 2), lua_toboolean(L, 3)));
}
static int binder_info_is_implicit(lua_State * L) { return push_boolean(L, to_expr_binder_info(L, 1).is_implicit()); }
static int binder_info_is_cast(lua_State * L) { return push_boolean(L, to_expr_binder_info(L, 1).is_cast()); }
static int binder_info_is_contextual(lua_State * L) { return push_boolean(L, to_expr_binder_info(L, 1).is_contextual()); }
static int binder_info_is_implicit(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_implicit()); }
static int binder_info_is_cast(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_cast()); }
static int binder_info_is_contextual(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_contextual()); }
static const struct luaL_Reg binder_info_m[] = {
{"__gc", expr_binder_info_gc},
{"__gc", binder_info_gc},
{"is_implicit", safe_function<binder_info_is_implicit>},
{"is_cast", safe_function<binder_info_is_cast>},
{"is_contextual", safe_function<binder_info_is_contextual>},
{0, 0}
};
static void open_binder_info(lua_State * L) {
luaL_newmetatable(L, expr_binder_info_mt);
luaL_newmetatable(L, binder_info_mt);
lua_pushvalue(L, -1);
lua_setfield(L, -2, "__index");
setfuncs(L, binder_info_m, 0);
SET_GLOBAL_FUN(mk_binder_info, "binder_info");
SET_GLOBAL_FUN(expr_binder_info_pred, "is_binder_info");
SET_GLOBAL_FUN(binder_info_pred, "is_binder_info");
}
// Expressions
@ -271,14 +271,14 @@ static int expr_mk_lambda(lua_State * L) {
if (nargs == 3)
return push_expr(L, mk_lambda(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3)));
else
return push_expr(L, mk_lambda(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3), to_expr_binder_info(L, 4)));
return push_expr(L, mk_lambda(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3), to_binder_info(L, 4)));
}
static int expr_mk_pi(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 3)
return push_expr(L, mk_pi(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3)));
else
return push_expr(L, mk_pi(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3), to_expr_binder_info(L, 4)));
return push_expr(L, mk_pi(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3), to_binder_info(L, 4)));
}
static int expr_mk_arrow(lua_State * L) {
int nargs = lua_gettop(L);
@ -426,7 +426,7 @@ static int expr_fields(lua_State * L) {
case expr_kind::Var:
return push_integer(L, var_idx(e));
case expr_kind::Constant:
push_name(L, const_name(e)); push_list_level(L, const_level_params(e)); return 2;
push_name(L, const_name(e)); push_list_level(L, const_levels(e)); return 2;
case expr_kind::Sort:
return push_level(L, sort_level(e));
case expr_kind::Macro:
@ -435,7 +435,7 @@ static int expr_fields(lua_State * L) {
push_expr(L, app_fn(e)); push_expr(L, app_arg(e)); return 2;
case expr_kind::Lambda:
case expr_kind::Pi:
push_name(L, binder_name(e)); push_expr(L, binder_domain(e)); push_expr(L, binder_body(e)); push_expr_binder_info(L, binder_info(e)); return 4;
push_name(L, binding_name(e)); push_expr(L, binding_domain(e)); push_expr(L, binding_body(e)); push_binder_info(L, binding_info(e)); return 4;
case expr_kind::Let:
push_name(L, let_name(e)); push_expr(L, let_type(e)); push_expr(L, let_value(e)); push_expr(L, let_body(e)); return 4;
case expr_kind::Meta:
@ -524,10 +524,10 @@ static int expr_abstract(lua_State * L) {
}
}
static int binder_name(lua_State * L) { return push_name(L, binder_name(to_binder(L, 1))); }
static int binder_domain(lua_State * L) { return push_expr(L, binder_domain(to_binder(L, 1))); }
static int binder_body(lua_State * L) { return push_expr(L, binder_body(to_binder(L, 1))); }
static int binder_info(lua_State * L) { return push_expr_binder_info(L, binder_info(to_binder(L, 1))); }
static int binding_name(lua_State * L) { return push_name(L, binding_name(to_binder(L, 1))); }
static int binding_domain(lua_State * L) { return push_expr(L, binding_domain(to_binder(L, 1))); }
static int binding_body(lua_State * L) { return push_expr(L, binding_body(to_binder(L, 1))); }
static int binding_info(lua_State * L) { return push_binder_info(L, binding_info(to_binder(L, 1))); }
static int let_name(lua_State * L) { return push_name(L, let_name(to_let(L, 1))); }
static int let_type(lua_State * L) { return push_expr(L, let_type(to_let(L, 1))); }
@ -587,10 +587,10 @@ static const struct luaL_Reg expr_m[] = {
{"fields", safe_function<expr_fields>},
{"data", safe_function<expr_fields>},
{"depth", safe_function<expr_depth>},
{"binder_name", safe_function<binder_name>},
{"binder_domain", safe_function<binder_domain>},
{"binder_body", safe_function<binder_body>},
{"binder_info", safe_function<binder_info>},
{"binding_name", safe_function<binding_name>},
{"binding_domain", safe_function<binding_domain>},
{"binding_body", safe_function<binding_body>},
{"binding_info", safe_function<binding_info>},
{"let_name", safe_function<let_name>},
{"let_type", safe_function<let_type>},
{"let_value", safe_function<let_value>},
@ -716,7 +716,7 @@ static int definition_get_value(lua_State * L) {
throw exception("arg #1 must be a definition");
}
static int definition_get_weight(lua_State * L) { return push_integer(L, to_definition(L, 1).get_weight()); }
static list<name> to_param_names(lua_State * L, int _idx) {
static list<name> to_level_param_names(lua_State * L, int _idx) {
return table_to_list<name>(L, _idx, [](lua_State * L, int idx) -> name {
if (is_level(L, idx)) {
level const & l = to_level(L, idx);
@ -735,23 +735,23 @@ static int definition_get_module_idx(lua_State * L) { return push_integer(L, to_
static int mk_var_decl(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 2)
return push_definition(L, mk_var_decl(to_name_ext(L, 1), param_names(), to_expr(L, 2)));
return push_definition(L, mk_var_decl(to_name_ext(L, 1), level_param_names(), to_expr(L, 2)));
else
return push_definition(L, mk_var_decl(to_name_ext(L, 1), to_param_names(L, 2), to_expr(L, 3)));
return push_definition(L, mk_var_decl(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3)));
}
static int mk_axiom(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 2)
return push_definition(L, mk_axiom(to_name_ext(L, 1), param_names(), to_expr(L, 2)));
return push_definition(L, mk_axiom(to_name_ext(L, 1), level_param_names(), to_expr(L, 2)));
else
return push_definition(L, mk_axiom(to_name_ext(L, 1), to_param_names(L, 2), to_expr(L, 3)));
return push_definition(L, mk_axiom(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3)));
}
static int mk_theorem(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 3)
return push_definition(L, mk_theorem(to_name_ext(L, 1), param_names(), to_expr(L, 2), to_expr(L, 3)));
return push_definition(L, mk_theorem(to_name_ext(L, 1), level_param_names(), to_expr(L, 2), to_expr(L, 3)));
else
return push_definition(L, mk_theorem(to_name_ext(L, 1), to_param_names(L, 2), to_expr(L, 3), to_expr(L, 4)));
return push_definition(L, mk_theorem(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3), to_expr(L, 4)));
}
static void get_definition_args(lua_State * L, int idx, bool & opaque, unsigned & weight, module_idx & mod_idx, bool & use_conv_opt) {
opaque = get_bool_named_param(L, idx, "opaque", opaque);
@ -769,21 +769,21 @@ static int mk_definition(lua_State * L) {
throw exception("mk_definition must have at least 4 arguments, when the first argument is an environment");
} else if (is_expr(L, 3)) {
get_definition_args(L, 5, opaque, weight, mod_idx, use_conv_opt);
return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), param_names(),
return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), level_param_names(),
to_expr(L, 3), to_expr(L, 4), opaque, mod_idx, use_conv_opt));
} else {
get_definition_args(L, 6, opaque, weight, mod_idx, use_conv_opt);
return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), to_param_names(L, 3),
return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), to_level_param_names(L, 3),
to_expr(L, 4), to_expr(L, 5), opaque, mod_idx, use_conv_opt));
}
} else {
if (is_expr(L, 2)) {
get_definition_args(L, 4, opaque, weight, mod_idx, use_conv_opt);
return push_definition(L, mk_definition(to_name_ext(L, 1), param_names(), to_expr(L, 2),
return push_definition(L, mk_definition(to_name_ext(L, 1), level_param_names(), to_expr(L, 2),
to_expr(L, 3), opaque, weight, mod_idx, use_conv_opt));
} else {
get_definition_args(L, 5, opaque, weight, mod_idx, use_conv_opt);
return push_definition(L, mk_definition(to_name_ext(L, 1), to_param_names(L, 2),
return push_definition(L, mk_definition(to_name_ext(L, 1), to_level_param_names(L, 2),
to_expr(L, 3), to_expr(L, 4), opaque, weight, mod_idx, use_conv_opt));
}
}
@ -1572,7 +1572,7 @@ int type_checker_ensure_sort(lua_State * L) { return push_expr(L, to_type_checke
int type_checker_check(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs <= 2)
return push_expr(L, to_type_checker_ref(L, 1)->check(to_expr(L, 2), param_names()));
return push_expr(L, to_type_checker_ref(L, 1)->check(to_expr(L, 2), level_param_names()));
else
return push_expr(L, to_type_checker_ref(L, 1)->check(to_expr(L, 2), to_list_name(L, 3)));
}

28
src/library/kernel_serializer.cpp
View file

@ -116,16 +116,16 @@ static expr read_macro_definition(deserializer & d, unsigned num, expr const * a
return it->second(d, num, args);
}
serializer & operator<<(serializer & s, expr_binder_info const & i) {
serializer & operator<<(serializer & s, binder_info const & i) {
s.write_bool(i.is_implicit());
s.write_bool(i.is_cast());
return s;
}
static expr_binder_info read_expr_binder_info(deserializer & d) {
static binder_info read_binder_info(deserializer & d) {
bool imp = d.read_bool();
bool cast = d.read_bool();
return expr_binder_info(imp, cast);
return binder_info(imp, cast);
}
class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp> {
@ -141,7 +141,7 @@ class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp
s << var_idx(a);
break;
case expr_kind::Constant:
s << const_name(a) << const_level_params(a);
s << const_name(a) << const_levels(a);
break;
case expr_kind::Sort:
s << sort_level(a);
@ -157,7 +157,7 @@ class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp
write_core(app_fn(a)); write_core(app_arg(a));
break;
case expr_kind::Lambda: case expr_kind::Pi:
s << binder_name(a) << binder_info(a); write_core(binder_domain(a)); write_core(binder_body(a));
s << binding_name(a) << binding_info(a); write_core(binding_domain(a)); write_core(binding_body(a));
break;
case expr_kind::Let:
s << let_name(a); write_core(let_type(a)); write_core(let_value(a)); write_core(let_body(a));
@ -180,7 +180,7 @@ public:
expr read_binder(expr_kind k) {
deserializer & d = get_owner();
name n = read_name(d);
expr_binder_info i = read_expr_binder_info(d);
binder_info i = read_binder_info(d);
expr t = read();
return mk_binder(k, n, t, read(), i);
}
@ -251,8 +251,8 @@ expr read_expr(deserializer & d) {
}
// Definition serialization
static serializer & operator<<(serializer & s, param_names const & ps) { return write_list<name>(s, ps); }
static param_names read_params(deserializer & d) { return read_list<name>(d); }
static serializer & operator<<(serializer & s, level_param_names const & ps) { return write_list<name>(s, ps); }
static level_param_names read_level_params(deserializer & d) { return read_list<name>(d); }
serializer & operator<<(serializer & s, definition const & d) {
char k = 0;
if (d.is_definition()) {
@ -274,12 +274,12 @@ serializer & operator<<(serializer & s, definition const & d) {
}
definition read_definition(deserializer & d, unsigned module_idx) {
char k = d.read_char();
bool has_value = (k & 1) != 0;
bool is_theorem = (k & 8) != 0;
name n = read_name(d);
param_names ps = read_params(d);
expr t = read_expr(d);
char k = d.read_char();
bool has_value = (k & 1) != 0;
bool is_theorem = (k & 8) != 0;
name n = read_name(d);
level_param_names ps = read_level_params(d);
expr t = read_expr(d);
if (has_value) {
expr v = read_expr(d);
if (is_theorem) {

22
src/tests/kernel/environment.cpp
View file

@ -20,43 +20,43 @@ static environment add_def(environment const & env, definition const & d) {
static void tst1() {
environment env1;
auto env2 = add_def(env1, mk_definition("Bool", param_names(), mk_Type(), mk_Bool()));
auto env2 = add_def(env1, mk_definition("Bool", level_param_names(), mk_Type(), mk_Bool()));
lean_assert(!env1.find("Bool"));
lean_assert(env2.find("Bool"));
lean_assert(env2.find("Bool")->get_value() == mk_Bool());
try {
auto env3 = add_def(env2, mk_definition("Bool", param_names(), mk_Type(), mk_Bool()));
auto env3 = add_def(env2, mk_definition("Bool", level_param_names(), mk_Type(), mk_Bool()));
lean_unreachable();
} catch (kernel_exception & ex) {
std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
}
try {
auto env4 = add_def(env2, mk_definition("BuggyBool", param_names(), mk_Bool(), mk_Bool()));
auto env4 = add_def(env2, mk_definition("BuggyBool", level_param_names(), mk_Bool(), mk_Bool()));
lean_unreachable();
} catch (kernel_exception & ex) {
std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
}
try {
auto env5 = add_def(env2, mk_definition("Type1", param_names(), mk_metavar("T", mk_sort(mk_meta_univ("l"))), mk_Type()));
auto env5 = add_def(env2, mk_definition("Type1", level_param_names(), mk_metavar("T", mk_sort(mk_meta_univ("l"))), mk_Type()));
lean_unreachable();
} catch (kernel_exception & ex) {
std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
}
try {
auto env6 = add_def(env2, mk_definition("Type1", param_names(), mk_Type(), mk_metavar("T", mk_sort(mk_meta_univ("l")))));
auto env6 = add_def(env2, mk_definition("Type1", level_param_names(), mk_Type(), mk_metavar("T", mk_sort(mk_meta_univ("l")))));
lean_unreachable();
} catch (kernel_exception & ex) {
std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
}
try {
auto env7 = add_def(env2, mk_definition("foo", param_names(), mk_Type() >> mk_Type(), mk_Bool()));
auto env7 = add_def(env2, mk_definition("foo", level_param_names(), mk_Type() >> mk_Type(), mk_Bool()));
lean_unreachable();
} catch (kernel_exception & ex) {
std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
}
expr A = Const("A");
expr x = Const("x");
auto env3 = add_def(env2, mk_definition("id", param_names(),
auto env3 = add_def(env2, mk_definition("id", level_param_names(),
Pi(A, mk_Type(), A >> A),
Fun({{A, mk_Type()}, {x, A}}, x)));
expr c = mk_local("c", Bool);
@ -73,16 +73,16 @@ static void tst1() {
static void tst2() {
environment env;
name base("base");
env = add_def(env, mk_var_decl(name(base, 0u), param_names(), Bool >> (Bool >> Bool)));
env = add_def(env, mk_var_decl(name(base, 0u), level_param_names(), Bool >> (Bool >> Bool)));
expr x = Const("x");
expr y = Const("y");
for (unsigned i = 1; i <= 100; i++) {
expr prev = Const(name(base, i-1));
env = add_def(env, mk_definition(env, name(base, i), param_names(), Bool >> (Bool >> Bool),
env = add_def(env, mk_definition(env, name(base, i), level_param_names(), Bool >> (Bool >> Bool),
Fun({{x, Bool}, {y, Bool}}, prev(prev(x, y), prev(y, x)))));
}
expr A = Const("A");
env = add_def(env, mk_definition("id", param_names(),
env = add_def(env, mk_definition("id", level_param_names(),
Pi(A, mk_Type(), A >> A),
Fun({{A, mk_Type()}, {x, A}}, x)));
type_checker checker(env, name_generator("tmp"));
@ -129,7 +129,7 @@ static void tst3() {
expr A = Const("A");
expr x = Const("x");
expr id = Const("id");
env = add_def(env, mk_definition("id", param_names(),
env = add_def(env, mk_definition("id", level_param_names(),
Pi(A, mk_Type(), A >> A),
Fun({{A, mk_Type()}, {x, A}}, x)));
expr mk = Const("mk");

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

@ -112,7 +112,7 @@ static unsigned count_core(expr const & a, expr_set & s) {
case expr_kind::App:
return count_core(app_fn(a), s) + count_core(app_arg(a), s) + 1;
case expr_kind::Lambda: case expr_kind::Pi:
return count_core(binder_domain(a), s) + count_core(binder_body(a), s) + 1;
return count_core(binding_domain(a), s) + count_core(binding_body(a), s) + 1;
case expr_kind::Let:
return count_core(let_value(a), s) + count_core(let_body(a), s) + 1;
}

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

@ -37,7 +37,7 @@ static void tst2() {
expr B = Const("Bool");
expr t = Fun({x, B}, Fun({y, B}, x));
lean_assert(closed(t));
lean_assert(!closed(binder_body(t)));
lean_assert(!closed(binding_body(t)));
}
static void tst3() {
@ -53,7 +53,7 @@ static void tst3() {
bool flag = true;
while (is_lambda(r)) {
flag = flag && closed(r);
r = binder_body(r);
r = binding_body(r);
}
}

22
src/tests/kernel/replace.cpp
View file

@ -35,8 +35,8 @@ static void tst2() {
lean_assert(instantiate(r, Const("a")) == mk_lambda("x", Type, mk_app({Var(0), Const("a"), Var(1)})));
lean_assert(instantiate(instantiate(r, Const("a")), Const("b")) ==
mk_lambda("x", Type, mk_app({Var(0), Const("a"), Const("b")})));
std::cout << instantiate(binder_body(r), Const("a")) << std::endl;
lean_assert(instantiate(binder_body(r), Const("a")) == mk_app({Const("a"), Var(0), Var(1)}));
std::cout << instantiate(binding_body(r), Const("a")) << std::endl;
lean_assert(instantiate(binding_body(r), Const("a")) == mk_app({Const("a"), Var(0), Var(1)}));
std::cout << instantiate(r, Var(10)) << std::endl;
lean_assert(instantiate(r, Var(10)) == mk_lambda("x", Type, mk_app({Var(0), Var(11), Var(1)})));
std::cout << mk_pi("_", Var(3), Var(4)) << std::endl;
@ -89,7 +89,7 @@ static void tst3() {
};
replace_fn replacer(proc, tracer(trace));
expr t = Fun({{x, A}, {y, A}}, f(x, f(f(f(x, x), f(y, d)), f(d, d))));
expr b = binder_body(t);
expr b = binding_body(t);
expr r = replacer(b);
std::cout << r << "\n";
lean_assert(r == Fun({y, A}, f(c, f(f(f(c, c), f(y, d)), f(d, d)))));
@ -97,14 +97,14 @@ static void tst3() {
std::cout << p.first << " --> " << p.second << "\n";
}
lean_assert(trace[c] == Var(1));
std::cout << arg(arg(binder_body(r), 2), 2) << "\n";
lean_assert(arg(arg(binder_body(r), 2), 2) == f(d, d));
lean_assert(trace.find(arg(arg(binder_body(r), 2), 2)) == trace.end());
lean_assert(trace.find(binder_body(r)) != trace.end());
lean_assert(trace.find(arg(binder_body(r), 2)) != trace.end());
lean_assert(trace.find(arg(arg(binder_body(r), 2), 1)) != trace.end());
lean_assert(trace.find(arg(arg(arg(binder_body(r), 2), 1), 1)) != trace.end());
lean_assert(trace.find(arg(arg(arg(binder_body(r), 2), 1), 2)) == trace.end());
std::cout << arg(arg(binding_body(r), 2), 2) << "\n";
lean_assert(arg(arg(binding_body(r), 2), 2) == f(d, d));
lean_assert(trace.find(arg(arg(binding_body(r), 2), 2)) == trace.end());
lean_assert(trace.find(binding_body(r)) != trace.end());
lean_assert(trace.find(arg(binding_body(r), 2)) != trace.end());
lean_assert(trace.find(arg(arg(binding_body(r), 2), 1)) != trace.end());
lean_assert(trace.find(arg(arg(arg(binding_body(r), 2), 1), 1)) != trace.end());
lean_assert(trace.find(arg(arg(arg(binding_body(r), 2), 1), 2)) == trace.end());
}
int main() {

16
tests/lua/expr3.lua
View file

@ -11,16 +11,16 @@ assert(not pcall(function() f:fn() end))
local pi1 = Pi(a, Bool, Type)
assert(pi1:is_pi())
assert(not pcall(function() f:binder_name() end))
assert(not pcall(function() f:binding_name() end))
local pi2 = mk_pi("a", Bool, Type, binder_info(true, true))
local pi3 = mk_pi("a", Bool, Type)
assert(pi2:binder_info():is_implicit())
assert(not pi3:binder_info():is_implicit())
assert(pi2:binding_info():is_implicit())
assert(not pi3:binding_info():is_implicit())
local l1 = mk_lambda("a", Bool, Var(0))
local l2 = mk_lambda("a", Bool, Var(0), binder_info(true, false))
assert(not l1:binder_info():is_implicit())
assert(l2:binder_info():is_implicit())
assert(not l1:binding_info():is_implicit())
assert(l2:binding_info():is_implicit())
local let1 = mk_let("a", Bool, Const("true"), f(Var(0)))
@ -32,9 +32,9 @@ local pi4 = Pi(a, Bool, b, Bool, a)
print(pi4)
assert(not pcall(function() Pi(a, Bool, b, Bool) end))
assert(not pcall(function() Pi({}, Bool) end))
assert(pi4:binder_name() == name("a"))
assert(pi4:binder_domain() == Bool)
assert(pi4:binder_body():is_pi())
assert(pi4:binding_name() == name("a"))
assert(pi4:binding_domain() == Bool)
assert(pi4:binding_body():is_pi())
assert(f:kind() == expr_kind.Constant)

8
tests/lua/tag1.lua
View file

@ -4,14 +4,14 @@ local a = Const("a")
local t1 = f(x, a, Var(1))
local t2 = Fun(x, Bool, t1)
assert(not t2:tag())
assert(not t2:binder_body():tag())
assert(not t2:binding_body():tag())
t2:set_tag(2)
t2:binder_body():set_tag(1)
t2:binding_body():set_tag(1)
assert(t2:tag() == 2)
assert(t2:binder_body():tag() == 1)
assert(t2:binding_body():tag() == 1)
print(t2)
local new_t2 = t2:instantiate(Const("b"))
assert(new_t2:tag() == 2)
assert(new_t2:binder_body():tag() == 1)
assert(new_t2:binding_body():tag() == 1)
assert(not (t2 == new_t2))

4
tests/lua/tc3.lua
View file

@ -12,7 +12,7 @@ assert(T1 == T2) -- The default equality ignores binder information
assert(not (T1:is_bi_equal(T2)))
print(tc:check(t1))
print(tc:check(t2))
assert(tc:check(t1):binder_info():is_implicit())
assert(not tc:check(t2):binder_info():is_implicit())
assert(tc:check(t1):binding_info():is_implicit())
assert(not tc:check(t2):binding_info():is_implicit())
assert(tc:check(t1):is_bi_equal(T1))
assert(tc:check(t2):is_bi_equal(T2))