Pantograph.lean

@@ -71,7 +71,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     Environment.addDecl args
   expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
     let state ← get
-    exprEcho args.expr args.type state.options
+    exprEcho args.expr args.type? state.options
   options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
     let state ← get
     let options := state.options

Pantograph/Protocol.lean

@@ -98,7 +98,7 @@ structure StatResult where
 -- Return the type of an expression
 structure ExprEcho where
   expr: String
-  type: Option String
+  type?: Option String
   deriving Lean.FromJson
 structure ExprEchoResult where
   expr: Expression

Test/Common.lean

@@ -24,6 +24,9 @@ def Goal.devolatilize (goal: Goal): Goal :=
 deriving instance DecidableEq, Repr for Expression
 deriving instance DecidableEq, Repr for Variable
 deriving instance DecidableEq, Repr for Goal
+deriving instance DecidableEq, Repr for ExprEchoResult
+deriving instance DecidableEq, Repr for InteractionError
+deriving instance DecidableEq, Repr for Option
 end Protocol
 
 def TacticResult.toString : TacticResult → String
@@ -38,8 +41,8 @@ def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message fa
 
 open Lean
 
-def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq): IO LSpec.TestSeq := do
-  let coreContext: Core.Context ← createCoreContext #[]
+def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array String := #[]): IO LSpec.TestSeq := do
+  let coreContext: Core.Context ← createCoreContext options
   match ← (coreM.run' coreContext { env := env }).toBaseIO with
   | .error exception =>
     return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")

Test/Library.lean

@@ -0,0 +1,35 @@
+import LSpec
+import Lean
+import Pantograph.Library
+import Test.Common
+
+open Lean
+open Pantograph
+
+namespace Pantograph.Test.Library
+
+def test_expr_echo: IO LSpec.TestSeq := do
+  let env: Environment ← importModules
+    (imports := #[`Init])
+    (opts := {})
+    (trustLevel := 1)
+  let inner: CoreM LSpec.TestSeq := do
+    let prop_and_proof := "⟨∀ (x: Prop), x → x, λ (x: Prop) (h: x) => h⟩"
+    let tests := LSpec.TestSeq.done
+    let echoResult ← exprEcho prop_and_proof (options := {})
+    let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
+      type := { pp? := "?m.2" }, expr := { pp? := "?m.3" }
+    }))
+    let echoResult ← exprEcho prop_and_proof (expectedType? := .some "Σ' p:Prop, p") (options := {})
+    let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
+      type := { pp? := "(p : Prop) ×' p" }, expr := { pp? := "⟨∀ (x : Prop), x → x, fun x h => h⟩" }
+    }))
+    return tests
+  runCoreMSeq env (options := #["pp.proofs.threshold=100"]) inner
+
+def suite: IO LSpec.TestSeq := do
+
+  return LSpec.group "Library" $
+    (LSpec.group "ExprEcho" (← test_expr_echo))
+
+end Pantograph.Test.Library

Test/Main.lean

@@ -1,7 +1,8 @@
 import LSpec
 import Test.Environment
-import Test.Metavar
 import Test.Integration
+import Test.Library
+import Test.Metavar
 import Test.Proofs
 import Test.Serial
 
@@ -11,11 +12,12 @@ def main := do
   Lean.initSearchPath (← Lean.findSysroot)
 
   let suites := [
-    Metavar.suite,
+    Environment.suite,
     Integration.suite,
+    Library.suite,
+    Metavar.suite,
     Proofs.suite,
     Serial.suite,
-    Environment.suite
   ]
   let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done
   LSpec.lspecIO $ all