(* Lifted map-reduce, nested loops, multiple prompts *) (* Loop variables are now polymorphic. We still assume that all loops are over the same, whole domain still holds. *) open Delimcc;; (* Preliminaries (Sec 2.1). *) (* 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)) ;; (* 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 = Compare of 'i var * (bool -> 'i req) ;; (* Polymorphic equality over loop variables *) (* Two variables of the same generation are identical. *) (*--start-equ--*) let equ (x : 'i var) (y : 'i var) : bool = match (x,y) with | (Var (gx,px), Var (gy,py)) -> if gx > gy then shift px (fun k -> Compare (y,k)) else if gx < gy then shift py (fun k -> Compare (x,k)) else true | (Val x, Val y) -> x = y | (Var (_,px), y) | (y, Var (_,px)) -> shift px (fun k -> Compare (y,k)) (*--end-equ--*) ;; let rec member x = function | [] -> false | (h::t) -> equ x h || member x t ;; (* Switch: the list of `cases' terminated with the default case. Compare with the result of HANSEI reification, the lazy tree of weighted choices. The `tail' of Switch can be made lazy; we omit the optimization for the sake of simplicity of the example. *) type ('i,'r) switch = Default of 'r | Case of 'i var * 'r * ('i,'r) switch ;; let rec reflect : ('i,'r) switch -> ('i var -> 'r) = function | Default r -> fun _ -> r | Case (x,r,fsw) -> fun x' -> if equ x x' then r else reflect fsw x' ;; (* No need to wrap in top: equ answers simple questions by itself. Top can't answer any questions about variables anyway. *) let 1 = reflect (Case (Val "alice",1,Default 2)) (Val "alice");; let 2 = reflect (Case (Val "alice",1,Default 2)) (Val "bob");; 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 make_case y (Default r) rest = abort presult (Case (y,r,rest)) in let rec loop_known w = function | Compare (y,k) -> loop_known w (k (equ y w)) in let rec loop ws = function | Compare (y,k) -> if member y ws then loop ws (k false) else make_case y (push_prompt presult (fun () -> loop_known y (k true))) (push_prompt presult (fun () -> loop (y::ws) (k false))) in push_prompt presult (fun () -> loop [] (push_prompt var_prompt (fun () -> abort presult (Default (f var))))) ;; (* There is no need for top *) let map_reduce_sw monoid fsw = let rec loop card = function | Default r -> 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 ;; (* No need for top *) let false = member (Val "carol") [Val "alice"; Val "bob"; Val "alice"] ;; let Case (Val "alice", true, Case (Val "bob", true, Default false)) = reify (fun x -> member x [Val "alice"; Val "bob"; Val "alice"]) ;; (* Our running example in Sec 2.1 *) let Case (Val "alice", 1, Default 2) = (reify (fun x -> 1 + if equ x (Val "alice") then 0 else 1)) ;; (* The final example of Sec 2 *) let 97 = let ivs = [Val"alice"; Val"bob"; Val"alice"] in map_reduce_sw sum_monoid (reify (fun x -> (if member x ivs then 0 else 1) * (if equ x (Val "alice") then 4 else 1) * (if equ x (Val "carol") then 0 else 1))) ;; (* On to nested loops *) (* The result is now correct for the nested loop: it is 99 * 99 = 9801 *) let 9801 = map_reduce_sw sum_monoid (reify (fun x -> map_reduce_sw sum_monoid (reify (fun y -> if equ x (Val "alice") || equ y (Val "bob") then 0 else 1)))) ;; let Case (Val "alice", 0, Case (Val "bob", 99, Default 98)) = reify (fun x -> (map_reduce_sw sum_monoid (reify (fun y -> if equ x (Val "alice") || equ y (Val "bob") || equ x y then 0 else 1)))) ;; (* This loop now gives the correct result *) let 9703 = (*--start-full-ex--*) map_reduce_sw sum_monoid (reify (fun x -> map_reduce_sw sum_monoid (reify (fun y -> if equ x (Val "alice") || equ y (Val "bob") || equ x y then 0 else 1)))) (*--end-full-ex--*) ;; print_endline "\nAll done";;