From dc2cc5be773d3cf95fe67cd30f9843c7fc3854a2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 4 Nov 2023 15:00:51 -0700 Subject: [PATCH] test: Separate mvar coupling tests --- Pantograph/Goal.lean | 9 ++- Test/Common.lean | 15 +++++ Test/Holes.lean | 129 ++++++++++++++++++++++++++++++------------- Test/Main.lean | 4 +- Test/Proofs.lean | 95 +------------------------------ 5 files changed, 116 insertions(+), 136 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 78a4194..eeb5a10 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -170,15 +170,18 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic /-- After finishing one branch of a proof (`graftee`), pick up from the point where the proof was left off (`target`) -/ -protected def GoalState.continue (target: GoalState) (graftee: GoalState): Except String GoalState := +protected def GoalState.continue (target: GoalState) (graftee: GoalState) (goals: Option (List MVarId) := .none): Except String GoalState := + let goals := match goals with + | .some goals => goals + | .none => target.goals if target.root != graftee.root then .error s!"Roots of two continued goal states do not match: {target.root.name} != {graftee.root.name}" -- Ensure goals are not dangling - else if ¬ (target.goals.all (λ goal => graftee.mvars.contains goal)) then + else if ¬ (goals.all (λ goal => graftee.mvars.contains goal)) then .error s!"Some goals in target are not present in the graftee" else -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic. - let unassigned := target.goals.filter (λ goal => + let unassigned := goals.filter (λ goal => let mctx := graftee.mctx ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal)) .ok { diff --git a/Test/Common.lean b/Test/Common.lean index f74e6a2..5b74a0f 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -1,4 +1,6 @@ import Pantograph.Protocol +import Pantograph.Goal +import LSpec namespace Pantograph @@ -15,6 +17,19 @@ def Goal.devolatilize (goal: Goal): Goal := v with name := "" } +deriving instance DecidableEq, Repr for Expression +deriving instance DecidableEq, Repr for Variable +deriving instance DecidableEq, Repr for Goal end Protocol +def TacticResult.toString : TacticResult → String + | .success state => s!".success ({state.goals.length} goals)" + | .failure messages => + let messages := "\n".intercalate messages.toList + s!".failure {messages}" + | .parseError error => s!".parseError {error}" + | .indexError index => s!".indexError {index}" + +def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false + end Pantograph diff --git a/Test/Holes.lean b/Test/Holes.lean index 64f2e2c..9b38087 100644 --- a/Test/Holes.lean +++ b/Test/Holes.lean @@ -1,31 +1,28 @@ import LSpec import Pantograph.Goal import Pantograph.Serial +import Test.Common namespace Pantograph.Test.Holes open Pantograph open Lean -abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Commands.Options M) +abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M) -deriving instance DecidableEq, Repr for Commands.Expression -deriving instance DecidableEq, Repr for Commands.Variable -deriving instance DecidableEq, Repr for Commands.Goal - -def add_test (test: LSpec.TestSeq): TestM Unit := do +def addTest (test: LSpec.TestSeq): TestM Unit := do set $ (← get) ++ test -def start_goal (hole: String): TestM (Option GoalState) := do +def startProof (expr: String): TestM (Option GoalState) := do let env ← Lean.MonadEnv.getEnv - let syn? := syntax_from_str env hole - add_test $ LSpec.check s!"Parsing {hole}" (syn?.isOk) + let syn? := syntax_from_str env expr + addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk) match syn? with | .error error => IO.println error return Option.none | .ok syn => - let expr? ← syntax_to_expr syn - add_test $ LSpec.check s!"Elaborating" expr?.isOk + let expr? ← syntax_to_expr_type syn + addTest $ LSpec.check s!"Elaborating" expr?.isOk match expr? with | .error error => IO.println error @@ -34,40 +31,21 @@ def start_goal (hole: String): TestM (Option GoalState) := do let goal ← GoalState.create (expr := expr) return Option.some goal -def assert_unreachable (message: String): LSpec.TestSeq := LSpec.check message false - -def build_goal (nameType: List (String × String)) (target: String): Commands.Goal := +def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal := { + userName?, target := { pp? := .some target}, vars := (nameType.map fun x => ({ - name := x.fst, + userName := x.fst, type? := .some { pp? := .some x.snd }, isInaccessible? := .some false })).toArray } --- Like `build_goal` but allow certain variables to be elided. -def build_goal_selective (nameType: List (String × Option String)) (target: String): Commands.Goal := - { - target := { pp? := .some target}, - vars := (nameType.map fun x => ({ - name := x.fst, - type? := x.snd.map (λ type => { pp? := type }), - isInaccessible? := x.snd.map (λ _ => false) - })).toArray - } - -def construct_sigma: TestM Unit := do - let goal? ← start_goal "∀ (n m: Nat), n + m = m + n" - add_test $ LSpec.check "Start goal" goal?.isSome - if let .some goal := goal? then - return () - - -def proof_runner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do +def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options let coreContext: Lean.Core.Context := { - currNamespace := str_to_name "Aniva", + currNamespace := Name.append .anonymous "Aniva", openDecls := [], -- No 'open' directives needed fileName := "", fileMap := { source := "", positions := #[0], lines := #[1] } @@ -83,17 +61,94 @@ def proof_runner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq : | .ok (_, a) => return a +/-- M-coupled goals -/ +def test_m_couple: TestM Unit := do + let state? ← startProof "(2: Nat) ≤ 5" + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + + let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) = + #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"]) + addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone + -- Set m to 3 + let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 3") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone + let state1b ← match state1.continue state2 with + | .error msg => do + addTest $ assertUnreachable $ msg + return () + | .ok state => pure state + addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = + #[.some "2 ≤ 3", .some "3 ≤ 5"]) + addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone + return () + +def test_proposition_generation: TestM Unit := do + let state? ← startProof "Σ' p:Prop, p" + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + + let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply PSigma.mk") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "apply PSigma.mk" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = + #[ + buildGoal [] "?fst" (userName? := .some "snd"), + buildGoal [] "Prop" (userName? := .some "fst") + ]) + if let #[goal1, goal2] := ← state1.serializeGoals (options := { (← read) with printExprAST := true }) then + addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})") + addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone + + let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) = + #[.some "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"]) + addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone + + let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) = + #[]) + addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome + return () + + def suite: IO LSpec.TestSeq := do let env: Lean.Environment ← Lean.importModules (imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false })) (opts := {}) (trustLevel := 1) let tests := [ - ("Σ'", construct_sigma) + ("2 < 5", test_m_couple), + ("Proposition Generation", test_proposition_generation) ] let tests ← tests.foldlM (fun acc tests => do let (name, tests) := tests - let tests ← proof_runner env tests + let tests ← proofRunner env tests return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done return LSpec.group "Holes" tests diff --git a/Test/Main.lean b/Test/Main.lean index 5b9a24a..cb7c055 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -1,5 +1,5 @@ import LSpec ---import Test.Holes +import Test.Holes import Test.Integration import Test.Proofs import Test.Serial @@ -11,7 +11,7 @@ unsafe def main := do Lean.initSearchPath (← Lean.findSysroot) let suites := [ - --Holes.suite, + Holes.suite, Integration.suite, Proofs.suite, Serial.suite diff --git a/Test/Proofs.lean b/Test/Proofs.lean index c08ecb2..8ec01a7 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -6,17 +6,6 @@ import Pantograph.Goal import Pantograph.Serial import Test.Common -namespace Pantograph - -def TacticResult.toString : TacticResult → String - | .success state => s!".success ({state.goals.length} goals)" - | .failure messages => - let messages := "\n".intercalate messages.toList - s!".failure {messages}" - | .parseError error => s!".parseError {error}" - | .indexError index => s!".indexError {index}" -end Pantograph - namespace Pantograph.Test.Proofs open Pantograph open Lean @@ -27,10 +16,6 @@ inductive Start where abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M) -deriving instance DecidableEq, Repr for Protocol.Expression -deriving instance DecidableEq, Repr for Protocol.Variable -deriving instance DecidableEq, Repr for Protocol.Goal - def addTest (test: LSpec.TestSeq): TestM Unit := do set $ (← get) ++ test @@ -64,8 +49,6 @@ def startProof (start: Start): TestM (Option GoalState) := do let goal ← GoalState.create (expr := expr) return Option.some goal -def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false - def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal := { userName?, @@ -303,80 +286,6 @@ def proof_or_comm: TestM Unit := do ] } -/-- M-coupled goals -/ -def proof_m_couple: TestM Unit := do - let state? ← startProof (.expr "(2: Nat) ≤ 5") - let state0 ← match state? with - | .some state => pure state - | .none => do - addTest $ assertUnreachable "Goal could not parse" - return () - - let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) = - #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"]) - addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone - -- Set m to 3 - let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 3") with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone - let state1b ← match state1.continue state2 with - | .error msg => do - addTest $ assertUnreachable $ msg - return () - | .ok state => pure state - addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = - #[.some "2 ≤ 3", .some "3 ≤ 5"]) - addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone - return () - -def proof_proposition_generation: TestM Unit := do - let state? ← startProof (.expr "Σ' p:Prop, p") - let state0 ← match state? with - | .some state => pure state - | .none => do - addTest $ assertUnreachable "Goal could not parse" - return () - - let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply PSigma.mk") with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check "apply PSigma.mk" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = - #[ - buildGoal [] "?fst" (userName? := .some "snd"), - buildGoal [] "Prop" (userName? := .some "fst") - ]) - if let #[goal1, goal2] := ← state1.serializeGoals (options := { (← read) with printExprAST := true }) then - addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})") - addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone - - let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) = - #[.some "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"]) - addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone - - let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) = - #[]) - addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome - return () def suite: IO LSpec.TestSeq := do let env: Lean.Environment ← Lean.importModules @@ -388,9 +297,7 @@ def suite: IO LSpec.TestSeq := do ("Nat.add_comm manual", proof_nat_add_comm true), ("Nat.add_comm delta", proof_delta_variable), ("arithmetic", proof_arith), - ("Or.comm", proof_or_comm), - ("2 < 5", proof_m_couple), - ("Proposition Generation", proof_proposition_generation) + ("Or.comm", proof_or_comm) ] let tests ← tests.foldlM (fun acc tests => do let (name, tests) := tests