From f73ff914eb44ee11b120d530e1f157cc4a765ee2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 10 Jan 2020 15:05:14 -0800
Subject: [PATCH] feat: extensible elaboration functions

@kha `termParserAttr.lean` has a small example
---
 src/Init/Lean/Elab/BuiltinNotation.lean |  18 ++--
 src/Init/Lean/Elab/Command.lean         |  48 ++++++-----
 src/Init/Lean/Elab/Definition.lean      |   2 +-
 src/Init/Lean/Elab/Exception.lean       |  13 ++-
 src/Init/Lean/Elab/Log.lean             |   4 +-
 src/Init/Lean/Elab/Term.lean            | 107 +++++++++++++-----------
 src/Init/Lean/Elab/TermApp.lean         |  19 +++--
 src/Init/Lean/Elab/TermBinders.lean     |   6 +-
 src/Init/Lean/Elab/Util.lean            |  11 ++-
 tests/lean/run/new_frontend2.lean       |   2 +
 tests/lean/run/termParserAttr.lean      |  18 +++-
 11 files changed, 148 insertions(+), 100 deletions(-)

diff --git a/src/Init/Lean/Elab/BuiltinNotation.lean b/src/Init/Lean/Elab/BuiltinNotation.lean
index e502678f04..9653dae75f 100644
--- a/src/Init/Lean/Elab/BuiltinNotation.lean
+++ b/src/Init/Lean/Elab/BuiltinNotation.lean
@@ -14,24 +14,24 @@ namespace Term
 @[builtinTermElab dollar] def elabDollar : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
 | `($f $ $a) => `($f $a)
-| _          => throwUnexpectedSyntax stx "application"
+| _          => throwUnsupportedSyntax
 
 @[builtinTermElab dollarProj] def elabDollarProj : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
 | `($term $.$field) => `($(term).$field)
-| _                 => throwUnexpectedSyntax stx "$."
+| _                 => throwUnsupportedSyntax
 
 @[builtinTermElab «if»] def elabIf : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
 | `(if $h : $cond then $t else $e) => let h := mkTermIdFromIdent h; `(dite $cond (fun $h => $t) (fun $h => $e))
 | `(if $cond then $t else $e)      => `(ite $cond $t $e)
-| _                                => throwUnexpectedSyntax stx "if-then-else"
+| _                                => throwUnsupportedSyntax
 
 @[builtinTermElab subtype] def elabSubtype : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
 | `({ $x : $type // $p }) => let x := mkTermIdFromIdent x; `(Subtype (fun ($x : $type) => $p))
 | `({ $x // $p })         => let x := mkTermIdFromIdent x; `(Subtype (fun ($x : _) => $p))
-| _                       => throwUnexpectedSyntax stx "subtype"
+| _                       => throwUnsupportedSyntax
 
 @[builtinTermElab anonymousCtor] def elabAnoymousCtor : TermElab :=
 fun stx expectedType? => do
@@ -59,7 +59,7 @@ match expectedType? with
 @[builtinTermElab «show»] def elabShow : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
 | `(show $type from $val) => let thisId := mkTermId stx `this; `((fun ($thisId : $type) => $thisId) $val)
-| _                       => throwUnexpectedSyntax stx "show-from"
+| _                       => throwUnsupportedSyntax
 
 @[builtinTermElab «have»] def elabHave : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
@@ -67,7 +67,7 @@ adaptExpander $ fun stx => match_syntax stx with
 | `(have $type := $val; $body)        => let thisId := mkTermId stx `this; `((fun ($thisId : $type) => $body) $val)
 | `(have $x : $type from $val; $body) => let x := mkTermIdFromIdent x; `((fun ($x : $type) => $body) $val)
 | `(have $x : $type := $val; $body)   => let x := mkTermIdFromIdent x; `((fun ($x : $type) => $body) $val)
-| _                                   => throwUnexpectedSyntax stx "have"
+| _                                   => throwUnsupportedSyntax
 
 @[termElab «where»] def elabWhere : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
