2 changed files with 121 additions and 105 deletions
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@ -3,40 +3,23 @@
 import LSpec
 import Pantograph
 import Repl
+import Test.Common

 namespace Pantograph.Test.Integration
 open Pantograph

-def subroutine_named_step (name cmd: String) (payload: List (String × Lean.Json))
-    (expected: Lean.Json): MainM LSpec.TestSeq := do
-  let result ← execute { cmd := cmd, payload := Lean.Json.mkObj payload }
-  return LSpec.test name (toString result = toString expected)
-def subroutine_step (cmd: String) (payload: List (String × Lean.Json))
-    (expected: Lean.Json): MainM LSpec.TestSeq := subroutine_named_step cmd cmd payload expected
+def step { α } [Lean.ToJson α] (cmd: String) (payload: List (String × Lean.Json))
+    (expected: α) (name? : Option String := .none): MainM LSpec.TestSeq := do
+  let payload := Lean.Json.mkObj payload
+  let name := name?.getD s!"{cmd} {payload.compress}"
+  let result ← execute { cmd, payload }
+  return LSpec.test name (toString result = toString (Lean.toJson expected))

-def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := do
-  -- Setup the environment for execution
-  let env ← Lean.importModules
-    (imports := #[{module := Lean.Name.str .anonymous "Init", runtimeOnly := false }])
-    (opts := {})
-    (trustLevel := 1)
-  let context: Context := {
-    imports := ["Init"]
-  }
-  let coreContext: Lean.Core.Context ← createCoreContext #[]
-  let commands: MainM LSpec.TestSeq :=
-    steps.foldlM (λ suite step => do
-      let result ← step
-      return suite ++ result) LSpec.TestSeq.done
-  try
-    let coreM := commands.run context |>.run' {}
-    return Prod.fst $ (← coreM.toIO coreContext { env := env })
-  catch ex =>
-    return LSpec.check s!"Uncaught IO exception: {ex.toString}" false
+abbrev Test := List (MainM LSpec.TestSeq)

-def test_elab : IO LSpec.TestSeq :=
-  subroutine_runner [
-    subroutine_step "expr.echo"
+def test_elab : Test :=
+  [
+    step "expr.echo"
      [("expr", .str "λ {α : Sort (u + 1)} => List α"), ("levels", .arr #["u"])]
     (Lean.toJson ({
       type := { pp? := .some "{α : Type u} → Type u" },
@ -44,46 +27,33 @@ def test_elab : IO LSpec.TestSeq :=
     }: Protocol.ExprEchoResult)),
  ]

-def test_option_modify : IO LSpec.TestSeq :=
+def test_option_modify : Test :=
  let pp? := Option.some "∀ (n : Nat), n + 1 = n.succ"
  let sexp? := Option.some "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))"
  let module? := Option.some "Init.Data.Nat.Basic"
  let options: Protocol.Options := {}
-  subroutine_runner [
-    subroutine_step "env.inspect"
-      [("name", .str "Nat.add_one")]
-     (Lean.toJson ({
-       type := { pp? }, module? }:
-      Protocol.EnvInspectResult)),
-    subroutine_step "options.set"
-      [("printExprAST", .bool true)]
-     (Lean.toJson ({ }:
-      Protocol.OptionsSetResult)),
-    subroutine_step "env.inspect"
-      [("name", .str "Nat.add_one")]
-     (Lean.toJson ({
-       type := { pp?, sexp? }, module? }:
-      Protocol.EnvInspectResult)),
-    subroutine_step "options.print"
-      []
-     (Lean.toJson ({ options with printExprAST := true }:
-      Protocol.Options))
+  [
+    step "env.inspect" [("name", .str "Nat.add_one")]
+     ({ type := { pp? }, module? }: Protocol.EnvInspectResult),
+    step "options.set" [("printExprAST", .bool true)]
+     ({ }: Protocol.OptionsSetResult),
+    step "env.inspect" [("name", .str "Nat.add_one")]
+     ({ type := { pp?, sexp? }, module? }: Protocol.EnvInspectResult),
+    step "options.print" []
+     ({ options with printExprAST := true }: Protocol.Options),
  ]
-def test_malformed_command : IO LSpec.TestSeq :=
+def test_malformed_command : Test :=
  let invalid := "invalid"
-  subroutine_runner [
-    subroutine_named_step "Invalid command" invalid
-      [("name", .str "Nat.add_one")]
-     (Lean.toJson ({
-       error := "command", desc := s!"Unknown command {invalid}"}:
-      Protocol.InteractionError)),
-    subroutine_named_step "JSON Deserialization" "expr.echo"
-      [(invalid, .str "Random garbage data")]
-     (Lean.toJson ({
-       error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected"}:
-      Protocol.InteractionError))
+  [
+    step invalid [("name", .str "Nat.add_one")]
+     ({ error := "command", desc := s!"Unknown command {invalid}" }: Protocol.InteractionError)
+     (name? := .some "Invalid Command"),
+    step "expr.echo" [(invalid, .str "Random garbage data")]
+     ({ error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected" }:
+      Protocol.InteractionError)
+    (name? := .some "JSON Deserialization")
  ]
-def test_tactic : IO LSpec.TestSeq :=
+def test_tactic : Test :=
  let goal1: Protocol.Goal := {
    name := "_uniq.11",
    target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
@ -97,77 +67,123 @@ def test_tactic : IO LSpec.TestSeq :=
      { name := "_uniq.16", userName := "y", type? := .some { pp? := .some "Prop" }}
    ],
  }
-  subroutine_runner [
-    subroutine_step "goal.start"
-      [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
-     (Lean.toJson ({stateId := 0, root := "_uniq.9"}:
-      Protocol.GoalStartResult)),
-    subroutine_step "goal.tactic"
-      [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
-     (Lean.toJson ({
-       nextStateId? := .some 1,
-       goals? := #[goal1],
-     }:
-      Protocol.GoalTacticResult)),
-    subroutine_step "goal.print"
-      [("stateId", .num 1)]
-     (Lean.toJson ({
-       parent? := .some { pp? := .some "fun x => ?m.12 x" },
-     }:
-      Protocol.GoalPrintResult)),
-    subroutine_step "goal.tactic"
-      [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
-     (Lean.toJson ({
-       nextStateId? := .some 2,
-       goals? := #[goal2],
-     }:
-      Protocol.GoalTacticResult))
+  [
+    step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
+     ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
+    step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
+     ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
+    step "goal.print" [("stateId", .num 1)]
+     ({ parent? := .some { pp? := .some "fun x => ?m.12 x" }, }: Protocol.GoalPrintResult),
+    step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
+     ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
+  ]
+def test_automatic_mode (automatic: Bool): Test :=
+  let varsPQ := #[
+    { name := "_uniq.10", userName := "p", type? := .some { pp? := .some "Prop" }},
+    { name := "_uniq.13", userName := "q", type? := .some { pp? := .some "Prop" }}
+  ]
+  let goal1: Protocol.Goal := {
+    name := "_uniq.17",
+    target := { pp? := .some "q ∨ p" },
+    vars := varsPQ ++ #[
+      { name := "_uniq.16", userName := "h", type? := .some { pp? := .some "p ∨ q" }}
+    ],
+  }
+  let goal2l: Protocol.Goal := {
+    name := "_uniq.59",
+    userName? := .some "inl",
+    target := { pp? := .some "q ∨ p" },
+    vars := varsPQ ++ #[
+      { name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
+    ],
+  }
+  let goal2r: Protocol.Goal := {
+    name := "_uniq.72",
+    userName? := .some "inr",
+    target := { pp? := .some "q ∨ p" },
+    vars := varsPQ ++ #[
+      { name := "_uniq.60", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true}
+    ],
+  }
+  let goal3l: Protocol.Goal := {
+    name := "_uniq.78",
+    userName? := .some "inl.h",
+    target := { pp? := .some "p" },
+    vars := varsPQ ++ #[
+      { name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
+    ],
+  }
+  [
+    step "options.set" [("automaticMode", .bool automatic)]
+     ({}: Protocol.OptionsSetResult),
+    step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
+     ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
+    step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro p q h")]
+     ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
+    step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "cases h")]
+     ({ nextStateId? := .some 2, goals? := #[goal2l, goal2r], }: Protocol.GoalTacticResult),
+    let goals? := if automatic then #[goal3l, goal2r] else #[goal3l]
+    step "goal.tactic" [("stateId", .num 2), ("goalId", .num 0), ("tactic", .str "apply Or.inr")]
+     ({ nextStateId? := .some 3, goals?, }: Protocol.GoalTacticResult),
  ]

-def test_env_add_inspect : IO LSpec.TestSeq :=
+def test_env_add_inspect : Test :=
  let name1 := "Pantograph.mystery"
  let name2 := "Pantograph.mystery2"
-  subroutine_runner [
-    subroutine_step "env.add"
+  [
+    step "env.add"
      [
        ("name", .str name1),
        ("type", .str "Prop → Prop → Prop"),
        ("value", .str "λ (a b: Prop) => Or a b"),
        ("isTheorem", .bool false)
      ]
-     (Lean.toJson ({}: Protocol.EnvAddResult)),
-    subroutine_step "env.inspect"
-      [("name", .str name1)]
-     (Lean.toJson ({
+     ({}: Protocol.EnvAddResult),
+    step "env.inspect" [("name", .str name1)]
+     ({
       value? := .some { pp? := .some "fun a b => a ∨ b" },
       type := { pp? := .some "Prop → Prop → Prop" },
     }:
-      Protocol.EnvInspectResult)),
-    subroutine_step "env.add"
+      Protocol.EnvInspectResult),
+    step "env.add"
      [
        ("name", .str name2),
        ("type", .str "Nat → Int"),
        ("value", .str "λ (a: Nat) => a + 1"),
        ("isTheorem", .bool false)
      ]
-     (Lean.toJson ({}: Protocol.EnvAddResult)),
-    subroutine_step "env.inspect"
-      [("name", .str name2)]
-     (Lean.toJson ({
+     ({}: Protocol.EnvAddResult),
+    step "env.inspect" [("name", .str name2)]
+     ({
       value? := .some { pp? := .some "fun a => ↑a + 1" },
       type := { pp? := .some "Nat → Int" },
     }:
-      Protocol.EnvInspectResult))
+      Protocol.EnvInspectResult)
  ]

-def suite: List (String × IO LSpec.TestSeq) :=
-  [
-    ("Elab", test_elab),
-    ("Option modify", test_option_modify),
+def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
+  -- Setup the environment for execution
+  let context: Context := {
+    imports := ["Init"]
+  }
+  let commands: MainM LSpec.TestSeq :=
+    steps.foldlM (λ suite step => do
+      let result ← step
+      return suite ++ result) LSpec.TestSeq.done
+  runCoreMSeq env <| commands.run context |>.run' {}
+
+
+def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
+  let tests := [
+    ("expr.echo", test_elab),
+    ("options.set options.print", test_option_modify),
    ("Malformed command", test_malformed_command),
    ("Tactic", test_tactic),
+    ("Manual Mode", test_automatic_mode false),
+    ("Automatic Mode", test_automatic_mode true),
    ("env.add env.inspect", test_env_add_inspect),
  ]
+  tests.map (fun (name, test) => (name, runTest env test))


 end Pantograph.Test.Integration
--- a/Test/Main.lean
+++ b/Test/Main.lean
@ -44,7 +44,7 @@ def main (args: List String) := do

  let suites: List (String × List (String × IO LSpec.TestSeq)) := [
    ("Environment", Environment.suite),
-    ("Integration", Integration.suite),
+    ("Integration", Integration.suite env_default),
    ("Library", Library.suite env_default),
    ("Metavar", Metavar.suite env_default),
    ("Proofs", Proofs.suite env_default),