Pantograph/Test/Integration.lean

161 lines
5.8 KiB
Plaintext
Raw Normal View History

2023-08-14 21:43:40 -07:00
/- Integration test for the REPL
-/
import LSpec
import Pantograph
namespace Pantograph.Test.Integration
2023-08-14 21:43:40 -07:00
open Pantograph
def subroutine_named_step (name cmd: String) (payload: List (String × Lean.Json))
(expected: Lean.Json): MainM LSpec.TestSeq := do
2023-08-14 21:43:40 -07:00
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
2023-08-14 21:43:40 -07:00
def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := do
2023-08-14 21:43:40 -07:00
-- Setup the environment for execution
let env ← Lean.importModules
2023-10-05 17:51:41 -07:00
(imports := #[{module := Lean.Name.str .anonymous "Init", runtimeOnly := false }])
2023-08-14 21:43:40 -07:00
(opts := {})
(trustLevel := 1)
let context: Context := {
imports := ["Init"]
}
2024-03-28 00:06:35 -07:00
let coreContext: Lean.Core.Context ← createCoreContext #[]
let commands: MainM LSpec.TestSeq :=
2023-08-14 21:43:40 -07:00
steps.foldlM (λ suite step => do
let result ← step
return suite ++ result) LSpec.TestSeq.done
try
let coreM := commands.run context |>.run' {}
2023-08-14 21:43:40 -07:00
return Prod.fst $ (← coreM.toIO coreContext { env := env })
catch ex =>
return LSpec.check s!"Uncaught IO exception: {ex.toString}" false
def test_option_modify : IO LSpec.TestSeq :=
2024-03-28 00:06:35 -07:00
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)))"
2023-08-14 21:43:40 -07:00
let module? := Option.some "Init.Data.Nat.Basic"
let options: Protocol.Options := {}
2023-08-14 21:43:40 -07:00
subroutine_runner [
subroutine_step "env.inspect"
2023-08-14 21:43:40 -07:00
[("name", .str "Nat.add_one")]
(Lean.toJson ({
type := { pp? }, module? }:
Protocol.EnvInspectResult)),
2023-08-14 21:43:40 -07:00
subroutine_step "options.set"
[("printExprAST", .bool true)]
(Lean.toJson ({ }:
Protocol.OptionsSetResult)),
subroutine_step "env.inspect"
2023-08-14 21:43:40 -07:00
[("name", .str "Nat.add_one")]
(Lean.toJson ({
type := { pp?, sexp? }, module? }:
Protocol.EnvInspectResult)),
2023-08-14 21:43:40 -07:00
subroutine_step "options.print"
[]
(Lean.toJson ({ options with printExprAST := true }:
Protocol.OptionsPrintResult))
2023-08-14 21:43:40 -07:00
]
def test_malformed_command : IO LSpec.TestSeq :=
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))
]
def test_tactic : IO LSpec.TestSeq :=
let goal1: Protocol.Goal := {
2023-10-30 14:44:06 -07:00
name := "_uniq.10",
target := { pp? := .some "∀ (q : Prop), x q → q x" },
vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
}
let goal2: Protocol.Goal := {
name := "_uniq.13",
target := { pp? := .some "x y → y x" },
vars := #[
{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
{ name := "_uniq.12", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
],
}
subroutine_runner [
subroutine_step "goal.start"
[("expr", .str "∀ (p q: Prop), p q → q p")]
2023-11-06 11:51:31 -08:00
(Lean.toJson ({stateId := 0, root := "_uniq.8"}:
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)),
2024-03-06 15:14:08 -08:00
subroutine_step "goal.print"
[("stateId", .num 1)]
(Lean.toJson ({
parent? := .some { pp? := .some "fun x => ?m.11 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))
]
2023-08-14 21:43:40 -07:00
2023-12-14 11:11:24 -08:00
def test_env : IO LSpec.TestSeq :=
let name1 := "Pantograph.mystery"
let name2 := "Pantograph.mystery2"
2023-12-14 11:11:24 -08:00
subroutine_runner [
subroutine_step "env.add"
[
("name", .str name1),
2023-12-14 11:11:24 -08:00
("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)]
2023-12-14 11:11:24 -08:00
(Lean.toJson ({
value? := .some { pp? := .some "fun a b => a b" },
type := { pp? := .some "Prop → Prop → Prop" },
}:
Protocol.EnvInspectResult)),
subroutine_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 ({
2024-03-28 00:06:35 -07:00
value? := .some { pp? := .some "fun a => ↑a + 1" },
type := { pp? := .some "Nat → Int" },
2023-12-14 11:11:24 -08:00
}:
Protocol.EnvInspectResult))
]
def suite: IO LSpec.TestSeq := do
2023-08-14 21:43:40 -07:00
return LSpec.group "Integration" $
(LSpec.group "Option modify" (← test_option_modify)) ++
(LSpec.group "Malformed command" (← test_malformed_command)) ++
2023-12-14 11:11:24 -08:00
(LSpec.group "Tactic" (← test_tactic)) ++
(LSpec.group "Env" (← test_env))
2023-08-14 21:43:40 -07:00
end Pantograph.Test.Integration