Pantograph/Protocol.lean

@@ -103,7 +103,7 @@ structure StatResult where
 -- Return the type of an expression
 structure ExprEcho where
   expr: String
-  type?: Option String
+  type?: Option String := .none
   -- universe levels
   levels: Option (Array String) := .none
   deriving Lean.FromJson
@@ -217,14 +217,14 @@ structure EnvSaveLoadResult where
 
 /-- Set options; See `Options` struct above for meanings -/
 structure OptionsSet where
-  printJsonPretty?: Option Bool
-  printExprPretty?: Option Bool
-  printExprAST?: Option Bool
-  printDependentMVars?: Option Bool
-  noRepeat?: Option Bool
-  printAuxDecls?: Option Bool
-  printImplementationDetailHyps?: Option Bool
-  automaticMode?: Option Bool
+  printJsonPretty?: Option Bool := .none
+  printExprPretty?: Option Bool := .none
+  printExprAST?: Option Bool := .none
+  printDependentMVars?: Option Bool := .none
+  noRepeat?: Option Bool := .none
+  printAuxDecls?: Option Bool := .none
+  printImplementationDetailHyps?: Option Bool := .none
+  automaticMode?: Option Bool := .none
   deriving Lean.FromJson
 structure OptionsSetResult where
   deriving Lean.ToJson
@@ -236,7 +236,7 @@ structure GoalStart where
   expr: Option String     -- Directly parse in an expression
   -- universe levels
   levels: Option (Array String) := .none
-  copyFrom: Option String -- Copy the type from a theorem in the environment
+  copyFrom: Option String := .none -- Copy the type from a theorem in the environment
   deriving Lean.FromJson
 structure GoalStartResult where
   stateId: Nat := 0

Test/Integration.lean

@@ -8,23 +8,33 @@ import Test.Common
 namespace Pantograph.Test.Integration
 open Pantograph.Repl
 
-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
+deriving instance Lean.ToJson for Protocol.EnvInspect
+deriving instance Lean.ToJson for Protocol.EnvAdd
+deriving instance Lean.ToJson for Protocol.ExprEcho
+deriving instance Lean.ToJson for Protocol.OptionsSet
+deriving instance Lean.ToJson for Protocol.OptionsPrint
+deriving instance Lean.ToJson for Protocol.GoalStart
+deriving instance Lean.ToJson for Protocol.GoalPrint
+deriving instance Lean.ToJson for Protocol.GoalTactic
+deriving instance Lean.ToJson for Protocol.FrontendProcess
+
+def step { α β } [Lean.ToJson α] [Lean.ToJson β] (cmd: String) (payload: α)
+    (expected: β) (name? : Option String := .none): MainM LSpec.TestSeq := do
+  let payload := Lean.toJson payload
   let name := name?.getD s!"{cmd} {payload.compress}"
   let result ← Repl.execute { cmd, payload }
   return LSpec.test name (result.pretty = (Lean.toJson expected).pretty)
 
 abbrev Test := List (MainM LSpec.TestSeq)
 
