From 6e4fcaaea9939bcc8cfab5540f3f6ccc8a89c75c Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 9 Nov 2021 19:00:33 +0100
Subject: [PATCH] fix: produce info tree even on macro or elab failure

---
 src/Lean/Elab/Command.lean            |  9 +++++----
 src/Lean/Elab/Term.lean               |  2 +-
 src/Lean/Elab/Util.lean               | 10 +++++-----
 tests/lean/infoTree.lean              |  1 +
 tests/lean/infoTree.lean.expected.out |  2 ++
 5 files changed, 14 insertions(+), 10 deletions(-)

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index a87e7a6c90..8f64396055 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -216,7 +216,7 @@ private def mkInfoTree (elaborator : Name) (stx : Syntax) (trees : Std.Persisten
   } tree
 
 private def elabCommandUsing (s : State) (stx : Syntax) : List (KeyedDeclsAttribute.AttributeEntry CommandElab) → CommandElabM Unit
-  | []                => throwError "unexpected syntax{indentD stx}"
+  | []                => withInfoTreeContext (mkInfoTree := mkInfoTree `no_elab stx) <| throwError "unexpected syntax{indentD stx}"
   | (elabFn::elabFns) =>
     catchInternalId unsupportedSyntaxExceptionId
       (withInfoTreeContext (mkInfoTree := mkInfoTree elabFn.declName stx) <| elabFn.value stx)
@@ -267,10 +267,11 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
         trace `Elab.command fun _ => stx;
         let s ← get
         match (← liftMacroM <| expandMacroImpl? s.env stx) with
-        | some (decl, stxNew) =>
+        | some (decl, stxNew?) =>
           withInfoTreeContext (mkInfoTree := mkInfoTree decl stx) do
-              withMacroExpansion stx stxNew do
-                elabCommand stxNew
+            let stxNew ← liftMacroM <| liftExcept stxNew?
+            withMacroExpansion stx stxNew do
+              elabCommand stxNew
         | _ =>
           match commandElabAttribute.getEntries s.env k with
           | []      => throwError "elaboration function for '{k}' has not been implemented"
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index e97ad934a0..afce91fdd3 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1248,7 +1248,7 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone :
     withNestedTraces do
     let env ← getEnv
     match (← liftMacroM (expandMacroImpl? env stx)) with
-    | some (decl, stxNew) =>
+    | some (decl, Except.ok stxNew) =>
       withInfoContext' (mkInfo := mkTermInfo decl (expectedType? := expectedType?) stx) <|
         withMacroExpansion stx stxNew <|
           withRef stxNew <|
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index d3be2bbbda..04b1e3737f 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -115,14 +115,14 @@ builtin_initialize macroAttribute : KeyedDeclsAttribute Macro ← mkMacroAttribu
 Try to expand macro at syntax tree root and return macro declaration name and new syntax if successful.
 Return none if all macros threw `Macro.Exception.unsupportedSyntax`.
 -/
-def expandMacroImpl? (env : Environment) : Syntax → MacroM (Option (Name × Syntax)) := fun stx => do
+def expandMacroImpl? (env : Environment) : Syntax → MacroM (Option (Name × Except Macro.Exception Syntax)) := fun stx => do
   for e in macroAttribute.getEntries env stx.getKind do
     try
       let stx' ← withFreshMacroScope (e.value stx)
-      return (e.declName, stx')
+      return (e.declName, Except.ok stx')
     catch
       | Macro.Exception.unsupportedSyntax => pure ()
-      | ex                                => throw ex
+      | ex                                => return (e.declName, Except.error ex)
   return none
 
 class MonadMacroAdapter (m : Type → Type) where
@@ -144,8 +144,8 @@ def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEn
     -- TODO: record recursive expansions in info tree?
     expandMacro?     := fun stx => do
       match (← expandMacroImpl? env stx) with
-      | some (_, stx) => some stx
-      | none          => none
+      | some (_, Except.ok stx) => some stx
+      | _                       => none
     hasDecl          := fun declName => return env.contains declName
     getCurrNamespace := return currNamespace
     resolveNamespace? := fun n => return ResolveName.resolveNamespace? env currNamespace openDecls n
diff --git a/tests/lean/infoTree.lean b/tests/lean/infoTree.lean
index dd8e415458..1898931c50 100644
--- a/tests/lean/infoTree.lean
+++ b/tests/lean/infoTree.lean
@@ -36,3 +36,4 @@ def f5 (x : Nat) : B := {
 
 open Nat in
 #print xor
+instance : Inhabited Nat where
diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out
index 635945d2a9..5c388f56ef 100644
--- a/tests/lean/infoTree.lean.expected.out
+++ b/tests/lean/infoTree.lean.expected.out
@@ -318,3 +318,5 @@ bitwise bne
   command @ ⟨38, 0⟩-⟨38, 10⟩ @ Lean.Elab.Command.elabPrint
     xor : Nat → Nat → Nat @ ⟨38, 7⟩-⟨38, 10⟩
   command @ ⟨37, 0⟩†-⟨38, 10⟩† @ Lean.Elab.Command.elabEnd
+infoTree.lean:40:0: error: unexpected end of input; expected identifier
+[Elab.info] command @ ⟨39, 0⟩-⟨39, 30⟩ @ no_elab