{-# OPTIONS --without-K --safe --guardedness --no-sized-types #-}
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
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
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# }
ν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)
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)}