@@ -76,7 +76,7 @@ adaptExpander $ fun stx => match_syntax stx with
   decls.foldrM
     (fun decl body => `(let $decl; $body))
     body
-| _                      => throwUnexpectedSyntax stx "where"
+| _                      => throwUnsupportedSyntax
 
 @[termElab «parser!»] def elabParserMacro : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
@@ -90,7 +90,7 @@ adaptExpander $ fun stx => match_syntax stx with
     `(HasOrelse.orelse (Lean.Parser.mkAntiquot $s (some $kind) true) (Lean.Parser.leadingNode $kind $e))
   | none          => throwError stx "invalid `parser!` macro, it must be used in definitions"
   | _             => throwError stx "invalid `parser!` macro, unexpected declaration name"
-| _             => throwUnexpectedSyntax stx "parser!"
+| _             => throwUnsupportedSyntax
 
 @[termElab «tparser!»] def elabTParserMacro : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
@@ -99,7 +99,7 @@ adaptExpander $ fun stx => match_syntax stx with
   match declName? with
   | some declName => let kind := quote declName; `(Lean.Parser.trailingNode $kind $e)
   | none          => throwError stx "invalid `tparser!` macro, it must be used in definitions"
-| _             => throwUnexpectedSyntax stx "tparser!"
+| _             => throwUnsupportedSyntax
 
 def elabInfix (f : Syntax) : TermElab :=
 fun stx expectedType? => do
diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean
index 3583f812f0..a92138c589 100644
--- a/src/Init/Lean/Elab/Command.lean
+++ b/src/Init/Lean/Elab/Command.lean
@@ -44,6 +44,8 @@ structure Context :=
 (macroStack     : List Syntax := [])
 (currMacroScope : MacroScope := 0)
 
+instance Exception.inhabited : Inhabited Exception := ⟨Exception.error $ arbitrary _⟩
+
 abbrev CommandElabCoreM (ε) := ReaderT Context (EIO ε)
 abbrev CommandElabM := CommandElabCoreM Exception
 abbrev CommandElab  := SyntaxNode → CommandElabM Unit
@@ -55,7 +57,7 @@ private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : M
 mkMessageAux ctx ref (toString err) MessageSeverity.error
 
 @[inline] def liftIOCore {α} (ctx : Context) (ref : Syntax) (x : IO α) : EIO Exception α :=
-EIO.adaptExcept (ioErrorToMessage ctx ref) x
+EIO.adaptExcept (fun ex => Exception.error $ ioErrorToMessage ctx ref ex) x
 
 @[inline] def liftIO {α} (ref : Syntax) (x : IO α) : CommandElabM α :=
 fun ctx => liftIOCore ctx ref x
@@ -121,13 +123,7 @@ def throwError {α} (ref : Syntax) (msgData : MessageData) : CommandElabM α :=
 ref ← getBetterRef ref;
 msgData ← addMacroStack msgData;
 msg ← mkMessage msgData MessageSeverity.error ref;
-throw msg
-
-def throwUnexpectedSyntax {α} (ref : Syntax) (expectedMsg : Option String := none) : CommandElabM α := do
-refFmt ← prettyPrint ref;
-match expectedMsg with
-| none    => throwError ref ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
-| some ex => throwError ref ("unexpected syntax, expected '" ++ ex ++ "'" ++ MessageData.nest 2 (Format.line ++ refFmt))
+throw (Exception.error msg)
 
 protected def getCurrMacroScope : CommandElabM Nat := do
 ctx ← read;
@@ -184,6 +180,15 @@ def mkCommandElabAttribute : IO CommandElabAttribute :=
 mkElabAttribute CommandElab `commandElab `Lean.Parser.Command `Lean.Elab.Command.CommandElab "command" builtinCommandElabTable
 @[init mkCommandElabAttribute] constant commandElabAttribute : CommandElabAttribute := arbitrary _
 
+private def elabCommandUsing (stxNode : SyntaxNode) : List CommandElab → CommandElabM Unit
+| []                => do
+  refFmt ← prettyPrint stxNode.val;
+  throwError stxNode.val ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
+| (elabFn::elabFns) => catch (elabFn stxNode)
+  (fun ex => match ex with
+    | Exception.error _           => throw ex
+    | Exception.unsupportedSyntax => elabCommandUsing elabFns)
+
 def elabCommand (stx : Syntax) : CommandElabM Unit :=
 stx.ifNode
   (fun n => do
@@ -191,8 +196,8 @@ stx.ifNode
     let table := (commandElabAttribute.ext.getState s.env).table;
     let k := n.getKind;
     match table.find? k with
-    | some elab => elab n
-    | none      => throwError stx ("command '" ++ toString k ++ "' has not been implemented"))
+    | some elabFns => elabCommandUsing n elabFns
+    | none         => throwError stx ("command '" ++ toString k ++ "' has not been implemented"))
   (fun _ => throwError stx ("unexpected command"))
 
 /- Elaborate `x` with `stx` on the macro stack -/
@@ -228,9 +233,10 @@ s.scopes.head!.varDecls
 
 private def toCommandResult {α} (ctx : Context) (s : State) (result : EStateM.Result Term.Exception Term.State α) : EStateM.Result Exception State α :=
 match result with
