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