Deep specification

This file illustrates that deep specification can produce constraints on the mappable morphisms over a given term. Here we use the following term of type Seq(Seq(ℕ × Bool)):

const (pair (const 5) (const true)) 

We will run adm on this term with respect to the specification Seq(Seq(β₁)).

module deep-gadt-spec where

open import map
open import nat using (5Nat)
open import bool using (true[])
open import seq using (Seq[_] ; ⊢Seq ; const[_] ; pair[_,_])
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 of this file, and the specification with respect to which we are considering it.

⊢SeqSeq[β₁] : Γβ₁ ∥ ∅ ⊢ Seq[ Seq[ varᵀ β₁ ] ]
⊢SeqSeq[β₁] = ⊢Seq (⊢Seq (var-intro ∋-last))

t = const[ pair[ const[ 5Nat ] , const[ true[] ] ] ]

C,s = adm t ⊢SeqSeq[β₁] [| varᵀ f |] (record { curr =  }) []