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 :=

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),

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