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

fix: Test failures

This commit is contained in:
Leni Aniva 2025-01-13 12:28:16 -08:00
parent 06fdf7e678
commit 60e78b322e
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
6 changed files with 58 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Test/Common.lean
View File

@ -48,6 +48,12 @@ namespace Condensed
deriving instance BEq, Repr for LocalDecl deriving instance BEq, Repr for LocalDecl
deriving instance BEq, Repr for Goal deriving instance BEq, Repr for Goal
-- Enable string interpolation
instance : ToString FVarId where
toString id := id.name.toString
instance : ToString MVarId where
toString id := id.name.toString
protected def LocalDecl.devolatilize (decl: LocalDecl): LocalDecl := protected def LocalDecl.devolatilize (decl: LocalDecl): LocalDecl :=
{ {
decl with fvarId := { name := .anonymous } decl with fvarId := { name := .anonymous }

12
Test/Integration.lean
View File

@ -90,27 +90,27 @@ def test_automatic_mode (automatic: Bool): Test :=
], ],
} }
let goal2l: Protocol.Goal := { let goal2l: Protocol.Goal := {
name := "_uniq.59", name := "_uniq.61",
userName? := .some "inl", userName? := .some "inl",
target := { pp? := .some "q ∨ p" }, target := { pp? := .some "q ∨ p" },
vars := varsPQ ++ #[ vars := varsPQ ++ #[
{ name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true} { name := "_uniq.49", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
], ],
} }
let goal2r: Protocol.Goal := { let goal2r: Protocol.Goal := {
name := "_uniq.72", name := "_uniq.74",
userName? := .some "inr", userName? := .some "inr",
target := { pp? := .some "q ∨ p" }, target := { pp? := .some "q ∨ p" },
vars := varsPQ ++ #[ vars := varsPQ ++ #[
{ name := "_uniq.60", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true} { name := "_uniq.62", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true}
], ],
} }
let goal3l: Protocol.Goal := { let goal3l: Protocol.Goal := {
name := "_uniq.78", name := "_uniq.80",
userName? := .some "inl.h", userName? := .some "inl.h",
target := { pp? := .some "p" }, target := { pp? := .some "p" },
vars := varsPQ ++ #[ vars := varsPQ ++ #[
{ name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true} { name := "_uniq.49", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
], ],
} }
[ [

4
Test/Metavar.lean
View File

@ -239,7 +239,7 @@ def test_partial_continuation: TestM Unit := do
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)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"]) #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
-- Roundtrip -- Roundtrip
@ -253,7 +253,7 @@ def test_partial_continuation: TestM Unit := do
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)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"]) #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
-- Continuation should fail if the state does not exist: -- Continuation should fail if the state does not exist:

61
Test/Proofs.lean
View File

