module Eval3 where

open import Data.Nat
open import Data.Fin hiding (_+_)
open import Data.Vec

Cxt : ℕ → Set1
Cxt n = Vec Set n

data Term {n : ℕ} (Γ : Cxt n) : Set → Set1 where
  lit : ℕ → Term Γ ℕ
  var : (x : Fin n) → Term Γ (lookup x Γ)
  _·_ : ∀ {a b} → Term Γ (a → b) → Term Γ a → Term Γ b
  add : Term Γ ℕ → Term Γ ℕ → Term Γ ℕ 
  ƛ   : ∀ {a b} → Term (a ∷ Γ) b → Term Γ (a → b)

infixr 5 _∷_

data Env : {n : ℕ} → Cxt n → Set1 where
  []  : Env []
  _∷_ : ∀ {a n} {Γ : Cxt n} → a → Env Γ → Env (a ∷ Γ)

envLookup : ∀ {n}{Γ : Cxt n} → (x : Fin n) → Env Γ → lookup x Γ
envLookup zero    (v ∷ ρ) = v 
envLookup (suc n) (v ∷ ρ) = envLookup n ρ 

eval : ∀ {a n} {Γ : Cxt n} → (ρ : Env Γ) → Term Γ a → a
eval ρ (lit m) = m
eval ρ (var x) = envLookup x ρ 
eval ρ (e₁ · e₂) = (eval ρ e₁) (eval ρ e₂) 
eval ρ (add e₁ e₂) = (eval ρ e₁) + (eval ρ e₂)  
eval ρ (ƛ e) = λ v → eval (v ∷ ρ) e