From 0443c1e70cfa9e6632958750af05c10c0c0e521c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 3 Dec 2014 12:56:30 -0800
Subject: [PATCH] fix(frontends/lean): intro tactic + universe variables, fixes
 #362

---
 src/frontends/lean/decl_cmds.cpp |  2 +-
 src/frontends/lean/util.cpp      | 22 ++++++++++++++++++++++
 src/frontends/lean/util.h        |  1 +
 src/library/locals.h             |  1 +
 tests/lean/run/362.lean          | 14 ++++++++++++++
 5 files changed, 39 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/362.lean

diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 621991253..2fdfde885 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -407,7 +407,7 @@ static environment definition_cmd_core(parser & p, def_cmd_kind kind, bool is_op
         new_locals.append(locals);
         erase_local_binder_info(new_locals);
         value = Fun_as_is(new_locals, value, p);
-        update_univ_parameters(ls_buffer, collect_univ_params(value, collect_univ_params(type)), p);
+        update_univ_parameters(ls_buffer, collect_univ_params_ignoring_tactics(value, collect_univ_params_ignoring_tactics(type)), p);
         remove_local_vars(p, locals);
         ls = to_list(ls_buffer.begin(), ls_buffer.end());
         levels local_ls = collect_local_nonvar_levels(p, ls);
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index 28a88ac8a..aed888975 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -108,6 +108,28 @@ void collect_locals(expr const & type, expr const & value, parser const & p, buf
     sort_locals(ls, p, ctx_ps);
 }
 
+name_set collect_univ_params_ignoring_tactics(expr const & e, name_set const & ls) {
+    if (!has_param_univ(e)) {
+        return ls;
+    } else {
+        name_set r = ls;
+        for_each(e, [&](expr const & e, unsigned) {
+                if (!has_param_univ(e)) {
+                    return false;
+                } else if (is_by(e)) {
+                    return false; // do not visit children
+                } else if (is_sort(e)) {
+                    collect_univ_params_core(sort_level(e), r);
+                } else if (is_constant(e)) {
+                    for (auto const & l : const_levels(e))
+                        collect_univ_params_core(l, r);
+                }
+                return true;
+            });
+        return r;
+    }
+}
+
 void remove_local_vars(parser const & p, buffer<expr> & locals) {
     unsigned j = 0;
     for (unsigned i = 0; i < locals.size(); i++) {
diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h
index 87c1a1625..e7a6a8541 100644
--- a/src/frontends/lean/util.h
+++ b/src/frontends/lean/util.h
@@ -28,6 +28,7 @@ name remove_root_prefix(name const & n);
 levels collect_local_nonvar_levels(parser & p, level_param_names const & ls);
 /** \brief Collect local constants occurring in \c type and \c value, sort them, and store in ctx_ps */
 void collect_locals(expr const & type, expr const & value, parser const & p, buffer<expr> & ctx_ps);
+name_set collect_univ_params_ignoring_tactics(expr const & e, name_set const & ls = name_set());
 /** \brief Copy the local names to \c ps, then sort \c ps (using the order in which they were declared). */
 void sort_locals(expr_struct_set const & locals, parser const & p, buffer<expr> & ps);
 /** \brief Remove from \c ps local constants that are tagged as variables. */
diff --git a/src/library/locals.h b/src/library/locals.h
index 3f6f6695a..0e0b09e04 100644
--- a/src/library/locals.h
+++ b/src/library/locals.h
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 #include "kernel/expr_sets.h"
 namespace lean {
+void collect_univ_params_core(level const & l, name_set & r);
 name_set collect_univ_params(expr const & e, name_set const & ls = name_set());
 void collect_locals(expr const & e, expr_struct_set & ls);
 level_param_names to_level_param_names(name_set const & ls);
diff --git a/tests/lean/run/362.lean b/tests/lean/run/362.lean
new file mode 100644
index 000000000..c84fa8bfc
--- /dev/null
+++ b/tests/lean/run/362.lean
@@ -0,0 +1,14 @@
+variables {a : Type}
+
+definition foo (A : Type) : A → A :=
+begin
+  intro a, assumption
+end
+
+(*
+local d = get_env():find("foo")
+assert(#d:univ_params() == 1)
+*)
+
+set_option pp.universes true
+check foo