------------------------------------------------------------------------
-- 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.