From 2130bcf3576912c7a4f6750dab8958d5a2dd2551 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 31 Mar 2024 16:43:30 -0700
Subject: [PATCH] test: Library test

---
 Pantograph.lean          |  2 +-
 Pantograph/Protocol.lean |  2 +-
 Test/Common.lean         |  7 +++++--
 Test/Library.lean        | 35 +++++++++++++++++++++++++++++++++++
 Test/Main.lean           |  8 +++++---
 5 files changed, 47 insertions(+), 7 deletions(-)
 create mode 100644 Test/Library.lean

diff --git a/Pantograph.lean b/Pantograph.lean
index 1def945..97f03f4 100644
--- a/Pantograph.lean
+++ b/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
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 7a2b341..6ee3354 100644
--- a/Pantograph/Protocol.lean
+++ b/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
diff --git a/Test/Common.lean b/Test/Common.lean
index 2e7149d..378dce8 100644
--- a/Test/Common.lean
+++ b/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}" = "")
diff --git a/Test/Library.lean b/Test/Library.lean
new file mode 100644
index 0000000..265335a
--- /dev/null
+++ b/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
diff --git a/Test/Main.lean b/Test/Main.lean
index d24f45f..6baffad 100644
--- a/Test/Main.lean
+++ b/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