(*
 *  In this example, we compute a staged power function while tracking how many
 *  multiplications the generated code performs.  This example demonstrates the
 *  utility of our environment-passing translation, in two ways.  First, it is
 *  easiest to write this example if we use a side effect such as mutable state
 *  in MetaOCaml, but such an extension (a piece of state of type int) has not
 *  been shown sound except through our translation.  Second, we can write this
 *  example in pure MetaOCaml (more awkwardly) using our translation.
 *
 *  Thanks to Olivier Danvy for suggesting this example.
 *)

let rec powerc = function
    | 0 -> (.<fun x -> 1>.,0)
    | 1 -> (.<fun x -> x>.,1)
    | n -> let (c,n1) = powerc (pred n) in
           (.<fun x -> (.~c x) * x>.,succ n1)
;;
(*
  val powerc : int -> ('a, int -> int) code * int = <fun>
*)

let test = powerc 5;;
(*
val test : ('a, int -> int) code * int =
  (.<fun x_5 ->
   (((fun x_4 ->
       (((fun x_3 ->
           (((fun x_2 -> (((fun x_1 -> x_1) x_2) * x_2)) x_3) * x_3)) x_4) *
         x_4)) x_5) * x_5)>.,
   5)
*)

let testc = (.! (fst test)) 2;;
(*
val testc : int = 32
*)

let mul x y = .<.<.~.~x * .~.~y>.>.;;
(*
val mul :
  ('a, ('b, int) code) code ->
  ('a, ('b, int) code) code -> ('a, ('b, int) code) code = <fun>
*)

let rec powerd = function
    | 0 -> (.<fun x -> .<1>.>.,0)
    | 1 -> (.<fun x -> x>.,1)
    | n -> let (c,n1) = powerd (pred n) in
           (.<fun x -> .~(mul .<.~c x>. .<x>.)>.,succ n1)
;;
(*
 val powerd : int -> ('a, ('b, int) code -> ('b, int) code) code * int = <fun>
*)

let test1 = powerd 5;;
(*
val test1 : ('a, ('_b, int) code -> ('_b, int) code) code * int =
  (.<fun x_5 ->
   .<(.~((fun x_4 ->
           .<(.~((fun x_3 ->
                   .<(.~((fun x_2 -> .<(.~((fun x_1 -> x_1) x_2) * .~x_2)>.)
                          x_3) * .~x_3)>.) x_4) * .~x_4)>.) x_5) * .~x_5)>.>.,
   5)
*)

let testd = .! (fst (powerd 5));;
let testdd = .<fun x -> .~(testd .<x>.)>.;;
(*
val testdd : ('_a, int -> int) code =
  .<fun x_1 -> ((((x_1 * x_1) * x_1) * x_1) * x_1)>.
*)

(* An attempt to write testd without overt use of multiple levels:
   no nested brackets.
*)
let one = .<1>.;;
let mul1 x y = .<.~x * .~y>.;;
let mull x y = .<mul1 .~x  .~y>.;;

let rec powerd1 = function
    | 0 -> (.<fun x -> one>.,0)
    | 1 -> (.<fun x -> x>.,1)
    | n -> let (c,n1) = powerd1 (pred n) in
           (.<fun x -> .~(mull .<.~c x>. .<x>.)>.,succ n1)
;;
(*
  val powerd1 : int -> ('a, ('b, int) code -> ('b, int) code) code * int = <fun>
*)

let test11 = powerd1 5;;
(*
val test11 : ('a, ('_b, int) code -> ('_b, int) code) code * int =
  (.<fun x_5 ->
   (((* cross-stage persistent value (as id: mul1) *))
     ((fun x_4 ->
        (((* cross-stage persistent value (as id: mul1) *))
          ((fun x_3 ->
             (((* cross-stage persistent value (as id: mul1) *))
               ((fun x_2 ->
                  (((* cross-stage persistent value (as id: mul1) *))
                    ((fun x_1 -> x_1) x_2) x_2)) x_3) x_3)) x_4) x_4)) x_5)
     x_5)>.,
   5)
*)

let testd1 = .! (fst (powerd1 5));;
let testdd1 = .<fun x -> .~(testd1 .<x>.)>.;;
(*
val testdd1 : ('_a, int -> int) code =
  .<fun x_1 -> ((((x_1 * x_1) * x_1) * x_1) * x_1)>.
*)