(* Deriving the context-passing implementation of polyvariadic printf,
   Section 5.2 of the paper.
*)

(* We start with the refined tupling implementation of printf in Fig 5,
   the descP3 implementation.
   The following is a brief summary.
*)

(* Constructors for the argument sequence *)
let nilA3      = ()
let consA3 h t = (h,t)
;;

(* Deconstructors for the argument sequence *)
let is_nilA3    = fun () -> ()
let un_consA3 x = x
;;

(* Constructors for the result, string sequence: *)
let nilS3 = ""
let consS3 h t = h ^ t
;;

(* Constructors for the descriptor sequence *)

(* val nilDP3 : unit -> string *)
let nilDP3           = fun x -> is_nilA3 x; nilS3
(* val consDP : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c *)
let consDP3 d tD = fun x -> d tD x (* identity *)
;;


(* Primitive format descriptors *)
let litP3 str = fun tD arg -> 
  consS3 str (tD arg)
;;

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

(* val charP3 : ('a -> string) -> char * 'a -> string *)
let string_of_char x = String.make 1 x;;
let charP3 = fun tD arg ->
  let (c,l2) = arg in
  consS3 (string_of_char c) (tD l2)
;;

let printf3 = fun x -> x
;;

(* The running example *)
let descP3 = consDP3 intP3
    (consDP3 (litP3 "-th character after ")
       (consDP3 charP3
          (consDP3 (litP3 " is ")
             (consDP3 charP3
                nilDP3))))
;;

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

printf3 descP3 (5,('a',('f',())));;

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



(* We now choose a slightly different representation for the string
sequence. It is no longer a string. Rather, it is a
function that receives a string (an accumulator) and appends to it.
In short, the S-sequence is now a difference string.  In the optimized
implementation, the accumulator could be a list of string fragments
accumulated in reverse order; Building of the S-sequence would
no longer need any string concatenations and can be done in
linear time (with respect to the length of the sequence). We defer
such an optimization to a later time, however.
*)

let nilSC4      = fun acc -> acc;;
let consSC4 h t = fun acc -> t (acc ^ h)
;;

(* We re-write our implementation to use nilSC4, consSC4 *)

let nilDPC4           = fun x -> is_nilA3 x; nilSC4
let consDPC4 = consDP3 (* remains the same, identity *)
;;

(* When we re-write litP, intP, charP, we inline consSC4 *)

let litPC4 str = fun tD arg acc -> 
  (tD arg) (acc ^ str)
;;

(* val intPC4 : ('a -> string -> 'b) -> int * 'a -> string -> 'b *)
let intPC4 = fun tD arg acc ->
  let (n,l2) = arg in
  (tD l2) (acc ^ (string_of_int n))
;;

let charPC4 = fun tD arg acc ->
  let (c,l2) = arg in
  (tD l2) (acc ^ (string_of_char c))
;;


(* Let us look at the bigger picture of that change. In Sec 2, we have
   derived the general implementation for consD and nilD, which we have
   been specializing since:

let consD dP tD = fun (y,l2) -> consS (dP y) (tD l2)
let nilD        = fun () -> nilS

If we inline nilSC4 and consSC4 here, we obtain

let consD dP tD = fun (y,l2) acc -> tD l2 (acc ^ (dP y))
let nilD        = fun () acc -> acc

Thus a descriptor sequence is a function of two arguments: it takes
an argument sequence and the accumulator.

Let us flip the argument order. That may sound a bit arbitrary, but we shall
see the reasons for that: to bring the arguments in the right
order for eta-reduction. But first, let's examine the consequences
of such a change:

let consD dP tD = fun acc (y,l2) -> tD (acc ^ (dP y)) l2
let nilD        = fun acc () -> acc

The descriptor sequence now takes the accumulator as the first argument.

We can also view this sequence of transformations -- introducing an
accumulator and switching the order of arguments -- as fusing the call
of tD with a bit of its context, (consS formatted_value []).

We should recall printf. Before, it was the identity. We have changed
the string sequence to be a difference string. We still want printf to
return an ordinary string. Thus we have to change printf to pass the
empty string as the accumulator. The flip in the argument order makes
the accumulator the first argument of the descriptor sequence, so that
new printf becomes

let printfC5 desc args = desc "" args

or, eta-reduced
*)

let printfC5 desc = desc "";;

(* we should flip the argument order -- put acc ahead of arg --
   in the other places
*)

let nilDPC5           = fun acc x -> is_nilA3 x; acc
let consDPC5 = consDP3 (* remains the same, identity *)
;;

(* Recall that tD is the rest of the descriptor sequences; that is,
   tD is a function whose argument order we have just flipped.
*)

let litPC5 str = fun tD acc arg -> 
  tD (acc ^ str) arg
;;

(* val intPC4 : ('a -> string -> 'b) -> int * 'a -> string -> 'b *)
let intPC5 = fun tD acc arg ->
  let (n,l2) = arg in
  tD (acc ^ (string_of_int n)) l2
;;

let charPC5 = fun tD acc arg ->
  let (c,l2) = arg in
  tD (acc ^ (string_of_char c)) l2
;;


(* The function litPC5 clearly shows the benefit of the flip: we can eta-reduce
   the arg argument:
*)

(* val litPC6 : string -> (string -> 'a) -> string -> 'a *)
let litPC6 str = fun tD acc -> 
  tD (acc ^ str)
;;

(* The function intPC5 can be re-written simply as

let intPC5 = fun tD acc (n,l2) ->
  tD (acc ^ (string_of_int n)) l2
;;

We can curry it, and eta-reduce l2:
*)

(* val intPC6 : (string -> 'a) -> string -> int -> 'a *)
let intPC6 = fun tD acc n ->
  tD (acc ^ (string_of_int n))
;;

(* and the same for charPC6 *)
let charPC6 = fun tD acc c ->
  tD (acc ^ (string_of_char c))
;;


let nilDPC6  = nilDPC5
let consDPC6 = consDP3 (* remains the same, identity *)
;;


(* The running example becomes *)
let descPC6 = consDPC6 intPC6
    (consDPC6 (litPC6 "-th character after ")
       (consDPC6 charPC6
          (consDPC6 (litPC6 " is ")
             (consDPC6 charPC6
                nilDPC6))))
;;

(* val descPC6 : string -> int -> char -> char -> unit -> string *)

(* The type shows that we have `uncurried' the tuple! *)

printfC5 descPC6 5 'a' 'f' ();;

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

(* We can trace the final () to is_NilA3 in nilDPC5. The function nilDPC5 
   does not have to take any argument x, which is dummy () anyway.
   After removing the argument, see see that
     let nilDPC7           = fun acc -> acc
   nilDP becomes the identity.
  
   Since consDP is the identity, we drop it. The descriptor sequence thus
   becomes

let descP = intP
    ((litP "-th character after ")
       (charP
          ((litP " is ")
             (charP
                nilDP))))
;;

which is just the functional composition of primitive descriptors applied
to  nilDP, which is the identity function.

We thus obtain the following final implementation.
*)

(* val printfC7 : (('a -> 'a) -> string -> 'b) -> 'b *)
let printfC7 desc = desc (fun x -> x) "";;


(* Primitive format descriptors *)
(* val litPC7 : string -> (string -> 'a) -> string -> 'a *)
let litPC7 str = fun tD acc -> 
  tD (acc ^ str)
;;

(* intPC7 : (string -> 'a) -> string -> int -> 'a *)
let intPC7 = fun tD acc n ->
  tD (acc ^ (string_of_int n))
;;

(* charPC7 : (string -> 'a) -> string -> char -> 'a *)
let charPC7 = fun tD acc c ->
  tD (acc ^ (string_of_char c))
;;

(* Functional composition: infix operation *)
(* val ( ^^ ) : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b *)
let (^^) f g = fun x -> f (g x);;


(* The running example becomes *)
let descPC7 = 
  intPC7 ^^ (litPC7 "-th character after ") ^^ charPC7 ^^ (litPC7 " is ") ^^ charPC7
;;

(* val descPC7 : (string -> '_a) -> string -> int -> char -> char -> '_a *)

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

(* We have thus derived Danvy's functional unparsing. *)