Imported Upstream version 8.2-1+dfsgupstream/8.2-1+dfsg

3 files changed, 53 insertions, 4 deletions

diff --git a/lib/envars.ml b/lib/envars.ml
index 5887adcd..d700ffe1 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -21,8 +21,9 @@ let guess_coqlib () =
     else 
       let coqbin = System.canonical_path_name (Filename.dirname Sys.executable_name) in
       let prefix = Filename.dirname coqbin in
-      let coqlib = if Coq_config.local then prefix else 
-	List.fold_left Filename.concat prefix ["lib";"coq"] in
+      let rpath = if Coq_config.local then [] else 
+	  (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in
+      let coqlib = List.fold_left Filename.concat prefix rpath in
 	if Sys.file_exists (Filename.concat coqlib file) then coqlib else
 	  Util.error "cannot guess a path for Coq libraries; please use -coqlib option"
 	  
diff --git a/lib/util.ml b/lib/util.ml
index a73a5558..a8a99c0b 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: util.ml 11845 2009-01-22 18:55:08Z letouzey $ *)
+(* $Id: util.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 
@@ -1354,6 +1354,39 @@ let pr_located pr (loc,x) =
 
 let surround p = hov 1 (str"(" ++ p ++ str")")
 
+(*s Memoization *)
+
+let memo1_eq eq f =
+  let m = ref None in
+  fun x ->
+    match !m with
+        Some(x',y') when eq x x' -> y'
+      | _ -> let y = f x in m := Some(x,y); y
+
+let memo1_1 f = memo1_eq (==) f
+let memo1_2 f =
+  let f' =
+    memo1_eq (fun (x,y) (x',y') -> x==x' && y==y') (fun (x,y) -> f x y) in
+  (fun x y -> f'(x,y))
+
+(* Memorizes the last n distinct calls to f. Since there is no hash,
+   Efficient only for small n. *)
+let memon_eq eq n f =
+  let cache = ref [] in (* the cache: a stack *)
+  let m = ref 0 in      (* usage of the cache *)
+  let rec find x = function
+    | (x',y')::l when eq x x' -> y', l (* cell is moved to the top *)
+    | [] -> (* we assume n>0, so creating one memo cell is OK *)
+        incr m; (f x, [])
+    | [_] when !m>=n -> f x,[] (* cache is full: dispose of last cell *)
+    | p::l (* not(eq x (fst p)) *) -> let (y,l') = find x l in (y, p::l')
+  in
+  (fun x ->
+    let (y,l) = find x !cache in
+    cache := (x,y)::l;
+    y)
+
+
 (*s Size of ocaml values. *)
 
 module Size = struct
diff --git a/lib/util.mli b/lib/util.mli
index 3cd934e7..5432eb98 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i $Id: util.mli 11769 2009-01-08 17:59:22Z glondu $ i*)
+(*i $Id: util.mli 11897 2009-02-09 19:28:02Z barras $ i*)
 
 (*i*)
 open Pp
@@ -298,6 +298,21 @@ val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds
 val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 val surround : std_ppcmds -> std_ppcmds
 
+(*s Memoization. *)
+
+(* General comments on memoization:
+   - cache is created whenever the function is supplied (because of
+      ML's polymorphic value restriction).
+   - cache is never flushed (unless the memoized fun is GC'd)
+ *)
+(* One cell memory: memorizes only the last call *)
+val memo1_1 : ('a -> 'b) -> ('a -> 'b)
+val memo1_2 : ('a -> 'b -> 'c) -> ('a -> 'b -> 'c)
+(* with custom equality (used to deal with various arities) *)
+val memo1_eq : ('a -> 'a -> bool) -> ('a -> 'b) -> ('a -> 'b)
+
+(* Memorizes the last [n] distinct calls. Efficient only for small [n]. *)
+val memon_eq : ('a -> 'a -> bool) -> int -> ('a -> 'b) -> ('a -> 'b)
 
 (*s Size of an ocaml value (in words, bytes and kilobytes). *)