module Core.Declarative

import Core.Context
import Core.Environment
import Core.Name
import Core.Term
import Core.Term.Substitution
import Core.Thinning
import Core.Var

import Data.Nat

public export
data EnvWf : Env sx -> Type
public export
data TypeWf : Env sx -> Term sx -> Type
public export
data TypeConv : Env sx -> Term sx -> Term sx -> Type
public export
data TermWf : Env sx -> Term sx -> Term sx -> Type
public export
data TermConv : Env sx -> Term sx -> Term sx -> Term sx -> Type

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

data TypeWf where
  SetType :
    EnvWf env ->
    ---
    TypeWf env Set
  PiType :
    TypeWf env f ->
    TypeWf (env :< f) g ->
    ---
    TypeWf env (Pi n f g)
  LiftType :
    TermWf env a Set ->
    ---
    TypeWf env a

data TypeConv where
  ReflType :
    TypeWf env a ->
    ---
    TypeConv env a a
  SymType :
    TypeConv env a b ->
    ---
    TypeConv env b a
  TransType :
    TypeConv env a b ->
    TypeConv env b c ->
    ---
    TypeConv env a c
  PiTypeConv :
    TypeWf env f ->
    TypeConv env f h ->
    TypeConv (env :< f) g e ->
    ---
    TypeConv env (Pi n f g) (Pi n h e)
  LiftConv :
    TermConv env a b Set ->
    ---
    TypeConv env a b

data TermWf where
  VarTerm :
    EnvWf env ->
    ---
    TermWf env (Var i) (index env i)
  PiTerm :
    TermWf env f Set ->
    TermWf (env :< f) g Set ->
    ---
    TermWf env (Pi n f g) Set
  AbsTerm :
    TypeWf env f ->
    TermWf (env :< f) t g ->
    ---
    TermWf env (Abs n t) (Pi n f g)
  AppTerm :
    TermWf env t (Pi n f g) ->
    TermWf env u f ->
    ---
    TermWf env (App t u) (subst g $ sub1 u)
  ConvTerm :
    TermWf env t a ->
    TypeConv env a b ->
    ---
    TermWf env t b

data TermConv where
  ReflTerm :
    TermWf env t a ->
    ---
    TermConv env t t a
  SymTerm :
    TermConv env t u a ->
    ---
    TermConv env u t a
  TransTerm :
    TermConv env t u a ->
    TermConv env u v a ->
    ---
    TermConv env t v a
  ConvTermConv :
    TermConv env t u a ->
    TypeConv env a b ->
    ---
    TermConv env t u b
  PiTermConv :
    TypeWf env f ->
    TermConv env f h Set ->
    TermConv (env :< f) g e Set ->
    ---
    TermConv env (Pi n f g) (Pi n h e) Set
  PiBeta :
    TypeWf env f ->
    TermWf (env :< f) t g ->
    TermWf env u f ->
    ---
    TermConv env (App (Abs n t) u) (subst t $ sub1 u) (subst g $ sub1 u)
  PiEta :
    TypeWf env f ->
    TermWf env t (Pi n f g) ->
    TermWf env u (Pi n f g) ->
    TermConv (env :< f) (App (wkn t $ drop (id _) n) a) (App (wkn u $ drop (id _) n) a) g ->
    ---
    TermConv env t u (Pi n f g)
  AppConv :
    TermConv env t u (Pi n f g) ->
    TermConv env a b f ->
    ---
    TermConv env (App t a) (App u b) (subst g $ sub1 a)

%name EnvWf envWf
%name TypeWf wf
%name TypeConv conv
%name TermWf wf
%name TermConv conv

public export
data ThinWf : sx `Thins` sy -> Env sy -> Env sx -> Type where
  IdWf : ThinWf (id sx) env env
  DropWf : ThinWf thin env2 env1 -> ThinWf (drop thin n) (Add env2 t) env1
  KeepWf :
    ThinWf thin env2 env1 ->
    ThinWf (keep thin n) (Add env2 (shift t thin)) (Add env1 t)

%name ThinWf thinWf

-- Environment Equality --------------------------------------------------------

