From befe2d96e1cfc51dc1053b56a8361a2bf5b7f69b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 4 Aug 2016 15:08:25 -0700
Subject: [PATCH] feat(frontends/lean/elaborator): chaining for anonymous
 constructors

---
 src/frontends/lean/builtin_exprs.h |  1 +
 src/frontends/lean/elaborator.cpp  | 16 +++++++++++++++-
 tests/lean/anc1.lean               | 10 ++++++++++
 tests/lean/anc1.lean.expected.out  |  4 ++++
 4 files changed, 30 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/builtin_exprs.h b/src/frontends/lean/builtin_exprs.h
index edde41be5e..9ba53afcae 100644
--- a/src/frontends/lean/builtin_exprs.h
+++ b/src/frontends/lean/builtin_exprs.h
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "frontends/lean/parse_table.h"
 namespace lean {
+expr mk_anonymous_constructor(expr const & e);
 bool is_anonymous_constructor(expr const & e);
 expr const & get_anonymous_constructor_arg(expr const & e);
 parse_table get_builtin_nud_table();
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 3bf99fe8b5..aa88409627 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1133,7 +1133,7 @@ expr elaborator::visit_by(expr const & e, optional<expr> const & expected_type)
 expr elaborator::visit_anonymous_constructor(expr const & e, optional<expr> const & expected_type) {
     lean_assert(is_anonymous_constructor(e));
     buffer<expr> args;
-    get_app_args(get_anonymous_constructor_arg(e), args);
+    expr const & c = get_app_args(get_anonymous_constructor_arg(e), args);
     if (!expected_type)
         throw elaborator_exception(e, "invalid constructor ⟨...⟩, expected type must be known");
     expr I = get_app_fn(m_ctx.relaxed_whnf(instantiate_mvars(*expected_type)));
@@ -1147,6 +1147,20 @@ expr elaborator::visit_anonymous_constructor(expr const & e, optional<expr> cons
     get_intro_rule_names(m_env, I_name, c_names);
     if (c_names.size() != 1)
         throw elaborator_exception(e, sstream() << "invalid constructor ⟨...⟩, '" << I_name << "' must have only one constructor");
+    expr type = m_env.get(c_names[0]).get_type();
+    unsigned num_explicit = 0;
+    while (is_pi(type)) {
+        if (is_explicit(binding_info(type)))
+            num_explicit++;
+        type = binding_body(type);
+    }
+    if (num_explicit > 1 && args.size() > num_explicit) {
+        unsigned num_extra = args.size() - num_explicit;
+        expr rest = copy_tag(e, mk_app(c, num_extra + 1, args.data() + num_explicit - 1));
+        rest = copy_tag(e, mk_anonymous_constructor(rest));
+        args.shrink(num_explicit);
+        args.back() = rest;
+    }
     expr new_e = copy_tag(e, mk_app(mk_constant(c_names[0]), args));
     return visit(new_e, expected_type);
 }
diff --git a/tests/lean/anc1.lean b/tests/lean/anc1.lean
index 8c8b2cd88c..b6766c1342 100644
--- a/tests/lean/anc1.lean
+++ b/tests/lean/anc1.lean
@@ -22,6 +22,11 @@ check λ (A B C : Prop),
   show B ∧ A ∧ C ∧ A, from
   ⟨Hb, ⟨Ha, ⟨Hc, Ha⟩⟩⟩
 
+check λ (A B C : Prop),
+  assume (Ha : A) (Hb : B) (Hc : C),
+  show B ∧ A ∧ C ∧ A, from
+  ⟨Hb, Ha, Hc, Ha⟩
+
 check λ (A B C : Prop),
   assume (Ha : A) (Hb : B) (Hc : C),
   show ((B ∧ true) ∧ A) ∧ (C ∧ A), from
@@ -36,3 +41,8 @@ check λ (A : Type) (P : A → Prop) (Q : A → Prop),
   take (a : A) (b : A), assume (H1 : P a) (H2 : Q b),
   show ∃ x y, P x ∧ Q y, from
   ⟨a, ⟨b, ⟨H1, H2⟩⟩⟩
+
+check λ (A : Type) (P : A → Prop) (Q : A → Prop),
+  take (a : A) (b : A), assume (H1 : P a) (H2 : Q b),
+  show ∃ x y, P x ∧ Q y, from
+  ⟨a, b, H1, H2⟩
diff --git a/tests/lean/anc1.lean.expected.out b/tests/lean/anc1.lean.expected.out
index 502f7300c4..9c7e281394 100644
--- a/tests/lean/anc1.lean.expected.out
+++ b/tests/lean/anc1.lean.expected.out
@@ -4,6 +4,8 @@ sigma.mk 1 sorry : Σ x, x > 0
 show true, from true.intro : true
 Exists.intro 1 (λ a, nat.no_confusion a) : ∃ x, 1 ≠ 0
 λ A B C Ha Hb Hc, show B ∧ A, from and.intro Hb Ha : ∀ A B C, A → B → C → B ∧ A
+λ A B C Ha Hb Hc, show B ∧ A ∧ C ∧ A, from and.intro Hb (and.intro Ha (and.intro Hc Ha)) :
+  ∀ A B C, A → B → C → B ∧ A ∧ C ∧ A
 λ A B C Ha Hb Hc, show B ∧ A ∧ C ∧ A, from and.intro Hb (and.intro Ha (and.intro Hc Ha)) :
   ∀ A B C, A → B → C → B ∧ A ∧ C ∧ A
 λ A B C Ha Hb Hc,
@@ -13,3 +15,5 @@ Exists.intro 1 (λ a, nat.no_confusion a) : ∃ x, 1 ≠ 0
   ∀ A P Q a, P a → Q a → (∃ x, P x ∧ Q x)
 λ A P Q a b H1 H2, show ∃ x y, P x ∧ Q y, from Exists.intro a (Exists.intro b (and.intro H1 H2)) :
   ∀ A P Q a b, P a → Q b → (∃ x y, P x ∧ Q y)
+λ A P Q a b H1 H2, show ∃ x y, P x ∧ Q y, from Exists.intro a (Exists.intro b (and.intro H1 H2)) :
+  ∀ A P Q a b, P a → Q b → (∃ x y, P x ∧ Q y)