module Tests.Typechecker

import Quox.Syntax
import Quox.Syntax.Qty.Three
import Quox.Typechecker as Lib
import public TypingImpls
import TAP


data Error'
  = TCError (Typing.Error Three)
  | WrongInfer (Term Three d n) (Term Three d n)
  | WrongQOut (QOutput Three n) (QOutput Three n)

export
ToInfo Error' where
  toInfo (TCError e) = toInfo e
  toInfo (WrongInfer good bad) =
    [("type", "WrongInfer"),
     ("wanted", prettyStr True good),
     ("got", prettyStr True bad)]
  toInfo (WrongQOut good bad) =
    [("type", "WrongQOut"),
     ("wanted", prettyStr True good),
     ("wanted", prettyStr True bad)]

0 M : Type -> Type
M = ReaderT (Definitions Three) $ Either Error'

inj : (forall m. CanTC Three m => m a) -> M a
inj act = do
  env <- ask
  let res = runReaderT env act {m = Either (Typing.Error Three)}
  either (throwError . TCError) pure res


reflTy : IsQty q => Term q d n
reflTy =
  Pi zero (TYPE 0) $ S ["A"] $ Y $
  Pi one  (BVT 0)  $ S ["x"] $ Y $
  Eq0 (BVT 1) (BVT 0) (BVT 0)

reflDef : IsQty q => Term q d n
reflDef = ["A","x"] :\\ ["i"] :\\% BVT 0