-| EStateM.Result.ok a newS                            => EStateM.Result.ok a { env := newS.env, messages := newS.messages, nextMacroScope := newS.nextMacroScope, .. s }
-| EStateM.Result.error (Term.Exception.error ex) newS => EStateM.Result.error ex { env := newS.env, messages := newS.messages, nextMacroScope := newS.nextMacroScope, .. s }
-| EStateM.Result.error Term.Exception.postpone newS   => unreachable!
+| EStateM.Result.ok a newS => EStateM.Result.ok a { env := newS.env, messages := newS.messages, nextMacroScope := newS.nextMacroScope, .. s }
+| EStateM.Result.error (Term.Exception.ex ex) newS =>
+  EStateM.Result.error ex { env := newS.env, messages := newS.messages, nextMacroScope := newS.nextMacroScope, .. s }
+| EStateM.Result.error Term.Exception.postpone newS          => unreachable!
 
 instance CommandElabM.inhabited {α} : Inhabited (CommandElabM α) :=
 ⟨throw $ arbitrary _⟩
@@ -239,12 +245,14 @@ instance CommandElabM.inhabited {α} : Inhabited (CommandElabM α) :=
 ctx ← read;
 s ← get;
 match (Term.elabBinders (getVarDecls s) elab (mkTermContext ctx s declName?)).run (mkTermState s) with
-| EStateM.Result.ok a newS                            => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; pure a
-| EStateM.Result.error (Term.Exception.error ex) newS => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; throw ex
-| EStateM.Result.error Term.Exception.postpone newS   => unreachable!
+| EStateM.Result.ok a newS                          => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; pure a
+| EStateM.Result.error (Term.Exception.ex ex) newS  => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; throw ex
+| EStateM.Result.error Term.Exception.postpone newS => unreachable!
 
 @[inline] def withLogging (x : CommandElabM Unit) : CommandElabM Unit :=
-catch x (fun ex => do logMessage ex; pure ())
+catch x (fun ex => match ex with
+  | Exception.error ex          => do logMessage ex; pure ()
+  | Exception.unsupportedSyntax => unreachable!)
 
 @[inline] def catchExceptions (x : CommandElabM Unit) : CommandElabCoreM Empty Unit :=
 fun ctx => EIO.catchExceptions (withLogging x ctx) (fun _ => pure ())
