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