From 2f4340f63cd9bdb0c9e773745edbe201d012b29d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 30 Aug 2020 16:14:38 -0700
Subject: [PATCH] feat: refine `refine` tactic

Now `refine stx` reports an error when there are natural unassigned
metavariables after we elaborate syntax `stx`. The idea is that only
synthetic holes `?<hole-name>` become new goals.
The tactic `refine! stx` implements the Lean3 behavior.
---
 src/Lean/Elab/Tactic/ElabTerm.lean | 26 ++++++++++++++++++++++++--
 src/Lean/MetavarContext.lean       |  4 ++++
 tests/lean/run/induction1.lean     |  2 +-
 tests/lean/run/newfrontend1.lean   |  8 ++++----
 4 files changed, 33 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index a55e481c20..7bce0c8d4b 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -40,13 +40,25 @@ fun stx => match_syntax stx with
     setGoals gs
   | _ => throwUnsupportedSyntax
 
-def refineCore (mvarId : MVarId) (stx : Syntax) (tagSuffix : Name) : TacticM (List MVarId) :=
+/- If `allowNaturalHoles == true`, then we allow the resultant expression to contain unassigned "natural" metavariables.
+   Recall that "natutal" metavariables are created for explicit holes `_` and implicit arguments. They are meant to be
+   filled by typing constraints.
+   "Synthetic" metavariables are meant to be filled by tactics and are usually created using the synthetic hole notation `?<hole-name>`. -/
+def refineCore (mvarId : MVarId) (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool := false) : TacticM (List MVarId) :=
 withMVarContext mvarId do
   decl ← getMVarDecl mvarId;
   val  ← elabTermEnsuringType stx decl.type;
   assignExprMVar mvarId val;
   newMVarIds ← getMVarsNoDelayed val;
-  let newMVarIds := newMVarIds.toList;
+  newMVarIds ←
+    if allowNaturalHoles then
+      pure newMVarIds.toList
+    else do {
+      naturalMVarIds ← newMVarIds.filterM fun mvarId => do { mvarDecl ← getMVarDecl mvarId; pure mvarDecl.kind.isNatural };
+      syntheticMVarIds ← newMVarIds.filterM fun mvarId => do { mvarDecl ← getMVarDecl mvarId; pure $ !mvarDecl.kind.isNatural };
+      liftM $ Term.logUnassignedUsingErrorContext naturalMVarIds;
+      pure syntheticMVarIds.toList
+    };
   tagUntaggedGoals decl.userName tagSuffix newMVarIds;
   pure newMVarIds
 
@@ -54,10 +66,20 @@ withMVarContext mvarId do
 fun stx => match_syntax stx with
   | `(tactic| refine $e) => do
     (g, gs) ← getMainGoal;
+    /- Remark: only synthetic holes become new goals (we are using `allowNaturalHoles == false`). -/
     gs' ← refineCore g e `refine;
     setGoals (gs' ++ gs)
   | _ => throwUnsupportedSyntax
 
+@[builtinTactic «refine!»] def evalRefineBang : Tactic :=
+fun stx => match_syntax stx with
+  | `(tactic| refine! $e) => do
+    (g, gs) ← getMainGoal;
+    /- Remark all unassigned metavariables become new goals. We consider delayed assignments as assignments here. -/
+    gs' ← refineCore g e `refine true;
+    setGoals (gs' ++ gs)
+  | _ => throwUnsupportedSyntax
+
 @[builtinTactic Lean.Parser.Tactic.apply] def evalApply : Tactic :=
 fun stx => match_syntax stx with
   | `(tactic| apply $e) => do
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 8e79128086..bd649c4fb8 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -244,6 +244,10 @@ def MetavarKind.isSyntheticOpaque : MetavarKind → Bool
 | MetavarKind.syntheticOpaque => true
 | _                           => false
 
+def MetavarKind.isNatural : MetavarKind → Bool
+| MetavarKind.natural => true
+| _                   => false
+
 structure MetavarDecl :=
 (userName       : Name := Name.anonymous)
 (lctx           : LocalContext)
diff --git a/tests/lean/run/induction1.lean b/tests/lean/run/induction1.lean
index d544b05c2f..fad857704f 100644
--- a/tests/lean/run/induction1.lean
+++ b/tests/lean/run/induction1.lean
@@ -45,7 +45,7 @@ theorem tst5 {p q : Prop } (h : p ∨ q) : q ∨ p :=
 by {
   induction h using elim2 with
   | right h => _
-  | left h  => { refine Or.inr _; exact h };
+  | left h  => { refine Or.inr ?_; exact h };
   case right { exact Or.inl h }
 }
 
diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index 1737758b08..cc3660d434 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -87,14 +87,14 @@ by {
 theorem simple6 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by {
   intro h1; intro _; intro h3;
-  refine Eq.trans _ h1;
+  refine Eq.trans ?_ h1;
   assumption
 }
 
 theorem simple7 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by {
   intro h1; intro _; intro h3;
-  refine Eq.trans ?pre ?post;
+  refine! Eq.trans ?pre ?post;
   exact y;
   { exact h3 };
   { exact h1 }
@@ -103,7 +103,7 @@ by {
 theorem simple8 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by {
   intro h1; intro _; intro h3;
-  refine Eq.trans ?pre ?post;
+  refine! Eq.trans ?pre ?post;
   case post { exact h1 };
   case pre { exact h3 };
 }
@@ -112,7 +112,7 @@ theorem simple9 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by {
   intros h1 _ h3;
   traceState;
-  { refine Eq.trans ?pre ?post;
+  { refine! Eq.trans ?pre ?post;
     (exact h1) <|> (exact y; exact h3; assumption) }
 }