feat(library/idx_metavar): add helper function for converting metavariables occurring in an expression into temporary metavariables

src/library/idx_metavar.cpp

@@ -7,6 +7,8 @@ Author: Leonardo de Moura
 #include "util/interrupt.h"
 #include "kernel/for_each_fn.h"
 #include "library/idx_metavar.h"
+#include "library/metavar_context.h"
+#include "library/replace_visitor.h"
 
 #ifndef LEAN_INSTANTIATE_METAIDX_CACHE_CAPACITY
 #define LEAN_INSTANTIATE_METAIDX_CACHE_CAPACITY 1024*8
@@ -98,4 +100,66 @@ bool has_idx_expr_metavar(expr const & e) {
         });
     return found;
 }
+
+struct to_idx_metavars_fn : public replace_visitor {
+    metavar_context const & m_mctx;
+    buffer<level> &         m_new_us;
+    buffer<expr> &          m_new_ms;
+    name_map<level>         m_lvl_cache;
+
+    to_idx_metavars_fn(metavar_context const & mctx, buffer<level> & new_us, buffer<expr> & new_ms):
+        m_mctx(mctx), m_new_us(new_us), m_new_ms(new_ms) {}
+
+    level visit(level const & l) {
+        if (!has_meta(l)) return l;
+        return replace(l, [&](level const & l) {
+                if (is_meta(l) && !is_idx_metauniv(l)) {
+                    if (auto it = m_lvl_cache.find(meta_id(l)))
+                        return some_level(*it);
+                    level new_l = mk_idx_metauniv(m_new_us.size());
+                    m_lvl_cache.insert(meta_id(l), new_l);
+                    m_new_us.push_back(new_l);
+                    return some_level(new_l);
+                }
+                return none_level();
+            });
+    }
+
+    levels visit(levels const & ls) {
+        return map_reuse(ls, [&](level const & l) { return visit(l); });
+    }
+
+    virtual expr visit_meta(expr const & m) override {
+        if (is_idx_metavar(m)) {
+            return m;
+        } else if (auto decl = m_mctx.find_metavar_decl(m)) {
+            expr new_type = visit(decl->get_type());
+            unsigned i    = m_new_ms.size();
+            expr new_m    = mk_idx_metavar(i, new_type);
+            m_new_ms.push_back(new_m);
+            return new_m;
+        } else {
+            throw exception("unexpected occurrence of metavariable");
+        }
+    }
+
+    virtual expr visit_constant(expr const & e) override {
+        return update_constant(e, visit(const_levels(e)));
+    }
+
+    virtual expr visit_sort(expr const & e) override {
+        return update_sort(e, visit(sort_level(e)));
+    }
+
+    virtual expr visit(expr const & e) override {
+        if (!has_metavar(e)) return e;
+        return replace_visitor::visit(e);
+    }
+};
+
+expr to_idx_metavars(metavar_context const & mctx, expr const & e, buffer<level> & new_us, buffer<expr> & new_ms) {
+    if (!has_metavar(e))
+        return e;
+    return to_idx_metavars_fn(mctx, new_us, new_ms)(e);
+}
 }

src/library/idx_metavar.h

@@ -32,6 +32,12 @@ bool has_idx_metavar(expr const & e);
 bool has_idx_expr_metavar(expr const & e);
 bool has_idx_metauniv(level const & l);
 
+class metavar_context;
+
+/** \brief Convert metavariables occurring in \c e into indexed/temporary metavariables.
+    New metavariables are added to new_us and new_ms. */
+expr to_idx_metavars(metavar_context const & mctx, expr const & e, buffer<level> & new_us, buffer<expr> & new_ms);
+
 void initialize_idx_metavar();
 void finalize_idx_metavar();
 }