@ -241,13 +241,15 @@ def test_or_comm: TestM Unit := do
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
let fvP := "_uniq.10" let [state1g0] := state1.goals | fail "Should have 1 goal"
let fvQ := "_uniq.13" let (fvP, fvQ, fvH) ← state1.withContext state1g0 do
let fvH := "_uniq.16" let lctx ← getLCtx
let state1g0 := "_uniq.17" let #[fvP, fvQ, fvH] := lctx.getFVarIds.map (toString ·.name) |
panic! "Incorrect number of decls"
pure (fvP, fvQ, fvH)
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)) = addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)) =
#[{ #[{
name := state1g0, name := state1g0.name.toString,
target := { pp? := .some "q ∨ p" }, target := { pp? := .some "q ∨ p" },
vars := #[ vars := #[
{ name := fvP, userName := "p", type? := .some { pp? := .some "Prop" } }, { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" } },
@ -269,7 +271,9 @@ def test_or_comm: TestM Unit := do
return () return ()
addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
#[branchGoal "inl" "p", branchGoal "inr" "q"]) #[branchGoal "inl" "p", branchGoal "inr" "q"])
let (caseL, caseR) := ("_uniq.64", "_uniq.77") let [state2g0, state2g1] := state2.goals |
fail s!"Should have 2 goals, but it has {state2.goals.length}"
let (caseL, caseR) := (state2g0.name.toString, state2g1.name.toString)
addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) = addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
#[caseL, caseR]) #[caseL, caseR])
addTest $ LSpec.check "(2 parent exists)" state2.parentExpr?.isSome addTest $ LSpec.check "(2 parent exists)" state2.parentExpr?.isSome
@ -293,7 +297,8 @@ def test_or_comm: TestM Unit := do
return () return ()
let state3_1parent ← state3_1.withParentContext do let state3_1parent ← state3_1.withParentContext do
serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!) serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!)
addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv _uniq.91))") let [state3_1goal0] := state3_1.goals | fail "Should have 1 goal"
addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv {state3_1goal0}))")
addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1) addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
| .success state => pure state | .success state => pure state
@ -559,12 +564,15 @@ def test_nat_zero_add: TestM Unit := do
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
let [mvarMotive, mvarMajor, mvarInduct, mvarConduit] := state2.goals |
fail "Incorrect number of goals"
let .num _ major := mvarMajor.name | fail "Incorrect form of mvar id"
addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) = addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
#[ #[
buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat → Prop" (.some "motive"), buildNamedGoal mvarMotive.name.toString [("n", "Nat")] "Nat → Prop" (.some "motive"),
buildNamedGoal "_uniq.72" [("n", "Nat")] "Nat", buildNamedGoal mvarMajor.name.toString [("n", "Nat")] "Nat",
buildNamedGoal "_uniq.73" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t", buildNamedGoal mvarInduct.name.toString [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
buildNamedGoal "_uniq.74" [("n", "Nat")] "?motive ?m.72 = (n + 0 = n)" (.some "conduit") buildNamedGoal mvarConduit.name.toString [("n", "Nat")] s!"?motive ?m.{major} = (n + 0 = n)" (.some "conduit")
]) ])
let tactic := "exact n" let tactic := "exact n"
@ -647,13 +655,15 @@ def test_nat_zero_add_alt: TestM Unit := do
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
let major := "_uniq.72" let [mvarMotive, mvarMajor, mvarInduct, mvarConduit] := state2.goals |
fail "Incorrect number of goals"
let .num _ major := mvarMajor.name | fail "Incorrect form of mvar id"
addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) = addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
#[ #[
buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat → Prop" (.some "motive"), buildNamedGoal mvarMotive.name.toString [("n", "Nat")] "Nat → Prop" (.some "motive"),
buildNamedGoal major [("n", "Nat")] "Nat", buildNamedGoal mvarMajor.name.toString [("n", "Nat")] "Nat",
buildNamedGoal "_uniq.73" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t", buildNamedGoal mvarInduct.name.toString [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
buildNamedGoal "_uniq.74" [("n", "Nat")] "?motive ?m.72 = (n + 0 = n)" (.some "conduit") buildNamedGoal mvarConduit.name.toString [("n", "Nat")] s!"?motive ?m.{major} = (n + 0 = n)" (.some "conduit")
]) ])
let tactic := "intro x" let tactic := "intro x"
@ -670,8 +680,7 @@ def test_nat_zero_add_alt: TestM Unit := do
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
let (eqL, eqR, eqT) := ("_uniq.92", "_uniq.93", "_uniq.91") let [eqL, eqR, eqT] := state3m2.goals | fail "Incorrect number of goals"
addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT]
let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict" let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
let state2b ← match state3m2.resume [conduit] with let state2b ← match state3m2.resume [conduit] with
| .ok state => pure state | .ok state => pure state
@ -681,20 +690,26 @@ def test_nat_zero_add_alt: TestM Unit := do
let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))" let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))"
let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))" let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))"
let fvN := "_uniq.67" let fvN ← state2b.withContext conduit do
let lctx ← getLCtx
pure $ lctx.getFVarIds.get! 0 |>.name
let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))" let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))"
let substOf (mv: String) := s!"(:subst (:mv {mv}) (:fv {fvN}) (:mv {major}))" let substOf (mvarId: MVarId) := s!"(:subst (:mv {mvarId.name}) (:fv {fvN}) (:mv {mvarMajor}))"
let .num _ nL := eqL.name | fail "Incorrect form of mvar id"
let .num _ nR := eqR.name | fail "Incorrect form of mvar id"
let nL' := nL + 4
let nR' := nR + 5
addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) = addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
#[ #[
{ {
name := "_uniq.74", name := mvarConduit.name.toString,
userName? := .some "conduit", userName? := .some "conduit",
target := { target := {
pp? := .some "(?m.96 ?m.72 = ?m.98 ?m.72) = (n + 0 = n)", pp? := .some s!"(?m.{nL'} ?m.{major} = ?m.{nR'} ?m.{major}) = (n + 0 = n)",
sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})", sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})",
}, },
vars := #[{ vars := #[{
name := fvN, name := fvN.toString,
userName := "n", userName := "n",
type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" }, type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" },
}], }],