@@ -278,13 +286,13 @@ addScopes ref "namespace" true header
 @[builtinCommandElab «namespace»] def elabNamespace : CommandElab :=
 fun stx => match_syntax stx.val with
   | `(namespace $n) => addNamespace stx.val n.getId
-  | _               => throwUnexpectedSyntax stx.val "namespace"
+  | _               => throw Exception.unsupportedSyntax
 
 @[builtinCommandElab «section»] def elabSection : CommandElab :=
 fun stx => match_syntax stx.val with
   | `(section $header:ident) => addScopes stx.val "section" false header.getId
   | `(section)               => do currNamespace ← getCurrNamespace; addScope "section" "" currNamespace
-  | _                        => throwUnexpectedSyntax stx.val "section"
+  | _                        => throw Exception.unsupportedSyntax
 
 def getScopes : CommandElabM (List Scope) := do
 s ← get; pure s.scopes
@@ -373,7 +381,7 @@ currNamespace ← getCurrNamespace;
 openDecls ← getOpenDecls;
 match Elab.resolveNamespace env currNamespace openDecls id with
 | some ns => pure ns
-| none    => throwErrorUsingCmdPos ("unknown namespace '" ++ toString id ++ "'")
+| none    => throw Exception.unsupportedSyntax
 
 @[builtinCommandElab «export»] def elabExport : CommandElab :=
 fun stx => do
diff --git a/src/Init/Lean/Elab/Definition.lean b/src/Init/Lean/Elab/Definition.lean
index fab75a1d68..2cbfcc1814 100644
--- a/src/Init/Lean/Elab/Definition.lean
+++ b/src/Init/Lean/Elab/Definition.lean
@@ -123,7 +123,7 @@ if kind == `Lean.Parser.Command.declValSimple then
 else if kind == `Lean.Parser.Command.declValEqns then
   Term.throwError defVal "equations have not been implemented yet"
 else
-  Term.throwUnexpectedSyntax defVal "definition body"
+  Term.throwUnsupportedSyntax
 
 def elabDefLike (view : DefView) : CommandElabM Unit :=
 let ref := view.ref;
diff --git a/src/Init/Lean/Elab/Exception.lean b/src/Init/Lean/Elab/Exception.lean
index 3bcc81f81d..37654a4dd3 100644
--- a/src/Init/Lean/Elab/Exception.lean
+++ b/src/Init/Lean/Elab/Exception.lean
@@ -9,7 +9,16 @@ import Init.Lean.Meta
 namespace Lean
 namespace Elab
 
-abbrev Exception := Message
+inductive Exception
+| error             : Message → Exception
+| unsupportedSyntax : Exception
+
+instance Exception.inhabited : Inhabited Exception := ⟨Exception.error $ arbitrary _⟩
+
+instance Exception.hasToString : HasToString Exception :=
+⟨fun ex => match ex with
+ | Exception.error msg         => toString msg
+ | Exception.unsupportedSyntax => "unsupported syntax"⟩
 
 def mkMessageCore (fileName : String) (fileMap : FileMap) (msgData : MessageData) (severity : MessageSeverity) (pos : String.Pos) : Message :=
 let pos := fileMap.toPosition pos;
@@ -17,7 +26,7 @@ let pos := fileMap.toPosition pos;
 
 def mkExceptionCore (fileName : String) (fileMap : FileMap) (msgData : MessageData) (pos : String.Pos) : Exception :=
 let pos := fileMap.toPosition pos;
-{ fileName := fileName, pos := pos, data := msgData, severity := MessageSeverity.error }
+Exception.error { fileName := fileName, pos := pos, data := msgData, severity := MessageSeverity.error }
 
 end Elab
 end Lean
diff --git a/src/Init/Lean/Elab/Log.lean b/src/Init/Lean/Elab/Log.lean
index e536923f06..f6cbe1159d 100644
--- a/src/Init/Lean/Elab/Log.lean
+++ b/src/Init/Lean/Elab/Log.lean
@@ -68,12 +68,12 @@ def logInfo [MonadLog m] (stx : Syntax) (msgData : MessageData) : m Unit :=
 log stx MessageSeverity.information msgData
 
 def throwError {α} [MonadPosInfo m] [MonadExcept Exception m] (ref : Syntax) (msgData : MessageData) : m α := do
-msg ← mkMessage msgData MessageSeverity.error ref; throw msg
+msg ← mkMessage msgData MessageSeverity.error ref; throw (Exception.error msg)
 
 def throwErrorUsingCmdPos {α} [MonadPosInfo m] [MonadExcept Exception m] (msgData : MessageData) : m α := do
 cmdPos ← getCmdPos;
 msg ← mkMessageAt msgData MessageSeverity.error cmdPos;
-throw msg
+throw (Exception.error msg)
 
 end Elab
 end Lean
diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 0cc076a3ef..72eb99cff7 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -61,12 +61,12 @@ instance State.inhabited : Inhabited State := ⟨{ env := arbitrary _ }⟩
 
   Remark: `Exception.postpone` is used only when `mayPostpone == true` in the `Context`. -/
 inductive Exception
-| error    : Elab.Exception → Exception
+| ex       : Elab.Exception → Exception
 | postpone : Exception
 
 instance Exception.inhabited : Inhabited Exception := ⟨Exception.postpone⟩
 instance Exception.hasToString : HasToString Exception :=
-⟨fun ex => match ex with | Exception.postpone => "postponed" | Exception.error ex => toString ex⟩
+⟨fun ex => match ex with | Exception.postpone => "postponed" | Exception.ex ex => toString ex⟩
 
 /-
   Term elaborator Monad. In principle, we could track statically which methods
@@ -79,7 +79,7 @@ abbrev TermElab  := SyntaxNode → Option Expr → TermElabM Expr
 instance TermElabM.inhabited {α} : Inhabited (TermElabM α) :=
 ⟨throw $ Exception.postpone⟩
 
-abbrev TermElabResult := EStateM.Result Elab.Exception State Expr
+abbrev TermElabResult := EStateM.Result Message State Expr
 instance TermElabResult.inhabited : Inhabited TermElabResult := ⟨EStateM.Result.ok (arbitrary _) (arbitrary _)⟩
 
 /--
@@ -89,17 +89,17 @@ instance TermElabResult.inhabited : Inhabited TermElabResult := ⟨EStateM.Resul
 @[inline] def observing (x : TermElabM Expr) : TermElabM TermElabResult :=
 fun ctx s =>
   match x ctx s with
-  | EStateM.Result.error Exception.postpone newS   => EStateM.Result.error Exception.postpone newS
-  | EStateM.Result.error (Exception.error ex) newS => EStateM.Result.ok (EStateM.Result.error ex newS) s
-  | EStateM.Result.ok e newS                       => EStateM.Result.ok (EStateM.Result.ok e newS) s
+  | EStateM.Result.error (Exception.ex (Elab.Exception.error errMsg)) newS => EStateM.Result.ok (EStateM.Result.error errMsg newS) s
+  | EStateM.Result.error ex newS                                           => EStateM.Result.error ex newS
+  | EStateM.Result.ok e newS                                               => EStateM.Result.ok (EStateM.Result.ok e newS) s
 
 /--
   Apply the result/exception and state captured with `observing`.
   We use this method to implement overloaded notation and symbols. -/
 def applyResult (result : TermElabResult) : TermElabM Expr :=
 match result with
-| EStateM.Result.ok e s     => do set s; pure e
-| EStateM.Result.error ex s => do set s; throw (Exception.error ex)
+| EStateM.Result.ok e s         => do set s; pure e
+| EStateM.Result.error errMsg s => do set s; throw (Exception.ex (Elab.Exception.error errMsg))
 
 def getEnv : TermElabM Environment := do s ← get; pure s.env
 def getMCtx : TermElabM MetavarContext := do s ← get; pure s.mctx
@@ -150,13 +150,10 @@ def throwError {α} (ref : Syntax) (msgData : MessageData) : TermElabM α := do
 ref ← getBetterRef ref;
 msgData ← addMacroStack msgData;
 msg ← mkMessage msgData MessageSeverity.error ref;
-throw (Exception.error msg)
+throw (Exception.ex (Elab.Exception.error msg))
 
-def throwUnexpectedSyntax {α} (ref : Syntax) (expectedMsg : Option String := none) : TermElabM α := do
-refFmt ← prettyPrint ref;
-match expectedMsg with
-| none    => throwError ref ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
-| some ex => throwError ref ("unexpected syntax, expected '" ++ ex ++ "'" ++ MessageData.nest 2 (Format.line ++ refFmt))
+def throwUnsupportedSyntax {α} : TermElabM α :=
+throw (Exception.ex Elab.Exception.unsupportedSyntax)
 
 protected def getCurrMacroScope : TermElabM MacroScope := do
 ctx ← read;
@@ -259,7 +256,7 @@ mkMessageCore ctx.fileName ctx.fileMap msgData severity (ref.getPos.getD ctx.cmd
 
 /-- Auxiliary function for `liftMetaM` -/
 private def fromMetaException (ctx : Context) (ref : Syntax) (ex : Meta.Exception) : Exception :=
-Exception.error $ mkMessageAux ctx ref ex.toMessageData MessageSeverity.error
+Exception.ex $ Elab.Exception.error $ mkMessageAux ctx ref ex.toMessageData MessageSeverity.error
 
 /-- Auxiliary function for `liftMetaM` -/
 private def fromMetaState (ref : Syntax) (ctx : Context) (s : State) (newS : Meta.State) (oldTraceState : TraceState) : State :=
@@ -310,7 +307,7 @@ def liftLevelM {α} (x : LevelElabM α) : TermElabM α :=
 fun ctx s =>
   match (x { .. ctx }).run { .. s } with
   | EStateM.Result.ok a newS     => EStateM.Result.ok a { mctx := newS.mctx, ngen := newS.ngen, .. s }
-  | EStateM.Result.error ex newS => EStateM.Result.error (Exception.error ex) s
+  | EStateM.Result.error ex newS => EStateM.Result.error (Exception.ex ex) s
 
 def elabLevel (stx : Syntax) : TermElabM Level :=
 liftLevelM $ Level.elabLevel stx
@@ -445,14 +442,14 @@ def expandCDot? : Syntax → TermElabM (Option Syntax)
     pure none
 | _ => pure none
 
-private def exceptionToSorry (ref : Syntax) (ex : Elab.Exception) (expectedType? : Option Expr) : TermElabM Expr := do
+private def exceptionToSorry (ref : Syntax) (errMsg : Message) (expectedType? : Option Expr) : TermElabM Expr := do
 expectedType : Expr ← match expectedType? with
   | none              => mkFreshTypeMVar ref
   | some expectedType => pure expectedType;
 u ← getLevel ref expectedType;
 -- TODO: should be `(sorryAx.{$u} $expectedType true) when we support antiquotations at that place
 let syntheticSorry := mkApp2 (mkConst `sorryAx [u]) expectedType (mkConst `Bool.true);
