From 195429611bad30911f6db69a17a7a7b8454f60dd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 14 Jul 2014 04:25:53 +0100
Subject: [PATCH] refactor(frontends/lean/builtin_cmds): cleanup 'check'
 command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/builtin_cmds.cpp | 17 ++++-------------
 src/frontends/lean/util.cpp         | 17 +++++++++++++++++
 src/frontends/lean/util.h           |  4 ++++
 3 files changed, 25 insertions(+), 13 deletions(-)

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 5434fd45b..8aa0f480d 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -82,24 +82,15 @@ environment end_scoped_cmd(parser & p) {
 
 environment check_cmd(parser & p) {
     expr e   = p.parse_expr();
-    buffer<expr> section_ps;
-    expr_struct_set locals;
-    collect_locals(e, locals);
-    sort_section_params(locals, p, section_ps);
-    e = p.lambda_abstract(section_ps, e);
+    buffer<expr> locals;
+    e = abstract_locals(e, p, locals);
     level_param_names ls = to_level_param_names(collect_univ_params(e));
     level_param_names new_ls;
     std::tie(e, new_ls) = p.elaborate_relaxed(e);
     auto tc = mk_type_checker_with_hints(p.env(), p.mk_ngen());
     expr type = tc->check(e, append(ls, new_ls));
-    // consume sections_ps introduced with mk_section_params
-    for (unsigned i = 0; i < section_ps.size(); i++) {
-        lean_assert(is_lambda(e));
-        lean_assert(is_pi(type));
-        expr local = section_ps[i];
-        e    = instantiate(binding_body(e), local);
-        type = instantiate(binding_body(type), local);
-    }
+    e    = instantiate_locals(e, locals);
+    type = instantiate_locals(type, locals);
     auto reg              = p.regular_stream();
     formatter const & fmt = reg.get_formatter();
     options opts          = p.ios().get_options();
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index f7bae2324..8433e7302 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -6,6 +6,8 @@ Author: Leonardo de Moura
 */
 #include <algorithm>
 #include "util/sstream.h"
+#include "kernel/abstract.h"
+#include "kernel/instantiate.h"
 #include "library/scoped_ext.h"
 #include "library/locals.h"
 #include "frontends/lean/parser.h"
@@ -56,4 +58,19 @@ void collect_section_locals(expr const & type, expr const & value, parser const
     collect_locals(value, ls);
     sort_section_params(ls, p, section_ps);
 }
+
+expr abstract_locals(expr const & e, parser const & p, buffer<expr> & locals) {
+    expr_struct_set ls;
+    collect_locals(e, ls);
+    sort_section_params(ls, p, locals);
+    return Fun(locals, e);
+}
+
+expr instantiate_locals(expr const & b, buffer<expr> & locals) {
+    expr _b = b;
+    unsigned sz = locals.size();
+    for (unsigned i = 0; i < sz; i++)
+        _b = binding_body(_b);
+    return instantiate_rev(_b, locals.size(), locals.data());
+}
 }
diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h
index 527af7a17..72516170b 100644
--- a/src/frontends/lean/util.h
+++ b/src/frontends/lean/util.h
@@ -19,4 +19,8 @@ levels collect_section_levels(level_param_names const & ls, parser & p);
 void collect_section_locals(expr const & type, expr const & value, parser const & p, buffer<expr> & section_ps);
 /** \brief Copy the local parameters to \c section_ps, then sort \c section_ps (using the order in which they were declared). */
 void sort_section_params(expr_struct_set const & locals, parser const & p, buffer<expr> & section_ps);
+/** \brief collect all locals in \c e and store and locals, and return Fun(locals, e) */
+expr abstract_locals(expr const & e, parser const & p, buffer<expr> & locals);
+/** \brief 'inverse' of \c abstract_locals, given a binding \c b instantiate it using locals */
+expr instantiate_locals(expr const & b, buffer<expr> & locals);
 }