(* More streamlined and condensed derivation of typed printf and scanf *)

(* The specification 

The format descriptor, argument list and the result of printf are all
sequences. That means they are built using `constructors' (consD,nilD),
(consA, nilA) and (consS, nilS) correspondingly.
  
The specification for printf is then
  
printf nilD nilA = nilS
printf (consD (lit str) desc) (consA () lst) = consS str (printf desc lst)
printf (consD int desc) (consA x lst) = consS (str_of_int x) (printf desc lst)
printf (consD char desc) (consA x lst) = consS (str_of_char x) (printf desc lst)

The specification for scanf is dual:
  
scanf nilD nilS = nilA
scanf (consD (lit s) desc) (consS s lst) = consA () (scanf desc lst)
scanf (consD int desc) (consS s lst) = consA (int_of_str s) (scanf desc lst)
scanf (consD char desc) (consS s lst) = consA (char_of_str s) (scanf desc lst)

This is the specification, not yet actual code. In particular, we still
have to decide on the representation for consD, nilD, consA, etc. 
`constructors' and what it means to pattern-match on them. These
`constructors' are not necessarily data constructors. We also leave aside
the issue of typing, till the moment we fix the representation.

*)

(* First, we define *)
let litP (str:string) () = str;;
let intP x = string_of_int x;;
let charP x = String.make 1 x;;

let litS (str:string) inp = assert (str = inp); ();;
let intS inp = int_of_string inp;;
let charS inp = inp.[0];;

(* We re-write the specification as follows then:

printf nilD nilA = nilS
printf (consD dP desc) (consA x lst) = consS (dP x) (printf desc lst)

scanf nilD nilS = nilA
scanf (consD dS desc) (consS s lst) = consA (dS s) (scanf desc lst)

Again, this is still the specification, not the actual code.

We have to choose the representation for nilD, consD, etc. We can
chose them to be data constructors, but then we get a typing problem:
the argument 'x' can be either unit, int or char. We'd like to avoid
the universal type so that
        printf (consD int desc) (consA 'c' lst)
would be a type error. We would like to try something like `tagless
final' approach (so that consD, nilD are constructor functions rather
than data constructors). Alas, at first blush, it does not seem to
apply: tagless final can express `evaluation' that is a fold. But our
printf is not fold: it is zipWith (with the restriction that two lists
must have the same size). The function zipWith has the following specification.

zipWith f nil nil = nil
zipWith f (cons x l1) (cons y l2) = cons (f x y) (zipWith f x l2)

In the case of printf and scanf, the 'f' function is the regular
functional application.

We can re-write the specification as follows:

zipWith f nil = fun nil -> nil
zipWith f (cons x l1) = fun (cons y l2) -> cons (f x y) ((zipWith f x) l2)

(implicitly relying on some sort of pattern-matching in the argument
of the function. We fix the exact form of that later.)

and again

zipWith f nil = fun nil -> nil
zipWith f (cons x l1) = (fun x -> fun z -> 
                                fun (cons y l2) -> cons (f x y) (z l2))
                        x (zipWith f x)

By the universality of foldr, we conclude that zipWith is foldr
(see Graham Hutton, A Tutorial on the Universality and Expressiveness of Fold,
JFP 1999).

zipWith f l1 l2 =  foldr f' z l1 l2

where f' x tD = fun (cons y l2) -> cons (f x y) (tD l2)
      z        = fun nil -> nil

In other words, the specification of printf can be expressed in terms of
foldr:

printf desc args = foldr f' z desc args

where f' dP tD = fun (consA y l2) -> consS (dP y) (tD l2)
      z         = fun nilA -> nilS


This immediately leads to the following code: we choose
  printf = id
  tuple-encoding for the argument list and the result list:
  nilA = () 
  consA x y = (x,y)
  ditto for consS, nilS

which gives as the specification

desc args = foldr f' z desc args
where f' dP tD = fun (y,l2) -> ((dP y),(tD l2))
      z         = fun () -> ()

and the representation for nilD and consD
*)

let nilD () = ();;
let consD d tD (y,l2) = ((d y),(tD l2));;

let desc1 = consD intP
    (consD (litP "-th character after ")
       (consD charP
          (consD (litP " is ")
             (consD charP
                nilD))));;

(*
 val desc1 :
  int * (unit * (char * (unit * (char * unit)))) ->
  string * (string * (string * (string * (string * unit)))) = <fun>
*)

(* printf is just the identity, which we elide *)
let r = desc1 (5,((),('a',((),('f',())))));;

(*
val r : string * (string * (string * (string * (string * unit)))) =
  ("5", ("-th character after ", ("a", (" is ", ("f", ())))))
*)

(* 
 We can also chose nilS to be an empty string and consS to be string
 concatenation, so obtain the output as the familiar string.
*)

(* The case for scanf is nearly identical. We show the final result.
 descS1 is descP1 with intP replaced with intS, etc.
*)

let descS1 = consD intS
    (consD (litS "-th character after ")
       (consD charS
          (consD (litS " is ")
             (consD charS
                nilD))));;

(*
 val descS1 :
  string * (string * (string * (string * (string * unit)))) ->
  int * (unit * (char * (unit * (char * unit)))) = <fun>
*)

descS1 r;;
(*
- : int * (unit * (char * (unit * (char * unit)))) =
(5, ((), ('a', ((), ('f', ())))))
*)

(*
We observe that (printf descP)  and (scanf descS) form an
injection-projection pair (where descS is obtained from descP by
replacing lit with litS, int with intS -- and vice versa).
*)

(* ========================================================================
   Deriving typed scanf satisfying the interface of the format input
   built into OCaml.
*)

(* Recall that nilA and consA are defined as follows: *)
let nilA = ()
let consA x y = (x,y)
;;

(* We re-write nilD and consD in terms of de-constructors *)
let is_nilS () = ()
let un_consS (h,t) = (h,t)
;;

let nilDS       = fun x -> is_nilS x; nilA
let consDS d tD = fun x -> let (y,l2) = un_consS x in
                           consA (d y) (tD l2)
;;

(* We now move un_consS into the definition of primitive descriptors.
 Now consDS becomes:
*)

let nilDS       = fun x -> is_nilS x; nilA
let consDS d tD = fun x -> let (v,l2) = d x in
                           consA v (tD l2)
;;

(* Where the new primitive descriptors (denoted as d above) are 
   defined as follows: *)

let litS11 (str:string) = fun x -> 
  let (y,l2) = un_consS x in
  assert (str = y); ((),l2)
let intS11  = fun x ->
  let (y,l2) = un_consS x in
  (int_of_string y,l2)
let charS11 = fun x ->
  let (y,l2) = un_consS x in
  (y.[0],l2)
;;


let nilD () = ();;
let consD d tD (y,l2) = ((d y),(tD l2));;


(* val nilDS : string -> unit *)
let nilDS        = fun x -> is_nilS x; nilA

(* val consDS : ('a -> 'b * 'c) -> ('c -> 'd) -> 'a -> 'b * 'd *)
let consDS d tD = fun x -> let (vy,l2) = d x in
                            consA vy (tD l2)
;;


(* We fix the formatted sequence to be a string:
   nilS is the empty string and consS is the string concatenation. 
   We fuse the string deconstruction with primitive scanf descriptors.
   The primitive scanf descriptors are now as follows:
*)


exception Scan_error of string
;;

(* val litS2 : string -> string -> unit * string *)
let litS2 str = fun inp -> 
  if String.length str <= String.length inp &&
     str = String.sub inp 0 (String.length str)
  then ((), String.sub inp (String.length str)
	                   (String.length inp - String.length str))
  else raise (Scan_error "lit")
;;

(* val intS2 : string -> int * string *)
let intS2 = fun inp ->
  let n = String.length inp in
  let rec loop acc i =
    if i >= n then (acc,"") else 
    let c = inp.[i] in
    if c >= '0' && c <= '9' then
      loop (acc * 10 + (int_of_char c - int_of_char '0')) (succ i)
    else if i = 0 then raise (Scan_error "int") 
    else (acc, String.sub inp i (n-i)) in
  if n = 0 then raise (Scan_error "int")
  else loop 0 0
;;

(* val charS2 : string -> char * string *)
let charS2 = fun inp ->
  if String.length inp = 0 
  then raise (Scan_error "char")
  else (inp.[0], String.sub inp 1 (String.length inp - 1));;



(* We re-define nilD and consD to use the new primitive descriptors.
   We introduce is_nilS to do the pattern-matching on the input,
   that is, to verify that the input is exhausted.
*)

let is_nilS x = assert (x = "");;

(* val nilDS : string -> unit *)
let nilDS        = fun x -> is_nilS x; nilA

(* val consDS : ('a -> 'b * 'c) -> ('c -> 'd) -> 'a -> 'b * 'd *)
let consDS d tD = fun x -> let (vy,l2) = d x in
                            consA vy (tD l2)
;;

(* The running example becomes as follows *)
let descS2 = consDS intS2
    (consDS (litS2 "-th character after ")
       (consDS charS2
          (consDS (litS2 " is ")
             (consDS charS2
                nilDS))));;
(*
val descS2 : string -> int * (unit * (char * (unit * (char * unit))))
*)

descS2 "5-th character after a is f";;
(*
- : int * (unit * (char * (unit * (char * unit)))) =
(5, ((), ('a', ((), ('f', ())))))
*)

(* We do further fusion: let the primitive descriptors themselves construct
   the A-sequence. We re-define the descriptors as follows:
*)

(* val litS3 : string -> (string -> 'a) -> string -> 'a *)
let litS3 str = fun tD inp -> 
  if String.length str <= String.length inp &&
     str = String.sub inp 0 (String.length str)
  then tD (String.sub inp (String.length str)
	                  (String.length inp - String.length str))
  else raise (Scan_error "lit")
;;

(* val intS3 : (string -> 'a) -> string -> int * 'a *)
let intS3 = fun tD inp ->
  let n = String.length inp in
  let rec loop acc i =
    if i >= n then consA acc (tD "") else 
    let c = inp.[i] in
    if c >= '0' && c <= '9' then
      loop (acc * 10 + (int_of_char c - int_of_char '0')) (succ i)
    else if i = 0 then raise (Scan_error "int") 
    else consA acc (tD (String.sub inp i (n-i))) in
  if n = 0 then raise (Scan_error "int")
  else loop 0 0
;;

(* val charS3 : (string -> 'a) -> string -> char * 'a *)
let charS3 = fun tD inp -> 
  if String.length inp = 0 
  then raise (Scan_error "char")
  else consA inp.[0] (tD (String.sub inp 1 (String.length inp - 1)));;


(* We re-define consD to use the new primitive descriptors.
*)
(* val consDS : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c *)
let consDS d tD = fun x -> d tD x
;;
(* The inferred type indicates this is essentially the identity function; 
   it becomes one after two eta-reductions
*)

(* The running example becomes as follows *)
(* Since consD is the identity, we could have just dropped all consD below *)
let descS3 = consDS intS3
    (consDS (litS3 "-th character after ")
       (consDS charS3
          (consDS (litS3 " is ")
             (consDS charS3
                nilDS))));;
(*
val descS3 : string -> int * (char * (char * unit))
*)

descS3 "5-th character after a is f";;
(*
- : int * (char * (char * unit)) = (5, ('a', ('f', ())))
*)
(* We have indeed got rid of the dummies *)

(* We'd like to have a different representation for argument list, as
a sequence of arguments, so to speak, rather than a nested tuple.
We choose a different representation for consA and nilA.
*)

let nilA = fun f -> f;;
let consA h t = fun f -> t (f h);;

(* The intuition for this choice:
 (consA x1 (consA x2 nilA)) is (beta-)equivalent to
 fun f -> f x1 x2
 So, we represent the collection as a sequence of arguments applied
 to some function.
*)

(* Now, we re-define everything to use the new definition of 3
as being nested tuples, we can use consD and nilD. However, we use the new
definitions of nilA and consA:
*)

(* val nilDS : string -> 'a -> 'a *)
let nilDS        = fun x -> is_nilS x; nilA

(* val litS4 : string -> (string -> 'a) -> string -> 'a *)
let litS4 str = fun tD inp -> 
  if String.length str <= String.length inp &&
     str = String.sub inp 0 (String.length str)
  then tD (String.sub inp (String.length str)
	                  (String.length inp - String.length str))
  else raise (Scan_error "lit")
;;

(* val intS4 : (string -> 'a -> 'b) -> string -> (int -> 'a) -> 'b *)
let intS4 = fun tD inp ->
  let n = String.length inp in
  let rec loop acc i =
    if i >= n then consA acc (tD "") else 
    let c = inp.[i] in
    if c >= '0' && c <= '9' then
      loop (acc * 10 + (int_of_char c - int_of_char '0')) (succ i)
    else if i = 0 then raise (Scan_error "int") 
    else consA acc (tD (String.sub inp i (n-i))) in
  if n = 0 then raise (Scan_error "int")
  else loop 0 0
;;

(* val charS4 : (string -> 'a -> 'b) -> string -> (char -> 'a) -> 'b *)
let charS4 = fun tD inp -> 
  if String.length inp = 0 
  then raise (Scan_error "char")
  else consA inp.[0] (tD (String.sub inp 1 (String.length inp - 1)));;

(* The running example becomes as follows *)
(* Since consD is the identity, we could have just dropped all consD below *)
let descS4 = consDS intS4
    (consDS (litS4 "-th character after ")
       (consDS charS4
          (consDS (litS4 " is ")
             (consDS charS4
                nilDS))));;
(* val descS4 : string -> (int -> char -> char -> '_a) -> '_a *)

(* Thus, we have derived scanf with the consumer function! *)

descS4 "5-th character after a is f" (fun x1 x2 x3 -> (x1,x2,x3));;
(*
- : int * char * char = (5, 'a', 'f')
*)
(* Thus we have derived sscanf of OCaml! *)

(* Examination of the inferred types of litS4, charS4, etc. demonstrates the
   relationship with CPS.
   Indeed, if we drop consD, we notice that a format descriptor is a functional
   _composition_ of the primitive descriptors, applied to nilDS.
*)

(* We can re-define the descriptors so that the input comes from a
   file descriptor rather than from a string. We can easily abstract over
   primitive descriptors: However, since they are polymorphic functions
  (which is obvious from their type), we need first-class
  polymorphism. Fortunately, OCaml supports such polymorphism in the
  form of polymorphic records.
*)

(* The type 'i is the type of the input to scanf: a string, a buffer, a 
   file descriptor, etc.
*)
type 'i descriptorS = {
    litS  : 'w. string -> ('i -> 'w) -> 'i -> 'w;
    intS  : 'a 'w. ('i -> 'a -> 'w) -> 'i -> (int -> 'a) -> 'w;
    charS : 'a 'w. ('i -> 'a -> 'w) -> 'i -> (char -> 'a) -> 'w;
  };;

(* primitive descriptors, this time generic *)
let litS5 str = fun {litS = f} -> f str;;
let intS5     = fun x -> x.intS;;
let charS5    = fun x -> x.charS;;

(* General composition function: composing two descriptors *)
(*val ( ^^ ) : ('a -> 'b -> 'c) -> ('a -> 'd -> 'b) -> 'a -> 'd -> 'c *)
let (^^) f g = fun d -> fun x -> f d (g d x);;

(*
  val descS5 :
  '_a descriptorS ->
  ('_a -> '_b -> '_c) -> '_a -> (int -> char -> char -> '_b) -> '_c
*)
let descS5 = 
  intS5 ^^ litS5 "-th character after " ^^ charS5 ^^ litS5 " is " ^^ charS5;;

(* The following function implements the interface of OCaml's sscanf,
   taking the input from a string
*)
(*
val scanf4 :
  (string descriptorS -> (string -> 'a -> 'a) -> 'b -> 'c) -> 'b -> 'c =
*)
let scanf4 d inp = d {litS=litS4;intS=intS4;charS=charS4} nilDS inp;;

scanf4 descS5 "5-th character after a is f" (fun x1 x2 x3 -> (x1,x2,x3));;
(*
- : int * char * char = (5, 'a', 'f')
*)

(* We have derived the real sscanf. We can derive a scanf that takes input
 from a file, using the same file descriptor.
*)

(* ========================================================================
                        Deriving printf 
*)

(* We rely on the symmetry between printf and scanf: 
   nilA <-> nilS and consA <-> consS
   To illustrate symmetry, we look back at descS2 version of scanf
   (with tuples for the A-sequence and string for the O-sequence).
   The dummy argument is still present.
   We `invert' the definition (by interchanging the A and O-sequences)
   to obtain a version of printf.
