module Core.Reducible

import Control.WellFounded

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

%prefix_record_projections off

data Level = Small | Large

%name Level l

Sized Level where
  size Small = 0
  size Large = 1

record LogicalRelation (eq : Equality) where
  constructor MkLogRel
  0 TypeRed : forall n. Env n -> Term n -> Type
  0 TypeEq : forall n. (env : Env n) -> (a, b : Term n) -> TypeRed {n} env a -> Type
  0 TermRed : forall n. (env : Env n) -> (t, a : Term n) -> TypeRed {n} env a -> Type
  0 TermEq : forall n. (env : Env n) -> (t, u, a : Term n) -> TypeRed {n} env a -> Type

data TypeRed :
  (eq : Equality) ->
  (l : Level) ->
  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq) ->
  (env : Env n) ->
  (a : Term n) ->
  Type
data TypeEq :
  (eq : Equality) ->
  (l : Level) ->
  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq) ->
  (env : Env n) ->
  (a, b : Term n) ->
  TypeRed eq l rec {n} env a ->
  Type
data TermRed :
  (eq : Equality) ->
  (l : Level) ->
  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq) ->
  (env : Env n) ->
  (t, a : Term n) ->
  TypeRed eq l rec {n} env a ->
  Type
data TermEq :
  (eq : Equality) ->
  (l : Level) ->
  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq) ->
  (env : Env n) ->
  (t, u, a : Term n) ->
  TypeRed eq l rec {n} env a ->
  Type

-- -- Neutrals

