{-# OPTIONS --without-K --safe --guardedness --no-sized-types #-}

----------------------------------------------------
-- The free monad construction                    --
-- also called "reflexive and transitive closure" --
----------------------------------------------------

open import prelude


module RTC where

module def {I : Set} (w : IS I) where
  open IS w renaming (Command to A ; Response to D ; next to n)

  data A* : I → Set where
    Leaf : {i : I} → A* i
    _◂_ : {i : I} → (a : A i) → (f : (d : (D i a)) → A* (n a d)) → A* i   -- ◂ is \t

  D* : (i : I) → (t : A* i) → Set
  D* i Leaf = One
  D* i (a ◂ f) = Σ (D i a) (λ d → D* (n a d) (f d))

  n* : {i : I} → (t : A* i) → (b : D* i t) → I
  n* {i} Leaf * = i
  n* (a ◂ f) ( d , ds ) = n* (f d) ds

open def using (Leaf ; _◂_) public

_* : {I : Set} → IS I → IS I
_* {I} w = let open def w in
             record { Command = A* ; Response = D* ; next = n* }