module Core.Term

import Data.Fin

import Core.Misc

%default total

{-
  The type of terms is indexed by the size of the environment in which
  they are valid, that is, it is impossible to construct an ill-scoped term.

  Defs are used for performance reasons and are not implemented in a type safe manner.
  if a def is not in scope the checker will scream at you.
-}
public export
data Term : (_ : Index) -> Type where
  TType   : Term n                               -- Type of types

  TTop    : Term n                               -- Unit type
  TStar   : Term n                               -- Unit term
  TTopInd : Term n -> Term n -> Term n           -- : (x : ⊤) → C x

  TBot    : Term n                               -- Empty type
  TBotInd : Term n -> Term n                     -- : (x : ⊥) → C x

  TNat    : Term n                               -- ℕ
  TZero   : Term n                               -- 0
  TSuc    : Term n -> Term n                     -- successor
  TNatInd : Term n -> Term n -> Term n -> Term n -- : (x : ℕ) → C x

  TSigma  : Term n -> Term n -> Term n                     -- Sum type (Σ _ : A, B _)
  TPair   : Term n -> Term n -> Term n                     -- Sum constructor _,_
  TSigInd : Term n -> Term n -> Term n -> Term n -> Term n -- A B C f : (x : Σ _ : A , B _) → C x

  TId     : Term n -> Term n -> Term n -> Term n                     -- Id Type (Id A x y)
  TRefl   : Term n -> Term n -> Term n                               -- Refl A x
  TJ      : Term n -> Term n -> Term n -> Term n -> Term n -> Term n -- A a b C d : (p : Id A a b) → C p

  TLet    : Term n -> Term n -> Term (S n) -> Term n       -- let _ : #0 := #1 in #2

  TLam    : Term (S n) -> Term n                 -- Lambda abstraction (λ _ . Scope)
  TPi     : Term n -> Term (S n) -> Term n       -- Pi type            (∏ _ : A . B _ )

  TApp    : Term n -> Term n -> Term n           -- Appliction

  TVar    : Fin n  -> Term n                     -- Variable

  TDef    : Int    -> Term n                     -- Def Variable

infixl 3 `TApp`

public export
Show (Term n) where
  show TType           = "TType"

  show TTop            = "⊤"
  show TStar           = "★"
  show (TTopInd c st)  = "⊤-ind (" ++ show c ++ ") (" ++ show st ++ ")"

  show TBot            = "⊥"
  show (TBotInd c)     = "⊥-ind (" ++ show c ++ ")"

  show TNat            = "ℕ"
  show TZero           = "0"
  show (TSuc n)        = "suc (" ++ show n ++ ")"
  show (TNatInd c z s) = "ℕ-ind (" ++ show c ++ ") (" ++ show z ++ ") (" ++ show s ++ ")"

  show (TSigma a b)    = "Σ (" ++ show a ++ ") (" ++ show b ++ ")"
  show (TPair a b)     = "Pair (" ++ show a ++ ") (" ++ show b ++ ")"
  show (TSigInd a b c f) = "Σ-ind (" ++ show a ++ ") (" ++ show b ++ ") (" ++ show c ++ ") (" ++ show f ++ ")"

  show (TId ty x y)  = "Id (" ++ show ty ++ ") (" ++ show x ++ ") (" ++ show y ++ ")"
  show (TRefl ty tr) = "Refl (" ++ show ty ++ ") (" ++ show tr ++ ")"
  show (TJ ty a b c d) = "J (" ++ show ty ++ ") (" ++ show a ++ ") (" ++ show b ++ ") (" 
                            ++ show c ++ ") (" ++ show d ++ ")"

  show (TLet ty tr itr) = "let : (" ++ show ty ++ ") := (" ++ show tr ++ ") in (" ++ show itr ++ ")"

  show (TLam sc)       = "λ (" ++ show sc ++ ")"
  show (TPi  ty sc)    = "Π (" ++ show ty ++ ") (" ++ show sc ++ ")"

  show (TApp f x)      = "(" ++ show f ++ ") TApp (" ++ show x ++ ")"
  show (TVar i)        = "Var " ++ show i
  show (TDef i)        = "Def " ++ show i

public export
weakTr : Term n -> Term (S n)
weakTr = go 0
  where
    go : {0 n : Nat} -> Fin (S n) -> Term n -> Term (S n)
    go n TType             = TType
    go n TTop              = TTop
    go n TStar             = TTop
    go n (TTopInd c st)    = TTopInd (go n c) (go n st)
    go n TBot              = TBot
    go n (TBotInd c)       = TBotInd (go n c)
    go n TNat              = TNat
    go n TZero             = TZero
    go n (TSuc m)          = TSuc (go n m)
    go n (TNatInd c z s)   = TNatInd (go n c) (go n z) (go n s)
    go n (TSigma a b)      = TSigma (go n a) (go n b)
    go n (TPair a b)       = TPair (go n a) (go n b)
    go n (TSigInd a b c f) = TSigInd (go n a) (go n b) (go n c) (go n f)
    go n (TId ty a b)      = TId (go n ty) (go n a) (go n b)
    go n (TRefl ty tr)     = TRefl (go n ty) (go n tr)
    go n (TJ ty a b c d)   = TJ (go n ty) (go n a) (go n b) (go n c) (go n d)
    go n (TLet ty tr itr)  = TLet (go n ty) (go n tr) (go (FS n) itr)
    go n (TLam sc)         = TLam (go (FS n) sc)
    go n (TPi  ty sc)      = TPi (go n ty) (go (FS n) sc)
    go n (TApp f x)        = TApp (go n f) (go n x)
    go n (TVar i)          = if weaken i < n
                                then TVar (weaken i)
                                else TVar (FS i)
    go n (TDef i)          = TDef i

public export
weakTr2 : Term n -> Term (2+n)
weakTr2 = weakTr . weakTr

public export
weakTr3 : Term n -> Term (3+n)
weakTr3 = weakTr . weakTr2

public export
weakTr4 : Term n -> Term (4+n)
weakTr4 = weakTr2 . weakTr2