module Data.Star where
open import Relation.Binary
open import Data.Function
infixr 5 _◅_
data Star {I : Set} (T : Rel I) : Rel I where
ε : Reflexive (Star T)
_◅_ : ∀ {i j k} (x : T i j) (xs : Star T j k) → Star T i k
infixr 5 _◅◅_
_◅◅_ : ∀ {I} {T : Rel I} → Transitive (Star T)
ε ◅◅ ys = ys
(x ◅ xs) ◅◅ ys = x ◅ (xs ◅◅ ys)
infixl 5 _▻_
_▻_ : ∀ {I} {T : Rel I} {i j k} →
Star T j k → T i j → Star T i k
_▻_ = flip _◅_
infixr 5 _▻▻_
_▻▻_ : ∀ {I} {T : Rel I} {i j k} →
Star T j k → Star T i j → Star T i k
_▻▻_ = flip _◅◅_
gmap : ∀ {I} {T : Rel I} {J} {U : Rel J} →
(f : I → J) → T =[ f ]⇒ U → Star T =[ f ]⇒ Star U
gmap f g ε = ε
gmap f g (x ◅ xs) = g x ◅ gmap f g xs
map : ∀ {I} {T U : Rel I} → T ⇒ U → Star T ⇒ Star U
map = gmap id
TransFlip : ∀ {a} → Rel a → Rel a → Rel a → Set
TransFlip P Q R = ∀ {i j k} → Q j k → P i j → R i k
gfold : ∀ {I J T} (f : I → J) P →
Trans T (P on₁ f) (P on₁ f) →
TransFlip (Star T) (P on₁ f) (P on₁ f)
gfold f P _⊕_ ∅ ε = ∅
gfold f P _⊕_ ∅ (x ◅ xs) = x ⊕ gfold f P _⊕_ ∅ xs
fold : ∀ {I T} (P : Rel I) →
Trans T P P → Reflexive P → Star T ⇒ P
fold P _⊕_ ∅ = gfold id P _⊕_ ∅
gfoldl : ∀ {I J T} (f : I → J) P →
Trans (P on₁ f) T (P on₁ f) →
Trans (P on₁ f) (Star T) (P on₁ f)
gfoldl f P _⊕_ ∅ ε = ∅
gfoldl f P _⊕_ ∅ (x ◅ xs) = gfoldl f P _⊕_ (∅ ⊕ x) xs
foldl : ∀ {I T} (P : Rel I) →
Trans P T P → Reflexive P → Star T ⇒ P
foldl P _⊕_ ∅ = gfoldl id P _⊕_ ∅
concat : ∀ {I} {T : Rel I} → Star (Star T) ⇒ Star T
concat {T = T} = fold (Star T) _◅◅_ ε
revApp : ∀ {I} {T U : Rel I} → Sym T U →
∀ {i j k} → Star T j i → Star U j k → Star U i k
revApp rev ε ys = ys
revApp rev (x ◅ xs) ys = revApp rev xs (rev x ◅ ys)
reverse : ∀ {I} {T U : Rel I} → Sym T U → Sym (Star T) (Star U)
reverse rev xs = revApp rev xs ε
return : ∀ {I} {T : Rel I} → T ⇒ Star T
return x = x ◅ ε
kleisliStar : ∀ {I J} {T : Rel I} {U : Rel J} (f : I → J) →
T =[ f ]⇒ Star U → Star T =[ f ]⇒ Star U
kleisliStar f g = concat ∘ gmap f g
_⋆ : ∀ {I} {T U : Rel I} →
T ⇒ Star U → Star T ⇒ Star U
_⋆ = kleisliStar id
infixl 1 _>>=_
_>>=_ : ∀ {I} {T U : Rel I} {i j} →
Star T i j → T ⇒ Star U → Star U i j
m >>= f = (f ⋆) m