module Core.Declarative

import Core.Context
import Core.Name
import Core.Term
import Core.Term.Environment
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 a ->
    ---
    EnvWf (env :< a)

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 wf
%name TypeWf wf
%name TypeConv conv
%name TermWf wf
%name TermConv conv