module Core.Reduction

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

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

public export
data TermStep : Env n -> Term n -> Term n -> Term n -> Type where
  AppStep :
    TermStep env t u (Pi a b) ->
    TermWf env v a ->
    ---
    TermStep env (App t v) (App u v) (subst b $ Wkn (id _) :< pure v)
  PiBeta :
    TypeWf env a ->
    TermWf (env :< pure a) t b ->
    TermWf env u a ->
    ---
    TermStep env
      (App (Abs t) u)
      (subst t $ Wkn (id _) :< pure u)
      (subst b $ Wkn (id _) :< pure u)
  ConvStep :
    TermStep env t u a ->
    TypeConv env a b ->
    ---
    TermStep env t u b

public export
TypeStep : Env n -> Term n -> Term n -> Type
TypeStep env a b = TermStep env a b Set

public export
data ReflTransClosure : (refl : a -> Type) -> (step : a -> a -> Type) -> a -> a -> Type where
  Refl :
    {0 refl : a -> Type} ->
    refl x ->
    ---
    ReflTransClosure refl step x x
  Step :
    {0 step : a -> a -> Type} ->
    step x y ->
    ReflTransClosure refl step y z ->
    ---
    ReflTransClosure refl step x z

public export
TypeReduce : Env n -> Term n -> Term n -> Type
TypeReduce env = ReflTransClosure (TypeWf env) (TypeStep env)

public export
TermReduce : Env n -> Term n -> Term n -> Term n -> Type
TermReduce env t u a = ReflTransClosure (\t => TermWf env t a) (\t, u => TermStep env t u a) t u

%name TermStep step
%name ReflTransClosure steps

-- Respects Environment Quotient -----------------------------------------------

export
termStepRespEq : TermStep env1 t u a -> env1 =~= env2 -> TermStep env2 t u a
termStepRespEq (AppStep step tmWf) prf =
  AppStep
    (termStepRespEq step prf)
    (termWfRespEq tmWf prf)
termStepRespEq (PiBeta tyWf tmWf tmWf1) prf =
  PiBeta
    (typeWfRespEq tyWf prf)
    (termWfRespEq tmWf $ prf :< Refl)
    (termWfRespEq tmWf1 prf)
termStepRespEq (ConvStep step tyConv) prf =
  ConvStep
    (termStepRespEq step prf)
    (typeConvRespEq tyConv prf)

export
typeStepRespEq : TypeStep env1 a b -> env1 =~= env2 -> TypeStep env2 a b
typeStepRespEq = termStepRespEq

export
typeRedRespEq : TypeReduce env1 a b -> env1 =~= env2 -> TypeReduce env2 a b
typeRedRespEq (Refl tyWf) prf = Refl (typeWfRespEq tyWf prf)
typeRedRespEq (Step step steps) prf = Step (typeStepRespEq step prf) (typeRedRespEq steps prf)

export
termRedRespEq : TermReduce env1 t u a -> env1 =~= env2 -> TermReduce env2 t u a
termRedRespEq (Refl tmWf) prf = Refl (termWfRespEq tmWf prf)
termRedRespEq (Step step steps) prf = Step (termStepRespEq step prf) (termRedRespEq steps prf)

-- Reduction Subsumed by Conversion --------------------------------------------

export
termStepImpliesConv : TermStep env t u a -> TermConv env t u a
termStepImpliesConv (AppStep step tmWf) = AppConv (termStepImpliesConv step) (ReflTm tmWf)
termStepImpliesConv (PiBeta tyWf tmWf tmWf1) = PiBeta tyWf tmWf tmWf1
termStepImpliesConv (ConvStep step tyConv) = ConvConv (termStepImpliesConv step) tyConv

export
typeStepImpliesConv : TypeStep env a b -> TypeConv env a b
typeStepImpliesConv = LiftConv . termStepImpliesConv

export
typeRedImpliesConv : TypeReduce env a b -> TypeConv env a b
typeRedImpliesConv (Refl tyWf) = ReflTy tyWf
typeRedImpliesConv (Step step steps) =
  TransTy
    (typeStepImpliesConv step)
    (typeRedImpliesConv steps)

export
termRedImpliesConv : TermReduce env t u a -> TermConv env t u a
termRedImpliesConv (Refl tmWf) = ReflTm tmWf
termRedImpliesConv (Step step steps) =
  TransTm
    (termStepImpliesConv step)
    (termRedImpliesConv steps)

-- Subject Typing --------------------------------------------------------------

export
termStepImpliesSubjectWf : TermStep env t u a -> TermWf env t a
termStepImpliesSubjectWf (AppStep step tmWf) = AppWf (termStepImpliesSubjectWf step) tmWf
termStepImpliesSubjectWf (PiBeta tyWf tmWf tmWf1) = AppWf (AbsWf tyWf tmWf) tmWf1
termStepImpliesSubjectWf (ConvStep step tyConv) = ConvWf (termStepImpliesSubjectWf step) tyConv

export
typeStepImpliesSubjectWf : TypeStep env a b -> TypeWf env a
typeStepImpliesSubjectWf = LiftWf . termStepImpliesSubjectWf

-- Whnfs Do Not Reduce ---------------------------------------------------------

export
whnfNoTermStep : Whnf t -> Not (TermStep env t u a)
whnfNoTermStep (Ntrl (App n)) (AppStep step tmWf) = whnfNoTermStep (Ntrl n) step
whnfNoTermStep (Ntrl (App n)) (PiBeta tyWf tmWf tmWf1) impossible
whnfNoTermStep n (ConvStep step tyConv) = whnfNoTermStep n step

export
whnfNoTypeStep : Whnf a -> Not (TypeStep env a b)
whnfNoTypeStep = whnfNoTermStep

export
whnfTypeRedStays : Whnf a -> TypeReduce env a b -> a = b
whnfTypeRedStays n (Refl tyWf) = Refl
whnfTypeRedStays n (Step step steps) = absurd (whnfNoTypeStep n step)

export
whnfTermRedStays : Whnf t -> TermReduce env t u a -> t = u
whnfTermRedStays n (Refl tmWf) = Refl
whnfTermRedStays n (Step step steps) = absurd (whnfNoTermStep n step)