{-# 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α))               = 1αC⇒Fac C 1α
WW-Fold-Fac C (inl (inr 1β))               = 1βC⇒Fac C 1β
WW-Fold-Fac C (inr (inl (inl 2α)))         = 2αC⇒Fac C 2α
WW-Fold-Fac C (inr (inl (inr 2β)))         = 2βC⇒Fac C 2β
WW-Fold-Fac C (inr (inr (3α , strictabs))) = 3αC⇒Fac strictabs C 3α

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

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