hoas-delim-cps.scm

#lang racket

(require scheme/control)

;; Pattern matching

(define (pattern? p e)
  (cond ((null? p) (null? e))
        ((equal? p '_) #t)
        ((symbol? p) (and (symbol? e) (equal? p e)))
        (else (and (pair? e)
                   (pattern? (car p) (car e))
                   (pattern? (cdr p) (cdr e))))))

;; Recursion on sexp lambda terms

(define (traverse var-case lam-case shift-case reset-case app-case)
  (lambda (exp)
    (cond ((symbol? exp) (var-case exp))
          ((pattern? '(lambda _ _) exp)
           (let ((args (cadr exp)) (body (caddr exp)))
             (lam-case args body)))
          ((and (pattern? '(shift _ _) exp)
                (symbol? (cadr exp)))
           (shift-case (cadr exp) (caddr exp)))
          ((pattern? '(reset _) exp)
           (reset-case (cadr exp)))
          ((list? exp) (app-case exp))
          (else (error "not a thing: " exp)))))

;; HOAS

(define (sym s) (lambda (sym var lam shft rset app) (sym s)))
(define (var v) (lambda (sym var lam shft rset app) (var v)))
(define (lam nms f) (lambda (sym var lam shft rset app) (lam nms f)))
(define (shft nm h) (lambda (sym var lam shft rset app) (shft nm h)))
(define (rset m) (lambda (sym var lam shft rset app) (rset m)))
(define (app . exp) (lambda (sym var lam shft rset app) (app exp)))

(define (concretize t)
  ;; HOAS -> sexp
  (t (lambda (s) s)
     (lambda (v) v)
     (lambda (nms f) (let ((gs (map gensym nms))) `(lambda ,gs ,(concretize (apply f gs)))))
     (lambda (nm h) (let ((n (gensym nm))) `(shift ,n ,(concretize (h n)))))
     (lambda (m) `(reset ,(concretize m)))
     (lambda (exp) (map concretize exp))))

(define example-1 (lam '(x) (lambda (x) (var x))))
(define example-2 (lam '(x) (lambda (x) (lam '(y) (lambda (y) (app (var y) (var x)))))))
(define example-3 (lam '(x y z) (lambda (x y z) (app (app (var x) (var y)) (app (var y) (var z))))))
(define example-4 (lam '(u v) (lambda (u v) (app (var u) (var v) (var v) (var v) (var u)))))
(define example-5 (rset (app (sym 'bar) (shft 'c (lambda (c) (app (var c) (app (var c) (sym 'foo))))))))

;; sexp -> HOAS

(define (hoas env)
  (traverse (lambda (v) (let ((r (assoc v env)))
                          (if r (var (cdr r)) (sym v))))
            (lambda (xs m) (lam xs (lambda ys ((hoas (append (map cons xs ys) env)) m))))
            (lambda (nm h) (shft nm (lambda (c) ((hoas (cons (cons nm c) env)) h))))
            (lambda (m) (rset ((hoas env) m)))
            (lambda (x) (apply app (map (hoas env) x)))))

;; >  (concretize ((hoas '()) '(lambda (x y z) ((lambda (y) (x y z x y)) (y z z)))))
;; '(lambda (x22094 y22095 z22096)
;;    ((lambda (y22097) (x22094 y22097 z22096 x22094 y22097)) (y22095 z22096 z22096)))
;; > (concretize ((hoas '()) '(shift c (c (reset (c (shift e (e f))))))))
;; '(shift c39549 (c39549 (reset (c39549 (shift e39550 (e39550 f))))))

;; CPS

;; Abstracting Control (1990) by Olivier Danvy, Andrzej Filinski 

(define (cps t)
  (t (lambda (s) (sym s))
     (lambda (v) (var v))
     (lambda (nms f)
       (let ((cont (gensym 'cont)))
         (lam (cons cont nms) (lambda ys (reset (app (var (car ys)) (cps (apply f (cdr ys)))))))))
     (lambda (nm h)
       (shift c (app (lam `(,nm) (lambda (nm) (reset (cps (h nm)))))
                     (lam `(k v) (lambda (k v) (app (var k) (c (var v))))))))
     (lambda (m)
       (reset (cps m)))
     (lambda (x)
       (shift c (apply app (cons (cps (car x)) (cons (lam '(a) (lambda (a) (c (var a)))) (map cps (cdr x)))))))))

;; (define (kons k x y) (k (cons x y)))
;; > (concretize (reset (app (sym 'halt) (cps ((hoas '()) '(cons x (reset (cons y (shift c (c (c (c z))))))))))))
;; '(cons
;;   (lambda (a50175) (halt a50175))
;;   x
;;   ((lambda (c50176)
;;      (c50176 (lambda (a50177) (c50176 (lambda (a50178) (c50176 (lambda (a50179) a50179) a50178)) a50177)) z))
;;    (lambda (k50180 v50181) (k50180 (cons (lambda (a50182) a50182) y v50181)))))
;; > (kons
;;   (lambda (a49129) (display a49129))
;;   'x
;;   ((lambda (c49130)
;;      (c49130 (lambda (a49131) (c49130 (lambda (a49132) (c49130 (lambda (a49133) a49133) a49132)) a49131)) 'z))
;;    (lambda (k49134 v49135) (k49134 (kons (lambda (a49136) a49136) 'y v49135)))))
;; (x y y y . z)

;; need to CPS again after removing control operators from the first CPS to get into 'every call is a tail call'
;; doing it twice means every function now takes two continuations and blows up a lot
;; will need a more efficient method