From 814778abb12da46d0bf1280c38b101f0abb7403b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Oct 2014 13:12:09 -0700 Subject: [PATCH] refactor(kernel/expr): tag expressions at "creation" time --- src/kernel/abstract.cpp | 4 +- src/kernel/expr.cpp | 127 ++++++++++++++----------- src/kernel/expr.h | 187 ++++++++++++++++++++++--------------- src/kernel/instantiate.cpp | 2 +- 4 files changed, 185 insertions(+), 135 deletions(-) diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp index 943cb7a75..5b21ab430 100644 --- a/src/kernel/abstract.cpp +++ b/src/kernel/abstract.cpp @@ -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(); diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 01cbc5a71..930d44af6 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -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(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::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 & todelete) { @@ -152,8 +154,8 @@ void expr_mlocal::dealloc(buffer & 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 & todelete) { @@ -164,21 +166,22 @@ void expr_local::dealloc(buffer & 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 & 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 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) { diff --git a/src/kernel/expr.h b/src/kernel/expr.h index dee56a4cf..683928bce 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -69,7 +69,7 @@ protected: static void dec_ref(expr & c, buffer & 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(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 & 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 & 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 & 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 & 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 & 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 const & l) { return mk_app(l.size(), l.begin()); } -template expr mk_app(T const & args) { return mk_app(args.size(), args.data()); } -template 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 expr mk_rev_app(T const & args) { return mk_rev_app(args.size(), args.data()); } -template 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 const & l, tag g = nulltag) { + return mk_app(l.size(), l.begin(), g); +} +template expr mk_app(T const & args, tag g = nulltag) { return mk_app(args.size(), args.data(), g); } +template 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 expr mk_rev_app(T const & args, tag g = nulltag) { return mk_rev_app(args.size(), args.data(), g); } +template 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 Pi(x.{sz-1}, domain[sz-1], ..., Pi(x.{0}, domain[0], range)...) */ -expr mk_pi(unsigned sz, expr const * domain, expr const & range); -inline expr mk_pi(buffer 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 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 */ diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index bde732f37..6aa237eef 100644 --- a/src/kernel/instantiate.cpp +++ b/src/kernel/instantiate.cpp @@ -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(); } };