diff --git a/Aesop/BuiltinRules/ApplyHyps.lean b/Aesop/BuiltinRules/ApplyHyps.lean index e4e7496..673452e 100644 --- a/Aesop/BuiltinRules/ApplyHyps.lean +++ b/Aesop/BuiltinRules/ApplyHyps.lean @@ -13,9 +13,14 @@ open Lean.Meta def applyHyp (hyp : FVarId) (goal : MVarId) (md : TransparencyMode) : MetaM RuleApplication := do - let (_, #[step]) ← applyS goal (.fvar hyp) none md |>.run + let (goals, #[step]) ← applyS goal (.fvar hyp) none md |>.run | throwError "aesop: internal error in applyHyps: multiple steps" - return .ofLazyScriptStep step none + return { + goals := goals.map ({ mvarId := ·, diff := ∅ }) + postState := step.postState + scriptSteps? := #[step] + successProbability? := none + } @[aesop unsafe 75% tactic (rule_sets := [builtin])] def applyHyps : RuleTac := λ input => diff --git a/Aesop/BuiltinRules/Assumption.lean b/Aesop/BuiltinRules/Assumption.lean index a2c836c..36a548e 100644 --- a/Aesop/BuiltinRules/Assumption.lean +++ b/Aesop/BuiltinRules/Assumption.lean @@ -44,7 +44,12 @@ def assumption : RuleTac := λ input => do let #[step] := steps | throwError "aesop: internal error in assumption: multiple steps" let proofHasMVar := (← fvarId.getType).hasMVar - let app := RuleApplication.ofLazyScriptStep step none + let app := { + goals := #[] + postState := step.postState + scriptSteps? := #[step] + successProbability? := none + } return some (app, proofHasMVar) end Aesop.BuiltinRules diff --git a/Aesop/BuiltinRules/DestructProducts.lean b/Aesop/BuiltinRules/DestructProducts.lean index 871fd56..3a7b7ca 100644 --- a/Aesop/BuiltinRules/DestructProducts.lean +++ b/Aesop/BuiltinRules/DestructProducts.lean @@ -120,6 +120,9 @@ where partial def destructProducts : RuleTac := RuleTac.ofSingleRuleTac λ input => do let md := input.options.destructProductsTransparency let (goal, steps) ← destructProductsCore input.goal md + -- TODO we can construct a better diff here, and it would be important to do + -- so because `destructProducts` often renames hypotheses. + let goal := { mvarId := goal, diff := ← diffGoals input.goal goal ∅ } return (#[goal], steps, none) end Aesop.BuiltinRules diff --git a/Aesop/BuiltinRules/Ext.lean b/Aesop/BuiltinRules/Ext.lean index c9a47fb..970dd06 100644 --- a/Aesop/BuiltinRules/Ext.lean +++ b/Aesop/BuiltinRules/Ext.lean @@ -22,6 +22,7 @@ def extCore (goal : MVarId) : ScriptM (Option (Array MVarId)) := def ext : RuleTac := RuleTac.ofSingleRuleTac λ input => do let (some goals, steps) ← extCore input.goal |>.run | throwError "found no applicable ext lemma" + let goals ← goals.mapM (mvarIdToSubgoal (parentMVarId := input.goal) · ∅) return (goals, steps, none) end Aesop.BuiltinRules diff --git a/Aesop/BuiltinRules/Intros.lean b/Aesop/BuiltinRules/Intros.lean index 2e361fa..ee117b4 100644 --- a/Aesop/BuiltinRules/Intros.lean +++ b/Aesop/BuiltinRules/Intros.lean @@ -20,6 +20,9 @@ def intros : RuleTac := RuleTac.ofSingleRuleTac λ input => do | some md => introsUnfoldingS input.goal md |>.run if newFVarIds.size == 0 then throwError "nothing to introduce" - return (#[goal], steps, none) + let addedFVars := newFVarIds.foldl (init := ∅) λ set fvarId => + set.insert fvarId + let diff := { addedFVars, removedFVars := ∅, fvarSubst := ∅ } + return (#[{ mvarId := goal, diff }], steps, none) end Aesop.BuiltinRules diff --git a/Aesop/BuiltinRules/Split.lean b/Aesop/BuiltinRules/Split.lean index 83e4757..26b1c0d 100644 --- a/Aesop/BuiltinRules/Split.lean +++ b/Aesop/BuiltinRules/Split.lean @@ -15,6 +15,7 @@ namespace Aesop.BuiltinRules def splitTarget : RuleTac := RuleTac.ofSingleRuleTac λ input => do let (some goals, steps) ← splitTargetS? input.goal |>.run | throwError "nothing to split in target" + let goals ← goals.mapM (mvarIdToSubgoal input.goal · ∅) return (goals, steps, none) partial def splitHypothesesCore (goal : MVarId) : @@ -34,6 +35,7 @@ partial def splitHypothesesCore (goal : MVarId) : def splitHypotheses : RuleTac := RuleTac.ofSingleRuleTac λ input => do let (some goals, steps) ← splitHypothesesCore input.goal |>.run | throwError "no splittable hypothesis found" + let goals ← goals.mapM (mvarIdToSubgoal input.goal · ∅) return (goals, steps, none) end Aesop.BuiltinRules diff --git a/Aesop/BuiltinRules/Subst.lean b/Aesop/BuiltinRules/Subst.lean index 3e00192..c32bd87 100644 --- a/Aesop/BuiltinRules/Subst.lean +++ b/Aesop/BuiltinRules/Subst.lean @@ -90,6 +90,9 @@ def subst : RuleTac := RuleTac.ofSingleRuleTac λ input => | _ => throwError "unexpected index match location" let (some goal, steps) ← substFVars input.goal hyps |>.run | throwError "no suitable hypothesis found" + -- TODO we can construct a better diff here, and doing so would be important + -- since `subst` often renames fvars. + let goal ← mvarIdToSubgoal input.goal goal ∅ return (#[goal], steps, none) end Aesop.BuiltinRules diff --git a/Aesop/RuleTac/Apply.lean b/Aesop/RuleTac/Apply.lean index f6bf00a..b9850d7 100644 --- a/Aesop/RuleTac/Apply.lean +++ b/Aesop/RuleTac/Apply.lean @@ -23,9 +23,15 @@ def applyExpr' (goal : MVarId) (e : Expr) (eStx : Term) pat.specializeRule patInst e else pure e - let (_, #[step]) ← applyS goal e eStx md |>.run + let (goals, #[step]) ← applyS goal e eStx md |>.run | throwError "aesop: internal error in applyExpr': multiple steps" - return .ofLazyScriptStep step none + let goals := goals.map λ mvarId => { mvarId, diff := ∅ } + return { + goals + postState := step.postState + scriptSteps? := #[step] + successProbability? := none + } def applyExpr (goal : MVarId) (e : Expr) (eStx : Term) (pat? : Option RulePattern) (patInsts : HashSet RulePatternInstantiation) diff --git a/Aesop/RuleTac/Basic.lean b/Aesop/RuleTac/Basic.lean index 4169ca9..6325e39 100644 --- a/Aesop/RuleTac/Basic.lean +++ b/Aesop/RuleTac/Basic.lean @@ -7,6 +7,8 @@ Authors: Jannis Limperg import Aesop.Index.Basic import Aesop.Options import Aesop.Percent +import Aesop.RuleTac.GoalDiff +import Aesop.RuleTac.FVarIdSubst import Aesop.Script.CtorNames import Aesop.Script.Step import Batteries.Lean.Meta.SavedState @@ -20,6 +22,8 @@ namespace Aesop /-! # Rule Tactic Types -/ +-- TODO put docs on the structure fields instead of the structures + /-- Input for a rule tactic. Contains: @@ -45,6 +49,23 @@ structure RuleTacInput where options : Options' deriving Inhabited +/-- A subgoal produced by a rule. -/ +structure Subgoal where + /-- The goal mvar. -/ + mvarId : MVarId + /-- + A diff between the goal the rule was run on and this goal. Many `MetaM` + tactics report information that allows you to easily construct a `GoalDiff`. + If you don't have access to such information, use `diffGoals`, but note that + it may not give optimal results. + -/ + diff : GoalDiff + deriving Inhabited + +def mvarIdToSubgoal (parentMVarId mvarId : MVarId) (fvarSubst : FVarIdSubst) : + MetaM Subgoal := + return { mvarId, diff := ← diffGoals parentMVarId mvarId fvarSubst } + /-- A single rule application, representing the application of a tactic to the input goal. Must accurately report the following information: @@ -59,27 +80,23 @@ goal. Must accurately report the following information: `none`, we use the success probability of the applied rule. -/ structure RuleApplication where - goals : Array MVarId + goals : Array Subgoal postState : Meta.SavedState scriptSteps? : Option (Array Script.LazyStep) successProbability? : Option Percent namespace RuleApplication -def check (r : RuleApplication) : MetaM (Option MessageData) := +def check (r : RuleApplication) (input : RuleTacInput) : + MetaM (Option MessageData) := r.postState.runMetaM' do for goal in r.goals do - if ← goal.isAssignedOrDelayedAssigned then - return some m!"subgoal metavariable {goal.name} is already assigned." + if ← goal.mvarId.isAssignedOrDelayedAssigned then + return some m!"subgoal metavariable ?{goal.mvarId.name} is already assigned." + if let some err ← goal.diff.check input.goal goal.mvarId then + return some err return none -def ofLazyScriptStep (step : Script.LazyStep) - (successProbability? : Option Percent) : RuleApplication where - goals := step.postGoals - postState := step.postState - scriptSteps? := #[step] - successProbability? := successProbability? - end RuleApplication /-- @@ -102,7 +119,7 @@ A `RuleTac` which generates only a single `RuleApplication`. -/ def SingleRuleTac := RuleTacInput → - MetaM (Array MVarId × Option (Array Script.LazyStep) × Option Percent) + MetaM (Array Subgoal × Option (Array Script.LazyStep) × Option Percent) @[inline] def SingleRuleTac.toRuleTac (t : SingleRuleTac) : RuleTac := λ input => do @@ -125,6 +142,7 @@ def RuleTac.ofTacticSyntax (t : RuleTacInput → MetaM Syntax.Tactic) : RuleTac tacticBuilders := #[return .unstructured stx] preState, postState, postGoals } + let postGoals ← postGoals.mapM (mvarIdToSubgoal input.goal · ∅) return (postGoals, some #[step], none) /-- diff --git a/Aesop/RuleTac/Cases.lean b/Aesop/RuleTac/Cases.lean index 37630f3..d768ac9 100644 --- a/Aesop/RuleTac/Cases.lean +++ b/Aesop/RuleTac/Cases.lean @@ -36,7 +36,7 @@ namespace RuleTac partial def cases (target : CasesTarget) (md : TransparencyMode) (isRecursiveType : Bool) (ctorNames : Array CtorNames) : RuleTac := SingleRuleTac.toRuleTac λ input => do - match ← go #[] #[] input.goal |>.run with + match ← go #[] #[] ∅ input.goal |>.run with | (none, _) => throwError "No matching hypothesis found." | (some goals, steps) => return (goals, steps, none) where @@ -58,8 +58,8 @@ partial def cases (target : CasesTarget) (md : TransparencyMode) else return none - go (newGoals : Array MVarId) (excluded : Array FVarId) (goal : MVarId) : - ScriptM (Option (Array MVarId)) := do + go (newGoals : Array Subgoal) (excluded : Array FVarId) (diff : GoalDiff) + (goal : MVarId) : ScriptM (Option (Array Subgoal)) := do let some hyp ← findFirstApplicableHyp excluded goal | return none let some goals ← tryCasesS goal hyp ctorNames @@ -67,21 +67,16 @@ partial def cases (target : CasesTarget) (md : TransparencyMode) let mut newGoals := newGoals for h : i in [:goals.size] do let g := goals[i] - let excluded := - if ! isRecursiveType then - excluded - else - let excluded := excluded.map λ fvarId => - match g.subst.find? fvarId with - | some (.fvar fvarId' ..) => fvarId' - | _ => fvarId - let fields := g.fields.filterMap λ - | (.fvar fvarId' ..) => some fvarId' - | _ => none - excluded ++ fields - match ← go newGoals excluded g.mvarId with + let newDiff ← diffGoals goal g.mvarId + (.ofFVarSubstIgnoringNonFVarIds g.subst) + let mut excluded := excluded + if isRecursiveType then + excluded := + excluded.map diff.fvarSubst.get ++ newDiff.addedFVars.toArray + let diff := diff.comp newDiff + match ← go newGoals excluded diff g.mvarId with | some newGoals' => newGoals := newGoals' - | none => newGoals := newGoals.push g.mvarId + | none => newGoals := newGoals.push { mvarId := g.mvarId, diff } return some newGoals end Aesop.RuleTac diff --git a/Aesop/RuleTac/FVarIdSubst.lean b/Aesop/RuleTac/FVarIdSubst.lean new file mode 100644 index 0000000..afda863 --- /dev/null +++ b/Aesop/RuleTac/FVarIdSubst.lean @@ -0,0 +1,80 @@ +/- +Copyright (c) 2024 Jannis Limperg. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jannis Limperg +-/ + +import Batteries.Data.HashMap + +open Lean Lean.Meta + +namespace Aesop + +structure FVarIdSubst where + map : Batteries.HashMap FVarId FVarId + deriving Inhabited + +namespace FVarIdSubst + +def isEmpty (s : FVarIdSubst) : Bool := + s.map.isEmpty + +def contains (s : FVarIdSubst) (fvarId : FVarId) : Bool := + s.map.contains fvarId + +def find? (s : FVarIdSubst) (fvarId : FVarId) : Option FVarId := + s.map.find? fvarId + +def get (s : FVarIdSubst) (fvarId : FVarId) : FVarId := + s.find? fvarId |>.getD fvarId + +def apply (s : FVarIdSubst) (e : Expr) : Expr := + if s.isEmpty || ! e.hasFVar then + e + else + e.replace λ + | .fvar fvarId => s.find? fvarId |>.map mkFVar + | _ => none + +def applyToLocalDecl (s : FVarIdSubst) : LocalDecl → LocalDecl + | .cdecl i id n t bi k => .cdecl i id n (s.apply t) bi k + | .ldecl i id n t v nd k => .ldecl i id n (s.apply t) (s.apply v) nd k + +def domain (s : FVarIdSubst) : HashSet FVarId := + s.map.fold (init := ∅) λ r k _ => r.insert k + +def codomain (s : FVarIdSubst) : HashSet FVarId := + s.map.fold (init := ∅) λ r _ v => r.insert v + +protected def empty : FVarIdSubst := + ⟨∅⟩ + +instance : EmptyCollection FVarIdSubst := + ⟨.empty⟩ + +def insert (s : FVarIdSubst) (old new : FVarId) : FVarIdSubst := + let map : Batteries.HashMap _ _ := s.map.mapVal λ _ v => + if v == old then new else v + ⟨map.insert old new⟩ + +def erase (s : FVarIdSubst) (fvarId : FVarId) : FVarIdSubst := + ⟨s.map.erase fvarId⟩ + +def append (s t : FVarIdSubst) : FVarIdSubst := + let map := s.map.mapVal λ _ v => t.get v + ⟨t.map.fold (init := map) λ s k v => s.insert k v⟩ + +def ofFVarSubstIgnoringNonFVarIds (s : FVarSubst) : FVarIdSubst := .mk $ + s.map.foldl (init := ∅) λ map k v => + if let .fvar fvarId := v then map.insert k fvarId else map + +def ofFVarSubst? (s : FVarSubst) : Option FVarIdSubst := Id.run do + let mut result := ∅ + for (k, v) in s.map do + if let .fvar fvarId := v then + result := result.insert k fvarId + else + return none + return some result + +end Aesop.FVarIdSubst diff --git a/Aesop/RuleTac/Forward.lean b/Aesop/RuleTac/Forward.lean index 601f447..e64cfeb 100644 --- a/Aesop/RuleTac/Forward.lean +++ b/Aesop/RuleTac/Forward.lean @@ -89,8 +89,8 @@ partial def makeForwardHyps (e : Expr) (pat? : Option RulePattern) return (proofsAcc, usedHypsAcc, proofTypesAcc) def assertForwardHyp (goal : MVarId) (hyp : Hypothesis) (depth : Nat) - (md : TransparencyMode) : ScriptM MVarId := do - withScriptStep goal (#[·]) (λ _ => true) tacticBuilder do + (md : TransparencyMode) : ScriptM (FVarId × MVarId) := do + withScriptStep goal (λ (_, g) => #[g]) (λ _ => true) tacticBuilder do withTransparency md do let hyp := { hyp with @@ -103,14 +103,16 @@ def assertForwardHyp (goal : MVarId) (hyp : Hypothesis) (depth : Nat) binderInfo := .default kind := .implDetail } - (·.snd) <$> goal.assertHypotheses' #[hyp, implDetailHyp] + let (#[fvarId, _], goal) ← goal.assertHypotheses' #[hyp, implDetailHyp] + | throwError "aesop: internal error in assertForwardHyp: unexpected number of asserted fvars" + return (fvarId, goal) where tacticBuilder _ := Script.TacticBuilder.assertHypothesis goal hyp md def applyForwardRule (goal : MVarId) (e : Expr) (pat? : Option RulePattern) (patInsts : HashSet RulePatternInstantiation) (immediate : UnorderedArraySet Nat) (clear : Bool) - (md : TransparencyMode) (maxDepth? : Option Nat) : ScriptM MVarId := + (md : TransparencyMode) (maxDepth? : Option Nat) : ScriptM Subgoal := withTransparency md $ goal.withContext do let forwardHypData ← getForwardHypData let mut newHypProofs := #[] @@ -136,12 +138,23 @@ def applyForwardRule (goal : MVarId) (e : Expr) (pat? : Option RulePattern) let type ← inferType proof newHyps := newHyps.push ({ value := proof, type, userName }, depth) let mut goal := goal + let mut addedFVars := ∅ for (newHyp, depth) in newHyps do - goal ← assertForwardHyp goal newHyp depth md + let (fvarId, goal') ← assertForwardHyp goal newHyp depth md + goal := goal' + addedFVars := addedFVars.insert fvarId + let mut diff := { + addedFVars + removedFVars := ∅ + fvarSubst := ∅ + } if clear then - let (goal', _) ← tryClearManyS goal usedHyps + let (goal', removedFVars) ← tryClearManyS goal usedHyps + let removedFVars := removedFVars.foldl (init := ∅) λ set fvarId => + set.insert fvarId + diff := { diff with removedFVars := removedFVars } goal := goal' - return goal + return { mvarId := goal, diff } where err {α} : MetaM α := throwError "found no instances of {e} (other than possibly those which had been previously added by forward rules)" diff --git a/Aesop/RuleTac/GoalDiff.lean b/Aesop/RuleTac/GoalDiff.lean new file mode 100644 index 0000000..d7d470d --- /dev/null +++ b/Aesop/RuleTac/GoalDiff.lean @@ -0,0 +1,203 @@ +/- +Copyright (c) 2024 Jannis Limperg. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jannis Limperg +-/ + +import Aesop.RuleTac.FVarIdSubst + +open Lean Lean.Meta + +namespace Aesop + +/-- +A representation of the differences between two goals. Each Aesop rule produces +a `GoalDiff` between the goal on which the rule was run (the 'old goal') and +each of the subgoals produced by the rule (the 'new goals'). + +We use the produced `GoalDiff`s to update stateful data structures which cache +information about Aesop goals and for which it is more efficient to update the +cached information than to recompute it for each goal. + +For a goal diff between an old goal with local context `Γ` and a new goal with +local context `Δ`, we expect that + +```text +Δ = (Γ \ removedFVars) ∪ addedFVars +``` + +when the local contexts are viewed as sets of `FVarId`s (excluding +implementation detail hypotheses). + +As an optimisation, the goal diff additionally contains an `fvarSubst : +FVarIdSubst` which tracks renamings of hypotheses. When the substitution +contains a mapping `h ↦ h'`, this means that `h` was renamed to `h'`. Note that +we do not guarantee that for all such mappings, `h` actually appears in the old +goal and `h'` in the new goal. But if they do, `fvarSubst(T)` and `T'` must be +defeq in the context of the new goal, where `h : T`, `h' : T'` and +`fvarSubst(T)` is the application of the substitution to `T`. If `h` and `h'` +are `let` decls with values `v` and `v'`, `fvarSubst(v)` must additionally be +defeq to `v'`. + +The `fvarSubst` is semantically irrelevant: it does not influence the sets of +added and removed hypotheses. However, it is an important performance +optimisation, so rules should strive to generate accurate substitutions whenever +possible. +-/ +structure GoalDiff where + /-- + `FVarId`s that appear in the new goal, but not in the old goal. + -/ + addedFVars : HashSet FVarId + /-- + `FVarId`s that appear in the old goal, but not in the new goal. + -/ + removedFVars : HashSet FVarId + /-- + An `FVarId` substitution that tracks hypotheses which have been renamed (but + have not otherwise been modified). + -/ + fvarSubst : FVarIdSubst + deriving Inhabited + +protected def GoalDiff.empty : GoalDiff where + addedFVars := ∅ + removedFVars := ∅ + fvarSubst := ∅ + +instance : EmptyCollection GoalDiff := + ⟨.empty⟩ + +def getNewFVars (oldLCtx newLCtx : LocalContext) : HashSet FVarId := + newLCtx.foldl (init := ∅) λ newFVars ldecl => + if ! ldecl.isImplementationDetail && ! oldLCtx.contains ldecl.fvarId then + newFVars.insert ldecl.fvarId + else + newFVars + +/-- +Diff two goals. +-/ +def diffGoals (old new : MVarId) (fvarSubst : FVarIdSubst) : + MetaM GoalDiff := do + let oldLCtx := (← old.getDecl).lctx + let newLCtx := (← new.getDecl).lctx + return { + addedFVars := getNewFVars oldLCtx newLCtx + removedFVars := getNewFVars newLCtx oldLCtx + fvarSubst + } + +-- TODO upstream +local instance [BEq α] [Hashable α] [Monad m] : + ForM m (Batteries.HashMap α β) (α × β) where + forM | m, f => m.forM λ a b => f (a, b) + +-- TODO upstream +local instance [BEq α] [Hashable α] [Monad m] : + ForIn m (Batteries.HashMap α β) (α × β) where + forIn := ForM.forIn + +namespace GoalDiff + +/-- +If `diff₁` is the difference between goals `g₁` and `g₂` and `diff₂` is the +difference between `g₂` and `g₃`, then `diff₁.comp diff₂` is the difference +between `g₁` and `g₃`. +-/ +def comp (diff₁ diff₂ : GoalDiff) : GoalDiff where + addedFVars := + diff₁.addedFVars.fold (init := diff₂.addedFVars) λ addedFVars fvarId => + if diff₂.removedFVars.contains fvarId then + addedFVars + else + addedFVars.insert fvarId + removedFVars := + diff₂.removedFVars.fold (init := diff₁.removedFVars) λ removedFVars fvarId => + if diff₁.addedFVars.contains fvarId then + removedFVars + else + removedFVars.insert fvarId + fvarSubst := diff₁.fvarSubst.append diff₂.fvarSubst + +def checkCore (diff : GoalDiff) (old new : MVarId) : + MetaM (Option MessageData) := do + let oldLCtx := (← old.getDecl).lctx + let newLCtx := (← new.getDecl).lctx + + -- Check that the added hypotheses were indeed added + for fvarId in diff.addedFVars do + if let some ldecl := oldLCtx.find? fvarId then + return some m!"addedFVars contains hypothesis {ldecl.userName} which was already present in the old goal" + unless newLCtx.contains fvarId do + return some m!"addedFVars contains hypothesis {fvarId.name} but this fvar does not exist in the new goal" + + -- Check that the removed hypotheses were indeed removed + for fvarId in diff.removedFVars do + if let some ldecl := newLCtx.find? fvarId then + return some m!"removedFVars contains hypothesis {ldecl.userName} but it is still present in the new goal" + unless oldLCtx.contains fvarId do + return some m!"removedFVars contains hypothesis {fvarId.name} but this fvar does not exist in the old goal" + + -- Check that all added hypotheses appear in addedFVars + for newLDecl in newLCtx do + if newLDecl.isImplementationDetail then + continue + let newFVarId := newLDecl.fvarId + if ! oldLCtx.contains newFVarId && + ! diff.addedFVars.contains newFVarId then + return some m!"hypothesis {newLDecl.userName} was added, but does not appear in addedFVars" + + -- Check that all removed hypotheses appear in removedFVars + for oldLDecl in oldLCtx do + if oldLDecl.isImplementationDetail then + continue + let oldFVarId := oldLDecl.fvarId + if ! newLCtx.contains oldFVarId && + ! diff.removedFVars.contains oldFVarId then + return some m!"hypothesis {oldLDecl.userName} was removed, but does not appear in removedFVars" + + -- Check that all common hypotheses are defeq + for newLDecl in newLCtx do + if newLDecl.isImplementationDetail then + continue + if let some oldLDecl := oldLCtx.find? newLDecl.fvarId then + let equalLDecls ← new.withContext do + isDefeqLocalDecl (diff.fvarSubst.applyToLocalDecl oldLDecl) newLDecl + unless equalLDecls do + return some m!"hypotheses {oldLDecl.userName} and {newLDecl.userName} have the same FvarId but are not defeq" + + -- Check the fvarSubst + for (oldFVarId, newFVarId) in diff.fvarSubst.map do + let some oldLDecl := oldLCtx.find? oldFVarId + | continue + if oldLDecl.isImplementationDetail then + continue + let some newLDecl := newLCtx.find? newFVarId + | continue + if newLDecl.isImplementationDetail then + return some m!"fvarSubst maps hypothesis {oldLDecl.userName} to {newLDecl.userName}, but {newLDecl.userName} is an implementation detail" + let equalLDecls ← new.withContext do + isDefeqLocalDecl (diff.fvarSubst.applyToLocalDecl oldLDecl) newLDecl + unless equalLDecls do + return some m!"fvarSubst maps hypothesis {oldLDecl.userName} to {newLDecl.userName} but these hypotheses are not defeq" + + return none +where + isDefeqLocalDecl : LocalDecl → LocalDecl → MetaM Bool + | .cdecl (type := type₁) .., + .cdecl (type := type₂) .. => + isDefEq type₁ type₂ + | .ldecl (type := type₁) (value := value₁) .., + .ldecl (type := type₂) (value := value₂) .. => + isDefEq type₁ type₂ <&&> isDefEq value₁ value₂ + | _, _ => return false + +def check (diff : GoalDiff) (old new : MVarId) : + MetaM (Option MessageData) := do + if let some err ← diff.checkCore old new then + addMessageContext m!"rule produced incorrect diff:{indentD err}\nold goal:{indentD old}\nnew goal:{indentD new}" + else + return none + +end Aesop.GoalDiff diff --git a/Aesop/RuleTac/Preprocess.lean b/Aesop/RuleTac/Preprocess.lean index 77a800f..2cbf7e0 100644 --- a/Aesop/RuleTac/Preprocess.lean +++ b/Aesop/RuleTac/Preprocess.lean @@ -16,7 +16,7 @@ This `RuleTac` is applied once to the root goal, before any other rules are tried. -/ def preprocess : RuleTac := RuleTac.ofSingleRuleTac λ input => do - let ((postMVarId, _), steps) ← renameInaccessibleFVarsS input.goal |>.run - return (#[postMVarId], steps, none) + let ((mvarId, _), steps) ← renameInaccessibleFVarsS input.goal |>.run + return (#[{ mvarId, diff := ∅ }], steps, none) end Aesop.RuleTac diff --git a/Aesop/RuleTac/Tactic.lean b/Aesop/RuleTac/Tactic.lean index 7ec93d1..a82f14b 100644 --- a/Aesop/RuleTac/Tactic.lean +++ b/Aesop/RuleTac/Tactic.lean @@ -18,6 +18,7 @@ unsafe def tacticMImpl (decl : Name) : RuleTac := SingleRuleTac.toRuleTac λ input => do let tac ← evalConst (TacticM Unit) decl let goals ← run input.goal tac |>.run' + let goals ← goals.mapM (mvarIdToSubgoal (parentMVarId := input.goal) · ∅) return (goals.toArray, none, none) -- Precondition: `decl` has type `TacticM Unit`. @@ -65,6 +66,8 @@ def tacticStx (stx : Syntax) : RuleTac := tacticBuilders := #[tacticBuilder] preState, postState, postGoals } + let postGoals ← + postGoals.mapM (mvarIdToSubgoal (parentMVarId := input.goal) · ∅) return (postGoals, some #[step], none) -- Precondition: `decl` has type `TacGen`. @@ -94,7 +97,14 @@ unsafe def tacGenImpl (decl : Name) : RuleTac := λ input => do tacticBuilders := #[return .unstructured ⟨stx⟩] postState, postGoals } - apps := apps.push $ .ofLazyScriptStep step successProbability + let postGoals ← + postGoals.mapM (mvarIdToSubgoal (parentMVarId := input.goal) · ∅) + apps := apps.push { + goals := postGoals + scriptSteps? := some #[step] + successProbability? := successProbability + postState + } catch e => errors := errors.push (tacticStr, e) if apps.isEmpty then throwError diff --git a/Aesop/Saturate.lean b/Aesop/Saturate.lean index 79683f3..341601b 100644 --- a/Aesop/Saturate.lean +++ b/Aesop/Saturate.lean @@ -28,7 +28,7 @@ def getSingleGoal [Monad m] [MonadError m] (o : RuleTacOutput) : | throwError "rule produced more than one rule application" let #[goal] := app.goals | throwError "rule did not produce exactly one subgoal" - return (goal, app.postState, app.scriptSteps?) + return (goal.mvarId, app.postState, app.scriptSteps?) initialize registerTraceClass `saturate diff --git a/Aesop/Search/Expansion/Basic.lean b/Aesop/Search/Expansion/Basic.lean index 1422138..c135cad 100644 --- a/Aesop/Search/Expansion/Basic.lean +++ b/Aesop/Search/Expansion/Basic.lean @@ -24,7 +24,7 @@ def runRuleTac (tac : RuleTac) (ruleName : RuleName) if ← Check.rules.isEnabled then if let (Sum.inr ruleOutput) := result then ruleOutput.applications.forM λ rapp => do - if let (some err) ← rapp.check then + if let (some err) ← rapp.check input then throwError "{Check.rules.name}: while applying rule {ruleName}: {err}" return result diff --git a/Aesop/Search/Expansion/Norm.lean b/Aesop/Search/Expansion/Norm.lean index c6e0926..e9145be 100644 --- a/Aesop/Search/Expansion/Norm.lean +++ b/Aesop/Search/Expansion/Norm.lean @@ -84,7 +84,7 @@ def runNormRuleTac (rule : NormRule) (input : RuleTacInput) : restoreState rapp.postState if rapp.goals.isEmpty then return some $ .proved rapp.scriptSteps? - let (#[g]) := rapp.goals + let (#[{ mvarId := g, .. }]) := rapp.goals | err m!"rule produced more than one subgoal." let mvars := .ofArray input.mvars.toArray if ← Check.rules.isEnabled then diff --git a/Aesop/Tree/AddRapp.lean b/Aesop/Tree/AddRapp.lean index a72ac3e..a06e920 100644 --- a/Aesop/Tree/AddRapp.lean +++ b/Aesop/Tree/AddRapp.lean @@ -136,6 +136,8 @@ private def makeInitialGoal (goal : MVarId) (mvars : UnorderedArraySet MVarId) } private unsafe def addRappUnsafe (r : AddRapp) : TreeM RappRef := do + let originalSubgoals := r.goals.map (·.mvarId) + let rref : RappRef ← IO.mkRef $ Rapp.mk { id := ← getAndIncrementNextRappId parent := r.parent @@ -144,7 +146,7 @@ private unsafe def addRappUnsafe (r : AddRapp) : TreeM RappRef := do isIrrelevant := false appliedRule := r.appliedRule scriptSteps? := r.scriptSteps? - originalSubgoals := r.goals + originalSubgoals successProbability := r.successProbability metaState := r.postState introducedMVars := {} -- will be filled in later @@ -153,7 +155,6 @@ private unsafe def addRappUnsafe (r : AddRapp) : TreeM RappRef := do let parentGoal ← r.parent.get let goalDepth := parentGoal.depth + 1 - let originalSubgoals := r.goals let (originalSubgoalMVars, assignedMVars, assignedOrDroppedMVars) ← r.postState.runMetaM' do diff --git a/AesopTest/Forward.lean b/AesopTest/Forward.lean index f2d79cc..858f578 100644 --- a/AesopTest/Forward.lean +++ b/AesopTest/Forward.lean @@ -26,7 +26,7 @@ def forwardTac (goal : MVarId) (id : Ident) (immediate : Option (Array Syntax)) let (goal, _) ← RuleTac.applyForwardRule goal (mkFVar ldecl.fvarId) none ∅ immediate clear md (maxDepth? := none) |>.run - return [goal] + return [goal.mvarId] @[tactic forward] def evalForward : Tactic