From ce622e9179fa363dbe388e305e34faa54e5ffe29 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 13 Dec 2015 13:39:34 -0800
Subject: [PATCH] feat(frontends/lean): add auto-include for structures and
 inductive decls

---
 src/frontends/lean/inductive_cmd.cpp       | 1 +
 src/frontends/lean/structure_cmd.cpp       | 1 +
 src/frontends/lean/util.cpp                | 2 +-
 src/frontends/lean/util.h                  | 2 ++
 tests/lean/run/auto_include_inductive.lean | 8 ++++++++
 5 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/auto_include_inductive.lean

diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index f4ad64fd90..3d435f10b7 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -431,6 +431,7 @@ struct inductive_cmd_fn {
         collect_locals_core(decls, local_set);
         if (local_set.empty())
             return;
+        collect_annonymous_inst_implicit(m_p, local_set);
         sort_locals(local_set.get_collected(), m_p, locals);
         m_num_params += locals.size();
     }
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 92c8b42de4..1e514ccf2c 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -306,6 +306,7 @@ struct structure_cmd_fn {
         }
         for (expr const & p : m_params)
             ::lean::collect_locals(mlocal_type(p), dep_set);
+        collect_annonymous_inst_implicit(m_p, dep_set);
         buffer<expr> ctx;
         sort_locals(dep_set.get_collected(), m_p, ctx);
 
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index 78ff697ba3..aa24284a61 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -128,7 +128,7 @@ static void collect_locals_ignoring_tactics(expr const & e, collected_locals & l
         });
 }
 
-static void collect_annonymous_inst_implicit(parser const & p, collected_locals & ls) {
+void collect_annonymous_inst_implicit(parser const & p, collected_locals & ls) {
     for (auto const & entry : p.get_local_entries()) {
         if (is_local(entry.second) && !ls.contains(entry.second) && local_info(entry.second).is_inst_implicit() &&
             // remark: remove the following condition condition, if we want to auto inclusion also for non anonymous ones.
diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h
index 87b689157c..8de535e18c 100644
--- a/src/frontends/lean/util.h
+++ b/src/frontends/lean/util.h
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/expr_sets.h"
 #include "kernel/type_checker.h"
 #include "library/util.h"
+#include "library/locals.h"
 #include "library/tactic/util.h"
 #include "frontends/lean/local_decls.h"
 
@@ -36,6 +37,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);
+void collect_annonymous_inst_implicit(parser const & p, collected_locals & ls);
 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(buffer<expr> const & locals, parser const & p, buffer<expr> & ps);
diff --git a/tests/lean/run/auto_include_inductive.lean b/tests/lean/run/auto_include_inductive.lean
new file mode 100644
index 0000000000..c459b9e823
--- /dev/null
+++ b/tests/lean/run/auto_include_inductive.lean
@@ -0,0 +1,8 @@
+import algebra.group
+
+variables {A : Type} [group A]
+
+inductive foo :=
+mk₁ : ∀ (a : A), a * a = a → foo
+
+print foo