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

import Syntax.PreorderReasoning

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) (Var Var.here))
      (App (wkn u $ drop (id _) n) (Var Var.here))
      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

-- 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 Preservation ------------------------------------------------------

wknPresTypeWf :
  {0 env1 : Env sx} ->
  TypeWf env1 a ->
  EnvWf env2 ->
  IsExtension thin env2 env1 ->
  TypeWf env2 (wkn a thin)
wknPresTypeConv :
  {0 env1 : Env sx} ->
  TypeConv env1 a b ->
  EnvWf env2 ->
  IsExtension thin env2 env1 ->
  TypeConv env2 (wkn a thin) (wkn b thin)
wknPresTermWf :
  {0 env1 : Env sx} ->
  TermWf env1 t a ->
  EnvWf env2 ->
  IsExtension thin env2 env1 ->
  TermWf env2 (wkn t thin) (wkn a thin)
wknPresTermConv :
  {0 env1 : Env sx} ->
  TermConv env1 t u a ->
  EnvWf env2 ->
  IsExtension thin env2 env1 ->
  TermConv env2 (wkn t thin) (wkn u thin) (wkn a thin)

wknPresTypeWf (SetType envWf1) envWf ext = SetType envWf
wknPresTypeWf (PiType {f, n} wf wf1) envWf ext =
  let wf' = wknPresTypeWf wf envWf ext in
  PiType wf' $
  typeWfRespEnvEq
    (wknPresTypeWf wf1 (envWf :< wf') $
     replace {p = \thin' => IsExtension (keep thin n) (Add env2 (f `Over` thin')) (env1 :< f)}
       (compRightIdentity thin)
       (KeepWf ext))
    ((:<) {t = f `Over` thin} Base (sym $ wknId $ expand $ f `Over` thin))
wknPresTypeWf (LiftType wf) envWf ext = LiftType (wknPresTermWf wf envWf ext)

wknPresTypeConv (ReflType wf) envWf ext = ReflType (wknPresTypeWf wf envWf ext)
wknPresTypeConv (SymType conv) envWf ext = SymType (wknPresTypeConv conv envWf ext)
wknPresTypeConv (TransType conv conv1) envWf ext =
  TransType
    (wknPresTypeConv conv envWf ext)
    (wknPresTypeConv conv1 envWf ext)
wknPresTypeConv (PiTypeConv {f, n} wf conv conv1) envWf ext =
  let wf' = wknPresTypeWf wf envWf ext in
  PiTypeConv wf' (wknPresTypeConv conv envWf ext) $
  typeConvRespEnvEq
    (wknPresTypeConv conv1 (envWf :< wf') $
     replace {p = \thin' => IsExtension (keep thin n) (Add env2 (f `Over` thin')) (env1 :< f)}
       (compRightIdentity thin)
       (KeepWf ext))
    ((:<) {t = f `Over` thin} Base (sym $ wknId $ expand $ f `Over` thin))
wknPresTypeConv (LiftConv conv) envWf ext = LiftConv (wknPresTermConv conv envWf ext)

wknPresTermWf (VarTerm {i} envWf1) envWf ext =
  rewrite wknIndex ext i in
  VarTerm envWf
wknPresTermWf (PiTerm {f, n} wf wf1) envWf ext =
  let wf' = wknPresTermWf wf envWf ext in
  PiTerm wf' $
  termWfRespEnvEq
    (wknPresTermWf wf1 (envWf :< LiftType wf') $
     replace {p = \thin' => IsExtension (keep thin n) (Add env2 (f `Over` thin')) (env1 :< f)}
       (compRightIdentity thin)
       (KeepWf ext))
    ((:<) {t = f `Over` thin} Base (sym $ wknId $ expand $ f `Over` thin))
wknPresTermWf (AbsTerm {f, n} wf wf1) envWf ext =
  let wf' = wknPresTypeWf wf envWf ext in
  AbsTerm wf' $
  termWfRespEnvEq
    (wknPresTermWf wf1 (envWf :< wf') $
     replace {p = \thin' => IsExtension (keep thin n) (Add env2 (f `Over` thin')) (env1 :< f)}
       (compRightIdentity thin)
       (KeepWf ext))
    ((:<) {t = f `Over` thin} Base (sym $ wknId $ expand $ f `Over` thin))
wknPresTermWf (AppTerm {g, u, n} wf wf1) envWf ext =
  rewrite wknSub1 g u thin in
  AppTerm (wknPresTermWf wf envWf ext) (wknPresTermWf wf1 envWf ext)
wknPresTermWf (ConvTerm wf conv) envWf ext =
  ConvTerm (wknPresTermWf wf envWf ext) (wknPresTypeConv conv envWf ext)

wknPresTermConv (ReflTerm wf) envWf ext = ReflTerm (wknPresTermWf wf envWf ext)
wknPresTermConv (SymTerm conv) envWf ext = SymTerm (wknPresTermConv conv envWf ext)
wknPresTermConv (TransTerm conv conv1) envWf ext =
  TransTerm
    (wknPresTermConv conv envWf ext)
    (wknPresTermConv conv1 envWf ext)
wknPresTermConv (ConvTermConv conv conv1) envWf ext =
  ConvTermConv
    (wknPresTermConv conv envWf ext)
    (wknPresTypeConv conv1 envWf ext)
wknPresTermConv (PiTermConv {f, n} wf conv conv1) envWf ext =
  let wf' = wknPresTypeWf wf envWf ext in
  PiTermConv wf' (wknPresTermConv conv envWf ext) $
  termConvRespEnvEq
    (wknPresTermConv conv1 (envWf :< wf') $
     replace {p = \thin' => IsExtension (keep thin n) (Add env2 (f `Over` thin')) (env1 :< f)}
       (compRightIdentity thin)
       (KeepWf ext))
    ((:<) {t = f `Over` thin} Base (sym $ wknId $ expand $ f `Over` thin))
wknPresTermConv (PiBeta {f, g, t, u, n} wf wf1 wf2) envWf ext =
  let wf' = wknPresTypeWf wf envWf ext in
  rewrite wknSub1 g u thin in
  rewrite wknSub1 t u thin in
  PiBeta wf'
    (termWfRespEnvEq
      (wknPresTermWf wf1 (envWf :< wf') $
       replace {p = \thin' => IsExtension (keep thin n) (Add env2 (f `Over` thin')) (env1 :< f)}
         (compRightIdentity thin)
         (KeepWf ext))
      ((:<) {t = f `Over` thin} Base (sym $ wknId $ expand $ f `Over` thin)))
    (wknPresTermWf wf2 envWf ext)
wknPresTermConv (PiEta {f, n, t, u} wf wf1 wf2 conv) envWf ext =
  let wf' = wknPresTypeWf wf envWf ext in
  PiEta wf'
    (wknPresTermWf wf1 envWf ext)
    (wknPresTermWf wf2 envWf ext)
    (termConvRespEnvEq
      (rewrite sym $ wknEta t thin n in
       rewrite sym $ wknEta u thin n in
       wknPresTermConv conv (envWf :< wf') $
       replace {p = \thin' => IsExtension (keep thin n) (Add env2 (f `Over` thin')) (env1 :< f)}
         (compRightIdentity thin)
         (KeepWf ext))
      ((:<) {t = f `Over` thin} Base (sym $ wknId $ expand $ f `Over` thin)))
wknPresTermConv (AppConv {g, n, a} conv conv1) envWf ext =
  rewrite wknSub1 g a thin in
  AppConv
    (wknPresTermConv conv envWf ext)
    (wknPresTermConv conv1 envWf ext)