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

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

module WWFoldInstantiate

  (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
    hiding (RollingRuleFold ; ComputationFold ; FoldFusion ; FoldReflectsStrictness ; FoldFunctorProp)

import FoldTheoremsInstantiated
open FoldTheoremsInstantiated ext fix Computation Induction fix-⊗ FixpointInduction F fmap' fmap-id fmap-comp μ inn out innSur outInj lemma-fold-inn

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

2α⇒2β : Strict f → Cond2α → Cond2β
2α⇒2β sf (β , sr) = sym (FoldFusionInstantiated f g rep sf sr β)

1β⇔2β : Strict abs → Strict rep → Strict f → AssC → Cond1β ↔ Cond2β
1β⇔2β sa sr sf C = ↔-≡ refl (

   fold (rep ∙ f ∙ fmap abs)
                                                ⟨ cong fold (∙-assocRL rep f (fmap abs)) ⟩
   fold ((rep ∙ f) ∙ fmap abs)
                                                ⟨ RollingRuleFoldInstantiated (rep ∙ f) (fmap abs) (StrictComposition f rep sf sr) (FmapPreservesStrictness abs sa) ⟩
   (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))
                                                                                        ⟨ FoldFunctorPropInstantiated
                                                                                             (abs ∙ rep ∙ f)
                                                                                             f
                                                                                             (StrictComposition (rep ∙ f) abs (StrictComposition f rep sf sr) sa)
                                                                                             sf
                                                                                             C
                                                                                        ⟩
                                                      fold (fmap f)
                                                                                        QED)
                                                ⟩
   (rep ∙ f) ∙ fold (fmap f)
                                                ⟨ ∙-assocLR rep f (fold (fmap f)) ⟩
   rep ∙ f ∙ fold (fmap f)
                                                ⟨ ∙-congL rep (sym (ComputationFoldInstantiated f sf)) ⟩
   rep ∙ fold f
                                                QED
   )


1βC⇒Fac : Strict abs → Strict rep → Strict f → AssC → Cond1β → WWFactorisation
1βC⇒Fac sa sr sf C β =

   fold f
                                       ⟨ sym C ⟩
   fold (abs ∙ rep ∙ f)
                                       ⟨ RollingRuleFoldInstantiated abs (rep ∙ f) sa (StrictComposition f rep sf sr) ⟩
   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 : Strict abs → Strict rep → Strict f → AssC → Cond2β → WWFactorisation
2βC⇒Fac sa sr sf C β = 1βC⇒Fac sa sr sf C (snd (1β⇔2β sa sr sf C) β)

1αC⇒Fac : Strict abs → Strict rep → Strict f → AssC → Cond1α → WWFactorisation
1αC⇒Fac sa sr sf C = 1βC⇒Fac sa sr sf C ∘ 1α⇒1β

2αC⇒Fac : Strict abs → Strict rep → Strict f → AssC → Cond2α → WWFactorisation
2αC⇒Fac sa sr sf C = 2βC⇒Fac sa sr sf C ∘ 2α⇒2β sf

2βC⇒Fusion : Strict abs → Strict rep → Strict f → AssC → Cond2β → WWFusion
2βC⇒Fusion sa sr sf C β =
                           rep ∙ abs ∙ fold g
                                              ⟨ ∙-congL rep (sym (2βC⇒Fac sa sr sf C β)) ⟩
                           rep ∙ fold f
                                              ⟨ sym β ⟩
                           fold g
                                              QED


1βC⇒Fusion : Strict abs → Strict rep → Strict f → AssC → Cond1β → WWFusion
1βC⇒Fusion sa sr sf C β = 2βC⇒Fusion sa sr sf C (fst (1β⇔2β sa sr sf C) β)

1αC⇒Fusion : Strict abs → Strict rep → Strict f → AssC → Cond1α → WWFusion
1αC⇒Fusion sa sr sf C = 1βC⇒Fusion sa sr sf C ∘ 1α⇒1β

2αC⇒Fusion : Strict abs → Strict rep → Strict f → AssC → Cond2α → WWFusion
2αC⇒Fusion sa sr sf C = 2βC⇒Fusion sa sr sf C ∘ 2α⇒2β sf

FactFusion⇔2β : Strict abs → Strict rep → Strict f → AssC → Cond2β ↔ (WWFactorisation × WWFusion)
FactFusion⇔2β sa sr sf C = (λ β → 2βC⇒Fac sa sr sf C β , 2βC⇒Fusion sa sr sf C β) , uncurry (FactFusionC⇒2β C)

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

3αC⇒Fac : Strict abs → Strict g → AssC → Cond3α → WWFactorisation
3αC⇒Fac sa sg C α = sym (FoldFusionInstantiated g f abs sg sa α)

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

-- Note the many strictness conditions

WW-Fold-Fac : AssC → Strict abs → (((Cond1α ⊎ Cond1β) ⊎ (Cond2α ⊎ Cond2β)) × Strict rep × Strict f) ⊎ (Cond3α × Strict g) → WWFactorisation
WW-Fold-Fac C sa (inl (inl (inl 1α) , sr , sf))  = 1αC⇒Fac sa sr sf C 1α
WW-Fold-Fac C sa (inl (inl (inr 1β) , sr , sf))  = 1βC⇒Fac sa sr sf C 1β
WW-Fold-Fac C sa (inl (inr (inl 2α) , sr , sf))  = 2αC⇒Fac sa sr sf C 2α
WW-Fold-Fac C sa (inl (inr (inr 2β) , sr , sf))  = 2βC⇒Fac sa sr sf C 2β
WW-Fold-Fac C sa (inr (3α , sg))                 = 3αC⇒Fac sa sg C 3α

WW-Fold-Fusion : AssC → Strict abs → Strict rep → Strict f → (Cond1α ⊎ Cond1β) ⊎ (Cond2α ⊎ Cond2β) → WWFusion
WW-Fold-Fusion C sa sr sf (inl (inl 1α)) = 1αC⇒Fusion sa sr sf C 1α
WW-Fold-Fusion C sa sr sf (inl (inr 1β)) = 1βC⇒Fusion sa sr sf C 1β
WW-Fold-Fusion C sa sr sf (inr (inl 2α)) = 2αC⇒Fusion sa sr sf C 2α
WW-Fold-Fusion C sa sr sf (inr (inr 2β)) = 2βC⇒Fusion sa sr sf C 2β

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