269 lines
10 KiB
Lean4
269 lines
10 KiB
Lean4
import BidirTT
|
|
|
|
open BidirTT
|
|
|
|
inductive Expectation where
|
|
| okTy : Tm → Expectation
|
|
| okTyNorm : Tm → Tm → Expectation
|
|
| errContains : String → Expectation
|
|
|
|
private def renderType (ty : Val) : Except String Tm :=
|
|
BidirTT.quote 0 ty
|
|
|
|
private def renderNormal (tm : Tm) : Except String Tm := do
|
|
let v ← eval [] tm
|
|
quote 0 v
|
|
|
|
private def containsText (haystack needle : String) : Bool :=
|
|
needle.isEmpty || (haystack.splitOn needle).length > 1
|
|
|
|
structure TestCase where
|
|
name : String
|
|
input : Raw
|
|
expect : Expectation
|
|
|
|
def cases : List TestCase := [
|
|
⟨"U0 is typed by U1", Examples.univ0,
|
|
.okTy (.univ 1)⟩,
|
|
⟨"U(max 0 1) is typed by U2", Examples.univMax,
|
|
.okTy (.univ 2)⟩,
|
|
⟨"U0 subsumes into U2", .ann (.univ 0) (.univ 2),
|
|
.okTy (.univ 2)⟩,
|
|
⟨"U0 subsumes into U(max 0 2)", .ann (.univ 0) (.univ (.max 0 2)),
|
|
.okTy (.univ 2)⟩,
|
|
⟨"Nat is typed by U0", .nat,
|
|
.okTy (.univ 0)⟩,
|
|
⟨"succ zero infers Nat", (.succ .zero),
|
|
.okTy .nat⟩,
|
|
⟨"id typechecks", Examples.idAnn,
|
|
.okTy (.pi (.univ 0) (.pi (.var 0) (.var 1)))⟩,
|
|
⟨"Pi subsumption is contravariant in the domain", .ann
|
|
(.ann
|
|
(.lam "A" (.var "A"))
|
|
(.pi "A" (.univ 1) (.univ 1)))
|
|
(.pi "A" (.univ 0) (.univ 2)),
|
|
.okTy (.pi (.univ 0) (.univ 2))⟩,
|
|
⟨"const typechecks", Examples.constAnn,
|
|
.okTy (.pi (.univ 0) (.pi (.univ 0) (.pi (.var 1) (.pi (.var 1) (.var 3)))))⟩,
|
|
⟨"swap typechecks", Examples.swapAnn,
|
|
.okTy (.pi (.univ 0) (.pi (.univ 0) (.pi (.sig (.var 1) (.var 1)) (.sig (.var 1) (.var 3)))))⟩,
|
|
⟨"dependent pair typechecks", Examples.depPairAnn,
|
|
.okTy (.sig (.univ 2) (.var 0))⟩,
|
|
⟨"dependent pair subsumes into a lifted Sigma", .ann Examples.depPairAnn
|
|
(.sig "A" (.univ 3) (.var "A")),
|
|
.okTy (.sig (.univ 3) (.var 0))⟩,
|
|
⟨"natElim computes on numerals", Examples.natFoldId,
|
|
.okTyNorm .nat (.succ (.succ .zero))⟩,
|
|
⟨"unitElim computes on tt", Examples.unitToNat,
|
|
.okTyNorm .nat (.succ (.succ .zero))⟩,
|
|
⟨"emptyElim builds absurd maps", Examples.absurdNat,
|
|
.okTy (.pi .empty .nat)⟩,
|
|
⟨"refl inhabits reflexive identity", Examples.reflZero,
|
|
.okTyNorm (.id .nat .zero .zero) .refl⟩,
|
|
⟨"idElim computes on refl", Examples.idElimNat,
|
|
.okTyNorm .nat .zero⟩,
|
|
⟨"transport combinator typechecks", Examples.transportNat,
|
|
.okTy (.pi .nat (.pi .nat (.pi (.id .nat (.var 1) (.var 0)) (.pi .nat .nat))))⟩,
|
|
⟨"transport computes on refl", Examples.transportNatRefl,
|
|
.okTyNorm .nat (.succ (.succ .zero))⟩,
|
|
⟨"congruence combinator typechecks", Examples.congSucc,
|
|
.okTy (.pi .nat (.pi .nat (.pi (.id .nat (.var 1) (.var 0)) (.id .nat (.succ (.var 2)) (.succ (.var 1))))))⟩,
|
|
⟨"congruence computes on refl", Examples.congSuccRefl,
|
|
.okTyNorm (.id .nat (.succ .zero) (.succ .zero)) .refl⟩,
|
|
⟨"fst infers the first projection", Examples.fstDepPair,
|
|
.okTy (.univ 2)⟩,
|
|
⟨"snd infers the dependent second projection", Examples.sndDepPair,
|
|
.okTy (.univ 1)⟩,
|
|
⟨"let infers through definitions", Examples.letUniverse,
|
|
.okTy (.univ 1)⟩,
|
|
⟨"bad succ rejected", Examples.badSucc,
|
|
.errContains "type mismatch: expected Nat, got U1"⟩,
|
|
⟨"self application rejected", Examples.omegaAnn,
|
|
.errContains "expected Pi type in application"⟩,
|
|
⟨"unknown variable rejected", Examples.unknownVar,
|
|
.errContains "unknown variable nope"⟩,
|
|
⟨"pair mismatch rejected at the Sigma body", Examples.pairMismatch,
|
|
.errContains "type mismatch: expected U1, got U2"⟩,
|
|
⟨"bad fst rejected", Examples.badFst,
|
|
.errContains "expected Sigma type in .1, got U1"⟩,
|
|
⟨"bad refl rejected", Examples.badRefl,
|
|
.errContains "refl cannot inhabit"⟩
|
|
]
|
|
|
|
def runCase (tc : TestCase) : IO Bool := do
|
|
match tc.expect, checkTop tc.input with
|
|
| .okTy expectedTy, .ok (_, ty) =>
|
|
match renderType ty with
|
|
| Except.ok actualTy =>
|
|
if actualTy == expectedTy then
|
|
IO.println s!"pass {tc.name}"
|
|
pure true
|
|
else
|
|
IO.println s!"fail {tc.name} (expected type {BidirTT.prettyTm expectedTy}, got {BidirTT.prettyTm actualTy})"
|
|
pure false
|
|
| Except.error err =>
|
|
IO.println s!"fail {tc.name} (could not quote type: {err})"
|
|
pure false
|
|
| .okTyNorm expectedTy expectedNf, .ok (tm, ty) =>
|
|
match renderType ty, renderNormal tm with
|
|
| Except.ok actualTy, Except.ok actualNf =>
|
|
if actualTy == expectedTy && actualNf == expectedNf then
|
|
IO.println s!"pass {tc.name}"
|
|
pure true
|
|
else if actualTy != expectedTy then
|
|
IO.println s!"fail {tc.name} (expected type {BidirTT.prettyTm expectedTy}, got {BidirTT.prettyTm actualTy})"
|
|
pure false
|
|
else
|
|
IO.println s!"fail {tc.name} (expected nf {BidirTT.prettyTm expectedNf}, got {BidirTT.prettyTm actualNf})"
|
|
pure false
|
|
| Except.error err, _ =>
|
|
IO.println s!"fail {tc.name} (could not quote type: {err})"
|
|
pure false
|
|
| _, Except.error err =>
|
|
IO.println s!"fail {tc.name} (could not normalize term: {err})"
|
|
pure false
|
|
| .okTy expectedTy, .error err =>
|
|
IO.println s!"fail {tc.name} (expected type {BidirTT.prettyTm expectedTy}, got error {err})"
|
|
pure false
|
|
| .okTyNorm expectedTy _, .error err =>
|
|
IO.println s!"fail {tc.name} (expected type {BidirTT.prettyTm expectedTy}, got error {err})"
|
|
pure false
|
|
| .errContains needle, .error err =>
|
|
if containsText err needle then
|
|
IO.println s!"pass {tc.name}"
|
|
pure true
|
|
else
|
|
IO.println s!"fail {tc.name} (expected error containing {needle}, got {err})"
|
|
pure false
|
|
| .errContains needle, .ok (_, ty) =>
|
|
match renderType ty with
|
|
| Except.ok actualTy =>
|
|
IO.println s!"fail {tc.name} (expected error containing {needle}, got type {BidirTT.prettyTm actualTy})"
|
|
pure false
|
|
| Except.error err =>
|
|
IO.println s!"fail {tc.name} (expected error containing {needle}, got quote failure {err})"
|
|
pure false
|
|
|
|
def runInternalSafetyChecks : IO Bool := do
|
|
let malformedEvalOk :=
|
|
match eval [] (.var 0) with
|
|
| Except.error err => containsText err "bad de Bruijn index 0"
|
|
| Except.ok _ => false
|
|
let malformedQuoteOk :=
|
|
match quote 0 (.neu (.var 0)) with
|
|
| Except.error err => containsText err "bad level 0"
|
|
| Except.ok _ => false
|
|
if malformedEvalOk && malformedQuoteOk then
|
|
IO.println "pass malformed core terms are rejected safely"
|
|
pure true
|
|
else
|
|
IO.println "fail malformed core terms are rejected safely"
|
|
pure false
|
|
|
|
def runNeutralRepresentationChecks : IO Bool := do
|
|
let stuckAppOk :=
|
|
match vApp (.neu (.var 0)) .zero with
|
|
| Except.ok (.neu (.app (.var 0) .zero)) => true
|
|
| _ => false
|
|
let stuckNatElimOk :=
|
|
match vNatElim .nat .zero (.neu (.var 1)) (.neu (.var 0)) with
|
|
| Except.ok (.neu (.natElim .nat .zero (.neu (.var 1)) (.var 0))) => true
|
|
| _ => false
|
|
if stuckAppOk && stuckNatElimOk then
|
|
IO.println "pass stuck eliminators stay in the neutral fragment"
|
|
pure true
|
|
else
|
|
IO.println "fail stuck eliminators stay in the neutral fragment"
|
|
pure false
|
|
|
|
def runContextInvariantChecks : IO Bool := do
|
|
let cxt :=
|
|
(Cxt.empty.bind "A" (.univ 0)).define "x" .zero .nat
|
|
let wfOk := Cxt.isWellFormed cxt
|
|
let lookupOk :=
|
|
match cxt.lookup "x", cxt.lookup "A" with
|
|
| some (ix, tx), some (iA, tA) =>
|
|
ix.val == 0 &&
|
|
iA.val == 1 &&
|
|
(match tx with | .nat => true | _ => false) &&
|
|
(match tA with | .univ 0 => true | _ => false)
|
|
| _, _ =>
|
|
false
|
|
let indexedOk :=
|
|
let latest : Fin cxt.lvl := ⟨0, by decide⟩
|
|
let outer : Fin cxt.lvl := ⟨1, by decide⟩
|
|
(match cxt.typeAt latest with
|
|
| ("x", .nat) => true
|
|
| _ => false) &&
|
|
(match cxt.typeAt outer with
|
|
| ("A", .univ 0) => true
|
|
| _ => false) &&
|
|
(match cxt.valueAt latest with
|
|
| .zero => true
|
|
| _ => false) &&
|
|
(match cxt.valueAt outer with
|
|
| .neu (.var 0) => true
|
|
| _ => false)
|
|
if wfOk && lookupOk && indexedOk then
|
|
IO.println "pass context lookup is indexed and scope invariants hold"
|
|
pure true
|
|
else
|
|
IO.println "fail context lookup is indexed and scope invariants hold"
|
|
pure false
|
|
|
|
def runLevelSolverChecks : IO Bool := do
|
|
let satOk :=
|
|
match solveLevelConstraints [(.max 0 1, 1), (1, .succ 1)] with
|
|
| Except.ok _ => true
|
|
| Except.error _ => false
|
|
let unsatOk :=
|
|
match solveLevelConstraints [(.succ 1, 1)] with
|
|
| Except.error err => containsText err "unsatisfiable level constraint"
|
|
| Except.ok _ => false
|
|
if satOk && unsatOk then
|
|
IO.println "pass level constraints are solved consistently"
|
|
pure true
|
|
else
|
|
IO.println "fail level constraints are solved consistently"
|
|
pure false
|
|
|
|
def runPrettyPrinterChecks : IO Bool := do
|
|
match checkTop Examples.idAnn with
|
|
| .ok (tm, ty) =>
|
|
match renderType ty with
|
|
| Except.ok qty =>
|
|
let termText := BidirTT.prettyTm tm
|
|
let typeText := BidirTT.prettyTm qty
|
|
let ok :=
|
|
containsText termText "fun x0 =>" &&
|
|
containsText typeText "Pi (x0 : U0)" &&
|
|
!containsText typeText "#"
|
|
if ok then
|
|
IO.println "pass pretty printer rehydrates binder names"
|
|
pure true
|
|
else
|
|
IO.println s!"fail pretty printer rehydrates binder names (term: {termText}, type: {typeText})"
|
|
pure false
|
|
| Except.error err =>
|
|
IO.println s!"fail pretty printer rehydrates binder names (could not quote type: {err})"
|
|
pure false
|
|
| .error err =>
|
|
IO.println s!"fail pretty printer rehydrates binder names (could not elaborate fixture: {err})"
|
|
pure false
|
|
|
|
def main : IO UInt32 := do
|
|
let results ← cases.mapM runCase
|
|
let safetyOk ← runInternalSafetyChecks
|
|
let neutralOk ← runNeutralRepresentationChecks
|
|
let contextOk ← runContextInvariantChecks
|
|
let levelOk ← runLevelSolverChecks
|
|
let prettyOk ← runPrettyPrinterChecks
|
|
let allResults := results ++ [safetyOk, neutralOk, contextOk, levelOk, prettyOk]
|
|
let failed := allResults.countP (· == false)
|
|
if failed == 0 then
|
|
IO.println s!"\n{allResults.length} passed, 0 failed"
|
|
pure 0
|
|
else
|
|
IO.println s!"\n{allResults.length - failed} passed, {failed} failed"
|
|
pure 1
|