```{-# OPTIONS --type-in-type --no-positivity-check #-}

open import NeilPrelude
open import Properties
open import Extensionality
open import SubSet

module CPO where

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

infix  3 _≣_ _⊑_ _⊑⊥_
infixr 4 _\$_
infixr 10 _⇒_
infixr 11 _⊕_
infixr 12 _⊗_ _,_

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

-- Sets extended with a bottom element
data _-⊥ (A : Set) : Set where
bot :     A -⊥
val : A → A -⊥

data _⊑⊥_ {A : Set} : Rel (A -⊥) where
⊑⊥-refl   : Reflexive _⊑⊥_
⊑⊥-botval : {a : A} → bot ⊑⊥ val a

⊑⊥-bot : {A : Set} → Initial bot (_⊑⊥_ {A})
⊑⊥-bot {_} {bot}   = ⊑⊥-refl
⊑⊥-bot {_} {val _} = ⊑⊥-botval

⊑⊥-trans : {A : Set} → Transitive {A -⊥} _⊑⊥_
⊑⊥-trans ⊑⊥-refl ⊑⊥-refl = ⊑⊥-refl
⊑⊥-trans ⊑⊥-refl ⊑⊥-botval = ⊑⊥-botval
⊑⊥-trans ⊑⊥-botval ⊑⊥-refl = ⊑⊥-botval

⊑⊥-antisym : {A : Set} → Antisymmetric {A -⊥} _⊑⊥_
⊑⊥-antisym ⊑⊥-refl ⊑⊥-refl = refl
⊑⊥-antisym ⊑⊥-botval ()

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

-- The CPO abstract syntax
-- These are the primary definitions

data Type : Set where
Base : Set         → Type
_⊗_  : Type → Type → Type
_⇒_  : Type → Type → Type
_⊕_  : Type → Type → Type

mutual

data CPO : (τ : Type) → Set where
base : {A : Set} → A -⊥                                  → CPO (Base A)
_,_  : {σ τ : Type} → CPO σ → CPO τ                      → CPO (σ ⊗ τ)
fun  : {σ τ : Type} → (f : CPO σ → CPO τ) → Continuous f → CPO (σ ⇒ τ)
inl  : {σ τ : Type} → CPO σ                              → CPO (σ ⊕ τ)
inr  : {σ τ : Type} → CPO τ                              → CPO (σ ⊕ τ)
bot  : {σ τ : Type}                                      → CPO (σ ⊕ τ)

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

-- Ordering on CPO
-- Note the use of Continuous inside the data type requires a large mutual block where we define continuity

data _⊑_ : {τ : Type} → Rel (CPO τ) where
⊑-base : {A : Set} → {a₁ a₂ : A -⊥} → a₁ ⊑⊥ a₂ → base a₁ ⊑ base a₂
⊑-prod : {σ τ : Type} → {x₁ x₂ : CPO σ} → {y₁ y₂ : CPO τ} → x₁ ⊑ x₂ → y₁ ⊑ y₂ → (x₁ , y₁) ⊑ (x₂ , y₂)
⊑-fun  : {σ τ : Type} → {f g : CPO σ → CPO τ} → {cf : Continuous f} → {cg : Continuous g} → ({x : CPO σ} → f x ⊑ g x) → fun f cf ⊑ fun g cg
⊑-inl  : {σ τ : Type} → {x₁ x₂ : CPO σ} → x₁ ⊑ x₂ → inl {σ} {τ} x₁ ⊑ inl x₂
⊑-inr  : {σ τ : Type} → {y₁ y₂ : CPO τ} → y₁ ⊑ y₂ → inr {σ} {τ} y₁ ⊑ inr y₂
⊑-sum  : {σ τ : Type} → {xy : CPO (σ ⊕ τ)} → bot ⊑ xy

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

Monotonic : {σ τ : Type} → (CPO σ → CPO τ) → Set
Monotonic {σ} f = {x y : CPO σ} → x ⊑ y → f x ⊑ f y

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

-- A Chain is a subset and a limit
Chain : Type → Set
Chain τ = SubSet (CPO τ) × CPO τ

_∈_ : {τ : Type} → CPO τ → Chain τ → Set
x ∈ (P , _) = P x

⨆ : {τ : Type} → Chain τ → CPO τ
⨆ (_ , ⨆X) = ⨆X

IsTotalOrder : {τ : Type} → Chain τ → Set
IsTotalOrder {τ} X = (x₁ x₂ : CPO τ) → x₁ ∈ X → x₂ ∈ X → (x₁ ⊑ x₂) ⊎ (x₂ ⊑ x₁)

-- upper bound
IsUB : {τ : Type} → Chain τ → Set
IsUB {τ} X = (x : CPO τ) → x ∈ X → x ⊑ ⨆ X

-- less than all upper bounds
IsLUB : {τ : Type} → Chain τ → Set
IsLUB {τ} X = (y : CPO τ) → ((x : CPO τ) → x ∈ X → x ⊑ y) → ⨆ X ⊑ y

IsChain : {τ : Type} → Chain τ → Set
IsChain X = IsTotalOrder X × IsUB X × IsLUB X

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

IsNonEmptyChain : {τ : Type} → Chain τ → Set
IsNonEmptyChain {τ} (P , ⨆X) = IsChain (P , ⨆X) × Σ (CPO τ) P

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

chainImage' : {σ τ : Type} → (CPO σ → CPO τ) → Chain σ → Chain τ
chainImage' f (P , ⨆X) = SubImage f P , f ⨆X

PreservesLUB : {σ τ : Type} → (CPO σ → CPO τ) → Set
PreservesLUB {σ} f = ((X : Chain σ) → IsNonEmptyChain X → IsLUB (chainImage' f X))

Continuous : {σ τ : Type} → (f : CPO σ → CPO τ) → Set
Continuous {σ} f = Monotonic f × PreservesLUB f

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

_\$_ : {σ τ : Type} → CPO (σ ⇒ τ) → CPO σ → CPO τ
fun f _ \$ x = f x

continuous : {σ τ : Type} → (f : CPO (σ ⇒ τ)) → Continuous (_\$_ f)
continuous (fun f cf) = cf

monotonic : {σ τ : Type} → (f : CPO (σ ⇒ τ)) → Monotonic (_\$_ f)
monotonic (fun f (mf , _)) = mf

preservesLUB : {σ τ : Type} → (f : CPO (σ ⇒ τ)) → PreservesLUB (_\$_ f)
preservesLUB (fun f (_ , plubf)) = plubf

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

chainImage : {σ τ : Type} → (f : CPO (σ ⇒ τ)) → Chain σ → Chain τ
chainImage f = chainImage' (_\$_ f)

monotonic⇒ImageTotalOrder : {σ τ : Type} → (f : CPO σ → CPO τ) → Monotonic f → (X : Chain σ) → IsTotalOrder X → IsTotalOrder (chainImage' f X)
monotonic⇒ImageTotalOrder f monf (P , ⨆X) tot ._ ._ (x₁ , Px₁ , refl) (x₂ , Px₂ , refl) with tot x₁ x₂ Px₁ Px₂
... | inl lt = inl (monf lt)
... | inr gt = inr (monf gt)

monotonic⇒ImageUB : {σ τ : Type} → (f : CPO σ → CPO τ) → Monotonic f → (X : Chain σ) → IsUB X → IsUB (chainImage' f X)
monotonic⇒ImageUB f monf (P , ⨆X) ub ._ (x , Px , refl) = monf (ub x Px)

imageIsTotalOrder : {σ τ : Type} → (f : CPO (σ ⇒ τ)) → (X : Chain σ) → IsTotalOrder X → IsTotalOrder (chainImage f X)
imageIsTotalOrder (fun f (monf , _)) = monotonic⇒ImageTotalOrder f monf

imageIsUB : {σ τ : Type} → (f : CPO (σ ⇒ τ)) → (X : Chain σ) → IsUB X → IsUB (chainImage f X)
imageIsUB (fun f (monf , _)) = monotonic⇒ImageUB f monf

imageIsNonEmptyChain : {σ τ : Type} → (f : CPO (σ ⇒ τ)) → (X : Chain σ) → IsNonEmptyChain X → IsNonEmptyChain (chainImage f X)
imageIsNonEmptyChain (fun f conf) X ((tot , ub , lub) , x , Px) = (imageIsTotalOrder (fun f conf) X tot , imageIsUB (fun f conf) X ub , preservesLUB (fun f conf) X ((tot , ub , lub) , x , Px)) , (f x , (x , (Px , refl)))

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

-- Uniqueness of proofs is useful as it allows the CPO data type contains Continuity proofs.
-- Without it, we wouldn't be able to prove two CPO elements equal.

-- Uniqueness of ⊑⊥ proofs
ultp' : {A : Set} → {a₁ a₂ : A -⊥} → (p q : a₁ ⊑⊥ a₂) → p ≡ q
ultp' ⊑⊥-refl ⊑⊥-refl     = refl
ultp' ⊑⊥-botval ⊑⊥-botval = refl

-- Uniqueness of ⊑ proofs
ultp : {{_ : Extensionality}} → {τ : Type} → {x y : CPO τ} → (p q : x ⊑ y) → p ≡ q
ultp (⊑-base p) (⊑-base q) = cong ⊑-base (ultp' p q)
ultp (⊑-prod p₁ q₁) (⊑-prod p₂ q₂) = cong2 ⊑-prod (ultp p₁ p₂) (ultp q₁ q₂)
ultp (⊑-fun p) (⊑-fun q) = cong ⊑-fun (ext-implicit (ultp p q))
ultp (⊑-inl p) (⊑-inl q) = cong ⊑-inl (ultp p q)
ultp (⊑-inr p) (⊑-inr q) = cong ⊑-inr (ultp p q)
ultp ⊑-sum ⊑-sum = refl

-- Uniqueness of monotonicity proofs
ump : {{_ : Extensionality}} → {σ τ : Type} → (f : CPO σ → CPO τ) → (p q : Monotonic f) → _≡_ {_} {Monotonic f} p q
ump {σ} f p q = ext-implicit (ext-implicit (ext (λ lt → ultp (p lt) (q lt))))

-- Uniqueness of preservation of least upper bound proofs
ulubp : {{_ : Extensionality}} → {σ τ : Type} → (f : CPO σ → CPO τ) → (p q : PreservesLUB f) → _≡_ {_} {PreservesLUB f} p q
ulubp f p q = ext (λ X → ext (λ pX → ext (λ y → ext (λ ubY → ultp (p X pX y ubY) (q X pX y ubY)))))

-- Uniqueness of continuity proofs
ucp : {{_ : Extensionality}} → {σ τ : Type} → (f : CPO σ → CPO τ) → (p q : Continuous f) → _≡_ {_} {Continuous f} p q
ucp {σ} f (monp , conp) (monq , conq) = ×-cong (ump f monp monq) (ulubp f conp conq)

--                                   this collapses to: {f g : CPO (σ ⇒ τ)} → f ≡ g → fun f cf ≡ fun g cg
injective-\$ : {{_ : Extensionality}} → {σ τ : Type} → Injective {CPO (σ ⇒ τ)} _\$_
injective-\$ {_} {_} {fun f cf} {fun .f cg} refl rewrite ucp f cf cg = refl

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

⊑-refl : {τ : Type} → Reflexive (_⊑_ {τ})
⊑-refl {Base _} {base _} = ⊑-base ⊑⊥-refl
⊑-refl {σ ⊗ τ} {_ , _}   = ⊑-prod ⊑-refl ⊑-refl
⊑-refl {σ ⇒ τ} {fun _ _} = ⊑-fun ⊑-refl
⊑-refl {σ ⊕ τ} {inl _}   = ⊑-inl ⊑-refl
⊑-refl {σ ⊕ τ} {inr _}   = ⊑-inr ⊑-refl
⊑-refl {σ ⊕ τ} {bot}     = ⊑-sum

⊑-eq : {τ : Type} → {x y : CPO τ} → x ≡ y → x ⊑ y
⊑-eq refl = ⊑-refl

⊑-trans : {τ : Type} → Transitive {CPO τ} _⊑_
⊑-trans (⊑-base {_} {bot} _) (⊑-base _) = ⊑-base ⊑⊥-bot
⊑-trans (⊑-base {_} {val _} ⊑⊥-refl) q = q
⊑-trans (⊑-prod a₁ a₂) (⊑-prod b₁ b₂) = ⊑-prod (⊑-trans a₁ b₁) (⊑-trans a₂ b₂)
⊑-trans (⊑-fun p) (⊑-fun q) = ⊑-fun (⊑-trans p q)
⊑-trans (⊑-inl p) (⊑-inl q) = ⊑-inl (⊑-trans p q)
⊑-trans (⊑-inr p) (⊑-inr q) = ⊑-inr (⊑-trans p q)
⊑-trans ⊑-sum _ = ⊑-sum

⊑-split : {σ τ : Type} → {x₁ x₂ : CPO σ} → {y₁ y₂ : CPO τ} → (x₁ , y₁) ⊑ (x₂ , y₂) → x₁ ⊑ x₂ × y₁ ⊑ y₂
⊑-split (⊑-prod lt₁ lt₂) = lt₁ , lt₂

⊑-antisym : {{_ : Extensionality}} → {τ : Type} → Antisymmetric {CPO τ} _⊑_
⊑-antisym (⊑-base p) (⊑-base q) = cong base (⊑⊥-antisym p q)
⊑-antisym (⊑-prod a₁ b₁) (⊑-prod a₂ b₂) = cong2 _,_ (⊑-antisym a₁ a₂) (⊑-antisym b₁ b₂)
⊑-antisym (⊑-fun p) (⊑-fun q) = injective-\$ (ext' (⊑-antisym p q))
⊑-antisym (⊑-inl p) (⊑-inl q) = cong inl (⊑-antisym p q)
⊑-antisym (⊑-inr p) (⊑-inr q) = cong inr (⊑-antisym p q)
⊑-antisym ⊑-sum ⊑-sum = refl

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

mutual

⊥ : {τ : Type} → CPO τ
⊥ {Base _} = base bot
⊥ {_ ⊗ _}  = ⊥ , ⊥
⊥ {_ ⇒ _}  = fun (λ _ → ⊥) continuous-⊥-fun
⊥ {_ ⊕ _}  = bot

⊑-bot : {τ : Type} → Initial (⊥ {τ}) _⊑_
⊑-bot {Base _} {base _}   = ⊑-base ⊑⊥-bot
⊑-bot {_ ⊗ _}  {_ , _}    = ⊑-prod ⊑-bot ⊑-bot
⊑-bot {σ ⇒ τ}  {fun f cf} = ⊑-fun {σ} {τ} {(λ _ → ⊥)} {f} ⊑-bot
⊑-bot {_ ⊕ _}  { _ }      = ⊑-sum

abstract

monotonic-⊥-fun : {σ τ : Type} → Monotonic {σ} {τ} (λ _ → ⊥)
monotonic-⊥-fun _ = ⊑-refl

continuous-⊥-fun : {σ τ : Type} → Continuous {σ} {τ} (λ _ → ⊥)
continuous-⊥-fun {σ} {τ} = monotonic-⊥-fun , (λ _ _ _ _ → ⊑-bot)

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

emptyChain : {τ : Type} → Chain τ
emptyChain = (λ _ → False) , ⊥

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

splitChain : {σ τ : Type} → Chain (σ ⊗ τ) → Chain σ × Chain τ
splitChain {σ} {τ} (P , ⨆X , ⨆Y) = ((λ x → Σ[ y ∶ CPO τ ] P (x , y)) , ⨆X) ,
((λ y → Σ[ x ∶ CPO σ ] P (x , y)) , ⨆Y)

fstChain : {σ τ : Type} → Chain (σ ⊗ τ) → Chain σ
fstChain = fst ∘ splitChain

sndChain : {σ τ : Type} → Chain (σ ⊗ τ) → Chain τ
sndChain = snd ∘ splitChain

uncurry-prop : {σ τ : Type} → {P : CPO (σ ⊗ τ) → Set} → ((x : CPO σ) → (y : CPO τ) → P (x , y)) → (xy : CPO (σ ⊗ τ)) → P xy
uncurry-prop f (x , y) = f x y

firstChain : {σ τ : Type} → CPO σ → Chain τ → Chain (σ ⊗ τ)
firstChain x (P , ⨆Y) = uncurry-prop (λ x' y → x ≡ x' × P y) , (x , ⨆Y)

secondChain : {σ τ : Type} → CPO τ → Chain σ → Chain (σ ⊗ τ)
secondChain y (P , ⨆X) = uncurry-prop (λ x y' → y ≡ y' × P x) , (⨆X , y)

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

singletonChain : {τ : Type} → CPO τ → Chain τ
singletonChain x = (λ x' → x' ≡ x) , x

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

_≣_ : {τ : Type} → Chain τ → Chain τ → Set
(P , ⨆X) ≣ (Q , ⨆Y) = SubSetEq P Q × (⨆X ≡ ⨆Y)

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

ChainComplete : {τ : Type} → (CPO τ → Set) → Set
ChainComplete {τ} P = (X : Chain τ) → IsNonEmptyChain X → ((x : CPO τ) → x ∈ X → P x) → P (⨆ X)

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

Strict : {σ τ : Type} → (g : CPO (σ ⇒ τ)) → Set
Strict g = g \$ ⊥ ≡ ⊥

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

FixedPoint : {τ : Type} → (f : CPO (τ ⇒ τ)) → CPO τ → Set
FixedPoint f x = f \$ x ≡ x

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

Functor : Set
Functor = Type → Type

------------------------------------------------------------------------
```