envWfRespEnvEq : EnvWf env1 -> EnvEq env1 env2 -> EnvWf env2
typeWfRespEnvEq : TypeWf env1 a -> EnvEq env1 env2 -> TypeWf env2 a
typeConvRespEnvEq : TypeConv env1 a b -> EnvEq env1 env2 -> TypeConv env2 a b
termWfRespEnvEq : TermWf env1 t a -> EnvEq env1 env2 -> TermWf env2 t a
termConvRespEnvEq : TermConv env1 t u b -> EnvEq env1 env2 -> TermConv env2 t u b

envWfRespEnvEq envWf Base = envWf
envWfRespEnvEq (envWf :< wf) (prf :< eq) =
  envWfRespEnvEq envWf prf :<
  rewrite sym eq in typeWfRespEnvEq wf prf

typeWfRespEnvEq (SetType envWf) prf = SetType (envWfRespEnvEq envWf prf)
typeWfRespEnvEq (PiType wf wf1) prf =
  PiType
    (typeWfRespEnvEq wf prf)
    (typeWfRespEnvEq wf1 $ prf :< Refl)
typeWfRespEnvEq (LiftType wf) prf = LiftType (termWfRespEnvEq wf prf)

typeConvRespEnvEq (ReflType wf) prf = ReflType (typeWfRespEnvEq wf prf)
typeConvRespEnvEq (SymType conv) prf = SymType (typeConvRespEnvEq conv prf)
typeConvRespEnvEq (TransType conv conv1) prf =
  TransType
    (typeConvRespEnvEq conv prf)
    (typeConvRespEnvEq conv1 prf)
typeConvRespEnvEq (PiTypeConv wf conv conv1) prf =
  PiTypeConv
    (typeWfRespEnvEq wf prf)
    (typeConvRespEnvEq conv prf)
    (typeConvRespEnvEq conv1 $ prf :< Refl)
typeConvRespEnvEq (LiftConv conv) prf = LiftConv (termConvRespEnvEq conv prf)

termWfRespEnvEq (VarTerm {i} envWf) prf =
  rewrite indexEqIsEq prf i in
  VarTerm (envWfRespEnvEq envWf prf)
termWfRespEnvEq (PiTerm wf wf1) prf =
  PiTerm
    (termWfRespEnvEq wf prf)
    (termWfRespEnvEq wf1 $ prf :< Refl)
termWfRespEnvEq (AbsTerm wf wf1) prf =
  AbsTerm
    (typeWfRespEnvEq wf prf)
    (termWfRespEnvEq wf1 $ prf :< Refl)
termWfRespEnvEq (AppTerm wf wf1) prf = AppTerm (termWfRespEnvEq wf prf) (termWfRespEnvEq wf1 prf)
termWfRespEnvEq (ConvTerm wf conv) prf =
  ConvTerm
    (termWfRespEnvEq wf prf)
    (typeConvRespEnvEq conv prf)

termConvRespEnvEq (ReflTerm wf) prf = ReflTerm (termWfRespEnvEq wf prf)
termConvRespEnvEq (SymTerm conv) prf = SymTerm (termConvRespEnvEq conv prf)
termConvRespEnvEq (TransTerm conv conv1) prf =
  TransTerm
    (termConvRespEnvEq conv prf)
    (termConvRespEnvEq conv1 prf)
termConvRespEnvEq (ConvTermConv conv conv1) prf =
  ConvTermConv (termConvRespEnvEq conv prf) (typeConvRespEnvEq conv1 prf)
termConvRespEnvEq (PiTermConv wf conv conv1) prf =
  PiTermConv
    (typeWfRespEnvEq wf prf)
    (termConvRespEnvEq conv prf)
    (termConvRespEnvEq conv1 $ prf :< Refl)
termConvRespEnvEq (PiBeta wf wf1 wf2) prf =
  PiBeta
    (typeWfRespEnvEq wf prf)
    (termWfRespEnvEq wf1 $ prf :< Refl)
    (termWfRespEnvEq wf2 prf)
termConvRespEnvEq (PiEta wf wf1 wf2 conv) prf =
  PiEta
    (typeWfRespEnvEq wf prf)
    (termWfRespEnvEq wf1 prf)
    (termWfRespEnvEq wf2 prf)
    (termConvRespEnvEq conv $ prf :< Refl)
