This file implement the following rose tree of rose tree of ℕ:
┌───┐ │ 2 │ │ ↓ │ │ ∅ │ └───┘ ↓ ┌─────┐ │┌───┐│ ││ 5 ││ │└───┘│ │ ↓ │ │ ∅ │ └─────┘
We then evaluate adm on this term against the specifications Rose(β₁) and Rose(Rose(β₁)). The former returns a set of constraints that reduces to no constraint on the map f passed as argument to adm, whereas the second returns a set of constraints that reduces to the sole constraint ⟨f , Rose(g)⟩ for some g.
module rose-deep where
open import map
open import list using (List[_] ; ⊢List ; nil[] ; cons[_,_])
open import rose using (Rose[_] ; ⊢Rose ; rnil[] ; rnode[_,_])
open import nat using (2Nat ; 5Nat)
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 (_,_)
β₁ : mix-var
β₁ = tvar 0
f : mix-var
f = fvar 0
Γβ₁ : type-context {mix-var}
Γβ₁ = ⟦ [| β₁ |] ⟧
⊢List[β₁] : Γβ₁ ∥ ∅ ⊢ List[ varᵀ β₁ ]
⊢List[β₁] = ⊢List (var-intro ∋-last)
⊢Rose[β₁] : Γβ₁ ∥ ∅ ⊢ Rose[ varᵀ β₁ ]
⊢Rose[β₁] = ⊢Rose (var-intro ∋-last)
⊢RoseRose[β₁] : Γβ₁ ∥ ∅ ⊢ Rose[ Rose[ varᵀ β₁ ] ]
⊢RoseRose[β₁] = ⊢Rose (⊢Rose (var-intro ∋-last))
t : term-expr
t = rnode[ rnode[ 2Nat , cons[ rnil[] , nil[] ] ] , cons[ rnode[ rnode[ 5Nat , nil[] ] , cons[ rnil[] , nil[] ] ] , nil[] ] ]
C,s = adm t ⊢Rose[β₁] [| varᵀ f |] (record { curr = 1 }) []
C,s-deep = adm t ⊢RoseRose[β₁] [| varᵀ f |] (record { curr = 1 }) []