module Core.Tests

import Core.Term
import Core.Check
import Core.Convert
import Core.Misc
import Core.Normalize
import Core.Value

import Control.Monad.RWS
import Control.Monad.Identity
import Control.Monad.Either

import Data.Fin

%default total

{- λA. λx. x : ∏ (A : Type) → A → A -}
test_id : Either String (Bool, List String)
test_id = typecheck (TLam (TLam (TVar 0)))
                    (TPi TType (TPi (TVar 0) (TVar 1)))

{- λA. λB. λf. λx. f x : ∏ (A : Type) ∏ (B : A → Type) ∏ (f : ∏ (x : A) B x) ∏ (x : A) B x -}
test_app : Either String (Bool, List String)
test_app = typecheck (TLam (TLam (TLam (TLam (TVar 1 `TApp` TVar 0)))))
                     (TPi TType 
                          (TPi (TPi (TVar 0) TType)
                               (TPi (TPi (TVar 1) (TVar 1 `TApp` TVar 0)) 
                                    (TPi (TVar 2) (TVar 2 `TApp` TVar 0)))))

{- λf. λx. f x ≃ λf. λx. (λy. f y) x -}
eta_test : Either String (Bool, List String)
eta_test = resolve action
  where
    action : PI Bool
    action = do
      x <- eval ctx0 (TLam (TLam (TVar 1 `TApp` TVar 0)))
      y <- eval ctx0 (TLam (TLam (TLam (TVar 2 `TApp` TVar 0) `TApp` TVar 0)))
      convert x y

addition : Term 0
addition = TNatInd (TLam (TPi TNat TNat)) 
                   (TLam (TVar 0)) 
                   (TLam {-n-} (TLam {-n+-} (TLam {-m-} (TSuc (TVar 1 `TApp` TVar 0)))))

additionty : Term 0
additionty = TPi TNat (TPi TNat TNat)

additionty_test : Either String (Bool, List String)
additionty_test = typecheck additionty TType

addition_test : Either String (Bool, List String)
addition_test = typecheck addition additionty

{- 2 + 1 = 3 -}
addition_compute_test : Either String (Bool, List String)
addition_compute_test = resolve action
  where
    action : PI Bool
    action = do
      x <- eval ctx0 (addition `TApp` TSuc (TSuc TZero) `TApp` TSuc TZero)
      y <- eval ctx0 (TSuc (TSuc (TSuc TZero)))
      convert x y

multi : Term 0
multi = TNatInd (TLam (TPi TNat TNat)) 
                (TLam TZero)
                (TLam {-n-} (TLam {-n*-} (TLam {-m-} (weakTr3 addition `TApp` TVar 0 `TApp` (TVar 1 `TApp` TVar 0)))))

multity : Term 0
multity = TPi TNat (TPi TNat TNat)

multity_test : Either String (Bool, List String)
multity_test = typecheck multity TType

multi_test : Either String (Bool, List String)
multi_test = typecheck multi multity

{- 2 * 3 = 6 -}
multi_compute_test : Either String (Bool, List String)
multi_compute_test = resolve action
  where
    action : PI Bool
    action = do
      x <- eval ctx0 (multi `TApp` TSuc (TSuc TZero) `TApp` TSuc (TSuc (TSuc TZero)))
      y <- eval ctx0 (TSuc (TSuc (TSuc (TSuc (TSuc (TSuc TZero))))))
      convert x y

-- no, not that kind
unit_test : Either String (Bool, List String)
unit_test = typecheck TStar TTop

absurd_test : Either String (Bool, List String)
absurd_test = typecheck (TLam (TBotInd (TLam (TVar 1)))) (TPi TType (TPi TBot (TVar 1)))

pr1ty : Term 0
pr1ty = TPi TType {- A : Type -}
            (TPi (TPi (TVar 0) TType) {- B : A → Type -}
                 (TPi (TSigma (TVar 1) (TVar 0)) {- Σ A B -}
                      (TVar 2)))

pr1 : Term 0
pr1 = TLam {- A : Type -} 
           (TLam {- B : A → Type -}
                 (TSigInd (TVar 1) (TVar 0) (TLam {-ΣAB-} (TVar 2)) (TLam (TLam (TVar 1)))))

pr1ty_test : Either String (Bool, List String)
pr1ty_test = typecheck pr1ty TType

pr1_test : Either String (Bool, List String)
pr1_test = typecheck pr1 pr1ty

pr2ty : Term 0
pr2ty = TPi TType {- A : Type -}
            (TPi (TPi (TVar 0) TType) {- B : A → Type -}
                 (TPi (TSigma (TVar 1) (TVar 0)) {- Σ A B -}
                      (TVar 1 `TApp` (TSigInd (TVar 2) (TVar 1) (TLam (TVar 3)) (TLam (TLam (TVar 1))) `TApp` TVar 0))))

pr2 : Term 0
pr2 = TLam {- A : Type -} 
           (TLam {- B : A → Type -}
                 (TSigInd (TVar 1)
                          (TVar 0)
                          (TLam {-ΣAB-}
                                (TVar 1 `TApp` (TSigInd (TVar 2) (TVar 1) (TLam (TVar 3)) (TLam (TLam (TVar 1))) `TApp` TVar 0)))
                          (TLam (TLam (TVar 0)))))

pr2ty_test : Either String (Bool, List String)
pr2ty_test = typecheck pr2ty TType

pr2_test : Either String (Bool, List String)
pr2_test = typecheck pr2 pr2ty

pr2ty_let : Term 0
pr2ty_let = TLet pr1ty pr1 {- pr1 : pr1ty -}
                 (TPi TType {- A : Type -}
                      (TPi (TPi (TVar 0) TType) {- B : A → Type -}
                           (TPi (TSigma (TVar 1) (TVar 0)) {- Σ A B -}
                                (TVar 1 `TApp` (TVar 3 `TApp` TVar 2 `TApp` TVar 1 `TApp` TVar 0)))))

pr2_let : Term 0
pr2_let = TLet pr1ty pr1 {- pr1 : pr1ty -}
               (TLam {- A : Type -} 
                     (TLam {- B : A → Type -}
                           (TSigInd (TVar 1)
                                    (TVar 0)
                                    (TLam {-ΣAB-}
                                          (TVar 1 `TApp` (TVar 3 `TApp` TVar 2 `TApp` TVar 1 `TApp` TVar 0)))
                                    (TLam (TLam (TVar 0))))))

pr2ty_let_test : Either String (Bool, List String)
pr2ty_let_test = typecheck pr2ty_let TType

pr2_let_test : Either String (Bool, List String)
pr2_let_test = typecheck pr2_let pr2ty_let