diff --git a/Test/Common.lean b/Test/Common.lean index 3998293..ce21ce8 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -130,6 +130,8 @@ def addTest [Monad m] (test: LSpec.TestSeq): TestT m Unit := do def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq := Prod.snd <$> t.run LSpec.TestSeq.done +def runTestWithResult { α } [Monad m] (t: TestT m α): m (α × LSpec.TestSeq) := + t.run LSpec.TestSeq.done def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit): IO LSpec.TestSeq := diff --git a/Test/Main.lean b/Test/Main.lean index 25bb0d9..6bf410e 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -1,11 +1,12 @@ import LSpec +import Test.Delate import Test.Environment import Test.Frontend import Test.Integration import Test.Library import Test.Metavar import Test.Proofs -import Test.Delate +import Test.Serial import Test.Tactic -- Test running infrastructure @@ -51,6 +52,7 @@ def main (args: List String) := do ("Metavar", Metavar.suite env_default), ("Proofs", Proofs.suite env_default), ("Delate", Delate.suite env_default), + ("Serial", Serial.suite env_default), ("Tactic/Congruence", Tactic.Congruence.suite env_default), ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default), ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default), diff --git a/Test/Serial.lean b/Test/Serial.lean new file mode 100644 index 0000000..4cca464 --- /dev/null +++ b/Test/Serial.lean @@ -0,0 +1,56 @@ +import LSpec +import Test.Common +import Lean +import Pantograph.Library + +open Lean + +namespace Pantograph.Test.Serial + +structure MultiState where + coreContext : Core.Context + coreStates : Array Core.State + +abbrev TestM := StateRefT MultiState $ TestT $ EIO LSpec.TestSeq + +def runCoreM { α } (id : Nat) (testCoreM: TestT CoreM α) : TestM α := do + let multiState ← get + let state ← match multiState.coreStates[id]? with + | .some state => pure state + | .none => + let test := LSpec.test "Invalid index" (id < multiState.coreStates.size) + throw test + let coreM := runTestWithResult testCoreM + match ← (coreM.run' multiState.coreContext state).toBaseIO with + | .error _ => do + let test := LSpec.test "Exception" false + throw test + | .ok (a, tests) => do + set $ (← getThe LSpec.TestSeq) ++ tests + return a + +def simple : TestM Unit := do + return + +structure Test where + name : String + nInstances : Nat + routine: TestM Unit + +protected def Test.run (test: Test) (env: Lean.Environment) : IO LSpec.TestSeq := do + -- Create the state + let state : MultiState := { + coreContext := ← createCoreContext #[], + coreStates := Array.range test.nInstances |>.map λ _ => { env }, + } + match ← (runTest $ test.routine.run' state).toBaseIO with + | .ok e => return e + | .error e => return e + +def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) := + let tests: List Test := [ + { name := "simple", nInstances := 2, routine := simple } + ] + tests.map (fun test => (test.name, test.run env)) + +end Pantograph.Test.Serial