refactor: paren as a (partial) macro

src/Lean/Elab/BuiltinNotation.lean

@@ -165,49 +165,35 @@ private partial def hasCDot : Syntax → Bool
     else args.any hasCDot
   | _ => false
 
-/--
-  Auxiliary function for expandind the `·` notation.
-  The extra state `Array Syntax` contains the new binder names.
-  If `stx` is a `·`, we create a fresh identifier, store in the
-  extra state, and return it. Otherwise, we just return `stx`. -/
-private partial def expandCDot : Syntax → StateT (Array Syntax) MacroM Syntax
-  | stx@(Syntax.node k args) =>
-    if k == `Lean.Parser.Term.paren then pure stx
-    else if k == `Lean.Parser.Term.cdot then withFreshMacroScope do
-      let id ← `(a)
-      modify fun s => s.push id;
-      pure id
-    else do
-      let args ← args.mapM expandCDot
-      pure $ Syntax.node k args
-  | stx => pure stx
-
 /--
   Return `some` if succeeded expanding `·` notation occurring in
   the given syntax. Otherwise, return `none`.
   Examples:
   - `· + 1` => `fun _a_1 => _a_1 + 1`
   - `f · · b` => `fun _a_1 _a_2 => f _a_1 _a_2 b` -/
-def expandCDot? (stx : Syntax) : MacroM (Option Syntax) := do
+partial def expandCDot? (stx : Syntax) : MacroM (Option Syntax) := do
   if hasCDot stx then
-    let (newStx, binders) ← (expandCDot stx).run #[];
+    let (newStx, binders) ← (go stx).run #[];
     `(fun $binders* => $newStx)
   else
     pure none
-
-/--
-  Try to expand `·` notation, and if successful elaborate result.
-  This method is used to elaborate the Lean parentheses notation.
-  Recall that in Lean the `·` notation must be surrounded by parentheses.
-  We may change this is the future, but right now, here are valid examples
-  - `(· + 1)`
-  - `(f ⟨·, 1⟩ ·)`
-  - `(· + ·)`
-  - `(f · a b)` -/
-private def elabCDot (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
-  match (← liftMacroM <| expandCDot? stx) with
-  | some stx' => withMacroExpansion stx stx' (elabTerm stx' expectedType?)
-  | none      => elabTerm stx expectedType?
+where
+  /--
+    Auxiliary function for expanding the `·` notation.
+    The extra state `Array Syntax` contains the new binder names.
+    If `stx` is a `·`, we create a fresh identifier, store in the
+    extra state, and return it. Otherwise, we just return `stx`. -/
+  go : Syntax → StateT (Array Syntax) MacroM Syntax
+    | stx@(Syntax.node k args) =>
+      if k == `Lean.Parser.Term.paren then pure stx
+      else if k == `Lean.Parser.Term.cdot then withFreshMacroScope do
+        let id ← `(a)
+        modify fun s => s.push id;
+        pure id
+      else do
+        let args ← args.mapM go
+        pure $ Syntax.node k args
+    | stx => pure stx
 
 /--
   Helper method for elaborating terms such as `(.+.)` where a constant name is expected.
@@ -230,18 +216,33 @@ where
     | _ => Term.expandCDot? stx
 
 
+/--
+  Try to expand `·` notation.
+  Recall that in Lean the `·` notation must be surrounded by parentheses.
+  We may change this is the future, but right now, here are valid examples
+  - `(· + 1)`
+  - `(f ⟨·, 1⟩ ·)`
+  - `(· + ·)`
+  - `(f · a b)` -/
+@[builtinMacro Lean.Parser.Term.paren] def expandParen : Macro
+  | `(())           => `(Unit.unit)
+  | `(($e : $type)) => do
+    match ← expandCDot? e with
+    | some e => `(($e : $type))
+    | none   => Macro.throwUnsupported
+  | `(($e))         => do return (← expandCDot? e).getD e
+  | `(($e, $es,*))  => do
+    let pairs ← mkPairs (#[e] ++ es)
+    (← expandCDot? pairs).getD pairs
+  | stx => throw <| Macro.Exception.error stx "unexpected parentheses notation"
+
 @[builtinTermElab paren] def elabParen : TermElab := fun stx expectedType? => do
   match stx with
-  | `(())           => return Lean.mkConst `Unit.unit
   | `(($e : $type)) =>
-    let type ← withSynthesize (mayPostpone := true) $ elabType type
-    let e ← elabCDot e type
+    let type ← withSynthesize (mayPostpone := true) <| elabType type
+    let e ← elabTerm e expectedType?
     ensureHasType type e
-  | `(($e))         => elabCDot e expectedType?
-  | `(($e, $es,*))  =>
-    let pairs ← liftMacroM <| mkPairs (#[e] ++ es)
-    withMacroExpansion stx pairs (elabCDot pairs expectedType?)
-  | _ => throwError "unexpected parentheses notation"
+  | _ => throwUnsupportedSyntax
 
 @[builtinTermElab subst] def elabSubst : TermElab := fun stx expectedType? => do
   let expectedType ← tryPostponeIfHasMVars expectedType? "invalid `▸` notation"