(* Lifted map-reduce, nested loops *)
(* Since this is an expository code, we limit the type
of loop variables to strings.
Polymorphic loop variables are possible, but the encoding
will be distracting. We obtain the polymorphism when we move to
multiple prompts, in lifted_nested_mp.ml
*)
(*
#load "delimcc_simple.cmo";;
#load "lifted_once.cmo";;
*)
open Delimcc_simple;;
open Lifted_once;;
(* Beginning the overrides *)
(* The triple stars in the comments mark the changes from
lifted_once.ml.
*)
(* The `Logic' variable of type indiv *)
(* There are two ways of introducing mutable things with identity:
either unit ref (used with physical equality comparison),
or bool ref (The identity test is equi-mutability test).
We go for physical equality here. Again, this is not necessary
and the code below could be implemented in SML that lacks physical
equality.
Incidentally, lifted_nested_mp.ml uses a generation counter
to identify `logic' variables.
*)
type var = Val of indiv | Var of unit ref
;;
(* 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.
Previously, the first component of Case was a value. Now it can
be a variable. Since we still assume all loops are over the entire
domain, the change doesn't matter as we ignore the first component
of Case. The assumption is lifted when we move to loops over the powerset.
*)
type 'r switch = Default of 'r | Case of var * 'r * 'r switch (* *** *)
;;
(* The definitions of req, equ, and member are repeated here only
because the definition of 'var' has changed.
*)
(* The interface to the reifier, which `runs' the lifted computation *)
type 'r req = Done of 'r | Compare of var * var * (bool -> 'r req);;
(* Equality over logic variables *)
let equ : var -> var -> bool = fun x y ->
shift (fun k -> Compare (x,y,k));;
let rec member x = function
| [] -> false
| (h::t) -> equ x h || member x t
;;
(* The reifier for nested loops *) (* *** *)
(* The use of equ in place of (=) means delegation *)
let reify : (var -> 'r) -> 'r switch = fun f ->
let var = Var (ref ()) in
let rec loop_known w = function
| Done r -> r
| Compare (x,y,k) when x == var && y == var ->
loop_known w (k true)
| Compare (x,y,k) when x == var ->
loop_known w (k (equ y w))
| Compare (y,x,k)when x == var ->
loop_known w (k (equ y w))
| Compare (x,y,k) ->
loop_known w (k (equ x y)) in
let rec loop ws = function
| Done r -> Default r
| Compare (x,y,k) when x == var && y == var ->
loop ws (k true)
| Compare (x,y,k) when x == var ->
make_case ws k y
| Compare (y,x,k) when x == var ->
make_case ws k y
| Compare (x,y,k) ->
loop ws (k (equ x y))
and make_case ws k y =
if member y ws
then loop ws (k false)
else Case (y,loop_known y (k true),
loop (y::ws) (k false))
in loop [] (reset (fun () -> Done (f var)))
;;
(* Handle the request that the other reifiers have not handled *)
(* This is new *** *)
(*--start-top--*)
let top thunk =
let rec loop = function
| Done r -> r
| Compare (x,y,k) -> loop (k (x = y))
in loop (reset (fun () -> Done (thunk ())))
(*--end-top--*)
;;
(* Map-reduce with the switch *)
(* val map_reduce_sw : 'r monoid -> 'r switch -> 'r *)
(*--start-mr-sw--*)
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
(*--end-mr-sw--*)
;;
(* Tests *)
let false = top (fun () ->
member (Val "carol") [Val "alice"; Val "bob"; Val "alice"])
;;
let Case (Val "alice", true, Case (Val "bob", true, Default false)) =
top (fun () ->
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) =
top (fun () -> 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
top (fun () -> 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 =
top (fun () ->
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)) =
(top (fun () ->
(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--*)
top (fun () ->
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";;