diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 70cc61c79..a5682f3bb 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -29,19 +29,12 @@ unsigned hash_levels(levels const & ls) { return r; } -bool has_meta(levels const & ls) { - for (auto const & l : ls) { - if (has_meta(l)) - return true; - } - return false; -} - -expr_cell::expr_cell(expr_kind k, unsigned h, bool has_mv, bool has_local): +expr_cell::expr_cell(expr_kind k, unsigned h, bool has_mv, bool has_local, bool has_param_univ): m_kind(static_cast(k)), m_flags(0), m_has_mv(has_mv), m_has_local(has_local), + m_has_param_univ(has_param_univ), m_hash(h), m_rc(0) { // m_hash_alloc does not need to be a unique identifier. @@ -85,18 +78,18 @@ void expr_cell::set_is_arrow(bool flag) { // Expr variables expr_var::expr_var(unsigned idx): - expr_cell(expr_kind::Var, idx, false, false), + expr_cell(expr_kind::Var, idx, false, false, false), m_vidx(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), + expr_cell(expr_kind::Constant, ::lean::hash(n.hash(), hash_levels(ls)), 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()), + 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()), m_name(n), m_type(t) {} void expr_mlocal::dealloc(buffer & todelete) { @@ -105,8 +98,8 @@ void expr_mlocal::dealloc(buffer & todelete) { } // Composite expressions -expr_composite::expr_composite(expr_kind k, unsigned h, bool has_mv, bool has_local, unsigned d): - expr_cell(k, h, has_mv, has_local), +expr_composite::expr_composite(expr_kind k, unsigned h, bool has_mv, bool has_local, bool has_param_univ, unsigned d): + expr_cell(k, h, has_mv, has_local, has_param_univ), m_depth(d) {} // Expr dependent pairs @@ -114,6 +107,7 @@ expr_dep_pair::expr_dep_pair(expr const & f, expr const & s, expr const & t): expr_composite(expr_kind::Pair, ::lean::hash(f.hash(), s.hash()), f.has_metavar() || s.has_metavar() || t.has_metavar(), f.has_local() || s.has_local() || t.has_local(), + f.has_param_univ() || s.has_param_univ() || t.has_param_univ(), std::max(get_depth(f), get_depth(s))+1), m_first(f), m_second(s), m_type(t) { } @@ -126,7 +120,8 @@ void expr_dep_pair::dealloc(buffer & todelete) { // Expr pair projection expr_proj::expr_proj(bool f, expr const & e): - expr_composite(f ? expr_kind::Fst : expr_kind::Snd, ::lean::hash(17, e.hash()), e.has_metavar(), e.has_local(), get_depth(e)+1), + expr_composite(f ? expr_kind::Fst : expr_kind::Snd, ::lean::hash(17, e.hash()), e.has_metavar(), e.has_local(), e.has_param_univ(), + get_depth(e)+1), m_expr(e) {} void expr_proj::dealloc(buffer & todelete) { dec_ref(m_expr, todelete); @@ -136,8 +131,9 @@ void expr_proj::dealloc(buffer & todelete) { // 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_metavar() || arg.has_metavar(), + fn.has_local() || arg.has_local(), + fn.has_param_univ() || arg.has_param_univ(), std::max(get_depth(fn), get_depth(arg)) + 1), m_fn(fn), m_arg(arg) {} void expr_app::dealloc(buffer & todelete) { @@ -149,8 +145,9 @@ void expr_app::dealloc(buffer & todelete) { // Expr binders (Lambda, Pi and Sigma) expr_binder::expr_binder(expr_kind k, name const & n, expr const & t, expr const & b): expr_composite(k, ::lean::hash(t.hash(), b.hash()), - t.has_metavar() || b.has_metavar(), - t.has_local() || b.has_local(), + t.has_metavar() || b.has_metavar(), + t.has_local() || b.has_local(), + t.has_param_univ() || b.has_param_univ(), std::max(get_depth(t), get_depth(b)) + 1), m_name(n), m_domain(t), @@ -165,7 +162,7 @@ void expr_binder::dealloc(buffer & todelete) { // Expr Sort expr_sort::expr_sort(level const & l): - expr_cell(expr_kind::Sort, ::lean::hash(l), has_meta(l), false), + expr_cell(expr_kind::Sort, ::lean::hash(l), has_meta(l), false, has_param(l)), m_level(l) { } expr_sort::~expr_sort() {} @@ -173,8 +170,9 @@ expr_sort::~expr_sort() {} // Expr Let expr_let::expr_let(name const & n, expr const & t, expr const & v, expr const & b): expr_composite(expr_kind::Let, ::lean::hash(v.hash(), b.hash()), - t.has_metavar() || v.has_metavar() || b.has_metavar(), - t.has_local() || v.has_local() || b.has_local(), + t.has_metavar() || v.has_metavar() || b.has_metavar(), + t.has_local() || v.has_local() || b.has_local(), + t.has_param_univ() || v.has_param_univ() || b.has_param_univ(), std::max({get_depth(t), get_depth(v), get_depth(b)}) + 1), m_name(n), m_type(t), @@ -225,7 +223,7 @@ static expr read_macro(deserializer & d) { } expr_macro::expr_macro(macro * m): - expr_cell(expr_kind::Macro, m->hash(), false, false), + expr_cell(expr_kind::Macro, m->hash(), false, false, false), m_macro(m) { m_macro->inc_ref(); } diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 6688de052..acc811eca 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -53,8 +53,9 @@ protected: // 2-3 - term is an arrow (0 - not initialized, 1 - is arrow, 2 - is not arrow) // Remark: we use atomic_uchar because these flags are computed lazily (i.e., after the expression is created) atomic_uchar m_flags; - unsigned m_has_mv:1; // term contains metavariables - unsigned m_has_local:1; // term contains local constants + unsigned m_has_mv:1; // term contains 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) unsigned m_hash_alloc; // hash based on 'time' of allocation (this is a good hash for pointer-based equality) MK_LEAN_RC(); // Declare m_rc counter @@ -74,12 +75,13 @@ protected: friend class has_free_var_fn; static void dec_ref(expr & c, buffer & todelete); public: - expr_cell(expr_kind k, unsigned h, bool has_mv, bool has_local); + expr_cell(expr_kind k, unsigned h, bool has_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_local() const { return m_has_local; } + bool has_param_univ() const { return m_has_param_univ; } }; class macro; @@ -118,6 +120,7 @@ public: unsigned hash_alloc() const { return m_ptr ? m_ptr->hash_alloc() : 23; } bool has_metavar() const { return m_ptr->has_metavar(); } bool has_local() const { return m_ptr->has_local(); } + bool has_param_univ() const { return m_ptr->has_param_univ(); } expr_cell * raw() const { return m_ptr; } @@ -197,7 +200,7 @@ class expr_composite : public expr_cell { unsigned m_depth; friend unsigned get_depth(expr const & e); public: - expr_composite(expr_kind k, unsigned h, bool has_mv, bool has_local, unsigned d); + expr_composite(expr_kind k, unsigned h, bool has_mv, bool has_local, bool has_param_univ, unsigned d); }; /** \brief Applications */ @@ -518,6 +521,7 @@ inline expr const & mlocal_type(expr const & e) { return to_mlocal(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_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); // ======================================= diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index 733f0dd91..53071233f 100644 --- a/src/kernel/instantiate.cpp +++ b/src/kernel/instantiate.cpp @@ -108,7 +108,20 @@ expr beta_reduce(expr t) { } expr instantiate_params(expr const & e, param_names const & ps, levels const & ls) { - // TODO(Leo) - return e; + if (!has_param_univ(e)) + return e; + return replace(e, [&](expr const & e, unsigned) -> optional { + 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), + [&](level const & l) { return instantiate(l, ps, ls); }, + [](level const & l1, level const & l2) { return is_eqp(l1, l2); }))); + } else if (is_sort(e)) { + return some_expr(update_sort(e, instantiate(sort_level(e), ps, ls))); + } else { + return none_expr(); + } + }); } } diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index 25f829438..714940e34 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -404,6 +404,22 @@ level_cnstrs read_level_cnstrs(deserializer & d) { return read_list(d, read_level_cnstr); } +bool has_meta(levels const & ls) { + for (auto const & l : ls) { + if (has_meta(l)) + return true; + } + return false; +} + +bool has_param(levels const & ls) { + for (auto const & l : ls) { + if (has_param(l)) + return true; + } + return false; +} + bool has_param(level_cnstr const & c) { return has_param(c.first) || has_param(c.second); } diff --git a/src/kernel/level.h b/src/kernel/level.h index 917ea2403..30ca75276 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -144,6 +144,9 @@ bool is_trivial(level const & lhs, level const & rhs); typedef list levels; +bool has_meta(levels const & ls); +bool has_param(levels const & ls); + /** \brief Simpler version of the constraint class. We use in the definition of objects.