#lang racket
;; Grammar (Λ)
;; t := λ t | app t t | i

;; Domain
;; D ≃ neu D_ne | fun [D → D]
;; D_ne = var i | app D_ne D
;; Define as we go

(define (ap a b)
  (match a
    [`(fun ,f) (f identity b)]
    [`(neu ,u) `(neu (app ,u ,b))]))

(define compose-ren compose)
(define (compose-ren-sub ξ ρ) (compose (curry ren-dom ξ) ρ))
(define (ext ρ a)
  (lambda (i)
    (if (zero? i)
        a
        (ρ (- i 1)))))

(define (ren-ne-dom ξ a)
  (match a
    [`(var ,i) `(var ,(ξ i))]
    [`(app ,a ,b) `(app ,(ren-ne-dom ξ a) ,(ren-dom ξ b))]))

(define (ren-dom ξ a)
  (match a
    [`(neu ,a) `(neu ,(ren-ne-dom ξ a))]
    [`(fun ,f) `(fun ,(λ (ξ0 α) (f (compose-ren ξ0 ξ) α)))]))

(define (interp a ρ)
  (match a
    [`(var ,i) (ρ i)]
    [`(λ ,a)  (list 'fun (λ (ξ x) (interp a (ext (compose-ren-sub ξ ρ) x))))]
    [`(app ,a ,b) (ap (interp a ρ) (interp b ρ))]))

(define (reify a)
  (match a
    [`(fun ,f) (list 'λ (reify (f  (curry + 1) '(neu (var 0)))))]
    [`(neu ,a) (reify-neu a)]))

(define (reify-neu a)
  (match a
    [`(app ,u ,v) (list 'app (reify-neu u) (reify a))]
    [`(var ,i) a]))

(define (idsub i) `(neu (var ,i)))

(define (normalize a)
  (reify (interp a idsub)))

(provide normalize)