From 623925b5d7044d7a71979f96a9ff0874126f7c8b Mon Sep 17 00:00:00 2001
From: Casey Klein <clklein@racket-lang.org>
Date: Mon, 16 Aug 2010 10:08:17 -0500
Subject: [PATCH] Adds the delimited continuations model to examples

---
 collects/meta/props                           |    1 +
 collects/redex/examples/README                |    4 +
 collects/redex/examples/delim-cont/README.txt |   22 +
 .../redex/examples/delim-cont/grammar.rkt     |   92 ++
 collects/redex/examples/delim-cont/meta.rkt   |  136 ++
 collects/redex/examples/delim-cont/reduce.rkt |  212 +++
 collects/redex/examples/delim-cont/tests.rkt  | 1141 +++++++++++++++++
 collects/redex/tests/run-tests.rkt            |    1 +
 8 files changed, 1609 insertions(+)
 create mode 100644 collects/redex/examples/delim-cont/README.txt
 create mode 100644 collects/redex/examples/delim-cont/grammar.rkt
 create mode 100644 collects/redex/examples/delim-cont/meta.rkt
 create mode 100644 collects/redex/examples/delim-cont/reduce.rkt
 create mode 100644 collects/redex/examples/delim-cont/tests.rkt

diff --git a/collects/meta/props b/collects/meta/props
index 681c9c6874..ba6d49a56e 100755
--- a/collects/meta/props
+++ b/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 *)
diff --git a/collects/redex/examples/README b/collects/redex/examples/README
index a4eafb380d..2a3396e5b0 100644
--- a/collects/redex/examples/README
+++ b/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
 
