open import Cubical.Foundations.Prelude

module SignatureAlgebra.Examples.PowerDomain (ℓi : Level) where

open import Cubical.Foundations.Function
open import Cubical.Foundations.Structure

open import Cubical.Data.Bool as Bool
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Sigma
open import Cubical.Data.Unit

open import DCPO ℓi
open import DCPO.Constructions.BinaryProduct ℓi
open import DCPO.Constructions.Lift ℓi
open import DCPO.Constructions.Product ℓi
open import DCPO.Constructions.Unit ℓi

open import SignatureAlgebra.Initial ℓi
open import SignatureAlgebra.Monomial ℓi
open import SignatureAlgebra.Signature ℓi
open import SignatureAlgebra.SignatureAlgebra ℓi

private
  variable
    ℓx ℓd ℓt : Level

data Tri : Type where
  tri1 : Tri
  tri2 : Tri
  tri3 : Tri

triElim : ∀ {ℓ} {X : Type ℓ} → (x1 x2 x3 : X) → Tri → X
triElim x1 x2 x3 tri1 = x1
triElim x1 x2 x3 tri2 = x2
triElim x1 x2 x3 tri3 = x3

data InequalityNames : Type where
  unionComm : InequalityNames
  unionAssoc : InequalityNames
  unionIdemp1 : InequalityNames
  unionIdemp2 : InequalityNames

∪ₘ : Monomial ℓ-zero ℓ-zero ℓ-zero
∪ₘ = monomial Bool unitDCPO

powerPreΣ : PreSignature ℓ-zero ℓ-zero ℓ-zero ℓ-zero
powerPreΣ = presignature Unit (λ _ → ∪ₘ)

_∪ₜ_ : {V : Type} (t₁ t₂ : Term powerPreΣ V) → Term powerPreΣ V
t₁ ∪ₜ t₂ = constr tt (if_then t₂ else t₁) tt*

unionInequalities : InequalityNames → Inequality powerPreΣ ℓ-zero
unionInequalities unionComm =
  inequality Bool
    (var false ∪ₜ var true)
    (var true  ∪ₜ var false)
unionInequalities unionAssoc =
  inequality Tri
    ((var tri1 ∪ₜ var tri2) ∪ₜ var tri3)
    (var tri1 ∪ₜ (var tri2 ∪ₜ var tri3))
unionInequalities unionIdemp1 =
  inequality Unit
    (var tt ∪ₜ var tt)
    (var tt)
unionInequalities unionIdemp2 =
  inequality Unit
    (var tt)
    (var tt ∪ₜ var tt)

powerΣ : Signature ℓ-zero ℓ-zero ℓ-zero ℓ-zero ℓ-zero ℓ-zero
powerΣ = signature powerPreΣ InequalityNames unionInequalities

PowerAlgebra : (ℓ ℓ' : Level) → Type (ℓ-max (ℓ-max (ℓ-suc ℓi) (ℓ-suc ℓ)) (ℓ-suc ℓ'))
PowerAlgebra = SignatureAlgebra powerΣ

poweralgebra : (D : DCPO ℓd ℓt)
              → (_∪_ : ⟨ D ⟩ → ⟨ D ⟩ → ⟨ D ⟩)
              → isContinuous (D ×ᵈᶜᵖᵒ D) D (uncurry _∪_)
              → ((x y : ⟨ D ⟩) → x ∪ y ⊑⟨ D ⟩ y ∪ x)
              → ((x y z : ⟨ D ⟩) → (x ∪ y) ∪ z ⊑⟨ D ⟩ x ∪ (y ∪ z))
              → ((x : ⟨ D ⟩) → x ∪ x ≡ x)
              → PowerAlgebra ℓd ℓt
