diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean index ab0fa565b2..c7a76c02c5 100644 --- a/src/Lean/Meta/Tactic/Apply.lean +++ b/src/Lean/Meta/Tactic/Apply.lean @@ -61,19 +61,38 @@ private def dependsOnOthers (mvar : Expr) (otherMVars : Array Expr) : MetaM Bool let otherMVarType ← inferType otherMVar return (otherMVarType.findMVar? fun mvarId => mvarId == mvar.mvarId!).isSome -private def reorderNonDependentFirst (newMVars : Array Expr) : MetaM (List MVarId) := do - let (nonDeps, deps) ← newMVars.foldlM (init := (#[], #[])) fun (nonDeps, deps) mvar => do +/-- Partitions the given mvars in to two arrays (non-deps, deps) +according to whether the given mvar depends on other mvars in the array.-/ +private def partitionDependentMVars (mvars : Array Expr) : MetaM $ Prod (Array MVarId) (Array MVarId) := + mvars.foldlM (init := (#[], #[])) fun (nonDeps, deps) mvar => do let currMVarId := mvar.mvarId! - if (← dependsOnOthers mvar newMVars) then + if (← dependsOnOthers mvar mvars) then pure (nonDeps, deps.push currMVarId) else pure (nonDeps.push currMVarId, deps) - return nonDeps.toList ++ deps.toList +/-- Controls which new mvars are turned in to goals by the `apply` tactic. +- `nonDependentFirst` mvars that don't depend on other goals appear first in the goal list. +- `nonDependentOnly` only mvars that don't depend on other goals are added to goal list. +- `all` all unassigned mvars are added to the goal list. +-/ inductive ApplyNewGoals where | nonDependentFirst | nonDependentOnly | all -def apply (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := +private def reorderGoals (mvars : Array Expr) : ApplyNewGoals → MetaM (List MVarId) + | ApplyNewGoals.nonDependentFirst => do + let (nonDeps, deps) ← partitionDependentMVars mvars + return nonDeps.toList ++ deps.toList + | ApplyNewGoals.nonDependentOnly => do + let (nonDeps, deps) ← partitionDependentMVars mvars + return nonDeps.toList + | ApplyNewGoals.all => pure $ Array.toList $ mvars.map Lean.Expr.mvarId! + +/-- Configures the behaviour of the `apply` tactic. -/ +structure ApplyConfig := + (newGoals := ApplyNewGoals.nonDependentFirst) + +def apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := withMVarContext mvarId do checkNotAssigned mvarId `apply let targetType ← getMVarType mvarId @@ -89,8 +108,7 @@ def apply (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := assignExprMVar mvarId (mkAppN e newMVars) let newMVars ← newMVars.filterM fun mvar => not <$> isExprMVarAssigned mvar.mvarId! let otherMVarIds ← getMVarsNoDelayed e - -- TODO: add option `ApplyNewGoals` and implement other orders - let newMVarIds ← reorderNonDependentFirst newMVars + let newMVarIds ← reorderGoals newMVars cfg.newGoals let otherMVarIds := otherMVarIds.filter fun mvarId => !newMVarIds.contains mvarId let result := newMVarIds ++ otherMVarIds.toList result.forM headBetaMVarType diff --git a/tests/lean/run/apply_tac.lean b/tests/lean/run/apply_tac.lean new file mode 100644 index 0000000000..a1f9ccc100 --- /dev/null +++ b/tests/lean/run/apply_tac.lean @@ -0,0 +1,33 @@ +import Lean +open Lean +open Lean.Elab +open Lean.Meta +open Lean.Elab.Tactic + +example (a b c : Nat) (h₁ : a = b) (h₂ : b = c) : a = c := by + apply Eq.trans _ h₂ -- the metavars created during elaboration become new goals + trace_state + exact h₁ + +example (a : Nat) : ∃ x, x = a := by + apply Exists.intro -- the goal for the witness should occur "after" the goal for x = a + trace_state + rfl + +elab "fapply " e:term : tactic => + evalApplyLikeTactic (Meta.apply (cfg := {newGoals := ApplyNewGoals.all})) e + +elab "eapply " e:term : tactic => + evalApplyLikeTactic (Meta.apply (cfg := {newGoals := ApplyNewGoals.nonDependentOnly})) e + +example (a : Nat) : ∃ x, x = a := by + eapply Exists.intro -- only metavars with out forward dependencies are added as goals. + trace_state + rfl + +example (a : Nat) : ∃ x, x = a := by + fapply Exists.intro -- all unassigned metavars are added as new goals using the order they were created. + trace_state + exact a + trace_state + rfl diff --git a/tests/lean/run/apply_tac.lean.expected.out b/tests/lean/run/apply_tac.lean.expected.out new file mode 100644 index 0000000000..6b736c9c21 --- /dev/null +++ b/tests/lean/run/apply_tac.lean.expected.out @@ -0,0 +1,24 @@ +a b c : Nat +h₁ : a = b +h₂ : b = c +⊢ a = b +case h +a : Nat +⊢ ?w = a + +case w +a : Nat +⊢ Nat +case h +a : Nat +⊢ ?w = a +case w +a : Nat +⊢ Nat + +case h +a : Nat +⊢ ?w = a +case h +a : Nat +⊢ a = a