defGlobals : Definitions Three
defGlobals = fromList
  [("A",  mkAbstract Zero $ TYPE 0),
   ("B",  mkAbstract Zero $ TYPE 0),
   ("C",  mkAbstract Zero $ TYPE 1),
   ("D",  mkAbstract Zero $ TYPE 1),
   ("P",  mkAbstract Zero $ Arr Any (FT "A") (TYPE 0)),
   ("a",  mkAbstract Any  $ FT "A"),
   ("a'", mkAbstract Any  $ FT "A"),
   ("b",  mkAbstract Any  $ FT "B"),
   ("f",  mkAbstract Any  $ Arr One (FT "A") (FT "A")),
   ("g",  mkAbstract Any  $ Arr One (FT "A") (FT "B")),
   ("f2", mkAbstract Any  $ Arr One (FT "A") $ Arr One (FT "A") (FT "A")),
   ("p",  mkAbstract Any  $ Pi One (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0),
   ("q",  mkAbstract Any  $ Pi One (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0),
   ("refl", mkDef Any reflTy reflDef)]

parameters (label : String) (act : Lazy (M ()))
           {default defGlobals globals : Definitions Three}
  testTC : Test
  testTC = test label $ runReaderT globals act

  testTCFail : Test
  testTCFail = testThrows label (const True) $ runReaderT globals act


ctx : TContext Three 0 n -> TyContext Three 0 n
ctx = MkTyContext new

inferredTypeEq : TyContext Three d n -> (exp, got : Term Three d n) -> M ()
inferredTypeEq ctx exp got =
  catchError
    (inj $ equalType ctx exp got)
    (\_ : Error' => throwError $ WrongInfer exp got)

qoutEq : (exp, got : QOutput Three n) -> M ()
qoutEq qout res = unless (qout == res) $ throwError $ WrongQOut qout res

inferAs : TyContext Three d n -> (sg : SQty Three) ->
          Elim Three d n -> Term Three d n -> M ()
inferAs ctx@(MkTyContext {dctx, _}) sg e ty = do
  case !(inj $ infer ctx sg e) of
    Just res => inferredTypeEq ctx ty res.type
    Nothing  => pure ()

inferAsQ : TyContext Three d n -> (sg : SQty Three) ->
           Elim Three d n -> Term Three d n -> QOutput Three n -> M ()
inferAsQ ctx@(MkTyContext {dctx, _}) sg e ty qout = do
  case !(inj $ infer ctx sg e) of
    Just res => do
      inferredTypeEq ctx ty res.type
      qoutEq qout res.qout
    Nothing => pure ()

infer_ : TyContext Three d n -> (sg : SQty Three) -> Elim Three d n -> M ()
infer_ ctx sg e = ignore $ inj $ infer ctx sg e

checkQ : TyContext Three d n -> SQty Three ->
         Term Three d n -> Term Three d n -> QOutput Three n -> M ()
checkQ ctx@(MkTyContext {dctx, _}) sg s ty qout = do
  case !(inj $ check ctx sg s ty) of
    Just res => qoutEq qout res
    Nothing  => pure ()

check_ : TyContext Three d n -> SQty Three ->
         Term Three d n -> Term Three d n -> M ()
check_ ctx sg s ty = ignore $ inj $ check ctx sg s ty

export
tests : Test
tests = "typechecker" :- [
  "universes" :- [
    testTC "0 · ★₀ ⇐ ★₁" $ check_ (ctx [<]) szero (TYPE 0) (TYPE 1),
    testTC "0 · ★₀ ⇐ ★₂" $ check_ (ctx [<]) szero (TYPE 0) (TYPE 2),
    testTC "0 · ★₀ ⇐ ★_" $ check_ (ctx [<]) szero (TYPE 0) (TYPE UAny),
    testTCFail "0 · ★₁ ⇍ ★₀" $ check_ (ctx [<]) szero (TYPE 1) (TYPE 0),
    testTCFail "0 · ★₀ ⇍ ★₀" $ check_ (ctx [<]) szero (TYPE 0) (TYPE 0),
    testTCFail "0 · ★_ ⇍ ★_" $ check_ (ctx [<]) szero (TYPE UAny) (TYPE UAny),
    testTCFail "1 · ★₀ ⇍ ★₁" $ check_ (ctx [<]) sone (TYPE 0) (TYPE 1),
    testTC "0=1 ⊢ 0 · ★₁ ⇐ ★₀" $
      check_ (MkTyContext (ZeroIsOne {d = 0}) [<]) szero (TYPE 1) (TYPE 0)
  ],

  "function types" :- [
    note "A, B : ★₀;  C, D : ★₁;  P : A ⇾ ★₀",
    testTC "0 · A ⊸ B ⇐ ★₀" $
      check_ (ctx [<]) szero (Arr One (FT "A") (FT "B")) (TYPE 0),
    note "subtyping",
    testTC "0 · A ⊸ B ⇐ ★₁" $
      check_ (ctx [<]) szero (Arr One (FT "A") (FT "B")) (TYPE 1),
    testTC "0 · C ⊸ D ⇐ ★₁" $
      check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 1),
    testTCFail "0 · C ⊸ D ⇍ ★₀" $
      check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 0),
    testTC "0 · (1·x : A) → P x ⇐ ★₀" $
      check_ (ctx [<]) szero
        (Pi One (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0)
        (TYPE 0),
    testTCFail "0 · A ⊸ P ⇍ ★₀" $
      check_ (ctx [<]) szero (Arr One (FT "A") $ FT "P") (TYPE 0),
    testTC "0=1 ⊢ 0 · A ⊸ P ⇐ ★₀" $
      check_ (MkTyContext (ZeroIsOne {d = 0}) [<]) szero
        (Arr One (FT "A") $ FT "P") (TYPE 0)
  ],

  "pair types" :- [
    note #""A × B" for "(_ : A) × B""#,
    testTC "0 · A × A ⇐ ★₀" $
      check_ (ctx [<]) szero (FT "A" `And` FT "A") (TYPE 0),
    testTCFail "1 · A × A ⇍ ★₀" $
      check_ (ctx [<]) sone (FT "A" `And` FT "A") (TYPE 0)
  ],

  "free vars" :- [
    note "A : ★₀",
    testTC "0 · A ⇒ ★₀" $
      inferAs (ctx [<]) szero (F "A") (TYPE 0),
    testTC "0 · [A] ⇐ ★₀" $
      check_ (ctx [<]) szero (FT "A") (TYPE 0),
    note "subtyping",
    testTC "0 · [A] ⇐ ★₁" $
      check_ (ctx [<]) szero (FT "A") (TYPE 1),
    note "(fail) runtime-relevant type",
    testTCFail "1 · A ⇏ ★₀" $
      infer_ (ctx [<]) sone (F "A"),
    note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ λᴰ _ ⇒ x)",
    testTC "1 · refl ⇒ ⋯" $ inferAs (ctx [<]) sone (F  "refl") reflTy,
    testTC "1 · [refl] ⇐ ⋯" $ check_ (ctx [<]) sone (FT "refl") reflTy
  ],

  "bound vars" :- [
    testTC "x : A ⊢ 1 · x ⇒ A ⊳ 1·x" $
      inferAsQ {n = 1} (ctx [< FT "A"]) sone
        (BV 0) (FT "A") [< one],
    testTC "x : A ⊢ 1 · [x] ⇐ A ⊳ 1·x" $
      checkQ {n = 1} (ctx [< FT "A"]) sone (BVT 0) (FT "A") [< one],
    note "f2 : A ⊸ A ⊸ A",
    testTC "x : A ⊢ 1 · f2 [x] [x] ⇒ A ⊳ ω·x" $
      inferAsQ {n = 1} (ctx [< FT "A"]) sone
        (F "f2" :@@ [BVT 0, BVT 0]) (FT "A") [< Any]
  ],

  "lambda" :- [
    note "linear & unrestricted identity",
    testTC "1 · (λ x ⇒ x) ⇐ A ⊸ A" $
      check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr One (FT "A") (FT "A")),
    testTC "1 · (λ x ⇒ x) ⇐ A → A" $
      check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr Any (FT "A") (FT "A")),
    note "(fail) zero binding used relevantly",
    testTCFail "1 · (λ x ⇒ x) ⇍ A ⇾ A" $
      check_ (ctx [<]) sone (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
    note "(but ok in overall erased context)",
    testTC "0 · (λ x ⇒ x) ⇐ A ⇾ A" $
      check_ (ctx [<]) szero (["x"] :\\ BVT 0) (Arr Zero (FT "A") (FT "A")),
    testTC "1 · (λ A x ⇒ refl A x) ⇐ ⋯  # (type of refl)" $
      check_ (ctx [<]) sone
        (["A", "x"] :\\ E (F "refl" :@@ [BVT 1, BVT 0]))
        reflTy,
    testTC "1 · (λ A x ⇒ λᴰ i ⇒ x) ⇐ ⋯  # (def. and type of refl)" $
      check_ (ctx [<]) sone reflDef reflTy
  ],

  "equalities" :- [
    testTC "1 · (λᴰ i ⇒ a) ⇐ a ≡ a" $
      check_ (ctx [<]) sone (DLam $ S ["i"] $ N $ FT "a")
        (Eq0 (FT "A") (FT "a") (FT "a")),
    testTC "0 · (λ p q ⇒ λᴰ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
      check_ (ctx [<]) szero
        (Lam $ S ["p"] $ Y $ Lam $ S ["q"] $ N $ DLam $ S ["i"] $ N $ BVT 0)
        (Pi Any (Eq0 (FT "A") (FT "a") (FT "a")) $ S ["p"] $ Y $
         Pi Any (Eq0 (FT "A") (FT "a") (FT "a")) $ S ["q"] $ Y $
         Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0)),
    testTC "0 · (λ p q ⇒ λᴰ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
      check_ (ctx [<]) szero
        (Lam $ S ["p"] $ N $ Lam $ S ["q"] $ Y $
         DLam $ S ["i"] $ N $ BVT 0)
        (Pi Any (Eq0 (FT "A") (FT "a") (FT "a")) $ S ["p"] $ Y $
         Pi Any (Eq0 (FT "A") (FT "a") (FT "a")) $ S ["q"] $ Y $
         Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0))
  ],

  "misc" :- [
    note "0·A : Type, 0·P : A → Type, ω·p : (1·x : A) → P x",
    note "⊢",
    note "1 · λ x y xy ⇒ λᴰ i ⇒ p (xy i)",
    note "  ⇐ (0·x y : A) → (1·xy : x ≡ y) → Eq [i ⇒ P (xy i)] (p x) (p y)",
    testTC "cong" $
      check_ (ctx [<]) sone
        (["x", "y", "xy"] :\\ ["i"] :\\% E (F "p" :@ E (BV 0 :% BV 0)))
        (Pi Zero (FT "A") $ S ["x"] $ Y $
         Pi Zero (FT "A") $ S ["y"] $ Y $
         Pi One  (Eq0 (FT "A") (BVT 1) (BVT 0)) $ S ["xy"] $ Y $
         Eq (S ["i"] $ Y $ E $ F "P" :@ E (BV 0 :% BV 0))
            (E $ F "p" :@ BVT 2) (E $ F "p" :@ BVT 1)),
    note "0·A : Type, 0·P : ω·A → Type,",
    note "ω·p q : (1·x : A) → P x",
    note "⊢",
    note "1 · λ eq ⇒ λᴰ i ⇒ λ x ⇒ eq x i",
    note "  ⇐ (1·eq : (1·x : A) → p x ≡ q x) → p ≡ q",
    testTC "funext" $
      check_ (ctx [<]) sone
        (["eq"] :\\ ["i"] :\\% ["x"] :\\ E (BV 1 :@ BVT 0 :% BV 0))
        (Pi One
            (Pi One (FT "A") $ S ["x"] $ Y $
              Eq0 (E $ F "P" :@ BVT 0)
                  (E $ F "p" :@ BVT 0) (E $ F "q" :@ BVT 0)) $
            S ["eq"] $ Y $
              Eq0 (Pi Any (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0)
                  (FT "p") (FT "q"))
  ]
]