module Exp6a 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 Maybe (A : Set) : Set where Nothing : Maybe A Just : A → Maybe A 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 Γ τ throw : ∀{Γ σ} → Exp Γ σ catch : ∀{Γ σ} → 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 Γ → Maybe (Val σ) eval (var i) γ = Just (lookup i γ) eval (nval n) γ = Just n eval (bval b) γ = Just b eval (add e1 e2) γ with eval e1 γ ... | Nothing = Nothing ... | Just n1 with eval e2 γ ... | Nothing = Nothing ... | Just n2 = Just (n1 + n2) eval (cond e1 e2 e3) γ with eval e1 γ ... | Nothing = Nothing ... | Just b = if b then eval e2 γ else eval e3 γ eval (Let e1 e2) γ with eval e1 γ ... | Nothing = Nothing ... | Just v = eval e2 (γ < v) eval throw γ = Nothing eval (catch e h) γ with eval e γ ... | Nothing = eval h γ ... | Just v = Just v