module Core.Generic

import Core.Declarative
import Core.Environment
import Core.Reduction
import Core.Term
import Core.Term.NormalForm
import Core.Term.Substitution
import Core.Term.Thinned
import Core.Thinning

%prefix_record_projections off

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

public export
record Equality where
  constructor MkEquality
  TypeEq : forall n. Env n -> Term n -> Term n -> Type
  TermEq : forall n. Env n -> Term n -> Term n -> Term n -> Type
  NtrlEq : forall n. Env n -> NeutralTerm n -> NeutralTerm n -> Term n -> Type

public export
interface IsEq (0 eq : Equality) where
  -- Subsumption
  ntrlEqImpliesTermEq :
    {0 n, m : NeutralTerm k} ->
    eq.NtrlEq env n m a ->
    eq.TermEq env n.fst m.fst a
  termEqImpliesTypeEq : eq.TermEq {n} env a b Set -> eq.TypeEq env a b
  termEqImpliesConv : eq.TermEq {n} env t u a -> TermConv env t u a
  typeEqImpliesConv : eq.TypeEq {n} env a b -> TypeConv env a b

  -- Partial Equivalence
  ntrlSym : eq.NtrlEq {n = k} env n m a -> eq.NtrlEq env m n a
  ntrlTrans : eq.NtrlEq {n = k} env n1 n2 a -> eq.NtrlEq env n2 n3 a -> eq.NtrlEq env n1 n3 a
  termSym : eq.TermEq {n} env t u a -> eq.TermEq env u t a
  termTrans : eq.TermEq {n} env t u a -> eq.TermEq env u v a -> eq.TermEq env t v a
  typeSym : eq.TypeEq {n} env a b -> eq.TypeEq env b a
  typeTrans : eq.TypeEq {n} env a b -> eq.TypeEq env b c -> eq.TypeEq env a c

  -- Conversion
  ntrlConv : eq.NtrlEq {n = k} env n m a -> TypeConv env a b -> eq.NtrlEq env n m b
  termConv : eq.TermEq {n} env t u a -> TypeConv env a b -> eq.TermEq env t u b

  -- Weakening
  wknNtrl :
    eq.NtrlEq {n = j} env1 n m a ->
    ExtendsWf thin env2 env1 ->
    eq.NtrlEq {n = k} env2 (wkn n thin) (wkn m thin) (wkn a thin)
  wknTerm :
    eq.TermEq {n = m} env1 t u a ->
    ExtendsWf thin env2 env1 ->
    eq.TermEq {n} env2 (wkn t thin) (wkn u thin) (wkn a thin)
  wknType :
    eq.TypeEq {n = m} env1 a b ->
    ExtendsWf thin env2 env1 ->
    eq.TypeEq {n} env2 (wkn a thin) (wkn b thin)

  -- Weak Head Expansion
  expandTerm :
    TermReduce env t t' a ->
    TermReduce env u u' a ->
    Whnf t' ->
    Whnf u' ->
    eq.TermEq {n} env t' u' a ->
    eq.TermEq env t u a
  expandType :
    TypeReduce env a a' ->
    TypeReduce env b b' ->
    Whnf a' ->
    Whnf b' ->
    eq.TypeEq {n} env a' b' ->
    eq.TypeEq env a b

  -- Neutral Congruence
  ntrlVar :
    TermWf env (Var i) a ->
    ---
    eq.NtrlEq {n} env (Element (Var i) Var) (Element (Var i) Var) a
  ntrlApp :
    {0 n, m : NeutralTerm k} ->
    eq.NtrlEq env n m (Pi a b) ->
    eq.TermEq env t u a ->
    ---
    eq.NtrlEq env
      (Element (App n.fst t) (App n.snd))
      (Element (App m.fst u) (App m.snd))
      (subst1 b t)

  -- Term Congurence
  termPi :
    TypeWf env a ->
    eq.TermEq env a c Set ->
    eq.TermEq (env :< pure a) b d Set ->
    ---
    eq.TermEq {n} env (Pi a b) (Pi c d) Set
  termPiEta :
    TypeWf env a ->
    TermWf env t (Pi a b) ->
    TermWf env u (Pi a b) ->
    eq.TermEq (env :< pure a)
      (App (wkn t $ drop $ id _) (Var FZ))
      (App (wkn u $ drop $ id _) (Var FZ))
      b ->
    ---
    eq.TermEq {n} env t u (Pi a b)

  -- Type Congruence
  typeSet :
    EnvWf env ->
    ---
    eq.TypeEq {n} env Set Set
  typePi :
    TypeWf env a ->
    eq.TypeEq env a c ->
    eq.TypeEq (env :< pure a) b d ->
    ---
    eq.TypeEq {n} env (Pi a b) (Pi c d)

export
ntrlEqImpliesTypeEq : IsEq eq => eq.NtrlEq {n = k} env n m Set -> eq.TypeEq env n.fst m.fst
ntrlEqImpliesTypeEq = termEqImpliesTypeEq . ntrlEqImpliesTermEq

-- Instance 1 ------------------------------------------------------------------

public export
Judgemental : Equality
Judgemental = MkEquality TypeConv TermConv (\env, n, m, a => TermConv env n.fst m.fst a)

judgeWknNtrl :
  (Judgemental .NtrlEq) {n = j} env1 n m a ->
  ExtendsWf thin env2 env1 ->
  (Judgemental .NtrlEq) {n = k} env2 (wkn n thin) (wkn m thin) (wkn a thin)
judgeWknNtrl {n = Element t n, m = Element u m} = weakenTermConv

export
IsEq Judgemental where
  -- Subsumption
  ntrlEqImpliesTermEq = id
  termEqImpliesTypeEq = LiftConv
  termEqImpliesConv = id
  typeEqImpliesConv = id

  -- Partial Equivalence
  ntrlSym = SymTm
  ntrlTrans = TransTm
  termSym = SymTm
  termTrans = TransTm
  typeSym = SymTy
  typeTrans = TransTy

  -- Conversion
  ntrlConv = ConvConv
  termConv = ConvConv

  -- Weakening
  wknNtrl = judgeWknNtrl
  wknTerm = weakenTermConv
  wknType = weakenTypeConv

  -- Weak Head Expansion
  expandTerm = \steps1, steps2, n, m, eq =>
    TransTm (termRedImpliesConv steps1) $
    TransTm eq $
    SymTm (termRedImpliesConv steps2)
  expandType = \steps1, steps2, n, m, eq =>
    TransTy (typeRedImpliesConv steps1) $
    TransTy eq $
    SymTy (typeRedImpliesConv steps2)

  -- Neutral Congruence
  ntrlVar = ReflTm
  ntrlApp = AppConv

  -- Term Congurence
  termPi = PiTmConv
  termPiEta = PiEta

  -- Type Congruence
  typeSet = ReflTy . SetTyWf
  typePi = PiConv