module Rose where

open import Common.Size

data List (A : Set) : {_ : Size} -> Set where
  []   : {size : Size} -> List A {↑ size}
  _::_ : {size : Size} -> A -> List A {size} -> List A {↑ size}

map : {A B : Set} -> (A -> B) ->
      {size : Size} -> List A {size} -> List B {size}
map f [] = []
map f (x :: xs) = f x :: map f xs

data Rose (A : Set) : {_ : Size} -> Set where
  rose : {size : Size} -> A -> List (Rose A {size}) {∞} -> Rose A {↑ size}

{-
mapRose : {A B : Set} -> (A -> B) ->
          {size : Size} -> Rose A {size} -> Rose B {size}
mapRose {A} {B} f .{↑ size} (rose {size} a l) =
   rose (f a) (map (\ r -> mapRose {A} {B} f {size} r) l)
-}

mapRose : {A B : Set} -> (A -> B) ->
          {size : Size} -> Rose A {size} -> Rose B {size}
mapRose f (rose a l) = rose (f a) (map (mapRose f) l)

