{-|
This module defines intrinsically well-staged rose trees,
and re-exports the StagedList module with StagedList renamed to StagedForest.
The module is parameterized by a ℕ-indexed type Item that represents the types of items stored in the tree.
-}

{-# OPTIONS --safe #-}
open import Data.Nat using (ℕ)
module Data.StagedTree (Item : ℕ → Set) where

open import Data.StagedList using (StagedList)

{- |
Rose tree data structure built from staged lists.
A StagedTree n contans an item at level n, and a subtree whose items are at level n or higher.

Fields:
  children: A staged list of subtrees, each at stage ≥ n
  item: An item at stage n
-}
infix  _⊢_
record StagedTree (n : ℕ) : Set where
  inductive
  constructor _⊢_
  field
    children : StagedList StagedTree n
    item : Item n

-- | A StagedForest n is a list of StagedTrees at level ≥ n.
open import Data.StagedList StagedTree renaming (StagedList to StagedForest) public