Bushes

We define the data type of bushes to be used in other examples.

module bush where

open import map
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 define the type variables and contexts we will use later on.

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

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

We define the data type of bushes, with the usual constructors bnil and bcons.

Bush-id : id-TC-var
Bush-id = 

Bush-name : TC-var 
Bush-name = TC Bush-id 

bnil-id bcons-id : id-data-constructor
bnil-id = 
bcons-id = 

bnil bcons : data-constructor 
bnil = bnil-id ∷ [] ⇒ᵀ [| varᵀ α |]
bcons =
  bcons-id
  ∷ (varᵀ β ∷ appᵀ Bush-name [ [| appᵀ Bush-name [ [| varᵀ β |] ] |] ] ∷ [])
  ⇒ᵀ [| varᵀ β |]
  
Bush : user-defined   
Bush = dataᵀ Bush-name whereᵀ (bnil ∷ bcons ∷ [])

Bush[_] = λ x → data-typeᵀ Bush [ [| x |] ]
bnil[] = dc bnil [||]
bcons[_,_] = λ x y → dc bcons (x ¦ y ¦ [||])

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

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

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

⊢Bush : ∀ {Γ χ x} _ → Γ ∥ χ ⊢ Bush[ x ] 
⊢Bush ⊢x = data-intro {Γcs = Γα ∷ Γβ ∷ []} {χcs = ∅ ∷ ∅ ∷ []} (⊢bnil , ⊢bcons , ∗) (⊢x , ∗)