From dcba76ba7e8991025e932e43c2bfdec3666c6a2d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 2 Aug 2016 14:45:04 -0700
Subject: [PATCH] feat(frontends/lean/parser): at parser::elaborate convert
 metavar_decl_ref's into regular metavars

---
 src/frontends/lean/parser.cpp | 32 +++++++++++++++++++++++++++++++-
 1 file changed, 31 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index f1d46b18c7..8708bb8953 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -965,13 +965,43 @@ public:
     local_context const & lctx() const { return m_lctx; }
 };
 
+static expr replace_with_simple_metavars(metavar_context & mctx, name_map<expr> & cache, expr const & e) {
+    if (!has_expr_metavar(e)) return e;
+    return replace(e, [&](expr const & e, unsigned) {
+            if (!is_metavar(e)) return none_expr();
+            if (auto r = cache.find(mlocal_name(e))) {
+                return some_expr(*r);
+            } else if (auto decl = mctx.get_metavar_decl(e)) {
+                expr new_type = replace_with_simple_metavars(mctx, cache, mctx.instantiate_mvars(decl->get_type()));
+                expr new_mvar = mk_metavar(mlocal_name(e), new_type);
+                cache.insert(mlocal_name(e), new_mvar);
+                return some_expr(new_mvar);
+            } else if (is_metavar_decl_ref(e)) {
+                throw exception("unexpected occurrence of internal elaboration metavariable");
+            }
+            return none_expr();
+        });
+}
+
+/** When the output of the elaborator may contain meta-variables, we convert the type_context level meta-variables
+    into regular kernel meta-variables. */
+static expr replace_with_simple_metavars(metavar_context & mctx, expr const & e) {
+    name_map<expr> cache;
+    return replace_with_simple_metavars(mctx, cache, e);
+}
+
 std::tuple<expr, level_param_names> parser::elaborate(metavar_context & mctx, expr const & e, bool check_unassigned) {
     local_context_adapter adapter;
     adapter.init(m_local_decls);
     expr tmp_e  = adapter.translate_to(e);
     std::tuple<expr, level_param_names> r =
         ::lean::elaborate(m_env, get_options(), mctx, adapter.lctx(), tmp_e, check_unassigned);
-    return std::make_tuple(adapter.translate_from(std::get<0>(r)), std::get<1>(r));
+    expr new_e = std::get<0>(r);
+    if (!check_unassigned) {
+        new_e = replace_with_simple_metavars(mctx, new_e);
+    }
+    new_e = adapter.translate_from(new_e);
+    return std::make_tuple(new_e, std::get<1>(r));
 }
 
 std::tuple<expr, level_param_names> parser::elaborate(expr const & e) {