Commits

Matthew Hammer  committed 99d8aaf

added AKList.memo_len_lte helper function; redesigned AKList.memo_reduce to use this function; simplified definition of merge and mergesort; everything is still correct according to tests.

  • Participants
  • Parent commits 40dd358
  • Branches nominal

Comments (0)

Files changed (6)

File Source/AdaptonUtil/AKList.ml

   and  type 'a alist = [ `Cons of 'a * Key.t * 'b | `Nil ] M.thunk as 'b
   =
 struct
+  module ABool = M.Make(Types.Bool)
 
   (** Adapton lists containing ['a]. *)
   type 'a alist = 'a alist' M.thunk
                 `Cons(x, xk1, contract xk2 ys)
       end
 
+    let memo_len_lte =
+      (* Tests if len(list) <= len.  Returns a thunked boolean. *)
+      (* Note: this memo table is globally shared. (this sharing is desirable.) *)
+      ABool.memo_keyed2 (module L) (module Types.Int) ~symbol:"len_lte" begin
+        fun len_lte xs len ->
+          match force xs, len with
+            | `Nil, _ -> true
+            | `Cons(_, _,  _), 0 -> false
+            | `Cons(_, xk, ys), n ->
+                assert (n > 0);
+                ABool.force (len_lte xk ys (n-1))
+      end
+
     let memo_reduce contract_f ?bias:(b=2) =
       (* contract is hoisted so as to fix its memo table in this body's closure *)
       let contract = memo_contract contract_f ~bias:b in
-      AData.memo_keyed2 (module L) (module Key) ~symbol:"reduce" begin
-        fun reduce xs iteration_key ->
-          match force xs with
-          | `Nil -> failwith "memo_reduce: empty list"
-          | `Cons (x, _, ys) ->
-              match force ys with
-                | `Nil -> x
-                | _ ->
-                    let (k1,k)  = Key.fork iteration_key in
-                    let (k2,k3) = Key.fork k in
-                    (*Log.more "contract" ; Log.end_more () ;*)
-                    let xs'     = contract k1 xs in
-                    (*Log.more "reduce" ; Log.end_more () ;*)
-                    let cont    = reduce k2 xs' k3 in
-                    (*Log.more "cont" ; Log.end_more () ;*)
-                    AData.force ( cont )
+      AData.memo_keyed2 (module Key) (module L) ~symbol:"reduce" begin
+        fun reduce xs_key xs ->
+          if ABool.force (memo_len_lte xs_key xs 1) then
+            match force xs with
+              | `Nil -> failwith "memo_reduce: empty list"
+              | `Cons (x, _, _) -> x
+          else
+            let (k1,k)  = Key.fork xs_key in
+            let (k2,k3) = Key.fork k in
+            (*Log.more "contract" ; Log.end_more () ;*)
+            let xs'     = contract k1 xs in
+            (*Log.more "reduce" ; Log.end_more () ;*)
+            let cont    = reduce k2 k3 xs' in
+            (*Log.more "cont" ; Log.end_more () ;*)
+            AData.force ( cont )
       end
 
 
     let memo_merge cmp =
       memo_keyed2 (module L) (module L) ~symbol:"merge" begin
         fun merge xs ys -> match (L.force xs), (L.force ys) with
-          | `Nil, `Nil  -> `Nil
-
-          | `Cons (x,xk,xstl), `Nil -> (* XXX -- copy tail; avoid sharing. *)
-              let (xk1,xk2) = Key.fork xk in
-              `Cons(x,xk1, merge xk2 xstl ys)
-
-          | `Nil, `Cons(y,yk,ystl) -> (* XXX -- copy tail; avoid sharing. *)
-              let (yk1,yk2) = Key.fork yk in
-              `Cons(y,yk1, merge yk2 xs ystl)
-
+          | `Nil, ys -> ys
+          | xs, `Nil -> xs
           | `Cons (x,xk,xstl), `Cons (y,yk,ystl) ->
               if cmp x y <= 0 then (* x is lesser *)
                 let (xk1,xk2) = Key.fork xk in
 
 
     (** Create memoizing constructor to mergesort an Adapton list with a comparator. *)
-    let memo_mergesort cmp ?bias:(b=2) =
-      let always_nil = const `Nil
-        (* TODO: it'd be nice to have immutable thunks (w/ dynamic
-           errors on update_const). *)
-      in
+    let memo_mergesort cmp ?bias:(b=2) xs_key xs =
       let singletons =
-        let single = memo_keyed2 (module R) (module Key)
-          ~symbol:"single"
-          (fun _ x xk -> `Cons (x, xk, always_nil))
+        let nil = const `Nil in
+        let single = memo_keyed2 (module R) (module Key) ~symbol:"single"
+          (fun _ x xk -> `Cons (x, xk, nil))
         in
         RunType.memo_map_with_key (module L)
           (fun x k ->
              let k1,k2 = Key.fork k in
              single k1 x k2)
       in
-
-      let mergesort xs iteration_key =
-        RunType.memo_reduce (memo_merge cmp) ~bias:b iteration_key xs
-      in
-      memo_keyed2 (module L) (module Key) ~symbol:"mergesort_setup" begin
-        fun _norecursion_ xs iteration_key ->
-          let (k1,k)  = Key.fork iteration_key in
+      L.thunk begin fun () ->
+        if ABool.force (L.memo_len_lte xs_key xs 1) then
+          L.force xs
+        else
+          let (k1,k ) = Key.fork xs_key in
           let (k2,k3) = Key.fork k in
-          match force xs with
-          | `Cons _ ->
-              let xs = singletons k1 xs in
-              let ys = mergesort xs k2 k3 in
-              force (RunType.AData.force ys)
-
-          | `Nil -> `Nil
+          let xs = singletons k1 xs in
+          let ys = RunType.memo_reduce (memo_merge cmp) ~bias:b k2 k3 xs in
+          L.force (RunType.AData.force ys)
       end
   end
 end

File Source/AdaptonUtil/Signatures.ml

 
         val memo_reduce :
           (Key.t -> data -> data -> data) -> ?bias:int ->
-          Key.t -> t -> Key.t -> AData.t (* Implemented. *)
+          Key.t -> Key.t -> t -> AData.t (* Implemented. *)
+
+        val memo_len_lte :
+          Key.t -> t -> int -> bool thunk (* Implemented. *)
 
 (* NOT YET IMPLEMENTED: *)
         val memo_append : t -> t -> t
         val memo_merge : (data -> data -> int) -> Key.t -> (t -> t -> t)
 
         val memo_quicksort : (data -> data -> int) -> (t -> t)
-        val memo_mergesort : (data -> data -> int) -> ?bias:int -> Key.t -> (t -> Key.t -> t)
+        val memo_mergesort : (data -> data -> int) -> ?bias:int -> Key.t -> (t -> t)
     end
 end = AKListType
 

File Source/AdaptonZoo/Adapton.ml

     type debug = unit
     END
 
-(* 
+(*
    Starting to design a better datatype for visualizing system logs:
 *)
     module Viz = struct
       type sys_ptr = debug
-          
+
       type sys_visit = sys_ptr * sys_evt list
-          
+
       and sys_evt =
         | Thunk of Symbol.t option * Key.t option * string
         | Cell  of Symbol.t option * Key.t option * string

File Test/TestAdapton/TestAKList.ml

 
   "Correctness" >::: [
 
-    "sumSmall" >:: begin fun () ->
-      let fn = (fun x y -> x + y) in
-      let kfn = (fun k x y -> fn x y) in
-      let reduce_fn = I.memo_reduce kfn in
-      test_aklist_op_with_test
-        ~test:(fun ~msg expected actual -> assert_int_equal ~msg expected (I.AData.force actual))
-        ~count:10000 ~size:(fun _ -> 10)
-        (List.fold_left fn 0)
-        (fun nondet xs' -> reduce_fn (nondet ())
-           (* prepend 0 to avoid empty lists *)
-           (I.const (`Cons ( 0, nondet (), xs' )))
-           (nondet ()))
-    end;
-
     "mergesort" >:: begin fun () ->
       let cmp  = compare in
       let bias = 2 in
       test_aklist_op
         (List.sort compare)
         (fun nondet xs' -> I.memo_mergesort cmp ~bias
-           (nondet ()) xs'
-           (nondet ()) )
+           (nondet ()) xs' )
     end;
 
     "map" >:: begin fun () ->
         ~test:(fun ~msg expected actual -> assert_int_equal ~msg expected (I.AData.force actual))
         (*~count:100 ~size:(fun _ -> 4)*)
         (List.fold_left fn 0)
-        (fun nondet xs' -> reduce_fn (nondet ())
+        (fun nondet xs' -> reduce_fn (nondet ()) (nondet ())
            (* prepend 0 to avoid empty lists *)
-           (I.const (`Cons ( 0, nondet (), xs' )))
-           (nondet ()))
+           (I.const (`Cons ( 0, nondet (), xs' ))) )
     end;
 
     "max" >:: begin fun () ->
       test_aklist_op_with_test
         ~test:(fun ~msg expected actual -> assert_int_equal ~msg expected (I.AData.force actual))
         (List.fold_left fn 0)
-        (fun nondet xs' -> reduce_fn (nondet ())
+        (fun nondet xs' -> reduce_fn (nondet ()) (nondet ())
            (* prepend 0 to avoid empty lists *)
-           (I.const (`Cons ( 0, Adapton.Key.nondet (), xs' )))
-           (nondet ()))
+           (I.const (`Cons ( 0, Adapton.Key.nondet (), xs' ))) )
     end;
 
     "sum" >:: begin fun () ->
                  assert_int_equal ~msg expected (I.AData.force actual))
         (List.fold_left fn 0) (* verifier *)
         (fun nondet xs' ->
-           reduce_fn (nondet ())
+           reduce_fn (nondet ()) (nondet ())
              (* prepend 0 to avoid empty lists *)
-             (I.const (`Cons ( 0, nondet (), xs' )))
-             (nondet ()))
+             (I.const (`Cons ( 0, nondet (), xs' ))) )
+    end;
+
+    "sumSmall" >:: begin fun () ->
+      let fn = (fun x y -> x + y) in
+      let kfn = (fun k x y -> fn x y) in
+      let reduce_fn = I.memo_reduce kfn in
+      test_aklist_op_with_test
+        ~test:(fun ~msg expected actual -> assert_int_equal ~msg expected (I.AData.force actual))
+        ~count:10000 ~size:(fun _ -> 10)
+        (List.fold_left fn 0)
+        (fun nondet xs' -> reduce_fn (nondet ()) (nondet ())
+           (* prepend 0 to avoid empty lists *)
+           (I.const (`Cons ( 0, nondet (), xs' ))) )
     end;
   ]
 

File Test/nominaladaptontest.ml

 
     let test_app nondet list =
       I.memo_reduce (fun _ x y -> if x > y then x else y)
-        (nondet ())
+        (nondet ()) (nondet ())
         (* prepend 0 to avoid empty lists *)
         (I.const (`Cons ( 0, nondet (), list )))
-        (nondet ())
+
   (*
     let test_app nondet list =
       AKLi.memo_map (module AKLi) succ (nondet ()) list

File Test/poplbenchmark.ml

 		Gc.compact ();
 
 		(* Fix seed. *)
-		Random.init i;
+		Random.init (i+20740);
 
 		(* Generate seeded list of floats. *)
 		let l_strict = gen_list n [] in
 		let l = IL.of_list l_strict in
 
 		(* Benchmark mergesort. *)
-		let sorted = IL.memo_mergesort Pervasives.compare (Key.nondet ()) l (Key.nondet ()) in
+		let sorted = IL.memo_mergesort Pervasives.compare (Key.nondet ()) l in
 		demand_list sorted n;
 		benchmark_demand handle l sorted;
 	done;