module Eval2 where

-- Another lambda evaluator, using higher-order abs. syntax
-- to avoid explicit de Bruin index.

open import Data.Nat

data Term : Set → Set1 where
  lit : ℕ → Term ℕ
  var : ∀ {a} → a → Term a
  _·_ : ∀ {a b} → Term (a → b) → Term a → Term b
  add : Term ℕ → Term ℕ → Term ℕ
  ƛ : ∀ {a b} → (a → Term b) → Term (a → b)

eval : ∀ {a} → Term a → a
eval (lit n) = n
eval (var v) = v
eval (e₁ · e₂) = eval e₁ (eval e₂)
eval (add e₁ e₂) = eval e₁ + eval e₂
eval (ƛ e) = λ x → eval (e x)