(* Lifted map-reduce, nested loops, multiple prompts *)
(* This is a different approach, more in the spirit of HANSEI.
It partitions the work between reify and map_reduce_sw differently.
The end results are identical to those achieved in lifted_nested_mp.ml.
Although this code is not described in the paper, it should be easy
to understand from the description in the paper. After all, it solves
the same problem.
*)
open Delimcc;;
(* The `Logic' (or loop) variable of type 'i *)
(* We use the value of the type `generation' to impose the total order on
logic variables. The variable of the greatest generation has been
created by the most recent reify. Of course that holds only
if no loop variable escapes from the scope of the reify that created
it. Well, if it does, the corresponding prompt will no longer
be set so that any attempt to use such a variable will lead to
failure.
*)
type generation = int
let new_generation =
let cnt = ref 0 in
fun () ->
incr cnt; !cnt
;;
(* The variable and the interface to the reifier,
which `runs' the lifted computation *)
(* The request is delivered to the closest reify and always concerns
its own variable. Therefore, we don't need to mention that
variable in the request.
*)
type 'i var = Val of 'i | Var of generation * 'i req prompt
and 'i req = C_eq of 'i var * (bool -> 'i req)
;;
(* Polymorphic equality over loop variables *)
(*--start-equ--*)
let equ : 'i var -> 'i var -> bool = fun x y ->
match (x,y) with
| (Var (gx,px), Var (gy,py)) ->
if gx > gy then
shift px (fun k -> C_eq (y,k))
else if gx < gy then
shift py (fun k -> C_eq (x,k))
else true
| (Val x, Val y) -> x = y
| (Var (_,px), y) | (y, Var (_,px)) ->
shift px (fun k -> C_eq (y,k))
(*--end-equ--*)
;;
let rec member x = function
| [] -> false
| (h::t) -> equ x h || member x t
;;
(* The result of reification: the lazy tree of `cases' terminated with
the default case. Compare with the result of HANSEI reification, the
lazy tree of weighted choices.
It is a binary tree (we try to be general so to easily add other
constraints).
*)
type ('i,'r) switch = Default of 'r
| Case of 'i var * ('i,'r) switch * ('i,'r) switch
;;
(* The reifier *)
(* Unlike the reifier in the paper, it does not try to solve the
constraints. It merely reifies the loop body to a tree.
It is quite like reify0 in HANSEI: it is very dumb.
All smarts are in map_reduce, in the function that uses the
reified data structure.
*)
let reify : ('i var -> 'r) -> ('i,'r) switch = fun f ->
let var_prompt = new_prompt () in
let var = Var (new_generation (), var_prompt) in
let presult = new_prompt () in
let rec loop = function
| C_eq (y,k) ->
abort presult
(Case (y,
(push_prompt presult (fun () -> loop (k true))),
(push_prompt presult (fun () -> loop (k false)))))
in
push_prompt presult (fun () ->
loop (push_prompt var_prompt (fun () ->
abort presult (Default (f var)))))
;;
(* The map-reduce part *)
type 'i coll = {coll_member : 'i var -> bool;
coll_cardinality : int};;
(* A sample collection used in all of the examples *)
(* The sample domain of people of cardinality 100. *)
let people =
{coll_member = (fun v -> true); (* Assume this is the whole domain *)
coll_cardinality = 100;
};;
(* A commutative monoid *)
type 'r monoid = {union : 'r -> 'r -> 'r;
empty : 'r}
let sum_monoid = {union = (+); empty = 0}
;;
let rec repeat monoid r = function
| 0 -> monoid.empty
| 1 -> r
| n when n mod 2 = 0 ->
repeat monoid (monoid.union r r) (n/2)
| n ->
monoid.union r (repeat monoid r (n-1))
;;
(* Fold over the collection coll. We apply the map function represented
by the switch, and reduce the result with the commutative monoid.
This is quite like explore of HANSEI
*)
let map_reduce_sw monoid coll fsw =
let rec loop coll = function
| Default x -> repeat monoid x coll.coll_cardinality
| Case (v,br_t,br_f) ->
(match v with Var _ -> print_endline "case-var"
| _ -> print_endline "case-val");
if coll.coll_member v
then
monoid.union
(loop {coll_member = (fun x -> equ x v); coll_cardinality = 1}
br_t)
(loop {coll_member =
(fun x -> if equ x v then false else coll.coll_member x);
coll_cardinality = coll.coll_cardinality - 1}
br_f)
else
loop coll br_f
in loop coll fsw;;
let sum_over coll = map_reduce_sw sum_monoid coll;;
(* Many tests follow *)
let 100 = sum_over people (reify (fun x -> 1));;
let 101 = sum_over people (reify (fun x ->
if equ x (Val "alice") then 2 else 1));;
let 103 = sum_over people (reify (fun x ->
if equ x (Val "alice") then 2 else if equ x (Val "bob") then 3 else 1));;
let 203 = sum_over people (reify (fun x ->
if equ x (Val "alice") then
(if equ (Val "alice") x then 102 else -100)
else if equ x (Val "bob") then 3 else 1));;
let 1 = sum_over people (reify (fun x ->
if equ x (Val "alice") then
(if equ (Val "bob") x then 102 else -100)
else if equ x (Val "bob") then 3 else 1));;
(* Double-nested loops *)
let 10000 =
sum_over people (reify (fun x ->
sum_over people (reify (fun y -> 1))));;
let 9900 =
sum_over people (reify (fun x ->
sum_over people (reify (fun y ->
if equ y (Val "alice") then 0 else 1))));;
let 9900 =
sum_over people (reify (fun x ->
sum_over people (reify (fun y ->
if equ x (Val "alice") then 0 else 1))));;
let 9900 =
sum_over people (reify (fun x ->
sum_over people (reify (fun y ->
if equ y x then 0 else 1))));;
let 9900 =
sum_over people (reify (fun x ->
sum_over people (reify (fun y ->
if equ x y then 0 else 1))));;
let 29800 = (* 99 * (99 + 200) + (99+100) *)
sum_over people (reify (fun x ->
sum_over people (reify (fun y ->
if equ x y then
(if equ x (Val "alice") then
100 else 200)
else 1))));;
let 29800 = (* 99 * (99 + 200) + (99+100) *)
sum_over people (reify (fun x ->
sum_over people (reify (fun y ->
if equ x y then
(if equ x (Val "alice") then
(if equ y (Val "alice") then 100 else -100000)
else 200)
else 1))));;
(* Our running example in the paper *)
let 9703 =
sum_over people (reify (fun x ->
sum_over people (reify (fun y ->
if equ x (Val "alice") ||
equ y (Val "bob") ||
equ x y
then 0 else 1))))
;;
(* Triple-nested loops *)
let 990000 =
sum_over people (reify (fun x ->
sum_over people (reify (fun y ->
sum_over people (reify (fun z ->
if equ x z then 0 else 1))))));;
let 990000 =
sum_over people (reify (fun x ->
sum_over people (reify (fun y ->
sum_over people (reify (fun z ->
if equ z x then 0 else 1))))));;
let 990000 =
sum_over people (reify (fun x ->
sum_over people (reify (fun y ->
sum_over people (reify (fun z ->
if equ x y then 0 else 1))))));;
let 990000 =
sum_over people (reify (fun x ->
sum_over people (reify (fun y ->
sum_over people (reify (fun z ->
if equ y x then 0 else 1))))));;
let 999900 = (* 100 * (9900 + 99) *)
sum_over people (reify (fun x ->
sum_over people (reify (fun y ->
sum_over people (reify (fun z ->
if equ y x && equ x z then 0 else 1))))));;
let 999900 = (* 100 * (9900 + 99) *)
sum_over people (reify (fun x ->
sum_over people (reify (fun y ->
sum_over people (reify (fun z ->
if equ y x && equ x z && equ y z then 0 else 1))))));;
let 980100 =
sum_over people (reify (fun x ->
sum_over people (reify (fun y ->
sum_over people (reify (fun z ->
if equ y x || equ x z then 0 else 1))))));;
let 970200 = (* 100 * 99 * 98 *)
sum_over people (reify (fun x ->
sum_over people (reify (fun y ->
sum_over people (reify (fun z ->
if equ x z || equ z y || equ x y then 0 else 1))))));;
(*
let range_coll m n =
assert (n >= m);
{coll_member = (fun v -> true); (* This assumes the collection is the whole
domain *)
coll_cardinality = n - m + 1;}
;;
*)
(*
Testing the complexity of dealing with the conjunction of disequality
constraints in the star form.
The conclusion of our tests below: if the user writes nested loops
explicitly, the user has selected the variable order -- which
may be far from optimal. If the wrong order is selected, things can get
very slow.
No surprise here: when working with BDDs, the user, too, has to
select the variable order. If the wrong (for the problem) order
is selected, computations can become really, really slow.
*)
(* Time the execution *)
let timeit thunk =
let time_start = Sys.time () in
let r = thunk () in
Printf.printf "\nTime spent: %g sec\n" (Sys.time () -. time_start);
r;;
(*
let map_reduce_sw monoid coll fsw =
let rec loop coll = function
| Default x ->
Printf.printf "repeating with counter %d\n" coll.coll_cardinality;
repeat monoid x coll.coll_cardinality
| Case (v,br_t,br_f) ->
if coll.coll_member v
then
monoid.union
(loop {coll_member = (fun x -> equ x v); coll_cardinality = 1}
br_t)
(loop {coll_member =
(fun x -> if equ x v then false else coll.coll_member x);
coll_cardinality = coll.coll_cardinality - 1}
br_f)
else
loop coll br_f
in loop coll fsw;;
sum_over people (reify (fun x ->
sum_over people (reify (fun y1 ->
sum_over people (reify (fun y2 ->
if equ x y1 || equ x y2
then 0 else 1))))))
;;
repeating with counter 99
repeating with counter 1
repeating with counter 100
repeating with counter 99
repeating with counter 1
repeating with counter 100
The result shows that we really need laziness:
sum_over people (reify (fun y1 ->
sum_over people (reify (fun y2 ->
sum_over people (reify (fun x ->
if equ x y1 || equ x y2
then 0 else 1))))))
;;
repeating with counter 98
repeating with counter 1
repeating with counter 1
repeating with counter 99
repeating with counter 1
repeating with counter 99
repeating with counter 1
repeating with counter 100
timeit (fun () ->
sum_over people (reify (fun x ->
sum_over people (reify (fun y1 ->
sum_over people (reify (fun y2 ->
sum_over people (reify (fun y3 ->
if equ x y1 || equ x y2 || equ x y3
then 0 else 1)))))))))
;;
repeating with counter 99
repeating with counter 1
repeating with counter 100
repeating with counter 99
repeating with counter 1
repeating with counter 100
repeating with counter 100
repeating with counter 99
repeating with counter 1
repeating with counter 100
timeit (fun () ->
sum_over people (reify (fun y1 ->
sum_over people (reify (fun y2 ->
sum_over people (reify (fun y3 ->
sum_over people (reify (fun x ->
if equ x y1 || equ x y2 || equ x y3
then 0 else 1)))))))))
;;
repeating with counter 97
repeating with counter 1
repeating with counter 1
repeating with counter 1
repeating with counter 98
repeating with counter 1
repeating with counter 1
repeating with counter 98
repeating with counter 1
repeating with counter 1
repeating with counter 98
repeating with counter 1
repeating with counter 1
repeating with counter 99
repeating with counter 1
repeating with counter 98
repeating with counter 1
repeating with counter 1
repeating with counter 99
repeating with counter 1
repeating with counter 99
repeating with counter 1
repeating with counter 99
repeating with counter 1
repeating with counter 100
for the loop y1..y2: 6 vs 8
for the loop y1..y3: 10 vs 25
for the loop y1..y4: 15 vs 230
For comparison: counting the number of invocations of repeat in the loops
(essentially, the number of Default leaves) in lifted_nested_mp.ml
The latter code handles Default for the `known' case specially and
hence it is not printed below.
let map_reduce_sw monoid fsw =
let rec loop card = function
| Default r ->
Printf.printf "repeating with counter %d\n" card;
repeat monoid r card
| Case (_,r,tail) ->
monoid.union r (loop (card-1) tail)
(* assume always the member of the domain *)
in loop 100 fsw
;;
map_reduce_sw sum_monoid (reify (fun x ->
map_reduce_sw sum_monoid (reify (fun y1 ->
map_reduce_sw sum_monoid (reify (fun y2 ->
if equ x y1 || equ x y2
then 0 else 1))))))
;;
repeating with counter 99
repeating with counter 100
repeating with counter 99
repeating with counter 100
- : int = 980100
map_reduce_sw sum_monoid (reify (fun y1 ->
map_reduce_sw sum_monoid (reify (fun y2 ->
map_reduce_sw sum_monoid (reify (fun x ->
if equ x y1 || equ x y2
then 0 else 1))))))
;;
repeating with counter 98
repeating with counter 99
repeating with counter 99
repeating with counter 100
map_reduce_sw sum_monoid (reify (fun x ->
map_reduce_sw sum_monoid (reify (fun y1 ->
map_reduce_sw sum_monoid (reify (fun y2 ->
map_reduce_sw sum_monoid (reify (fun y3 ->
if equ x y1 || equ x y2 || equ x y3
then 0 else 1))))))))
;;
repeating with counter 99
repeating with counter 100
repeating with counter 99
repeating with counter 100
repeating with counter 100
repeating with counter 99
repeating with counter 100
- : int = 97029900
map_reduce_sw sum_monoid (reify (fun y1 ->
map_reduce_sw sum_monoid (reify (fun y2 ->
map_reduce_sw sum_monoid (reify (fun y3 ->
map_reduce_sw sum_monoid (reify (fun x ->
if equ x y1 || equ x y2 || equ x y3
then 0 else 1))))))))
;;
for the loop y1..y2: 4 vs 4
for the loop y1..y3: 7 vs 9
for the loop y1..y4: 11 vs 24
*)
print_endline "\nAll done";;