From e654909f7a7c2dfd34ebfd03e0649ee7ea237bfd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 16 Jan 2020 18:21:11 -0800
Subject: [PATCH] feat: add `Exception.tactic`

---
 src/Init/Lean/Meta/Exception.lean         | 3 +++
 src/Init/Lean/Meta/Message.lean           | 1 +
 src/Init/Lean/Meta/Tactic/Assumption.lean | 4 ++--
 src/Init/Lean/Meta/Tactic/Intro.lean      | 4 ++--
 src/Init/Lean/Meta/Tactic/Util.lean       | 8 +++++---
 5 files changed, 13 insertions(+), 7 deletions(-)

diff --git a/src/Init/Lean/Meta/Exception.lean b/src/Init/Lean/Meta/Exception.lean
index 09c3a158ad..f473950e9b 100644
--- a/src/Init/Lean/Meta/Exception.lean
+++ b/src/Init/Lean/Meta/Exception.lean
@@ -35,6 +35,7 @@ inductive Exception
 | notInstance          (e : Expr) (ctx : ExceptionContext)
 | appBuilder           (op : Name) (msg : String) (args : Array Expr) (ctx : ExceptionContext)
 | synthInstance        (inst : Expr) (ctx : ExceptionContext)
+| tactic               (tacticName : Name) (mvarId : MVarId) (msg : MessageData) (ctx : ExceptionContext)
 | bug                  (b : Bug) (ctx : ExceptionContext)
 | other                (msg : String)
 
@@ -61,6 +62,7 @@ def toStr : Exception → String
 | notInstance _ _               => "type class instance expected"
 | appBuilder _ _ _ _            => "application builder failure"
 | synthInstance _ _             => "type class instance synthesis failed"
+| tactic tacName _ _ _          => "tactic '" ++ toString tacName ++ "' failed"
 | bug _ _                       => "bug"
 | other s                       => s
 
@@ -89,6 +91,7 @@ def toTraceMessageData : Exception → MessageData
 | notInstance i ctx               => mkCtx ctx $ `notInstance ++ " " ++ i
 | appBuilder op msg args ctx      => mkCtx ctx $ `appBuilder ++ " " ++ op ++ " " ++ args ++ " " ++ msg
 | synthInstance inst ctx          => mkCtx ctx $ `synthInstance ++ " " ++ inst
+| tactic tacName msg _ ctx        => mkCtx ctx $ `tacticFailure ++ " " ++ tacName ++ " " ++ msg
 | bug _ _                         => "internal bug" -- TODO improve
 | other s                         => s
 
diff --git a/src/Init/Lean/Meta/Message.lean b/src/Init/Lean/Meta/Message.lean
index 28acd506db..c13fa2005f 100644
--- a/src/Init/Lean/Meta/Message.lean
+++ b/src/Init/Lean/Meta/Message.lean
@@ -78,6 +78,7 @@ def toMessageData : Exception → MessageData
 | notInstance i ctx               => mkCtx ctx $ "not a type class instance " ++ i
 | appBuilder op msg args ctx      => mkCtx ctx $ "application builder failure " ++ op ++ " " ++ args ++ " " ++ msg
 | synthInstance inst ctx          => mkCtx ctx $ "failed to synthesize" ++ indentExpr inst
+| tactic tacName mvarId msg ctx   => "tactic '" ++ tacName ++ "' failed " ++ msg
 | bug _ _                         => "internal bug" -- TODO improve
 | other s                         => s
 
diff --git a/src/Init/Lean/Meta/Tactic/Assumption.lean b/src/Init/Lean/Meta/Tactic/Assumption.lean
index 8159efcc9f..d874b4415e 100644
--- a/src/Init/Lean/Meta/Tactic/Assumption.lean
+++ b/src/Init/Lean/Meta/Tactic/Assumption.lean
@@ -12,7 +12,7 @@ namespace Meta
 
 def assumptionAux (mvarId : MVarId) : MetaM Bool :=
 withMVarContext mvarId $ do
-  checkNotAssigned mvarId "assumption";
+  checkNotAssigned mvarId `assumption;
   mvarType ← getMVarType mvarId;
   lctx ← getLCtx;
   h? ← lctx.findDeclRevM? $ fun decl => condM (isDefEq mvarType decl.type) (pure (some decl.toExpr)) (pure none);
@@ -21,7 +21,7 @@ withMVarContext mvarId $ do
   | none   => pure false
 
 def assumption (mvarId : MVarId) : MetaM Unit :=
-unlessM (assumptionAux mvarId) $ throw $ Exception.other "`assumption` failed"
+unlessM (assumptionAux mvarId) $ throwTacticEx `assumption mvarId ""
 
 end Meta
 end Lean
diff --git a/src/Init/Lean/Meta/Tactic/Intro.lean b/src/Init/Lean/Meta/Tactic/Intro.lean
index 19d957e5eb..683b6d088f 100644
--- a/src/Init/Lean/Meta/Tactic/Intro.lean
+++ b/src/Init/Lean/Meta/Tactic/Intro.lean
@@ -45,11 +45,11 @@ def introNCoreAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name → σ
       if newType.isForall then
         introNCoreAux i lctx fvars fvars.size s newType
       else
-        throw $ Exception.other "`introN` failed, insufficient number of binders"
+        throwTacticEx `introN mvarId "insufficient number of binders"
 
 @[specialize] def introNCore {σ} (mvarId : MVarId) (n : Nat) (mkName : LocalContext → Name → σ → Name × σ) (s : σ) : MetaM (Array Expr × MVarId) :=
 withMVarContext mvarId $ do
-  checkNotAssigned mvarId "introN";
+  checkNotAssigned mvarId `introN;
   mvarType ← getMVarType mvarId;
   lctx ← getLCtx;
   introNCoreAux mvarId mkName n lctx #[] 0 s mvarType
diff --git a/src/Init/Lean/Meta/Tactic/Util.lean b/src/Init/Lean/Meta/Tactic/Util.lean
index 28fdc19694..98fd6b899f 100644
--- a/src/Init/Lean/Meta/Tactic/Util.lean
+++ b/src/Init/Lean/Meta/Tactic/Util.lean
@@ -12,9 +12,11 @@ namespace Meta
 def mkFreshExprSyntheticOpaqueMVar (type : Expr) (userName : Name := Name.anonymous) : MetaM Expr :=
 mkFreshExprMVar type userName MetavarKind.syntheticOpaque
 
-def checkNotAssigned (mvarId : MVarId) (tacticName : String) : MetaM Unit :=
-whenM (isExprMVarAssigned mvarId) $
-  throw $ Exception.other ("`" ++ tacticName ++ "` failed, metavariable has already been assigned")
+def throwTacticEx {α} (tacticName : Name) (mvarId : MVarId) (msg : MessageData) : MetaM α := do
+throwEx $ fun ctx => Exception.tactic tacticName mvarId (MessageData.withContext ctx msg) ctx
+
+def checkNotAssigned (mvarId : MVarId) (tacticName : Name) : MetaM Unit :=
+whenM (isExprMVarAssigned mvarId) $ throwTacticEx tacticName mvarId "metavariable has already been assigned"
 
 def getMVarType (mvarId : MVarId) : MetaM Expr := do
 mvarDecl ← getMVarDecl mvarId;