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

fix(goal): Over-eager deduplication of goals

This commit is contained in:
Leni Aniva 2025-05-01 13:34:27 -04:00
parent 4db09c3abc
commit 8c1cea17e3
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
2 changed files with 5 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Pantograph/Goal.lean
View File

@ -140,8 +140,7 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S
-- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic. -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
let unassigned := goals.filter λ goal => let unassigned := goals.filter λ goal =>
let isSolved := state.mctx.eAssignment.contains goal || state.mctx.dAssignment.contains goal let isSolved := state.mctx.eAssignment.contains goal || state.mctx.dAssignment.contains goal
let isDuplicate := state.goals.contains goal ¬ isSolved
(¬ isDuplicate) && (¬ isSolved)
return { return {
state with state with
savedState := { savedState := {

8
Test/Metavar.lean
View File

@ -238,21 +238,21 @@ def test_partial_continuation: TestM Unit := do
addTest $ assertUnreachable $ msg addTest $ assertUnreachable $ msg
return () return ()
| .ok state => pure state | .ok state => pure state
addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = addTest $ LSpec.check "(continue 1)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"]) #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
checkTrue "(2 root)" state1b.rootExpr?.get!.hasExprMVar checkTrue "(2 root)" state1b.rootExpr?.get!.hasExprMVar
-- Roundtrip -- Roundtrip
--let coupled_goals := coupled_goals.map (λ g => --let coupled_goals := coupled_goals.map (λ g =>
-- { name := str_to_name $ serializeName g.name (sanitize := false)}) -- { name := str_to_name $ serializeName g.name (sanitize := false)})
let coupled_goals := coupled_goals.map (λ g => serializeName g.name (sanitize := false)) let coupled_goals := coupled_goals.map (·.name.toString)
let coupled_goals := coupled_goals.map (λ g => { name := g.toName }) let coupled_goals := coupled_goals.map ({ name := ·.toName })
let state1b ← match state2.resume (goals := coupled_goals) with let state1b ← match state2.resume (goals := coupled_goals) with
| .error msg => do | .error msg => do
addTest $ assertUnreachable $ msg addTest $ assertUnreachable $ msg
return () return ()
| .ok state => pure state | .ok state => pure state
addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = addTest $ LSpec.check "(continue 2)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"]) #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
checkTrue "(2 root)" state1b.rootExpr?.get!.hasExprMVar checkTrue "(2 root)" state1b.rootExpr?.get!.hasExprMVar