-def test_elab : Test :=
+def test_expr_echo : Test :=
   [
     step "expr.echo"
-      [("expr", .str "λ {α : Sort (u + 1)} => List α"), ("levels", .arr #["u"])]
-     (Lean.toJson ({
+     ({ expr := "λ {α : Sort (u + 1)} => List α", levels := .some #["u"]}: Protocol.ExprEcho)
+     ({
        type := { pp? := .some "{α : Type u} → Type u" },
        expr := { pp? := .some "fun {α} => List α" }
-     }: Protocol.ExprEchoResult)),
+     }: Protocol.ExprEchoResult),
   ]
 
 def test_option_modify : Test :=
@@ -33,22 +43,22 @@ def test_option_modify : Test :=
   let module? := Option.some "Init.Data.Nat.Basic"
   let options: Protocol.Options := {}
   [
-    step "env.inspect" [("name", .str "Nat.add_one")]
+    step "env.inspect" ({ name := "Nat.add_one" } : Protocol.EnvInspect)
      ({ type := { pp? }, module? }: Protocol.EnvInspectResult),
-    step "options.set" [("printExprAST", .bool true)]
+    step "options.set" ({ printExprAST? := .some true } : Protocol.OptionsSet)
      ({ }: Protocol.OptionsSetResult),
-    step "env.inspect" [("name", .str "Nat.add_one")]
+    step "env.inspect" ({ name := "Nat.add_one" } : Protocol.EnvInspect)
      ({ type := { pp?, sexp? }, module? }: Protocol.EnvInspectResult),
-    step "options.print" []
+    step "options.print" ({} : Protocol.OptionsPrint)
      ({ options with printExprAST := true }: Protocol.Options),
   ]
 def test_malformed_command : Test :=
   let invalid := "invalid"
   [
-    step invalid [("name", .str "Nat.add_one")]
+    step invalid ({ name := "Nat.add_one" }: Protocol.EnvInspect)
      ({ error := "command", desc := s!"Unknown command {invalid}" }: Protocol.InteractionError)
      (name? := .some "Invalid Command"),
-    step "expr.echo" [(invalid, .str "Random garbage data")]
+    step "expr.echo" (Lean.Json.mkObj [(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")
@@ -69,14 +79,17 @@ def test_tactic : Test :=
     ],
   }
   [
-    step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
+    step "goal.start" ({ expr := "∀ (p q: Prop), p ∨ q → q ∨ p" }: Protocol.GoalStart)
      ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
-    step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
+    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro x" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
-    step "goal.print" [("stateId", .num 1), ("parentExpr", .bool true), ("rootExpr", .bool true)]
+    step "goal.print" ({ stateId := 1, parentExpr? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
      ({ parent? := .some { pp? := .some "fun x => ?m.11" }, }: Protocol.GoalPrintResult),
-    step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
+    step "goal.tactic" ({ stateId := 1, tactic? := .some "intro y" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
+    step "goal.tactic" ({ stateId := 1, tactic? := .some "apply Nat.le_of_succ_le" }: Protocol.GoalTactic)
+     ({ tacticErrors? := .some #["tactic 'apply' failed, failed to unify\n  ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith\n  ∀ (q : Prop), x ∨ q → q ∨ x\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }:
+      Protocol.GoalTacticResult)
   ]
 def test_automatic_mode (automatic: Bool): Test :=
   let varsPQ := #[
@@ -115,16 +128,16 @@ def test_automatic_mode (automatic: Bool): Test :=
     ],
   }
   [
-    step "options.set" [("automaticMode", .bool automatic)]
+    step "options.set" ({automaticMode? := .some automatic}: Protocol.OptionsSet)
      ({}: Protocol.OptionsSetResult),
-    step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
+    step "goal.start" ({ expr := "∀ (p q: Prop), p ∨ q → q ∨ p"} : Protocol.GoalStart)
      ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
-    step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro p q h")]
+    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro p q h" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
-    step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "cases h")]
+    step "goal.tactic" ({ stateId := 1, tactic? := .some "cases h" }: Protocol.GoalTactic)
      ({ 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")]
+    step "goal.tactic" ({ stateId := 2, tactic? := .some "apply Or.inr" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 3, goals?, }: Protocol.GoalTacticResult),
   ]
 
@@ -133,28 +146,28 @@ def test_env_add_inspect : Test :=
   let name2 := "Pantograph.mystery2"
   [
     step "env.add"
-      [
-        ("name", .str name1),
-        ("type", .str "Prop → Prop → Prop"),
-        ("value", .str "λ (a b: Prop) => Or a b"),
-        ("isTheorem", .bool false)
-      ]
+      ({
+        name := name1,
+        type := "Prop → Prop → Prop",
+        value := "λ (a b: Prop) => Or a b",
+        isTheorem := false
+      }: Protocol.EnvAdd)
      ({}: Protocol.EnvAddResult),
-    step "env.inspect" [("name", .str name1)]
+    step "env.inspect" ({name := name1, value? := .some true} : Protocol.EnvInspect)
      ({
        value? := .some { pp? := .some "fun a b => a ∨ b" },
        type := { pp? := .some "Prop → Prop → Prop" },
      }:
       Protocol.EnvInspectResult),
     step "env.add"
-      [
-        ("name", .str name2),
-        ("type", .str "Nat → Int"),
-        ("value", .str "λ (a: Nat) => a + 1"),
-        ("isTheorem", .bool false)
-      ]
+      ({
+        name := name2,
+        type := "Nat → Int",
+        value := "λ (a: Nat) => a + 1",
+        isTheorem := false
+      }: Protocol.EnvAdd)
      ({}: Protocol.EnvAddResult),
-    step "env.inspect" [("name", .str name2)]
+    step "env.inspect" ({name := name2, value? := .some true} : Protocol.EnvInspect)
      ({
        value? := .some { pp? := .some "fun a => ↑a + 1" },
        type := { pp? := .some "Nat → Int" },
@@ -167,19 +180,14 @@ example : ∀ (p: Prop), p → p := by
   exact h
 
 def test_frontend_process : Test :=
+  let file := "example : ∀ (p q: Prop), p → p ∨ q := by\n  intro p q h\n  exact Or.inl h"
+  let goal1 := "p q : Prop\nh : p\n⊢ p ∨ q"
   [
-    let file := "example : ∀ (p q: Prop), p → p ∨ q := by\n  intro p q h\n  exact Or.inl h"
-    let goal1 := "p q : Prop\nh : p\n⊢ p ∨ q"
     step "frontend.process"
-      [
-        ("file",              .str file),
-        ("invocations",       .bool true),
-        ("readHeader",        .bool false),
-        ("inheritEnv",        .bool false),
-        ("sorrys",            .bool false),
-        ("typeErrorsAsGoals", .bool false),
-        ("newConstants",      .bool false),
-      ]
+      ({
+        file? := .some file,
+        invocations := true,
+      }: Protocol.FrontendProcess)
      ({
        units := [{
          boundary := (0, file.utf8ByteSize),
@@ -215,15 +223,10 @@ def test_frontend_process_sorry : Test :=
       vars := #[{ name := "_uniq.4", userName := "p", type? := .some { pp? := .some "Prop" }}],
     }
     step "frontend.process"
-      [
-        ("file", .str file),
-        ("readHeader",        .bool false),
-        ("inheritEnv",        .bool false),
-        ("invocations", .bool false),
-        ("sorrys", .bool true),
-        ("typeErrorsAsGoals", .bool false),
-        ("newConstants", .bool false),
-      ]
+      ({
+        file? := .some file,
+        sorrys := true,
+      }: Protocol.FrontendProcess)
      ({
        units := [{
          boundary := (0, solved.utf8ByteSize),
@@ -234,7 +237,34 @@ def test_frontend_process_sorry : Test :=
          goalSrcBoundaries? := .some #[(57, 62)],
          messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
        }],
-    }: Protocol.FrontendProcessResult),
+     }: Protocol.FrontendProcessResult),
+  ]
+
+def test_import_open : Test :=
+  let header := "import Init\nopen Nat"
+  let goal1: Protocol.Goal := {
+    name := "_uniq.67",
+    target := { pp? := .some "n + 1 = n.succ" },
+    vars := #[{ name := "_uniq.66", userName := "n", type? := .some { pp? := .some "Nat" }}],
+  }
+  [
+    step "frontend.process"
+      ({
+        file? := .some header,
+        readHeader := true,
+        inheritEnv := true,
+      }: Protocol.FrontendProcess)
+     ({
+       units := [{
+         boundary := (12, header.utf8ByteSize),
+       }],
+     }: Protocol.FrontendProcessResult),
+    step "goal.start" ({ expr := "∀ (n : Nat), n + 1 = Nat.succ n"} : Protocol.GoalStart)
+     ({ stateId := 0, root := "_uniq.65" }: Protocol.GoalStartResult),
+    step "goal.tactic" ({ stateId := 0, tactic? := .some "intro n" }: Protocol.GoalTactic)
+     ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
+    step "goal.tactic" ({ stateId := 1, tactic? := .some "apply add_one" }: Protocol.GoalTactic)
+     ({ nextStateId? := .some 2, goals? := .some #[], }: Protocol.GoalTacticResult),
   ]
 
 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
@@ -246,7 +276,7 @@ def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
 
 def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
-    ("expr.echo", test_elab),
+    ("expr.echo", test_expr_echo),
     ("options.set options.print", test_option_modify),
     ("Malformed command", test_malformed_command),
     ("Tactic", test_tactic),
@@ -255,6 +285,7 @@ def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
     ("env.add env.inspect", test_env_add_inspect),
     ("frontend.process invocation", test_frontend_process),
     ("frontend.process sorry", test_frontend_process_sorry),
+    ("frontend.process import", test_import_open),
   ]
   tests.map (fun (name, test) => (name, runTest env test))