CPS transform using Eff

cps.eff

(* delimited continuations from Programming with Algebraic Effects and Handlers - Andrej Bauer, Matija Pretnar*)

type ('a, 'b) delimited = effect
 operation shift : (('a -> 'b) -> 'b) -> 'a
end

let rec reset d = handler
 | d#shift f k -> with reset d handle (f k)


(* Named variable and HOAS syntax *)

type t =
 | TSym of string
 | TVar of int
 | TApp of (t * t)
 | TAbs of (int * t)
 | TReset of t
 | TShift of (int * t)

type 'a h =
 | HSym of string
 | HVar of 'a
 | HApp of ('a h * 'a h)
 | HAbs of ('a -> 'a h)
 | HReset of ('a h)
 | HShift of ('a -> 'a h)

let rec reify e i = match e with
 | HSym s -> TSym s
 | HVar x -> x
 | HApp (m,n) -> TApp (reify m i, reify n i)
 | HAbs f -> TAbs (i, reify (f (TVar i)) (i+1))
 | HReset b -> TReset (reify b i)
 | HShift h -> TShift (i, reify (h (TVar i)) (i+1))

let rec reflect e l = match e with
 | TSym s -> HSym s
 | TVar i -> (match assoc i l with Some r -> r)
 | TApp (m,n) -> HApp (reflect m l, reflect n l)
 | TAbs (i,m) -> HAbs (fun x -> reflect m ((i, HVar x) :: l))
 | TReset b -> HReset (reflect b l)
 | TShift (i,m) -> HShift (fun c -> reflect m ((i, HVar c) :: l))

(* CPS transform: Abstracting Control by Olivier Danvy, Andrzej Filinski *)

let d = new delimited

let rec cps e = match e with
 | HSym s -> HSym s
 | HVar i -> HVar i
 | HApp (m,n) -> d#shift (fun k -> (HApp (HApp (cps m,cps n),HAbs (fun t -> k (HVar t)))))
 | HAbs m -> HAbs (fun x -> HAbs (fun k ->
               with reset d handle
                 HApp (HVar k,cps (m x))))
 | HReset b -> with reset d handle cps b
 | HShift h -> d#shift (fun c -> HApp (HAbs (fun x -> with reset d handle cps (h x)),
                                       HAbs (fun v -> HAbs (fun k -> HApp (HVar k, c (HVar v))))))

let cps_transform e = reify (with reset d handle cps (reflect e [])) 0

(* Examples:

\x -> x  ==>  \x k -> k x

# cps_transform (TAbs (0,TVar 0));;
- : t = TAbs (0, TAbs (1, TApp (TVar 1, TVar 0)))


(\x -> x) (\y -> y)  ==>  (\x k -> k x) (\y k -> k y) id

# cps_transform (TApp (TAbs (0,TVar 0),TAbs (0,TVar 0)));;
- : t = TApp (TApp (TAbs (0, TAbs (1, TApp (TVar 1, TVar 0))), 
                    TAbs (0, TAbs (1, TApp (TVar 1, TVar 0)))), 
              TAbs (0, TVar 0))


(\x -> (\y -> y x))  ==>  (\x k -> k (\y c -> (y x) (\z -> c z)))

# cps_transform (TAbs (0,TAbs (1,TApp (TVar 1,TVar 0))));;
- : t = TAbs (0, 
              TAbs (1, 
                    TApp (TVar 1, 
                          TAbs (2, 
                                TAbs (3, 
                                      TApp (TApp (TVar 2, TVar 0), 
                                            TAbs (4, TApp (TVar 3, TVar 4))))))))

cps_transform (TReset (TApp (TSym "Goldilocks said: ", TReset (TApp (TSym "the porridge is ", TShift (0,TApp (TApp (TVar 0, TSym "too hot"), TApp (TApp (TVar 0, TSym "too cold"), TApp (TApp (TVar 0, TSym "just right"), TSym ".")))))))));;

*)

(* shift/reset example from http://okmij.org/ftp/papers/delimcc-tohoku-talk.pdf *)

let join (x,y) = TApp (TApp (TSym "^", x), y)

let goldilocks_pre = (TReset
       (join (TSym "Goldilocks said: ",
               TReset (join (join (TSym "the porridge is ",
                  TShift (0, join (TApp (TVar 0, TSym "too hot"),
                              join (TApp (TVar 0, TSym "too cold"),
                                    TApp (TVar 0, TSym "just right"))))), TSym ". ")))));;

let goldilocks = cps_transform goldilocks_pre ;;


(* emit scheme to test *)

let rec print_t exp = 
  match exp with
  | TSym s -> print s
  | TVar i -> print_string "v"; print i
  | TApp (f, a) -> print_string "("; print_t f; print_string " "; print_t a; print_string ")"
  | TAbs (a, t) -> print_string "(lambda (v"; print a; print_string ") "; print_t t; print_string ")"
  | TReset t -> print_string "(reset "; print_t t; print_string ")"
  | TShift (i, t) -> print_string "(shift v"; print i; print_string " "; print_t t; print_string ")" ;;


print_t goldilocks_pre;;
print_endline "----";;
print_t goldilocks;;

(*



#lang racket
(require racket/control)

;; (define ^ (lambda (x) (lambda (y) (string-append x y))))
;; (reset ((^ "Goldilocks said: ") (reset ((^ ((^ "the porridge is ") (shift v0 ((^ (v0 "too hot")) ((^ (v0 "too cold")) (v0 "just right")))))) ". "))))
;; ;; "Goldilocks said: the porridge is too hot. the porridge is too cold. the porridge is just right. "

(define ^ (lambda (x) (lambda (k) (k (lambda (y) (lambda (c) (c (string-append x y))))))))
((^ "Goldilocks said: ") (lambda (v0) ((v0 ((^ "the porridge is ") (lambda (v1) ((lambda (v2) ((v2 "too hot") (lambda (v3) ((^ v3) (lambda (v4) ((v2 "too cold") (lambda (v5) ((^ v5) (lambda (v6) ((v2 "just right") (lambda (v7) ((v6 v7) (lambda (v8) ((v4 v8) (lambda (v9) v9))))))))))))))) (lambda (v2) (lambda (v3) (v3 ((v1 v2) (lambda (v4) ((^ v4) (lambda (v5) ((v5 ". ") (lambda (v6) v6))))))))))))) (lambda (v1) v1))))
;; "Goldilocks said: the porridge is too hot. the porridge is too cold. the porridge is just right. "

*)

You know that you can put the racket thing in a separate file, in the same gist?