- provide generic memoization routines in Hashweak

- convert Trans and Register to use weak memoization

src/core/task.ml

@@ -45,7 +45,6 @@ and tdecl =
 let task_known = option_apply Mid.empty (fun t -> t.task_known)
 let task_clone = option_apply Mid.empty (fun t -> t.task_clone)
 let task_used  = option_apply Mid.empty (fun t -> t.task_used)
-let task_tag   = option_apply (-1)      (fun t -> t.task_tag)
 
 module Task = struct
   type t = task_hd

src/core/task.mli

@@ -44,7 +44,6 @@ and tdecl = private
 val task_known : task -> known_map
 val task_clone : task -> clone_map
 val task_used  : task -> use_map
-val task_tag   : task -> int
 
 (* constructors *)
 

src/core/trans.ml

@@ -43,35 +43,27 @@ let compose_l f g x = list_apply g (f x)
 
 let apply f x = f x
 
-let memo tag f =
-  let h = Hashtbl.create 63 in fun x ->
-    let t = tag x in
-    try Hashtbl.find h t
-    with Not_found ->
-      let r = f x in
-      Hashtbl.add h t r;
-      r
+module WHtask = Hashweak.Make (struct
+  type t = task_hd
+  let tag t = t.task_tag
+end)
 
-let term_tag t = t.t_tag
-let fmla_tag f = f.f_tag
-let decl_tag d = d.d_tag
-
-let store f = memo task_tag f
+let store fn = WHtask.memoize_option 63 fn
 
 let fold fn v =
-  let h = Hashtbl.create 63 in
+  let h = WHtask.create 63 in
   let rewind acc task =
     let acc = fn task acc in
-    Hashtbl.add h task.task_tag acc;
+    WHtask.add h task acc;
     acc
   in
-  let curr task =
-    try Some (Hashtbl.find h task.task_tag)
+  let current task =
+    try Some (WHtask.find h task)
     with Not_found -> None
   in
   let rec accum todo = function
     | None -> List.fold_left rewind v todo
-    | Some task -> begin match curr task with
+    | Some task -> begin match current task with
         | Some v -> List.fold_left rewind v todo
         | None   -> accum (task::todo) task.task_prev
       end
@@ -86,8 +78,13 @@ let fold_map_l fn v t = conv_res (List.rev_map snd) (fold_l fn (v, t))
 let map   fn = fold   (fun t1 t2 -> fn t1 t2)
 let map_l fn = fold_l (fun t1 t2 -> fn t1 t2)
 
+module WHdecl = Hashweak.Make (struct
+  type t = decl
+  let tag d = d.d_tag
+end)
+
 let decl fn =
-  let fn = memo decl_tag fn in
+  let fn = WHdecl.memoize 63 fn in
   let fn task acc = match task.task_decl with
     | Decl d -> List.fold_left add_decl acc (fn d)
     | td -> add_tdecl acc td
@@ -95,7 +92,7 @@ let decl fn =
   map fn
 
 let decl_l fn =
-  let fn = memo decl_tag fn in
+  let fn = WHdecl.memoize 63 fn in
   let fn task acc = match task.task_decl with
     | Decl d -> List.rev_map (List.fold_left add_decl acc) (fn d)
     | td -> [add_tdecl acc td]

src/driver/driver.ml

@@ -265,9 +265,10 @@ module Hsdq = Hashcons.Make (struct
   type t = driver_query
 
   let equal q1 q2 = q1.query_driver == q2.query_driver &&
-                    q1.query_lclone == q2.query_lclone
+    option_eq (==) q1.query_lclone q2.query_lclone
 
-  let hash q = Hashcons.combine q.query_driver.drv_tag (task_tag q.query_lclone)
+  let hash q = Hashcons.combine q.query_driver.drv_tag
+    (option_apply 0 (fun t -> 1 + t.task_tag) q.query_lclone)
 
   let tag n q = { q with query_tag = n }
 end)

src/driver/register.ml

@@ -39,34 +39,48 @@ let create gen = {
   generate = gen;
 }
 
+module WHenv = Hashweak.Make (struct
+  type t = Env.env
+  let tag = Env.env_tag
+end)
+
+module WHquery = Hashweak.Make (struct
+  type t = driver_query
+  let tag = query_tag
+end)
+
+module WHtask = Hashweak.Make (struct
+  type t = task_hd
+  let tag t = t.task_tag
+end)
+
 exception ArgumentNeeded
 
-let memo tag ext f =
-  let h = Hashtbl.create 7 in fun x ->
-    let t = tag x in
-    try Hashtbl.find h t
-    with Not_found ->
-      let r = f (ext x) in
-      Hashtbl.add h t r;
-      r
-
-let memo_env f =
-  let f = memo Env.env_tag (fun e -> e) f in function
+let memo_env fn =
+  let fn = WHenv.memoize 7 fn in function
     | None -> raise ArgumentNeeded
-    | Some env -> f env
+    | Some env -> fn env
 
-let memo_query f =
-  let f = memo query_tag (fun q -> q) f in function
+let memo_query fn =
+  let fn = WHquery.memoize 7 fn in function
     | None -> raise ArgumentNeeded
-    | Some drv -> fun task -> f (driver_query drv task) task
+    | Some drv -> fun task -> fn (driver_query drv task)
+
+let memo_use fn =
+  let fn task = fn (task_used task) in
+  let fn = WHtask.memoize_option 63 fn in
+  fun task -> fn (last_use task)
+
+let memo_clone fn =
+  let fn task = fn (task_clone task) in
+  let fn = WHtask.memoize_option 63 fn in
+  fun task -> fn (last_clone task)
 
