; Evaluation of this file yields an HTML document
; $Id: impromptu-shift-tr.scm 632 2005-03-23 23:27:38Z oleg $

(define Content
'(html:begin
  (Header
   (title "How to remove a dynamic prompt")
   (description "Dynamic and static delimited control operators are
equally expressible. Macro-expressing control/prompt etc. in terms of
shift/reset, and formal proofs.")
   (Date-Revision-yyyymmdd "20050323")
   (Date-Creation-yyyymmdd "20050111")
   (keywords "Scheme, control, prompt, shift, reset, delimited
continuation, abstracting control")
   (Author "Oleg Kiselyov")
   (Affiliation "")
;   (Affiliation "Fleet Numerical Meteorology and Oceanography Center,
;  Monterey, CA 93943")
   (AuthorAddress "oleg-at-okmij.org")
   (long-title ("How to remove a dynamic " "prompt: " 
		 "static and dynamic " "delimited continuation operators "
		 "are equally expressible"))
   (Links
    (start "index.html" (title "Scheme Hash"))
    (contents "../README.html")
    (prev "enumerators-callcc.html")
    (next "universally-CooL-symbols.html")
    (top "index.html")
    (home "http://pobox.com/~oleg/ftp/")))

  (body
   (navbar)
   (page-title)

    (abstract
    "We show how to remove a dynamic " (code "prompt") " (aka " (code
"reset") ") and thus to turn so-called static delimited continuation
operators (" (code "shift") "/" (code "reset") ") into dynamic ones:
" (code "control") ", " (code "control0") ", " (code "shift0") ". Our
technique extends the continuation captured by " (code "shift") " by
composing it with the previous fragments of the `stack'. Composition
of context fragments " (em "can") " be done via regular functional
composition. We thus demonstrate that all the above delimited continuation
operators are " (em "macro") "-expressible in term of each other ---
without capturing undelimited continuations and without using mutable
state. Furthermore, the operators " (code "shift") ",
" (code "control") ", " (code "control0") ", " (code "shift0") " are
the members of a single parameterized family, and the standard CPS is
sufficient to express their denotational semantics." (br)
  (indent)
       "We give the simplest Scheme implementation of the dynamic
control operators. We give a formal simulation proof that " (code
"control") " realized through " (code "shift") " indeed has its
standard reduction semantics."  )

    (TOC)

   
(Section 2 "Introduction")

(p "There have been proposed a number of delimited continuation
operators, which are concisely surveyed in " (cite "shift-to-control")
". The most well-known operators are " (code "control") "/" (code
"prompt") " (which were historically the first) and " (code "shift")
"/" (code "reset") ". It is of considerable interest both to the
implementors and the users to establish the relationship among various
control operators. In one direction, it is obvious that " (code
"shift") "/" (code "reset") " is macro-expressible " (cite
"Felleisen-expressive") " in terms of " (code "control") "/" (code
"prompt") ". Whether " (code "control") "/" (code "prompt") " and
similar operators (" (code "shift0") ", " (code "splitter") ", " (code
"spawn") ", " (code "cupto") ", etc.) can be macro-expressed in terms
of " (code "shift") "/" (code "reset") " has been for a long time an
open question " (cite "Gunter-cupto") ". The so-called static
delimited continuation operators " (code "shift") "/" (code "reset") "
have the well-known denotational (CPS) semantics " (cite "abstracting-control")
". It was unknown if " (code "control") "/" (code "prompt") " and the
other, so-called dynamic delimited continuation operators, have
likewise CPS semantics --- or they require extensions to the standard
CPS, as sometimes claimed " (cite "abstract-continuations") ".")

(p "These open questions were answered by Chung-chieh Shan " (cite
"shift-to-control") ", who for the first time showed that the dynamic
delimited continuation operators are macro-expressible in terms of
" (code "shift") "/" (code "reset") ". This paper presents another,
more uniform solution. We outline the general method of removing a
dynamic " (code "prompt") ", and so reify the operation of composing
frames of control stack. Contrary to the common belief " (cite
"abstract-continuations")
", we do not need any special primitives for composing stack fragments
other than the operation of capturing the fragments with
" (code "shift") "/" (code "reset") ", which is expressible in standard CPS.
Furthermore, we show that both
static and dynamic delimited continuation operators are the members of
a single family of delimited control, parameterized by simple
functions specifying the composition of stack fragments. We
demonstrate the simplest known Scheme implementation of " (code
"control") "/" (code "prompt") " and other delimited control operators
in terms of " (code "shift") "/" (code "reset") ". Finally, we
formally prove that " (code "control") " implemented in terms of
" (code "shift") " indeed satisfies its standard reduction
semantics. Our proof method is general and can be used for proving
other properties of delimited continuations.")

(p "The next section introduces notation and defines delimited
continuation operators under investigation. Section 3 formulates the
theorem of macro-expressivity of " (code "control") "/" (code
"prompt") " in terms of " (code "shift") "/" (code "reset") ", and
gives corollaries. One of them states that the delimited continuation
operators are the members of the same family. We then give the Scheme
implementation of the dynamic delimited continuation operators, and tests. In
Section 5, we prove the macro-expressivity theorem. The proof
demonstrates the composition of captured delimited continuations,
which is achievable without any new primitives. We then conclude.")


(Section 2 "Notation")

(p "For simplicity, we will be considering delimited continuation
operators in the context of untyped call-by-value
lambda-calculus. Generalizations to richer call-by-value calculi are
straightforward. Table " (xref "FigSyntax") " presents the syntax of
the language. We write " ($ (let ((x e1)) e2)) " as an abbreviation for
" ($ ((lambda (x) e2) e1)) ". Table " (xref "FigRed") " gives the
standard small-step operational semantics of the control-free fragment
of the language, by introducing the reduction relation " ($ (red e1
e2)) " and the evaluation context " ($ (M)) ". We write " ($ (red* e1
e2)) " for the composition of zero or more reduction
steps. Intuitively, to reduce a term " ($ e) ", we find its
representation in the form "($ (M e0)) " where " ($ e0) " is a redex
and " ($ (red e0 e1)) ".  Then "($ (red (M e0) (M e1))) ". As usual,
"($ (ren (x v) e)) " means a capture-free substitution of value " ($
v) " for variable " ($ x) " in expression " ($ e) ".")

(p "A typical proposal " (cite "shift-to-control") " for treating
delimited continuations as first class values defines syntactic forms
to set the delimiter, and to capture and reify the continuation up to
the delimiter. The delimiter setting-form is commonly called
``prompt'' or ``reset''. We will write " ($ (a-prompt ...)) " for a
general prompt, and " ($ (prompt ...)) ", " ($ (reset ...)) " etc. for
the delimiters of specific delimited continuation proposals. The
capturing and reifying form is commonly called ``shift'' or
``control''. Likewise, we will use the notation " ($ (a-control f
e)) " for a generic form and " ($ (shift f e)) ", " ($ (control f
e)) " etc. for a specific delimited continuation operator.")

(figure FigSyntax
  "Syntax"
  (table-of-expr
    
    (ebnf-def ($ e) (comment "Expression")
      (ebnf-choice
	(($ v) (comment "Value"))
	(($ ((e1 e2))) (comment "Application"))
	(($ (a-prompt e)) (comment "Set a delimiter"))
	(($ (a-control f e)) (comment "Capture and reify"))))

    (ebnf-def ($ v) (comment "Value")
      (ebnf-choice
	((ebnf-several ($ x) ($ y) ($ f) ($ g)) (comment "Variables"))
	(($ (lambda (x) e)) (comment  "Abstraction"))))

))

(figure FigRed
  "Operational Semantics"
  (table-of-expr
    
    (ebnf-def ($ (C)) (comment "(Delimited) Evaluation context")
      (ebnf-choice
	(($ Hole) (comment "Hole"))
	(($ ((C) e)))
	(($ (v (C))) (comment "Application"))))

    (ebnf-def ($ (M)) (comment "Arbitrary evaluation context")
      (ebnf-choice
	($ (C))
	(($ (M (a-prompt (C)))) (comment ""))))

    (($ (red
	 ((lambda (x) e) v)
	 (ren (x v) e)))
      (comment ("(" (greek beta) "-) Redex")))
))
      


(p "To account for delimited continuation operators, we augment the
operational semantics in Table 2. The so-called ``static'' delimited
continuation operators " (code "shift") "/" (code "reset") " are
defined by the following reduction rules.")

(peq "S1" ($ (red (M (reset v)) (M v))))
(peq "S2" ($ (red (M (reset (C (shift f e))))
	          (M (reset e'))))
  (br)
  "where " ($ (is e' (let ((f (lambda (x) (reset (C x))))) e))))

(pn "Here, " ($ (C)) " is the context that does not cross the
delimiter's (i.e., " (code "reset") ") boundary. In contrast, the
context " ($ (M)) " may do so.")

(p "All these reduction rules do not handle the case when
"($ (a-control f e))
" occurs without a dynamically enclosing " ($ (a-prompt ...)) ".  We
shall call a program that exhibits such a case to be ``stuck on
control.''  We could have followed the original Danvy and Filinski's
proposal of assuming that the entire program is enclosed in a
top-level
" ($ (a-prompt ...)) ". However, we chose to consider stuck on control
expressions to be in error --- as do several implementations of
delimited continuations, e.g., Scheme48.")

(p "The most well-known of so-called ``dynamic'' delimited
continuation operators (and historically the first delimited
continuation operators proposed) are " (code "control") "/" (code
"prompt") ":")

(peq "C1" ($ (red (M (prompt v)) (M v))))
(peq "C2" ($ (red (M (prompt (C (control f e))))
	          (M (prompt e'))))
  (br)
  "where " ($ (is e' (let ((f (lambda (x) (C x)))) e))))

(p "All various delimited continuation operators " ($ (a-control f e))
" capture the continuation up to the closest dynamically enclosing
delimiter, and reify that continuation as a function. That function,
bound to the variable " ($ f) " in the body " ($ e) " may be invoked
in the body zero or more times. The reified delimited continuation may
also be incorporated in the result of " ($ e) ", and invoked elsewhere
in the program many times.  The difference among the delimited
continuation operators emerges when either the body " ($ e) " or the
captured continuation themselves contain delimited continuation
operators. The operator " (code "shift") " encloses the captured
continuation in a delimiter, whereas " (code "control") " does
not. Therefore, in the case of " (code "shift") ", the delimited
continuation operators in " ($ (C)) " can capture only a part of that
context, but no more. In contrast, in the case of " (code "control") ",
delimited continuation operators embedded in " ($ (C)) " can capture
continuations that span far beyond that context. Other such dynamic
delimited continuation operators are possible, whose reduction rules
eliminate even more delimiters:")


(peq "S2'" ($ (red (M (reset0 (C (shift0 f e))))
	          (M e')))
  (br)
  "where " ($ (is e' (let ((f (lambda (x) (reset0 (C x))))) e))))

(peq "C2'" ($ (red (M (prompt0 (C (control0 f e))))
	          (M e')))
  (br)
  "where " ($ (is e' (let ((f (lambda (x) (C x)))) e))))


(p "Both these operators do not preserve the original delimiter,
permitting therefore the body of the delimited continuation operator
to capture a part of " ($ (M)) ". The operator " (code "shift0") " was
briefly considered in " (cite "abstracting-control-tr") ", whereas " (code
"control0") " is equivalent to a single-prompt " (code "cupto")
" " (cite "Gunter-cupto") ".")



(Section 2 "Removing" 
  " a dynamic " (code "prompt") " and expressing " (code "control") "
via " (code "shift"))

(p
  "We introduce a sum (discriminated union) datatype " (code "H") ", similar to
Haskell's " (code "Either") " datatype:")

(p (ebnf-def ($ H)
     (ebnf-choice
       ($ (H v1 v2))
       ($ (HV v))))
)

(pn "Such a datatype is trivially realized in our calculus (cf., one of
the Scheme implementations below): constructors " ($ H) " and " ($ HV) "
become regular functions that yield abstractions. Slightly informally,
we will call " ($ (H v1 v2)) " and " ($ (HV v)) " values themselves.")


(p
  "We introduce the following source-to-source transformation:")

(peq "PR"
  (align-left
  ($ (expressed-as
       (prompt e)
       (h (reset (HV e)))))
  ($ (expressed-as 
       (control f e)
       (shift f' (H (compose h' f') (lambda (f) e))))))
  )

(pn "where the functions " ($ "h") " and " ($ "h'") " are defined
as follows:")

(peq "H"
  (align-left
    ($ (is (h (H f x))
         (prompt (x f))))
    ($ (is (h (HV x)) x)))
)

(peq "H'"
  (align-left
    ($ (is (h' (H f x))
	 (shift g (H (compose h' g f) x))))
    ($ (is (h' (HV x)) x))))


(p "We also introduce the following transformation rule:")

(peq "PR1"
  ($ (expressed-as
       (M (C e))
       (equiv (M (h' (reset (HV (C e)))))
	         (M (B (C e))))))
  )

(pn "The notation " ($ (B e)) " is a mere shorthand for
" ($ (h' (reset (HV e)))) ". The context " ($ (C)) " in (PR1) may be
empty.")

(p "It is straightforward to extend (PR) to expressions and
contexts. We will write " ($ (T n e *e)) " for the transformation of
an expression " ($ e) " yielding " ($ *e) " by applying (PR) and " ($
n) "-times the rule (PR1). When we apply the rule (PR1), the place to
insert " ($ (B)) " is chosen non-deterministically. If the number of
applications of (PR1) is irrelevant, we may write simply " ($ (T e
*e)) ". The properties of the transformation are summarized by the
following Theorem.")


(p
  "Theorem 1. " (code "Prompt") " and " (code "control") " are
macro-expressible in terms of " (code "shift") " and " (code "reset")
": applying the transformation (PR) to a program yields an
observationally equivalent program. In particular, the 
transformations (PR) and (PR1) have the following properties:")

(peq "T1"
  ($ *v) " is a value")
(pn "That is, values are transformed to values.")

(peq "T2"
  ($ (T (M e) (*M *e))))

(pn "Transformations (PR) and (PR1) are context independent. This is
another statement of macro-expressibility.")

(peq "T3"
  "if " ($ (red e1 e2)) " and " ($ (T n e1 *e1)) " then "
  ($ (exists m (T m e2 *e2))) " and " ($ (red* *e1 *e2)))

(pn "That is, the transformed code simulates reductions. In particular:")

(peq "T4"
  "if " ($ (red* e v)) " then " ($ (T 0 e *e)) " and " ($ (red* *e *v)))

(pn "and if reductions of " ($ e) " diverge, so do reductions of " ($
*e) ".")




(Section 3 "One family of delimited continuation operators")

(p
  "Corollary 1. Both static and dynamic delimited continuation
operators are the members of a single family " ($ (greset hr e)) " and
" ($ (gshift hs f e)) " parameterized by functions " (code "hr") " and
" (code "hs") ":")

(table
(tr
 (td
   (peq #f
     (align-left
       ($ (is (reset e) (greset hr-stop e)))
       ($ (is (shift f e) (gshift hs-stop f e)))
       ))
   )
  (td
    (peq #f
      (align-left
	($ (is (prompt e) (greset hr-stop e)))
	($ (is (control f e) (gshift hs-prop f e)))))
    ))
(tr
  (td
    (peq #f
      (align-left
	($ (is (reset0 e) (greset hr-prop e)))
	($ (is (shift0 f e) (gshift hs-stop f e)))))
    )
  (td
    (peq #f
      (align-left
	($ (is (prompt0 e) (greset hr-prop e)))
	($ (is (control0 f e) (gshift hs-prop f e)))))
    )))

(p "where " ($ (greset hr e)) " and " ($ (gshift hs f e)) " and the
functions " ($ hr-stop) ", " ($ hs-stop) ", " ($ hr-prop) ", and " ($
hs-prop) " are themselves macro-expressible in terms of " (code
"shift") " and " (code "reset")
":")

(peq #f
  (align-left
    ($ (expressed-as (greset hr e)
	 (hr (reset (HV e)))))
    ($ (expressed-as (gshift hs f e)
	 (shift f' (H (compose hs f') (lambda (f) e)))))
    ))

(peq #f
  (align-left
    ($ (is (hr-stop (H f x))
	 (greset hr-stop (x f))))
    ($ (is (hr-stop (HV x)) x))
    ($ (is hs-stop hr-stop))))

(peq #f
  (align-left
    ($ (is (hr-prop (H f x)) (x f)))
    ($ (is (hr-prop (HV x)) x))
))

(peq #f
  (align-left
    ($ (is (hs-prop (H f x))
	 (shift g (H (compose hs-prop g f) x))))
    ($ (is (hs-prop (HV x)) x))
))



(Section 3 "Fischer-style" " CPS transform of dynamic delimited
continuation operators")

(p
  "Corollary 2. Dynamic delimited continuation operators " (code
"control") "/" (code "prompt") " and the others have a simple
denotational semantics and a Fischer-style " (cite "FischerCPS") " CPS
transform, induced by the CPS transform of " (code "shift") "/" (code
"reset") ".")



(Section 2 "Scheme" " implementation of the dynamic delimited continuation
operators")

(p "We shall treat the sum datatype " (code "H") " as an abstract
datatype with two constructors " (code "H") " and " (code "HV") " and
a deconstructor " (code "case-H") ". The datatype can be realized by
the following pure lambda-terms in our calculus:")

(verbatim
  "; Constructors"
  "(define (H a b)"
  "  (lambda (on-h)"
  "    (lambda (on-hv)"
  "      ((on-h a) b))))"
  ""
  "(define (HV v)"
  "  (lambda (on-h)"
  "    (lambda (on-hv)"
  "      (on-hv v))))"
  ""
  "; Deconstructor"
  "(define-syntax case-H"
  "  (syntax-rules ()"
  "    ((case-H e"
  "       ((f x) on-h)"
  "       (v on-hv))"
  "     ((e (lambda (f) (lambda (x) on-h)))"
  "       (lambda (v) on-hv)))))"
  )

(p "Alternatively, we may, potentially more efficiently, implement the
" (code "H") " datatype via Scheme's indiscriminated union:")

(verbatim
  "(define H-tag (list 'H-tag))"
  ""
  "; Constructors"
  "(define (H a b) (cons H-tag (cons a b)))"
  "(define-syntax HV                       ; just the identity"
  "  (syntax-rules ()"
  "    ((HV v) v)))"
  ""
  "; Deconstructor"
  "(define-syntax case-H"
  "  (syntax-rules ()"
  "    ((case-H e"
  "       ((f x) on-h)"
  "       (v on-hv))"
  "     (let ((val e))"
  "       (if (and (pair? val) (eq? (car val) H-tag))"
  "         (let ((f (cadr val)) (x (cddr val))) on-h)"
  "         (let ((v val)) on-hv))))))"
  )


(p "The family of the delimited continuation operators is implemented
by the straightforward transcription into Scheme of the expressions in 
Corollary 1.")

(verbatim
  "(define-syntax greset"
  "  (syntax-rules ()"
  "    ((greset hr e) (hr (reset (HV e))))))"
  ""
  "(define-syntax gshift"
  "  (syntax-rules ()"
  "    ((gshift hs f e)"
  "      (shift f* (H (lambda (x) (hs (f* x))) (lambda (f) e))))))"
  ""
  "(define (hr-stop v)"
  "  (case-H v"
  "    ; on-h"
  "    ((f x) (greset hr-stop (x f)))"
  "    (v v))) ; on-hv"
  ""
  "(define hs-stop hr-stop)"
  ""
  "(define (hr-prop v)"
  "  (case-H v"
  "    ; on-h"
  "    ((f x) (x f))"
  "    ; on-hv"
  "    (v v)))"
  ""
  ""
  "(define (hs-prop v)"
  "  (case-H v"
  "    ; on-h"
  "    ((f x)"
  "      (shift g"
  "        (H (lambda (y) (hs-prop (g (f y)))) x)))"
  "    ; on-hv"
  "    (v v)))"
  )


(p "Using the operational semantics of " (code "shift") "/" (code
"reset") ", it is easy to see that " ($ (greset hr-stop e)) " is
"($ (reset e)) ", and " ($ (gshift hs-stop f e)) " is itself
"($ (shift f e)) ".")


(p "The operators " (code "prompt") " and " (code "control") ", in
particular, have the following simple implementation:")


(verbatim
  "(define-syntax prompt"
  "  (syntax-rules ()"
  "    ((prompt e) (greset hr-stop e))))"
  ""
  "(define-syntax control"
  "  (syntax-rules ()"
  "    ((control f e) (gshift hs-prop f e))))"
  )

(p "It is patently clear then that " (code "control") " and " (code "prompt")
" are indeed " (em "macro") "-expressible in terms of " (code "shift") " and
" (code "reset") ".")


(Section 3 "Tests")

"The tests run on Scheme48, with its built-in implementation of
" (code "shift") " and " (code "reset") "."


(small-verbatim
  "(reset (let ((x (shift f (cons 'a (f '()))))) (shift g x)))"
  "; ==> '(a)"
  "(prompt (let ((x (control f (cons 'a (f '()))))) (control g x)))"
  "; ==> '()"
  ""
  "(prompt ((lambda (x) (control l 2)) (control l (+ 1 (l 0)))))"
  "; ==> 2"
  "(prompt (control f (cons 'a (f '()))))"
  "; ==> '(a)"
  "(prompt (let ((x (control f (cons 'a (f '())))))"
  "          (control g (g x))))"
  "; ==> '(a)"
  "(prompt0 (prompt0 (let ((x (control0 f (cons 'a (f '())))))"
  "                     (control0 g x))))"
  "; ==> '()"
  "; prompt0 is the same as reset0"
  "(prompt0 (cons 'a (prompt0 (shift0 f (shift0 g '())))))"
  "; ==> '()"
  "(prompt0 (cons 'a (prompt0 (prompt0 (shift0 f (shift0 g '()))))))"
  "; ==> '(a)"
  ""
  "; Example by Chung-chieh Shan"
  "(prompt (begin (display (control f (begin (f 1) (f 2))))"
  "               (display (control f (begin (f 3) (f 4))))))"
  "; ==> 132342344234442344442344444234444442344444442344444444234...."
  )

(Section 2 "Proof" " of Theorem 1")

(p "In this section we formally prove that " (code "control")
"/" (code "prompt") " operators realized in terms of " (code "shift")
"/" (code "reset") ", Theorem 1, satisfy their standard reduction
semantics, eqs. (C1-C2). To be precise, we prove that reductions in
the translated language (" (code "control") "/" (code "prompt") "
expressed via " (code "shift") "/" (code "reset") ") simulate
reductions in the original language. We must stress that our proof
elucidates how the context fragment compositions (implicit in the original
language with " (code "control") "/" (code "prompt") ") become
" (em "explicit") ", as functional compositions, in the translated
language.")

(p "Properties (T1) and (T2) are obvious. Before we prove the
simulation property (T3), we consider the following Lemma. ")

(p "Lemma 1.")
(peq #f
  ($ (red* (B v) v)))

(p "The proof is straightforward from the definition of " ($ (B e)) " as
" ($ (h' (reset (HV e)))) ", the fact that " ($ (HV v)) " is also a
value, the definition of " ($ h') " in eq. (H'), and eq. (S1). The Lemma
is easily generalized to arbitrary sequences of " ($ (B)) ".")

(p "The notation " ($ (red e1 e2)) " describes three different
reductions: the " (greek beta) "-reduction in Table " (xref "FigRed")
" and control reductions (C1) and (C2). We shall consider all three
reductions in turn.")

(p "In order for the " (greek beta) "-reduction to apply, the
expression " ($ e1) " must have the form " ($ (M ((lambda (x) e1')
v))) ". Thus we have:")

(peq #f
 (align-left
   ($ (equiv e1 (M ((lambda (x) e1') v))))
   ($ (T n "" (*M ((B (lambda (x) *e1')) (B *v)))))
   (explain "Lemma 1")
   ($ (red* "" (*M ((lambda (x) *e1') *v))))
   ($ (red "" (*M (ren (x *v) *e1'))))))

(p "On the other hand,")
(peq #f
 (align-left
   ($ (equiv e1 (M ((lambda (x) e1') v))))
   ($ (red "" (M (ren (x v) e1'))))
   ($ (T m "" (*M (ren (x *v) *e1'))))
))

(pn "for some " ($ m) ".")

(p "Another possible reduction is (C1). It applies when the expression
in question has the form " ($ (M (prompt v))) ". Therefore,")

(peq #f
 (align-left
   ($ (equiv e1 (M (prompt v))))
   ($ (T n "" (*M (h (reset (HV (B *v)))))))
   (explain "Lemma 1")
   ($ (red* "" (*M (h (reset (HV *v))))))
   (explain "equations (S1) and (H)")
   ($ (red* "" (*M *v)))
))

(pn "The latter expression is obviously a transform image from
" ($ (M v)) ", which is the result of one-step reduction of " ($ e1)
".")

(p "Lemma 2.")
(peq #f
  ($ (red* (B (C (shift g (H (compose h' g f') (lambda (f) e)))))
           (shift g (H (lambda (x) (h' (g (B (C (f' x))))))
		       (lambda (f) e)))))
)

(pn "Informally, the translation image of " ($ (control f e)) " can be
lifted out of " ($ (B (C))) " with the latter context fragment added
to the captured continuation.  Indeed,")

(peq #f
 (align-left
  ($ (B (C (shift g (H (compose h' g f') (lambda (f) e))))))
  (explain "Definition of " ($ (B)))
  ($ (equiv ""
       (h' (reset (HV (C (shift g (H (compose h' g f') (lambda (f) e)))))))))
  (explain "(S2), along with the fact " ($ (HV e)) " may be subsumed ")
  (explain "as a part of a non-reset-crossing context " ($ (C)))
  ($ (red ""
       (h' (reset (let ((g (lambda (x) (reset (HV (C x))))))
		  (H (compose h' g f') (lambda (f) e)))))))
  (explain ($ (H a b)) " is a value, apply (S1) and then (H')")
  ($ (red* ""
       (let ((g (lambda (x) (reset (HV (C x))))))
	 (shift g' (H (compose h' g' h' g f') (lambda (f) e))))))
  ($ (equiv ""
       (shift g' (H (lambda (x) (h' (g' (h' (reset (HV (C (f' x))))))))
		    (lambda (f) e)))))
  ($ (equiv ""
       (shift g' (H (lambda (x) (h' (g' (B (C (f' x))))))
		    (lambda (f) e)))))
))

(p "The last reduction to consider, (C2), applies when the expression
" ($ e1) " has the form of " ($ (M (prompt (C (control f e)))))
". When we transform that expression, we have to keep in mind that the
transform of a non--delimiter-crossing context " ($ (C)) " may, in
general, be a delimiter-crossing context: a potentially inserted
" ($ (B)) " contains the delimiter, " (code "reset") ".  We first consider the
case, however, when the image of the context " ($ (C)) " is a
non--delimiter-crossing context " ($ (*C)) ". We can then write:")

(peq "*"
 (align-left
   ($ (equiv e1 (M (prompt (C (control f e))))))
   ($ (T n "" (*M (h (reset (HV (*C 
		  (shift f' (H (compose h' f') (lambda (f) *e))))))))))
  (explain "(S2), along with the fact " ($ (HV e)) " may be subsumed ")
  (explain "as a part of a non-reset-crossing context " ($ (*C)))
  ($ (red "" (*M (h (reset
		       (let ((f' (lambda (x) (reset (HV (*C x))))))
		       (H (compose h' f') (lambda (f) *e))))))))
  (explain ($ (H a b)) " is a value, apply (S1) and then (H)")
  ($ (red* "" (*M (h (reset (HV
		(let ((f' (lambda (x) (reset (HV (*C x))))))
		  ((lambda (f) *e) (compose h' f')))))))))
  ($ (equiv "" (*M (h (reset (HV
		(let ((f (lambda (x) (h' (reset (HV (*C x))))))) *e)))))))
  (explain "definition of " ($ (B)))
  ($ (equiv "" (*M (h (reset (HV
		(let ((f (lambda (x) (B (*C x))))) *e)))))))
))

(p "On the other hand,")
(peq #f
 (align-left
   ($ (equiv e1 (M (prompt (C (control f e))))))
   (explain "apply (C2)")
   ($ (red "" (M (prompt (let ((f (lambda (x) (C x)))) e)))))
   ($ (T m "" (*M (h (reset (HV (let ((f (lambda (x) (B (*C x))))) *e)))))))
))

(pn "for some " ($ m) " --- actually, for " ($ (is m "n+1")) ".")

(p "Finally, we consider the general case when the image of the
context " ($ (C)) " does include " ($ (B)) ". We can always 
decompose " ($ (C)) " into " ($ (C2 (C1))) " so that ")

(peq "D"
  ($ (equiv (C) (C2 (C1))))
  ($ (T n "" (*M2 (B (*C1)))))
)

(pn "where either of the contexts " ($ (C1)) " or " ($ (C2)) " may be
empty and " ($ (T m (C2) (*M2))) " for some " ($ m) " smaller than " ($
n) ". This equation merely expresses the fact of the insertion of
" ($ (B)) ". It follows then:")

(peq "**"
 (align-left
   ($ (equiv e1 (M (prompt (C (control f e))))))
   ($ (T n "" (*M (h (reset (HV (*M2 (B (*C1 
		  (shift f' (H (compose h' f') (lambda (f) *e))))))))))))
   (explain "Lemma 2")
   ($ (red* "" (*M (h (reset (HV (*M2
		  (shift f' (H (lambda (x) (h' (f' (B (*C1 x)))))
			       (lambda (f) *e))))))))))
))

(p "If the context " ($ (*M2)) " does not cross the delimiter boundary
--- that is, contains no " ($ (B)) ", we can denote it as " ($ (*C2)) "
and apply (*), obtaining ")

(peq #f
  ($ (*M (h (reset (HV
		(let ((f (lambda (x) (B (*C2 (B (*C1 x))))))) *e))))))
)

(pn "which is again the image of ")
(peq #f
  ($ (M (prompt (let ((f (lambda (x) (C x)))) e)))))

(pn "keeping in mind that " ($ (equiv (C e) (C2 (C1 e)))) " by (D). If,
however, " ($ (*M2)) " did contain " ($ (B)) ", we can apply (D) 
and (**) one more time. We recall that " ($ (T m (C2) (*M2)))
" with " ($ m) " strictly less than " ($ n) ", thus our procedure must
terminate.")

(p "Property (T4) is a simple consequence of (T3) and the fact " ($ (T
n v (red* e *v))) ", which follows from Lemma 1. We also observe that
the transform of a stuck-on-control expression is itself stuck on
control.")


 (Section 2 "Conclusions")

 (p "We have introduced a general method of removing a dynamic prompt,
so that delimited continuation operators may capture continuations
beyond that prompt. Contrary to the previously held beliefs, composing
of contexts can be done by the regular functional composition. No
primitives other than the operation of capturing fragments of the
context with " (code "shift") "/" (code "reset") " are
needed. Therefore, the standard CPS is sufficient for giving
denotational semantics of the dynamic delimited continuations, and the
dynamic delimited continuation operators are just as expressible as
" (code "shift") "/" (code "reset") ". We thus confirm the results of
" (cite "shift-to-control") " using a more general framework and
giving the formal proof.")

 (p "Our technique of removing a dynamic prompt is rather general and
thus can be used for the design of many other delimited control
operators, which permit capturing the continuation up to an arbitrary
(not necessarily the closest one) enclosing delimiter. It becomes
entirely up to the user which delimiters to skip and how the captured
frames are to be composed or used separately. The essence of our
technique is reifying the control effect (or the absence of it) into
regular values, instances of the datatype " (code "H") ". Therefore,
the user program has the ability to determine which control effects, if
any, had occurred during the evaluation of a piece of code --- and act
accordingly. Our technique is thus reminiscent of ``referring to the
central authority'' approach by Cartwright and Felleisen " (cite
"extensible-denot") ". However, instead of one central authority, we
have bureaucracy --- a sequence of authorities. A particular
authority may either fulfill a request for service, or pass it, after
perhaps modifying it, up the (dynamic) chain of hierarchy.")

 (p "Practically, we have shown that both static and dynamic delimited
continuation operators are the members of a single family of delimited
control, parameterized by simple functions specifying the composition
of stack fragments. This gives rise to the simplest Scheme realization
of the delimited control operators in terms of " (code "shift")
"/"(code "reset") ".")


 (Acknowledgment "Acknowledgments")
 (p
   "This paper owes its existence to " (cite "shift-to-control")
". The inspiration of the latter cannot be over-emphasized. I am very
grateful to Chung-chieh Shan for many insightful discussions. I would
like to thank Amr A. Sabry for his encouragement and shepherding, and
Daniel P. Friedman for valuable comments.")

 (BibReferences)


   (footer)


)))

;(pp Content)


;------------------------------------------------------------------------
;			SXML->LaTeX conversion

; Given a string, check to make sure it does not contain characters
; such as '_' or '&' that require encoding. Return either the original
; string, or a list of string fragments with special characters
; replaced by appropriate "escape sequences"

(define string->goodTeX
  (make-char-quotator
   '((#\# . "\\#") (#\$ . "\\$") (#\% . "\\%") (#\& . "\\&")
     (#\~ . "\\textasciitilde{}") (#\_ . "\\_") (#\^ . "\\^")
     (#\\ . "$\\backslash$") (#\{ . "\\{") (#\} . "\\}"))))


; Place the 'body' within the LaTeX environment named 'tex-env-name'
; options is a string or a list of strings that specify optional or
; mandatory parameters for the environment
; Return the list of fragments (suitable for SRV:send-reply)
(define (in-tex-env tex-env-name options body)
  (list "\\begin{" tex-env-name "}" options nl
	body
	"\\end{" tex-env-name "}" nl))

(define (>list a) (if (or (pair? a) (null? a)) a (list a)))

; Typesetting an expression in our calculus
; An expression may be `simple', like variable, or
; `complex', like an application.
; A complex expression is usually typeset with parentheses around it;
; A simple expression is typeset without parentheses.
; Here's the complications: 
; first of all, some complex-looking expressions like `context applications'
; (C x) are considered simple.
; Furthermore, complex expressions can also be typeset without surrounding
; parentheses, e.g., if such an expression appears at the `top' level,
; or as an argument to a `context application', `reset', etc.
; So, only an expression knows if it is simple or complex.
; Only the context knows if the enclosing parentheses are required or not.
; So, an expression, to properly typeset itself, must be aware of its
; context. Ken: ``give an expression access to its own context.''
;
; Complications:
;  (f x) is a function applications and should be typeset as
;  "f x" or "(f x)"
;  (C x) is a `context application' and should be typeset as
;  "C[x]"
; One may think it's easy to see which is which, based on the `head'
; of the expression. Alas, it is more complex, because of possible
; `decorations': we can write (f1 x), which is an abbreviation for
; ((sub f "1") x)
; as well as (C1 x), which is an abbreviation of ((sub C "1") x)
; So, the processing becomes less clear.
; Additional complication: when we typeset "reset0" as
; "\\mathbf{reset_0}" we wish the subscript to be within the decoration.
; OTH, when we typeset (M1 x) as "\\mathcal{M}_1[x]", we really
; need the subscript to be outside (otherwise, the subscript is mangled).
;
; During evaluation, we pass along the env, with the following
; dynamic bindings
;  &paren -- boolean flag if the context suggest we need enclosing paren
;  &decor -- list of decorations
;
; We could have used another binding: &ctx 
; to handle ``macros''. However, we do that in a different way,
; by returning a function.


(define (typeset-exp tag exp)

  (define (context-notation letter)
    (lambda (env)
      (let ((kw (decorate env `("\\mathcal{",letter"}"))))
	(h-simple #t
	  (lambda e
	    `(,kw "\\!\\left[" ,e "\\right]"))))))


  (define init-env
    `((Hole . "[\\enspace]")
      (hr-stop . "hr_{stop}")
      (hs-stop . "hs_{stop}")
      (hr-prop . "hr_{prop}")
      (hs-prop . "hs_{prop}")
      (HV . "\\mathsf{HV}\\,")
      (H . "\\mathsf{H}\\,")
      (lambda 
	. ,(lambda (_)
	     (h-simple #t
	       (lambda (formal body)
		 (list "\\lambda " formal "." body)))))
      (let
	. ,(lambda (_)
	     (lambda (envp bindings body)
	       (let ((env (ext-paren envp #f)))
		 (add-paren envp
		   (list "\\mathrm{let}\\,"
		     (handle env (caar bindings)) "\\!=\\!"
		     (handle env (cadar bindings))
		     "\\,\\mathrm{in}\\," (handle env body)))))))

      ; contexts
      (C . ,(context-notation "C"))
      (M . ,(context-notation "M"))
      (B . ,(context-notation "B"))

      ; Transformation 
      ; (T n e e1) or (T e e1)
      (T . ,(lambda (_)
	     (lambda (env . args)
	       (let*-values
		 (((n args)
		    (if (= 3 (length args)) (values (car args) (cdr args))
		      (values #f args))))
		 (apply 
		   (h-simple #f
		     (lambda (from to)
		       `(,from 
			 ,(if n `("\\stackrel{",n"}{\\rightharpoonup}")
			    "\\rightharpoonup")
			  "\\," ,to)))
		   env args)))))
       
	
      (a-prompt . ,(lambda (_)
	(h-simple #f
	       (lambda (e) (list "D[" e "]")))))

      (prompt
	. ,(lambda (env)
	     (let ((kw (list "\\mathbf{" (decorate env "prompt") "}\\;")))
	       (h-simple #t
		 (lambda (e) (list kw e))))))

      (reset
	. ,(lambda (env)
	     (let ((kw (list "\\mathbf{" (decorate env "reset") "}\\;")))
	       (h-simple #t
		 (lambda (e) (list kw e))))))

      (greset
	. ,(lambda (env)
	     (let ((kw 
		     (lambda (hr)
		       (list "\\mathbf{"
			 (decorate env 
			   (list "reset_\\mathrm{" hr "}")) "}\\;"))))
	       (h-simple #t
		 (lambda (hr e) (list (kw hr) e))))))

      (a-control
	. ,(lambda (_)
	     (h-simple #t (lambda (f e) `("\\eta{}" ,f "." ,e )))))

      (control
	. ,(lambda (env)
	     (let ((kw (list "\\mathbf{" (decorate env "control") "}\\;")))
	       (h-simple #t (lambda (f e) (list kw f "." e))))))

      (shift
	. ,(lambda (env)
	     (let ((kw (list "\\mathbf{" (decorate env "shift") "}\\;")))
	       (h-simple #t (lambda (f e) (list kw f "." e))))))

      (gshift
	. ,(lambda (env)
	     (let ((kw 
		     (lambda (hs)
		       (list "\\mathbf{"
			 (decorate env 
			   (list "shift_\\mathrm{" hs "}")) "}\\;"))))
	       (h-simple #t
		 (lambda (hs f e) (list (kw hs) f "." e))))))


       (red 
	 . ,(lambda (_)
	      (h-simple #f
		(lambda (from to)
		  `(,from "\\,\\vartriangleright\\," ,to)))))

       (red* 
	 . ,(lambda (_)
	      (h-simple #f
		(lambda (from to)
		  `(,from "\\,\\vartriangleright^{*}\\," ,to)))))

       (is 
	 . ,(lambda (_)
	      (h-simple #f
		(lambda (from to)
		  `(,from "\\,=\\;\\," ,to)))))

       (then
	 . ,(lambda (_)
	      (h-simple #f
		(lambda (expr)
		  `("\\;\\Rightarrow\\;" ,expr)))))

       (expressed-as
	 . ,(lambda (_)
	      (h-simple #f
		(lambda (from to)
		  `(,from "\\,\\Longrightarrow\\," ,to)))))

       (equiv
	 . ,(lambda (_)
	      (h-simple #f
		(lambda (from to)
		  `(,from "\\,\\equiv\\," ,to)))))


      (ren
	. ,(lambda (_)
	     (lambda (env binding exp)
	       (let ((env (ext-paren env #f)))
		 (list (handle env exp)
		   "[" 
		   (handle env (cadr binding))
		   "/" (handle env (car binding)) "]")))))

       (compose 
	 . ,(lambda (_)
	      (h-simple #t (lambda elems
			  (list-intersperse elems "\\,\\cdot\\,")))))

       (exists
	 . ,(lambda (_)
	      (h-simple #t
		(lambda (var term)
		  `("\\exists " ,var ".\\:" ,term)))))


     ))

  ; handle an atomic expression
  (define (handle-atom env atom)
    (if (not (symbol? atom)) atom
      (let ((resolved (lookup-def atom env #f)))
	(if resolved
	  (if (procedure? resolved) (handle env (resolved env))
	    (decorate env resolved))
	  ; check for embdedded decorations
	  (let* ((str (symbol->string atom))
		 (len (string-length str)))
	    (cond
	      ((zero? len) (decorate env str)) ; empty string
	      ((char-numeric? (string-ref str (dec len)))
		(handle-atom (ext-decoration env 
			       `(>right "_{" ,(string-ref str (dec len))
				  "}"))
		  (string->symbol (substring str 0 (dec len)))))
	      ((char=? #\' (string-ref str (dec len)))
		 (handle-atom (ext-decoration env '(>right "'"))
		   (string->symbol (substring str 0 (dec len)))))
	      ((char=? #\* (string-ref str 0)) ; transformation marker
		(handle-atom (ext-decoration env '(>in "\\overline"))
		  (string->symbol (substring str 1 len))))
	      (else
		(decorate env str))))))))


  (define (ext-decoration env decoration)
    (cons
      (cons '&decor
	(cons decoration
	  (cond ((assq '&decor env) => cdr) (else '()))))
      env))

  (define (ext-paren env flag)
    (cons (cons '&paren flag) env))

  (define (add-paren env exp)
    (if (lookup-def '&paren env #f)
      (list "(" exp ")")
      exp))

  (define (decorate env x)
    (let loop ((decor (cond ((assq '&decor env) => cdr) (else '())))
	       (res x))
      (if (not (pair? decor)) res
	(let* ((decor1 (car decor)) ; must be (kwd args)
	       (kwd (car decor1))
	       (args (cdr decor1)))
	  (loop (cdr decor)
	    (case kwd
	      ((>right) (cons res args))
	      ((>in) (list args "{" res "}"))
	      (else (error "invalid decoration: " decor1))))))))

  ; handle (a b ...) where 'a' may be a `macro'
  (define (handle-app envp app)
    (let ((env (ext-paren envp #t))) ; use paren
      (let ((hd (handle env (car app))))
	(if (procedure? hd)
	  (apply hd envp (cdr app))
	  (add-paren envp
	    (cons hd (map (lambda (x) (handle env x)) (cdr app))))))))

  (define (handle env exp)
    (if (pair? exp) (handle-app env exp) (handle-atom env exp)))

  ; For use within init-env
  ; Produce a complex-result? expression whose constituents are `simple'
  ; (that is, unparenthesized expressions)
  (define (h-simple complex-result? handler)
    (lambda (envp . args)
      (let ((env (ext-paren envp #f)))
	(add-paren (if complex-result? envp env)
	  (apply handler (map (lambda (x) (handle env x)) args))))))


  ; get the ball rolling
  (let ((res (handle init-env exp)))
    (assert (not (procedure? res)))
    (cerr res nl)
    (list "$" res "$"))
)


(define (generate-TEX Content)

 (SRV:send-reply
  (pre-post-order Content
   `(
			; General conversion rules
     (@
      ((*default*       ; local override for attributes
	. ,(lambda (attr-key . value) (cons attr-key value))))
      . ,(lambda (trigger . value) (list '@ value)))
     (*default* . ,(lambda (tag . elems)
		       (cerr "Tag: " tag " ignored" nl)
		       '()))
     (*text* . ,(lambda (trigger str) 
		  (if (string? str) (string->goodTeX str) str)))
     (n_		; a non-breaking space
      . ,(lambda (tag . elems)
	   (list "~" elems)))

     (html:begin
      . ,(lambda (tag . elems)
	   (list
	    "% SXML->TEX created this file" nl
	    "\\documentclass[english,12pt]{article}" nl
	    "\\usepackage{babel}" nl
	    "\\usepackage{amssymb}" nl
	    "\\usepackage{psfig}" nl

	     ;"\\let\\citeauthoryear\\relax" nl
	     ;"\\let\\iint\\relax" nl
	     ;"\\let\\iiint\\relax" nl
	     ;"\\let\\bibhang\\relax" nl
	     "\\usepackage[numbers,sort&compress]{natbib1}" nl
	     ;"\\makeatletter \\let\\@biblabel\\@empty \\makeatother" nl
	     "\\newcommand\\bibfont{\\footnotesize}" nl
	     "\\providecommand\\newblock{}" nl
	     ;"\\renewcommand\\bibnumfmt[1]{\\releft#1\\redot\\reright}" nl
	     "\\setlength{\\bibsep}{0pt}" nl

	    ;"\\usepackage{graphicx}" nl
	    ;"\\usepackage[latin1]{inputenc}" nl
	    ;"\\usepackage{times}" nl
	    ;"\\pagestyle{empty}" nl

	    "\\makeatletter" nl

	     "%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands." nl
; 	     " \\LyXsNoCenterfalse"
; 	     " \\newcommand{\\lyxendslide}[1]{"
; 	     "    \\ifLyXsNoCenter%"
; 	     "         \\vfill%"
; 	     "    \\fi%"
; 	     "    \\ifcase \\value{slidetype}%"
; 	     "         \\or % no action for 0"
; 	     "         \\end{slide} \\or%"
; 	     "         \\end{overlay} \\or%"
; 	     "         \\end{note}%"
; 	     "    \\fi%"
; 	     "    \\setcounter{slidetype}{0}"
; 	     "\\visible"
; 	     " }"
	     " \\newenvironment{lyxcode}" nl
	     "   {\\begin{list}{}{" nl
;	     "     \\setlength{\\rightmargin}{\\leftmargin}" nl
	     "     \\raggedright" nl
	     "     \\setlength{\\itemsep}{-5pt}" nl
	     "     \\setlength{\\parsep}{-3pt}" nl
	     "     \\normalfont\\ttfamily}%" nl
	     "    \\item[]}" nl
	     "   {\\end{list}}" nl

; 	     "            % Uncomment to print out only slides and overlays"
; 	     "            %"
; 	     "            %\\onlyslides{\\slides}"
; 	     "            "
; 	     "            % Uncomment to print out only notes"
; 	     "             %"
; 	     "             %\\onlynotes{\\notes}"

	    "\\makeatother" nl
	    "\\sloppy" nl
	    "\\newcommand{\\minitab}[2][l]{\\begin{tabular}{#1}#2\\end{tabular}}" nl

	    nl
	    elems
	    )))

     (Header		; It is just the placeholder for the meta-information
      *preorder*
      . ,(lambda (tag . headers) '()))

     (body
      . ,(lambda (tag . elems)
	   (in-tex-env "document" '() elems)))

     (page-title	
      . ,(lambda (tag) 
	   (let* ((header-parms (find-Header Content))
		  (title (lookup-def 'long-title header-parms #f))
		  (authors (lookup-def 'Author header-parms #f))
		  (affiliations 
				(lookup-def 'Affiliation header-parms #f))
		  (emails 
			   (lookup-def 'AuthorAddress header-parms #f)))
	     (list
	       "\\thispagestyle{empty}" nl
	       "\\setcounter{page}{0}" nl
	       (in-tex-env "center" '()
		 (list
		 "\\Large" nl
		 (in-tex-env "picture" '()
		   (list
		   "(0,0)" nl
		 "\\put(0,54){\\makebox[0pt]{\\sc Technical Report No. 611}}" nl
		  ))
		 nl "\\vspace*{\\fill}" nl nl
		 "\\huge" nl
		 (map (lambda (str)
			(list "{\\textbf{" str "}}\\\\" nl))
		   (>list title)) nl
		 nl "\\vspace*{\\baselineskip}"nl nl
		 "\\large by " "\\\\"
		 "\\Large{}" 
		 "\\vspace*{\\baselineskip}" nl
		 (list-intersperse (>list authors) "\\\\") 
		 "$^*$"
		   nl nl

		 "\\vspace*{\\baselineskip}" nl
		 "March 2005" nl nl 
		 "\\vspace*{\\fill}" nl nl
		 "\\Large" nl
		 "\\makebox[0pt]{\\psfig{figure=IUseal.ps,width=2in}}" nl nl ; "\\\\" nl

		 (in-tex-env "picture" '()
		   (list "(0,0)" nl
		 "\\put(0,-18){\\makebox[0pt]{\\sc Computer Science Department}}" nl
		 "\\put(0,-36){\\makebox[0pt]{\\sc Indiana University}}" nl
		 "\\put(0,-54){\\makebox[0pt]{\\sc Bloomington, Indiana 47405-7104}}" nl
		 ))
		 ))
	       (in-tex-env "picture" '()
		   (list "(0,0)" nl
		 "\\put(180,-60){\\makebox[0pt]{\\small{}$^*$Collaborating with Profs. Daniel P. Friedman
and Amr A. Sabry on logical programming systems}}"))

	       "\\newpage" nl))))


     ; Standard typography
     (em
      . ,(lambda (tag . elems)
	   (list "\\emph{" elems "}")))

     (p
      . ,(lambda (tag . elems)
	   (list elems nl nl)))

     (pn
      . ,(lambda (tag . elems)
	   (list "\\noindent{}" elems nl nl)))

     (div
      . ,(lambda (tag . elems)
	   (in-tex-env "trivlist" '()  (list "\\item{}" elems))))

     (br
      . ,(lambda (tag)
	   (list "\\\\ ")))

     (indent
       . ,(lambda (tag) "\\indent{}"))
       
     ($ *preorder* . ,typeset-exp)
        

     (code
      . ,(lambda (tag . elems)
	   ;(in-tex-env "ttfamily" '() elems) ;
	   (list "\\texttt{" elems "}")
	   ))

     (cite
      . ,(lambda (tag key)
	   (list "\\cite{" key "}")))

     (xref
      . ,(lambda (tag key)
	   (list "\\ref{" key "}")))

;      (peq
;        . ,(lambda (tag eqn . body)
; 	    `("\\parbox{4.2in}{" ,body "\\hfill{}(" ,eqn ")" "}" ,nl ,nl)))

;      (peq
;        . ,(lambda (tag eqn . body)
; 	    (list "\\par\\noindent{}" (in-tex-env "tabular" '("{cr}") 
; 	      (list "\\parbox{4.0in}{\\centering{}\\parbox{4.0in}{" body 
; 		"}} & " (and eqn (list " (" eqn ")")) "\\\\\n")) nl)))

     (peq
       ((explain *macro* . ,(lambda (tag . strs) `("{ " ,strs " }")))
       )
       . ,(lambda (tag eqn . body)
	    (list "\\addvspace{\\smallskipamount}"
	      "\\par\\noindent{}" (in-tex-env "tabular" '("{cr}") 
	      (list "\\parbox{4.4in}{\\centering{}" body 
		"} & " (and eqn (list " (" eqn ")")) "\\\\")) nl
	      "\\addvspace{\\smallskipamount}")))


     (align-left
       . ,(lambda (tag . lines)
	    (list 
	      "\\parbox[t]{8in}{"
	      "\\vspace{-\\smallskipamount}"
	      (in-tex-env "tabbing" '()
		(list-intersperse lines "\\\\"))
	      "\\vspace{-\\medskipamount}"
	      "}")))

     (footnote 
       . ,(lambda (tag . exp) (list "\\footnote{" exp "}")))

     (ul			; Unnumbered lists
      . ,(lambda (tag . elems)
	   (in-tex-env "itemize" '() elems)))

     (ol			; Numbered lists
      . ,(lambda (tag . elems)
	   (in-tex-env "enumerate" '() elems)))

     (li
      . ,(lambda (tag . elems)
	   (list "\\item " elems nl)))

     (dl			; Definition list
				; deal with the sequences of dt/dd in CPS

      ; dl and dt are translated to procedures that take one argument:
      ; previously set label: list of fragments or #f if none
      ; The procedure returns a pair: (new-label . generate-fragments)
      ; Initially, label is #f

      ((dt			; The item title
	. ,(lambda (tag . elems)
	    (lambda (label)
	      (cons elems	; elems become the new label
		    (if label	; the label was set: we've seen dt without dd
			(list "\\item [" label "]" nl) ; empty body
			'())))))
       (dd			; The item body
	. ,(lambda (tag . elems)
	    (lambda (label)
	      (cons #f		; consume the existing label
		    (list "\\item [" (or label "") "] " elems nl)))))
       )
      . ,(lambda (tag . procs)	; execute provs generated by dt/dd
	  (let loop ((procs procs) (label #f) (accum '()))
	    (if (null? procs) (in-tex-env "description" '() (reverse accum))
		(let ((result ((car procs) label)))
		  (loop (cdr procs) (car result) (cons (cdr result) accum))))))
      )
	
     (URL 
      . ,(lambda (tag url) (list " \\texttt{" url "} ")))

     (LaTeX
      . ,(lambda (tag) "\\LaTeX{} "))

     (blockquote
      . ,(lambda (tag . elems)
	   (in-tex-env "quote" '() elems)))

     (Section	; (Section level "content ...")
      . ,(lambda (tag level head-word . elems)
	   (list #\\
		 (case level
		   ((1 2) "section")
		   ((3) "subsection")
		   ((4) "subsubsection")
		   (else (error "unsupported section level: " level)))
		 "{" head-word elems "}" nl)))

     (abstract			; The abstract of the document
      ((Revision
	. ,(lambda (tag)	; Find the Header in the Content
				; and create the revision record
	     (let ((header-parms (find-Header Content)))
	       (list "The present article specifies revision "
		     (lookup-def 'Revision header-parms #f) " of SXML. "))))
       (prod-note
	. ,(lambda (tag . master-url)
	     (list
	      "\\\\The paper is written in SXML itself. The present paper is the result of translating that SXML code into \\LaTeX, using an appropriate \"stylesheet\". A different stylesheet converted the specification to HTML. The master file, the stylesheets and the corresponding HTML and \\LaTeX documents are available at "  master-url ".")))
       (keywords
	. ,(lambda (tag)
	     (let ((header-parms (find-Header Content)))
	       (list "\\\\Keywords: " 
		     (lookup-def 'keywords header-parms #f) "."))))

       )
      . ,(lambda (tag . abstract-body)
	   (in-tex-env "abstract" '() abstract-body))
      )

     (Acknowledgment
      . ,(lambda (tag title)
	   (list "\\subsection*{" title "}" nl)))

;      (References	; (References bibitem ...)
;       *preorder*	; (bibitem label key . text)
;       . ,(lambda (tag . bib-items)
; 	   (let
; 	       ((widest-label ; first search for the widest label
; 			      ; among the bibitems
; 		 (let loop ((items bib-items) (widest ""))
; 		   (if (null? items) widest
; 		       (loop (cdr items)
; 			     (let ((label (cadar items)))
; 			       (if (> (string-length label)
; 				      (string-length widest))
; 				   label widest))))))
; 		(processed-items
; 		 (map
; 		  (lambda (bib-item)
; 		    (apply
; 		     (lambda (tag label key . text)
; 		       (list "\\bibitem[" label "]{" key "} " text nl))
; 		     bib-item))
; 		  bib-items)))
; 	     (in-tex-env "thebibliography" (list "{" "" "}")
; 			 processed-items))))

      (References	; (References bibitem ...)
       ((bibitem
	 . ,(lambda (tag label key . text)
	      (list "\\bibitem{" key "} " text nl)))
	)
       . ,(lambda (tag . bib-items)
	    (in-tex-env "thebibliography" "{}"
			bib-items)))

      (BibReferences	; (BibReferences bibitem ...)
        . ,(lambda (tag)
	    (list "\\bibliographystyle{mcbride}" nl
	      "%\\divide\\bibsep 3" nl
	      "%\\setlength{\\bibsep}{0pt}" nl
	      "\\bibliography{mybib}" nl
	      "%\\newcommand{\\bibpreamble}{\\nobreak\\vspace*{-.5\\parskip}}"
	      nl
	      "\\kern-\\prevdepth" nl
	      )))

;      (verbatim	; set off pieces of code: one or several lines
;       ((*text* . ; Different quotation rules apply within a verbatim block
; 	       ,(let ((string->goodTeX-in-verbatim
; 		      (make-char-quotator
; 		       '( (#\^ . "\\^")
; 			 ))))
; 		  (lambda (trigger str) 
; 		    (if (string? str) (string->goodTeX-in-verbatim str) str)))
; 	       ))
;       . ,(lambda (tag . lines)
; 	   (in-tex-env "verbatim" '()
; 		       (map (lambda (line) (list "   " line nl))

     (verbatim	; set off pieces of code: one or several lines
      ((*text* . ; Different quotation rules apply within a "verbatim" block
	       ,(let ((string->goodTeX-in-verbatim
		      (make-char-quotator
		       '((#\space "~")	; All spaces are "hard"
			 (#\# . "\\#") (#\$ . "\\$") (#\% . "\\%")
			 (#\& . "\\&") (#\~ . "\\textasciitilde{}")
			 (#\_ . "\\_") (#\^ . "\\^")
			 (#\\ . "$\\backslash$") (#\{ . "\\{")
			 (#\} . "\\}")))))
		  (lambda (trigger str) 
		    (if (string? str) (string->goodTeX-in-verbatim str) str)))
	       )
	(strong
	  . ,(lambda (tag . elems)
	       (list "\\textrm{\\small\\bfseries{}" elems "}")))
	)
      . ,(lambda (tag . lines)
	   (in-tex-env "lyxcode" '()
		       (map (lambda (line) 
			      (list (if (equal? line "") "~" line) 
				    "\\\\" nl))
			    lines))))

      (small-verbatim	; set off pieces of code: one or several lines
      ((*text* . ; Different quotation rules apply within a "verbatim" block
	       ,(let ((string->goodTeX-in-verbatim
		      (make-char-quotator
		       '((#\space "~")	; All spaces are "hard"
			 (#\# . "\\#") (#\$ . "\\$") (#\% . "\\%")
			 (#\& . "\\&") (#\~ . "\\textasciitilde{}")
			 (#\_ . "\\_") (#\^ . "\\^")
			 (#\\ . "$\\backslash$") (#\{ . "\\{")
			 (#\} . "\\}")))))
		  (lambda (trigger str) 
		    (if (string? str) (string->goodTeX-in-verbatim str) str)))
	       ))
      . ,(lambda (tag . lines)
	   (in-tex-env "list" '()
	     (list "{}"
	       "{%\\raggedright" nl
	        "\\setlength{\\rightmargin}{-15pt}" nl
	        "\\setlength{\\itemsep}{-12pt}" nl
	        "\\setlength{\\parsep}{-4pt}" nl
	        "\\small\\ttfamily}%" nl
	       (map (lambda (line) 
		      (list "\\item  "
			(if (equal? line "") "~" line)
			"\\\\" nl))
		 lines)))))

     (table
		; verbatim mode does not work in tabular <deep sigh> ...
		; we have to emulate
      ((verbatim	
	((*text* . ; Different quotation rules apply within a "verbatim" block
	       ,(let ((string->goodTeX-in-verbatim
		      (make-char-quotator
		       '((#\space "~")	; All spaces are "hard"
			 (#\# . "\\#") (#\$ . "\\$") (#\% . "\\%")
			 (#\& . "\\&") (#\~ . "\\textasciitilde{}")
			 (#\_ . "\\_") (#\^ . "\\^")
			 (#\\ . "$\\backslash$") (#\{ . "\\{")
			 (#\} . "\\}")))))
		  (lambda (trigger str) 
		    (if (string? str) (string->goodTeX-in-verbatim str) str)))
	       ))
	. ,(lambda (tag . lines)	
	     (map (lambda (line) (list "\\texttt{\\small " line "}\\\\"))
		  lines)))
       (peq . ,(lambda (tag eqn . body) body))
       (tr		; elems ::= [(@ attrib ...)] td ...
			; we disregard all attributes of a row
			; The result is (td ...)
	. ,(lambda (tag . elems)
	     (if (and (pair? elems) (pair? (car elems))
		      (eq? '@ (caar elems)))
		 (cdr elems)
		 elems)))

       (td		; elems ::= [(@ attrib ...)] body ...
			; we're only interested in (align "alignment") attr
			; and the (colspan "number") attr
			; The result is ("alignment" colspan body ...)
			; where "alignment" will be #\l, #\c, #\r
			; (#\l if not given); colspan is the integer
	. ,(lambda (tag . elems)
	     (define (get-alignment attrs)
	       (cond
		((assq 'align attrs) =>
		 (lambda (attr)
		   ;(cerr "align attr: " attr nl)
		   (cond
		    ((string-ci=? (cadr attr) "left") #\l)
		    ((string-ci=? (cadr attr) "right") #\r)
		    ((string-ci=? (cadr attr) "center") #\c)
		    (else (error "wrong alignment attribute: " attr)))))
		(else #\l)))
	     (define (get-colspan attrs)
	       (cond
		((assq 'colspan attrs) =>
		 (lambda (attr)
		   (let ((val (string->number (cadr attr))))
		     (assert val)
		     val)))
		(else 1)))
	     (if (and (pair? elems) (pair? (car elems))
		      (eq? '@ (caar elems)))
		 (cons (get-alignment (cadar elems))
		   (cons (get-colspan (cadar elems))
			 (cdr elems)))
		 (cons (get-alignment '())
		   (cons (get-colspan '())
			elems)))))

       (th		; elems ::= [(@ attrib ...)] body ...
			; we're only interested in (align "alignment") attr
			; and the (colspan "number") attr
			; The result is ("alignment" colspan body ...)
			; where "alignment" will be #\l, #\c, #\r
			; (#\c if not given); colspan is the integer
	. ,(lambda (tag . elems)
	     (define (get-alignment attrs)
	       (cond
		((assq 'align attrs) =>
		 (lambda (attr)
		   ;(cerr "align attr: " attr nl)
		   (cond
		    ((string-ci=? (cadr attr) "left") #\l)
		    ((string-ci=? (cadr attr) "right") #\r)
		    ((string-ci=? (cadr attr) "center") #\c)
		    (else (error "wrong alignment attribute: " attr)))))
		(else #\c)))
	     (define (get-colspan attrs)
	       (cond
		((assq 'colspan attrs) =>
		 (lambda (attr)
		   (let ((val (string->number (cadr attr))))
		     (assert val)
		     val)))
		(else 1)))
	     (if (and (pair? elems) (pair? (car elems))
		      (eq? '@ (caar elems)))
		 (cons (get-alignment (cadar elems))
		   (cons (get-colspan (cadar elems))
			 (cdr elems)))
		 (cons (get-alignment '())
		   (cons (get-colspan '())
			elems)))))
       )
			; (table [(@ attrib ...)] tr ...
      . ,(lambda (tag row . rows)
	   (let*-values
	    (((attrs rows)
	      (if (and (pair? row) (eq? '@ (car row)))
		  (values (cadr row) rows)
		  (values '() (cons row rows))))
	     ((border?)
	      (cond
	       ((assq 'border attrs) => 
		(lambda (border-attr) (not (equal? "0" (cadr border-attr)))))
	       (else #f)))
	     ((caption label table-type table-alignment)
	      (apply values
		     (map (lambda (name)
			    (cond
			     ((assq name attrs) => cadr)
			     (else #f)))
			  '(caption key table-type align))))
	     (dummy (assert (pair? rows))) ; at least one row must be given
	     ((ncols) (length (car rows)))
	     ((tex-cols)
	      (let ((col-codes
		     (map (lambda (_) (if border? "l|" "l")) (car rows))))
		(if border?
		    (apply string-append 
			   (cons "|" col-codes))
		    (apply string-append col-codes))))
	     )
	    (list
	      (list
	       (and (equal? table-alignment "center")
		    "\\centering")
	       (in-tex-env "tabular"
			   (list "{" ; "@{\\extracolsep{-25pt}}" 
				 tex-cols "}")
		(list (and border? "\\hline\n")
		  (map
		   (lambda (row)
		     (list
		      (list-intersperse
		       (map
			(lambda (col)
			  (apply
			   (lambda (alignment span . data)
			     (list "\\multicolumn{" span "}{" alignment "}{"
				   "\\minitab[" alignment "]{"
				   data "}}")
			     )
			   col))
			row)
		       " & ")
		      "\\\\" (and border? "\\hline") nl))
		   rows)
		  nl))
; 	       (and caption (list "\\caption{" 
; 				  (and label 
; 				       (list "\\label{" label "}"))
; 				  caption "}"))
	       ))
	    )))

     ; Floating figure
     (figure
      . ,(lambda (tag refkey caption . body)
	   (in-tex-env "figure" '()
		       (list body
		       "\\caption{" (and refkey 
				       (list "\\label{" refkey "}"))
		       caption "}")
		       )))
		       
     (fbox			; Frame box
      . ,(lambda (tag . text)
	   (list "\\fbox{" text "}")))

     ; Simple LaTeX drawing
     (picture
      ((textbox .
	,(lambda (tag x y . text-strs)
	   (list "\\put(" x "," y "){" text-strs "} ")))
       (line .
	,(lambda (tag x y length slope-x slope-y)
	   (list "\\put(" x "," y "){\\line(" slope-x "," slope-y"){" 
		 length "}} ")))
       )
      . ,(lambda (tag width height . elems)
	   (list "\\begin{picture}(" width "," height ")(0,0)" nl
		 elems
		 "\\end{picture}" nl))
      )

     ; Include an EPSF file
     ; A graphicx package is assumes
     ; Attributes are passed as name=value pairs of the includegraphics command
     (includegraphics		; Include an EPSF file
      ((@ ((*default* . ,(lambda args args))) . ,(lambda args args)))
      . ,(lambda (tag maybe-attrs . text)
	   (let*
	       ((attrs (and (pair? maybe-attrs) (eq? '@ (car maybe-attrs))
			    (cdr maybe-attrs)))
		(text (if attrs text (cons maybe-attrs text))))
	   (list "\\includegraphics["
		 (list-intersperse
		  (map
		  (lambda (name-val)
		    (list (car name-val) "=" (cdr name-val)))
		  attrs)
		  ",")
		 "]{" text "}"))))

     ; Fancy characters
     (Longrightarrow
      . ,(lambda (tag)
	   "$\\Longrightarrow$"))

     (rightarrow
      . ,(lambda (tag)
	   "$\\rightarrow$"))

     (diag-arrow   ; direction is: nw ne se sw
      *preorder*
      . ,(lambda (tag direction)
	   "$\\" 
	   (case direction
	     ((nw) "nw")
	     ((ne) "ne")
	     ((se) "se")
	     ((sw) "sw")
	     (else (error "wrong direction: " direction)))
	   "arrow$"))

     (symbol-equiv
      . ,(lambda (tag)
	   "$\\equiv$"))

     (greek
      . ,(lambda (tag letter)
	   (list "$\\" letter "$")))

     (displaymath
       ((symbol-equiv . ,(lambda (tag) "\\equiv{}"))
	(underbrace . ,(lambda (tag text . label) 
			 (list "\\underbrace{" text "}"
			   (and (pair? label) (list "_{" label "}")))))
	(*text*
	  . ,(lambda (tag str)
	       (with-output-to-string
		 (lambda ()
		   (with-input-from-string str
		     (lambda ()
		       (do ((c (read-char) (read-char)))
			 ((eof-object? c))
			 (case c
			   ((#\space) (display "\\;"))
			   (else (write-char c))))))))))
       )
       . ,(lambda (tag . elems)
	    (list "\\[" elems "\\]" nl)))


     ; Slide terms

     ; Centered paragraph
     (pcenter
      . ,(lambda (tag . elems)
	   (in-tex-env "center" '() elems)))

     (small
      . ,(lambda (tag . elems)
	   (list "{\\small{}" elems "}")))

     (strong
      . ,(lambda (tag . elems)
	   (list "{\\rmfamily\\bfseries{}" elems "}")))

     (scshape
      . ,(lambda (tag . elems)
	   (in-tex-env "scshape" '() elems)))

     (vspace   ; in points
      . ,(lambda (tag size)
	   (list "\\vspace{" size "pt" "}")))

     (tex      ; raw tex expression
       *preorder*
       . ,(lambda (tag str) str))
	    
     (extra   ; additional stuff
      . ,(lambda (tag . elems)
	   (list "\\parbox{6in}{\\medskip\\tiny{}" elems "}\\medskip" nl)))

     ; Grammatical terms

     (table-of-expr
       ((comment *macro*
	 . ,(lambda (tag str)
	      `((tex " &") ,str (br))))
	 )
       . ,(lambda (tag . exprs)
	    (in-tex-env "tabular*"
	      '("{5in}" "{" "l@{\\extracolsep{1in}}l" "}")
	      (list-intersperse
		exprs
		"~&~\\\\\n"))))

     (ebnf-def	; Choice of terms
      *macro*
      . ,(lambda (tag term-def . others)
	   `(,term-def (tex "$\\:::=\\:$") ,@others)))

     (ebnf-choice	; Choice of terms
      . ,(lambda (tag . terms)
	   (list "~~~" (list-intersperse terms "$\\,\\bigm\\vert\\,$"))))


     (ebnf-several
       . ,(lambda (tag . elems)
	    (list-intersperse elems ", ")))
     
     )))
 )

(generate-TEX Content)


; LocalWords:  CPS args env cc expr greset gshift greek redex pcenter Plotkin
; LocalWords:  fixpoint Felleisen cupto Chung chieh reifying peq Danvy HV equiv
; LocalWords:  Filinski's PR deconstructor hv hr ren ebnf Sabry