module STLCJ where

open import Data.Unit
open import Data.Nat
open import Data.List
open import Data.Sum
open import Data.Product

data Ty : Set where
  ι   : Ty
  _⇒_ : (σ τ : Ty) → Ty

Cx = List Ty

data Var : Cx → Ty → Set where
  zero : ∀ {  τ γ}              → Var (τ ∷ γ) τ
  suc  : ∀ {σ τ γ}(x : Var γ τ) → Var (σ ∷ γ) τ

data Tm : Cx → Ty → Set where
  var : ∀ {  τ γ}(x : Var γ τ)                  → Tm γ τ
  ƛ   : ∀ {σ τ γ}(t : Tm (σ ∷ γ) τ)             → Tm γ (σ ⇒ τ)
  _·_ : ∀ {σ τ γ}(s : Tm γ (σ ⇒ τ))(t : Tm γ σ) → Tm γ τ

postulate Iota : Set

sem : Ty -> Set
sem ι = Iota
sem (σ ⇒ τ) = sem σ → sem τ

E : Cx -> Set
E [] = ⊤
E (x ∷ xs) = sem x × E xs

getE : ∀ {τ γ}(x : Var γ τ)(ρ : E γ) → sem τ
getE zero (s , _) = s
getE (suc x) (_ , γ) = getE x γ

eval : ∀ {γ τ} -> Tm γ τ -> E γ -> sem τ
eval (var x) γ' = getE x γ'
eval (ƛ t) γ' = λ x -> eval t (x , γ')
eval (s · t) γ' = (eval s γ') (eval t γ')

id : Tm (ι ∷ []) ι
id = ƛ (var zero) · var zero