module Core.Reduction

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

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
termStepImpliesTermConv (PiBeta wf wf1 wf2) = PiBeta wf wf1 wf2
termStepImpliesTermConv (AppStep step wf) = AppConv (termStepImpliesTermConv step) (ReflTerm wf)
termStepImpliesTermConv (StepConv step conv) = ConvTermConv (termStepImpliesTermConv step) conv

typeStepImpliesTypeConv : TypeStep env a b -> TypeConv env a b
typeStepImpliesTypeConv step = LiftConv (termStepImpliesTermConv step)

typeRedImpliesTypeConv : TypeRed env a b -> TypeConv env a b
typeRedImpliesTypeConv (Stay wf) = ReflType wf
typeRedImpliesTypeConv (step :: steps) =
  TransType
    (typeStepImpliesTypeConv step)
    (typeRedImpliesTypeConv steps)

termRedImpliesTermConv : TermRed env t u a -> TermConv env t u a
termRedImpliesTermConv (Stay wf) = ReflTerm wf
termRedImpliesTermConv (step :: steps) =
  TransTerm
    (termStepImpliesTermConv step)
    (termRedImpliesTermConv steps)

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

termStepImpliesSubjectWf : TermStep env t u a -> TermWf env t a
termStepImpliesSubjectWf (PiBeta wf wf1 wf2) = AppTerm (AbsTerm wf wf1) wf2
termStepImpliesSubjectWf (AppStep step wf) = AppTerm (termStepImpliesSubjectWf step) wf
termStepImpliesSubjectWf (StepConv step conv) = ConvTerm (termStepImpliesSubjectWf step) conv

typeStepImpliesSubjectWf : TypeStep env a b -> TypeWf env a
typeStepImpliesSubjectWf step = LiftType (termStepImpliesSubjectWf step)

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

-- Cannot step from whnf

termStepWhnfImpossible : Whnf t -> Not (TermStep env t u a)
termStepWhnfImpossible n (StepConv step conv) = termStepWhnfImpossible n step
termStepWhnfImpossible (Ntrl (App n)) (PiBeta wf wf1 wf2) impossible
termStepWhnfImpossible (Ntrl (App n)) (AppStep step wf) = termStepWhnfImpossible (Ntrl n) step

typeStepWhnfImpossible : Whnf a -> Not (TypeStep env a b)
typeStepWhnfImpossible = termStepWhnfImpossible

-- Reduction starting from whnf goes nowhere

typeRedWhnfStays : Whnf a -> TypeRed env a b -> a = b
typeRedWhnfStays n (Stay wf) = Refl
typeRedWhnfStays n (step :: steps) = absurd $ typeStepWhnfImpossible n step

termRedWhnfStays : Whnf t -> TermRed env t u a -> t = u
termRedWhnfStays n (Stay wf) = Refl
termRedWhnfStays n (step :: steps) = absurd $ termStepWhnfImpossible n step

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

termStepDeterministic : TermStep env t u a -> TermStep env t v b -> u = v
termStepDeterministic (StepConv step conv) step1 = termStepDeterministic step step1
termStepDeterministic step (StepConv step1 conv) = termStepDeterministic step step1
termStepDeterministic (PiBeta _ _ _) (PiBeta _ _ _) = Refl
termStepDeterministic (PiBeta _ _ _) (AppStep step _) = absurd $ termStepWhnfImpossible Abs step
termStepDeterministic (AppStep step _) (PiBeta _ _ _) = absurd $ termStepWhnfImpossible Abs step
termStepDeterministic (AppStep step _) (AppStep step1 _) =
  cong (flip App _) $
  termStepDeterministic step step1

typeStepDeterministic : TypeStep env a b -> TypeStep env a c -> b = c
typeStepDeterministic = termStepDeterministic

typeRedDeterministic : TypeRed env a b -> TypeRed env a c -> Whnf b -> Whnf c -> b = c
typeRedDeterministic (Stay _) red n m = typeRedWhnfStays n red
typeRedDeterministic red (Stay _) n m = sym $ typeRedWhnfStays m red
typeRedDeterministic (step :: steps) (step1 :: steps1) n m =
  let steps1' = rewrite typeStepDeterministic step step1 in steps1 in
  typeRedDeterministic steps steps1' n m

termRedDeterministic : TermRed env t u a -> TermRed env t v b -> Whnf u -> Whnf v -> u = v
termRedDeterministic (Stay _) red n m = termRedWhnfStays n red
termRedDeterministic red (Stay _) n m = sym $ termRedWhnfStays m red
termRedDeterministic (step :: steps) (step1 :: steps1) n m =
  let steps1' : TermRed env _ v b = rewrite termStepDeterministic step step1 in steps1 in
  termRedDeterministic steps steps1' n m

-- Weakening Preservation ------------------------------------------------------

wknPresTermStep :
  {0 env1 : Env sx} ->
  TermStep env1 t u a ->
  EnvWf env2 ->
  IsExtension thin env2 env1 ->
  TermStep env2 (wkn t thin) (wkn u thin) (wkn a thin)
wknPresTermStep (PiBeta {f, g, n, t, u} wf wf1 wf2) envWf ext =
  rewrite wknSub1 g u thin in
  rewrite wknSub1 t u thin in
  let wf' = wknPresTypeWf wf envWf ext in
  PiBeta wf'
    (termWfRespEnvEq
      (wknPresTermWf wf1 (envWf :< wf') $
       replace {p = \thin' => IsExtension (keep thin n) (Add env2 (f `Over` thin')) (env1 :< f)}
         (compRightIdentity thin)
         (KeepWf ext))
      ((:<) {t = f `Over` thin} Base (sym $ wknId $ expand $ f `Over` thin)))
    (wknPresTermWf wf2 envWf ext)
wknPresTermStep (AppStep {g, a} step wf) envWf ext =
  rewrite wknSub1 g a thin in
  AppStep (wknPresTermStep step envWf ext) (wknPresTermWf wf envWf ext)
wknPresTermStep (StepConv step conv) envWf ext =
  StepConv (wknPresTermStep step envWf ext) (wknPresTypeConv conv envWf ext)

wknPresTypeStep :
  {0 env1 : Env sx} ->
  TypeStep env1 a b ->
  EnvWf env2 ->
  IsExtension thin env2 env1 ->
  TypeStep env2 (wkn a thin) (wkn b thin)
wknPresTypeStep = wknPresTermStep

wknPresTypeRed :
  {0 env1 : Env sx} ->
  TypeRed env1 a b ->
  EnvWf env2 ->
  IsExtension thin env2 env1 ->
  TypeRed env2 (wkn a thin) (wkn b thin)
wknPresTypeRed (Stay wf) envWf ext = Stay (wknPresTypeWf wf envWf ext)
wknPresTypeRed (step :: steps) envWf ext =
  wknPresTypeStep step envWf ext :: wknPresTypeRed steps envWf ext

wknPresTermRed :
  {0 env1 : Env sx} ->
  TermRed env1 t u a ->
  EnvWf env2 ->
  IsExtension thin env2 env1 ->
  TermRed env2 (wkn t thin) (wkn u thin) (wkn a thin)
wknPresTermRed (Stay wf) envWf ext = Stay (wknPresTermWf wf envWf ext)
wknPresTermRed (step :: steps) envWf ext =
  wknPresTermStep step envWf ext :: wknPresTermRed steps envWf ext