module Core.Syntax where

import Core.Info
import Common

data LetBind = LetBind {
    letBindName :: Name
  , letBindTy   :: Ty
  , letBindBody :: Tm
  }

data PiBind = PiBind {
    piBindName  :: Name
  , piBindInfo  :: PiDomKind
  , piBindDomTy :: Ty
  , piBindBody  :: Ty
  }

data LamBind = LamBind {
    lamBindName  :: Name
  , lamBindInfo  :: PiDomKind
  , lamBindDomTy :: Ty
  , lamBindBody  :: Tm
  }

instance Show PiBind where
  show (PiBind x i a b) = show (x, i, a, b)

instance Show LamBind where
  show (LamBind x i a t) = show (x, i, a, t)

instance Show LetBind where
  show (LetBind x a t) = show (x, a, t)

data Sub
  = SNil        -- ^ Sub Γ ∙
  | SExt Sub Tm -- ^ vanilla extension
  | SDef Sub Tm -- ^ extend codomain with a definition
  deriving Show

{-
     σ : Sub Γ Δ   t : Tm Δ A
  ───────────────────────────────
  SDef σ t : Sub Γ (Δ, x : A = t)
-}

data MetaSub
  = MSId
  | MSSub Sub
  deriving Show

data Level
  = ZeroPlus Tm
  | OmegaPlus Integer
  | OmegaPlusOmega
  deriving Show

data Tm
  = Var Ix
  | TopDef {-# nounpack #-} DefInfo
  | Meta MetaVar MetaSub
  | Let Tm LetBind
  | App Tm Tm PiDomKind
  | Lam LamBind
  | LZero
  | LSuc Tm
  | LMax Tm Tm
  | Wk Tm
  | Code Level Ty
  | Cast Ty Ty Tm
  deriving Show

data Ty
  = TYPE Level
  | Pi PiBind
  | FinLevel
  | Decode Level Tm
  deriving Show

data Locals
  = LNil
  | LLet Locals Name Tm Ty
  | LBind Locals Name ~Ty
  deriving Show

instance Sized Locals where
  size = go 0 where
    go acc LNil = acc
    go acc (LLet ls _ _ _) = go (acc + 1) ls
    go acc (LBind ls _ _)  = go (acc + 1) ls

localsToNames :: Locals -> Names
localsToNames = \case
  LNil          -> Nil
  LLet ls x _ _ -> Cons x (localsToNames ls)
  LBind ls x _  -> Cons x (localsToNames ls)

type LocalsArg = (?locals :: Locals)

data RevLocals
  = RLNil
  | RLLet   Name Tm Ty RevLocals
  | RLBind  Name ~Ty RevLocals
  deriving Show

reverseLocals :: Locals -> RevLocals
reverseLocals = go RLNil where
  go acc = \case
    LNil          -> acc
    LLet ls x t a -> go (RLLet x t a acc) ls
    LBind ls x a  -> go (RLBind x a acc) ls

makeFields ''PiBind
makeFields ''LetBind