module Core.Declarative

import Core.Environment
import Core.Term
import Core.Term.Substitution
import Core.Term.Thinned
import Core.Thinning

-- Definition ------------------------------------------------------------------

data EnvWf : Env n -> Type
data TypeWf : Env n -> Term n -> Type
data TypeConv : Env n -> Term n -> Term n -> Type
data TermWf : Env n -> Term n -> Term n -> Type
data TermConv : Env n -> Term n -> Term n -> Term n -> Type

data EnvWf where
  Lin : EnvWf [<]
  (:<) : EnvWf env -> TypeWf env (expand a) -> EnvWf (env :< a)

data TypeWf where
  SetTyWf :
    EnvWf env ->
    ---
    TypeWf env Set
  PiTyWf :
    TypeWf env a ->
    TypeWf (env :< pure a) b ->
    ---
    TypeWf env (Pi a b)
  LiftWf :
    TermWf env a Set ->
    ---
    TypeWf env a

data TypeConv where
  ReflTy :
    TypeWf env a ->
    ---
    TypeConv env a a
  SymTy :
    TypeConv env a b ->
    ---
    TypeConv env b a
  TransTy :
    TypeConv env a b ->
    TypeConv env b c ->
    ---
    TypeConv env a c
  PiConv :
    TypeWf env a ->
    TypeConv env a c ->
    TypeConv (env :< pure a) b d ->
    ---
    TypeConv env (Pi a b) (Pi c d)
  LiftConv :
    TermConv env a b Set ->
    ---
    TypeConv env a b

data TermWf where
  PiTmWf :
    TermWf env a Set ->
    TermWf (env :< pure a) b Set ->
    ---
    TermWf env (Pi a b) Set
  VarWf :
    EnvWf env ->
    ---
    TermWf env (Var i) (expand $ index env i)
  AbsWf :
    TypeWf env a ->
    TermWf (env :< pure a) t b ->
    ---
    TermWf env (Abs t) (Pi a b)
  AppWf :
    TermWf env t (Pi a b) ->
    TermWf env u a ->
    ---
    TermWf env (App t u) (subst b $ Wkn (id _) :< pure u)
  ConvWf :
    TermWf env t a ->
    TypeConv env a b ->
    ---
    TermWf env t b

data TermConv where
  ReflTm :
    TermWf env t a ->
    ---
    TermConv env t t a
  SymTm :
    TermConv env t u a ->
    ---
    TermConv env u t a
  TransTm :
    TermConv env t u a ->
    TermConv env u v a ->
    ---
    TermConv env t v a
  AppConv :
    TermConv env f g (Pi a b) ->
    TermConv env t u a ->
    ---
    TermConv env (App f t) (App g u) (subst b $ Wkn (id _) :< pure t)
  PiTmConv :
    TypeWf env a ->
    TermConv env a c Set ->
    TermConv (env :< pure a) b d Set ->
    ---
    TermConv env (Pi a b) (Pi c d) Set
  PiEta :
    TypeWf env a ->
    TermWf env t (Pi a b) ->
    TermWf env u (Pi a b) ->
    TermConv (env :< pure a)
      (App (wkn t $ drop $ id _) (Var FZ))
      (App (wkn u $ drop $ id _) (Var FZ))
      b ->
    ---
    TermConv env t u (Pi a b)
  PiBeta :
    TypeWf env a ->
    TermWf (env :< pure a) t b ->
    TermWf env u a ->
    ---
    TermConv env
      (App (Abs t) u)
      (subst t $ Wkn (id _) :< pure u)
      (subst g $ Wkn (id _) :< pure u)
  ConvConv :
    TermConv env t u a ->
    TypeConv env a b ->
    ---
    TermConv env t u b

%name EnvWf envWf
%name TypeWf tyWf
%name TypeConv tyConv
%name TermWf tmWf
%name TermConv tmConv

-- Respects Environment Quotient -----------------------------------------------

export
envWfRespEq : EnvWf env1 -> env1 =~= env2 -> EnvWf env2
export
typeWfRespEq : TypeWf env1 a -> env1 =~= env2 -> TypeWf env2 a
export
typeConvRespEq : TypeConv env1 a b -> env1 =~= env2 -> TypeConv env2 a b
export
termWfRespEq : TermWf env1 t a -> env1 =~= env2 -> TermWf env2 t a
export
termConvRespEq : TermConv env1 t u a -> env1 =~= env2 -> TermConv env2 t u a

