fix: Auto bound implicit in elab
This commit is contained in:
parent
d44693e548
commit
d72a60f4e4
|
@ -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 }
|
||||
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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),
|
||||
|
|
|
@ -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)
|
||||
|
|
Loading…
Reference in New Issue