Beta-WHNF NbE for STLC

STLCBetaWHNF.agda

module STLCBetaWHNF where

open import Data.Sum
open import Data.Unit using (⊤ ; tt)
open import Data.Product

--------------------
-- Term syntax, etc.
--------------------

data Ty : Set where
  𝕓  : Ty
  _⇒_   : Ty → Ty → Ty

data Ctx : Set where
  []   : Ctx
  _`,_ : Ctx → Ty → Ctx

variable
  Γ Δ Γ' Δ' : Ctx
  a b       :  Ty

data _≤_  : Ctx → Ctx → Set where
  base   : [] ≤ []
  drop   : Γ ≤ Δ → (Γ `, a) ≤ Δ
  keep   : Γ ≤ Δ → (Γ `, a) ≤ (Δ `, a)

idWk : Γ ≤ Γ
idWk {[]}     = base
idWk {Γ `, x} = keep idWk

_∙_ : {Σ : Ctx} → Δ ≤ Σ → Γ ≤ Δ → Γ ≤ Σ
w       ∙ base     = w
w       ∙ drop w'  = drop (w ∙ w')
drop w  ∙ keep w'  = drop (w ∙ w')
keep w  ∙ keep w'  = keep (w ∙ w')

data Var : Ctx → Ty → Set where
  ze : Var (Γ `, a) a
  su : (v : Var Γ a) → Var (Γ `, b) a

wkVar : Γ' ≤ Γ → Var Γ a → Var Γ' a
wkVar (drop w) ze     = su (wkVar w ze)
wkVar (keep w) ze     = ze
wkVar (drop w) (su v) = su (wkVar w (su v))
wkVar (keep w) (su v) = su (wkVar w v)

data Tm : Ctx → Ty → Set where

  var  : Var Γ a
       ---------
       → Tm Γ a

  lam  : Tm (Γ `, a) b
         -------------
       → Tm Γ (a ⇒ b)

  app  : Tm Γ (a ⇒ b) → Tm Γ a
         ---------------------
       → Tm Γ b

wkTm : Γ' ≤ Γ → Tm Γ a → Tm Γ' a
wkTm w (var x)   = var (wkVar w x)
wkTm w (lam t)   = lam (wkTm (keep w) t)
wkTm w (app t u) = app (wkTm w t) (wkTm w u)

data Sub : Ctx → Ctx → Set where
  []   : Sub Δ []
  _`,_ : Sub Δ Γ → Tm Δ a → Sub Δ (Γ `, a)

wkSub : Γ' ≤ Γ → Sub Γ Δ → Sub Γ' Δ
wkSub w []          = []
wkSub w (s `, t)    = (wkSub w s) `, wkTm w t

substVar : Sub Γ Δ → Var Δ a → Tm Γ a
substVar (s `, t) ze     = t
substVar (s `, t) (su x) = substVar s x

substTm : Sub Δ Γ → Tm Γ a → Tm Δ a
substTm s (var x)     = substVar s x
substTm s (lam t)     = lam (substTm (wkSub (drop idWk) s `, var ze) t)
substTm s (app t u)   = app (substTm s t) (substTm s u)

---------------
-- Normal forms
---------------

data Ne : Ctx → Ty → Set
data Nf : Ctx → Ty → Set

data Ne where
  var   : Var Γ a → Ne Γ a
  app   : Ne Γ (a ⇒ b) → Nf Γ a → Ne Γ b

-- β-WHNFs (i.e., no η for _⇒_ and no congruence for lam)
data Nf where
  up  : Ne Γ a → Nf Γ a
  lam : Tm (Γ `, a) b → Nf Γ (a ⇒ b)

wkNe : Γ' ≤ Γ → Ne Γ a → Ne Γ' a
wkNf : Γ' ≤ Γ → Nf Γ a → Nf Γ' a

wkNe w (var x)   = var (wkVar w x)
wkNe w (app m n) = app (wkNe w m) (wkNf w n)

wkNf w (up x)  = up (wkNe w x)
wkNf w (lam n) = lam (wkTm (keep w) n)

embNe : Ne Γ a → Tm Γ a
embNf : Nf Γ a → Tm Γ a

embNe (var x)   = var x
embNe (app m n) = app (embNe m) (embNf n)

embNf (up x)    = embNe x
embNf (lam t)   = lam t

------------------------------
-- Normalisation by Evaluation
------------------------------

-- interpretation of types (⟦_⟧)
Tm' : Ctx → Ty → Set
Tm' Γ 𝕓       = Nf Γ 𝕓
Tm' Γ (a ⇒ b) = (Tm' Γ a → Tm' Γ b) × Nf Γ (a ⇒ b)

-- note: `Γ' ≤ Γ → Tm' Γ a → Tm' Γ' a` is not admissible, fails for _⇒_ type

-- semantics supports reification
reify : Tm' Γ a → Nf Γ a
reify {a = 𝕓}      n = n
reify {a = a ⇒ b}  x = proj₂ x

-- semantic domain supports reflection
reflect : Ne Γ a → Tm' Γ a
reflect {a = 𝕓}      n = up n
reflect {a = a ⇒ b}  n = (λ x → reflect (app n (reify x))) , up n

-- retraction of eval
quot : Tm' Γ a → Tm Γ a
quot x = embNf (reify x)

-- interpretation of contexts
Sub' : Ctx → Ctx → Set
Sub' Δ []       = ⊤
Sub' Δ (Γ `, a) = Sub' Δ Γ × Tm' Δ a

-- interpretation of variables
substVar' : Var Γ a → ({Δ : Ctx} → Sub' Δ Γ → Tm' Δ a)
substVar' ze     (_ , x) = x
substVar' (su x) (γ , _) = substVar' x γ

-- retraction of evalₛ
quotₛ : Sub' Δ Γ → Sub Δ Γ
quotₛ {Γ = []}     tt         = []
quotₛ {Γ = Γ `, _} (s , x)    = (quotₛ s) `, quot x

-- interpretation of terms
eval : Tm Γ a → ({Δ : Ctx} → Sub' Δ Γ → Tm' Δ a)
eval (var x)           s  = substVar' x s
eval (lam t)           s  = (λ x → eval t (s , x))
  , (lam (substTm (wkSub (drop idWk) (quotₛ s) `, (var ze)) t))
eval (app t u)         s  = proj₁ (eval t s) (eval u s)

-- variable substitution
data VSub : Ctx → Ctx → Set where
  []   : VSub Γ []
  _`,_ : VSub Γ Δ → Var Γ a → VSub Γ (Δ `, a)

-- weaken variable substitutions
wkVSub : Γ' ≤ Γ → VSub Γ Δ → VSub Γ' Δ
wkVSub w []        = []
wkVSub w (ns `, x) = wkVSub w ns `, wkVar w x

-- identity variable substitution
idVSub : VSub Γ Γ
idVSub {[]}     = []
idVSub {Γ `, x} = wkVSub (drop idWk) idVSub `, ze

-- reflect a variable substitution
reflectVSub : VSub Γ Δ → Sub' Γ Δ
reflectVSub []        = tt
reflectVSub (ns `, n) = reflectVSub ns , reflect (var n)

-- identity semantic substitution
idₛ' : Sub' Γ Γ
idₛ' = reflectVSub idVSub

-- normalisation function
norm : Tm Γ a → Nf Γ a
norm t = reify (eval t idₛ')