Adds the delimited continuations model to examples

collects/meta/props

@@ -1182,6 +1182,7 @@ path/s is either such a string or a list of them.
 "collects/redex/examples/church.rkt" drdr:command-line (mzc *)
 "collects/redex/examples/combinators.rkt" drdr:command-line (mzc *)
 "collects/redex/examples/compatible-closure.rkt" drdr:command-line (mzc *)
+"collects/redex/examples/delim-cont/tests.rkt" drdr:command-line (mzc *)
 "collects/redex/examples/letrec.rkt" drdr:command-line (mzc *)
 "collects/redex/examples/omega.rkt" drdr:command-line (mzc *)
 "collects/redex/examples/r6rs/r6rs-tests.rkt" drdr:command-line (mzc *)

collects/redex/examples/README

@@ -22,6 +22,10 @@ to demonstrate various different uses of PLT Redex:
   with function contracts, (eager) pair contracts, 
   and a few numeric predicates
 
+  delim-cont: The model from Flatt, Yu, Findler, and Felleisen's ICFP
+  '07 paper "Adding Delimited and Composable Control to a Production
+  Programming Environment"
+
   letrec.rkt: shows how to model letrec with a store and
   some infinite looping terms
 

collects/redex/examples/delim-cont/README.txt

@@ -0,0 +1,22 @@
+To run the tests using the model:
+---------------------------------
+
+ 1. Open "tests.rkt" in DrRacket
+
+ 2. Change DrRacket's current language to "Use the langauge declared
+ in the source"
+
+ 3. Click "Run"
+
+Afterward, in the REPL window that shows whether the tests passed, you
+can try your own expressions using the `show' function. The program
+`call/cc-loop' is helpfully defined, so that you can try
+
+ (show call/cc-loop)
+
+
+To read the program:
+--------------------
+
+After a quick look at "grammar.rkt", read "reduce.rkt". If you become
+interested in a metafunction, see "meta.rkt"

collects/redex/examples/delim-cont/grammar.rkt

