------------------------------------------------------------------------ -- The syntax of the untyped λ-calculus with constants ------------------------------------------------------------------------ module Lambda.Syntax where open import Data.Nat open import Data.Fin open import Data.Vec open import Relation.Nullary.Decidable ------------------------------------------------------------------------ -- Terms -- Variables are represented using de Bruijn indices. infixl 9 _·_ data Tm (n : ℕ) : Set where con : (i : ℕ) → Tm n var : (x : Fin n) → Tm n ƛ : (t : Tm (suc n)) → Tm n _·_ : (t₁ t₂ : Tm n) → Tm n -- Convenient helper. vr : ∀ m {n} {m<n : True (suc m ≤? n)} → Tm n vr _ {m<n = m<n} = var (#_ _ {m<n = m<n}) ------------------------------------------------------------------------ -- Values, potentially with free variables module WHNF where data Value (n : ℕ) : Set where con : (i : ℕ) → Value n ƛ : (t : Tm (suc n)) → Value n ⌜_⌝ : ∀ {n} → Value n → Tm n ⌜ con i ⌝ = con i ⌜ ƛ t ⌝ = ƛ t ------------------------------------------------------------------------ -- Closure-based definition of values -- Environments and values. Defined in a module parametrised on the -- type of terms. module Closure (Tm : ℕ → Set) where mutual -- Environments. Env : ℕ → Set Env n = Vec Value n -- Values. Lambdas are represented using closures, so values do -- not contain any free variables. data Value : Set where con : (i : ℕ) → Value ƛ : ∀ {n} (t : Tm (suc n)) (ρ : Env n) → Value