fix: Prevent incorrect inheritance of calc rhs

This commit is contained in:
Leni Aniva 2024-04-11 16:11:06 -07:00
parent f20ee8dc87
commit 036fab0ad6
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
2 changed files with 11 additions and 2 deletions

View File

@ -325,6 +325,11 @@ protected def GoalState.convExit (state: GoalState):
catch exception => catch exception =>
return .failure #[← exception.toMessageData.toString] return .failure #[← exception.toMessageData.toString]
protected def GoalState.calcPrevRhsOf? (state: GoalState) (goalId: Nat) :=
if goalId == 1 then
state.calcPrevRhs?
else
.none
protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
Elab.TermElabM TacticResult := do Elab.TermElabM TacticResult := do
state.restoreElabM state.restoreElabM
@ -340,20 +345,21 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
(fileName := filename) with (fileName := filename) with
| .ok syn => pure syn | .ok syn => pure syn
| .error error => return .parseError error | .error error => return .parseError error
let calcPrevRhs? := state.calcPrevRhsOf? goalId
try try
goal.withContext do goal.withContext do
let target ← instantiateMVars (← goal.getDecl).type let target ← instantiateMVars (← goal.getDecl).type
let tag := (← goal.getDecl).userName let tag := (← goal.getDecl).userName
let mut step ← Elab.Term.elabType <| ← do let mut step ← Elab.Term.elabType <| ← do
if let some prevRhs := state.calcPrevRhs? then if let some prevRhs := calcPrevRhs? then
Elab.Term.annotateFirstHoleWithType pred (← Meta.inferType prevRhs) Elab.Term.annotateFirstHoleWithType pred (← Meta.inferType prevRhs)
else else
pure pred pure pred
let some (_, lhs, rhs) ← Elab.Term.getCalcRelation? step | let some (_, lhs, rhs) ← Elab.Term.getCalcRelation? step |
throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}" throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}"
if let some prevRhs := state.calcPrevRhs? then if let some prevRhs := calcPrevRhs? then
unless (← Meta.isDefEqGuarded lhs prevRhs) do unless (← Meta.isDefEqGuarded lhs prevRhs) do
throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}" -- " throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}" -- "

View File

@ -510,6 +510,8 @@ def test_calc: TestM Unit := do
interiorGoal [] "a + b = b + c" (.some "calc"), interiorGoal [] "a + b = b + c" (.some "calc"),
interiorGoal [] "b + c = c + d" interiorGoal [] "b + c = c + d"
]) ])
addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? 0 |>.isNone)
addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? 1 |>.isSome)
let tactic := "apply h1" let tactic := "apply h1"
let state2m ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with let state2m ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
@ -532,6 +534,7 @@ def test_calc: TestM Unit := do
#[ #[
interiorGoal [] "b + c = c + d" (.some "calc") interiorGoal [] "b + c = c + d" (.some "calc")
]) ])
addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? 0 |>.isNone)
let tactic := "apply h2" let tactic := "apply h2"
let state4m ← match ← state4.tryTactic (goalId := 0) (tactic := tactic) with let state4m ← match ← state4.tryTactic (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state