module Core.Reduction

import Core.Context
import Core.Declarative
import Core.Term
import Core.Term.Environment
import Core.Term.NormalForm
import Core.Term.Substitution

public export
data TermStep : Env sx -> Term sx -> Term sx -> Term sx -> Type where
  PiBeta :
    TypeWf env f ->
    TermWf (env :< f) t g ->
    TermWf env u f ->
    ---
    TermStep env (App (Abs n t) u) (subst t $ sub1 u) (subst g $ sub1 u)
  AppStep :
    TermStep env t u (Pi n f g) ->
    TermWf env a f ->
    ---
    TermStep env (App t a) (App u a) (subst g $ sub1 a)
  StepConv :
    TermStep env t u a ->
    TypeConv env a b ->
    ---
    TermStep env t u b

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

namespace Type
  public export
  data TypeRed : Env sx -> Term sx -> Term sx -> Type where
    Stay : TypeWf env a -> TypeRed env a a
    (::) : TypeStep env a b -> TypeRed env b c -> TypeRed env a c

namespace Term
  public export
  data TermRed : Env sx -> Term sx -> Term sx -> Term sx -> Type where
    Stay : TermWf env t a -> TermRed env t t a
    (::) : TermStep env t u a -> TermRed env u v a -> TermRed env t v a

%name TypeStep step
%name TermStep step
%name TypeRed steps
%name TermRed steps

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

termStepImpliesTermConv : TermStep env t u a -> TermConv env t u a
typeStepImpliesTypeConv : TypeStep env a b -> TypeConv env a b
typeRedImpliesTypeConv : TypeRed env a b -> TypeConv env a b
termRedImpliesTermConv : TermRed env t u a -> TermConv env t u a

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

termStepImpliesSubjectWf : TermStep env t u a -> TermWf env t a
typeStepImpliesSubjectWf : TypeStep env a b -> TypeWf env a

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

-- Cannot step from whnf

termStepWhnfImpossible : Whnf t -> Not (TermStep env t u a)
typeStepWhnfImpossible : Whnf a -> Not (TypeStep env a b)

-- Reduction starting from whnf goes nowhere

typeRedWhnfStays : Whnf a -> TypeRed env a b -> a = b
termRedWhnfStays : Whnf t -> TermRed env t u a -> t = u

-- Reduction is Deterministic --------------------------------------------------

termStepDeterministic : TermStep env t u a -> TermStep env t v b -> u = v
typeStepDeterministic : TypeStep env a b -> TypeStep env a c -> b = c
typeRedDeterministic : TypeRed env a b -> TypeRed env a c -> Whnf b -> Whnf c -> b = c
termRedDeterministic : TermRed env t u a -> TermRed env t v b -> Whnf u -> Whnf v -> u = v