From c58f61e925bfb921b372f0f0873b60c7438c74ac Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 9 Mar 2017 00:11:51 -0800
Subject: [PATCH] feat(frontends/lean/elaborator): new encoding for structure
 updates `{s with ...}`
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

See discussion at #1438
https://github.com/leanprover/lean/pull/1438#discussion_r105007325

@digama0 With this commit, the original `array_list.write` will also
perform a destructive update when the reference counter for `l` is 1.

```lean def write {α} (l : array_list α) : fin l^.length → α → array_list α :=
λ ⟨n, h⟩ v, { l with data := l^.data^.write ⟨n, l^.lt_capacity h⟩ h v }
```
---
 library/init/algebra/group.lean   |  2 ++
 src/frontends/lean/elaborator.cpp | 22 +++++++++++++++++-----
 2 files changed, 19 insertions(+), 5 deletions(-)

diff --git a/library/init/algebra/group.lean b/library/init/algebra/group.lean
index 644d1be264..2ac92d4932 100644
--- a/library/init/algebra/group.lean
+++ b/library/init/algebra/group.lean
@@ -210,6 +210,8 @@ meta def multiplicative_to_additive_pairs : list (name × name) :=
   [/- map operations -/
    (`mul, `add), (`one, `zero), (`inv, `neg),
    (`has_mul, `has_add), (`has_one, `has_zero), (`has_inv, `has_neg),
+   /- map constructors -/
+   (`has_mul.mk, `has_add.mk), (`has_one, `has_zero.mk), (`has_inv, `has_neg.mk),
    /- map structures -/
    (`semigroup, `add_semigroup),
    (`monoid, `add_monoid),
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 621ab31ec7..cadb525d6d 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2463,7 +2463,8 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
                                    S_name << "' is not the name of a structure type");
     lean_assert(fnames.size() == fvalues.size());
     name src_S_name;
-    unsigned src_S_nparams = 0;
+    bool src_S_name_is_class = false;
+    unsigned src_S_nparams   = 0;
     if (src) {
         src = visit(*src, none_expr());
         synthesize_type_class_instances();
@@ -2477,8 +2478,9 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
                                        line() + format("which has type") +
                                        pp_indent(pp_fn, type));
         }
-        src_S_name    = const_name(src_S);
-        src_S_nparams = *inductive::get_num_params(m_env, src_S_name);
+        src_S_name          = const_name(src_S);
+        src_S_nparams       = *inductive::get_num_params(m_env, src_S_name);
+        src_S_name_is_class = is_class(env(), src_S_name);
     }
     if (S_name.is_anonymous()) {
         if (expected_type) {
@@ -2513,6 +2515,7 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
     expr c_type      = infer_type(c);
     buffer<expr> c_args;
     buffer<std::tuple<name, expr, expr>> to_elaborate;
+    type_context::tmp_locals let_decls(m_ctx);
     /* First check for explicit, implicit, parent, auto_param fields.
        We create metavariables for parameters.
        For auto_param fields, we create metavariable and use the specifed tactic to synthesize the field.
@@ -2569,6 +2572,16 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
                             msg += std::get<2>(pp_data);
                             throw elaborator_exception(ref, msg);
                         }
+                        if (!m_ctx.is_prop(c_arg_type) && !src_S_name_is_class) {
+                            /* The condition (!src_S_name_is_class) is a temporary workaround
+                               to address unification failures in the algebraic hierarchy.
+                               We need to investigate why the extra let-expressions are affecting the unifier.
+
+                               The condition (!m_ctx.is_prop(c_arg_type)) is an optimization.
+                               To solve the issue described at #1438, we don't need to create
+                               let-declarations for proofs since they will be erased. */
+                            c_arg = let_decls.push_let(name("_src").append_after(let_decls.size()+1), c_arg_type, c_arg);
+                        }
                         field2value.insert(S_fname, c_arg);
                     } else {
                         name full_S_fname = S_name + S_fname;
@@ -2663,8 +2676,7 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
         }
         last_progress = progress;
     }
-
-    return mk_app(c, c_args);
+    return let_decls.mk_lambda(mk_app(c, c_args));
 }
 
 static expr quote(expr const & e) {