aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

fix: Prevent incorrect inheritance of calc rhs #66

Merged
aniva merged 5 commits from goal/calc into dev 2024-04-12 20:52:18 -07:00
Conversation 0 Commits 5 Files Changed 3 +18 -19
1 changed files with 18 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit e834765896 - Show all commits

37
Pantograph/Goal.lean
View File

@ -164,22 +164,21 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
let errors ← (messages.map Message.data).mapM fun md => md.toString let errors ← (messages.map Message.data).mapM fun md => md.toString
return .failure errors return .failure errors
else let prevMCtx := state.savedState.term.meta.meta.mctx
let prevMCtx := state.savedState.term.meta.meta.mctx let nextMCtx ← getMCtx
let nextMCtx ← getMCtx -- Generate a list of mvarIds that exist in the parent state; Also test the
-- Generate a list of mvarIds that exist in the parent state; Also test the -- assertion that the types have not changed on any mvars.
-- assertion that the types have not changed on any mvars. let newMVars := newMVarSet prevMCtx nextMCtx
let newMVars := newMVarSet prevMCtx nextMCtx let nextGoals ← newMVars.toList.filterM (λ mvar => do pure !(← mvar.isAssigned))
let nextGoals ← newMVars.toList.filterM (λ mvar => do pure !(← mvar.isAssigned)) return .success {
return .success { root := state.root,
root := state.root, savedState := {
savedState := { term := ← MonadBacktrack.saveState,
term := ← MonadBacktrack.saveState, tactic := { goals := nextGoals }
tactic := { goals := nextGoals } },
}, newMVars,
newMVars, parentMVar? := .some goal,
parentMVar? := .some goal, }
}
catch exception => catch exception =>
return .failure #[← exception.toMessageData.toString] return .failure #[← exception.toMessageData.toString]
@ -346,10 +345,10 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
| .ok syn => pure syn | .ok syn => pure syn
| .error error => return .parseError error | .error error => return .parseError error
let calcPrevRhs? := state.calcPrevRhsOf? goalId let calcPrevRhs? := state.calcPrevRhsOf? goalId
let target ← instantiateMVars (← goal.getDecl).type
let tag := (← goal.getDecl).userName
try try
goal.withContext do goal.withContext do
let target ← instantiateMVars (← goal.getDecl).type
let tag := (← goal.getDecl).userName
let mut step ← Elab.Term.elabType <| ← do let mut step ← Elab.Term.elabType <| ← do
if let some prevRhs := calcPrevRhs? then if let some prevRhs := calcPrevRhs? then
@ -377,7 +376,7 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
-- The calc tactic either solves the main goal or leaves another relation. -- The calc tactic either solves the main goal or leaves another relation.
-- Replace the main goal, and save the new goal if necessary -- Replace the main goal, and save the new goal if necessary
if ¬(← Meta.isDefEq proofType target) then unless ← Meta.isDefEq proofType target do
let rec throwFailed := let rec throwFailed :=
throwError "'calc' tactic failed, has type{indentExpr proofType}\nbut it is expected to have type{indentExpr target}" throwError "'calc' tactic failed, has type{indentExpr proofType}\nbut it is expected to have type{indentExpr target}"
let some (_, _, rhs) ← Elab.Term.getCalcRelation? proofType | throwFailed let some (_, _, rhs) ← Elab.Term.getCalcRelation? proofType | throwFailed