module Exp6 where

data Nat : Set where
  z : Nat
  s : Nat → Nat

{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN ZERO z #-}
{-# BUILTIN SUC s #-}

_+_ : Nat → Nat → Nat
z   + n = n
s m + n = s (m + n)

data Bool : Set where
  tt : Bool
  ff : Bool

if_then_else_ : {A : Set} → Bool → A → A → A
if tt then x else _ = x
if ff then _ else y = y

data TyCode : Set where
  nat  : TyCode
  bool : TyCode

Val : TyCode → Set
Val nat  = Nat
Val bool = Bool

data Con : Set where
  ε : Con
  _<_ : Con → TyCode → Con

data Var : Con → TyCode → Set where
  vz : {Γ : Con}{σ : TyCode} → Var (Γ < σ) σ
  vs : {Γ : Con}{σ τ : TyCode} → Var Γ τ → Var (Γ < σ) τ

data Exp : Con → TyCode → Set where
  var : ∀{Γ σ} → Var Γ σ → Exp Γ σ
  nval : ∀{Γ} → Nat → Exp Γ nat
  bval : ∀{Γ} → Bool → Exp Γ bool
  add  : ∀{Γ} → Exp Γ nat → Exp Γ nat → Exp Γ nat
  cond : ∀{Γ σ} → Exp Γ bool → Exp Γ σ → Exp Γ σ → Exp Γ σ
  Let : ∀{Γ σ τ} → Exp Γ σ → Exp (Γ < σ) τ → Exp Γ τ

data Env : Con → Set where
  ε : Env ε
  _<_ : ∀{Γ σ} → Env Γ → Val σ → Env (Γ < σ)

lookup : ∀{Γ σ} → Var Γ σ → Env Γ → Val σ
lookup vz     (γ < v) = v
lookup (vs i) (γ < v) = lookup i γ

eval : ∀{Γ σ} → Exp Γ σ → Env Γ → Val σ
eval (var i)         γ = lookup i γ
eval (nval n)        γ = n
eval (bval b)        γ = b
eval (add e1 e2)     γ = eval e1 γ + eval e2 γ
eval (cond e1 e2 e3) γ = if eval e1 γ then eval e2 γ else eval e3 γ
eval (Let e1 e2)     γ = eval e2 (γ < eval e1 γ)