From 655da9baefbee5460d0cc0d96eaf5ed847905d24 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 19 Jan 2020 09:04:25 -0800
Subject: [PATCH] fix: tag `refine` subgoals

---
 src/Init/Lean/Elab/Tactic/Basic.lean    | 20 ++++++++++++++++++++
 src/Init/Lean/Elab/Tactic/ElabTerm.lean |  4 +++-
 src/Init/Lean/MetavarContext.lean       | 10 ++++++++++
 3 files changed, 33 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Elab/Tactic/Basic.lean b/src/Init/Lean/Elab/Tactic/Basic.lean
index db54ad5602..11368e64ae 100644
--- a/src/Init/Lean/Elab/Tactic/Basic.lean
+++ b/src/Init/Lean/Elab/Tactic/Basic.lean
@@ -59,6 +59,7 @@ def liftMetaM {α} (ref : Syntax) (x : MetaM α) : TacticM α := liftTermElabM $
 
 def getEnv : TacticM Environment := do s ← get; pure s.env
 def getMCtx : TacticM MetavarContext := do s ← get; pure s.mctx
+@[inline] def modifyMCtx (f : MetavarContext → MetavarContext) : TacticM Unit := modify $ fun s => { mctx := f s.mctx, .. s }
 def getLCtx : TacticM LocalContext := do ctx ← read; pure ctx.lctx
 def getLocalInsts : TacticM LocalInstances := do ctx ← read; pure ctx.localInstances
 def getOptions : TacticM Options := do ctx ← read; pure ctx.config.opts
@@ -237,6 +238,25 @@ done ref;
 setGoals gs;
 pure a
 
+/--
+  Use `parentTag` to tag untagged goals at `newGoals`.
+  If there are multiple new goals, they are named using `<parentTag>.<newSuffix>_<idx>` where `idx > 0`.
+  If there is only one new goal, then we just use `parentTag` -/
+def tagUntaggedGoals (parentTag : Name) (newSuffix : Name) (newGoals : List MVarId) : TacticM Unit := do
+mctx ← getMCtx;
+match newGoals with
+| [g] => modifyMCtx $ fun mctx => if mctx.isAnonymousMVar g then mctx.renameMVar g parentTag else mctx
+| _   => modifyMCtx $ fun mctx =>
+  let (mctx, _) := newGoals.foldl
+    (fun (acc : MetavarContext × Nat) (g : MVarId) =>
+       let (mctx, idx) := acc;
+       if mctx.isAnonymousMVar g then
+         (mctx.renameMVar g (parentTag ++ newSuffix.appendIndexAfter idx), idx+1)
+       else
+         acc)
+    (mctx, 1);
+  mctx
+
 @[builtinTactic seq] def evalSeq : Tactic :=
 fun stx => (stx.getArg 0).forSepArgsM evalTactic
 
diff --git a/src/Init/Lean/Elab/Tactic/ElabTerm.lean b/src/Init/Lean/Elab/Tactic/ElabTerm.lean
index f03e5fbc77..5a8d58b6bb 100644
--- a/src/Init/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Init/Lean/Elab/Tactic/ElabTerm.lean
@@ -44,7 +44,9 @@ fun stx => match_syntax stx with
       val  ← elabTerm e decl.type;
       val  ← ensureHasType ref decl.type val;
       assignExprMVar g val;
-      collectMVars ref val
+      gs'  ← collectMVars ref val;
+      tagUntaggedGoals decl.userName `refine gs';
+      pure gs'
     };
     setGoals (gs' ++ gs)
   | _ => throwUnsupportedSyntax
diff --git a/src/Init/Lean/MetavarContext.lean b/src/Init/Lean/MetavarContext.lean
index c6d35a4aa9..e0121ca659 100644
--- a/src/Init/Lean/MetavarContext.lean
+++ b/src/Init/Lean/MetavarContext.lean
@@ -332,6 +332,16 @@ match mctx.findLevelDepth? mvarId with
 | some d => d
 | none   => panic! "unknown metavariable"
 
+def isAnonymousMVar (mctx : MetavarContext) (mvarId : MVarId) : Bool :=
+match mctx.findDecl? mvarId with
+| none          => false
+| some mvarDecl => mvarDecl.userName.isAnonymous
+
+def renameMVar (mctx : MetavarContext) (mvarId : MVarId) (newUserName : Name) : MetavarContext :=
+match mctx.findDecl? mvarId with
+| none          => panic! "unknown metavariable"
+| some mvarDecl => { decls := mctx.decls.insert mvarId { userName := newUserName, .. mvarDecl }, .. mctx }
+
 @[export lean_metavar_ctx_assign_level]
 def assignLevel (m : MetavarContext) (mvarId : MVarId) (val : Level) : MetavarContext :=
 { lAssignment := m.lAssignment.insert mvarId val, .. m }