diff --git a/collects/redex/examples/delim-cont/README.txt b/collects/redex/examples/delim-cont/README.txt
new file mode 100644
index 0000000000..4403bc3f2d
--- /dev/null
+++ b/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"
diff --git a/collects/redex/examples/delim-cont/grammar.rkt b/collects/redex/examples/delim-cont/grammar.rkt
new file mode 100644
index 0000000000..bfe5918dc5
--- /dev/null
+++ b/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?)
diff --git a/collects/redex/examples/delim-cont/meta.rkt b/collects/redex/examples/delim-cont/meta.rkt
new file mode 100644
index 0000000000..01b0424177
--- /dev/null
+++ b/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)
diff --git a/collects/redex/examples/delim-cont/reduce.rkt b/collects/redex/examples/delim-cont/reduce.rkt
new file mode 100644
index 0000000000..90873e0b53
--- /dev/null
+++ b/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 :->)
\ No newline at end of file
diff --git a/collects/redex/examples/delim-cont/tests.rkt b/collects/redex/examples/delim-cont/tests.rkt
new file mode 100644
index 0000000000..7d2bad03f1
--- /dev/null
+++ b/collects/redex/examples/delim-cont/tests.rkt
@@ -0,0 +1,1141 @@
+#lang racket
+
+(require redex
+         "grammar.ss"
+         "meta.ss"
+         "reduce.ss")
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Abbreviations:
+
+;; The classic (let ([v (call/cc call/cc)]) 
+;;              ((call/cc call/cc) v))
+(define call/cc-loop
+  `(<>
+    () []
+    (% 0
+       ((λ (v) ((call/cc (λ (x) (call/cc x 0)) 0) v))
+        (call/cc (λ (x) (call/cc x 0)) 0))
+       (λ (x) x))))
+
+(define (show prog)
+  (stepper :-> prog))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Tests
+(define (test desc expr result)
+  (let ([r (car (apply-reduction-relation* :-> expr))])
+    (unless (equal? r result)
+      (printf "~s:\n~s\n" desc expr)
+      (printf "=> ~s\n\n" r)
+      (error 'test "expected ~s" result)))
+  (set! tests-passed (add1 tests-passed)))
+(define tests-passed 0)
+
+;; Basic ----------------------------------------
+
+(define (basic-tests)
+  (test "basic dw"
+        '(<>
+          () []
+          (dynamic-wind (λ () (print 1))
+                        (λ () (print 2))
+                        (λ () (print 3))))
+        '(<> () (1 2 3) #f))
+  (test "call/cc dw"
+        '(<>
+          () []
+          (%
+           0
+           (call/cc
+            (λ (k)
+              (dynamic-wind (λ () (print 1))
+                            (λ () (k 0))
+                            (λ () (print 3))))
+            0)
+           (λ (x) x)))
+        '(<> () (1 3) 0))
+  (test "abort"
+        '(<>
+          () []
+          (%
+           0             
+           (+ 10 (abort 0 7))
+           (λ (x) (+ x 1))))
+        '(<>
+          () []
+          8))
+  (test "abort inner"
+        '(<>
+          () []
+          (%
+           0             
+           (+ 10 
+              (%
+               1         
+               (abort 1 7)
+               (λ (x) (+ x 1))))
+           (λ (x) (+ x 2))))
+        '(<>
+          () []
+          18))
+  (test "abort outer"
+        '(<>
+          () []
+          (%
+           0             
+           (+ 10 
+              (%
+               1
+               (abort 0 7)
+               (λ (x) (+ x 1))))
+           (λ (x) (+ x 2))))
+        '(<>
+          () []
+          9))
+  (test "abort inner with same tag"
+        '(<>
+          () []
+          (%
+           0             
+           (+ 10 
+              (%
+               0
+               (abort 0 7)
+               (λ (x) (+ x 1))))
+           (λ (x) (+ x 2))))
+        '(<>
+          () []
+          18))
+  (test "abort handler in tail position"
+        '(<>
+          () []
+          (%
+           0
+           (call/cm
+            100 1
+            (λ ()
+              (%
+               1
+               (abort 1 (λ ()
+                          (call/cm
+                           100 2
+                           (λ ()
+                             (current-marks 100 0)))))
+               (λ (f)
+                 (f)))))
+           (λ (x) x)))
+        '(<>
+          () []
+          (list 2)))
+  (test "abort dw"
+        '(<>
+          () []
+          (%
+           0
+           (call/cc
+            (λ (k)
+              (dynamic-wind (λ () (print 1))
+                            (λ () (abort 0 7))
+                            (λ () (print 3))))
+            0)
+           (λ (x) (+ x 1))))
+        '(<> () (1 3) 8))
+  (test "call/cc 2 levels dw"
+        '(<>
+          ()
+          []
+          (%
+           0
+           (call/cc
+            (λ (k)
+              (dynamic-wind
+               (λ () (print 1))
+               (λ ()
+                 (dynamic-wind
+                  (λ () (print 2))
+                  (λ ()
+                    (k 10))
+                  (λ () (print 3))))
+               (λ () (print 4))))
+            0)
+           (λ (x) x)))
+        '(<> () [1 2 3 4] 10))
+  (test "abort 2 levels dw"
+        '(<>
+          ()
+          []
+          (%
+           0
+           (dynamic-wind
+            (λ () (print 1))
+            (λ ()
+              (dynamic-wind
+               (λ () (print 2))
+               (λ ()
+                 (abort 0 10))
+               (λ () (print 3))))
+            (λ () (print 4)))
+           (λ (x) (+ x 1))))
+        '(<> () [1 2 3 4] 11))
+  (test "in thunk isn't really in"
+        '(<>
+          () []
+          (%
+           0
+           (call/cc
+            (λ (k)
+              (dynamic-wind
+               (λ () (begin
+                       (print 1)
+                       (k 11)))
+               (λ () (print 2))
+               (λ () (print 3))))
+            0)
+           (λ (x) x)))
+        '(<> () [1] 11))
+  (test "in thunk isn't really in, but it's in surrounding"
+        '(<>
+          () []
+          (%
+           0
+           (call/cc
+            (λ (k)
+              (dynamic-wind
+               (λ () (print -1))
+               (λ ()
+                 (dynamic-wind
+                  (λ () (begin
+                          (print 1)
+                          (k 11)))
+                  (λ () (print 2))
+                  (λ () (print 3))))
+               (λ () (print -2))))
+            0)
+           (λ (x) x)))
+        '(<> () [-1 1 -2] 11))
+  (test "dw shared during jump"
+        '(<>
+          () []
+          (% 0 
+             (dynamic-wind 
+              (λ () (print 0))
+              (λ () ((call/cc (λ (f) f) 0) (λ (x) 10)))
+              (λ () (print 1)))
+             (λ (x) x)))
+        '(<> () [0 1] 10))
+  (test "dw not shared during jump"
+        '(<>
+          () []
+          (% 0 
+             ((dynamic-wind 
+               (λ () (print 0))
+               (λ () (call/cc (λ (f) f) 0))
+               (λ () (print 1)))
+              (λ (x) 10))
+             (λ (x) x)))
+        '(<> () [0 1 0 1] 10))
+  (test "composable captures continuation marks"
+        '(<>
+          () []
+          (%
+           100
+           ((λ (k) (k (λ (v) (current-marks 0 100)))) 
+            (% 0 
+               (call/cm 0 100 
+                        (λ ()
+                          ((call/comp (λ (k) (λ (v) k)) 0)
+                           99)) )
+               (λ (x) x)))
+           (λ (x) x)))
+        '(<> () [] (list 100)))
+  (test "continuation marks wrapping % not captured"
+        '(<>
+          () []
+          (%
+           101
+           ((λ (k) (k (λ (v) (current-marks 0 101)))) 
+            (call/cm 0 100 
+                     (λ ()
+                       (% 0 
+                          ((call/comp (λ (k) (λ (v) k)) 0)
+                           99)
+                          (λ (x) x)))))
+           (λ (x) x)))
+        '(<> () [] (list)))
+  (test "visible marks restricted by prompt tag"
+        '(<>
+          () []
+          (% 101
+             (call/cm 0 100
+                      (λ ()
+                        (% 102
+                           (call/cm 0 99
+                                    (λ () 
+                                      (current-marks 0 102)))
+                           (λ (x) x))))
+             (λ (x) x)))
+        '(<> () [] (list 99)))
+  (test "visible marks not restricted by other prompt tags"
+        '(<>
+          () []
+          (% 101
+             (call/cm 0 100
+                      (λ ()
+                        (% 102
+                           (call/cm 0 99
+                                    (λ () 
+                                      (current-marks 0 101)))
+                           (λ (x) x))))
+             (λ (x) x)))
+        '(<> () [] (list 99 100)))
+  (test "getting marks fails if there's no prompt with the given tag"
+        '(<>
+          () []
+          (% 101
+             (call/cm 0 100
+                      (λ ()
+                        (current-marks 0 102)))
+             (λ (x) x)))
+        '(<> () [] (% 101 (wcm ((0 100)) (current-marks 0 102)) (λ (x) x))))
+  (test "pre and post thunks in a composable continuation"
+        '(<> 
+          () []
+          ((λ (f)
+             (f (λ (v) 10)))
+           (%
+            0
+            (dynamic-wind
+             (λ () (print 1))
+             (λ ()
+               (call/comp (λ (k) k) 0))
+             (λ () (print 2)))
+            (λ (x) x))))
+        '(<>
+          ()
+          [1 2 1 2]
+          (λ (v) 10))))
+
+;; R6RS dynamic-wind ----------------------------------------
+
+(define (r6rs-dw-tests)
+  (test "out thunk is really out"
+        '(<>
+          ([n 0]
+           [do-jump? #t]
+           [k-out #f])
+          []
+          (%
+           0
+           (begin
+             (begin
+               (call/cc
+                (λ (k)
+                  (dynamic-wind
+                   (λ () (set! n (+ n 1)))
+                   (λ () (k 99))
+                   (λ ()
+                     (begin
+                       (set! n (+ n 1))
+                       (call/cc (λ (k) (set! k-out k)) 0)))))
+                0)
+               (if do-jump?
+                   (begin
+                     (set! do-jump? #f)
+                     (k-out 0))
+                   11))
+             (begin
+               (set! k-out #f)
+               n))
+           (λ (x) x)))
+        '(<> ([n 2] [do-jump? #f] [k-out #f]) [] 2))
+  (test "out thunk is really out during trimming"
+        '(<>
+          ([n 0]
+           [do-jump? #t]
+           [k-out #f])
+          []
+          (%
+           0
+           (begin
+             (call/cc
+              (λ (k)
+                (dynamic-wind
+                 (λ () (set! n (+ n 1)))
+                 (λ () (k 100))
+                 (λ ()
+                   (begin
+                     (set! n (+ n 1))
+                     (call/cc (λ (k) (set! k-out k)) 0)))))
+              0)
+             (begin
+               (if do-jump?
+                   (begin
+                     (set! do-jump? #f)
+                     (k-out 0))
+                   11)
+               (begin
+                 (set! k-out #f)
+                 n)))
+           (λ (x) x)))
+        '(<> ([n 2] [do-jump? #f] [k-out #f]) () 2))
+  (test "jumping during the results of trimming, pre-thunk"
+        '(<> 
+          ([pre-count 0]
+           [pre-jump? #f]
+           [after-jump? #t]
+           [grab? #t]
+           [the-k #f])
+          []
+          (%
+           0
+           (begin
+             (dynamic-wind
+              (λ ()
+                (begin
+                  (set! pre-count (+ pre-count 1))
+                  (if pre-jump?
+                      (begin
+                        (set! pre-jump? #f)
+                        (begin
+                          (set! after-jump? #f)
+                          (the-k 999)))
+                      999)))
+              (λ () 
+                (if grab?
+                    (call/cc
+                     (λ (k)
+                       (begin
+                         (set! grab? #f)
+                         (set! the-k k)))
+                     0)
+                    999))
+              (λ () (+ 0 10)))
+             (begin
+               (if after-jump?
+                   (begin
+                     (set! pre-jump? #t)
+                     (the-k 999))
+                   999)
+               (begin
+                 (set! the-k #f) ;; just to make testing simpler
+                 pre-count)))
+           (λ (x) x)))
+        '(<>
+          ([pre-count 3]
+           [pre-jump? #f]
+           [after-jump? #f]
+           [grab? #f]
+           [the-k #f])
+          ()
+          3))
+  (test "jumping during the results of trimming, post-thunk"
+        '(<>
+          ([post-count 0] 
+           [post-jump? #t]
+           [jump-main? #t]
+           [grab? #t]
+           [the-k #f])
+          []
+          (%
+           0
+           (begin
+             (begin
+               (if grab?
+                   (call/cc
+                    (λ (k)
+                      (begin
+                        (set! grab? #f)
+                        (set! the-k k)))
+                    0)
+                   999)
+               (dynamic-wind
+                (λ () (+ 0 1))
+                (λ () 
+                  (if jump-main?
+                      (begin
+                        (set! jump-main? #f)
+                        (the-k 999))
+                      999))
+                (λ () 
+                  (begin
+                    (set! post-count (+ post-count 1))
+                    (if post-jump?
+                        (begin
+                          (set! post-jump? #f)
+                          (the-k 999))
+                        999)))))
+             (begin
+               (set! the-k #f) ;; just to make testing simpler
+               post-count))
+           (λ (x) x)))
+        '(<>
+          ([post-count 2]
+           [post-jump? #f]
+           [jump-main? #f]
+           [grab? #f]
+           [the-k #f]) 
+          []
+          2))
+  (test "hop out one level"
+        '(<>
+          ()
+          []
+          
+          (%
+           0
+           ((dynamic-wind (λ () (print 0))
+                          (λ () (call/cc (λ (k) k) 0))
+                          (λ () (print 1)))
+            (λ (y) (print 7)))
+           (λ (x) x)))
+        '(<>
+          ()
+          [0 1 0 1 7]
+          #f))
+  (test "hop out two levels"
+        '(<> ()
+             []
+             (%
+              0
+              ((dynamic-wind 
+                (λ () (print 1))
+                (λ () 
+                  (dynamic-wind
+                   (λ () (print 2))
+                   (λ () (call/cc (λ (k) k) 0))
+                   (λ () (print 3))))
+                (λ () (print 4)))
+               (λ (y) (print 8)))
+              (λ (x) x)))
+        '(<>
+          ()
+          [1 2 3 4 1 2 3 4 8]
+          #f))
+  (test "don't duplicate tail"
+        '(<>
+          ()
+          []
+          (%
+           0
+           (dynamic-wind 
+            (λ () (print 1))
+            (λ () 
+              ((dynamic-wind (λ () (print 2))
+                             (λ () (call/cc (λ (k) k) 0))
+                             (λ () (print 3)))
+               (λ (y) (print 9))))
+            (λ () (print 4)))
+           (λ (x) x)))
+        '(<>
+          ()
+          [1 2 3 2 3 9 4]
+          #f))
+  (test "don't duplicate tail, 2 deep"
+        '(<>
+          ()
+          []
+          
+          (%
+           0
+           (dynamic-wind 
+            (λ () (print 1))
+            (λ () 
+              (dynamic-wind 
+               (λ () (print 2))
+               (λ () 
+                 ((dynamic-wind (λ () (print 3))
+                                (λ () (call/cc (λ (k) k) 0))
+                                (λ () (print 4)))
+                  (λ (y) (print 9))))
+               (λ () (print 5))))
+            (λ () (print 6)))
+           (λ (x) x)))
+        '(<>
+          ()
+          [1 2 3 4 3 4 9 5 6]
+          #f))
+  (test "hop out and back into another one"
+        '(<>
+          ()
+          []
+          (%
+           0
+           ((λ (ok)
+              (dynamic-wind (λ () (print 1))
+                            (λ () (ok (λ (y) (print 9))))
+                            (λ () (print 2))))
+            (dynamic-wind (λ () (print 3))
+                          (λ () (call/cc (λ (k) k) 0))
+                          (λ () (print 4))))
+           (λ (x) x)))
+        '(<>
+          ()
+          [3 4 1 2 3 4 1 9 2]
+          #f))
+  (test "hop out one level and back in two levels"
+        '(<>
+          ()
+          []
+          (%
+           0
+           ((λ (ok)
+              (dynamic-wind
+               (λ () (print 1))
+               (λ ()
+                 (dynamic-wind
+                  (λ () (print 2))
+                  (λ () (ok (λ (y) (print 9))))
+                  (λ () (print 3))))
+               (λ () (print 4))))
+            (call/cc (λ (k) k) 0))
+           (λ (x) x)))
+        '(<>
+          ()
+          [1 2 3 4 1 2 9 3 4]
+          #f))
+  (test "hop out two levels and back in two levels"
+        '(<>
+          ()
+          []
+          (%
+           0
+           ((λ (ok)
+              (dynamic-wind
+               (λ () (print 1))
+               (λ () 
+                 (dynamic-wind
+                  (λ () (print 2))
+                  (λ () (ok (λ (y) (print 9))))
+                  (λ () (print 3))))
+               (λ () (print 4))))
+            (dynamic-wind
+             (λ () (print 5))
+             (λ () 
+               (dynamic-wind
+                (λ () (print 6))
+                (λ () (call/cc (λ (k) k) 0))
+                (λ () (print 7))))
+             (λ () (print 8))))
+           (λ (x) x)))
+        '(<>
+          ()
+          [5 6 7 8 1 2 3 4 5 6 7 8 1 2 9 3 4]
+          #f)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; composability
+
+(define (cont-tests)
+  (test "captured under new %"
+        '(<>
+          ([retry #f])
+          []
+          (begin
+            (%
+             0
+             (+ 18
+                (call/cc
+                 (λ (k)
+                   (begin
+                     (set! retry k)
+                     17))
+                 0))
+             (λ (x) x))
+            ((λ (y)
+               (begin
+                 (set! retry #f)
+                 y))
+             (+ 1 (%
+                   0
+                   (retry 10)
+                   (λ (x) x))))))
+        '(<>
+          ([retry #f])
+          []
+          29))               
+  (test "catch in composed"
+        '(<>
+          () []
+          (%
+           0
+           ((λ (k)
+              ((λ (k2)
+                 (%
+                  0
+                  (k2 (list 89))
+                  (λ (x) x)))
+               (%
+                0
+                (k (λ ()
+                     (first (call/cc (λ (k2)
+                                       (cons k2 (list)))
+                                     0))))
+                (λ (x) x))))
+            (%
+             0
+             ((call/cc (λ (k) (λ () k))
+                       0))
+             (λ (x) x)))
+           (λ (x) x)))
+        '(<>
+          () []
+          89))
+  (test "simple composable"
+        '(<>
+          [] ()
+          ((λ (k)
+             (k (λ () 8)))
+           (%
+            0
+            ((call/comp
+              (λ (k) (λ () k))
+              0))
+            (λ (x) x))))
+        '(<> [] () 8))
+  (test "composable doesn't introduce %"
+        '(<>
+          [] ()
+          (%
+           0
+           ((λ (k)
+              ((λ (k2)
+                 (if (first (rest k2))
+                     ((first k2) (list 10 #f))
+                     (first k2)))
+               (k (λ ()
+                    (call/cc (λ (k2) 
+                               (cons k2 (list #t)))
+                             0)))))
+            (%
+             0
+             ((call/comp
+               (λ (k) (λ () k))
+               0))
+             (λ (x) x)))
+           (λ (x) x)))
+        '(<>
+          [] ()
+          10))
+  (test "post thunk runs current continuation as composable"
+        '(<>
+          ([a #f]
+           [do-a? #t])
+          []
+          (%
+           0
+           (dynamic-wind
+            (λ () (print 1))
+            (λ ()
+              (begin
+                (dynamic-wind
+                 (λ () (print 2))
+                 (λ () 
+                   ((call/cc (λ (k)
+                               (begin
+                                 (set! a k)
+                                 (λ () 12)))
+                             0)))
+                 (λ () (print 3)))
+                (dynamic-wind
+                 (λ () (print 4))
+                 (λ ()
+                   (if do-a?
+                       (begin
+                         (set! do-a? #f)
+                         (a (λ () 11)))
+                       (begin
+                         (set! a #f)
+                         12)))
+                 (λ ()
+                   (begin
+                     (print 5)
+                     (call/comp
+                      (λ (k)
+                        (k 10))
+                      0))))))
+            (λ () (print 6)))
+           (λ (x) x)))
+        '(<>
+          ([a #f][do-a? #f])
+          [1 2 3 4 5 1 6 2 3 4 5 1 6 6]
+          12))
+  (test "post thunk runs current continuation as composable under %"
+        '(<>
+          ([a #f]
+           [do-a? #t])
+          []
+          (%
+           0
+           (dynamic-wind
+            (λ () (print 1))
+            (λ ()
+              (begin
+                (dynamic-wind
+                 (λ () (print 2))
+                 (λ () 
+                   ((call/cc (λ (k)
+                               (begin
+                                 (set! a k)
+                                 (λ () 12)))
+                             0)))
+                 (λ () (print 3)))
+                (dynamic-wind
+                 (λ () (print 4))
+                 (λ ()
+                   (if do-a?
+                       (begin
+                         (set! do-a? #f)
+                         (a (λ () 11)))
+                       (begin
+                         (set! a #f)
+                         12)))
+                 (λ ()
+                   (begin
+                     (print 5)
+                     (call/comp
+                      (λ (k)
+                        (%
+                         0
+                         (k 10)
+                         (λ (x) x)))
+                      0))))))
+            (λ () (print 6)))
+           (λ (x) x)))
+        '(<>
+          ([a #f] [do-a? #f])
+          [1 2 3 4 5 1 2 3 4 5 1 6 6 2 3 4 5 1 6 6]
+          12))
+  (test "post think trims dws to run on exit"
+        '(<>
+          ([output (list)]
+           [exit-k #f]
+           [done? #f])
+          []
+          (%
+           0
+           (begin
+             ;; Capture a continuation w.r.t. the default prompt tag:
+             (call/cc
+              (λ (esc)
+                (dynamic-wind
+                 (λ () 0)
+                 (λ () 
+                   ;; Set a prompt for tag p1:
+                   (%
+                    1
+                    
+                    (dynamic-wind
+                     (λ () 0)
+                     ;; inside d-w, jump out:
+                     (λ () (esc 100))
+                     (λ ()
+                       (begin
+                         ;; As we jump out, capture a continuation 
+                         ;; w.r.t. p1:
+                         ((call/cc
+                           (λ (k) 
+                             (begin
+                               (set! exit-k k)
+                               (λ () 10)))
+                           1))
+                         (set! output (cons 99 output)))))
+                    (λ (x) x)))
+                 (λ ()
+                   ;; This post thunk is not in the
+                   ;;  delimited continuation captured
+                   ;; via tag p1:
+                   (set! output (cons 101 output)))))
+              0)
+             (if done?
+                 (begin
+                   (set! exit-k #f)
+                   output)
+                 (begin
+                   (set! done? #t)
+                   ;; Now invoke the delimited continuation, which must
+                   ;; somehow continue the jump to `esc':
+                   (%
+                    1
+                    (exit-k (λ () 10))
+                    (λ (x) x)))))
+           (λ (x) (x))))
+        '(<> 
+          ([output (list 99 101 99)]
+           [exit-k #f]
+           [done? #t])
+          ()
+          (list 99 101 99)))
+  (test "post thunk captures continuation that is invoked without target % (gets stuck)"
+        '(<>
+          ([output (list)]
+           [exit-k #f])
+          ()
+          (%
+           0
+           ((λ (k)
+              (abort 0
+                     (λ ()
+                       (%
+                        1
+                        (exit-k (λ () (set! exit-k #f)))
+                        (λ (x) x)))))
+            (call/cc 
+             (λ (esc)
+               (%
+                1
+                (dynamic-wind
+                 (λ () 0)
+                 (λ () (esc 100))
+                 (λ ()
+                   (begin
+                     ((call/cc
+                       (λ (k) 
+                         (begin
+                           (set! exit-k k)
+                           (λ () 10)))
+                       1))
+                     (set! output (cons 101 output)))))
+                (λ (x) x)))
+             0))
+           (λ (f) (f))))
+        (term (<>
+               ((output (list 101 101))
+                (exit-k #f))
+               ()
+               (%
+                1
+                ((cont 0
+                       ((λ (k)
+                          (abort
+                           0
+                           (λ ()
+                             (%
+                              1
+                              (exit-k (λ () (set! exit-k #f)))
+                              (λ (x) x)))))
+                        hole))
+                 100)
+                (λ (x) x)))))
+  (test "similar way to get stuck, but using the pre thunk"
+        '(<>
+          ([output (list)]
+           [exit-k #f])
+          ()
+          (%
+           0
+           ((λ (k)
+              (abort 0
+                     (λ ()
+                       (%
+                        1
+                        (exit-k (λ () (set! exit-k #f)))
+                        (λ (x) x)))))
+            (call/cc 
+             (λ (esc)
+               (%
+                1
+                (dynamic-wind
+                 (λ ()
+                   (begin
+                     ((call/cc
+                       (λ (k) 
+                         (begin
+                           (set! exit-k k)
+                           (λ () 10)))
+                       1))
+                     (set! output (cons 101 output))))
+                 (λ () (esc 100))
+                 (λ () 0))
+                (λ (x) x)))
+             0))
+           (λ (f) (f))))
+        (term (<>
+               ((output (list 101 101))
+                (exit-k #f))
+               ()
+               (%
+                1
+                (dw
+                 x_1 ; <--- beware: this is a fresh variable. Will it always be x_1?
+                 (begin
+                   ((call/cc
+                     (λ (k1)
+                       (begin
+                         (set! exit-k k1)
+                         (λ () 10)))
+                     1))
+                   (set! output (cons 101 output)))
+                 ((cont
+                   0
+                   ((λ (k)
+                      (abort
+                       0
+                       (λ ()
+                         (%
+                          1
+                          (exit-k (λ () (set! exit-k #f)))
+                          (λ (x)
+                            x)))))
+                    hole))
+                  100)
+                 0)
+                (λ (x) x)))))
+  (test "loop"
+        '(<>
+          ([counter (list 4 3 2 1 0)])
+          []
+          (%
+           0
+           ((λ (k)
+              ((λ (k2)
+                 (if (first (rest k2))
+                     ((first k2) (λ () 
+                                   (if (zero? (first counter))
+                                       (list 10 #f)
+                                       (begin
+                                         (set! counter (rest counter))
+                                         ((call/cc (λ (k) (λ () 
+                                                            (cons k (list #t))))
+                                                   0))))))
+                     (first k2)))
+               (%
+                1
+                (k (λ ()
+                     ((call/cc (λ (k) (λ () 
+                                        (cons k (list #t))))
+                               0))))
+                (λ (x) x))))
+            (%
+             1
+             ((call/cc (λ (k) (λ () k))
+                       1))
+             (λ (x) x)))
+           (λ (x) x)))
+        '(<>
+          ([counter (list 0)])
+          []
+          10))
+  (void))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Chain
+
+(define chain-defns
+  `([make
+     (λ (pre post)
+       (%
+        0
+        (dynamic-wind
+         (λ () (print pre))
+         (λ ()
+           ((call/comp
+             (λ (k) (λ () k))
+             0)))
+         (λ () (print post)))
+        (λ (x) x)))]
+    [chain
+     (λ (E_1 E_2)
+       (%
+        0
+        (E_1 (λ ()
+               (E_2 (λ ()
+                      ((call/comp
+                        (λ (k) (λ () k))
+                        0))))))
+        (λ (x) x)))]
+    [composable->replacing
+     (λ (E)
+       (%
+        0
+        (E (λ ()
+             ((call/cc
+               (λ (k) (λ () k))
+               0))))
+        (λ (x) x)))]))
+
+(define (with-chain-bindings e)
+  `((λ (one-two three-four)
+      ((λ (one-three-four-two one-NINE-three-four-two )
+         ((λ (one-two* three-four* one-three-four-two* one-NINE-three-four-two*)
+            (%
+             0
+             ,e
+             (λ (x) x)))
+          (composable->replacing one-two)
+          (composable->replacing three-four)
+          (composable->replacing one-three-four-two)
+          (composable->replacing one-NINE-three-four-two)))
+       (chain one-two three-four)
+       (chain one-two (λ (x) ((λ (z)
+                                (begin (print 9) z))
+                              (three-four x))))))
+    (make 1 2)
+    (make 3 4)))
+
+(define chain-output '(1 2 3 4 1 3 4 2 1 3 4 9 2 1 2 3 4 1 3 4 2 1 3 4 9 2))
+
+(define (chain-tests)
+  (test "check chain setup"
+        `(<>
+          (,@chain-defns)
+          []
+          ,(with-chain-bindings 10))
+        `(<>
+          (,@chain-defns)
+          [,@chain-output]
+          10))
+  (test "chain sharing"
+        `(<>
+          (,@chain-defns)
+          []
+          ,(with-chain-bindings 
+            `(one-three-four-two* (λ ()
+                                    (one-two* (λ () 0))))))
+        `(<>
+          (,@chain-defns)
+          [,@chain-output 1 3 4 2]
+          0))
+  (test "chain non-sharing"
+        `(<>
+          (,@chain-defns)
+          []
+          ,(with-chain-bindings 
+            `(one-three-four-two* (λ ()
+                                    (three-four* (λ () 0))))))
+        `(<>
+          (,@chain-defns)
+          [,@chain-output 1 3 4 2 3 4]
+          0))
+  (test "chain sharing with spliced frame"
+        `(<>
+          (,@chain-defns)
+          []
+          ,(with-chain-bindings 
+            `(one-three-four-two* (λ ()
+                                    (one-NINE-three-four-two* (λ () 0))))))
+        `(<>
+          (,@chain-defns)
+          [,@chain-output 1 3 4 9 2]
+          0))
+  (test "chain sharing with spliced frame (skipped)"
+        `(<>
+          (,@chain-defns)
+          []
+          ,(with-chain-bindings 
+            `(one-NINE-three-four-two* (λ ()
+                                         (one-three-four-two* (λ () 0))))))
+        `(<>
+          (,@chain-defns)
+          [,@chain-output 1 3 4 2]
+          0)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Run
+
+(begin
+  (basic-tests)
+  (r6rs-dw-tests)
+  (cont-tests)
+  (chain-tests)
+  (printf "All ~s tests passed.\n" tests-passed))
\ No newline at end of file
diff --git a/collects/redex/tests/run-tests.rkt b/collects/redex/tests/run-tests.rkt
index 46e05c2262..672e36f997 100644
--- a/collects/redex/tests/run-tests.rkt
+++ b/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))
        '())))