From 3b23bec25b9682d3277ad9719906d3a1e706fd17 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 8 Oct 2014 08:37:54 -0700
Subject: [PATCH] feat(frontends/lean): variables/parameters and check commands
 have access to all section variables/parameters, closes #231

---
 src/frontends/lean/builtin_cmds.cpp |  2 +-
 src/frontends/lean/decl_cmds.cpp    |  2 +-
 src/frontends/lean/parser.cpp       |  4 ++++
 tests/lean/const.lean               | 17 +++++++++++++++++
 tests/lean/const.lean.expected.out  |  2 ++
 5 files changed, 25 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/const.lean
 create mode 100644 tests/lean/const.lean.expected.out

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 3c903e54d..a23dfe57c 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -130,7 +130,7 @@ environment end_scoped_cmd(parser & p) {
 /** \brief Auxiliary function for check/eval */
 static std::tuple<expr, level_param_names> parse_local_expr(parser & p) {
     expr e   = p.parse_expr();
-    list<expr> ctx = locals_to_context(e, p);
+    list<expr> ctx = p.locals_to_context();
     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, ctx);
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 5c86f49fe..d749c3b65 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -167,7 +167,7 @@ environment variable_cmd_core(parser & p, variable_kind k) {
         ls = to_list(ls_buffer.begin(), ls_buffer.end());
     }
     level_param_names new_ls;
-    list<expr> ctx = locals_to_context(type, p);
+    list<expr> ctx = p.locals_to_context();
     std::tie(type, new_ls) = p.elaborate_type(type, ctx);
     update_section_local_levels(p, new_ls, k == variable_kind::Variable);
     return declare_var(p, p.env(), n, append(ls, new_ls), type, k, bi, pos);
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index e17c8ac5f..c2b3275b5 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -463,6 +463,10 @@ void parser::get_include_variables(buffer<expr> & vars) const {
         });
 }
 
+list<expr> parser::locals_to_context() const {
+    return filter(m_local_decls.get_values(), [](expr const & e) { return is_local(e); });
+}
+
 static unsigned g_level_add_prec = 10;
 static unsigned g_level_cup_prec = 5;
 
diff --git a/tests/lean/const.lean b/tests/lean/const.lean
new file mode 100644
index 000000000..70df5fc54
--- /dev/null
+++ b/tests/lean/const.lean
@@ -0,0 +1,17 @@
+import logic
+
+
+definition foo {A : Type} {H : inhabited A} : A :=
+inhabited.rec (λa, a) H
+
+constant bla {A : Type} {H : inhabited A} : Type.{1}
+
+set_option pp.implicit true
+
+section
+  variable A : Type
+  variable S : inhabited A
+  variable B : bla
+  check B
+  check @foo A _
+end
diff --git a/tests/lean/const.lean.expected.out b/tests/lean/const.lean.expected.out
new file mode 100644
index 000000000..453e9b677
--- /dev/null
+++ b/tests/lean/const.lean.expected.out
@@ -0,0 +1,2 @@
+B : @bla A S
+@foo A S : A