module ErrorDomains where

𝕍 : Setβ‚‚
𝕍 = Set₁

π•Œ : 𝕍
π•Œ = Set

open import Relation.Binary.PropositionalEquality using (_≑_)
open import Data.Product

record Preorder : 𝕍 where
  field
    X   : π•Œ
    _βŠ‘_ : X β†’ X β†’ π•Œ
    refl : βˆ€ (x : X) β†’ x βŠ‘ x
    trans : βˆ€ {x y z : X} β†’ x βŠ‘ y β†’ y βŠ‘ z β†’ x βŠ‘ z

infixr 20 _⇨_
infixr 20 _β‡’_

record _⇨_ (X : Preorder) (Y : Preorder) : π•Œ where
  module X = Preorder X
  module Y = Preorder Y
  field
    f   : X.X β†’ Y.X
    mon : βˆ€ {x y} β†’ X._βŠ‘_ x y β†’ Y._βŠ‘_ (f x) (f y)

app : βˆ€ {X Y} β†’ (X ⇨ Y) β†’ Preorder.X X β†’ Preorder.X Y
app = _⇨_.f

_$_ = app

_β‡’_ : Preorder β†’ Preorder β†’ Preorder
X β‡’ Y = record { X = X ⇨ Y
               ; _βŠ‘_ = Ξ» f g β†’ (x : X.X) β†’ _⇨_.f f x βŠ‘y _⇨_.f g x
               ; refl = Ξ» x x₁ β†’ _⇨_.mon x (X.refl x₁)
               ; trans = Ξ» p1 p2 x β†’ Y.trans (p1 x) (p2 x) }
  where
    module X = Preorder X
    module Y = Preorder Y
    _βŠ‘y_ = Y._βŠ‘_

_⊨_βŠ‘_ : (X : Preorder) β†’ Preorder.X X β†’ Preorder.X X β†’ Set
X ⊨ x βŠ‘ x' = Preorder._βŠ‘_ X x x'

record _⊨_≣_ (X : Preorder) (x y : Preorder.X X) : Set where
  module X = Preorder X
  _βŠ‘_ = X._βŠ‘_
  field
    to  : x βŠ‘ y
    fro : y βŠ‘ x

record _⇔_ (X : Preorder) (Y : Preorder) : Set where
  field
    to  : X ⇨ Y
    fro : Y ⇨ X
    eqX : βˆ€ x β†’ X ⊨ app fro (app to x) ≣ x
    eqY : βˆ€ y β†’ Y ⊨ app to (app fro y) ≣ y

record _β—ƒ_ (X Y : Preorder) : Set where
  _βŠ‘y_ = Preorder._βŠ‘_ Y
  field
    emb  : X ⇨ Y
    prj  : Y ⇨ X
    projection : βˆ€ y β†’ Y ⊨ app emb (app prj y) βŠ‘ y
    retraction : βˆ€ x β†’ X ⊨ x ≣ app prj (app emb x)

product : Preorder β†’ Preorder β†’ Preorder
product X Y = record { X = X.X Γ— Y.X
                     ; _βŠ‘_ = Ξ» p1 p2 β†’ (proj₁ p1 βŠ‘x proj₁ p2) Γ— (projβ‚‚ p1 βŠ‘y projβ‚‚ p2)
                     ; refl = Ξ» x β†’ (X.refl (proj₁ x)) , (Y.refl (projβ‚‚ x))
                     ; trans = Ξ» leq1 leq2 β†’ (X.trans (proj₁ leq1) (proj₁ leq2)) , Y.trans (projβ‚‚ leq1) (projβ‚‚ leq2)
                     }
  where module X = Preorder X
        _βŠ‘x_ = X._βŠ‘_
        module Y = Preorder Y
        _βŠ‘y_ = Y._βŠ‘_

data TransClosure {X : π•Œ}(_R_ : X β†’ X β†’ π•Œ) : X β†’ X β†’ π•Œ where
  one  : βˆ€ {x y} β†’ x R y β†’ TransClosure _R_ x y
  more : βˆ€ {x y z} β†’ x R y β†’ TransClosure _R_ y z β†’ TransClosure _R_ x z

transClosureAppend : βˆ€ {X}{_R_ : X β†’ _}{x y z} β†’ TransClosure _R_ x y β†’ TransClosure _R_ y z β†’ TransClosure _R_ x z
transClosureAppend (one x) pyz      = more x pyz
transClosureAppend (more x pxy) pyz = more x (transClosureAppend pxy pyz)

record ReflGraph : 𝕍 where
  field
    X : π•Œ
    _βŠ‘_ : X β†’ X β†’ π•Œ
    refl : βˆ€ x β†’ x βŠ‘ x

_^+ : ReflGraph β†’ Preorder
G ^+ = record
  { X = G.X
  ; _βŠ‘_ = TransClosure G._βŠ‘_
  ; refl = Ξ» x β†’ one (G.refl x)
  ; trans = transClosureAppend
  }
  where module G = ReflGraph G

-- Let's get some clocks going
postulate
  K : π•Œ
  β–Έ^  : K β†’ π•Œ β†’ π•Œ
  β–Έ^' : K β†’ 𝕍 β†’ 𝕍
  next^ : βˆ€ {A}{k} β†’ A β†’ β–Έ^ k A
  gfix^ : βˆ€ {k : K}{X : π•Œ} β†’ (β–Έ^ k X β†’ X) β†’ X
  gfix^-unfold : βˆ€ {k}{X} (f : β–Έ^ k X β†’ X) β†’ gfix^ f ≑ f (next^ (gfix^ f))

  next^' : βˆ€ {A}{k} β†’ A β†’ β–Έ^' k A
  gfix^' : βˆ€ {k : K}{X : 𝕍} β†’ (β–Έ^' k X β†’ X) β†’ X
  gfix^'-unfold : βˆ€ {k}{X} (f : β–Έ^' k X β†’ X) β†’ gfix^' f ≑ f (next^' (gfix^' f))