-unless ex.data.hasSyntheticSorry $ logMessage ex;
+unless errMsg.data.hasSyntheticSorry $ logMessage errMsg;
 pure syntheticSorry
 
 /-- If `mayPostpone == true`, throw `Expection.postpone`. -/
@@ -476,6 +473,39 @@ ctx ← read;
 registerSyntheticMVar stx mvar.mvarId! (SyntheticMVarKind.postponed ctx.macroStack);
 pure mvar
 
+/-
+  Helper function for `elabTerm` is tries the registered elaboration functions for `stxNode` kind until it finds one that supports the syntax or
+  an error is found. -/
+private def elabTermUsing (s : State) (stxNode : SyntaxNode) (expectedType? : Option Expr) (errToSorry : Bool) (catchExPostpone : Bool)
+    : List TermElab → TermElabM Expr
+| []                => do
+  refFmt ← prettyPrint stxNode.val;
+  throwError stxNode.val ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
+| (elabFn::elabFns) => catch (elabFn stxNode expectedType?)
+  (fun ex => match ex with
+    | Exception.ex (Elab.Exception.error errMsg)    => if errToSorry then exceptionToSorry stxNode.val errMsg expectedType? else throw ex
+    | Exception.ex Elab.Exception.unsupportedSyntax => elabTermUsing elabFns
+    | Exception.postpone          =>
+      if catchExPostpone then do
+        /- If `elab` threw `Exception.postpone`, we reset any state modifications.
+           For example, we want to make sure pending synthetic metavariables created by `elab` before
+           it threw `Exception.postpone` are discarded.
+           Note that we are also discarding the messages created by `elab`.
+
+           For example, consider the expression.
+           `((f.x a1).x a2).x a3`
+           Now, suppose the elaboration of `f.x a1` produces an `Exception.postpone`.
+           Then, a new metavariable `?m` is created. Then, `?m.x a2` also throws `Exception.postpone`
+           because the type of `?m` is not yet known. Then another, metavariable `?n` is created, and
+          finally `?n.x a3` also throws `Exception.postpone`. If we did not restore the state, we would
+          keep "dead" metavariables `?m` and `?n` on the pending synthetic metavariable list. This is
+          wasteful because when we resume the elaboration of `((f.x a1).x a2).x a3`, we start it from scratch
+          and new metavariables are created for the nested functions. -/
+          set s;
+          postponeElabTerm stxNode.val expectedType?
+        else
+          throw ex)
+
 /--
   Main function for elaborating terms.
   It extracts the elaboration methods from the environment using the node kind.
