feat: elaborate fun/forall binder extensions

doc/lean3changes.md

@@ -204,13 +204,12 @@ one of the following three equivalent notations:
 `forall x : α, β x` or `∀ x : α, β x` or `Π x : α, β x`.
 The first two were intended to be used for writing propositions, and the latter for writing code.
 Although the notation `Π x : α, β x` has historical significance, we have removed it from Lean 4 because
-it is awkward to use and often confuses new users. We can still write `forall (x : α), β x` and `∀ (x : α), β x`,
-but the parentheses are not optional when the type is provided explicitly.
+it is awkward to use and often confuses new users. We can still write `forall x : α, β x` and `∀ x : α, β x`.
 
 ```lean
 #check forall (α : Type), α → α
 #check ∀ (α : Type), α → α
--- #check ∀ α : Type, α → α -- Not valid in Lean 4
+#check ∀ α : Type, α → α
 #check ∀ α, α → α
 #check (α : Type) → α → α
 #check {α : Type} → (a : Array α) → (i : Nat) → i < a.size → α

src/Lean/Elab/Binders.lean

@@ -97,13 +97,25 @@ private def getBinderIds (ids : Syntax) : TermElabM (Array Syntax) :=
     else
       throwErrorAt id "identifier or `_` expected"
 
+/-
+  Recall that
+  ```
+  def typeSpec := parser! " : " >> termParser
+  def optType : Parser := optional typeSpec
+  ``` -/
+def expandOptType (ref : Syntax) (optType : Syntax) : Syntax :=
+  if optType.isNone then
+    mkHole ref
+  else
+    optType[0][1]
+
 private def matchBinder (stx : Syntax) : TermElabM (Array BinderView) :=
   match stx with
   | Syntax.node k args => do
     if k == `Lean.Parser.Term.simpleBinder then
-      -- binderIdent+
+      -- binderIdent+ >> optType
       let ids ← getBinderIds args[0]
-      let type := mkHole stx
+      let type := expandOptType stx args[1]
       ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := type, bi := BinderInfo.default }
     else if k == `Lean.Parser.Term.explicitBinder then
       -- `(` binderIdent+ binderType (binderDefault <|> binderTactic)? `)`
@@ -244,6 +256,7 @@ partial def expandFunBinders (binders : Array Syntax) (body : Syntax) : TermElab
       | Syntax.node `Lean.Parser.Term.implicitBinder _ => loop body (i+1) (newBinders.push binder)
       | Syntax.node `Lean.Parser.Term.instBinder _     => loop body (i+1) (newBinders.push binder)
       | Syntax.node `Lean.Parser.Term.explicitBinder _ => loop body (i+1) (newBinders.push binder)
+      | Syntax.node `Lean.Parser.Term.simpleBinder _   => loop body (i+1) (newBinders.push binder)
       | Syntax.node `Lean.Parser.Term.hole _ =>
         let ident ← mkFreshIdent binder
         let type := binder
@@ -340,18 +353,6 @@ def elabFunBinders {α} (binders : Array Syntax) (expectedType? : Option Expr) (
     resettingSynthInstanceCacheWhen (s.localInsts.size > localInsts.size) $ withLCtx s.lctx s.localInsts $
       x s.fvars s.expectedType?
 
-/-
-  Recall that
-  ```
-  def typeSpec := parser! " : " >> termParser
-  def optType : Parser := optional typeSpec
-  ``` -/
-def expandOptType (ref : Syntax) (optType : Syntax) : Syntax :=
-  if optType.isNone then
-    mkHole ref
-  else
-    optType[0][1]
-
 /- Helper function for `expandEqnsIntoMatch` -/
 private def getMatchAltNumPatterns (matchAlts : Syntax) : Nat :=
   let alt0 := matchAlts[1][0]

src/Lean/Parser/Term.lean

@@ -119,10 +119,7 @@ Note that we did not add a `explicitShortBinder` parser since `(α) → α →
 -/
 @[builtinTermParser] def depArrow := parser! bracketedBinder true >> checkPrec 25 >> unicodeSymbol " → " " -> " >> termParser
 
-def simpleBinder := parser!
-  (checkInsideQuot >> many1 binderIdent >> optType)
-  <|>
-  (checkOutsideQuot >> many1 binderIdent)
+def simpleBinder := parser! many1 binderIdent >> optType
 @[builtinTermParser]
 def «forall» := parser!:leadPrec unicodeSymbol "∀ " "forall" >> many1 (ppSpace >> (simpleBinder <|> bracketedBinder)) >> ", " >> termParser
 
@@ -141,8 +138,8 @@ def matchDiscr := parser! optional («try» (ident >> checkNoWsBefore "no space
 @[builtinTermParser] def «nomatch»  := parser!:leadPrec "nomatch " >> termParser
 
 def funImplicitBinder := «try» (lookahead ("{" >> many1 binderIdent >> (" : " <|> "}"))) >> implicitBinder
-def funSimpleBinder   := parser! «try» (lookahead (many1 binderIdent >> " : ")) >> many1 binderIdent >> optType
-def funBinder : Parser := funImplicitBinder <|> instBinder <|> (checkInsideQuot >> funSimpleBinder) <|> termParser maxPrec
+def funSimpleBinder   := «try» (lookahead (many1 binderIdent >> " : ")) >> simpleBinder
+def funBinder : Parser := funImplicitBinder <|> instBinder <|> funSimpleBinder <|> termParser maxPrec
 -- NOTE: we use `nodeWithAntiquot` to ensure that `fun $b => ...` remains a `term` antiquotation
 def basicFun : Parser := nodeWithAntiquot "basicFun" `Lean.Parser.Term.basicFun (many1 (ppSpace >> funBinder) >> darrow >> termParser)
 @[builtinTermParser] def «fun» := parser!:maxPrec unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts false)

