Normalizer for lambda calculus

newtry6.agda

module newtry6 where
-- derived from https://gist.github.com/rntz/2543cf9ef5ee4e3d990ce3485a0186e2
--              http://eprints.nottingham.ac.uk/41385/1/th.pdf

open import Level
open import Function using (id; _∘_)

infixr 5 _⇒_

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

data Con : Set where
  ∙ : Con
  _,_ : Con → Ty → Con

data Tm : Con → Ty → Set

data Tms : Con → Con → Set where
  _∘t_ : ∀{X Y Z} → Tms Y Z → Tms X Y → Tms X Z
  Id : ∀{X} → Tms X X
  ε : ∀{X} → Tms X ∙
  _,_ : ∀{X Y A} → (p : Tms X Y) → Tm X A → Tms X (Y , A)
  π₁ : ∀{X Y A} → Tms X (Y , A) → Tms X Y

data Tm where
  _[_] : ∀{X Y A} → Tm X A → (p : Tms Y X) → Tm Y A
  π₂ : ∀{X Y A} → (p : Tms X (Y , A)) → Tm X A
  lam : ∀{X A B} → Tm (X , A) B → Tm X (A ⇒ B)
  app : ∀{X A B} → Tm X (A ⇒ B) → Tm (X , A) B

wk : ∀{X A} → Tms (X , A) X
wk = π₁ Id

vz : ∀{X A} → Tm (X , A) A
vz = π₂ Id

vs : ∀{X A B} → Tm X A → Tm (X , B) A
vs x = x [ wk ]

<_> : ∀{Γ}{A : Ty} → Tm Γ A → Tms Γ (Γ , A)
< t > = Id , t

infixl 4 _$_

_$_ : ∀ {Γ}{A : Ty}{B : Ty}(t : Tm Γ (A ⇒ B))(u : Tm Γ A) → Tm Γ B
t $ u = (app t) [ < u > ]

[_⊢_] : Con → Ty → Set₁
[ X ⊢ base ] = Lift (suc zero) (Tm X base)
[ X ⊢ a ⇒ b ] = ∀ {Y} (s : Tms Y X) → [ Y ⊢ a ] → [ Y ⊢ b ]

reify : ∀{a X} → [ X ⊢ a ] → Tm X a
reflect : ∀{a X} → Tm X a → [ X ⊢ a ]

reify {base} (lift lower) = lower
reify {a ⇒ a₁} f = lam (reify (f (π₁ Id) (reflect vz)))

reflect {base} i = lift i
reflect {a ⇒ b} R s = reflect ∘ _$_ (R [ s ]) ∘ reify

data In : Con → Ty → Set where
  Z : ∀{X x} → In (X , x) x
  S : ∀{X x y} → In X x → In (X , y) x

[_⊢*_] : Con -> Con -> Set₁
[ X ⊢* Y ] = ∀{a} -> In Y a -> [ X ⊢ a ]

rename : ∀{X Y} (s : Tms Y X) {a} -> [ X ⊢ a ] -> [ Y ⊢ a ]
rename s {base} (lift l) = lift (l [ s ])
rename s {a ⇒ b} f t = f (s ∘t t)

extend : ∀{X Y a} -> [ Y ⊢* X ] -> [ Y ⊢ a ] -> [ Y ⊢* X , a ]
extend p x Z = x
extend p x (S z) = p z

inject : ∀{X a} → (x : In X a) → Tm X a
inject Z = vz
inject (S x) = vs (inject x)

id* : ∀ {X} -> [ X ⊢* X ]
id* = reflect ∘ inject

weaken : ∀{X Y A} → [ Y ⊢* X , A ] → [ Y ⊢* X ]
weaken x i = x (S i)

apply : ∀ {X W} (tms : Tms X W) {Y} → (p : [ Y ⊢* X ]) → [ Y ⊢* W ]
den : ∀{X a} -> Tm X a -> ∀ {Y} -> [ Y ⊢* X ] -> [ Y ⊢ a ]

apply (t ∘t v) p = apply t (apply v p)
apply Id p = p
apply (tms , x) p Z = den x p
apply (tms , x) p (S n) = apply tms p n
apply (π₁ tms) p n = apply tms p (S n)

den (M [ tms ]) p = den M (apply tms p) 
den (π₂ tms) p = (apply tms p) Z
den (lam M) p s x = den M (extend (rename s ∘ p) x)
den (app M) p = den M (weaken p) Id (p Z)

normalize : ∀{X a} → Tm X a → Tm X a
normalize M = reify (den M id*)

cnat : Ty
cnat = (base ⇒ base) ⇒ base ⇒ base

czero : ∀{G} → Tm G cnat
czero = lam (π₂ Id)

csuc : ∀{G} → Tm G (cnat ⇒ cnat)
csuc = lam (lam (lam (vs vz $ (vs (vs vz) $ vs vz $ vz))))

ctwo : ∀{G} → Tm G cnat
ctwo = csuc $ (csuc $ czero)