@@ -496,32 +526,8 @@ withFreshMacroScope $ withNode stx $ fun node => do
   let table := (termElabAttribute.ext.getState s.env).table;
   let k := node.getKind;
   match table.find? k with
-  | some elab =>
-    catch
-      (elab node expectedType?)
-      (fun ex => match ex with
-        | Exception.error err => if errToSorry then exceptionToSorry stx err expectedType? else throw ex
-        | Exception.postpone =>
-          if catchExPostpone then do
-            /- If `elab` threw `Exception.postpone`, we reset any state modifications.
-               For example, we want to make sure pending synthetic metavariables created by `elab` before
-               it threw `Exception.postpone` are discarded.
-               Note that we are also discarding the messages created by `elab`.
-
-               For example, consider the expression.
-               `((f.x a1).x a2).x a3`
-               Now, suppose the elaboration of `f.x a1` produces an `Exception.postpone`.
-               Then, a new metavariable `?m` is created. Then, `?m.x a2` also throws `Exception.postpone`
-               because the type of `?m` is not yet known. Then another, metavariable `?n` is created, and
-               finally `?n.x a3` also throws `Exception.postpone`. If we did not restore the state, we would
-               keep "dead" metavariables `?m` and `?n` on the pending synthetic metavariable list. This is
-               wasteful because when we resume the elaboration of `((f.x a1).x a2).x a3`, we start it from scratch
-               and new metavariables are created for the nested functions. -/
-            set s;
-            postponeElabTerm stx expectedType?
-          else
-            throw ex)
-  | none      => throwError stx ("elaboration function for '" ++ toString k ++ "' has not been implemented")
+  | some elabFns => elabTermUsing s node expectedType? errToSorry catchExPostpone elabFns
+  | none         => throwError stx ("elaboration function for '" ++ toString k ++ "' has not been implemented")
 
 /-- Auxiliary function used to implement `synthesizeSyntheticMVars`. -/
 private def resumeElabTerm (stx : Syntax) (expectedType? : Option Expr) (errToSorry := true) : TermElabM Expr :=
@@ -594,8 +600,13 @@ withMVarContext mvarId $ do
       assignExprMVar mvarId result;
       pure true)
     (fun ex => match ex with
-      | Exception.postpone  => pure false
-      | Exception.error msg => if postponeOnError then do set s; pure false else do logMessage msg; pure true)
+      | Exception.postpone                            => pure false
+      | Exception.ex Elab.Exception.unsupportedSyntax => unreachable!
+      | Exception.ex (Elab.Exception.error msg)       =>
+        if postponeOnError then do
+          set s; pure false
+        else do
+          logMessage msg; pure true)
 
 /- Try to synthesize metavariable using type class resolution.
    This method assumes the local context and local instances of `instMVar` coincide