tests/compiler/termparsertest1.lean.expected.out

@@ -140,7 +140,7 @@ f ((x : a) -> b)
 ∀ x y (z : Nat), x > y -> x > y - z
 (Term.forall
  "∀"
- [(Term.simpleBinder [`x `y]) (Term.explicitBinder "(" [`z] [":" `Nat] [] ")")]
+ [(Term.simpleBinder [`x `y] []) (Term.explicitBinder "(" [`z] [":" `Nat] [] ")")]
  ","
  (Term.arrow (Term.gt `x ">" `y) "->" (Term.gt `x ">" (Term.sub `y "-" `z))))
 

tests/lean/StxQuot.lean.expected.out

@@ -21,8 +21,8 @@
 "(Term.fun\n \"fun\"\n (Term.basicFun\n  [`a._@.UnhygienicMain._hyg.1\n   (Term.paren \"(\" [`b._@.UnhygienicMain._hyg.1 [(Term.typeAscription \":\" `Nat._@.UnhygienicMain._hyg.1)]] \")\")]\n  \"=>\"\n  (numLit \"1\")))"
 "#[(Term.paren \"(\" [`a._@.UnhygienicMain._hyg.1 [(Term.typeAscription \":\" `Nat._@.UnhygienicMain._hyg.1)]] \")\"), `b._@.UnhygienicMain._hyg.1]"
 "`a._@.UnhygienicMain._hyg.1"
-"(Term.forall \"∀\" [(Term.simpleBinder [(Term.hole \"_\")])] \",\" `c._@.UnhygienicMain._hyg.1)"
-"(Term.simpleBinder [(Term.hole \"_\")])"
+"(Term.forall \"∀\" [(Term.simpleBinder [(Term.hole \"_\")] [])] \",\" `c._@.UnhygienicMain._hyg.1)"
+"(Term.simpleBinder [(Term.hole \"_\")] [])"
 "`a._@.UnhygienicMain._hyg.1"
 "(Term.explicitUniv `a._@.UnhygienicMain._hyg.1 \".{\" [(numLit \"0\")] \"}\")"
 "#[]"

tests/lean/match1.lean.expected.out

@@ -22,3 +22,7 @@ constructor expected
 match1.lean:124:0: error: invalid match-expression, type of pattern variable 'a' contains metavariables
   ?m
 fun (x : ?m × ?m) => ?m x : ?m × ?m → ?m
+fun (x : Nat × Nat) => _check.match_1 (fun (x_1 : Nat × Nat) => Nat) x fun (a b : Nat) => a + b : Nat × Nat → Nat
+fun (x : Bool × Bool) =>
+  _check.match_1 (fun (x_1 : Bool × Bool) => Bool) x fun (a b : Bool) => a && b : Bool × Bool → Bool
+fun (x : Nat × Nat) => _check.match_1 (fun (x_1 : Nat × Nat) => Nat) x fun (a b : Nat) => a + b : Nat × Nat → Nat

tests/lean/run/newfrontend1.lean

@@ -12,6 +12,8 @@ xs.foldl (init := 10) (· + ·)
 
 #check tst [1, 2, 3]
 
+#check fun x y : Nat => x + y
+
 #check tst
 
 #check (fun stx => if True then let e := stx; Pure.pure e else Pure.pure stx : Nat → Id Nat)