(* * 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 -> (. 1>.,0) | 1 -> (. x>.,1) | n -> let (c,n1) = powerc (pred n) in (. (.~c x) * x>.,succ n1) ;; (* val powerc : int -> ('a, int -> int) code * int = *) let test = powerc 5;; (* val test : ('a, int -> int) code * int = (. (((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 = *) let rec powerd = function | 0 -> (. .<1>.>.,0) | 1 -> (. x>.,1) | n -> let (c,n1) = powerd (pred n) in (. .~(mul .<.~c x>. ..)>.,succ n1) ;; (* val powerd : int -> ('a, ('b, int) code -> ('b, int) code) code * int = *) let test1 = powerd 5;; (* val test1 : ('a, ('_b, int) code -> ('_b, int) code) code * int = (. .<(.~((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 = . .~(testd ..)>.;; (* val testdd : ('_a, int -> int) code = . ((((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 = ..;; let rec powerd1 = function | 0 -> (. one>.,0) | 1 -> (. x>.,1) | n -> let (c,n1) = powerd1 (pred n) in (. .~(mull .<.~c x>. ..)>.,succ n1) ;; (* val powerd1 : int -> ('a, ('b, int) code -> ('b, int) code) code * int = *) let test11 = powerd1 5;; (* val test11 : ('a, ('_b, int) code -> ('_b, int) code) code * int = (. (((* 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 = . .~(testd1 ..)>.;; (* val testdd1 : ('_a, int -> int) code = . ((((x_1 * x_1) * x_1) * x_1) * x_1)>. *)