From e04e9ff87e005600652efb7bb163917a8fe9861e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 13 Mar 2021 17:11:37 -0800
Subject: [PATCH] feat: extend anonymous ctor notation

---
 src/Lean/Elab/BuiltinNotation.lean | 21 ++++++++++++++++++++-
 tests/lean/run/newfrontend3.lean   | 15 +++++++++++----
 2 files changed, 31 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index bb06db6bcb..1965610dfe 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -25,7 +25,26 @@ open Meta
         (fun ival us => do
           match ival.ctors with
           | [ctor] =>
-            let newStx ← `($(mkCIdentFrom stx ctor) $(args)*)
+            let cinfo ← getConstInfoCtor ctor
+            let numExplicitFields ← forallTelescopeReducing cinfo.type fun xs _ => do
+              let mut n := 0
+              for i in [cinfo.numParams:xs.size] do
+                if (← getFVarLocalDecl xs[i]).binderInfo.isExplicit then
+                  n := n + 1
+              return n
+            let args := args.getElems
+            if args.size < numExplicitFields then
+              throwError "invalid constructor ⟨...⟩, insufficient number of arguments, constructs '{ctor}' has #{numExplicitFields} explicit fields, but only #{args.size} provided"
+            let newStx ←
+              if args.size == numExplicitFields then
+                `($(mkCIdentFrom stx ctor) $(args)*)
+              else if numExplicitFields == 0 then
+                throwError "invalid constructor ⟨...⟩, insufficient number of arguments, constructs '{ctor}' does not have explicit fields, but #{args.size} provided"
+              else
+                let extra := args[numExplicitFields-1:args.size]
+                let newLast ← `(⟨$[$extra],*⟩)
+                let newArgs := args[0:numExplicitFields-1].toArray.push newLast
+                `($(mkCIdentFrom stx ctor) $(newArgs)*)
             withMacroExpansion stx newStx $ elabTerm newStx expectedType?
           | _ => throwError "invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor {indentExpr expectedType}")
     | none => throwError "invalid constructor ⟨...⟩, expected type must be known"
diff --git a/tests/lean/run/newfrontend3.lean b/tests/lean/run/newfrontend3.lean
index c6f488fbd6..61bd2481b0 100644
--- a/tests/lean/run/newfrontend3.lean
+++ b/tests/lean/run/newfrontend3.lean
@@ -1,4 +1,4 @@
-
+--
 
 structure S  :=
 (g {α} : α → α)
@@ -16,11 +16,18 @@ by {
 }
 
 def g (i j k : Nat) (a : Array Nat) (h₁ : i < k) (h₂ : k < j) (h₃ : j < a.size) : Nat :=
-let vj := a.get ⟨j, h₃⟩;
-let vi := a.get ⟨i, Nat.ltTrans h₁ (Nat.ltTrans h₂ h₃)⟩;
-vi + vj
+  let vj := a.get ⟨j, h₃⟩;
+  let vi := a.get ⟨i, Nat.ltTrans h₁ (Nat.ltTrans h₂ h₃)⟩;
+  vi + vj
 
 set_option pp.all true in
 #print g
 
 #check g.proof_1
+
+theorem ex1 {p q r s : Prop} : p ∧ q ∧ r ∧ s → r ∧ s ∧ q ∧ p :=
+  fun ⟨hp, hq, hr, hs⟩ => ⟨hr, hs, hq, hp⟩
+
+theorem ex2 {p q r s : Prop} : p ∧ q ∧ r ∧ s → r ∧ s ∧ q ∧ p := by
+  intro ⟨hp, hq, hr, hs⟩
+  exact ⟨hr, hs, hq, hp⟩