-- An evaluator for well-typed lambda terms.

module LambdaEvaluator where

open import Bool
open import List

infixr 8 _=>_
data Type : Set where
  bool : Type -- a base type
  _=>_ : Type → Type → Type

-- A context is a plain list of types. We don't care about the length.
Context = List Type

-- We can define a pattern synonym to recover the right-to-left notation
-- for contexts.
infixl 1 _,_
pattern _,_ xs x = x :: xs

-- deBruijn indices are more interesting now!
-- Proof reading: A proof of x ∈ xs is simply
-- an index into xs where x can be found.
data _∈_ {A : Set} (x : A) : List A → Set where
  zero : ∀ {xs} → x ∈ (x :: xs)
  succ : ∀ {xs y} → x ∈ xs → x ∈ (y :: xs)

-- Typed lambda terms!
data Term (Γ : Context) : Type → Set where
  var : ∀ {a} → a ∈ Γ → Term Γ a
  lam : ∀ {a b} → Term (Γ , a) b → Term Γ (a => b)
  app : ∀ {a b} → Term Γ (a => b) → Term Γ a → Term Γ b

-- Evaluation ---------

-- We use Agda as the value domain.
Value : Type → Set
Value bool     = Bool
Value (a => b) = Value a → Value b

-- More interesting lists, where each element can have a different type.
-- Proof reading: A proof of All P xs is a list of proofs P x for each
-- element x in xs.
data All {A : Set} (P : A → Set) : List A → Set where
  []   : All P []
  _::_ : ∀ {x xs} → P x → All P xs → All P (x :: xs)

-- If we know All P xs and x ∈ xs, it follows that P x. Also known as
-- looking up the nth element of a list.
lookupAll : ∀ {A} {P : A → Set} {x xs} → All P xs → x ∈ xs → P x
lookupAll (px :: ps) zero     = px
lookupAll (px :: ps) (succ i) = lookupAll ps i

-- An environment is a list of values, one for each element
-- of the context.
Env : Context → Set
Env Γ = All Value Γ

-- Evaluation practically writes itself.
eval : ∀ {Γ a} → Env Γ → Term Γ a → Value a
eval env (var x)   = lookupAll env x
eval env (lam v)   = λ x → eval (x :: env) v
eval env (app u v) = eval env u (eval env v)

-- Examples -------

-- First some convenient notation.
infixl 9 _∙_
pattern _∙_ u v = app u v

pattern var₀ = var zero
pattern var₁ = var (succ zero)
pattern var₂ = var (succ (succ zero))

Γ₁ : Context
Γ₁ = bool :: bool => bool :: bool :: []

v₀ : bool ∈ Γ₁
v₀ = zero

v₁ : (bool => bool) ∈ Γ₁
v₁ = succ zero

v₂ : bool ∈ Γ₁
v₂ = succ (succ zero)

tm₁ : Term Γ₁ (bool => bool)
tm₁ = var₁

tm₂ : Term Γ₁ (bool => bool)
tm₂ = lam (var₂ ∙ var₀)

run₂ : Bool → Bool
run₂ = eval (false :: not :: true :: []) tm₂