```module IDesc.Examples.STLC where

open import Data.Unit
open import Data.Nat
open import Data.Fin
open import Data.Vec hiding (_∈_ ; module _∈_)
open import Data.Product
open import Data.List

open import Relation.Binary.PropositionalEquality

open import IDesc.IDesc
open import IDesc.Fixpoint
open import IDesc.Tagged

-- Paper: Example 3.10

infixr 60 _⇒_
data Ty : Set where
unit : Ty
_⇒_ : (A B : Ty) → Ty

infixl 50 _∙_
data Context : Set where
ε : Context
_∙_ : (Γ : Context)(T : Ty) → Context

infix  40 _∈_
data _∈_ : Ty → Context → Set where
ze : ∀{Γ T} → T ∈ Γ ∙ T
su : ∀{Γ T T'} → T ∈ Γ → T ∈ Γ ∙ T'

STLCD : func (Context × Ty) (Context × Ty)
STLCD = func.mk λ { (Γ , T) →
`Σ (Fin 3) λ
{ zero → `Σ (T ∈ Γ) λ _ → `1
; (suc zero) → `Σ Ty λ S → `var (Γ , S ⇒ T) `× `var (Γ , S)
; (suc (suc zero)) → help Γ T
; (suc (suc (suc ()))) } }
where help : Context → Ty → IDesc (Context × Ty)
help Γ unit = `Σ (Fin 1) λ { zero → `1 ; (suc ()) }
help Γ (S ⇒ T) = `Σ (Fin 1) λ { zero → `var (Γ ∙ S , T) ; (suc ()) }

infix 20 _⊢_
_⊢_ : Context → Ty → Set
Γ ⊢ T = μ STLCD (Γ , T)

var : ∀{Γ T} → T ∈ Γ → Γ ∙ T ⊢ T
var v = ⟨ zero , ze , tt ⟩

app : ∀{Γ S T} → Γ ⊢ S ⇒ T → Γ ⊢ S → Γ ⊢ T
app f s = ⟨ suc zero , _ , f , s ⟩

void : ∀{Γ} → Γ ⊢ unit
void = ⟨ suc (suc zero) , zero , tt ⟩

lam : ∀{Γ S T} → Γ ∙ S ⊢ T → Γ ⊢ S ⇒ T
lam b = ⟨ suc (suc zero) , zero , b ⟩```