------------------------------------------------------------------------
-- 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 5 _◅_

-- 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 5 _◅◅_

_◅◅_ :  {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 5 _▻_

_▻_ :  {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 5 _▻▻_

_▻▻_ :  {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 10 _⋆

_⋆ :  {i t u} {I : Set i} {T : Rel I t} {U : Rel I u} 
     T  Star U  Star T  Star U
_⋆ = kleisliStar id

infixl 1 _>>=_

_>>=_ :  {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.