------------------------------------------------------------------------
-- The Agda standard library
--
-- The reflexive transitive closures of McBride, Norell and Jansson
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Relation.Binary.Construct.Closure.ReflexiveTransitive where
 
open import Relation.Binary.Core using (Rel; _=[_]⇒_; _⇒_)
open import Relation.Binary.Definitions
  using (Transitive; Trans; Sym; TransFlip; Reflexive)
open import Function.Base
open import Level using (_⊔_)
 
infixr  _◅_
 
-- Reflexive transitive closure.
 
data Star {i t} {I : Set i} (T : Rel I t) : Rel I (i ⊔ t) where
  ε   : Reflexive (Star T)
  _◅_ : ∀ {i j k} (x : T i j) (xs : Star T j k) → Star T i k
        -- The type of _◅_ is Trans T (Star T) (Star T); The
        -- definition is expanded in order to be able to name
        -- the arguments (x and xs).
 
-- Append/transitivity.
 
infixr  _◅◅_
 
_◅◅_ : ∀ {i t} {I : Set i} {T : Rel I t} → Transitive (Star T)
ε        ◅◅ ys = ys
(x ◅ xs) ◅◅ ys = x ◅ (xs ◅◅ ys)
 
-- Sometimes you want to view cons-lists as snoc-lists. Then the
-- following "constructor" is handy. Note that this is _not_ snoc for
-- cons-lists, it is just a synonym for cons (with a different
-- argument order).
 
infixl  _▻_
 
_▻_ : ∀ {i t} {I : Set i} {T : Rel I t} {i j k} →
      Star T j k → T i j → Star T i k
_▻_ = flip _◅_
 
-- A corresponding variant of append.
 
infixr  _▻▻_
 
_▻▻_ : ∀ {i t} {I : Set i} {T : Rel I t} {i j k} →
       Star T j k → Star T i j → Star T i k
_▻▻_ = flip _◅◅_
 
-- A generalised variant of map which allows the index type to change.
 
gmap : ∀ {i j t u} {I : Set i} {T : Rel I t} {J : Set j} {U : Rel J u} →
       (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} {I : Set i} {T : Rel I t} {U : Rel I u} →
      T ⇒ U → Star T ⇒ Star U
map = gmap id
 
-- A generalised variant of fold.
 
gfold : ∀ {i j t p} {I : Set i} {J : Set j} {T : Rel I t}
        (f : I → J) (P : Rel 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} {I : Set i} {T : Rel I t} (P : Rel I p) →
       Trans T P P → Reflexive P → Star T ⇒ P
fold P _⊕_ ∅ = gfold id P _⊕_ ∅
 
gfoldl : ∀ {i j t p} {I : Set i} {J : Set j} {T : Rel I t}
         (f : I → J) (P : Rel 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} {I : Set i} {T : Rel I t} (P : Rel I p) →
        Trans P T P → Reflexive P → Star T ⇒ P
foldl P _⊕_ ∅ = gfoldl id P _⊕_ ∅
 
concat : ∀ {i t} {I : Set i} {T : Rel I t} → Star (Star T) ⇒ Star T
concat {T = T} = fold (Star T) _◅◅_ ε
 
-- If the underlying relation is symmetric, then the reflexive
-- transitive closure is also symmetric.
 
revApp : ∀ {i t u} {I : Set i} {T : Rel I t} {U : Rel I u} →
         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} {I : Set i} {T : Rel I t} {U : Rel I u} →
          Sym T U → Sym (Star T) (Star U)
reverse rev xs = revApp rev xs ε
 
-- Reflexive transitive closures form a (generalised) monad.
 
-- return could also be called singleton.
 
return : ∀ {i t} {I : Set i} {T : Rel I t} → T ⇒ Star T
return x = x ◅ ε
 
-- A generalised variant of the Kleisli star (flip bind, or
-- concatMap).
 
kleisliStar : ∀ {i j t u}
                {I : Set i} {J : Set j} {T : Rel I t} {U : Rel J u}
              (f : I → J) → T =[ f ]⇒ Star U → Star T =[ f ]⇒ Star U
kleisliStar f g = concat ∘′ gmap f g
 
infix  _⋆
 
_⋆ : ∀ {i t u} {I : Set i} {T : Rel I t} {U : Rel I u} →
     T ⇒ Star U → Star T ⇒ Star U
_⋆ = kleisliStar id
 
infixl  _>>=_
 
_>>=_ : ∀ {i t u} {I : Set i} {T : Rel I t} {U : Rel I u} {j k} →
        Star T j k → T ⇒ Star U → Star U j k
m >>= f = (f ⋆) m
 
-- Note that the monad-like structure above is not an indexed monad
-- (as defined in Effect.Monad.Indexed). If it were, then _>>=_
-- would have a type similar to
--
--   ∀ {I} {T U : Rel I t} {i j k} →
--   Star T i j → (T i j → Star U j k) → Star U i k.
--                  ^^^^^
-- Note, however, that there is no scope for applying T to any indices
-- in the definition used in Effect.Monad.Indexed.