@@ -629,8 +640,8 @@ private def synthesizePendingInstMVar (ref : Syntax) (instMVar : MVarId) : TermE
 withMVarContext instMVar $ catch
   (synthesizeInstMVarCore ref instMVar)
   (fun ex => match ex with
-    | Exception.error ex => do logMessage ex; pure true
-    | Exception.postpone => unreachable!)
+    | Exception.ex (Elab.Exception.error errMsg) => do logMessage errMsg; pure true
+    | _ => unreachable!)
 
 /--
   Return `true` iff `mvarId` is assigned to a term whose the
diff --git a/src/Init/Lean/Elab/TermApp.lean b/src/Init/Lean/Elab/TermApp.lean
index f10162ca0b..0eea83c389 100644
--- a/src/Init/Lean/Elab/TermApp.lean
+++ b/src/Init/Lean/Elab/TermApp.lean
@@ -189,22 +189,23 @@ match eType.getAppFn, lval with
 | _, _ =>
   throwLValError ref e eType "invalid field notation, type is not of the form (C ...) where C is a constant"
 
-private partial def resolveLValLoop (ref : Syntax) (e : Expr) (lval : LVal) : Expr → Array Elab.Exception → TermElabM LValResolution
+private partial def resolveLValLoop (ref : Syntax) (e : Expr) (lval : LVal) : Expr → Array Message → TermElabM LValResolution
 | eType, previousExceptions => do
   eType ← whnfCore ref eType;
   tryPostponeIfMVar eType;
   catch (resolveLValAux ref e eType lval)
     (fun ex =>
       match ex with
-      | Exception.postpone => throw ex
-      | Exception.error ex => do
+      | Exception.postpone                            => throw ex
+      | Exception.ex Elab.Exception.unsupportedSyntax => throw ex
+      | Exception.ex (Elab.Exception.error errMsg)    => do
         eType? ← unfoldDefinition? ref eType;
         match eType? with
-        | some eType => resolveLValLoop eType (previousExceptions.push ex)
+        | some eType => resolveLValLoop eType (previousExceptions.push errMsg)
         | none       => do
           previousExceptions.forM $ fun ex =>
-            logMessage ex;
-          throw (Exception.error ex))
+            logMessage errMsg;
+          throw (Exception.ex (Elab.Exception.error errMsg)))
 
 private def resolveLVal (ref : Syntax) (e : Expr) (lval : LVal) : TermElabM LValResolution := do
 eType ← inferType ref e;
@@ -331,7 +332,7 @@ private partial def elabAppFn (ref : Syntax) : Syntax → List LVal → Array Na
           s ← observing $ elabAppLVals ref f (lvals' ++ lvals) namedArgs args expectedType? explicit;
           pure $ acc.push s)
         acc
-    | _ => throwUnexpectedSyntax id "identifier"
+    | _ => throwUnsupportedSyntax
   | _ => do
     f ← elabTerm f none;
     s ← observing $ elabAppLVals ref f lvals namedArgs args expectedType? explicit;
@@ -353,8 +354,8 @@ else
 private def mergeFailures {α} (failures : Array TermElabResult) (stx : Syntax) : TermElabM α := do
 msgs ← failures.mapM $ fun failure =>
   match failure with
-  | EStateM.Result.ok _ _     => unreachable!
-  | EStateM.Result.error ex s => toMessageData ex stx;
+  | EStateM.Result.ok _ _         => unreachable!
+  | EStateM.Result.error errMsg s => toMessageData errMsg stx;
 throwError stx ("overloaded, errors " ++ MessageData.ofArray msgs)
 
 private def elabAppAux (ref : Syntax) (f : Syntax) (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) : TermElabM Expr := do