-let memo_use   f = memo (fun t -> task_tag (last_use   t)) task_used  f
-let memo_clone f = memo (fun t -> task_tag (last_clone t)) task_clone f
-let memo_goal  f = memo task_tag (fun t -> t) f
+let memo_goal fn = WHtask.memoize_option 7 fn
 
-let gen_gen f () =
+let gen_task f () =
   let f0 = Trans.apply (f ()) in
-  fun _ _ -> f0
+  fun _ _ task -> f0 task
 
 let gen_env f () =
   let f0 env = Trans.apply (f env) in
@@ -76,7 +90,7 @@ let gen_env f () =
 let gen_query f () =
   let f0 query = Trans.apply (f query) in
   let f1 = memo_query f0 in
-  fun _ drv task -> f1 drv task
+  fun _ drv task -> f1 drv task task
 
 let gen_arg memo_arg f () =
   let f0 env arg = Trans.apply (f env arg) in
@@ -88,7 +102,7 @@ let gen_full f () =
   let f0 query goal = Trans.apply (f query goal) in
   let f1 query = memo_goal (f0 query) in
   let f2 = memo_query f1 in
-  fun _ drv task -> f2 drv task task
+  fun _ drv task -> f2 drv task task task
 
 let gen_both f () =
   let f0 env use clone = Trans.apply (f env use clone) in
@@ -97,7 +111,7 @@ let gen_both f () =
   let f3 = memo_env f2 in
   fun env _ task -> f3 env task task task
 
-let store       f = create (gen_gen f)
+let store       f = create (gen_task f)
 let store_env   f = create (gen_env f)
 let store_goal  f = create (gen_arg memo_goal f)
 let store_clone f = create (gen_arg memo_clone f)

src/util/hashweak.ml

@@ -17,45 +17,50 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module Make (S : Util.Tagged) =
-struct
+module Make (S : Util.Tagged) = struct
 
-  type 'a t = { ht : (int,'a) Hashtbl.t;
-                final : S.t -> unit}
+  type 'a t = {
+    table : (int,'a) Hashtbl.t;
+    final : S.t -> unit;
+  }
 
-  let wget w = Weak.get w 0
-  let wref v =
+  let create n =
+    let table = Hashtbl.create n in
     let w = Weak.create 1 in
-    Weak.set w 0 (Some v);
-    w
+    Weak.set w 0 (Some table);
+    let final x = match Weak.get w 0 with
+      | None -> ()
+      | Some h -> Hashtbl.remove h (S.tag x)
+    in
+    { table = table; final = final }
 
-  let create i =
-    let ht = Hashtbl.create i in
-    let w = wref ht in
-    let final x =
-      match wget w with
-        | None -> ()
-        | Some h -> Hashtbl.remove h (S.tag x) in
-    { ht = ht; final = final }
+  let add_tag  h = Hashtbl.add  h.table
+  let mem_tag  h = Hashtbl.mem  h.table
+  let find_tag h = Hashtbl.find h.table
 
-  let find h e = Hashtbl.find h.ht (S.tag e)
-
-  let mem h e = Hashtbl.mem h.ht (S.tag e)
-
-
-  exception AlreadyBounded
-
-  let add h e v =
-    let tag = S.tag e in
-    if Hashtbl.mem h.ht tag
-    then raise AlreadyBounded
-    else begin
-      Gc.finalise h.final e;
-      Hashtbl.replace h.ht tag v
-    end
+  let add_tag h t e v =
+    Gc.finalise h.final e; add_tag h t v
 
+  let add  h e = add_tag  h (S.tag e) e
+  let mem  h e = mem_tag  h (S.tag e)
+  let find h e = find_tag h (S.tag e)
 
+  let memoize n fn =
+    let h = create n in fun e ->
+      let t = S.tag e in
+      try find_tag h t
+      with Not_found ->
+        let v = fn e in
+        add_tag h t e v;
+        v
 
+  let memoize_option n fn =
+    let v = fn None in
+    let fn e = fn (Some e) in 
+    let fn = memoize n fn in
+    function
+      | Some e -> fn e
+      | None -> v
 
 end
 

src/util/hashweak.mli

@@ -17,25 +17,27 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module Make (X : Util.Tagged) :
-sig
+module Make (S : Util.Tagged) : sig
 
   type 'a t
 
   val create : int -> 'a t
-    (* create a hashtbl with weak key*)
+    (* create a hashtbl with weak keys *)
 
-  val find : 'a t -> X.t -> 'a
-    (* find the value binded to a key.
-       raise Not_found if there is no binding *)
+  val find : 'a t -> S.t -> 'a
+    (* find the value bound to a key.
+       Raises Not_found if there is no binding *)
 
-  val mem : 'a t -> X.t -> bool
-    (* test if a key bind to something.*)
+  val mem : 'a t -> S.t -> bool
+    (* test if a key is bound *)
 
-  exception AlreadyBounded
+  val add : 'a t -> S.t -> 'a -> unit
+    (* bind the key with the value given *)
+
+  val memoize : int -> (S.t -> 'a) -> (S.t -> 'a)
+    (* create a memoizing function *)
+
+  val memoize_option : int -> (S.t option -> 'a) -> (S.t option -> 'a)
+    (* memoizing functions on option types *)
 
-  val add : 'a t -> X.t -> 'a -> unit
-    (* bind the key with the value given.
-       It raises AlreadyBounded if a bound exists
-    *)
 end