From d72a60f4e484a74554a7dfbaf41aca1b5f2d4346 Mon Sep 17 00:00:00 2001 From: Leni Aniva 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)