Rose trees

Here we define the data type of rose trees.

module rose where

open import map
open import list using (List[_] ; ⊢List ; nil[] ; cons[_,_])
open import Data.List using (_∷_ ; [] ; [_])
open import Data.Vec renaming ([] to [||] ; _∷_ to _¦_  ; [_] to [|_|])
open import Data.Unit renaming (tt to ∗)
open import Data.Product using (_,_)

We introduce variables and contexts for the declaration of Rose’s data constructors.

α β : mix-var
α = tvar 0
β = tvar 1

Γα Γβ : type-context {mix-var}
Γα = ⟦ [| α |] ⟧
Γβ = ⟦ [| β |] ⟧

We then define rose trees as usual, with a constructor rnil producing an empty rose tree, and a constructor rnode making a rose tree out of a label and a list of children, each of which is itself a rose tree.

Rose-id : id-TC-var
Rose-id = 3

Rose-name : TC-var 1
Rose-name = TC Rose-id 1

rnode-id rnil-id : id-data-constructor
rnil-id = 30
rnode-id = 31

rnode rnil : data-constructor 1
rnil = rnil-id ∷ [] ⇒ᵀ [| varᵀ α |]
rnode = rnode-id ∷ ((varᵀ β) ∷ (List[ appᵀ Rose-name [ [| varᵀ β |] ] ]) ∷ []) ⇒ᵀ [| varᵀ β |]

Rose : user-defined {mix-var} 1
Rose = dataᵀ Rose-name whereᵀ (rnil ∷ rnode ∷ [])

Rose[_] = λ x → data-typeᵀ Rose [ [| x |] ]
rnil[] = dc rnil [||]
rnode[_,_] = λ x y → dc rnode (x ¦ y ¦ [||])

Finally, we justify the application of Rose to a type expression.

⊢rnil : Γα ∥ ∅ ⊢ᶜ rnil
⊢rnil = dcᵀ-intro {G = Rose-name} ∗ (var-intro ∋-last , ∗) 

⊢rnode : Γβ ∥ ∅ ⊢ᶜ rnode
⊢rnode = dcᵀ-intro {G = Rose-name} (var-intro ∋-last , ⊢List (app-intro (var-intro ∋-last , ∗) ∋-last) , ∗) (var-intro ∋-last , ∗) 

⊢Rose : ∀ {Γ χ φ} → _ → Γ ∥ χ ⊢ Rose[ φ ]
⊢Rose ⊢φ =
  data-intro
  {Γcs = Γα ∷ Γβ ∷ []}
  {χcs = ∅ ∷ ∅ ∷ []}
  (⊢rnil , ⊢rnode , ∗)
  (⊢φ , ∗)