nachivpn · June 18, 2021 13:37
diff --git a/STLCBetaWHNF.agda b/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ₛ')
	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ₛ')