diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 4b87c566a..833a6a587 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -36,10 +36,11 @@ unsigned hash_levels(levels const & ls) { MK_THREAD_LOCAL_GET(unsigned, get_hash_alloc_counter, 0) -expr_cell::expr_cell(expr_kind k, unsigned h, bool has_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): m_flags(0), m_kind(static_cast(k)), - m_has_mv(has_mv), + m_has_expr_mv(has_expr_mv), + m_has_univ_mv(has_univ_mv), m_has_local(has_local), m_has_param_univ(has_param_univ), m_hash(h), @@ -93,7 +94,7 @@ bool is_meta(expr const & e) { // Expr variables expr_var::expr_var(unsigned idx): - expr_cell(expr_kind::Var, idx, false, false, false), + expr_cell(expr_kind::Var, idx, false, false, false, false), m_vidx(idx) { if (idx == std::numeric_limits::max()) throw exception("invalid free variable index, de Bruijn index is too big"); @@ -101,13 +102,14 @@ expr_var::expr_var(unsigned idx): // Expr constants expr_const::expr_const(name const & n, levels const & ls): - expr_cell(expr_kind::Constant, ::lean::hash(n.hash(), hash_levels(ls)), has_meta(ls), false, has_param(ls)), + expr_cell(expr_kind::Constant, ::lean::hash(n.hash(), hash_levels(ls)), false, has_meta(ls), false, has_param(ls)), m_name(n), m_levels(ls) {} // Expr metavariables and local variables expr_mlocal::expr_mlocal(bool is_meta, name const & n, expr const & t): - expr_cell(is_meta ? expr_kind::Meta : expr_kind::Local, n.hash(), is_meta || t.has_metavar(), !is_meta || t.has_local(), t.has_param_univ()), + expr_cell(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()), m_name(n), m_type(t) {} void expr_mlocal::dealloc(buffer & todelete) { @@ -125,17 +127,19 @@ void expr_local::dealloc(buffer & todelete) { } // Composite expressions -expr_composite::expr_composite(expr_kind k, unsigned h, bool has_mv, bool has_local, bool has_param_univ, unsigned d, unsigned fv_range): - expr_cell(k, h, has_mv, has_local, has_param_univ), +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 d, unsigned fv_range): + expr_cell(k, h, has_expr_mv, has_univ_mv, has_local, has_param_univ), m_depth(d), m_free_var_range(fv_range) {} // Expr applications expr_app::expr_app(expr const & fn, expr const & arg): expr_composite(expr_kind::App, ::lean::hash(fn.hash(), arg.hash()), - fn.has_metavar() || arg.has_metavar(), - fn.has_local() || arg.has_local(), - fn.has_param_univ() || arg.has_param_univ(), + 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(), std::max(get_depth(fn), get_depth(arg)) + 1, std::max(get_free_var_range(fn), get_free_var_range(arg))), m_fn(fn), m_arg(arg) { @@ -160,9 +164,10 @@ bool operator==(binder_info const & i1, binder_info const & i2) { // Expr binders (Lambda, Pi) 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(), - t.has_param_univ() || b.has_param_univ(), + 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(), std::max(get_depth(t), get_depth(b)) + 1, std::max(get_free_var_range(t), dec(get_free_var_range(b)))), m_binder(n, t, i), @@ -178,7 +183,7 @@ void expr_binding::dealloc(buffer & todelete) { // Expr Sort expr_sort::expr_sort(level const & l): - expr_cell(expr_kind::Sort, ::lean::hash(l), has_meta(l), false, has_param(l)), + expr_cell(expr_kind::Sort, ::lean::hash(l), false, has_meta(l), false, has_param(l)), m_level(l) { } expr_sort::~expr_sort() {} @@ -229,7 +234,8 @@ static unsigned get_free_var_range(unsigned num, expr const * args) { expr_macro::expr_macro(macro_definition const & m, unsigned num, expr const * args): 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_metavar(); }), + std::any_of(args, args+num, [](expr const & e) { return e.has_expr_metavar(); }), + std::any_of(args, args+num, [](expr const & e) { return e.has_univ_metavar(); }), 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(); }), max_depth(num, args) + 1, diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 8c3669b01..11baadb16 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -52,7 +52,8 @@ protected: // Remark: we use atomic_uchar because these flags are computed lazily (i.e., after the expression is created) atomic_uchar m_flags; unsigned m_kind:8; - unsigned m_has_mv:1; // term contains metavariables + unsigned m_has_expr_mv:1; // term contains expression metavariables + unsigned m_has_univ_mv:1; // term contains universe metavariables unsigned m_has_local:1; // term contains local constants unsigned m_has_param_univ:1; // term constains parametric universe levels unsigned m_hash; // hash based on the structure of the expression (this is a good hash for structural equality) @@ -67,11 +68,12 @@ protected: static void dec_ref(expr & c, buffer & todelete); public: - expr_cell(expr_kind k, unsigned h, bool has_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); expr_kind kind() const { return static_cast(m_kind); } unsigned hash() const { return m_hash; } unsigned hash_alloc() const { return m_hash_alloc; } - bool has_metavar() const { return m_has_mv; } + bool has_expr_metavar() const { return m_has_expr_mv; } + bool has_univ_metavar() const { return m_has_univ_mv; } bool has_local() const { return m_has_local; } bool has_param_univ() const { return m_has_param_univ; } void set_tag(tag t); @@ -113,7 +115,9 @@ public: expr_kind kind() const { return m_ptr->kind(); } unsigned hash() const { return m_ptr ? m_ptr->hash() : 23; } unsigned hash_alloc() const { return m_ptr ? m_ptr->hash_alloc() : 23; } - bool has_metavar() const { return m_ptr->has_metavar(); } + bool has_expr_metavar() const { return m_ptr->has_expr_metavar(); } + bool has_univ_metavar() const { return m_ptr->has_univ_metavar(); } + bool has_metavar() const { return has_expr_metavar() || has_univ_metavar(); } bool has_local() const { return m_ptr->has_local(); } bool has_param_univ() const { return m_ptr->has_param_univ(); } @@ -251,7 +255,8 @@ protected: friend unsigned get_depth(expr const & e); friend unsigned get_free_var_range(expr const & e); public: - expr_composite(expr_kind k, unsigned h, bool has_mv, bool has_local, bool has_param_univ, unsigned d, unsigned fv_range); + expr_composite(expr_kind k, unsigned h, bool has_expr_mv, bool has_univ_mv, bool has_local, + bool has_param_univ, unsigned d, unsigned fv_range); }; /** \brief Applications */ @@ -573,6 +578,8 @@ inline binder_info const & local_info(expr const & e) { return to_local(e) inline bool is_constant(expr const & e, name const & n) { return is_constant(e) && const_name(e) == n; } inline bool has_metavar(expr const & e) { return e.has_metavar(); } +inline bool has_expr_metavar(expr const & e) { return e.has_expr_metavar(); } +inline bool has_univ_metavar(expr const & e) { return e.has_univ_metavar(); } inline bool has_local(expr const & e) { return e.has_local(); } inline bool has_param_univ(expr const & e) { return e.has_param_univ(); } unsigned get_depth(expr const & e);