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 γ)