%!TEX root = ../Main.tex

\section{Types of Values}
\begin{small}
\begin{code}
Inductive TYPE (ds: defs) (ke: kienv) (te: tyenv) : exp -> ty -> Prop :=
| TYVar  :  forall i t
         ,  get i te = Some t
         -> TYPE ds ke te (XVar i) t

| TYLAM  :  forall x1 t1
         ,  TYPE ds (ke :> KStar) (liftTE 0 te) x1 t1 
         -> TYPE ds ke te (XLAM x1) (TForall t1)

| TYAPP  :  forall x1 t1 t2
         ,  TYPE ds ke te x1 (TForall t1)
         -> KIND ke t2 KStar
         -> TYPE ds ke te (XAPP x1 t2) (substTT 0 t2 t1)

| TYLam  :  forall x t1 t2
         ,  KIND ke t1 KStar
         -> TYPE ds ke (te :> t1) x            t2
         -> TYPE ds ke te (XLam t1 x) (tFun t1 t2)

| TYApp  :  forall x1 x2 t1 t2
         ,  TYPE ds ke te x1 (tFun t1 t2)
         -> TYPE ds ke te x2 t1
         -> TYPE ds ke te (XApp x1 x2) t2
                                              
| TYCon  :  forall tc ks tsFields tsParam xs dc dcs
         ,  DEFSOK ds
         -> getTypeDef tc ds = Some (DefDataType tc ks       dcs)
         -> getDataDef dc ds = Some (DefData     dc tsFields tc)
         -> Forall2 (KIND ke) tsParam ks
         -> Forall2 (TYPE ds ke te) xs (map (substTTs 0 tsParam) tsFields)
         -> TYPE ds ke te (XCon dc tsParam xs) (makeTApps (TCon tc) tsParam)

| TYCase :  forall xObj tObj tcObj ks tResult alts dcs
         ,  TYPE ds ke te xObj tObj
         -> Forall (fun alt => TYPEA ds ke te alt tObj tResult) alts
         -> getCtorOfType tObj  = Some tcObj
         -> getTypeDef tcObj ds = Some (DefDataType tcObj ks dcs)
         -> Forall (fun dc => In dc (map dcOfAlt alts)) dcs
         -> TYPE ds ke te (XCase xObj alts) tResult

with TYPEA  (ds: defs) (ke: kienv) (te: tyenv) : alt -> ty -> ty -> Prop :=     
| TYAlt  :  forall x1 dc tc ks tsParam tsFields tResult dcs
         ,  DEFSOK ds
         -> getTypeDef tc ds = Some (DefDataType tc ks dcs)
         -> getDataDef dc ds = Some (DefData     dc tsFields tc)
         -> Forall2 (KIND ke) tsParam ks
         -> TYPE  ds ke (te >< map (substTTs 0 tsParam) tsFields) x1 tResult
         -> TYPEA ds ke te (AAlt dc x1) (makeTApps (TCon tc) tsParam) tResult.
\end{code}
\end{small}
