import BidirTT

open BidirTT

def runOne (label : String) (r : Raw) : IO Unit := do
  match checkTop r with
  | .ok (t, ty) =>
      IO.println s!"[ok]   {label}"
      IO.println s!"  term : {BidirTT.prettyTm t}"
      match quote 0 ty with
      | Except.ok qt =>
          IO.println s!"  type : {BidirTT.prettyTm qt}"
      | Except.error err =>
          IO.println s!"  type : <error: {err}>"
  | .error e =>
      IO.println s!"[err]  {label}: {e}"

def main : IO Unit := do
  runOne "U0"            Examples.univ0
  runOne "id"            Examples.idAnn
  runOne "const"         Examples.constAnn
  runOne "swap"          Examples.swapAnn
  runOne "depPair"       Examples.depPairAnn
  runOne "depPair.1"     Examples.fstDepPair
  runOne "depPair.2"     Examples.sndDepPair
  runOne "nat fold id"   Examples.natFoldId
  runOne "unit elim"     Examples.unitToNat
  runOne "empty absurd"  Examples.absurdNat
  runOne "refl zero"     Examples.reflZero
  runOne "id elim"       Examples.idElimNat
  runOne "transport nat" Examples.transportNat
  runOne "transport refl" Examples.transportNatRefl
  runOne "cong succ"     Examples.congSucc
  runOne "cong succ refl" Examples.congSuccRefl
  runOne "let universe"  Examples.letUniverse
  runOne "omega (bad)"   Examples.omegaAnn
  runOne "unknown var"   Examples.unknownVar
  runOne "pair mismatch" Examples.pairMismatch
  runOne "bad fst"       Examples.badFst
  runOne "bad succ"      Examples.badSucc
  runOne "bad refl"      Examples.badRefl