From a7efe5b60e86b26fefd4795b46d66af369b97329 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 30 Aug 2023 18:00:30 +1000 Subject: [PATCH] Revert "fix: make sure `refine` preserves pre-existing natural mvars (#2435)" (#2485) This reverts commit 0b64c1e3301f04b7b36fed76ee1593962f6c34e5. --- src/Lean/Elab/Tactic/ElabTerm.lean | 14 +++-- tests/lean/refinePreservesNaturalMVars.lean | 53 ------------------- ...inePreservesNaturalMVars.lean.expected.out | 14 ----- 3 files changed, 6 insertions(+), 75 deletions(-) delete mode 100644 tests/lean/refinePreservesNaturalMVars.lean delete mode 100644 tests/lean/refinePreservesNaturalMVars.lean.expected.out diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index f8d23ff549..dce00625b0 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/src/Lean/Elab/Tactic/ElabTerm.lean @@ -124,23 +124,21 @@ where let newMVarIds ← getMVarsNoDelayed val /- ignore let-rec auxiliary variables, they are synthesized automatically later -/ let newMVarIds ← newMVarIds.filterM fun mvarId => return !(← Term.isLetRecAuxMVar mvarId) - /- The following `unless … do` block guards against unassigned natural mvarids created during - `k` in the case that `allowNaturalHoles := false`. If we pass this block without aborting, we - can be assured that `newMVarIds` does not contain unassigned natural mvars created during `k`. - Note that in all cases we must allow `newMVarIds` to contain unassigned natural mvars which - were created *before* `k`; this is the purpose of `mvarCounterSaved`, which lets us distinguish - mvars created before `k` from those created during and after. See issue #2434. -/ - unless allowNaturalHoles do + let newMVarIds ← if allowNaturalHoles then + pure newMVarIds.toList + else let naturalMVarIds ← newMVarIds.filterM fun mvarId => return (← mvarId.getKind).isNatural + let syntheticMVarIds ← newMVarIds.filterM fun mvarId => return !(← mvarId.getKind).isNatural let naturalMVarIds ← filterOldMVars naturalMVarIds mvarCounterSaved logUnassignedAndAbort naturalMVarIds + pure syntheticMVarIds.toList /- We sort the new metavariable ids by index to ensure the new goals are ordered using the order the metavariables have been created. See issue #1682. Potential problem: if elaboration of subterms is delayed the order the new metavariables are created may not match the order they appear in the `.lean` file. We should tell users to prefer tagged goals. -/ - let newMVarIds ← sortMVarIdsByIndex newMVarIds.toList + let newMVarIds ← sortMVarIdsByIndex newMVarIds tagUntaggedGoals (← getMainTag) tagSuffix newMVarIds return (val, newMVarIds) diff --git a/tests/lean/refinePreservesNaturalMVars.lean b/tests/lean/refinePreservesNaturalMVars.lean deleted file mode 100644 index 952656e504..0000000000 --- a/tests/lean/refinePreservesNaturalMVars.lean +++ /dev/null @@ -1,53 +0,0 @@ -import Lean - -/-! Ensures that `refine` does not remove pre-existing natural goals from the goal list. -/ - -open Lean Meta Elab Tactic Term - -elab "add_natural_goal" s:ident " : " t:term : tactic => do - let g ← mkFreshExprMVar (← elabType t) .natural s.getId - appendGoals [g.mvarId!] - -/-! - -In the following, `refine` would erroneously close each focused goal, leading to a -`(kernel) declaration has metavariables '_example'` error. - -This occurred because `withCollectingNewGoalsFrom` was only erroring on new natural goals (as -determined by `index`), while simultaneously only passing through non-natural goals to construct -the resulting goal list. This orphaned old natural metavariables and closed the goal list -erroneously. - -As such, all of the following tests should lead to an `unsolved goals` error, followed by a -`no goals` error (instead of a successful focus). - --/ - -example : Bool × Nat := by - add_natural_goal d : Bool - add_natural_goal e : Nat - · refine (?d,?e) - · refine ?d - · refine ?e - -example : Bool × Bool := by - add_natural_goal d : Bool - add_natural_goal e : Bool - · refine (?d,?e) - · case d => refine ?e - · refine ?e - -/-! - -Previously, this would error, as `refine (?d, ?e)` erroneously closed the goal, leading to a -`no goals` error. Instead, this should succeed. - --/ - -example : Bool × Bool := by - add_natural_goal d : Bool - add_natural_goal e : Bool - · refine (?d,?e) - refine ?d - refine ?e -- This unifies `?d` and `?e`, so only one goal remains. - exact true diff --git a/tests/lean/refinePreservesNaturalMVars.lean.expected.out b/tests/lean/refinePreservesNaturalMVars.lean.expected.out deleted file mode 100644 index 4090434dc5..0000000000 --- a/tests/lean/refinePreservesNaturalMVars.lean.expected.out +++ /dev/null @@ -1,14 +0,0 @@ -refinePreservesNaturalMVars.lean:29:2-29:3: error: unsolved goals -case d -⊢ Bool - -case e -⊢ Nat -refinePreservesNaturalMVars.lean:30:2-30:3: error: no goals to be solved -refinePreservesNaturalMVars.lean:36:2-36:3: error: unsolved goals -case d -⊢ Bool - -case e -⊢ Bool -refinePreservesNaturalMVars.lean:37:2-37:3: error: no goals to be solved