refactor(kernel): instantiate_params

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/expr.cpp

@@ -29,19 +29,12 @@ unsigned hash_levels(levels const & ls) {
     return r;
 }
 
-bool has_meta(levels const & ls) {
+expr_cell::expr_cell(expr_kind k, unsigned h, bool has_mv, bool has_local, bool has_param_univ):
-    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):
     m_kind(static_cast<unsigned>(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<expr_cell*> & todelete) {
@@ -105,8 +98,8 @@ void expr_mlocal::dealloc(buffer<expr_cell*> & todelete) {
 }
 
 // Composite expressions
-expr_composite::expr_composite(expr_kind k, unsigned h, bool has_mv, bool has_local, unsigned d):
+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),
+    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<expr_cell*> & 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<expr_cell*> & todelete) {
     dec_ref(m_expr, todelete);
@@ -136,8 +131,9 @@ void expr_proj::dealloc(buffer<expr_cell*> & 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_metavar()    || arg.has_metavar(),
-                   fn.has_local()   || arg.has_local(),
+                   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<expr_cell*> & todelete) {
@@ -149,8 +145,9 @@ void expr_app::dealloc(buffer<expr_cell*> & 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_metavar()    || b.has_metavar(),
-                   t.has_local() || b.has_local(),
+                   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<expr_cell*> & 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_metavar()    || v.has_metavar()    || b.has_metavar(),
-                   t.has_local() || v.has_local() || b.has_local(),
+                   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();
 }

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_mv:1;         // term contains metavariables
-    unsigned           m_has_local:1; // term contains local constants
+    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<expr_cell*> & 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<expr_kind>(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);
 // =======================================
 

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)
+    if (!has_param_univ(e))
-    return 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),
+                                                              [&](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();
+            }
+        });
 }
 }

src/kernel/level.cpp

@@ -404,6 +404,22 @@ level_cnstrs read_level_cnstrs(deserializer & d) {
     return read_list<level_cnstr>(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);
 }

src/kernel/level.h

@@ -144,6 +144,9 @@ bool is_trivial(level const & lhs, level const & rhs);
 
 typedef list<level> 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.