{-# OPTIONS --type-in-type #-}

open import NeilPrelude
open import Extensionality
open import Logic
open import EquationalEq
open import CPO
open import CPOLemmas
open import CPOFunctions
import Fold

module WWFoldDirect

  (ext : Extensionality)

  (fix : {τ : Type}  CPO (τ  τ)  CPO τ)
  (Computation : {τ : Type}  (f : CPO (τ  τ))  fix f  f $ (fix f))
  (Induction : {τ : Type}  {x : CPO τ}   (f : CPO (τ  τ))  f $ x  x  fix f  x)

  (fix-⊗ : {σ τ : Type}  {f : CPO (σ  σ)}  {g : CPO (τ  τ)}  fix (f :×: g)  (fix f , fix g))

  (FixpointInduction : {τ : Type}  (P : CPO τ  Set)  (f : CPO (τ  τ))  ChainComplete P  P   ((x : CPO τ)  P x  P (f $ x))  P (fix f))

  (F : Functor)
  (fmap' : {σ τ : Type}  CPO ((σ  τ)  (F σ  F τ)))
  (fmap-id   : {τ : Type}  fmap' $ identity {τ}  identity)
  (fmap-comp : {σ τ υ : Type}  (f : CPO (τ  υ))  (g : CPO (σ  τ))  fmap' $ (f  g)  (fmap' $ f)  (fmap' $ g))

  (μ : Functor  Type)
  (inn    : CPO (F (μ F)  μ F))
  (out    : CPO (μ F  F (μ F)))
  (innSur : inn  out  identity)
  (outInj : out  inn  identity)
  (lemma-fold-inn : (Fold.fold ext fix F fmap' μ out) inn  identity)

  (A : Type)
  (B : Type)

  (f   : CPO (F A  A))
  (g   : CPO (F B  B))
  (rep : CPO (A  B))
  (abs : CPO (B  A))

where

import WWFoldCommon
open WWFoldCommon ext fix Computation Induction fix-⊗ FixpointInduction F fmap' fmap-id fmap-comp μ inn out innSur outInj lemma-fold-inn A B f g rep abs

------------------------------------------------

2α⇒2β : Cond2α  Cond2β
2α⇒2β (β , strictrep) = sym (FoldFusion f g rep strictrep β)

1β⇔2β : AssC  Cond1β  Cond2β
1β⇔2β C = ↔-≡ refl (

   fold (rep  f  fmap abs)
                                                 cong fold (∙-assocRL rep f (fmap abs)) 
   fold ((rep  f)  fmap abs)
                                                 RollingRuleFold (rep  f) (fmap abs) 
   (rep  f)  fold (fmap abs  fmap (rep  f))
                                                 ∙-congL (rep  f) (
                                                      fold (fmap abs  fmap (rep  f))
                                                                                        cong fold (sym (fmap-comp abs (rep  f))) 
                                                      fold (fmap (abs  rep  f))
                                                                                        FoldFunctorProp (abs  rep  f) f C 
                                                      fold (fmap f)
                                                                                       QED)
                                                
   (rep  f)  fold (fmap f)
                                                 ∙-assocLR rep f (fold (fmap f)) 
   rep  f  fold (fmap f)
                                                 ∙-congL rep (sym (ComputationFold f)) 
   rep  fold f
                                                QED
   )

1βC⇒Fac : AssC  Cond1β  WWFactorisation
1βC⇒Fac C β =

   fold f
                                       sym C 
   fold (abs  rep  f)
                                       RollingRuleFold abs (rep  f) 
   abs  fold ((rep  f)  fmap abs)
                                       ∙-congL abs (
                                            fold ((rep  f)  fmap abs)
                                                                          cong fold (∙-assocLR rep f (fmap abs)) 
                                            fold (rep  f  fmap abs)
                                                                          sym β 
                                            fold g
                                                                         QED
                                            )
                                      
   abs  fold g
                                      QED

2βC⇒Fac : AssC  Cond2β  WWFactorisation
2βC⇒Fac C β = 1βC⇒Fac C (snd (1β⇔2β C) β)

1αC⇒Fac : AssC  Cond1α  WWFactorisation
1αC⇒Fac C = 1βC⇒Fac C  1α⇒1β

2αC⇒Fac : AssC  Cond2α  WWFactorisation
2αC⇒Fac C = 2βC⇒Fac C  2α⇒2β

2βC⇒Fusion : AssC  Cond2β  WWFusion
2βC⇒Fusion C β =

    rep  abs  fold g
                         ∙-congL rep (sym (2βC⇒Fac C β)) 
    rep  fold f
                         sym β 
    fold g
                        QED

1βC⇒Fusion : AssC  Cond1β  WWFusion
1βC⇒Fusion C β = 2βC⇒Fusion C (fst (1β⇔2β C) β)

1αC⇒Fusion : AssC  Cond1α  WWFusion
1αC⇒Fusion C = 1βC⇒Fusion C  1α⇒1β

2αC⇒Fusion : AssC  Cond2α  WWFusion
2αC⇒Fusion C = 2βC⇒Fusion C  2α⇒2β

FactFusion⇔2β : AssC  Cond2β  (WWFactorisation × WWFusion)
FactFusion⇔2β C =  β  2βC⇒Fac C β , 2βC⇒Fusion C β) , uncurry (FactFusionC⇒2β C)

------------------------------------------------

-- Using FoldFusion requires Strict abs
3αC⇒Fac : Strict abs  AssC  Cond3α  WWFactorisation
3αC⇒Fac strictabs C α = sym (FoldFusion g f abs strictabs α)

------------------------------------------------

-- Note the strictness condition
WW-Fold-Fac : AssC  (Cond1α  Cond1β)  (Cond2α  Cond2β)  (Cond3α × Strict abs)  WWFactorisation
WW-Fold-Fac C (inl (inl ))               = 1αC⇒Fac C 
WW-Fold-Fac C (inl (inr ))               = 1βC⇒Fac C 
WW-Fold-Fac C (inr (inl (inl )))         = 2αC⇒Fac C 
WW-Fold-Fac C (inr (inl (inr )))         = 2βC⇒Fac C 
WW-Fold-Fac C (inr (inr ( , strictabs))) = 3αC⇒Fac strictabs C 

WW-Fold-Fusion : AssC  (Cond1α  Cond1β)  (Cond2α  Cond2β)  WWFusion
WW-Fold-Fusion C (inl (inl )) = 1αC⇒Fusion C 
WW-Fold-Fusion C (inl (inr )) = 1βC⇒Fusion C 
WW-Fold-Fusion C (inr (inl )) = 2αC⇒Fusion C 
WW-Fold-Fusion C (inr (inr )) = 2βC⇒Fusion C 

------------------------------------------------