envWfRespEq envWf Refl = envWf
envWfRespEq (envWf :< tyWf) (prf :< prf') =
  envWfRespEq envWf prf :<
  rewrite sym prf' in typeWfRespEq tyWf prf

typeWfRespEq (SetTyWf envWf) prf = SetTyWf (envWfRespEq envWf prf)
typeWfRespEq (PiTyWf tyWf tyWf1) prf =
  PiTyWf
    (typeWfRespEq tyWf prf)
    (typeWfRespEq tyWf1 $ prf :< Refl)
typeWfRespEq (LiftWf tmWf) prf = LiftWf (termWfRespEq tmWf prf)

typeConvRespEq (ReflTy tyWf) prf = ReflTy (typeWfRespEq tyWf prf)
typeConvRespEq (SymTy tyConv) prf = SymTy (typeConvRespEq tyConv prf)
typeConvRespEq (TransTy tyConv tyConv1) prf =
  TransTy
    (typeConvRespEq tyConv prf)
    (typeConvRespEq tyConv1 prf)
typeConvRespEq (PiConv tyWf tyConv tyConv1) prf =
  PiConv
    (typeWfRespEq tyWf prf)
    (typeConvRespEq tyConv prf)
    (typeConvRespEq tyConv1 $ prf :< Refl)
typeConvRespEq (LiftConv tmConv) prf = LiftConv (termConvRespEq tmConv prf)

termWfRespEq (PiTmWf tmWf tmWf1) prf =
  PiTmWf
    (termWfRespEq tmWf prf)
    (termWfRespEq tmWf1 $ prf :< Refl)
termWfRespEq (VarWf {i} envWf) prf =
  rewrite indexCong prf i in
  VarWf (envWfRespEq envWf prf)
termWfRespEq (AbsWf tyWf tmWf) prf =
  AbsWf
    (typeWfRespEq tyWf prf)
    (termWfRespEq tmWf $ prf :< Refl)
termWfRespEq (AppWf tmWf tmWf1) prf =
  AppWf
    (termWfRespEq tmWf prf)
    (termWfRespEq tmWf1 prf)
termWfRespEq (ConvWf tmWf tyConv) prf =
  ConvWf
    (termWfRespEq tmWf prf)
    (typeConvRespEq tyConv prf)

termConvRespEq (ReflTm tmWf) prf = ReflTm (termWfRespEq tmWf prf)
termConvRespEq (SymTm tmConv) prf = SymTm (termConvRespEq tmConv prf)
termConvRespEq (TransTm tmConv tmConv1) prf =
  TransTm
    (termConvRespEq tmConv prf)
    (termConvRespEq tmConv1 prf)
termConvRespEq (AppConv tmConv tmConv1) prf =
  AppConv
    (termConvRespEq tmConv prf)
    (termConvRespEq tmConv1 prf)
termConvRespEq (PiTmConv tyWf tmConv tmConv1) prf =
  PiTmConv
    (typeWfRespEq tyWf prf)
    (termConvRespEq tmConv prf)
    (termConvRespEq tmConv1 $ prf :< Refl)
termConvRespEq (PiEta tyWf tmWf tmWf1 tmConv) prf =
  PiEta
    (typeWfRespEq tyWf prf)
    (termWfRespEq tmWf prf)
    (termWfRespEq tmWf1 prf)
    (termConvRespEq tmConv $ prf :< Refl)
termConvRespEq (PiBeta tyWf tmWf tmWf1) prf =
  PiBeta
    (typeWfRespEq tyWf prf)
    (termWfRespEq tmWf $ prf :< Refl)
    (termWfRespEq tmWf1 prf)
termConvRespEq (ConvConv tmConv tyConv) prf =
  ConvConv
    (termConvRespEq tmConv prf)
    (typeConvRespEq tyConv prf)

-- Well-Formed Environment -----------------------------------------------------

export
typeWfImpliesEnvWf : TypeWf env a -> EnvWf env
export
typeConvImpliesEnvWf : TypeConv env a b -> EnvWf env
export
termWfImpliesEnvWf : TermWf env t a -> EnvWf env
export
termConvImpliesEnvWf : TermConv env t u a -> EnvWf env

typeWfImpliesEnvWf (SetTyWf envWf) = envWf
typeWfImpliesEnvWf (PiTyWf tyWf tyWf1) = typeWfImpliesEnvWf tyWf
typeWfImpliesEnvWf (LiftWf tmWf) = termWfImpliesEnvWf tmWf

typeConvImpliesEnvWf (ReflTy tyWf) = typeWfImpliesEnvWf tyWf
typeConvImpliesEnvWf (SymTy tyConv) = typeConvImpliesEnvWf tyConv
typeConvImpliesEnvWf (TransTy tyConv tyConv1) = typeConvImpliesEnvWf tyConv
typeConvImpliesEnvWf (PiConv tyWf tyConv tyConv1) = typeConvImpliesEnvWf tyConv
typeConvImpliesEnvWf (LiftConv tmConv) = termConvImpliesEnvWf tmConv

termWfImpliesEnvWf (PiTmWf tmWf tmWf1) = termWfImpliesEnvWf tmWf
termWfImpliesEnvWf (VarWf envWf) = envWf
termWfImpliesEnvWf (AbsWf tyWf tmWf) = typeWfImpliesEnvWf tyWf
termWfImpliesEnvWf (AppWf tmWf tmWf1) = termWfImpliesEnvWf tmWf
termWfImpliesEnvWf (ConvWf tmWf tyConv) = termWfImpliesEnvWf tmWf

termConvImpliesEnvWf (ReflTm tmWf) = termWfImpliesEnvWf tmWf
termConvImpliesEnvWf (SymTm tmConv) = termConvImpliesEnvWf tmConv
termConvImpliesEnvWf (TransTm tmConv tmConv1) = termConvImpliesEnvWf tmConv
termConvImpliesEnvWf (AppConv tmConv tmConv1) = termConvImpliesEnvWf tmConv
termConvImpliesEnvWf (PiTmConv tyWf tmConv tmConv1) = termConvImpliesEnvWf tmConv
termConvImpliesEnvWf (PiEta tyWf tmWf tmWf1 tmConv) = termWfImpliesEnvWf tmWf
termConvImpliesEnvWf (PiBeta tyWf tmWf tmWf1) = typeWfImpliesEnvWf tyWf
termConvImpliesEnvWf (ConvConv tmConv tyConv) = termConvImpliesEnvWf tmConv