{-# OPTIONS --lossy-unification --safe #-}

open import Algebra
open import Algebra.Monus
open import Prelude
open import Path.Reasoning

module Data.Weighted.CutoffMonus {β„“} {𝑆 : Type β„“} (mon : TMAPOM 𝑆) where

open TMAPOM mon

open import Data.Weighted.Definition βŠ“-semigroup
open import Data.Weighted.CommutativeMonoid βŠ“-semigroup
open import Data.Weighted.Monad (weight 𝑆 tapom)
open import Data.Weighted.Cutoff totalOrder
open import Data.Weighted.Eliminators βŠ“-semigroup
open import Data.Weighted.Functor

⊒-wmap : βˆ€ (f : A β†’ B) x w β†’ wmap f x ⊒ w ≑ wmap f (x ⊒ w)
⊒-wmap f x w = ⟦ alg f w ⟧ x
  where
  alg : βˆ€ (f : A β†’ B) w β†’ Ξ¨[ x ⦂ Weighted A ] ↦ wmap f x ⊒ w ≑ wmap f (x ⊒ w)
  alg f w .snd = eq-coh
  alg f w .fst βŸ…βŸ† = refl
  alg f w .fst (q β–Ή x ∷ xs ⟨ P⟨xs⟩ ⟩) with q ≀? w
  ... | yes _ = cong (q β–Ή f x ∷_) P⟨xs⟩
  ... | no _ = P⟨xs⟩

>-β‹Š-⊒ : βˆ€ w (s : Weighted A) v β†’ w > v β†’ (w β‹Š s) ⊒ v ≑ βŸ…βŸ†
>-β‹Š-⊒ w s v w>v = ⟦ alg w v w>v ⟧ s
  where
  alg : βˆ€ w v β†’ w > v β†’ Ξ¨[ s ⦂ Weighted A ] ↦ (w β‹Š s) ⊒ v ≑ βŸ…βŸ†
  alg w v w>v .snd = eq-coh
  alg w v w>v .fst βŸ…βŸ† = refl
  alg w v w>v .fst (u β–Ή x ∷ xs ⟨ P⟨xs⟩ ⟩) =
    (w β‹Š u β–Ή x ∷ xs) ⊒ v         β‰‘βŸ¨βŸ©
    (w βˆ™ u β–Ή x ∷ w β‹Š xs) ⊒ v     β‰‘βŸ¨βŸ©
    v / w βˆ™ u β–Ή x βˆͺ (w β‹Š xs) ⊒ v β‰‘βŸ¨ cong (_βˆͺ (w β‹Š xs) ⊒ v) (/β‰° v (w βˆ™ u) x ≲[ <[ w>v ] ≲; ≀[ x≀xβˆ™y ] ]) ⟩
    (w β‹Š xs) ⊒ v β‰‘βŸ¨ P⟨xs⟩ ⟩
    βŸ…βŸ† ∎

module Depth where
  Deeper : 𝑆 β†’ Weighted A β†’ Type-
  Deeper w x = βˆƒ y Γ— w β‹Š y ≑ x

  deeper-β‰₯ : βˆ€ v w (x : Weighted A) β†’ Deeper v x β†’ v β‰₯ w β†’ Deeper w x
  deeper-β‰₯ v w x (y , v>|x) (k , v≑wβˆ™k) = k β‹Š y , (β‹Š-assoc w k y ΝΎ cong (_β‹Š y) (sym v≑wβˆ™k) ΝΎ v>|x)

  Ξ΅-deeper : (x : Weighted A) β†’ Deeper Ξ΅ x
  Ξ΅-deeper x = x , Ξ΅β‹Š x

return-⊒ : βˆ€ (x : A) w β†’ return x ⊒ w ≑ return x
return-⊒ x w = βˆͺ-idΚ³ _ ΝΎ /≀ w Ξ΅ x (positive w)

>>=-⊒-lemma : βˆ€ w v (x : A) (k : A β†’ Weighted B) β†’ (w β‹Š k x) ⊒ v ≑ (v / w β–Ή x >>= k) ⊒ v
>>=-⊒-lemma w v x k with w ≀? v
... | no  wβ‰°v = >-β‹Š-⊒ w (k x) v wβ‰°v
... | yes w≀v = sym (cong (_⊒ v) (βˆͺ-idΚ³ (w β‹Š k x)))

>>=-⊒ˑ : βˆ€ v (s : Weighted A) (k : A β†’ Weighted B) β†’
  (s >>= k) ⊒ v ≑ (s ⊒ v >>= k) ⊒ v
>>=-⊒ˑ v s k = ⟦ alg v k ⟧ s
  where
  alg : βˆ€ v (k : A β†’ Weighted B) β†’ Ξ¨[ s ⦂ Weighted A ] ↦ (s >>= k) ⊒ v ≑ (s ⊒ v >>= k) ⊒ v
  alg v k .snd = eq-coh
  alg v k .fst βŸ…βŸ† = refl
  alg v k .fst (w β–Ή x ∷ xs ⟨ P⟨xs⟩ ⟩) =
    (w β–Ή x ∷ xs >>= k) ⊒ v                     β‰‘βŸ¨βŸ©
    ((w β‹Š k x) βˆͺ (xs >>= k)) ⊒ v               β‰‘βŸ¨ ⊒-βˆͺ (w β‹Š k x) _ _ ⟩
    (w β‹Š k x) ⊒ v βˆͺ (xs >>= k) ⊒ v             β‰‘βŸ¨ cong ((w β‹Š k x) ⊒ v βˆͺ_) P⟨xs⟩ ⟩
    (w β‹Š k x) ⊒ v βˆͺ (xs ⊒ v >>= k) ⊒ v         β‰‘βŸ¨ cong (_βˆͺ (xs ⊒ v >>= k) ⊒ v) (>>=-⊒-lemma w v x k ) ⟩
    (v / w β–Ή x >>= k) ⊒ v βˆͺ (xs ⊒ v >>= k) ⊒ v β‰‘Λ˜βŸ¨ ⊒-βˆͺ (v / w β–Ή x >>= k) _ _ ⟩
    ((v / w β–Ή x >>= k) βˆͺ (xs ⊒ v >>= k)) ⊒ v   β‰‘Λ˜βŸ¨ cong (_⊒ v) (>>=-βˆͺ (v / w β–Ή x) _ k) ⟩
    (v / w β–Ή x βˆͺ xs ⊒ v >>= k) ⊒ v             β‰‘βŸ¨βŸ©
    ((w β–Ή x ∷ xs) ⊒ v >>= k) ⊒ v ∎

/βˆ™βŠ’ : βˆ€ u v w (x : A) β†’ v / w βˆ™ u β–Ή x ≑ (w β‹Š v / u β–Ή x) ⊒ v
/βˆ™βŠ’ u v w x with u ≀? v
... | yes _ = sym (βˆͺ-idΚ³ (v / w βˆ™ u β–Ή x))
... | no u>v = /β‰° v (w βˆ™ u) x ≲[ <[ u>v ] ≲; ≀[ x≀xβˆ™y ] ≲; ≑[ comm u w ] ]

>>=-⊒ʳ-lemma : βˆ€ w (s : Weighted A) v β†’ (w β‹Š s) ⊒ v ≑ (w β‹Š s ⊒ v) ⊒ v
>>=-⊒ʳ-lemma w s v = ⟦ alg w v ⟧ s
  where
  alg : βˆ€ w v β†’ Ξ¨[ s ⦂ Weighted A ] ↦ (w β‹Š s) ⊒ v ≑ (w β‹Š s ⊒ v) ⊒ v
  alg w v .snd = eq-coh
  alg w v .fst βŸ…βŸ† = refl
  alg w v .fst (u β–Ή x ∷ xs ⟨ P⟨xs⟩ ⟩) =
    (w β‹Š u β–Ή x ∷ xs) ⊒ v                   β‰‘βŸ¨βŸ©
    (w βˆ™ u β–Ή x ∷ w β‹Š xs) ⊒ v               β‰‘βŸ¨βŸ©
    v / w βˆ™ u β–Ή x βˆͺ (w β‹Š xs) ⊒ v           β‰‘βŸ¨ cong (v / w βˆ™ u β–Ή x βˆͺ_) P⟨xs⟩ ⟩
    v / w βˆ™ u β–Ή x βˆͺ (w β‹Š xs ⊒ v) ⊒ v       β‰‘βŸ¨ cong (_βˆͺ (w β‹Š xs ⊒ v) ⊒ v) (/βˆ™βŠ’ u v w x) ⟩
    (w β‹Š v / u β–Ή x) ⊒ v βˆͺ (w β‹Š xs ⊒ v) ⊒ v β‰‘Λ˜βŸ¨ ⊒-βˆͺ (w β‹Š v / u β–Ή x) _ v ⟩
    ((w β‹Š v / u β–Ή x) βˆͺ (w β‹Š xs ⊒ v)) ⊒ v   β‰‘Λ˜βŸ¨ cong (_⊒ v) (β‹ŠβŸ¨βˆͺ⟩ w (v / u β–Ή x) _) ⟩
    (w β‹Š v / u β–Ή x βˆͺ xs ⊒ v) ⊒ v           β‰‘βŸ¨βŸ©
    (w β‹Š (u β–Ή x ∷ xs) ⊒ v) ⊒ v ∎

>>=-⊒ʳ : βˆ€ v (s : Weighted A) (k : A β†’ Weighted B) β†’
  (s >>= k) ⊒ v ≑ (s >>= k ∘⊒ v) ⊒ v
>>=-⊒ʳ v s k = ⟦ alg v k ⟧ s
  where
  alg : βˆ€ v (k : A β†’ Weighted B) β†’ Ξ¨[ s ⦂ Weighted A ] ↦ (s >>= k) ⊒ v ≑ (s >>= k ∘⊒ v) ⊒ v
  alg v k .snd = eq-coh
  alg v k .fst βŸ…βŸ† = refl
  alg v k .fst (w β–Ή x ∷ xs ⟨ P⟨xs⟩ ⟩) =
    (w β–Ή x ∷ xs >>= k) ⊒ v                  β‰‘βŸ¨βŸ©
    ((w β‹Š k x) βˆͺ (xs >>= k)) ⊒ v            β‰‘βŸ¨ ⊒-βˆͺ (w β‹Š k x) _ _ ⟩
    (w β‹Š k x) ⊒ v βˆͺ (xs >>= k) ⊒ v          β‰‘βŸ¨ cong ((w β‹Š k x) ⊒ v βˆͺ_) P⟨xs⟩ ⟩
    (w β‹Š k x) ⊒ v βˆͺ (xs >>= k ∘⊒ v) ⊒ v     β‰‘βŸ¨ cong (_βˆͺ (xs >>= k ∘⊒ v) ⊒ v) (>>=-⊒ʳ-lemma w (k x) v) ⟩
    (w β‹Š k x ⊒ v) ⊒ v βˆͺ (xs >>= k ∘⊒ v) ⊒ v β‰‘Λ˜βŸ¨ ⊒-βˆͺ (w β‹Š k x ⊒ v) _ _ ⟩
    ((w β‹Š k x ⊒ v) βˆͺ (xs >>= k ∘⊒ v)) ⊒ v   β‰‘βŸ¨βŸ©
    (w β–Ή x ∷ xs >>= k ∘⊒ v) ⊒ v ∎

module _ {A : Type a} where
  β‹Š-βˆͺ-β‹Š : βˆ€ (x y : Weighted A) p q β†’ p ≀ q β†’ y βŠ‘ x β†’ q β‹Š y βŠ† p β‹Š x
  β‹Š-βˆͺ-β‹Š x y p q p≀q (k , yβŠ‘x) = βˆͺ-com (q β‹Š y) (p β‹Š x) ΝΎ cong (Ξ» e β†’ (p β‹Š x) βˆͺ (q β‹Š e)) yβŠ‘x ΝΎ ⟦ alg ⟧ x
    where
    alg : Ξ¨[ x ⦂ Weighted A ] ↦ (p β‹Š x) βˆͺ (q β‹Š x ⊒ k) ≑ p β‹Š x
    alg .fst βŸ…βŸ† = refl
    alg .fst (w β–Ή x ∷ xs ⟨ P⟨xs⟩ ⟩) with w ≀? k
    ... | yes w≀k =
      (p β‹Š w β–Ή x ∷ xs) βˆͺ (q β‹Š w β–Ή x ∷ (xs ⊒ k))            β‰‘βŸ¨βŸ©
      (p βˆ™ w β–Ή x ∷ p β‹Š xs) βˆͺ (q βˆ™ w β–Ή x ∷ q β‹Š (xs ⊒ k))    β‰‘Λ˜βŸ¨ cong (p βˆ™ w β–Ή x ∷_) (βˆͺ-cons (q βˆ™ w) x _ _) ⟩
      p βˆ™ w β–Ή x ∷ q βˆ™ w β–Ή x ∷ (p β‹Š xs) βˆͺ (q β‹Š xs ⊒ k)      β‰‘βŸ¨ dup (p βˆ™ w) (q βˆ™ w) x _ ⟩
      ((p βˆ™ w) βŠ“ (q βˆ™ w)) β–Ή x ∷ (p β‹Š xs) βˆͺ (q β‹Š (xs ⊒ k))  β‰‘βŸ¨ cong (_β–Ή x ∷ ((p β‹Š xs) βˆͺ (q β‹Š xs ⊒ k))) (βŠ“β‰€β‰‘ (p βˆ™ w) (q βˆ™ w) (≀-congΚ³ w p≀q)) ⟩
      (p βˆ™ w) β–Ή x ∷ (p β‹Š xs) βˆͺ (q β‹Š (xs ⊒ k))              β‰‘βŸ¨ cong (p βˆ™ w β–Ή x ∷_) P⟨xs⟩ ⟩
      (p βˆ™ w) β–Ή x ∷ (p β‹Š xs)                                β‰‘βŸ¨βŸ©
      p β‹Š w β–Ή x ∷ xs ∎
    ... | no  w≰k =
      (p β‹Š w β–Ή x ∷ xs) βˆͺ (q β‹Š (xs ⊒ k))     β‰‘βŸ¨βŸ©
      p βˆ™ w β–Ή x ∷ (p β‹Š xs) βˆͺ (q β‹Š (xs ⊒ k)) β‰‘βŸ¨ cong (p βˆ™ w β–Ή x ∷_) P⟨xs⟩ ⟩
      p βˆ™ w β–Ή x ∷ (p β‹Š xs)                   β‰‘βŸ¨βŸ©
      p β‹Š w β–Ή x ∷ xs ∎
    alg .snd = eq-coh