From 54844e2325d38243d5854909a3276228b7aed783 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 5 Jul 2016 14:52:00 -0700
Subject: [PATCH] feat(frontends/lean): add parent classes to local context in
 struct definitions

Fixes #1066
---
 src/frontends/lean/structure_cmd.cpp   | 51 ++++++++++++++------------
 tests/lean/run/parent_struct_inst.lean | 10 +++++
 2 files changed, 38 insertions(+), 23 deletions(-)
 create mode 100644 tests/lean/run/parent_struct_inst.lean

diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 7bf1285d8..d53718e97 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -293,11 +293,12 @@ struct structure_cmd_fn {
         return new_tmp;
     }
 
-    expr update_parents(expr new_tmp) {
+    expr update_parents(expr new_tmp, bool inst) {
         for (unsigned i = 0; i < m_parents.size(); i++) {
             m_parents[i]   = copy_tag(m_parents[i], expr(binding_domain(new_tmp)));
             new_tmp        = binding_body(new_tmp);
-            lean_assert(closed(new_tmp));
+            if (inst)
+                new_tmp = instantiate(new_tmp, mk_parent_expr(i));
         }
         return new_tmp;
     }
@@ -342,7 +343,7 @@ struct structure_cmd_fn {
         m_params.clear();
         m_params.append(ctx);
         m_params.append(explicit_params);
-        new_tmp = update_parents(new_tmp);
+        new_tmp = update_parents(new_tmp, false);
         m_type = new_tmp;
     }
 
@@ -471,6 +472,24 @@ struct structure_cmd_fn {
         solve_constraints(cseq);
     }
 
+    /** \brief Create expression of type \c m_parents[i] from corresponding fields */
+    expr mk_parent_expr(unsigned i) {
+        expr const & parent            = m_parents[i];
+        field_map const & fmap         = m_field_maps[i];
+        buffer<expr> parent_params;
+        expr const & parent_fn         = get_app_args(parent, parent_params);
+        levels const & parent_ls       = const_levels(parent_fn);
+        name const & parent_name       = const_name(parent_fn);
+        auto parent_info               = get_parent_info(parent_name);
+        name const & parent_intro_name = inductive::intro_rule_name(std::get<2>(parent_info));
+        expr parent_intro              = mk_app(mk_constant(parent_intro_name, parent_ls), parent_params);
+        for (unsigned idx : fmap) {
+            expr const & field = m_fields[idx];
+            parent_intro = mk_app(parent_intro, field);
+        }
+        return parent_intro;
+    }
+
     /** \brief Add params, fields and references to parent structures into parser local scope */
     void add_locals() {
         if (m_explicit_universe_params) {
@@ -482,22 +501,8 @@ struct structure_cmd_fn {
         for (expr const & field : m_fields)
             m_p.add_local(field);
         for (unsigned i = 0; i < m_parents.size(); i++) {
-            if (auto n = m_parent_refs[i]) {
-                expr const & parent            = m_parents[i];
-                field_map const & fmap         = m_field_maps[i];
-                buffer<expr> parent_params;
-                expr const & parent_fn         = get_app_args(parent, parent_params);
-                levels const & parent_ls       = const_levels(parent_fn);
-                name const & parent_name       = const_name(parent_fn);
-                auto parent_info               = get_parent_info(parent_name);
-                name const & parent_intro_name = inductive::intro_rule_name(std::get<2>(parent_info));
-                expr parent_intro              = mk_app(mk_constant(parent_intro_name, parent_ls), parent_params);
-                for (unsigned idx : fmap) {
-                    expr const & field = m_fields[idx];
-                    parent_intro = mk_app(parent_intro, field);
-                }
-                m_p.add_local_expr(*n, mk_as_is(parent_intro));
-            }
+            if (auto n = m_parent_refs[i])
+                m_p.add_local_expr(*n, mk_as_is(mk_parent_expr(i)));
         }
     }
 
@@ -552,22 +557,22 @@ struct structure_cmd_fn {
 
     /** \brief Elaborate new fields, and copy them to m_fields */
     void elaborate_new_fields(buffer<expr> & new_fields) {
-        expr dummy = mk_Prop();
+        expr tmp = Pi_as_is(m_fields, Pi(new_fields, mk_Prop(), m_p), m_p);
         unsigned j = m_parents.size();
         while (j > 0) {
             --j;
-            dummy = mk_arrow(mk_as_is(m_parents[j]), dummy);
+            tmp = mk_arrow(mk_as_is(m_parents[j]), tmp);
         }
-        expr tmp = Pi_as_is(m_params, Pi_as_is(m_fields, Pi(new_fields, dummy, m_p), m_p), m_p);
+        tmp = Pi_as_is(m_params, tmp, m_p);
         level_param_names new_ls;
         expr new_tmp;
         std::tie(new_tmp, new_ls) = m_p.elaborate_type(tmp, list<expr>());
         for (auto new_l : new_ls)
             m_level_names.push_back(new_l);
         new_tmp = update_locals(new_tmp, m_params);
+        new_tmp = update_parents(new_tmp, true);
         new_tmp = update_locals(new_tmp, m_fields);
         new_tmp = update_locals(new_tmp, new_fields);
-        new_tmp = update_parents(new_tmp);
         lean_assert(new_tmp == mk_Prop());
         m_fields.append(new_fields);
     }
diff --git a/tests/lean/run/parent_struct_inst.lean b/tests/lean/run/parent_struct_inst.lean
new file mode 100644
index 000000000..edba6a59c
--- /dev/null
+++ b/tests/lean/run/parent_struct_inst.lean
@@ -0,0 +1,10 @@
+open nat
+
+structure A [class] := (n : ℕ)
+
+definition f [A] := A.n
+
+structure B extends A :=
+(Hf : f = 0)
+
+example : B := ⦃B, n := 0, Hf := rfl⦄