refactor(kernel): substitution

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

src/kernel/expr.cpp

@@ -371,6 +371,20 @@ expr update_mlocal(expr const & e, expr const & new_type) {
         return e;
 }
 
+expr update_sort(expr const & e, level const & new_level) {
+    if (!is_eqp(sort_level(e), new_level))
+        return mk_sort(new_level);
+    else
+        return e;
+}
+
+expr update_constant(expr const & e, levels const & new_levels) {
+    if (!is_eqp(const_level_params(e), new_levels))
+        return mk_constant(const_name(e), new_levels);
+    else
+        return e;
+}
+
 bool is_atomic(expr const & e) {
     switch (e.kind()) {
     case expr_kind::Constant: case expr_kind::Sort:

src/kernel/expr.h

@@ -570,6 +570,8 @@ expr update_pair(expr const & e, expr const & new_first, expr const & new_second
 expr update_binder(expr const & e, expr const & new_domain, expr const & new_body);
 expr update_let(expr const & e, expr const & new_type, expr const & new_val, expr const & new_body);
 expr update_mlocal(expr const & e, expr const & new_type);
+expr update_sort(expr const & e, level const & new_level);
+expr update_constant(expr const & e, levels const & new_levels);
 // =======================================
 
 // =======================================

src/kernel/instantiate.cpp

@@ -109,4 +109,9 @@ expr beta_reduce(expr t) {
             t = new_t;
     }
 }
+
+expr instantiate_params(expr const & e, param_names const & ps, levels const & ls) {
+    // TODO(Leo)
+    return e;
+}
 }

src/kernel/instantiate.h

@@ -30,4 +30,11 @@ expr apply_beta(expr f, unsigned num_args, expr const * args);
 bool is_head_beta(expr const & t);
 expr head_beta_reduce(expr const & t);
 expr beta_reduce(expr t);
+
+/**
+    \brief Instantiate the universe level parameters \c ps occurring in \c e with the levels \c ls.
+
+    \pre length(ps) == length(ls)
+*/
+expr instantiate_params(expr const & e, param_names const & ps, levels const & ls);
 }

src/kernel/level.cpp

@@ -428,19 +428,19 @@ bool has_meta(level_cnstrs const & cs) {
     return false;
 }
 