termConvRespEnvEq (AppConv conv conv1) prf =
  AppConv
    (termConvRespEnvEq conv prf)
    (termConvRespEnvEq conv1 prf)

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

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

typeWfImpliesEnvWf (SetType envWf) = envWf
typeWfImpliesEnvWf (PiType wf wf1) = typeWfImpliesEnvWf wf
typeWfImpliesEnvWf (LiftType wf) = termWfImpliesEnvWf wf

typeConvImpliesEnvWf (ReflType wf) = typeWfImpliesEnvWf wf
typeConvImpliesEnvWf (SymType conv) = typeConvImpliesEnvWf conv
typeConvImpliesEnvWf (TransType conv conv1) = typeConvImpliesEnvWf conv
typeConvImpliesEnvWf (PiTypeConv wf conv conv1) = typeConvImpliesEnvWf conv
typeConvImpliesEnvWf (LiftConv conv) = termConvImpliesEnvWf conv

termWfImpliesEnvWf (VarTerm envWf) = envWf
termWfImpliesEnvWf (PiTerm wf wf1) = termWfImpliesEnvWf wf
termWfImpliesEnvWf (AbsTerm wf wf1) = typeWfImpliesEnvWf wf
termWfImpliesEnvWf (AppTerm wf wf1) = termWfImpliesEnvWf wf
termWfImpliesEnvWf (ConvTerm wf conv) = termWfImpliesEnvWf wf

termConvImpliesEnvWf (ReflTerm wf) = termWfImpliesEnvWf wf
termConvImpliesEnvWf (SymTerm conv) = termConvImpliesEnvWf conv
termConvImpliesEnvWf (TransTerm conv conv1) = termConvImpliesEnvWf conv
termConvImpliesEnvWf (ConvTermConv conv conv1) = termConvImpliesEnvWf conv
termConvImpliesEnvWf (PiTermConv wf conv conv1) = termConvImpliesEnvWf conv
termConvImpliesEnvWf (PiBeta wf wf1 wf2) = typeWfImpliesEnvWf wf
termConvImpliesEnvWf (PiEta wf wf1 wf2 conv) = typeWfImpliesEnvWf wf
termConvImpliesEnvWf (AppConv conv conv1) = termConvImpliesEnvWf conv

-- Weakening Composition -------------------------------------------------------

CompWf : ThinWf thin2 env3 env2 -> ThinWf thin1 env2 env1 -> ThinWf (thin2 . thin1) env3 env1
CompWf IdWf thinWf1 = rewrite compLeftIdentity thin1 in thinWf1
CompWf (DropWf {thin = thin2, n} thinWf2) thinWf1 =
  rewrite compLeftDrop thin2 thin1 n in
  DropWf (CompWf thinWf2 thinWf1)
CompWf (KeepWf {thin = thin2, n} thinWf2) IdWf =
  rewrite compRightIdentity $ keep thin2 n in
  KeepWf thinWf2
CompWf (KeepWf {thin = thin2, n} thinWf2) (DropWf {thin = thin1} thinWf1) =
  rewrite compRightDrop thin2 thin1 n in
  DropWf (CompWf thinWf2 thinWf1)
CompWf (KeepWf {thin = thin2, n} thinWf2) (KeepWf {thin = thin1, t} thinWf1) =
  rewrite compKeep thin2 thin1 n in
  rewrite shiftHomo t thin1 thin2 in
  KeepWf (CompWf thinWf2 thinWf1)

-- Weakening Preservation ------------------------------------------------------

wknPresTypeWf :
  TypeWf env1 a ->
  ThinWf thin env2 env1 ->
  TypeWf env2 (wkn a thin)
wknPresTypeConv :
  TypeConv env1 a b ->
  ThinWf thin env2 env1 ->
  TypeConv env2 (wkn a thin) (wkn b thin)
wknPresTermWf :
  TermWf env1 t a ->
  ThinWf thin env2 env1 ->
  TermWf env2 (wkn t thin) (wkn a thin)
wknPresTermConv :
  TermConv env1 t u a ->
  ThinWf thin env2 env1 ->
  TermConv env2 (wkn t thin) (wkn u thin) (wkn a thin)