module Eval where

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

open import Relation.Binary.PropositionalEquality

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)

Env : ℕ → Set1
Env n = Vec (Σ Set (λ a → a)) n

lookup-proj : ∀ {n} (x : Fin n) (ρ : Env n) →
              lookup x (map proj₁ ρ) ≡ proj₁ (lookup x ρ)
lookup-proj zero (_ ∷ _) = refl
lookup-proj (suc i) (_ ∷ xs) = lookup-proj i xs

eval : ∀ {a n} → (ρ : Env n) → Term (map proj₁ ρ) a → a
eval ρ (lit m) = m
eval ρ (var x) rewrite lookup-proj x ρ = proj₂ (lookup x ρ)
eval ρ (e₁ · e₂) = eval ρ e₁ (eval ρ e₂)
eval ρ (add e₁ e₂) = (eval ρ e₁) + (eval ρ e₂)
eval ρ (ƛ e) = λ v → eval ((_ , v) ∷ ρ) e