Perfect trees

Here we define the data type of perfect trees to be used in other examples.

module ptree 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 introduce the type variables and contexts we will use later on.

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

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

We then define the data type of perfect trees, with the usual constructors pleaf and pnode.

Ptree-id : id-TC-var
Ptree-id = 10

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

pleaf-id pnode-id : id-data-constructor
pleaf-id = 101
pnode-id = 102

pleaf pnode : data-constructor 1
pleaf = pleaf-id ∷ [ varᵀ α ] ⇒ᵀ  [| varᵀ α |]
pnode = pnode-id ∷ [ appᵀ Ptree-name [ [| varᵀ β ×ᵀ varᵀ β |] ] ] ⇒ᵀ  [| varᵀ β |]

Ptree : user-defined 1
Ptree = dataᵀ Ptree-name whereᵀ (pleaf ∷ pnode ∷ [])

Ptree[_] = λ x → data-typeᵀ Ptree [ [| x |] ]
pleaf[_] = λ x → dc pleaf [| x |]
pnode[_] = λ x → dc pnode [| x |]

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

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

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

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