6
Test/Tactic/Congruence.lean
View File

@ -28,7 +28,7 @@ def test_congr_arg_list : TestT Elab.TermElabM Unit := do
let results ← Meta.withAssignableSyntheticOpaque do f.apply (← parseSentence "List.reverse") let results ← Meta.withAssignableSyntheticOpaque do f.apply (← parseSentence "List.reverse")
addTest $ LSpec.check "apply" (results.length = 0) addTest $ LSpec.check "apply" (results.length = 0)
addTest $ LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂") addTest $ LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂")
addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)") addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(List.reverse ?a₁ = List.reverse ?a₂) = (l1.reverse = l2.reverse)")
def test_congr_arg : TestT Elab.TermElabM Unit := do def test_congr_arg : TestT Elab.TermElabM Unit := do
let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m" let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m"
let expr ← parseSentence expr let expr ← parseSentence expr
@ -37,7 +37,7 @@ def test_congr_arg : TestT Elab.TermElabM Unit := do
let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId! let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
[ [
(`α, "Sort ?u.70"), (`α, "Sort ?u.73"),
(`a₁, "?α"), (`a₁, "?α"),
(`a₂, "?α"), (`a₂, "?α"),
(`f, "?α → Nat"), (`f, "?α → Nat"),
@ -52,7 +52,7 @@ def test_congr_fun : TestT Elab.TermElabM Unit := do
let newGoals ← runTacticOnMVar Tactic.evalCongruenceFun target.mvarId! let newGoals ← runTacticOnMVar Tactic.evalCongruenceFun target.mvarId!
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
[ [
(`α, "Sort ?u.159"), (`α, "Sort ?u.165"),
(`f₁, "?α → Nat"), (`f₁, "?α → Nat"),
(`f₂, "?α → Nat"), (`f₂, "?α → Nat"),
(`h, "?f₁ = ?f₂"), (`h, "?f₁ = ?f₂"),

6
Test/Tactic/MotivatedApply.lean
View File

@ -40,7 +40,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do
"Nat → Prop", "Nat → Prop",
"Nat", "Nat",
"∀ (t : Nat), Nat.below t → ?motive t", "∀ (t : Nat), Nat.below t → ?motive t",
"?motive ?m.71 = (n + 0 = n)", "?motive ?m.74 = (n + 0 = n)",
]) ])
addTest test addTest test
@ -83,7 +83,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
let tactic := Tactic.evalMotivatedApply recursor let tactic := Tactic.evalMotivatedApply recursor
let newGoals ← runTacticOnMVar tactic target.mvarId! let newGoals ← runTacticOnMVar tactic target.mvarId!
let majorId := 71 let majorId := 74
addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
[ [
"Nat → Prop", "Nat → Prop",
@ -100,7 +100,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
addTest $ ← conduit.withContext do addTest $ ← conduit.withContext do
let t := toString (← Meta.ppExpr $ ← conduit.getType) let t := toString (← Meta.ppExpr $ ← conduit.getType)
return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.146 ?m.{majorId}) = (n + 0 = n)") return LSpec.check "conduit" (t = s!"(Nat.add ?m.{majorId} + 0 = ?m.149 ?m.{majorId}) = (n + 0 = n)")
def suite (env: Environment): List (String × IO LSpec.TestSeq) := def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[ [