From 2ca96cb2b0bcc4dc52ac7197e8473049eceefc29 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 1 Jan 2020 15:19:04 -0800
Subject: [PATCH] feat: include macroStack in error messages

---
 src/Init/Lean/Elab/Term.lean  | 23 +++++++++++++++++++++++
 tests/lean/run/frontend1.lean |  1 +
 2 files changed, 24 insertions(+)

diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 4ec0acb9ea..60b1056cd2 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -106,10 +106,33 @@ instance TermElabM.MonadLog : MonadLog TermElabM :=
   getFileName := do ctx ← read; pure ctx.fileName,
   logMessage  := fun msg => modify $ fun s => { messages := s.messages.add msg, .. s } }
 
+/- If `ref` does not have position information, then try to use macroStack -/
+private def getBetterRef (ref : Syntax) : TermElabM Syntax :=
+match ref.getPos with
+| some _ => pure ref
+| none   => do
+  ctx ← read;
+  match ctx.macroStack.find? $ fun (macro : Syntax) => macro.getPos != none with
+  | some macro => pure macro
+  | none       => pure ref
+
+private def addMacroStack (msgData : MessageData) : TermElabM MessageData := do
+ctx ← read;
+if ctx.macroStack.isEmpty then pure msgData
+else
+  pure $ ctx.macroStack.foldl
+    (fun (msgData : MessageData) (macro : Syntax) =>
+      match macro.reprint with -- TODO use pretty printer
+      | some str => msgData ++ Format.line ++ "while expanding" ++ MessageData.nest 2 (Format.line ++ str)
+      | none     => msgData ++ Format.line ++ "while expanding macro")
+    msgData
+
 /--
   Throws an error with the given `msgData` and extracting position information from `ref`.
   If `ref` does not contain position information, then use `cmdPos` -/
 def throwError {α} (ref : Syntax) (msgData : MessageData) : TermElabM α := do
+ref ← getBetterRef ref;
+msgData ← addMacroStack msgData;
 msg ← mkMessage msgData MessageSeverity.error ref;
 throw (Exception.error msg)
 
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index ab667d33a6..fc8cca9165 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -176,3 +176,4 @@ f a
 #eval run "universes u v #check Sort (max u v)"
 #eval run "universes u v #check Type (max u v)"
 #eval run "#check 'a'"
+#eval fail "#check #['a', \"hello\"]"