refactor: split paren parser

src/Lean/Elab/Binders.lean

@@ -352,35 +352,26 @@ partial def expandFunBinders (binders : Array Syntax) (body : Syntax) : MacroM (
       | ``Lean.Parser.Term.explicitBinder
       | ``Lean.Parser.Term.hole | `ident => loop body (i+1) (newBinders.push binder)
       | ``Lean.Parser.Term.paren =>
-        -- `(` (termParser >> parenSpecial)? `)`
-        -- parenSpecial := (tupleTail <|> typeAscription)?
-        let binderBody := binder[1]
-        if binderBody.isNone then
-          processAsPattern ()
-        else
-          let term    := binderBody[0]
-          let special := binderBody[1]
-          if special.isNone then
-            match (← getFunBinderIds? term) with
-            | some idents =>
-              -- `fun (x ...) ...` ~> `fun (x : _) ...`
-              -- Interpret `(x ...)` as sequence of binders instead of pattern only if none of the idents
-              -- are defined in the global scope. Technically, it would be sufficient to only check the
-              -- first ident to be sure that the syntax cannot possibly be a valid pattern. However, for
-              -- consistency we apply the same check to all idents so that the possibility of shadowing
-              -- a global decl is identical for all of them.
-              if (← idents.allM fun ident => return List.isEmpty (← Macro.resolveGlobalName ident.getId)) then
-                loop body (i+1) (newBinders ++ idents.map (mkExplicitBinder · (mkHole binder)))
-              else
-                processAsPattern ()
-            | none => processAsPattern ()
-          else if special[0].getKind != ``Lean.Parser.Term.typeAscription then
+        let term := binder[1]
+        match (← getFunBinderIds? term) with
+        | some idents =>
+          -- `fun (x ...) ...` ~> `fun (x : _) ...`
+          -- Interpret `(x ...)` as sequence of binders instead of pattern only if none of the idents
+          -- are defined in the global scope. Technically, it would be sufficient to only check the
+          -- first ident to be sure that the syntax cannot possibly be a valid pattern. However, for
+          -- consistency we apply the same check to all idents so that the possibility of shadowing
+          -- a global decl is identical for all of them.
+          if (← idents.allM fun ident => return List.isEmpty (← Macro.resolveGlobalName ident.getId)) then
+            loop body (i+1) (newBinders ++ idents.map (mkExplicitBinder · (mkHole binder)))
+          else
             processAsPattern ()
-          -- typeAscription := `:` (term)?
-          else if let some idents ← getFunBinderIds? term then
-            let type := special[0][1].getOptional?.getD (mkHole binder)
-            loop body (i+1) (newBinders ++ idents.map (mkExplicitBinder · type))
-          else processAsPattern ()
+        | none => processAsPattern ()
+      | ``Lean.Parser.Term.typeAscription =>
+        let term := binder[1]
+        let type := binder[3].getOptional?.getD (mkHole binder)
+        match (← getFunBinderIds? term) with
+        | some idents => loop body (i+1) (newBinders ++ idents.map (fun ident => mkExplicitBinder ident type))
+        | none        => processAsPattern ()
       | _ => processAsPattern ()
     else
       pure (newBinders, body, false)

src/Lean/Elab/BuiltinNotation.lean

@@ -159,10 +159,11 @@ partial def mkPairs (elems : Array Term) : MacroM Term :=
       pure acc
   loop (elems.size - 1) elems.back
 
+open Parser in
 partial def hasCDot : Syntax → Bool
   | Syntax.node _ k args =>
-    if k == ``Lean.Parser.Term.paren then false
-    else if k == ``Lean.Parser.Term.cdot then true
+    if k == ``Term.paren || k == ``Term.typeAscription || k == ``Term.tuple then false
+    else if k == ``Term.cdot then true
     else args.any hasCDot
   | _ => false
 
@@ -222,32 +223,32 @@ where
     | _ => Term.expandCDot? stx
 
 @[builtin_macro Lean.Parser.Term.paren] def expandParen : Macro
-  | `(())           => `(Unit.unit)
+  | `(($e)) => return (← expandCDot? e).getD e
+  | _       => Macro.throwUnsupported
+
+@[builtin_macro Lean.Parser.Term.tuple] def expandTuple : Macro
+  | `(()) => ``(Unit.unit)
+  | `(($e, $es,*)) => do
+    let pairs ← mkPairs (#[e] ++ es)
+    return (← expandCDot? pairs).getD pairs
+  | _ => Macro.throwUnsupported
+
+@[builtin_macro Lean.Parser.Term.typeAscription] def expandTypeAscription : Macro
   | `(($e : $(type)?)) => do
     match (← expandCDot? e) with
     | some e => `(($e : $(type)?))
     | none   => Macro.throwUnsupported
-  | `(($e))         => return (← expandCDot? e).getD e
-  | `(($e, $es,*))  => do
-    let pairs ← mkPairs (#[e] ++ es)
-    return (← expandCDot? pairs).getD pairs
-  | stx =>
-    if !stx[1][0].isMissing && stx[1][1].isMissing then
-      -- parsed `(` and `term`, assume it's a basic parenthesis to get any elaboration output at all
-      `(($(⟨stx[1][0]⟩)))
-    else
-      throw <| Macro.Exception.error stx "unexpected parentheses notation"
+  | _ => Macro.throwUnsupported
 
-@[builtin_term_elab paren] def elabParen : TermElab := fun stx expectedType? => do
-  match stx with
-  | `(($e : $type:term)) =>
+@[builtin_term_elab typeAscription] def elabTypeAscription : TermElab
+  | `(($e : $type)), _ => do
     let type ← withSynthesize (mayPostpone := true) <| elabType type
     let e ← elabTerm e type
     ensureHasType type e
-  | `(($e :)) =>
+  | `(($e :)), expectedType? => do
     let e ← withSynthesize (mayPostpone := false) <| elabTerm e none
     ensureHasType expectedType? e
-  | _ => throwUnsupportedSyntax
+  | _, _ => throwUnsupportedSyntax
 
 /-- Return `true` if `lhs` is a free variable and `rhs` does not depend on it. -/
 private def isSubstCandidate (lhs rhs : Expr) : MetaM Bool :=

src/Lean/Elab/PatternVar.lean

@@ -134,20 +134,11 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
     `(.( $stx ))
   else if k == ``Lean.Parser.Term.syntheticHole then
     `(.( $stx ))
-  else if k == ``Lean.Parser.Term.paren then
-    let arg := stx[1]
-    if arg.isNone then
-      return stx -- `()`
-    else
-      let t := arg[0]
-      let s := arg[1]
-      if s.isNone || s[0].getKind == ``Lean.Parser.Term.typeAscription then
-        -- Ignore `s`, since it empty or it is a type ascription
-        let t ← collect t
-        let arg := arg.setArg 0 t
-        return stx.setArg 1 arg
-      else
-        return stx
+  else if k == ``Lean.Parser.Term.typeAscription then
+    -- Ignore type term
+    let t := stx[1]
+    let t ← collect t
+    return stx.setArg 1 t
   else if k == ``Lean.Parser.Term.explicitUniv then
     processCtor stx[0]
   else if k == ``Lean.Parser.Term.namedPattern then

src/Lean/Elab/Quotation/Precheck.lean

@@ -116,16 +116,11 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
       | `(argument| $e:term)    => precheck e
   | _ => throwUnsupportedSyntax
 
-@[builtin_quot_precheck Lean.Parser.Term.paren] def precheckParen : Precheck
-  | `(())                => pure ()
-  | `(($e : $type:term)) => do
+@[builtin_quot_precheck Lean.Parser.Term.typeAscription] def precheckTypeAscription : Precheck
+  | `(($e : $type)) => do
     precheck e
     precheck type
-  | `(($e :))
-  | `(($e))              => precheck e
-  | `(($e, $es,*))       => do
-    precheck e
-    es.getElems.raw.forM precheck
+  | `(($e :)) => precheck e
   | _ => throwUnsupportedSyntax
 
 @[builtin_quot_precheck choice] def precheckChoice : Precheck := fun stx => do

src/Lean/Linter/UnusedVariables.lean

@@ -95,7 +95,7 @@ builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts =>
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts =>
   !getLinterUnusedVariablesFunArgs opts &&
   (stack.matches [`null, ``Lean.Parser.Term.basicFun] ||
-  stack.matches [`null, ``Lean.Parser.Term.paren, `null, ``Lean.Parser.Term.basicFun]))
+  stack.matches [``Lean.Parser.Term.typeAscription, `null, ``Lean.Parser.Term.basicFun]))
 
 -- is pattern variable
 builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts =>

src/Lean/Parser/Term.lean

@@ -129,11 +129,9 @@ For example, `(· + ·)` is equivalent to `fun x y => x + y`.
 @[builtin_term_parser] def cdot   := leading_parser
   symbol "·" <|> "."
 def typeAscription := leading_parser
-  " : " >> optional termParser
-def tupleTail      := leading_parser
-  ", " >> sepBy1 termParser ", "
-def parenSpecial : Parser :=
-  optional (tupleTail <|> typeAscription)
+  "(" >> withoutPosition (withoutForbidden (termParser >> " : " >> optional termParser)) >> ")"
+def tuple := leading_parser
+  "(" >> optional (withoutPosition (withoutForbidden (termParser >> ", " >> sepBy1 termParser ", "))) >> ")"
 /--
 Parentheses, used for
 - Grouping expressions, e.g., `a * (b + c)`.
@@ -149,8 +147,8 @@ Parentheses, used for
   - `(f · a b)` is shorthand for `fun x => f x a b`
   - `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`
 -/
-@[builtin_term_parser] def paren := leading_parser
-  "(" >> (withoutPosition (withoutForbidden (optional (ppDedentIfGrouped termParser >> parenSpecial)))) >> ")"
+@[builtin_term_parser] def paren := (leading_parser
+  atomic ("(" >> withoutPosition (withoutForbidden (ppDedentIfGrouped termParser)) >> ")")) <|> atomic typeAscription <|> tuple
 /--
 The *anonymous constructor* `⟨e, ...⟩` is equivalent to `c e ...` if the
 expected type is an inductive type with a single constructor `c`.

stage0/src/stdlib_flags.h

@@ -8,10 +8,10 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
-    opts = opts.update({"quotPrecheck"}, true);
+    opts = opts.update({"quotPrecheck"}, false);
 
     opts = opts.update({"pp", "rawOnError"}, true);
 #endif