\begin{code}
{-# OPTIONS --cubical --safe #-}

open import Algebra
open import Level

module Control.Monad.Weighted.Cond {β„“} {𝑅 : Type β„“} (rng : Semiring 𝑅) where

open Semiring rng

open import Level
open import Path
open import Path.Reasoning
open import HLevels
open import Data.Sigma

open import Control.Monad.Weighted.Definition rng
open import Control.Monad.Weighted.Eliminators rng
open import Control.Monad.Weighted.Union rng

open import Control.Monad.Weighted.Functor rng
open import Control.Monad.Weighted.Functor.TypeDef
\end{code}
%<*cond-alg>
\begin{code}
β‹Š-alg : 𝑅 β†’ Ξ¦ A (Weighted A)
β‹Š-alg w .fst (p β—ƒ x ∷ xs ⟨ wβ‹Šxs ⟩)  = (w * p) β—ƒ x ∷ wβ‹Šxs
β‹Š-alg w .fst []                     = []
\end{code}
%</cond-alg>
%<*cond-coh>
\begin{code}
β‹Š-alg w .snd .c-com p x q  y xs wβ‹Šxs = com (w * p) x (w * q) y wβ‹Šxs

β‹Š-alg w .snd .c-dup p q x xs wβ‹Šxs =
                             w * p β—ƒ x ∷ w * q β—ƒ x ∷ wβ‹Šxs  β‰‘βŸ¨ dup (w * p) (w * q) x wβ‹Šxs ⟩
                             w * p + w * q β—ƒ x ∷ wβ‹Šxs      β‰‘Λ˜βŸ¨ cong (_β—ƒ x ∷ wβ‹Šxs) (*⟨+⟩ w p q) ⟩
                             w * (p + q) β—ƒ x ∷ wβ‹Šxs ∎

β‹Š-alg w .snd .c-del x xs wβ‹Šxs =
                             w * 0# β—ƒ x ∷ wβ‹Šxs  β‰‘βŸ¨ cong (_β—ƒ x ∷ wβ‹Šxs) (*0 w) ⟩
                             0# β—ƒ x ∷ wβ‹Šxs      β‰‘βŸ¨ del x wβ‹Šxs ⟩
                             wβ‹Šxs ∎
\end{code}
%</cond-coh>
\begin{code}
β‹Š-alg c .snd .c-set _ = trunc

infixr 5.5 _β‹Š_
\end{code}
%<*cond-impl>
\begin{code}
_β‹Š_ : 𝑅 β†’ Weighted A β†’ Weighted A
x β‹Š xs = ⟦ β‹Š-alg x ⟧ xs
\end{code}
%</cond-impl>
\begin{code}

_ : βˆ€ {w w₁ wβ‚‚ w₃} β†’ {x y z : A} β†’
\end{code}
%<*cond-example>
\begin{code}
  w β‹Š (w₁ β—ƒ x ∷ wβ‚‚ β—ƒ y ∷ w₃ β—ƒ z ∷ []) ≑ (w * w₁) β—ƒ x ∷ (w * wβ‚‚) β—ƒ y ∷ (w * w₃) β—ƒ z ∷ []
\end{code}
%</cond-example>
\begin{code}
_ = refl

β‹Š-distribΚ³ : βˆ€ p q β†’ (xs : Weighted A) β†’ (p β‹Š xs) βˆͺ (q β‹Š xs) ≑ p + q β‹Š xs
β‹Š-distribΚ³ p q = ⟦ β‹Š-distribΚ³β€² p q ⟧
  where
  β‹Š-distribΚ³β€² : βˆ€ p q β†’ Ξ¨[ xs ⦂ A ] (p β‹Š xs) βˆͺ (q β‹Š xs) ≑ (p + q) β‹Š xs
  β‹Š-distribΚ³β€² p q .fst [] = refl
  β‹Š-distribΚ³β€² p q .fst (r β—ƒ x ∷ xs ⟨ P ⟩) =
    (p β‹Š (r β—ƒ x ∷ xs)) βˆͺ (q β‹Š (r β—ƒ x ∷ xs))  β‰‘Λ˜βŸ¨ βˆͺ-cons (q * r) x (p β‹Š (r β—ƒ x ∷ xs)) (q β‹Š xs)  ⟩
    q * r β—ƒ x ∷ (p β‹Š (r β—ƒ x ∷ xs)) βˆͺ q β‹Š xs  β‰‘βŸ¨ cong (_βˆͺ q β‹Š xs) (dup (q * r) (p * r) x (p β‹Š xs)) ⟩
    q * r + p * r β—ƒ x ∷ (p β‹Š xs) βˆͺ q β‹Š xs    β‰‘Λ˜βŸ¨ cong (_β—ƒ x ∷ ((p β‹Š xs) βˆͺ (q β‹Š xs))) (⟨+⟩* q p r) ⟩
    (q + p) * r β—ƒ x ∷ (p β‹Š xs) βˆͺ (q β‹Š xs)    β‰‘βŸ¨ cong ((q + p) * r β—ƒ x ∷_) P ⟩
    (q + p) * r β—ƒ x ∷ (p + q) β‹Š xs           β‰‘βŸ¨ cong (Ξ» pq β†’ pq * r β—ƒ x ∷ (p + q) β‹Š xs) (+-comm q p) ⟩
    (p + q) * r β—ƒ x ∷ (p + q) β‹Š xs           β‰‘βŸ¨βŸ©
    (p + q) β‹Š (r β—ƒ x ∷ xs) ∎
  β‹Š-distribΚ³β€² p q .snd = eq-coh

β‹Š-distribΛ‘ : βˆ€ p β†’ (xs ys : Weighted A) β†’ (p β‹Š xs) βˆͺ (p β‹Š ys) ≑ p β‹Š (xs βˆͺ ys)
β‹Š-distribΛ‘ = Ξ» p xs ys β†’ ⟦ β‹Š-distribΛ‘β€² p ys ⟧ xs
  module JDistribL where
  β‹Š-distribΛ‘β€² : βˆ€ p ys β†’ Ξ¨[ xs ⦂ A ] (p β‹Š xs) βˆͺ (p β‹Š ys) ≑ p β‹Š (xs βˆͺ ys)
  β‹Š-distribΛ‘β€² p ys .fst [] = refl
  β‹Š-distribΛ‘β€² p ys .fst (q β—ƒ x ∷ xs ⟨ P ⟩) = cong (p * q β—ƒ x ∷_) P
  β‹Š-distribΛ‘β€² p ys .snd = eq-coh

0β‹Š : (xs : Weighted A) β†’ 0# β‹Š xs ≑ []
0β‹Š = ⟦ 0β‹Šβ€² ⟧
  where
  0β‹Šβ€² : Ξ¨[ xs ⦂ A ] 0# β‹Š xs ≑ []
  0β‹Šβ€² .fst [] = refl
  0β‹Šβ€² .fst (p β—ƒ x ∷ xs ⟨ P ⟩) =
    0# β‹Š (p β—ƒ x ∷ xs)     β‰‘βŸ¨βŸ©
    0# * p β—ƒ x ∷ 0# β‹Š xs  β‰‘βŸ¨ cong (_β—ƒ x ∷ 0# β‹Š xs) (0* p) ⟩
    0# β—ƒ x ∷ 0# β‹Š xs      β‰‘βŸ¨ del x (0# β‹Š xs) ⟩
    0# β‹Š xs               β‰‘βŸ¨ P ⟩
    [] ∎
  0β‹Šβ€² .snd = eq-coh

1β‹Š : (xs : Weighted A) β†’ 1# β‹Š xs ≑ xs
1β‹Š = ⟦ 1β‹Šβ€² ⟧
  where
  1β‹Šβ€² : Ξ¨[ xs ⦂ A ] 1# β‹Š xs ≑ xs
  1β‹Šβ€² .fst [] = refl
  1β‹Šβ€² .fst (p β—ƒ x ∷ xs ⟨ P ⟩) =
    1# β‹Š (p β—ƒ x ∷ xs) β‰‘βŸ¨βŸ©
    1# * p β—ƒ x ∷ 1# β‹Š xs β‰‘βŸ¨ cong (_β—ƒ x ∷ 1# β‹Š xs) (1* p) ⟩
    p β—ƒ x ∷ 1# β‹Š xs β‰‘βŸ¨ cong (p β—ƒ x ∷_) P ⟩
    p β—ƒ x ∷ xs ∎
  1β‹Šβ€² .snd = eq-coh

*-assoc-β‹Š : βˆ€ p q (xs : Weighted A) β†’ (p * q) β‹Š xs ≑ p β‹Š (q β‹Š xs)
*-assoc-β‹Š p q = ⟦ *-assoc-β‹Šβ€² p q ⟧
  where
  *-assoc-β‹Šβ€² : βˆ€ p q β†’ Ξ¨[ xs ⦂ A ] (p * q) β‹Š xs ≑ p β‹Š (q β‹Š xs)
  *-assoc-β‹Šβ€² p q .fst [] = refl
  *-assoc-β‹Šβ€² p q .fst (r β—ƒ x ∷ xs ⟨ P ⟩) =
    p * q β‹Š (r β—ƒ x ∷ xs) β‰‘βŸ¨βŸ©
    p * q * r β—ƒ x ∷ (p * q β‹Š xs) β‰‘βŸ¨ cong (_β—ƒ x ∷ (p * q β‹Š xs)) (*-assoc p q r) ⟩
    p * (q * r) β—ƒ x ∷ (p * q β‹Š xs) β‰‘βŸ¨ cong (p * (q * r) β—ƒ x ∷_) P ⟩
    p * (q * r) β—ƒ x ∷ (p β‹Š (q β‹Š xs)) β‰‘βŸ¨βŸ©
    p β‹Š (q β‹Š (r β—ƒ x ∷ xs)) ∎
  *-assoc-β‹Šβ€² p q .snd = eq-coh

β‹Šβˆ… : (x : 𝑅) β†’ x β‹Š ([] {A = A}) ≑ []
β‹Šβˆ… x = refl
\end{code}