*)

let nilS = ""
let consS = (^);;

(* val is_nilA : unit -> unit *)
let is_nilA x = assert (x = ());;

(* val nilDP : unit -> string *)
let nilDP        = fun x -> is_nilA x; nilS;;

(* val consDP : ('a -> string * 'b) -> ('b -> string) -> 'a -> string *)
let consDP d tD = fun x -> let (vy,l2) = d x in
                            consS vy (tD l2)
;;

(* The primitive printf descriptors, the dual of scanf descriptors
   litS2, intS2, charS2. They de-construct the A-sequence
   on their own.
*)

(* val litP2 : string -> unit * 'a -> string * 'a *)
let litP2 str = fun arg ->
  let ((),l2) = arg in
  (litP str (),l2)
;;

(* val intP2 : int * 'a -> string * 'a *)
let intP2 = fun arg ->
  let (n,l2) = arg in
  (intP n,l2)
;;

(* val charP2 : char * 'a -> string * 'a *)
let charP2 = fun arg ->
  let (c,l2) = arg in
  (charP c,l2)
;;

(* The running example becomes as follows *)
(* It is descS2 with S replaced by P *)
let descP2 = consDP intP2
    (consDP (litP2 "-th character after ")
       (consDP charP2
          (consDP (litP2 " is ")
             (consDP charP2
                nilDP))));;
(*
val descP2 : int * (unit * (char * (unit * (char * unit)))) -> string
For comparison, descS2 had the type
val descS2 : string -> int * (unit * (char * (unit * (char * unit))))
*)

descP2 (5,((),('a',((),('f',())))));;

(*
- : string = "5-th character after a is f"
*)



(* Getting rid of the dummy unit arguments is significantly simpler now.
   We merely modify litP2

(* val litP3 : string -> 'a -> string * 'a *)
let litP21 str = fun arg ->
  let l2 = arg in
  (litP str (),l2)
;;

let intP21  = intP2;;
let charP21 = charP2;;

OTH, we just proceed as we did with scanf
*)


(* We do further fusion: let the primitive descriptors themselves construct
   the S-sequence. We re-define the descriptors as follows:
*)

(* val litP3 : string -> ('a -> string) -> 'a -> string *)
(* val litS3 : string -> (string -> 'a) -> string -> 'a *)
let litP3 str = fun tD arg -> 
  consS str (tD arg)
;;

(* val intS3 : (string -> 'a) -> string -> int * 'a *)
(* val intP3 : ('a -> string) -> int * 'a -> string *)
let intP3 = fun tD arg ->
  let (n,l2) = arg in
  consS (intP n) (tD l2)
;;

(* val charP3 : ('a -> string) -> char * 'a -> string *)
let charP3 = fun tD arg ->
  let (c,l2) = arg in
  consS (charP c) (tD l2)
;;

(* Since consDS that uses primitive descriptors litS3, etc.
   no longer depends on consS or consA, 
   consDP is the same as consDS: just the identity function
*)
(* val consDS : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c *)
let consDP d tD = fun x -> d tD x
;;

let descP3 = consDP intP3
    (consDP (litP3 "-th character after ")
       (consDP charP3
          (consDP (litP3 " is ")
             (consDP charP3
                nilDP))));;

(*
val descP3 : int * (char * (char * unit)) -> string = <fun>
*)
descP3 (5,('a',('f',())));;

(*
- : string = "5-th character after a is f"
*)


(* 
We now turn to the representation for the A-sequence that we used
for scanf. Recall:

let nilA = fun f -> f;;
let consA h t = fun f -> t (f h);;

How to write un_consA? it should satisfy the equation

un_consA (consA h t) = (h,t)

Since (consA h t) is a function, the only thing we can do is to apply it.

(consA h t) (fun h -> ...) = (h,t)
or, after inlining consA:

t ((fun h -> ...) h) -> (h,t)

Now we see the problem: ... needs to obtain one of its arguments, t,
from its context!

The solution is known: we can either use CPS or direct-style (that is,
delimited control). The derivation in CPS style is given in
derive6.ml, which yields printfC4 through printfC7. The following is the
direct-style derivation using multi-prompt delimited control. The
parallel direct-style derivation for the ordinary shift/reset is given
in Derive5.hs.

*)

open Delimcc;;

(* val un_consA : (('a -> 'b) -> 'c) -> 'a * ('b -> 'c) *)
let un_consA x =
   let pr = new_prompt () in
   let p = new_prompt () in
   push_prompt pr (fun () ->
   push_prompt p (fun () ->
    x (fun h -> shift p (fun t -> abort pr (h,t)))); 
   failwith "unreachable")
;;

let is_nilA x = x () = ();;

(*
Contrast the inferred type of un_consA with that of consA:
  val un_consA : (('a -> 'b) -> 'c) -> 'a * ('b -> 'c)
The inverse is easy to see.
*)

(* The example of the de-construction: *)

let l1 = consA 5 (consA 'a' (consA 'f' nilA));;
let (h1,l11) = un_consA l1;;
(*
  val h1 : int = 5
  val l11 : (char -> char -> '_a) -> '_a = <fun>
*)
let (h2,l12) = un_consA l11;;
(*
  val h2 : char = 'a'
  val l12 : (char -> '_a) -> '_a = <fun>
*)
let (h3,l13) = un_consA l12;;
(*
  val h3 : char = 'f'
  val l13 : '_a -> '_a = <fun>
*)

(* val litP4 : string -> ('a -> string) -> 'a -> string *)
let litP4 = litP3;;

(* val intP4 : (('a -> 'b) -> string) -> ((int -> 'a) -> 'b) -> string *)
let intP4 = fun tD arg ->
  let (n,l2) = un_consA arg in
  consS (intP n) (tD l2)
;;

let charP4 = fun tD arg ->
  let (c,l2) = un_consA arg in
  consS (charP c) (tD l2)
;;

(* is_nilA x should ``test'' if x is the identity function.
   The following is just as good test as applying x to () and checking
   that the result is unit.
*)
let nilDP        = fun x -> x nilS;;

let descP4 = consDP intP4
    (consDP (litP4 "-th character after ")
       (consDP charP4
          (consDP (litP4 " is ")
             (consDP charP4
                nilDP))));;
(*
val descP4 : ((int -> char -> char -> string) -> string) -> string = <fun>
*)

descP4 (consA 5 (consA 'a' (consA 'f' nilA)));;
(*
- : string = "5-th character after a is f"
*)

(* We would like the argument sequence to be just the application of the
arguments. We would like to transform
  (xxx x1 x2 x3)
to (fun f -> f x1 x2 x3), which is needed as an argument to descP4.
We can do that if we enclose the whole printf expression in reset.
*)

let p = new_prompt () in
push_prompt p (fun () ->
  shift p descP4 5 'a' 'f')
;;
(* 
- : string = "5-th character after a is f" ()
*)

(* Since printf always returns the string, the prompt p can be made
global. Alas, the need to enclose the whole expression into reset
is unsatisfying.
*)

(* Begin experiment: using control instead of shift.
   The derivation in the paper indicates that control should
   work just as well, if not better (no extra reset inserted).
   In the following, we repeat the development leading to descP4
   using control instead of shift. Everything works as before.
 *)

let un_consA x =
   let pr = new_prompt () in
   let p = new_prompt () in
   push_prompt pr (fun () ->
   push_prompt p (fun () ->
    x (fun h -> control p (fun t -> abort pr (h,t)))); 
   failwith "unreachable")
;;

let is_nilA x = x () = ();;

(*
Contrast the inferred type of un_consA with that of consA:
  val un_consA : (('a -> 'b) -> 'c) -> 'a * ('b -> 'c)
The inverse is easy to see.
*)

(* The example of the de-construction: *)

let l1 = consA 5 (consA 'a' (consA 'f' nilA));;
let (h1,l11) = un_consA l1;;
(*
  val h1 : int = 5
  val l11 : (char -> char -> '_a) -> '_a = <fun>
*)
let (h2,l12) = un_consA l11;;
(*
  val h2 : char = 'a'
  val l12 : (char -> '_a) -> '_a = <fun>
*)
let (h3,l13) = un_consA l12;;
(*
  val h3 : char = 'f'
  val l13 : '_a -> '_a = <fun>
*)

(* val litP4 : string -> ('a -> string) -> 'a -> string *)
let litP4 = litP3;;

(* val intP4 : (('a -> 'b) -> string) -> ((int -> 'a) -> 'b) -> string *)
let intP4 = fun tD arg ->
  let (n,l2) = un_consA arg in
  consS (intP n) (tD l2)
;;

let charP4 = fun tD arg ->
  let (c,l2) = un_consA arg in
  consS (charP c) (tD l2)
;;

(* is_nilA x should ``test'' if x is the identity function.
   The following is just as good test as applying x to () and checking
   that the result is unit.
*)
let nilDP        = fun x -> x nilS;;

let descP4 = consDP intP4
    (consDP (litP4 "-th character after ")
       (consDP charP4
          (consDP (litP4 " is ")
             (consDP charP4
                nilDP))));;
(*
val descP4 : ((int -> char -> char -> string) -> string) -> string = <fun>
*)

descP4 (consA 5 (consA 'a' (consA 'f' nilA)));;
(*
- : string = "5-th character after a is f"
*)

let p = new_prompt () in
push_prompt p (fun () ->
  control p descP4 5 'a' 'f')
;;
(* 
- : string = "5-th character after a is f" ()
*)

(* End of experiment: using control instead of shift *)


(* A different take, viewing un_consA as `reading' from a sequence. *)

(* The following is a ad hoc, especially the introduction of the accumulator *)
(* The accumulation is clearly very inefficient; that could be fixed;
   e.g., by making the accumulator a list of strings, to be accumulated
   in the reverse order and concatenated at the very end.
*)

let un_consA1 p =
   shift p (fun k h -> 
     let p' = new_prompt () in
     push_prompt p' (fun () -> 
       k (h,p'); failwith "out-of-bound ret"))
;;

(* Again, it works if shift replaced with control, or even
   control0 (aka, cupto). To test this, uncomment the definition below.
let un_consA1 p =
   control p (fun k h -> 
     let p' = new_prompt () in
     push_prompt p' (fun () -> 
       k (h,p'); failwith "out-of-bound ret"))
;;
*)

let nilDP5        = fun p acc -> abort p acc;;


(* litP5 : string -> ('a -> string -> 'b) -> 'a -> string -> 'b *)
let litP5 str = fun tD arg acc -> 
  (tD arg) (consS acc str)
;;

(* The only difference from intP4/charP4 is the introduction of the
   accumulator and the use of un_consA1 rather than un_consA.
*)

(*
 val intP5 :
  ('a Delimcc.prompt -> string -> 'b) ->
  (int -> 'a) Delimcc.prompt -> string -> 'b = <fun>
*)
let intP5 = fun tD arg acc ->
  let (n,l2) = un_consA1 arg in
  (tD l2) (consS acc (intP n))
;;

let charP5 = fun tD arg acc ->
  let (c,l2) = un_consA1 arg in
  (tD l2) (consS acc (charP c))
;;

(* printf5 : ('a Delimcc.prompt -> string -> 'a) -> 'a *)
let printf5 desc =
  let p = new_prompt () in
  push_prompt p (fun () -> desc p "");;

(* Note, consDP remains as before: the identity function *)
let descP5 = consDP intP5
    (consDP (litP5 "-th character after ")
       (consDP charP5
          (consDP (litP5 " is ")
             (consDP charP5
                nilDP5))));;
(*
val descP5 : (int -> char -> char -> string) Delimcc.prompt -> string -> 'a *)

printf5 descP5;;
(*
- : int -> char -> char -> string = <fun>
*)

printf5 descP5 5 'a' 'f';;
(*
- : string = "5-th character after a is f"
*)