From 5a60ca74d5a455716f05efdba5d6113f97f96c81 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 6 Apr 2024 17:45:36 -0700
Subject: [PATCH] fix: Auto bound implicit in elab

---
 Pantograph/Library.lean | 10 ++++++----
 Test/Common.lean        | 12 ++++--------
 Test/Integration.lean   | 11 +++++++++++
 Test/Serial.lean        | 12 +++++++++---
 4 files changed, 30 insertions(+), 15 deletions(-)

diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index d36866a..bf8a014 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -36,13 +36,15 @@ end Lean
 
 namespace Pantograph
 
+def defaultTermElabMContext: Lean.Elab.Term.Context := {
+    autoBoundImplicit := true,
+    declName? := some "_pantograph".toName,
+    errToSorry := false
+  }
 def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α :=
   metaM.run'
 def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α :=
-  termElabM.run' (ctx := {
-    declName? := .none,
-    errToSorry := false,
-  }) |>.run'
+  termElabM.run' (ctx := defaultTermElabMContext) |>.run'
 
 def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
 
diff --git a/Test/Common.lean b/Test/Common.lean
index 9c13a6d..6fa858b 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -43,6 +43,9 @@ namespace Test
 def expectationFailure (desc: String) (error: String): LSpec.TestSeq := LSpec.test desc (LSpec.ExpectationFailure "ok _" error)
 def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false
 
+def parseFailure (error: String) := expectationFailure "parse" error
+def elabFailure (error: String) := expectationFailure "elab" error
+
 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
@@ -52,15 +55,8 @@ def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array
 def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq :=
   runCoreMSeq env metaM.run'
 def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
-  termElabM.run' (ctx := {
-    declName? := .none,
-    errToSorry := false,
-  })
+  termElabM.run' (ctx := Pantograph.defaultTermElabMContext)
 
-def defaultTermElabMContext: Lean.Elab.Term.Context := {
-    declName? := some "_pantograph".toName,
-    errToSorry := false
-  }
 end Test
 
 end Pantograph
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 4f3bcba..29cb82d 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -32,6 +32,16 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d
   catch ex =>
     return LSpec.check s!"Uncaught IO exception: {ex.toString}" false
 
+def test_elab : IO LSpec.TestSeq :=
+  subroutine_runner [
+    subroutine_step "expr.echo"
+      [("expr", .str "λ {α : Sort (u + 1)} => List α")]
+     (Lean.toJson ({
+       type := { pp? := .some "{α : Type u} → Type u" },
+       expr := { pp? := .some "fun {α} => List α" }
+     }: Protocol.ExprEchoResult)),
+  ]
+
 def test_option_modify : IO LSpec.TestSeq :=
   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)))"
@@ -150,6 +160,7 @@ def test_env_add_inspect : IO LSpec.TestSeq :=
 
 def suite: List (String × IO LSpec.TestSeq) :=
   [
+    ("Elab", test_elab),
     ("Option modify", test_option_modify),
     ("Malformed command", test_malformed_command),
     ("Tactic", test_tactic),
diff --git a/Test/Serial.lean b/Test/Serial.lean
index 0a46acc..15761c5 100644
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@@ -51,12 +51,18 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
 def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
   let entries: List (String × String) := [
     ("λ x: Nat × Bool => x.1", "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"),
-    ("λ x: Array Nat => x.data", "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))")
+    ("λ x: Array Nat => x.data", "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"),
+    -- This tests `autoBoundImplicit`
+    ("λ {α : Sort (u + 1)} => List α", "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"),
   ]
   let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do
     let env ← MonadEnv.getEnv
-    let s := parseTerm env source |>.toOption |>.get!
-    let expr := (← elabTerm s) |>.toOption |>.get!
+    let s ← match parseTerm env source with
+      | .ok s => pure s
+      | .error e => return parseFailure e
+    let expr ← match (← elabTerm s) with
+      | .ok expr => pure expr
+      | .error e => return elabFailure e
     let test := LSpec.check source ((← serialize_expression_ast expr) = target)
     return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
   let metaM := termElabM.run' (ctx := defaultTermElabMContext)