-static optional<name> get_undef_param(level const & l, list<name> const & param_names) {
+static optional<name> get_undef_param(level const & l, param_names const & ps) {
     if (!has_meta(l))
         return optional<name>();
     switch (l.kind()) {
     case level_kind::Succ:
-        return get_undef_param(succ_of(l), param_names);
+        return get_undef_param(succ_of(l), ps);
     case level_kind::Max: case level_kind::IMax:
-        if (auto it = get_undef_param(to_max_core(l).m_lhs, param_names))
+        if (auto it = get_undef_param(to_max_core(l).m_lhs, ps))
             return it;
         else
-            return get_undef_param(to_max_core(l).m_rhs, param_names);
+            return get_undef_param(to_max_core(l).m_rhs, ps);
     case level_kind::Param:
-        if (std::find(param_names.begin(), param_names.end(), param_id(l)) == param_names.end())
+        if (std::find(ps.begin(), ps.end(), param_id(l)) == ps.end())
             return optional<name>(param_id(l));
         else
             return optional<name>();
@@ -450,16 +450,69 @@ static optional<name> get_undef_param(level const & l, list<name> const & param_
     lean_unreachable(); // LCOV_EXCL_LINE
 }
 
-optional<name> get_undef_param(level_cnstrs const & cs, list<name> const & param_names) {
+optional<name> get_undef_param(level_cnstrs const & cs, param_names const & ps) {
     for (auto const & c : cs) {
-        if (auto it = get_undef_param(c.first, param_names))
+        if (auto it = get_undef_param(c.first, ps))
             return it;
-        if (auto it = get_undef_param(c.second, param_names))
+        if (auto it = get_undef_param(c.second, ps))
             return it;
     }
     return optional<name>();
 }
 
+level update_succ(level const & l, level const & new_arg) {
+    if (is_eqp(succ_of(l), new_arg))
+        return l;
+    else
+        return mk_succ(new_arg);
+}
+
+level update_max(level const & l, level const & new_lhs, level const & new_rhs) {
+    if (is_eqp(to_max_core(l).m_lhs, new_lhs) && is_eqp(to_max_core(l).m_rhs, new_rhs))
+        return l;
+    else if (is_max(l))
+        return mk_max(new_lhs, new_rhs);
+    else
+        return mk_imax(new_lhs, new_rhs);
+}
+
+level replace_level_fn::apply(level const & l) {
+    optional<level> r = m_f(l);
+    if (r)
+        return *r;
+    switch (l.kind()) {
+    case level_kind::Succ:
+        return update_succ(l, apply(succ_of(l)));
+    case level_kind::Max: case level_kind::IMax:
+        return update_max(l, apply(to_max_core(l).m_lhs), apply(to_max_core(l).m_rhs));
+    case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
+        return l;
+    }
+    lean_unreachable(); // LCOV_EXCL_LINE
+}
+
+level instantiate(level const & l, param_names const & ps, levels const & ls) {
+    lean_assert(length(ps) == length(ls));
+    return replace(l, [=](level const & l) {
+            if (!has_param(l)) {
+                return some_level(l);
+            } else if (is_param(l)) {
+                name const & id = param_id(l);
+                list<name> const *it1 = &ps;
+                list<level> const * it2 = &ls;
+                while (!is_nil(*it1)) {
+                    if (head(*it1) == id)
+                        return some_level(head(*it2));
+                    it1 = &tail(*it1);
+                    it2 = &tail(*it2);
+                }
+                return some_level(l);
+            } else {
+                return none_level();
+            }
+        });
+}
+
 static void print(std::ostream & out, level l);
 
 static void print_child(std::ostream & out, level const & l) {

src/kernel/level.h

@@ -44,6 +44,7 @@ class level {
     friend class environment;
     level_cell * m_ptr;
     friend level_cell const & to_cell(level const & l);
+    friend class optional<level>;
 public:
     /** \brief Universe zero */
     level();
@@ -66,6 +67,15 @@ public:
     struct ptr_eq { bool operator()(level const & n1, level const & n2) const { return n1.m_ptr == n2.m_ptr; } };
 };
 
+bool operator==(level const & l1, level const & l2);
+inline bool operator!=(level const & l1, level const & l2) { return !operator==(l1, l2); }
+
+SPECIALIZE_OPTIONAL_FOR_SMART_PTR(level)
+
+inline optional<level> none_level() { return optional<level>(); }
+inline optional<level> some_level(level const & e) { return optional<level>(e); }
+inline optional<level> some_level(level && e) { return optional<level>(std::forward<level>(e)); }
+
 level const & mk_level_zero();
 level const & mk_level_one();
 level mk_max(level const & l1, level const & l2);
@@ -74,12 +84,7 @@ level mk_succ(level const & l);
 level mk_param_univ(name const & n);
 level mk_meta_univ(name const & n);
 
-bool operator==(level const & l1, level const & l2);
-inline bool operator!=(level const & l1, level const & l2) { return !operator==(l1, l2); }
-
-/**
-   \brief An arbitrary (monotonic) total order on universe level terms.
-*/
+/** \brief An arbitrary (monotonic) total order on universe level terms. */
 bool is_lt(level const & l1, level const & l2);
 
 inline unsigned hash(level const & l) { return l.hash(); }
@@ -113,6 +118,21 @@ bool has_meta(level const & l);
 /** \brief Return true iff \c l contains parameters */
 bool has_param(level const & l);
 
+/**
+   \brief Return a new level expression based on <tt>l == succ(arg)</tt>, where \c arg is replaced with
+   \c new_arg.
+
+   \pre is_succ(l)
+*/
+level update_succ(level const & l, level const & new_arg);
+/**
+   \brief Return a new level expression based on <tt>l == max(lhs, rhs)</tt>, where \c lhs is replaced with
+   \c new_lhs and \c rhs is replaced with \c new_rhs.
+
+   \pre is_max(l) || is_imax(l)
+*/
+level update_max(level const & l, level const & new_lhs, level const & new_rhs);
+
 /**
    \brief Return true if lhs <= rhs is a trivial constraint.
    That is, it is a constraint that is always valid, and can be discarded.
@@ -136,15 +156,36 @@ bool has_param(level_cnstrs const & cs);
 bool has_meta(level_cnstr const & c);
 bool has_meta(level_cnstrs const & cs);
 
+typedef list<name> param_names;
+
 /**
    \brief If \c cs contains a parameter that is not in \c param_names, then return it.
    Otherwise, return none.
 */
-optional<name> get_undef_param(level_cnstrs const & cs, list<name> const & param_names);
+optional<name> get_undef_param(level_cnstrs const & cs, param_names const & ps);
 
 /**
-   \brief Printer for debugging purposes
+   \brief Functional for applying <tt>F</tt> to the level expressions.
 */
+class replace_level_fn {
+    std::function<optional<level>(level const &)>  m_f;
+    level apply(level const & l);
+public:
+    template<typename F> replace_level_fn(F const & f):m_f(f) {}
+    level operator()(level const & l) { return apply(l); }
+};
+
+template<typename F> level replace(level const & l, F const & f) {
+    return replace_level_fn(f)(l);
+}
+
+/**
+    \brief Instantiate the universe level parameters \c ps occurring in \c l with the levels \c ls.
+    \pre length(ps) == length(ls)
+*/
+level instantiate(level const & l, param_names const & ps, levels const & ls);
+
+/** \brief Printer for debugging purposes */
 std::ostream & operator<<(std::ostream & out, level const & l);
 
 /**
@@ -168,9 +209,7 @@ format pp(level l, bool unicode, unsigned indent);
 /** \brief Pretty print the given level expression using the given configuration options. */
 format pp(level const & l, options const & opts = options());
 
-/**
-   \brief Auxiliary class used to manage universe constraints.
-*/
+/** \brief Auxiliary class used to manage universe constraints. */
 class universe_context {
     struct imp;
     std::unique_ptr<imp> m_ptr;

src/kernel/metavar.cpp

@@ -11,43 +11,106 @@ Author: Leonardo de Moura
 #include "kernel/justification.h"
 #include "kernel/instantiate.h"
 #include "kernel/find_fn.h"
+#include "kernel/level.h"
 
 namespace lean {
-bool substitution::is_assigned(name const & m) const {
-    return m_subst.contains(m);
+bool substitution::is_expr_assigned(name const & m) const {
+    return m_expr_subst.contains(m);
 }
 
-optional<std::pair<expr, justification>> substitution::get_assignment(name const & m) const {
-    auto it = m_subst.find(m);
+optional<std::pair<expr, justification>> substitution::get_expr_assignment(name const & m) const {
+    auto it = m_expr_subst.find(m);
     if (it)
         return optional<std::pair<expr, justification>>(*it);
     else
         return optional<std::pair<expr, justification>>();
 }
 
+bool substitution::is_level_assigned(name const & m) const {
+    return m_level_subst.contains(m);
+}
+
+optional<std::pair<level, justification>> substitution::get_level_assignment(name const & m) const {
+    auto it = m_level_subst.find(m);
+    if (it)
+        return opt_level_jst(*it);
+    else
+        return opt_level_jst();
+}
+
 optional<expr> substitution::get_expr(name const & m) const {
-    auto it = m_subst.find(m);
+    auto it = m_expr_subst.find(m);
     if (it)
         return some_expr(it->first);
     else
         return none_expr();
 }
 
+optional<level> substitution::get_level(name const & m) const {
+    auto it = m_level_subst.find(m);
+    if (it)
+        return some_level(it->first);
+    else
+        return none_level();
+}
+
 void substitution::assign(name const & m, expr const & t, justification const & j) {
     lean_assert(closed(t));
-    m_subst.insert(m, mk_pair(t, j));
+    m_expr_subst.insert(m, mk_pair(t, j));
 }
 
 void substitution::assign(name const & m, expr const & t) {
     assign(m, t, justification());
 }
 
+void substitution::assign(name const & m, level const & l, justification const & j) {
+    m_level_subst.insert(m, mk_pair(l, j));
+}
+
+void substitution::assign(name const & m, level const & l) {
+    assign(m, l, justification());
+}
+
 void substitution::for_each(std::function<void(name const & n, expr const & e, justification const & j)> const & fn) const {
-    m_subst.for_each([=](name const & n, std::pair<expr, justification> const & a) {
+    m_expr_subst.for_each([=](name const & n, std::pair<expr, justification> const & a) {
             fn(n, a.first, a.second);
         });
 }
 
+void substitution::for_each(std::function<void(name const & n, level const & e, justification const & j)> const & fn) const {
+    m_level_subst.for_each([=](name const & n, std::pair<level, justification> const & a) {
+            fn(n, a.first, a.second);
+        });
+}
+
+std::pair<level, justification> instantiate_metavars(level const & l, substitution & s, bool use_jst, bool updt) {
+    if (!has_param(l))
+        return mk_pair(l, justification());
+    justification j;
+    auto save_jst = [&](justification const & j2) { j = mk_composite1(j, j2); };
+    level r = replace(l, [&](level const & l) {
+            if (!has_meta(l)) {
+                return some_level(l);
+            } else if (is_meta(l)) {
+                auto p1 = s.get_assignment(l);
+                if (p1) {
+                    auto p2 = instantiate_metavars(p1->first, s, use_jst, updt);
+                    if (use_jst) {
+                        justification new_jst = mk_composite1(p1->second, p2.second);
+                        if (updt)
+                            s.assign(l, p2.first, new_jst);
+                        save_jst(new_jst);
+                    } else if (updt) {
+                        s.assign(l, p2.first);
+                    }
+                    return some_level(p2.first);
+                }
+            }
+            return none_level();
+        });
+    return mk_pair(r, j);
+}
+
 class instantiate_metavars_fn : public replace_visitor {
 protected:
     substitution & m_subst;
@@ -57,9 +120,28 @@ protected:
 
     void save_jst(justification const & j) { m_jst = mk_composite1(m_jst, j); }
 
+    level visit_level(level const & l) {
+        auto p1 = instantiate_metavars(l, m_subst, m_use_jst, m_update);
+        if (m_use_jst)
+            save_jst(p1.second);
+        return p1.first;
+    }
+
+    levels visit_levels(levels const & ls) {
+        return map_reuse(ls, [&](level const & l) { return visit_level(l); }, [](level const & l1, level const & l2) { return is_eqp(l1, l2); });
+    }
+
+    virtual expr visit_sort(expr const & s, context const &) {
+        return update_sort(s, visit_level(sort_level(s)));
+    }
+
+    virtual expr visit_constant(expr const & c, context const &) {
+        return update_constant(c, visit_levels(const_level_params(c)));
+    }
+
     virtual expr visit_meta(expr const & m, context const &) {
         name const & m_name = mlocal_name(m);
-        auto p1 = m_subst.get_assignment(m_name);
+        auto p1 = m_subst.get_expr_assignment(m_name);
         if (p1) {
             if (!has_metavar(p1->first)) {
                 if (m_use_jst)
@@ -99,7 +181,7 @@ protected:
             it = &app_fn(*it);
         }
         expr const & f = *it;
-        if (is_metavar(f) && m_subst.is_assigned(mlocal_name(f))) {
+        if (is_metavar(f) && m_subst.is_expr_assigned(mlocal_name(f))) {
             expr new_f = visit_meta(f, ctx);
             return apply_beta(new_f, args.size(), args.data());
         } else {
@@ -108,6 +190,14 @@ protected:
         }
     }
 
+    virtual expr visit(expr const & e, context const & ctx) {
+        if (!has_metavar(e)) {
+            return e;
+        } else {
+            return replace_visitor::visit(e, ctx);
+        }
+    }
+
 public:
     instantiate_metavars_fn(substitution & s, bool use_jst, bool updt):
         m_subst(s), m_use_jst(use_jst), m_update(updt) {}
@@ -134,7 +224,7 @@ expr substitution::d_instantiate_metavars_wo_jst(expr const & e) {
     return instantiate_metavars_fn(*this, false, true)(e);
 }
 
-bool substitution::occurs(name const & m, expr const & e) const {
+bool substitution::occurs_expr(name const & m, expr const & e) const {
     if (!has_metavar(e))
         return false;
     auto it = find(e, [&](expr const & e, unsigned) {
@@ -142,7 +232,7 @@ bool substitution::occurs(name const & m, expr const & e) const {
                 if (mlocal_name(e) == m)
                     return true;
                 auto s = get_expr(e);
-                return s && occurs(m, *s);
+                return s && occurs_expr(m, *s);
             } else {
                 return false;
             }

src/kernel/metavar.h

@@ -13,23 +13,43 @@ Author: Leonardo de Moura
 
 namespace lean {
 class substitution {
-    rb_map<name, std::pair<expr, justification>, name_quick_cmp> m_subst;
+    rb_map<name, std::pair<expr, justification>, name_quick_cmp>  m_expr_subst;
+    rb_map<name, std::pair<level, justification>, name_quick_cmp> m_level_subst;
 public:
-    typedef optional<std::pair<expr, justification>> opt_expr_jst;
-    bool is_assigned(name const & m) const;
-    opt_expr_jst get_assignment(name const & m) const;
+    typedef optional<std::pair<expr,  justification>> opt_expr_jst;
+    typedef optional<std::pair<level, justification>> opt_level_jst;
+
+    bool is_expr_assigned(name const & m) const;
+    opt_expr_jst get_expr_assignment(name const & m) const;
+
+    bool is_level_assigned(name const & m) const;
+    opt_level_jst get_level_assignment(name const & m) const;
+
     optional<expr> get_expr(name const & m) const;
+    optional<level> get_level(name const & m) const;
+
     void assign(name const & m, expr const & t, justification const & j);
     void assign(name const & m, expr const & t);
-    void for_each(std::function<void(name const & n, expr const & e, justification const & j)> const & fn) const;
 
-    bool is_assigned(expr const & m) const { lean_assert(is_metavar(m)); return is_assigned(mlocal_name(m)); }
-    opt_expr_jst get_assignment(expr const & m) const { lean_assert(is_metavar(m)); return get_assignment(mlocal_name(m)); }
+    void assign(name const & m, level const & t, justification const & j);
+    void assign(name const & m, level const & t);
+
+    void for_each(std::function<void(name const & n, expr const & e, justification const & j)> const & fn) const;
+    void for_each(std::function<void(name const & n, level const & e, justification const & j)> const & fn) const;
+
+    bool is_assigned(expr const & m) const { lean_assert(is_metavar(m)); return is_expr_assigned(mlocal_name(m)); }
+    opt_expr_jst get_assignment(expr const & m) const { lean_assert(is_metavar(m)); return get_expr_assignment(mlocal_name(m)); }
     optional<expr> get_expr(expr const & m) const { lean_assert(is_metavar(m)); return get_expr(mlocal_name(m)); }
     void assign(expr const & m, expr const & t, justification const & j) { lean_assert(is_metavar(m)); assign(mlocal_name(m), t, j); }
     void assign(expr const & m, expr const & t) { lean_assert(is_metavar(m)); return assign(mlocal_name(m), t); }
 
-    /** \brief Instantiate metavariables in \c e assigned in the substitution \c s. */
+    bool is_assigned(level const & m) const { lean_assert(is_meta(m)); return is_level_assigned(meta_id(m)); }
+    opt_level_jst get_assignment(level const & m) const { lean_assert(is_meta(m)); return get_level_assignment(meta_id(m)); }
+    optional<level> get_level(level const & m) const { lean_assert(is_meta(m)); return get_level(meta_id(m)); }
+    void assign(level const & m, level const & l, justification const & j) { lean_assert(is_meta(m)); assign(meta_id(m), l, j); }
+    void assign(level const & m, level const & l) { lean_assert(is_meta(m)); return assign(meta_id(m), l); }
+
+    /** \brief Instantiate metavariables in \c e assigned in this substitution. */
     std::pair<expr, justification> instantiate_metavars(expr const & e) const;
 
     /**
@@ -47,10 +67,12 @@ public:
 
     expr d_instantiate_metavars_wo_jst(expr const & e);
 
-    /**
-       \brief Return true iff \c m occurrs (directly or indirectly) in \c e.
-    */
-    bool occurs(name const & m, expr const & e) const;
-    bool occurs(expr const & m, expr const & e) const { lean_assert(is_metavar(m)); return occurs(mlocal_name(m), e); }
+    /** \brief Return true iff the metavariable \c m occurrs (directly or indirectly) in \c e. */
+    bool occurs_expr(name const & m, expr const & e) const;
+    /** \brief Return true iff the meta universe parameter \c m occurrs (directly or indirectly) in \c e. */
+    bool occurs_level(name const & m, expr const & e) const;
+
+    bool occurs(expr const & m, expr const & e) const { lean_assert(is_metavar(m)); return occurs_expr(mlocal_name(m), e); }
+    bool occurs(level const & m, expr const & e) const { lean_assert(is_meta(m)); return occurs_expr(meta_id(m), e); }
 };
 }

src/kernel/normalizer.cpp

@@ -146,6 +146,7 @@ class normalizer::imp {
         case expr_kind::Constant: {
             optional<object> obj = env()->find_object(const_name(a));
             if (should_unfold(obj)) {
+                // TODO(Leo): instantiate level parameters
                 freset<cache> reset(m_cache);
                 r = normalize(obj->get_value(), value_stack(), 0);
             } else {

src/kernel/object.h

@@ -20,8 +20,6 @@ class io_state;
 class object;
 enum class object_kind { Definition, Postulate, Neutral };
 
-typedef list<name> param_names;
-
 class object_cell {
 protected:
     friend class object;