Merge pull request 'fix: Auto bound implicit in elab' () from elab/level into dev

Reviewed-on: 
This commit is contained in:
Leni Aniva 2024-04-06 22:04:31 -07:00
commit 013cb8bb57
4 changed files with 30 additions and 15 deletions

View File

@ -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 }

View File

@ -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

View File

@ -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),

View File

@ -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)