module Core.Generic

import Core.Context
import Core.Declarative
import Core.Environment
import Core.Reduction
import Core.Term
import Core.Term.NormalForm
import Core.Term.Substitution
import Core.Thinning
import Core.Var

%prefix_record_projections off

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

record GenericEquality where
  constructor MkEquality
  TypeEq : forall sx. Env sx -> Term sx -> Term sx -> Type
  TermEq : forall sx. Env sx -> Term sx -> Term sx -> Term sx -> Type
  NtrlEq : forall sx. Env sx -> Term sx -> Term sx -> Term sx -> Type

interface IsGenericEquality (eq : GenericEquality) where
  -- Subsumption
  ntrlImpliesTermEq : eq.NtrlEq {sx} env t u a -> eq.TermEq env t u a
  termImpliesTypeEq : eq.TermEq {sx} env a b Set -> eq.TypeEq env a b
  eqImpliesTermConv : eq.TermEq {sx} env t u a -> TermConv env t u a
  eqImpliesTypeConv : eq.TypeEq {sx} env a b -> TypeConv env a b

  -- Partial Equivalence
  ntrlSym : eq.NtrlEq {sx} env t u a -> eq.NtrlEq env u t a
  ntrlTrans : eq.NtrlEq {sx} env t u a -> eq.NtrlEq env u v a -> eq.NtrlEq env t v a
  termSym : eq.TermEq {sx} env t u a -> eq.TermEq env u t a
  termTrans : eq.TermEq {sx} env t u a -> eq.TermEq env u v a -> eq.TermEq env t v a
  typeSym : eq.TypeEq {sx} env a b -> eq.TypeEq env b a
  typeTrans : eq.TypeEq {sx} env a b -> eq.TypeEq env b c -> eq.TypeEq env a c

  -- Conversion
  ntrlConv : eq.NtrlEq {sx} env t u a -> TypeConv env a b -> eq.NtrlEq env t u b
  termConv : eq.TermEq {sx} env t u a -> TypeConv env a b -> eq.TermEq env t u b

  -- Weakening
  wknPresNtrlEq :
    eq.NtrlEq {sx} env1 t u a ->
    EnvWf env2 ->
    IsExtension thin env2 env1 ->
    eq.NtrlEq {sx = sy} env2 (wkn t thin) (wkn u thin) (wkn a thin)
  wknPresTermEq :
    eq.TermEq {sx} env1 t u a ->
    EnvWf env2 ->
    IsExtension thin env2 env1 ->
    eq.TermEq {sx = sy} env2 (wkn t thin) (wkn u thin) (wkn a thin)
  wknPresTypeEq :
    eq.TypeEq {sx} env1 a b ->
    EnvWf env2 ->
    IsExtension thin env2 env1 ->
    eq.TypeEq {sx = sy} env2 (wkn a thin) (wkn b thin)

  -- Weak Head Expansion
  typeExpansion :
    TypeRed env a a' ->
    TypeRed env b b' ->
    Whnf a' ->
    Whnf b' ->
    eq.TypeEq {sx} env a' b' ->
    eq.TypeEq env a b
  termExpansion :
    TypeRed env a b ->
    TermRed env t t' b ->
    TermRed env u u' b ->
    Whnf b ->
    Whnf t' ->
    Whnf u' ->
    eq.TermEq {sx} env t' u' b ->
    eq.TermEq env t u a

  -- Type Constructor Congruence
  typeSet :
    EnvWf env ->
    ---
    eq.TypeEq {sx} env Set Set
  typePi :
    TypeWf env f ->
    eq.TypeEq env f h ->
    eq.TypeEq (env :< f) g e ->
    ---
    eq.TypeEq {sx} env (Pi n f g) (Pi n h e)

  -- Term Constructor Congruence and η
  termPi :
    TypeWf env f ->
    eq.TermEq env f h Set ->
    eq.TermEq (env :< f) g e Set ->
    ---
    eq.TermEq {sx} env (Pi n f g) (Pi n h e) Set
  termPiEta :
    TypeWf env f ->
    TermWf env t (Pi n f g) ->
    TermWf env u (Pi n f g) ->
    eq.TermEq (env :< f)
      (App (wkn t (wkn1 _ n)) (Var Var.here))
      (App (wkn u (wkn1 _ n)) (Var Var.here))
      g ->
    ---
    eq.TermEq {sx} env t u (Pi n f g)

  -- Neutral Congruence
  ntrlVar :
    TermWf env (Var i) a ->
    ---
    eq.NtrlEq {sx} env (Var i) (Var i) a
  ntrlApp :
    eq.NtrlEq env t u (Pi n f g) ->
    eq.TermEq env a b f ->
    ---
    eq.NtrlEq {sx} env (App t a) (App u b) (subst g (sub1 a))

-- Judgemental Equality --------------------------------------------------------

Judgemental : GenericEquality
Judgemental = MkEquality TypeConv TermConv TermConv

IsGenericEquality Judgemental where
  ntrlImpliesTermEq = id
  termImpliesTypeEq = LiftConv
  eqImpliesTermConv = id
  eqImpliesTypeConv = id

  ntrlSym = SymTerm
  ntrlTrans = TransTerm
  termSym = SymTerm
  termTrans = TransTerm
  typeSym = SymType
  typeTrans = TransType

  ntrlConv = ConvTermConv
  termConv = ConvTermConv

  wknPresNtrlEq = wknPresTermConv
  wknPresTermEq = wknPresTermConv
  wknPresTypeEq = wknPresTypeConv

  typeExpansion steps1 steps2 n m conv =
    TransType (typeRedImpliesTypeConv steps1) $
    TransType conv $
    SymType (typeRedImpliesTypeConv steps2)
  termExpansion steps1 steps2 steps3 n m k conv =
    ConvTermConv
      (TransTerm (termRedImpliesTermConv steps2) $
       TransTerm conv $
       SymTerm (termRedImpliesTermConv steps3))
      (SymType $ typeRedImpliesTypeConv steps1)

  typeSet = ReflType . SetType
  typePi = PiTypeConv

  termPi = PiTermConv
  termPiEta = PiEta

  ntrlVar = ReflTerm
  ntrlApp = AppConv