@@ -0,0 +1,92 @@
+#lang racket
+
+(require redex/reduction-semantics)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Expression grammar:
+
+;; `core-grammar' is typeset for the paper, but `grammar'
+;; extends it with some standard things (such as arithmetic,
+;; assignment, and output) to make testing easier.
+
+(define-language core-grammar
+  ;; Expressions
+  ;;  Constrain `wcm' so that it can't
+  ;;  wrap an immediate `wcm':
+  (e m (wcm w m))
+  (m x v (e e ...) (begin e e) (% e e e) (dw x e e e)) 
+  
+  ;; Values
+  (v (list v ...) (λ (x ...) e) (cont v (hide-hole E)) (comp (hide-hole E))
+     dynamic-wind abort current-marks
+     cons u)
+  (n number)
+  
+  ;; Primitives that need a wcm wrapper:
+  (u call/cc call/comp call/cm)
+  
+  ;; Variables
+  (x (variable-except λ if begin set!
+                      call/cc cont 
+                      % call/comp abort comp
+                      dynamic-wind dw
+                      call/cm wcm current-marks
+                      zero? + print cons list first rest
+                      * <>))
+  
+  ;; `wcm' bindings
+  (w ((v v) ...))
+  
+  ;; Evaluation contexts
+  ;;  Constrain `wcm' so it can't wrap a `wcm'.
+  ;;  General evalation context:
+  (E W (in-hole W (dw x e E e)))
+  ;;  Evaluation context without `dw':
+  (W M (wcm w M))
+  (M hole (v ... W e ...) (begin W e) (% v W v))
+  ;; Context ending on a dw boundary:
+  (D hole (in-hole E (dw x e hole e))))
+
+(define-extended-language grammar core-grammar
+  
+  (p (<> s       ; store
+         (o ...) ; output
+         e))     ; expression
+  
+  (m ....
+     (if e e e)
+     (set! x e))
+  (v ....
+     n #f #t
+     zero? print + first rest)
+  
+  ;; Store
+  (s ([x v] ...))
+  
+  ;; Output
+  (o number)
+  
+  (M ....
+     (set! x W)
+     (if W e e)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Debugging:
+
+(define-syntax (define-language-predicates stx)
+  (syntax-case stx ()
+    [(_ id)
+     (with-syntax ([? (datum->syntax
+                       #'id
+                       (string->symbol (format "~s?" (syntax-e #'id)))
+                       #'id)])
+       #'(define ? (redex-match grammar id)))]
+    [(_ id ...)
+     #'(begin (define-language-predicates id) ...)]))
+
+(define-language-predicates p e x v E)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(provide core-grammar grammar
+         p? e? x? v? E?)

collects/redex/examples/delim-cont/meta.rkt

@@ -0,0 +1,136 @@
+#lang racket
+
+(require redex/reduction-semantics
+         "grammar.ss")
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Substitution:
+
+(define-metafunction grammar
+  [(subst x_1 x_1 e_1) ; shortcut
+   e_1]
+  [(subst x_1 e_1 (λ (x_2 ... x_1 x_3 ...) e_2))
+   (λ (x_2 ... x_1 x_3 ...) e_2)]
+  [(subst x_1 x_2 (λ (x_3 ...) e_1)) ; shortcut; x_1 != any x_3
+   (λ (x_3 ...) (subst x_1 x_2 e_1))]
+  [(subst x_1 e_1 (λ (x_2 ...) e_2)) ; x_1 != any x_2
+   ,(term-let ([(x_new ...) (variables-not-in (term e_1) (term (x_2 ...)))])
+              (term (λ (x_new ...) 
+                      (subst x_1 e_1 (subst* (x_2 ...) (x_new ...) e_2)))))]
+  [(subst x_1 e_1 x_1) e_1]
+  [(subst x_1 e x_2) x_2] ; x_1 != x_2, since previous didn't match
+  [(subst x_1 e_1 v_1) v_1] ; all other values are atomic
+  [(subst x_1 e_1 (list v_1 ...)) (list (subst x_1 e_1 v_1) ...)]
+  [(subst x_1 e_1 (e_2 ...))
+   ((subst x_1 e_1 e_2) ...)]
+  [(subst x_1 e_1 (if e_2 e_3 e_4))
+   (if (subst x_1 e_1 e_2) 
+       (subst x_1 e_1 e_3)
+       (subst x_1 e_1 e_4))]
+  [(subst x_1 e_1 (begin e_2 e_3))
+   (begin (subst x_1 e_1 e_2) 
+          (subst x_1 e_1 e_3))]
+  [(subst x_1 e_1 (set! x_2 e_2))
+   (set! x_2 (subst x_1 e_1 e_2))]
+  [(subst x_1 e_1 (% e_2 e_3 e_4))
+   (% (subst x_1 e_1 e_2) 
+      (subst x_1 e_1 e_3) 
+      (subst x_1 e_1 e_4))]    
+  [(subst x_1 e_1 (wcm ((v_1 v_2) ...) e_2))
+   (wcm (((subst x_1 e_1 v_1)
+          (subst x_1 e_1 v_2)) ...)
+        (subst x_1 e_1 e_2))]
+  [(subst x_1 e_1 (dw x_2 e_2 e_3 e_4))
+   (dw x_2
+       (subst x_1 e_1 e_2) 
+       (subst x_1 e_1 e_3) 
+       (subst x_1 e_1 e_4))])
+
+(define-metafunction grammar
+  [(subst* () () e_1) e_1]
+  [(subst* (x_1 x_2 ...) (e_1 e_2 ...) e_3)
+   (subst* (x_2 ...) (e_2 ...) (subst x_1 e_1 e_3))])
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Other meta-functions:
+
+(define-metafunction grammar
+  [(noPrompt v_1 (% v_1 E v)) #f]
+  [(noPrompt v_1 (% v_2 E_1 v)) (noPrompt v_1 E_1)]
+  [(noPrompt v hole) #t]
+  [(noPrompt v_1 (v ... E_1 e ...)) (noPrompt v_1 E_1)]
+  [(noPrompt v_1 (if E_1 e_2 e_3)) (noPrompt v_1 E_1)]
+  [(noPrompt v_1 (begin E_1 e_2)) (noPrompt v_1 E_1)]
+  [(noPrompt v_1 (set! x E_1)) (noPrompt v_1 E_1)]
+  [(noPrompt v_1 (wcm w E_1)) (noPrompt v_1 E_1)]
+  [(noPrompt v_1 (dw x e_0 E_1 e_1)) (noPrompt v_1 E_1)])
+
+(define-metafunction grammar
+  [(get-marks-core (in-hole hole hole) v e_2) e_2]
+  [(get-marks-core (wcm (name w_1 ((v_4 v_5) ... (v_1 v_3) (v_6 v_7) ...)) E_1) v_1 e_2) (get-marks E_1 v_1 (cons v_3 e_2))]
+  [(get-marks-core (wcm w_1 E_1) v_1 e_2) (get-marks E_1 v_1 e_2) (side-condition (term (notInDom (v_1 w_1))))]
+  [(get-marks-core (v ... E_1 e ...) v_1 e_2) (get-marks E_1 v_1 e_2)]
+  [(get-marks-core (begin E_1 e) v_1 e_2) (get-marks E_1 v_1 e_2)]
+  [(get-marks-core (% v_2 E_1 v_3) v_1 e_2) (get-marks E_1 v_1 e_2)]
+  [(get-marks-core (dw x e E_1 e) v_1 e_2) (get-marks E_1 v_1 e_2)])
+
+(define-metafunction grammar
+  [(get-marks (if E_1 e e) v_1 e_2) (get-marks E_1 v_1 e_2)]
+  [(get-marks (set! x E_1) v_1 e_2) (get-marks E_1 v_1 e_2)]
+  [(get-marks E_1 v_1 e_2) (get-marks-core E_1 v_1 e_2)])
+
+(define-metafunction grammar
+  [(expose-wcm e_1) e_1 (side-condition (term (noMatchWCM e_1 (wcm w e))))]
+  [(expose-wcm (wcm () e_1)) e_1]
+  [(expose-wcm (wcm ((v_1 v_2) (v_3 v_4) ...) e_1))
+   (call/cm v_1 v_2 (λ () (expose-wcm (wcm ((v_3 v_4) ...) e_1))))])
+
+(define-metafunction grammar
+  [(sameDWs W_1 W_2) (True)]
+  [(sameDWs (in-hole W_1 (dw x_1 e_1 E_1 e_2)) 
+            (in-hole W_2 (dw x_1 e_1 E_2 e_2)))
+   (sameDWs E_1 E_2)]
+  [(sameDWs any_1 any_2) (False)])
+
+(define-metafunction grammar
+  [(noShared (in-hole W_1 (dw x_1 e_1 E_1 e_2))
+             (in-hole W_2 (dw x_1 e_1 E_2 e_2)))
+   (False)]
+  [(noShared any_1 any_2) (True)])
+
+(define-metafunction grammar
+  [(nonWCM (in-hole E (wcm w hole))) #f]
+  [(nonWCM any) #t])
+
+;; The rest are helpers that are typeset specially in the paper
+
+(define-metafunction grammar
+  [(noMatch E_1 any (% v_1 any_1 any_2)) (noPrompt v_1 E_1)]
+  [(noMatch E_1 any (wcm any_1 any_2)) (nonWCM E_1)])
+
+(define-metafunction grammar
+  [(noMatchWCM (wcm w e_1) any) #f]
+  [(noMatchWCM any_1 any_2) #t])
+
+(define-metafunction grammar
+  [(notIn v_1 (v_2 ...)) ,(not (member (term v_1) (term (v_2 ...))))])
+
+(define-metafunction grammar
+  [(notInDom v_1 ((v_2  v_3) ...)) (notIn v_1 (v_2 ...))])
+
+(define-metafunction grammar [(True) #t])
+(define-metafunction grammar [(False) #f])
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(provide subst subst*
+         noPrompt
+         get-marks get-marks-core
+         expose-wcm
+         sameDWs
+         noShared
+         nonWCM
+         noMatch
+         noMatchWCM
+         notIn
+         notInDom)

collects/redex/examples/delim-cont/reduce.rkt

@@ -0,0 +1,212 @@
+#lang racket
+
+(require redex/reduction-semantics
+         "grammar.ss"
+         "meta.ss")
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Reductions:
+
+(define :->
+  (reduction-relation
+   grammar
+   
+   ;; beta
+   (~~> ((λ (x_1 ...) e_1) v_1 ...)
+        (subst* (x_1 ...) (v_1 ...) e_1)
+        "beta")
+   
+   ;; arithmetic
+   (~~> (+ n_1 n_2)
+        ,(+ (term n_1) (term n_2))
+        "+")
+   (~~> (zero? 0)
+        #t
+        "zero?")
+   (~~> (zero? v_1)
+        #f
+        (side-condition (not (zero? (term v_1))))
+        "non-zero")
+   
+   ;; lists
+   (~~> (cons v_1 (list v_2 ...))
+        (list v_1 v_2 ...)
+        "cons")
+   (~~> (first (list v_1 v_2 ...))
+        v_1
+        "first")
+   (~~> (rest (list v_1 v_2 ...))
+        (list v_2 ...)
+        "rest")
+   
+   ;; printing
+   (--> (<> s_1 [o_1 ...] (in-hole E_1 (print o_2)))
+        (<> s_1 [o_1 ... o_2] (in-hole E_1 #f))
+        "print")
+   
+   ;; if
+   (~~> (if #t e_1 e_2)
+        e_1
+        "ift")
+   (~~> (if #f e_1 e_2)
+        e_2
+        "iff")
+   
+   ;; begin
+   (~~> (begin v e_1)
+        e_1
+        "begin-v")
+   
+   ;; set! and lookup
+   (--> (<> ([x_1 v_1] ... [x_2 v_2] [x_3 v_3] ...) [o_1 ...] (in-hole E_1 (set! x_2 v_4)))
+        (<> ([x_1 v_1] ... [x_2 v_4] [x_3 v_3] ...) [o_1 ...] (in-hole E_1 #f))
+        "assign")
+   (--> (<> ([x_1 v_1] ... [x_2 v_2] [x_3 v_3] ...) [o_1 ...] (in-hole E_1 x_2))
+        (<> ([x_1 v_1] ... [x_2 v_2] [x_3 v_3] ...) [o_1 ...] (in-hole E_1 v_2))
+        "lookup")
+   
+   ;; prompt
+   ;;  When we get a value, drop the prompt.
+   (~~> (% v_1 v_2 v_3)
+        v_2
+        "prompt-v")
+   
+   ;; call/cc
+   ;;  Capture; the context E_2 must not include a prompt with the same tag,
+   ;;  and we don't want immediate marks.
+   (~~> (% v_2 (in-hole E_2 (wcm w_1 (call/cc v_1 v_2))) v_3)
+        (% v_2 (in-hole E_2 (wcm w_1 (v_1 (cont v_2 E_2)))) v_3)
+        (side-condition (term (noMatch E_2 E (% v_2 E v))))
+        "call/cc")
+   ;;  Invoke a continuation when there are no dw pre or post thunks to run (i.e.,
+   ;;  no dw thunks in the unshared parts of the current and target continuations).
+   ;;  D_2/D_6 is shared between the captured and current continuations; we make sure
+   ;;  that W_3 and E_4 don't share.
+   (~~> (% v_1 (in-hole D_2 (in-hole W_3 ((cont v_1 (in-hole D_6 (in-hole W_4 hole))) v_2))) v_3)
+        (% v_1 (in-hole D_6 (in-hole W_4 v_2)) v_3)
+        (side-condition (term (noMatch (in-hole D_2 W_3) E (% v_1 E v))))
+        (side-condition (term (sameDWs D_2 D_6)))
+        (side-condition (term (noShared W_3 W_4)))
+        "cont")
+   ;;  Invoke a continuation where there is a dw post thunk to run:
+   ;;   - D_2/D_6 is the shared prefix of the current and captured continuation.
+   ;;     (We make sure that E_3[(dw x_1 e_1 W_5 e_2)] and E_4 don't share.)
+   ;;   - Keep D_2[E_3], replacing the relevant `dw' to run the post thunk
+   ;;     and then resume the continuation jump.
+   ;;  The second step means replacing (dw x e_1 W_5[((cont ...) v)] e_2)
+   ;;  with (begin e_2 ((cont ...) v))).
+   (~~> (% v_2 (in-hole D_2 (in-hole E_3 (dw x_1 e_1 (in-hole W_5 ((cont v_2 (in-hole D_6 (hide-hole E_4))) v_1)) e_2))) v_3)
+        (% v_2 (in-hole D_2 (in-hole E_3 (begin e_2 ((cont v_2 (in-hole D_6 E_4)) v_1)))) v_3)
+        (side-condition (term (noMatch (in-hole D_2 E_3) E (% v_2 E v))))
+        (side-condition (term (sameDWs D_2 D_6)))
+        (side-condition (term (noMatch W_5 E (% v_2 E v))))
+        (side-condition (term (noShared (in-hole E_3 (dw x_1 e_1 W_5 e_2)) E_4)))
+        "cont-post")
+   ;;  Invoke a continuation when there are only dw pre thunks to run (i.e.,
+   ;;  no dw thunks in the unshared part of the current continuation).
+   ;;  D_2/D_6 is shared between the captured and current continuations; we
+   ;;  make sure that W_3 and W_4[(dw ...)] don't share.
+   ;;  We do one pre thunk at a time, just in case the pre thunk arranges for
+   ;;  the relevant prompt to disappear. To do just one pre thunk, we
+   ;;  create `(begin e_1 (dw x_1 e_1 ((cont ...) v) e_2))', which runs the pre
+   ;;  thunk and then tries again to invoke the continuation --- but inside a
+   ;;  `dw' for the already-run pre-thunk, so that it's treated as shared and not
+   ;;  run again.
+   (~~> (% v_1 (in-hole D_2 (in-hole W_3 ((cont v_1 (name k_1 (in-hole D_6 (in-hole W_4 (dw x_1 e_1 (hide-hole E_5) e_2))))) v_2))) v_3)
+        (% v_1 (in-hole D_6 (in-hole W_4 (begin e_1 (dw x_1 e_1 ((cont v_1 k_1) v_2) e_2)))) v_3)
+        (side-condition (term (noMatch (in-hole D_2 W_3) E (% v_1 E v))))
+        (side-condition (term (sameDWs D_2 D_6)))
+        (side-condition (term (noShared W_3 (in-hole W_4 (dw x_1 e_1 E_5 e_2)))))
+        "cont-pre")
+   
+   ;; abort
+   ;;  Like continuation invocation, the case without dw post thunks:
+   (~~> (% v_1 (in-hole W_2 (abort v_1 v_2)) v_3)
+        (v_3 v_2)
+        (side-condition (term (noMatch W_2 E (% v_1 E v))))
+        "abort")
+   ;;  And the case with a dw post thunk --- simpler than invoking a
+   ;;  continuation, because we don't have to compute shared parts:
+   (~~> (dw x_1 e_1 (in-hole W_2 (abort v_1 v_2)) e_2)
+        (begin e_2 (abort v_1 v_2))
+        (side-condition (term (noMatch W_2 E (% v_1 E v))))
+        "abort-post")
+   
+   ;; composable continuation
+   ;;  Capture up to the relevant prompt, not including immediate marks:
+   (~~> (% v_2 (in-hole E_2 (wcm w_1 (call/comp v_1 v_2))) v_3)
+        (% v_2 (in-hole E_2 (wcm w_1 (v_1 (comp E_2)))) v_3)
+        (side-condition (term (noMatch E_2 E (% v_2 E v))))
+        "call/comp")
+   ;;  On invocation, we want to splice leading `wcm's with any marks
+   ;;  at the invocation context. We do that by convertings the leading
+   ;;  `wcm's back to `call/cm', so they get spliced as usual
+   ;;  for evaluating `call/cm' (see below). Meanwhile, we need to
+   ;;  handle the case that there are dw pre thunks to run on the way in
+   ;;  (which is a little simpler than for non-composable continuations,
+   ;;  since we don't have to worry about sharing w.r.t. a prompt).
+   (~~> ((comp (in-hole W_1 hole)) v_1)
+        (expose-wcm (in-hole W_1 v_1))
+        "comp")
+   (~~> ((comp (in-hole W_1 (dw x_1 e_1 (hide-hole E_2) e_2))) v_1)
+        (expose-wcm (in-hole W_1 (begin e_1 (dw x_1 e_1 ((comp E_2) v_1) e_2))))
+        "comp-pre")
+   
+   ;; continuation marks
+   ;;  Introduce a `wcm' when needed for certain primitives:
+   (-+> (in-hole E_1 (u_1 v_1 ...))
+        (in-hole E_1 (wcm () (u_1 v_1 ...)))
+        (side-condition (term (noMatch E_1 E (wcm w hole))))
+        "wcm-intro")
+   ;;  When we get a value, discard marks:
+   (~~> (wcm w v_1)
+        v_1
+        "wcm-v")
+   
+   ;;  When `call/cm' uses the same key as a wrapping
+   ;;  mark, then replace the old value.
+   (~~> (wcm ((v_1 v_2) ... (v_3 v_4) (v_5 v_6) ...) 
+             (call/cm v_3 v_7 (λ () e_1)))
+        (wcm ((v_1 v_2) ... (v_3 v_7) (v_5 v_6) ...) e_1)
+        "wcm-set")
+   ;;  When `call/cm' uses a different key than any wrapping
+   ;;  mark, then add a new mark.
+   (~~> (wcm ((v_1 v_2) ...) (call/cm v_3 v_4 (λ () e_1)))
+        (wcm ((v_1 v_2) ... (v_3 v_4)) e_1)
+        (side-condition (term (notIn v_3 (v_1 ...))))
+        "wcm-add")
+   ;;  To get the current mark value for mark key, search
+   ;;  the current context (using `get-marks'), using only
+   ;;  the part of the continuation up to a prompt with the
+   ;;  given tag.
+   (~~> (% v_2 (in-hole E_2 (current-marks v_1 v_2)) v_3)
+        (% v_2 (in-hole E_2 (get-marks E_2 v_1 (list))) v_3)
+        (side-condition (term (noMatch E_2 E (% v_2 E v))))
+        "marks")
+   
+   ;; dynamic-wind
+   ;;  Evaluate a `dynamic-wind' function by generating a new `dw'
+   ;;  wrapper. The wrapper uses a newly allocated (globally unique)
+   ;;  tag variable. Also, introduce a `begin' with the pre-thunk
+   ;;  body --- which, crucially, is put *outside* the generated `dw'.
+   (~~> (dynamic-wind (λ () e_1) (λ () e_2) (λ () e_3))
+        (begin e_1 (dw x_1 e_1 e_2 e_3))
+        (fresh x_1)
+        "dw")
+   ;;  When we get a result from the dw, evaluate the post thnk
+   ;;  (outside the `dw') and then continue returning the result.
+   (~~> (dw x e_1 v_1 e_3)
+        (begin e_3 v_1)
+        "dw-v")
+   
+   with
+   ;; -+> is evaluation independent of the store and output:
+   [(--> (<> s_1 [o_1 ...] from) (<> s_1 [o_1 ...] to)) (-+> from to)]
+   ;; ~~> is evaluation in any E:
+   [(-+> (in-hole E_1 from)
+         (in-hole E_1 to))
+    (~~> from to)]))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(provide :->)

collects/redex/tests/run-tests.rkt

@@ -31,6 +31,7 @@
          ("../examples/beginner.ss" main)
          "../examples/racket-machine/reduction-test.ss"
          "../examples/racket-machine/verification-test.ss"
+         "../examples/delim-cont/tests.rkt"
          ("../examples/r6rs/r6rs-tests.ss" main))
        '())))