refactor(frontends/lean): replace collect_metavars with metavar_closure helper class

src/frontends/lean/elaborator.cpp

@@ -28,6 +28,7 @@ Author: Leonardo de Moura
 #include "library/locals.h"
 #include "library/let.h"
 #include "library/deep_copy.h"
+#include "library/metavar_closure.h"
 #include "library/typed_expr.h"
 #include "library/tactic/tactic.h"
 #include "library/tactic/expr_to_tactic.h"
@@ -870,14 +871,11 @@ public:
 
     expr solve_unassigned_mvars(substitution & subst, expr e, name_set & visited) {
         e = subst.instantiate(e);
-        buffer<expr> mvars;
-        collect_metavars(e, mvars);
-        if (mvars.empty())
-            return e;
-        for (auto mvar : mvars) {
-            check_interrupted();
-            solve_unassigned_mvar(subst, mvar, visited);
-        }
+        metavar_closure mvars(e);
+        mvars.for_each_expr_mvar([&](expr const & mvar) {
+                check_interrupted();
+                solve_unassigned_mvar(subst, mvar, visited);
+            });
         return subst.instantiate(e);
     }
 

src/frontends/lean/placeholder_elaborator.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "library/unifier.h"
 #include "library/opaque_hints.h"
+#include "library/metavar_closure.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/class.h"
 #include "frontends/lean/tactic_hint.h"
@@ -76,8 +77,6 @@ struct placeholder_elaborator : public choice_iterator {
     list<tactic_hint_entry> m_tactics;
     // result produce by last executed tactic.
     proof_state_seq         m_tactic_result;
-    // metavariables that occur in m_meta_type, the tactics may instantiate some of them
-    buffer<expr>            m_mvars_in_meta_type;
     justification           m_jst;
 
     placeholder_elaborator(std::shared_ptr<placeholder_context> const & C,
@@ -90,7 +89,6 @@ struct placeholder_elaborator : public choice_iterator {
         m_local_instances(local_insts), m_instances(instances),
         m_tactics(tacs),
         m_jst(j) {
-        collect_metavars(meta_type, m_mvars_in_meta_type);
     }
 
     constraints mk_constraints(constraint const & c, buffer<constraint> const & cs) {
@@ -163,13 +161,11 @@ struct placeholder_elaborator : public choice_iterator {
             if (!empty(next->first.get_goals()))
                 continue; // has unsolved goals
             substitution subst = next->first.get_subst();
-            buffer<constraint> cs;
             expr const & mvar = get_app_fn(m_meta);
             bool relax        = m_C->m_relax;
-            cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst, relax));
-            for (auto const & mvar : m_mvars_in_meta_type)
-                cs.push_back(mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst, relax));
-            return optional<constraints>(to_list(cs.begin(), cs.end()));
+            constraints cs    = metavar_closure(m_meta_type).mk_constraints(subst, m_jst, relax);
+            constraint  c     = mk_eq_cnstr(mvar, subst.instantiate(mvar), m_jst, relax);
+            return some(cons(c, cs));
         }
         return optional<constraints>();
     }

src/frontends/lean/util.cpp

@@ -226,14 +226,4 @@ justification mk_failed_to_synthesize_jst(environment const & env, expr const &
             return format("failed to synthesize placeholder") + line() + ps.pp(fmt);
         });
 }
-
-void collect_metavars(expr const & e, buffer<expr> & mvars) {
-    for_each(e, [&](expr const & e, unsigned) {
-            if (is_metavar(e)) {
-                mvars.push_back(e);
-                return false; /* do not visit its type */
-            }
-            return has_metavar(e);
-        });
-}
 }

src/frontends/lean/util.h

@@ -49,8 +49,4 @@ expr instantiate_meta(expr const & meta, substitution & subst);
 /** \brief Return a 'failed to synthesize placholder' justification for the given
     metavariable application \c m of the form (?m l_1 ... l_k) */
 justification mk_failed_to_synthesize_jst(environment const & env, expr const & m);
-
-/** \brief Copy the metavariables occurring in \c e to \c mvars,
-    this procedure ignores metavariables occurring in the type of metavariables. */
-void collect_metavars(expr const & e, buffer<expr> & mvars);
 }

src/kernel/metavar.h

@@ -55,6 +55,7 @@ public:
     void assign(level const & m, level const & t) { assign(m, t, justification ()); }
 
     pair<level, justification> instantiate_metavars(level const & l) { return instantiate_metavars(l, true); }
