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

-----------------------------------------
-- Layering, using induction-recursion --
-----------------------------------------

open import prelude


module Layering where

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

  mutual
    data A# : I  Set where
      Leaf : { i : I }  A# i
      _◂_ : {i : I}  (t : A# i)  ((b : D# i t)  A (n# t b))  A# i    -- ◂ is \triangle

    D# : (i : I)  A# i  Set
    D# i Leaf = One
    D# i (t  l) = Σ (D# i t)  ds  D (n# t ds) (l ds))

    n# : {i : I}  (t : A# i)  D# i t  I
    n# {i} Leaf * = i
    n# {i} (t  l) ( ds , d ) = n {n# {i} t ds} (l ds) d
--  The previous line doesn't work when Σ is defined by a "data" as
--  there is no eta expansion with data...
--    n# (t ◂ l) dsd = n (l (fst dsd)) (snd dsd)
-- end of module Layer

open def using (Leaf ; _◂_) public


_# : {I : Set}  IS I  IS I    -- alternative notation : _≙, where ≙ is \and=
_# {I} w =
  let open def w in
  record { Command = A# ; Response = D# ; next = n# }


-- given a balanced (well-founded) tree in "A# i", we can look at its extentions to a full
-- infinite tree in ν w i...
νextend : {I : Set} (w : IS I) (i₀ : I)  Pow (def.A# w i₀)
νextend {I} w i₀ t =
  let open def w in
  (ds : D# i₀ t)  ν w (n# t ds)


-----------------------------------------------------------------------
-- Layered transition system from an initialized interaction system. --
-- The state space is A# i₀.                                         --
-- Intuition : a transition from a state "t : A# i₀" is a new layer  --
-- on top of t.                                                      --
-----------------------------------------------------------------------
LayeredTS : {I : Set}  (w : IS I)  (i₀ : I)  TS (IS.Command (w #) i₀)
LayeredTS w i₀ =
  let open IS w renaming (Command to A ; Response to D ; next to n) in
  let open def w using (D# ; n#) in
    record { Transition = λ t  Π (D# i₀ t)  ds  A (n# t ds)) ;
             next =  {t} l  t  l)}