diff --git a/src/Init/Lean/Elab/TermBinders.lean b/src/Init/Lean/Elab/TermBinders.lean
index edd6279a3e..d24ddd3fd6 100644
--- a/src/Init/Lean/Elab/TermBinders.lean
+++ b/src/Init/Lean/Elab/TermBinders.lean
@@ -53,7 +53,7 @@ else
   else if kind == `Lean.Parser.Term.binderTactic then do
     throwError modifier "not implemented yet"
   else
-    throwUnexpectedSyntax modifier "default argument or tactic name"
+    throwUnsupportedSyntax
 
 private def matchBinder (stx : Syntax) : TermElabM (Array BinderView) :=
 withNode stx $ fun node => do
@@ -143,12 +143,12 @@ fun stx _ => match_syntax stx.val with
   elabBinders binders $ fun xs => do
     e ← elabType term;
     mkForall stx.val xs e
-| _ => throwUnexpectedSyntax stx.val "forall"
+| _ => throwUnsupportedSyntax
 
 @[builtinTermElab arrow] def elabArrow : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
 | `($dom:term -> $rng) => `(forall (a : $dom), $rng)
-| _                    => throwUnexpectedSyntax stx "->"
+| _                    => throwUnsupportedSyntax
 
 @[builtinTermElab depArrow] def elabDepArrow : TermElab :=
 fun stx _ =>
diff --git a/src/Init/Lean/Elab/Util.lean b/src/Init/Lean/Elab/Util.lean
index 661004f48b..910238afa6 100644
--- a/src/Init/Lean/Elab/Util.lean
+++ b/src/Init/Lean/Elab/Util.lean
@@ -37,7 +37,12 @@ structure ElabAttributeOLeanEntry :=
 structure ElabAttributeEntry (γ : Type) extends ElabAttributeOLeanEntry :=
 (elabFn   : γ)
 
-abbrev ElabFnTable (γ : Type) := SMap SyntaxNodeKind γ
+abbrev ElabFnTable (γ : Type) := SMap SyntaxNodeKind (List γ)
+
+def ElabFnTable.insert {γ} (table : ElabFnTable γ) (k : SyntaxNodeKind) (f : γ) : ElabFnTable γ :=
+match table.find? k with
+| some fs => table.insert k (f::fs)
+| none    => table.insert k [f]
 
 structure ElabAttributeExtensionState (γ : Type) :=
 (newEntries : List ElabAttributeOLeanEntry := [])
@@ -75,8 +80,8 @@ match env.find? constName with
 @[implementedBy mkElabFnOfConstantUnsafe]
 constant mkElabFnOfConstant (γ : Type) (env : Environment) (typeName : Name) (constName : Name) : ExceptT String Id γ := throw ""
 
-private def ElabAttribute.addImportedParsers {γ} (typeName : Name) (builtinTableRef : IO.Ref (ElabFnTable γ)) (env : Environment) (es : Array (Array ElabAttributeOLeanEntry))
-    : IO (ElabAttributeExtensionState γ) := do
+private def ElabAttribute.addImportedParsers {γ} (typeName : Name) (builtinTableRef : IO.Ref (ElabFnTable γ))
+    (env : Environment) (es : Array (Array ElabAttributeOLeanEntry)) : IO (ElabAttributeExtensionState γ) := do
 table ← builtinTableRef.get;
 table ← es.foldlM
   (fun table entries =>
diff --git a/tests/lean/run/new_frontend2.lean b/tests/lean/run/new_frontend2.lean
index 45ba4a9c74..6f6e4b00f5 100644
--- a/tests/lean/run/new_frontend2.lean
+++ b/tests/lean/run/new_frontend2.lean
@@ -3,6 +3,8 @@ new_frontend
 variable {m : Type → Type}
 variable [s : Functor m]
 
+#check @Nat.rec
+
 #check s.map
 
 /-
diff --git a/tests/lean/run/termParserAttr.lean b/tests/lean/run/termParserAttr.lean
index b6342aba1f..a5a8b59b0d 100644
--- a/tests/lean/run/termParserAttr.lean
+++ b/tests/lean/run/termParserAttr.lean
@@ -12,7 +12,7 @@ do env  ← MetaIO.getEnv;
    pure ()
 
 open Lean.Parser
-@[termParser] def tst := parser! "(|" >> termParser >> "|)"
+@[termParser] def tst := parser! "(|" >> termParser >> optional (", " >> termParser) >> "|)"
 
 @[termParser] def boo : ParserDescr :=
 ParserDescr.node `boo
@@ -25,8 +25,9 @@ ParserDescr.node `boo
 open Lean.Elab.Term
 
 @[termElab tst] def elabTst : TermElab :=
-fun stx expected? =>
-  elabTerm (stx.getArg 1) expected?
+adaptExpander $ fun stx => match_syntax stx with
+ | `((| $e |)) => pure e
+ | _           => throwUnsupportedSyntax
 
 @[termElab boo] def elabBoo : TermElab :=
 fun stx expected? =>
@@ -34,3 +35,14 @@ fun stx expected? =>
 
 #eval run "#check [| @id.{1} Nat |]"
 #eval run "#check (| id 1 |)"
+-- #eval run "#check (| id 1, id 1 |)" -- it will fail
+
+@[termElab tst] def elabTst2 : TermElab :=
+adaptExpander $ fun stx => match_syntax stx with
+ | `((| $e1, $e2 |)) => `(($e1, $e2))
+ | _                 => throwUnsupportedSyntax
+
+-- Now both work
+
+#eval run "#check (| id 1 |)"
+#eval run "#check (| id 1, id 2 |)"