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

refactor(kernel/expr): tag expressions at "creation" time

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-15 13:12:09 -07:00
parent d960c1994e
commit 814778abb1
4 changed files with 185 additions and 135 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/abstract.cpp
View file

@ -20,7 +20,7 @@ expr abstract(expr const & e, unsigned s, unsigned n, expr const * subst) {
while (i > 0) {
--i;
if (subst[i] == e)
return some_expr(copy_tag(e, mk_var(offset + s + n - i - 1)));
return some_expr(mk_var(offset + s + n - i - 1, e.get_tag()));
}
}
return none_expr();
@ -41,7 +41,7 @@ expr abstract_locals(expr const & e, unsigned n, expr const * subst) {
while (i > 0) {
--i;
if (mlocal_name(subst[i]) == mlocal_name(m))
return some_expr(copy_tag(m, mk_var(offset + n - i - 1)));
return some_expr(mk_var(offset + n - i - 1, m.get_tag()));
}
}
return none_expr();

127
src/kernel/expr.cpp
View file

@ -52,7 +52,8 @@ unsigned hash_levels(levels const & ls) {
LEAN_THREAD_VALUE(unsigned, g_hash_alloc_counter, 0);
expr_cell::expr_cell(expr_kind k, unsigned h, bool has_expr_mv, bool has_univ_mv, bool has_local, bool has_param_univ):
expr_cell::expr_cell(expr_kind k, unsigned h, bool has_expr_mv, bool has_univ_mv,
bool has_local, bool has_param_univ, tag g):
m_flags(0),
m_kind(static_cast<unsigned>(k)),
m_has_expr_mv(has_expr_mv),
@ -60,7 +61,7 @@ expr_cell::expr_cell(expr_kind k, unsigned h, bool has_expr_mv, bool has_univ_mv
m_has_local(has_local),
m_has_param_univ(has_param_univ),
m_hash(h),
m_tag(nulltag),
m_tag(g),
m_rc(0) {
// m_hash_alloc does not need to be a unique identifier.
// We want diverse hash codes because given expr_cell * c1 and expr_cell * c2,
@ -110,8 +111,8 @@ bool is_meta(expr const & e) {
// Expr variables
DEF_THREAD_MEMORY_POOL(get_var_allocator, sizeof(expr_var));
expr_var::expr_var(unsigned idx):
expr_cell(expr_kind::Var, idx, false, false, false, false),
expr_var::expr_var(unsigned idx, tag g):
expr_cell(expr_kind::Var, idx, false, false, false, false, g),
m_vidx(idx) {
if (idx == std::numeric_limits<unsigned>::max())
throw exception("invalid free variable index, de Bruijn index is too big");
@ -123,8 +124,9 @@ void expr_var::dealloc() {
// Expr constants
DEF_THREAD_MEMORY_POOL(get_const_allocator, sizeof(expr_const));
expr_const::expr_const(name const & n, levels const & ls):
expr_cell(expr_kind::Constant, ::lean::hash(n.hash(), hash_levels(ls)), false, has_meta(ls), false, has_param(ls)),
expr_const::expr_const(name const & n, levels const & ls, tag g):
expr_cell(expr_kind::Constant, ::lean::hash(n.hash(), hash_levels(ls)), false,
has_meta(ls), false, has_param(ls), g),
m_name(n),
m_levels(ls) {
}
@ -139,10 +141,10 @@ unsigned binder_info::hash() const {
// Expr metavariables and local variables
DEF_THREAD_MEMORY_POOL(get_mlocal_allocator, sizeof(expr_mlocal));
expr_mlocal::expr_mlocal(bool is_meta, name const & n, expr const & t):
expr_mlocal::expr_mlocal(bool is_meta, name const & n, expr const & t, tag g):
expr_composite(is_meta ? expr_kind::Meta : expr_kind::Local, n.hash(), is_meta || t.has_expr_metavar(), t.has_univ_metavar(),
!is_meta || t.has_local(), t.has_param_univ(),
1, get_free_var_range(t)),
1, get_free_var_range(t), g),
m_name(n),
m_type(t) {}
void expr_mlocal::dealloc(buffer<expr_cell*> & todelete) {
@ -152,8 +154,8 @@ void expr_mlocal::dealloc(buffer<expr_cell*> & todelete) {
}
DEF_THREAD_MEMORY_POOL(get_local_allocator, sizeof(expr_local));
expr_local::expr_local(name const & n, name const & pp_name, expr const & t, binder_info const & bi):
expr_mlocal(false, n, t),
expr_local::expr_local(name const & n, name const & pp_name, expr const & t, binder_info const & bi, tag g):
expr_mlocal(false, n, t, g),
m_pp_name(pp_name),
m_bi(bi) {}
void expr_local::dealloc(buffer<expr_cell*> & todelete) {
@ -164,21 +166,22 @@ void expr_local::dealloc(buffer<expr_cell*> & todelete) {
// Composite expressions
expr_composite::expr_composite(expr_kind k, unsigned h, bool has_expr_mv, bool has_univ_mv,
bool has_local, bool has_param_univ, unsigned w, unsigned fv_range):
expr_cell(k, h, has_expr_mv, has_univ_mv, has_local, has_param_univ),
bool has_local, bool has_param_univ, unsigned w, unsigned fv_range, tag g):
expr_cell(k, h, has_expr_mv, has_univ_mv, has_local, has_param_univ, g),
m_weight(w),
m_free_var_range(fv_range) {}
// Expr applications
DEF_THREAD_MEMORY_POOL(get_app_allocator, sizeof(expr_app));
expr_app::expr_app(expr const & fn, expr const & arg):
expr_app::expr_app(expr const & fn, expr const & arg, tag g):
expr_composite(expr_kind::App, ::lean::hash(fn.hash(), arg.hash()),
fn.has_expr_metavar() || arg.has_expr_metavar(),
fn.has_univ_metavar() || arg.has_univ_metavar(),
fn.has_local() || arg.has_local(),
fn.has_param_univ() || arg.has_param_univ(),
inc_weight(add_weight(get_weight(fn), get_weight(arg))),
std::max(get_free_var_range(fn), get_free_var_range(arg))),
std::max(get_free_var_range(fn), get_free_var_range(arg)),
g),
m_fn(fn), m_arg(arg) {
m_hash = ::lean::hash(m_hash, m_weight);
}
@ -202,14 +205,15 @@ bool operator==(binder_info const & i1, binder_info const & i2) {
// Expr binders (Lambda, Pi)
DEF_THREAD_MEMORY_POOL(get_binding_allocator, sizeof(expr_binding));
expr_binding::expr_binding(expr_kind k, name const & n, expr const & t, expr const & b, binder_info const & i):
expr_binding::expr_binding(expr_kind k, name const & n, expr const & t, expr const & b, binder_info const & i, tag g):
expr_composite(k, ::lean::hash(t.hash(), b.hash()),
t.has_expr_metavar() || b.has_expr_metavar(),
t.has_univ_metavar() || b.has_univ_metavar(),
t.has_local() || b.has_local(),
t.has_param_univ() || b.has_param_univ(),
inc_weight(add_weight(get_weight(t), get_weight(b))),
std::max(get_free_var_range(t), dec(get_free_var_range(b)))),
std::max(get_free_var_range(t), dec(get_free_var_range(b))),
g),
m_binder(n, t, i),
m_body(b) {
m_hash = ::lean::hash(m_hash, m_weight);
@ -224,8 +228,8 @@ void expr_binding::dealloc(buffer<expr_cell*> & todelete) {
// Expr Sort
DEF_THREAD_MEMORY_POOL(get_sort_allocator, sizeof(expr_sort));
expr_sort::expr_sort(level const & l):
expr_cell(expr_kind::Sort, ::lean::hash(l), false, has_meta(l), false, has_param(l)),
expr_sort::expr_sort(level const & l, tag g):
expr_cell(expr_kind::Sort, ::lean::hash(l), false, has_meta(l), false, has_param(l), g),
m_level(l) {
}
expr_sort::~expr_sort() {}
@ -274,7 +278,7 @@ static unsigned get_free_var_range(unsigned num, expr const * args) {
return r;
}
expr_macro::expr_macro(macro_definition const & m, unsigned num, expr const * args):
expr_macro::expr_macro(macro_definition const & m, unsigned num, expr const * args, tag g):
expr_composite(expr_kind::Macro,
lean::hash(num, [&](unsigned i) { return args[i].hash(); }, m.hash()),
std::any_of(args, args+num, [](expr const & e) { return e.has_expr_metavar(); }),
@ -282,7 +286,8 @@ expr_macro::expr_macro(macro_definition const & m, unsigned num, expr const * ar
std::any_of(args, args+num, [](expr const & e) { return e.has_local(); }),
std::any_of(args, args+num, [](expr const & e) { return e.has_param_univ(); }),
inc_weight(add_weight(num, args)),
get_free_var_range(num, args)),
get_free_var_range(num, args),
g),
m_definition(m),
m_num_args(num) {
m_args = new expr[num];
@ -321,20 +326,30 @@ inline expr cache(expr && e) { return e; }
bool enable_expr_caching(bool) { return true; } // NOLINT
#endif
expr mk_var(unsigned idx) { return cache(expr(new (get_var_allocator().allocate()) expr_var(idx))); }
expr mk_constant(name const & n, levels const & ls) { return cache(expr(new (get_const_allocator().allocate()) expr_const(n, ls))); }
expr mk_macro(macro_definition const & m, unsigned num, expr const * args) { return cache(expr(new expr_macro(m, num, args))); }
expr mk_metavar(name const & n, expr const & t) { return cache(expr(new (get_mlocal_allocator().allocate()) expr_mlocal(true, n, t))); }
expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi) {
return cache(expr(new (get_local_allocator().allocate()) expr_local(n, pp_n, t, bi)));
expr mk_var(unsigned idx, tag g) {
return cache(expr(new (get_var_allocator().allocate()) expr_var(idx, g)));
}
expr mk_app(expr const & f, expr const & a) {
return cache(expr(new (get_app_allocator().allocate()) expr_app(f, a)));
expr mk_constant(name const & n, levels const & ls, tag g) {
return cache(expr(new (get_const_allocator().allocate()) expr_const(n, ls, g)));
}
expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i) {
return cache(expr(new (get_binding_allocator().allocate()) expr_binding(k, n, t, e, i)));
expr mk_macro(macro_definition const & m, unsigned num, expr const * args, tag g) {
return cache(expr(new expr_macro(m, num, args, g)));
}
expr mk_metavar(name const & n, expr const & t, tag g) {
return cache(expr(new (get_mlocal_allocator().allocate()) expr_mlocal(true, n, t, g)));
}
expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi, tag g) {
return cache(expr(new (get_local_allocator().allocate()) expr_local(n, pp_n, t, bi, g)));
}
expr mk_app(expr const & f, expr const & a, tag g) {
return cache(expr(new (get_app_allocator().allocate()) expr_app(f, a, g)));
}
expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i, tag g) {
return cache(expr(new (get_binding_allocator().allocate()) expr_binding(k, n, t, e, i, g)));
}
expr mk_sort(level const & l, tag g) {
return cache(expr(new (get_sort_allocator().allocate()) expr_sort(l, g)));
}
expr mk_sort(level const & l) { return cache(expr(new (get_sort_allocator().allocate()) expr_sort(l))); }
// =======================================
typedef buffer<expr_cell*> del_buffer;
@ -365,38 +380,38 @@ void expr_cell::dealloc() {
}
// Auxiliary constructors
expr mk_app(expr const & f, unsigned num_args, expr const * args) {
expr mk_app(expr const & f, unsigned num_args, expr const * args, tag g) {
expr r = f;
for (unsigned i = 0; i < num_args; i++)
r = mk_app(r, args[i]);
r = mk_app(r, args[i], g);
return r;
}
expr mk_app(unsigned num_args, expr const * args) {
expr mk_app(unsigned num_args, expr const * args, tag g) {
lean_assert(num_args >= 2);
return mk_app(mk_app(args[0], args[1]), num_args - 2, args+2);
return mk_app(mk_app(args[0], args[1], g), num_args - 2, args+2, g);
}
expr mk_rev_app(expr const & f, unsigned num_args, expr const * args) {
expr mk_rev_app(expr const & f, unsigned num_args, expr const * args, tag g) {
expr r = f;
unsigned i = num_args;
while (i > 0) {
--i;
r = mk_app(r, args[i]);
r = mk_app(r, args[i], g);
}
return r;
}
expr mk_rev_app(unsigned num_args, expr const * args) {
expr mk_rev_app(unsigned num_args, expr const * args, tag g) {
lean_assert(num_args >= 2);
return mk_rev_app(mk_app(args[num_args-1], args[num_args-2]), num_args-2, args);
return mk_rev_app(mk_app(args[num_args-1], args[num_args-2], g), num_args-2, args, g);
}
expr mk_app_vars(expr const & f, unsigned n) {
expr mk_app_vars(expr const & f, unsigned n, tag g) {
expr r = f;
while (n > 0) {
--n;
r = mk_app(r, Var(n));
r = mk_app(r, mk_var(n, g), g);
}
return r;
}
@ -453,14 +468,16 @@ static name const & get_default_var_name() {
static name const & g_default_var_name = get_default_var_name(); // force it to be initialized
bool is_default_var_name(name const & n) { return n == get_default_var_name(); }
expr mk_arrow(expr const & t, expr const & e) { return mk_pi(get_default_var_name(), t, e); }
expr mk_arrow(expr const & t, expr const & e, tag g) {
return mk_pi(get_default_var_name(), t, e, binder_info(), g);
}
expr mk_pi(unsigned sz, expr const * domain, expr const & range) {
expr mk_pi(unsigned sz, expr const * domain, expr const & range, tag g) {
expr r = range;
unsigned i = sz;
while (i > 0) {
--i;
r = mk_pi(name(g_default_var_name, i), domain[i], r);
r = mk_pi(name(g_default_var_name, i), domain[i], r, binder_info(), g);
}
return r;
}
@ -494,7 +511,7 @@ expr copy_tag(expr const & e, expr && new_e) {
expr update_app(expr const & e, expr const & new_fn, expr const & new_arg) {
if (!is_eqp(app_fn(e), new_fn) || !is_eqp(app_arg(e), new_arg))
return copy_tag(e, mk_app(new_fn, new_arg));
return mk_app(new_fn, new_arg, e.get_tag());
else
return e;
}
@ -503,24 +520,24 @@ expr update_rev_app(expr const & e, unsigned num, expr const * new_args) {
expr const * it = &e;
for (unsigned i = 0; i < num - 1; i++) {
if (!is_app(*it) || !is_eqp(app_arg(*it), new_args[i]))
return copy_tag(e, mk_rev_app(num, new_args));
return mk_rev_app(num, new_args, e.get_tag());
it = &app_fn(*it);
}
if (!is_eqp(*it, new_args[num - 1]))
return copy_tag(e, mk_rev_app(num, new_args));
return mk_rev_app(num, new_args, e.get_tag());
return e;
}
expr update_binding(expr const & e, expr const & new_domain, expr const & new_body) {
if (!is_eqp(binding_domain(e), new_domain) || !is_eqp(binding_body(e), new_body))
return copy_tag(e, mk_binding(e.kind(), binding_name(e), new_domain, new_body, binding_info(e)));
return mk_binding(e.kind(), binding_name(e), new_domain, new_body, binding_info(e), e.get_tag());
else
return e;
}
expr update_binding(expr const & e, expr const & new_domain, expr const & new_body, binder_info const & bi) {
if (!is_eqp(binding_domain(e), new_domain) || !is_eqp(binding_body(e), new_body) || bi != binding_info(e))
return copy_tag(e, mk_binding(e.kind(), binding_name(e), new_domain, new_body, bi));
return mk_binding(e.kind(), binding_name(e), new_domain, new_body, bi, e.get_tag());
else
return e;
}
@ -529,16 +546,16 @@ expr update_mlocal(expr const & e, expr const & new_type) {
if (is_eqp(mlocal_type(e), new_type))
return e;
else if (is_metavar(e))
return copy_tag(e, mk_metavar(mlocal_name(e), new_type));
return mk_metavar(mlocal_name(e), new_type, e.get_tag());
else
return copy_tag(e, mk_local(mlocal_name(e), local_pp_name(e), new_type, local_info(e)));
return mk_local(mlocal_name(e), local_pp_name(e), new_type, local_info(e), e.get_tag());
}
expr update_local(expr const & e, expr const & new_type, binder_info const & bi) {
if (is_eqp(mlocal_type(e), new_type) && local_info(e) == bi)
return e;
else
return copy_tag(e, mk_local(mlocal_name(e), local_pp_name(e), new_type, bi));
return mk_local(mlocal_name(e), local_pp_name(e), new_type, bi, e.get_tag());
}
expr update_local(expr const & e, binder_info const & bi) {
@ -547,14 +564,14 @@ expr update_local(expr const & e, binder_info const & bi) {
expr update_sort(expr const & e, level const & new_level) {
if (!is_eqp(sort_level(e), new_level))
return copy_tag(e, mk_sort(new_level));
return mk_sort(new_level, e.get_tag());
else
return e;
}
expr update_constant(expr const & e, levels const & new_levels) {
if (!is_eqp(const_levels(e), new_levels))
return copy_tag(e, mk_constant(const_name(e), new_levels));
return mk_constant(const_name(e), new_levels, e.get_tag());
else
return e;
}
@ -569,7 +586,7 @@ expr update_macro(expr const & e, unsigned num, expr const * args) {
if (i == num)
return e;
}
return copy_tag(e, mk_macro(to_macro(e)->m_definition, num, args));
return mk_macro(to_macro(e)->m_definition, num, args, e.get_tag());
}
bool is_atomic(expr const & e) {

187
src/kernel/expr.h
View file

@ -69,7 +69,7 @@ protected:
static void dec_ref(expr & c, buffer<expr_cell*> & todelete);
public:
expr_cell(expr_kind k, unsigned h, bool has_expr_mv, bool has_univ_mv, bool has_local, bool has_param_univ);
expr_cell(expr_kind k, unsigned h, bool has_expr_mv, bool has_univ_mv, bool has_local, bool has_param_univ, tag g);
expr_kind kind() const { return static_cast<expr_kind>(m_kind); }
unsigned hash() const { return m_hash; }
unsigned hash_alloc() const { return m_hash_alloc; }
@ -128,29 +128,35 @@ public:
expr_cell * raw() const { return m_ptr; }
friend expr mk_var(unsigned idx);
friend expr mk_sort(level const & l);
friend expr mk_constant(name const & n, levels const & ls);
friend expr mk_metavar(name const & n, expr const & t);
friend expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi);
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_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i);
friend expr mk_macro(macro_definition const & m, unsigned num, expr const * args);
friend expr mk_var(unsigned idx, tag g);
friend expr mk_sort(level const & l, tag g);
friend expr mk_constant(name const & n, levels const & ls, tag g);
friend expr mk_metavar(name const & n, expr const & t, tag g);
friend expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi,
tag g);
friend expr mk_app(expr const & f, expr const & a, tag g);
friend expr mk_pair(expr const & f, expr const & s, expr const & t, tag g);
friend expr mk_proj(bool fst, expr const & p, tag g);
friend expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i,
tag g);
friend expr mk_macro(macro_definition const & m, unsigned num, expr const * args, tag g);
friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; }
// Overloaded operator() can be used to create applications
expr operator()(expr const & a1) const;
expr operator()(expr const & a1, expr const & a2) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5, expr const & a6) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5, expr const & a6,
expr const & a7) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5, expr const & a6,
expr const & a7, expr const & a8) const;
expr operator()(expr const & a1, tag g = nulltag) const;
expr operator()(expr const & a1, expr const & a2, tag g = nulltag) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, tag g = nulltag) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4,
tag g = nulltag) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4,
expr const & a5, tag g = nulltag) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4,
expr const & a5, expr const & a6, tag g = nulltag) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4,
expr const & a5, expr const & a6, expr const & a7, tag g = nulltag) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4,
expr const & a5, expr const & a6, expr const & a7, expr const & a8,
tag g = nulltag) const;
};
expr copy_tag(expr const & e, expr && new_e);
@ -181,7 +187,7 @@ class expr_var : public expr_cell {
friend expr_cell;
void dealloc();
public:
expr_var(unsigned idx);
expr_var(unsigned idx, tag g);
unsigned get_vidx() const { return m_vidx; }
};
@ -192,7 +198,7 @@ class expr_const : public expr_cell {
friend expr_cell;
void dealloc();
public:
expr_const(name const & n, levels const & ls);
expr_const(name const & n, levels const & ls, tag g);
name const & get_name() const { return m_name; }
levels const & get_levels() const { return m_levels; }
};
@ -206,7 +212,7 @@ protected:
friend unsigned get_free_var_range(expr const & e);
public:
expr_composite(expr_kind k, unsigned h, bool has_expr_mv, bool has_univ_mv, bool has_local,
bool has_param_univ, unsigned w, unsigned fv_range);
bool has_param_univ, unsigned w, unsigned fv_range, tag g);
};
/** \brief Metavariables and local constants */
@ -217,7 +223,7 @@ protected:
friend expr_cell;
void dealloc(buffer<expr_cell*> & todelete);
public:
expr_mlocal(bool is_meta, name const & n, expr const & t);
expr_mlocal(bool is_meta, name const & n, expr const & t, tag g);
name const & get_name() const { return m_name; }
expr const & get_type() const { return m_type; }
};
@ -273,7 +279,7 @@ class expr_local : public expr_mlocal {
friend expr_cell;
void dealloc(buffer<expr_cell*> & todelete);
public:
expr_local(name const & n, name const & pp_name, expr const & t, binder_info const & bi);
expr_local(name const & n, name const & pp_name, expr const & t, binder_info const & bi, tag g);
name const & get_pp_name() const { return m_pp_name; }
binder_info const & get_info() const { return m_bi; }
};
@ -285,7 +291,7 @@ class expr_app : public expr_composite {
friend expr_cell;
void dealloc(buffer<expr_cell*> & todelete);
public:
expr_app(expr const & fn, expr const & arg);
expr_app(expr const & fn, expr const & arg, tag g);
expr const & get_fn() const { return m_fn; }
expr const & get_arg() const { return m_arg; }
};
@ -296,7 +302,7 @@ class binder {
expr m_type;
binder_info m_info;
public:
binder(name const & n, expr const & t, binder_info const & bi = binder_info()):
binder(name const & n, expr const & t, binder_info const & bi):
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; }
@ -311,7 +317,8 @@ class expr_binding : public expr_composite {
friend class expr_cell;
void dealloc(buffer<expr_cell*> & todelete);
public:
expr_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i = binder_info());
expr_binding(expr_kind k, name const & n, expr const & t, expr const & e,
binder_info const & i, tag g);
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; }
@ -325,7 +332,7 @@ class expr_sort : public expr_cell {
friend expr_cell;
void dealloc();
public:
expr_sort(level const & l);
expr_sort(level const & l, tag g);
~expr_sort();
level const & get_level() const { return m_level; }
};
@ -399,7 +406,7 @@ class expr_macro : public expr_composite {
friend expr update_macro(expr const & e, unsigned num, expr const * args);
void dealloc(buffer<expr_cell*> & todelete);
public:
expr_macro(macro_definition const & v, unsigned num, expr const * args);
expr_macro(macro_definition const & v, unsigned num, expr const * args, tag g);
~expr_macro();
macro_definition const & get_def() const { return m_definition; }
@ -442,79 +449,105 @@ bool is_meta(expr const & e);
// =======================================
// Constructors
expr mk_var(unsigned idx);
expr mk_var(unsigned idx, tag g = nulltag);
inline expr Var(unsigned idx) { return mk_var(idx); }
expr mk_constant(name const & n, levels const & ls);
expr mk_constant(name const & n, levels const & ls, tag g = nulltag);
inline expr mk_constant(name const & n) { return mk_constant(n, levels()); }
inline expr Const(name const & n) { return mk_constant(n); }
expr mk_macro(macro_definition const & m, unsigned num = 0, expr const * args = nullptr);
expr mk_metavar(name const & n, expr const & t);
expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi);
inline expr mk_local(name const & n, expr const & t) { return mk_local(n, n, t, binder_info()); }
inline expr mk_local(name const & n, expr const & t, binder_info const & bi) { return mk_local(n, n, t, bi); }
inline expr Local(name const & n, expr const & t, binder_info const & bi = binder_info()) { return mk_local(n, t, bi); }
expr mk_app(expr const & f, expr const & a);
expr mk_app(expr const & f, unsigned num_args, expr const * args);
expr mk_app(unsigned num_args, expr const * args);
inline expr mk_app(std::initializer_list<expr> const & l) { return mk_app(l.size(), l.begin()); }
template<typename T> expr mk_app(T const & args) { return mk_app(args.size(), args.data()); }
template<typename T> expr mk_app(expr const & f, T const & args) { return mk_app(f, args.size(), args.data()); }
expr mk_rev_app(expr const & f, unsigned num_args, expr const * args);
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()); }
expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i = binder_info());
inline expr mk_lambda(name const & n, expr const & t, expr const & e, binder_info const & i = binder_info()) {
return mk_binding(expr_kind::Lambda, n, t, e, i);
expr mk_macro(macro_definition const & m, unsigned num = 0, expr const * args = nullptr, tag g = nulltag);
expr mk_metavar(name const & n, expr const & t, tag g = nulltag);
expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi, tag g = nulltag);
inline expr mk_local(name const & n, expr const & t, tag g = nulltag) { return mk_local(n, n, t, binder_info(), g); }
inline expr mk_local(name const & n, expr const & t, binder_info const & bi, tag g = nulltag) {
return mk_local(n, n, t, bi, g);
}
inline expr mk_pi(name const & n, expr const & t, expr const & e, binder_info const & i = binder_info()) {
return mk_binding(expr_kind::Pi, n, t, e, i);
inline expr Local(name const & n, expr const & t, binder_info const & bi = binder_info(), tag g = nulltag) {
return mk_local(n, t, bi, g);
}
expr mk_sort(level const & l);
expr mk_app(expr const & f, expr const & a, tag g = nulltag);
expr mk_app(expr const & f, unsigned num_args, expr const * args, tag g = nulltag);
expr mk_app(unsigned num_args, expr const * args, tag g = nulltag);
inline expr mk_app(std::initializer_list<expr> const & l, tag g = nulltag) {
return mk_app(l.size(), l.begin(), g);
}
template<typename T> expr mk_app(T const & args, tag g = nulltag) { return mk_app(args.size(), args.data(), g); }
template<typename T> expr mk_app(expr const & f, T const & args, tag g = nulltag) {
return mk_app(f, args.size(), args.data(), g);
}
expr mk_rev_app(expr const & f, unsigned num_args, expr const * args, tag g = nulltag);
expr mk_rev_app(unsigned num_args, expr const * args, tag g = nulltag);
template<typename T> expr mk_rev_app(T const & args, tag g = nulltag) { return mk_rev_app(args.size(), args.data(), g); }
template<typename T> expr mk_rev_app(expr const & f, T const & args, tag g = nulltag) {
return mk_rev_app(f, args.size(), args.data(), g);
}
expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e,
binder_info const & i = binder_info(), tag g = nulltag);
inline expr mk_lambda(name const & n, expr const & t, expr const & e,
binder_info const & i = binder_info(), tag g = nulltag) {
return mk_binding(expr_kind::Lambda, n, t, e, i, g);
}
inline expr mk_pi(name const & n, expr const & t, expr const & e, binder_info const & i = binder_info(), tag g = nulltag) {
return mk_binding(expr_kind::Pi, n, t, e, i, g);
}
expr mk_sort(level const & l, tag g = nulltag);
/** \brief Return <tt>Pi(x.{sz-1}, domain[sz-1], ..., Pi(x.{0}, domain[0], range)...)</tt> */
expr mk_pi(unsigned sz, expr const * domain, expr const & range);
inline expr mk_pi(buffer<expr> const & domain, expr const & range) { return mk_pi(domain.size(), domain.data(), range); }
expr mk_pi(unsigned sz, expr const * domain, expr const & range, tag g = nulltag);
inline expr mk_pi(buffer<expr> const & domain, expr const & range, tag g = nulltag) {
return mk_pi(domain.size(), domain.data(), range, g);
}
expr mk_Prop();
expr mk_Type();
bool is_default_var_name(name const & n);
expr mk_arrow(expr const & t, expr const & e);
expr mk_arrow(expr const & t, expr const & e, tag g = nulltag);
inline expr operator>>(expr const & t, expr const & e) { return mk_arrow(t, e); }
// Auxiliary
inline expr mk_app(expr const & e1, expr const & e2, expr const & e3) { return mk_app({e1, e2, e3}); }
inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({e1, e2, e3, e4}); }
inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) {
return mk_app({e1, e2, e3, e4, e5});
inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, tag g = nulltag) {
return mk_app({e1, e2, e3}, g);
}
inline expr expr::operator()(expr const & a1) const { return mk_app({*this, a1}); }
inline expr expr::operator()(expr const & a1, expr const & a2) const { return mk_app({*this, a1, a2}); }
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3) const { return mk_app({*this, a1, a2, a3}); }
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const {
return mk_app({*this, a1, a2, a3, a4});
inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, tag g = nulltag) {
return mk_app({e1, e2, e3, e4}, g);
}
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const {
return mk_app({*this, a1, a2, a3, a4, a5});
inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5,
tag g = nulltag) {
return mk_app({e1, e2, e3, e4, e5}, g);
}
inline expr expr::operator()(expr const & a, tag g) const {
return mk_app({*this, a}, g);
}
inline expr expr::operator()(expr const & a1, expr const & a2, tag g) const {
return mk_app({*this, a1, a2}, g);
}
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, tag g) const {
return mk_app({*this, a1, a2, a3}, g);
}
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, tag g) const {
return mk_app({*this, a1, a2, a3, a4}, g);
}
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4,
expr const & a5, tag g) const {
return mk_app({*this, a1, a2, a3, a4, a5}, g);
}
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5,
expr const & a6) const {
return mk_app({*this, a1, a2, a3, a4, a5, a6});
expr const & a6, tag g) const {
return mk_app({*this, a1, a2, a3, a4, a5, a6}, g);
}
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5,
expr const & a6, expr const & a7) const {
return mk_app({*this, a1, a2, a3, a4, a5, a6, a7});
expr const & a6, expr const & a7, tag g) const {
return mk_app({*this, a1, a2, a3, a4, a5, a6, a7}, g);
}
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5,
expr const & a6, expr const & a7, expr const & a8) const {
return mk_app({*this, a1, a2, a3, a4, a5, a6, a7, a8});
expr const & a6, expr const & a7, expr const & a8, tag g) const {
return mk_app({*this, a1, a2, a3, a4, a5, a6, a7, a8}, g);
}
/** \brief Return application (...((f x_{n-1}) x_{n-2}) ... x_0) */
expr mk_app_vars(expr const & f, unsigned n);
expr mk_app_vars(expr const & f, unsigned n, tag g = nulltag);
expr mk_local_for(expr const & b, name_generator const & ngen);
expr mk_local_for(expr const & b, name_generator const & ngen, tag g = nulltag);
bool enable_expr_caching(bool f);
/** \brief Helper class for temporarily enabling/disabling expression caching */

2
src/kernel/instantiate.cpp
View file

@ -30,7 +30,7 @@ struct instantiate_easy_fn {
if (app && is_app(a))
if (auto new_a = operator()(app_arg(a), false))
if (auto new_f = operator()(app_fn(a), true))
return some_expr(copy_tag(a, mk_app(*new_f, *new_a)));
return some_expr(mk_app(*new_f, *new_a, a.get_tag()));
return none_expr();
}
};