+    level instantiate(level const & l) { return instantiate_metavars(l, false).first; }
 
     /** \brief Instantiate metavariables occurring in \c e, by default this method does not visit the types of local constants.
         For substituting the metavariables occurring in local constants, use instantiate_metavars_all.

src/library/CMakeLists.txt

@@ -9,6 +9,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   explicit.cpp num.cpp string.cpp opaque_hints.cpp head_map.cpp
   match.cpp definition_cache.cpp declaration_index.cpp
   print.cpp annotation.cpp typed_expr.cpp let.cpp type_util.cpp
-  protected.cpp)
+  protected.cpp metavar_closure.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/metavar_closure.cpp

@@ -0,0 +1,64 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/for_each_fn.h"
+#include "library/metavar_closure.h"
+
+namespace lean {
+void metavar_closure::add(level const & l) {
+    for_each(l, [&](level const & l) {
+            if (is_meta(l)) {
+                m_lvl_mvars.insert(l);
+                return false;
+            } else {
+                return has_meta(l);
+            }
+        });
+}
+
+void metavar_closure::add(expr const & e) {
+    for_each(e, [&](expr const & e, unsigned) {
+            if (is_metavar(e)) {
+                m_expr_mvars.insert(e);
+                return false; /* do not visit its type */
+            } else if (is_sort(e)) {
+                add(sort_level(e));
+                return false;
+            } else if (is_constant(e)) {
+                for (level const & l : const_levels(e))
+                    add(l);
+                return false;
+            } else {
+                return has_metavar(e);
+            }
+        });
+}
+
+void metavar_closure::for_each_expr_mvar(std::function<void(expr const &)> const & fn) const {
+    m_expr_mvars.for_each(fn);
+}
+
+void metavar_closure::for_each_level_mvar(std::function<void(level const &)> const & fn) const {
+    m_lvl_mvars.for_each(fn);
+}
+
+void metavar_closure::mk_constraints(substitution s, justification const & j, bool relax, buffer<constraint> & r) const {
+    m_expr_mvars.for_each([&](expr const & m) {
+            if (s.is_expr_assigned(mlocal_name(m)))
+                r.push_back(mk_eq_cnstr(m, s.instantiate(m), j, relax));
+        });
+    m_lvl_mvars.for_each([&](level const & m) {
+            if (s.is_level_assigned(meta_id(m)))
+                r.push_back(mk_level_eq_cnstr(m, s.instantiate(m), j));
+        });
+}
+
+constraints metavar_closure::mk_constraints(substitution s, justification const & j, bool relax) const {
+    buffer<constraint> cs;
+    mk_constraints(s, j, relax, cs);
+    return to_list(cs.begin(), cs.end());
+}
+}

src/library/metavar_closure.h

@@ -0,0 +1,39 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/rb_tree.h"
+#include "kernel/metavar.h"
+#include "library/expr_lt.h"
+
+namespace lean {
+/** \brief Helper object for collecting metavariables occurring in expressions.
+    It also provides a method that given a substitution \c s, produces a constraint
+           ?m =?= s(?m)
+    for each collected metavariable ?m that is assigned in \c s.
+
+    \remark Metavariables occuring in the type of other metavariables are ignored.
+*/
+class metavar_closure {
+    rb_tree<expr, expr_quick_cmp>   m_expr_mvars;
+    rb_tree<level, level_quick_cmp> m_lvl_mvars;
+ public:
+    metavar_closure() {}
+    metavar_closure(expr const & e) { add(e); }
+    /** \brief Collect metavariables occurring in \c e */
+    void add(expr const & e);
+    void add(level const & l);
+    /** \brief Execute \c fn for each collected metavariable */
+    void for_each_expr_mvar(std::function<void(expr const &)> const & fn) const;
+    void for_each_level_mvar(std::function<void(level const &)> const & fn) const;
+    /** \brief For each collected metavariable ?m, store in \c r constraints of the form ?m =?= s(?m)
+        if ?m is assigned by \c s. The constraints are justified by \c j and \c relax
+        \see mk_eq_cnstr
+    */
+    void mk_constraints(substitution s, justification const & j, bool relax, buffer<constraint> & r) const;
+    constraints mk_constraints(substitution s, justification const & j, bool relax) const;
+};
+}