poweralgebra D _∪_ ∪Cont ∪Comm ∪Assoc ∪Idemp =
  signaturealgebra
    (presignaturealgebra D
      (λ _ → uncurry _∪_ ∘ pairing (λ x → fst x false) (λ x → fst x true))
      (λ _ →
        isContinuous-∘ (⟦ ∪ₘ ⟧ₘ D) (D ×ᵈᶜᵖᵒ D) D
          (uncurry _∪_) (pairing (λ x → fst x false) (λ x → fst x true))
          ∪Cont
          (pairingIsContinuous (⟦ ∪ₘ ⟧ₘ D) D D
            (λ x → fst x false) (λ x → fst x true)
            (λ I α δ →
              ∐isSup D (pointwiseFamilyIsDirected' Bool (λ _ → D)
                (fstIsDirected' (Πᵈᶜᵖᵒ Bool (λ _ → D)) (unitDCPO {ℓ-zero} {ℓ-zero}) δ) false))
            (λ I α δ →
              ∐isSup D (pointwiseFamilyIsDirected' Bool (λ _ → D)
                (fstIsDirected' (Πᵈᶜᵖᵒ Bool (λ _ → D)) (unitDCPO {ℓ-zero} {ℓ-zero}) δ) true)))))
    λ { unionComm ρ   → ∪Comm (ρ false) (ρ true)
      ; unionAssoc ρ  → ∪Assoc (ρ tri1) (ρ tri2) (ρ tri3)
      ; unionIdemp1 ρ → ≡→⊑ D (∪Idemp (ρ tt))
      ; unionIdemp2 ρ → ≡→⊑ D (sym (∪Idemp (ρ tt)))}

initialPowerAlgebra : PowerAlgebra (ℓ-suc ℓi) (ℓ-suc ℓi)
initialPowerAlgebra = initialSignatureAlgebra powerΣ

module _ (X : PowerAlgebra ℓx ℓt) where
  _∪_ : ⟨ X ⟩ → ⟨ X ⟩ → ⟨ X ⟩
  _∪_ x y = interpretation X tt ((if_then y else x) , tt*)

  ∪IsContinuous : isContinuous
                    ((Πᵈᶜᵖᵒ Bool (λ _ → underlyingDCPO X)) ×ᵈᶜᵖᵒ unitDCPO)
                    (underlyingDCPO X)
                    (interpretation X tt)
  ∪IsContinuous = interpretationIsContinuous X tt

  ∪IsMonotone : isMonotone
                  ((Πᵈᶜᵖᵒ Bool (λ _ → underlyingDCPO X)) ×ᵈᶜᵖᵒ unitDCPO)
                    (underlyingDCPO X)
                    (interpretation X tt)
  ∪IsMonotone =
    isContinuous→isMonotone
      ((Πᵈᶜᵖᵒ Bool (λ _ → underlyingDCPO X)) ×ᵈᶜᵖᵒ unitDCPO)
      (underlyingDCPO X)
      (interpretation X tt)
      ∪IsContinuous

  ⟦∪ₜ⟧-≡ : {V : Type} {t₁ t₂ : Term powerPreΣ V}
         → {ρ : V → ⟨ X ⟩}
         → ⟦ t₁ ∪ₜ t₂ ⟧ₜ (underlyingDCPO X) (interpretation X) ρ
         ≡ (⟦ t₁ ⟧ₜ (underlyingDCPO X) (interpretation X) ρ) ∪
           (⟦ t₂ ⟧ₜ (underlyingDCPO X) (interpretation X) ρ)
  ⟦∪ₜ⟧-≡ = cong (interpretation X tt) (≡-× (funExt (Bool.elim refl refl)) refl)

  ∪Comm⊑ : (x y : ⟨ X ⟩)
         → (x ∪ y) ⊑⟨ underlyingDCPO X ⟩ (y ∪ x)
  ∪Comm⊑ x y = subst2 (order (underlyingDCPO X)) ⟦∪ₜ⟧-≡ ⟦∪ₜ⟧-≡
                (inequalityValidity X unionComm (if_then y else x))

  ∪Comm : (x y : ⟨ X ⟩) → x ∪ y ≡ y ∪ x
  ∪Comm x y = antisymmetry (underlyingDCPO X) _ _ (∪Comm⊑ x y) (∪Comm⊑ y x)

  ∪Assoc⊑ : (x y z : ⟨ X ⟩)
          → ((x ∪ y) ∪ z) ⊑⟨ underlyingDCPO X ⟩ (x ∪ (y ∪ z))
  ∪Assoc⊑ x y z =
    subst2 (λ u v → (u ∪ z) ⊑⟨ underlyingDCPO X ⟩ (x ∪ v)) ⟦∪ₜ⟧-≡ ⟦∪ₜ⟧-≡
      (subst2 (order (underlyingDCPO X)) ⟦∪ₜ⟧-≡ ⟦∪ₜ⟧-≡
        (inequalityValidity X unionAssoc (triElim x y z)))

  ∪Assoc : (x y z : ⟨ X ⟩) → (x ∪ y) ∪ z ≡ x ∪ (y ∪ z)
  ∪Assoc x y z = antisymmetry (underlyingDCPO X) _ _ (∪Assoc⊑ x y z) lem
    where
      open DCPOReasoning

      lem : (x ∪ (y ∪ z)) ⊑⟨ underlyingDCPO X ⟩ ((x ∪ y) ∪ z)
      lem = x ∪ (y ∪ z) ⊑⟨ underlyingDCPO X ⟩[ ∪IsMonotone (Bool.elim (∪Comm⊑ y z) (reflexivity (underlyingDCPO X) x) , lift refl) ]
            x ∪ (z ∪ y) ⊑⟨ underlyingDCPO X ⟩[ ∪Comm⊑ x (z ∪ y) ]
            (z ∪ y) ∪ x ⊑⟨ underlyingDCPO X ⟩[ ∪Assoc⊑ z y x ]
            z ∪ (y ∪ x) ⊑⟨ underlyingDCPO X ⟩[ ∪Comm⊑ z (y ∪ x) ]
            (y ∪ x) ∪ z ⊑⟨ underlyingDCPO X ⟩[ ∪IsMonotone (Bool.elim (reflexivity (underlyingDCPO X) z) (∪Comm⊑ y x) , lift refl) ]
            (x ∪ y) ∪ z ∎⟨ underlyingDCPO X ⟩

  ∪Idemp : (x : ⟨ X ⟩) → x ∪ x ≡ x
  ∪Idemp x =
    antisymmetry (underlyingDCPO X) _ _
      (subst (λ - → - ⊑⟨ underlyingDCPO X ⟩ x) ⟦∪ₜ⟧-≡
        (inequalityValidity X unionIdemp1 (λ _ → x)))
      (subst (λ - → x ⊑⟨ underlyingDCPO X ⟩ -) ⟦∪ₜ⟧-≡
        (inequalityValidity X unionIdemp2 (λ _ → x)))