StandardSTLC.agda

module STLC where




data Ty : Set where
  Zero One : Ty
  _*_ _=>_ _+_ : Ty → Ty → Ty

data Ctx : Set where
  <> : Ctx
  _,_ : Ctx → Ty → Ctx

data Var : Ctx → Ty → Set where
  here : ∀ {Γ A} → Var (Γ , A) A
  there : ∀ {Γ A B} → Var Γ A → Var (Γ , B) A

data Tm (Γ : Ctx) : Ty → Set where
  var : ∀ {A} → Var Γ A → Tm Γ A
  <> : Tm Γ One
  <_,_> : ∀ {A B} → Tm Γ A → Tm Γ B → Tm Γ (A * B)
  fst : ∀ {A B} → Tm Γ (A * B) → Tm Γ A
  snd : ∀ {A B} → Tm Γ (A * B) → Tm Γ B
  lam : ∀ {A B} → Tm (Γ , A) B → Tm Γ (A => B)
  _$_ : ∀ {A B} → Tm Γ (A => B) → Tm Γ A → Tm Γ B
  abort : ∀ {C} → Tm Γ Zero → Tm Γ C
  left : ∀ {A B} → Tm Γ A → Tm Γ (A + B)
  right : ∀ {A B} → Tm Γ B → Tm Γ (A + B)
  case_of_,_ : ∀ {A B C} → Tm Γ (A + B) → Tm (Γ , A) C → Tm (Γ , B) C → Tm Γ C






data ⊥ : Set where

⊥-elim : ∀ {C : Set} → ⊥ → C
⊥-elim ()

record ⊤ : Set where
  constructor tt

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B

open _×_

data _⊎_ (A B : Set) : Set where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

either : ∀ {A B C : Set} → (A → C) → (B → C) → A ⊎ B → C
either f g (inj₁ x) = f x
either f g (inj₂ y) = g y


⟦_⟧ty : Ty → Set
⟦ Zero ⟧ty = ⊥
⟦ One ⟧ty = ⊤
⟦ A * B ⟧ty = ⟦ A ⟧ty × ⟦ B ⟧ty
⟦ A => B ⟧ty = ⟦ A ⟧ty → ⟦ B ⟧ty
⟦ A + B ⟧ty = ⟦ A ⟧ty ⊎ ⟦ B ⟧ty

⟦_⟧ctx : Ctx → Set
⟦ <> ⟧ctx = ⊤
⟦ Γ , A ⟧ctx = ⟦ Γ ⟧ctx × ⟦ A ⟧ty



lookup : ∀ {Γ A} → Var Γ A → ⟦ Γ ⟧ctx → ⟦ A ⟧ty
lookup here (env , x) = x
lookup (there v) (env , _) = lookup v env

eval : ∀ {Γ A} → Tm Γ A → ⟦ Γ ⟧ctx → ⟦ A ⟧ty
eval (var v) env = lookup v env
eval <> env = tt
eval < M , N > env = eval M env , eval N env
eval (fst P) env = proj₁ (eval P env)
eval (snd P) env = proj₂ (eval P env)
eval (lam M) env = λ z → eval M (env , z)
eval (M $ N) env = eval M env (eval N env)
eval (abort M) env = ⊥-elim (eval M env)
eval (left M) env = inj₁ (eval M env)
eval (right N) env = inj₂ (eval N env)
eval (case D of M , N) env = either (λ x → eval M (env , x)) (λ y → eval N (env , y)) (eval D env)