record NeutralTyRed
  (eq : Equality)
  (l : Level)
  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
  (env : Env n)
  (a : Term n)
  where
  constructor MkNtrlTyRed
  {0 a' : Term n}
  tyWf : TypeWf env a
  steps : TypeReduce env a a'
  tyWf' : TypeWf env a'
  0 ntrl : Neutral a'
  prf : eq.NtrlEq env (Element a' ntrl) (Element a' ntrl) Set

record NeutralTyEq
  (eq : Equality)
  (l : Level)
  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
  (env : Env n)
  (a, b : Term n)
  (red : NeutralTyRed eq l rec {n} env a)
  where
  constructor MkNtrlTyEq
  {0 b' : Term n}
  tyWf : TypeWf env b
  steps : TypeReduce env b b'
  tyWf' : TypeWf env b'
  0 ntrl : Neutral b'
  prf : eq.NtrlEq env (Element red.a' red.ntrl) (Element b' ntrl) Set

record NeutralTmRed
  (eq : Equality)
  (l : Level)
  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
  (env : Env n)
  (t, a : Term n)
  (red : NeutralTyRed eq l rec {n} env a)
  where
  constructor MkNtrlTmRed
  {0 t' : Term n}
  tmWf : TermWf env t a
  steps : TermReduce env t t' a
  tmWf' : TermWf env t' a
  0 ntrl : Neutral t'
  prf : eq.NtrlEq env (Element t' ntrl) (Element t' ntrl) a

record NeutralTmEq
  (eq : Equality)
  (l : Level)
  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
  (env : Env n)
  (t, u, a : Term n)
  (red : NeutralTyRed eq l rec {n} env a)
  where
  constructor MkNtrlTmEq
  {0 t', u' : Term n}
  tmWf1 : TermWf env t a
  tmWf2 : TermWf env u a
  steps1 : TermReduce env t t' a
  steps2 : TermReduce env u u' a
  tmWf1' : TermWf env t' a
  tmWf2' : TermWf env u' a
  0 ntrl1 : Neutral t'
  0 ntrl2 : Neutral u'
  prf : eq.NtrlEq env (Element t' ntrl1) (Element u' ntrl2) a

-- Set

record SetTyRed
  (eq : Equality)
  (l : Level)
  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
  (env : Env n)
  (a : Term n)
  where
  constructor MkSetTyRed
  tyWf : TypeWf env a
  steps : TypeReduce env a Set
  tyWf' : TypeWf env Set
  prf : Smaller Small l

record SetTyEq
  (eq : Equality)
  (l : Level)
  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
  (env : Env n)
  (a, b : Term n)
  (red : SetTyRed eq l rec {n} env a)
  where
  constructor MkSetTyEq
  tyWf : TypeWf env b
  steps : TypeReduce env b Set
  tyWf' : TypeWf env Set

record SetTmRed
  (eq : Equality)
  (l : Level)
  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
  (env : Env n)
  (t, a : Term n)
  (red : SetTyRed eq l rec {n} env a)
  where
  constructor MkSetTmRed
  {0 t' : Term n}
  tmWf : TermWf env t a
  steps : TypeReduce env t t'
  tyWf' : TermWf env t' a
  0 whnf : Whnf t'
  prf : eq.TermEq env t' t' a
  tyRed : (rec Small red.prf).TypeRed env t

record SetTmEq
  (eq : Equality)
  (l : Level)
  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
  (env : Env n)
  (t, u, a : Term n)
  (red : SetTyRed eq l rec {n} env a)
  where
  constructor MkSetTmEq
  {0 t', u' : Term n}
  tmWf1 : TermWf env t a
  tmWf2 : TermWf env u a
  steps1 : TypeReduce env t t'
  steps2 : TypeReduce env u u'
  tyWf1' : TermWf env t' Set
  tyWf2' : TermWf env u' Set
  0 whnf1 : Whnf t'
  0 whnf2 : Whnf u'
  prf : eq.TermEq env t' u' a
  tyRed1 : (rec Small red.prf).TypeRed env t
  tyRed2 : (rec Small red.prf).TypeRed env u
  tyEq : (rec Small red.prf).TypeEq env t u tyRed1

-- Pi

record PiTyRed
  (eq : Equality)
  (l : Level)
  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
  (env : Env n)
  (a : Term n)
  where
  constructor MkPiTyRed
  {0 f : Term n}
  {0 g : Term (S n)}
  tyWf : TypeWf env a
  steps : TypeReduce env a (Pi f g)
  tyWf' : TypeWf env (Pi f g)
  domWf : TypeWf env f
  codWf : TypeWf (env :< pure f) g
  domRed :
    forall m.
    {0 thin : n `Thins` m} ->
    forall env'.
    ExtendsWf thin env' env ->
    TypeRed eq l rec env' (wkn f thin)
  codRed :
    forall m.
    {0 thin : n `Thins` m} ->
    forall env'.
    (thinWf : ExtendsWf thin env' env) ->
    forall t.
    TermRed eq l rec env' t (wkn f thin) (domRed thinWf) ->
    TypeRed eq l rec env' (subst g (Wkn thin :< pure t))
  codEq :
    forall m.
    {0 thin : n `Thins` m} ->
    forall env'.
    (thinWf : ExtendsWf thin env' env) ->
    forall t, u.
    (red : TermRed eq l rec env' t (wkn f thin) (domRed thinWf)) ->
    TermRed eq l rec env' u (wkn f thin) (domRed thinWf) ->
    TermEq eq l rec env' t u (wkn f thin) (domRed thinWf) ->
    TypeEq eq l rec env'
      (subst g (Wkn thin :< pure t))
      (subst g (Wkn thin :< pure u))
      (codRed thinWf red)

record PiTyEq
  (eq : Equality)
  (l : Level)
  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
  (env : Env n)
  (a, b : Term n)
  (red : PiTyRed eq l rec env a)
  where
  constructor MkPiTyEq
  {0 f : Term n}
  {0 g : Term (S n)}
  tyWf : TypeWf env b
  steps : TypeReduce env b (Pi f g)
  tyWf' : TypeWf env (Pi f g)
  prf : eq.TypeEq env (Pi red.f red.g) (Pi f g)
  domEq :
    forall m.
    {0 thin : n `Thins` m} ->
    forall env'.
    (thinWf : ExtendsWf thin env' env) ->
    TypeEq eq l rec env' (wkn red.f thin) (wkn f thin) (red.domRed thinWf)
  codEq :
    forall m.
    {0 thin : n `Thins` m} ->
    forall env'.
    (thinWf : ExtendsWf thin env' env) ->
    forall t.
    (red' : TermRed eq l rec env' t (wkn red.f thin) (red.domRed thinWf)) ->
    TypeEq eq l rec env'
      (subst red.g (Wkn thin :< pure t))
      (subst g (Wkn thin :< pure t))
      (red.codRed thinWf red')

record PiTmRed
  (eq : Equality)
  (l : Level)
  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
  (env : Env n)
  (t, a : Term n)
  (red : PiTyRed eq l rec env a)
  where
  constructor MkPiTmRed
  {0 t' : Term n}
  tmWf : TermWf env t a
  steps : TermReduce env t t' a
  tmWf' : TermWf env t' a
  0 whnf : Whnf t'
  prf : eq.TermEq env t' t' a
  codRed :
    forall m.
    {0 thin : n `Thins` m} ->
    forall env'.
    (thinWf : ExtendsWf thin env' env) ->
    forall u.
    (red' : TermRed eq l rec env' u (wkn red.f thin) (red.domRed thinWf)) ->
    TermRed eq l rec env'
      (App (wkn t' thin) u)
      (subst red.g (Wkn thin :< pure u))
      (red.codRed thinWf red')
  codEq :
    forall m.
    {0 thin : n `Thins` m} ->
    forall env'.
    (thinWf : ExtendsWf thin env' env) ->
    forall u, v.
    (red' : TermRed eq l rec env' u (wkn red.f thin) (red.domRed thinWf)) ->
    TermRed eq l rec env' v (wkn red.f thin) (red.domRed thinWf) ->
    TermEq eq l rec env' u v (wkn red.f thin) (red.domRed thinWf) ->
    TermEq eq l rec env'
      (App (wkn t' thin) u)
      (App (wkn t' thin) v)
      (subst red.g (Wkn thin :< pure u))
      (red.codRed thinWf red')

record PiTmEq
  (eq : Equality)
  (l : Level)
  (rec : (l' : Level) -> Smaller l' l -> LogicalRelation eq)
  (env : Env n)
  (t, u, a : Term n)
  (red : PiTyRed eq l rec env a)
  where
  constructor MkPiTmEq
  {0 t', u' : Term n}
  tmWf1 : TermWf env t a
  tmWf2 : TermWf env u a
  steps1 : TermReduce env t t' a
  steps2 : TermReduce env u u' a
  tmWf1' : TermWf env t' a
  tmWf2' : TermWf env u' a
  0 whnf1 : Whnf t'
  0 whnf2 : Whnf u'
  prf : eq.TermEq env t' u' a
  red1 : PiTmRed eq l rec env t a red
  red2 : PiTmRed eq l rec env u a red
  codEq :
    forall m.
    {0 thin : n `Thins` m} ->
    forall env'.
    (thinWf : ExtendsWf thin env' env) ->
    forall v.
    (red' : TermRed eq l rec env' v (wkn red.f thin) (red.domRed thinWf)) ->
    TermEq eq l rec env'
      (App (wkn t' thin) v)
      (App (wkn u' thin) v)
      (subst red.g (Wkn thin :< pure v))
      (red.codRed thinWf red')

-- Putting it all together

data TypeRed where
  RedNtrlTy : NeutralTyRed eq l rec env a -> TypeRed eq l rec env a
  RedSetTy : SetTyRed eq l rec env a -> TypeRed eq l rec env a
  RedPiTy : PiTyRed eq l rec env a -> TypeRed eq l rec env a

data TypeEq where
  EqNtrlTy : NeutralTyEq eq l rec env a b red -> TypeEq eq l rec env a b (RedNtrlTy red)
  EqSetTy : SetTyEq eq l rec env a b red -> TypeEq eq l rec env a b (RedSetTy red)
  EqPiTy : PiTyEq eq l rec env a b red -> TypeEq eq l rec env a b (RedPiTy red)

data TermRed where
  RedNtrlTm : NeutralTmRed eq l rec env t a red -> TermRed eq l rec env t a (RedNtrlTy red)
  RedSetTm : SetTmRed eq l rec env t a red -> TermRed eq l rec env t a (RedSetTy red)
  RedPiTm : PiTmRed eq l rec env t a red -> TermRed eq l rec env t a (RedPiTy red)

data TermEq where
  EqNtrlTm : NeutralTmEq eq l rec env t u a red -> TermEq eq l rec env t u a (RedNtrlTy red)
  EqSetTm : SetTmEq eq l rec env t u a red -> TermEq eq l rec env t u a (RedSetTy red)
  EqPiTm : PiTmEq eq l rec env t u a red -> TermEq eq l rec env t u a (RedPiTy red)

-- Induction -------------------------------------------------------------------

LogRel : (eq : Equality) -> Level -> LogicalRelation eq
LogRel eq =
  sizeRec $ \l, rec =>
    MkLogRel
      (TypeRed eq l rec)
      (TypeEq eq l rec)
      (TermRed eq l rec)
      (TermEq eq l rec)