Deep by instantiation

This file illustrate the last sentence of Section 2 in the paper. It uses the following term of type Bush(List(Ptree(ℕ))):

╔                            ╗  
║  ┌                       ┐ ║    
║  │                ∙      │ ║   
║  │              ↙   ↘    │ ║   
║  │   ∙         ∙     ∙   │ ║   
║  │  ↙ ↘   ,   ↙ ↘   ↙ ↘  │ ║   
║  │ 5   2     1   3 2   5 │ ║   
║  └                       ┘ ║  
╚                            ╝

where the square brackets denote lists and the double square brackets denote bushes.

module deep-by-inst where

open import map
open import nat using (1Nat ; 2Nat ; 3Nat ; 5Nat)
open import ptree using (Ptree[_] ; ⊢Ptree ; pleaf[_] ; pnode[_])
open import bush using (Bush[_] ; ⊢Bush ; bnil[] ; bcons[_,_])
open import list using (List[_] ; ⊢List ; nil[] ; cons[_,_])
open import Data.List using ([] ; _∷_ ; [_])
open import Data.Vec renaming ([] to [||] ; _∷_ to _¦_  ; [_] to [|_|] )

We start with the declaration of variables that will be used in the call to adm.

β₁ : mix-var
β₁ = tvar 

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

f : mix-var
f = fvar 

We then define the term given in introduction to this file, and the specification with respect to which we are considering it.

⊢BushListPtree[β₁] : Γβ₁ ∥ ∅ ⊢ Bush[ List[ Ptree[ varᵀ β₁ ] ] ]
⊢BushListPtree[β₁] = ⊢Bush (⊢List (⊢Ptree (var-intro ∋-last)))

t =
  bcons[
    cons[
      pnode[
        pleaf[ (5Nat , 2Nat) ]
      ] ,
      cons[
        pnode[
          pnode[
            pleaf[ ((1Nat , 3Nat) , (2Nat , 5Nat)) ]
          ]
        ] ,
        nil[]
      ]
    ] ,
    bnil[]
  ]
  
C,s = adm t ⊢BushListPtree[β₁] [| varᵀ f |] (record { curr =  }) []