Imported Upstream version 8.1~gammaupstream/8.1.gamma

6 files changed, 46 insertions, 65 deletions

diff --git a/lib/options.ml b/lib/options.ml
index 2e29f61b..c46857e3 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: options.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
+(* $Id: options.ml 9191 2006-09-29 15:45:42Z courtieu $ *)
 
 open Util
 
@@ -22,6 +22,7 @@ let batch_mode = ref false
 let debug = ref false
 
 let print_emacs = ref false
+let print_emacs_safechar = ref false
 
 let term_quality = ref false
 
diff --git a/lib/options.mli b/lib/options.mli
index 1a5444a4..30d585fb 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: options.mli 7740 2005-12-26 20:07:21Z herbelin $ i*)
+(*i $Id: options.mli 9191 2006-09-29 15:45:42Z courtieu $ i*)
 
 (* Global options of the system. *)
 
@@ -17,6 +17,7 @@ val batch_mode : bool ref
 val debug : bool ref
 
 val print_emacs : bool ref
+val print_emacs_safechar : bool ref
 
 val term_quality : bool ref
 
diff --git a/lib/stamps.ml b/lib/stamps.ml
deleted file mode 100644
index 0f481516..00000000
--- a/lib/stamps.ml
+++ /dev/null
@@ -1,28 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: stamps.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
-
-let new_stamp = 
-  let stamp_ctr = ref 0 in
-  fun () -> incr stamp_ctr; !stamp_ctr
-
-type 'a timestamped = { stamp : int; ed : 'a }
-
-let ts_stamp st = st.stamp
-let ts_mod f st = { stamp = new_stamp(); ed = f st.ed }
-let ts_it st = st.ed
-let ts_mk v = { stamp = new_stamp(); ed = v}
-let ts_eq st1 st2 = st1.stamp = st2.stamp
-
-type 'a idstamped = 'a timestamped
-
-let ids_mod f st = { stamp = st.stamp; ed = f st.ed}
-let ids_it = ts_it
-let ids_mk = ts_mk
-let ids_eq = ts_eq
diff --git a/lib/stamps.mli b/lib/stamps.mli
deleted file mode 100644
index 6fa3077f..00000000
--- a/lib/stamps.mli
+++ /dev/null
@@ -1,28 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: stamps.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
-
-(* Time stamps. *)
-
-type 'a timestamped
-
-(* [ts_mod] gives a ['b timestamped] with a new stamp *)
-val ts_mod : ('a -> 'b) -> 'a timestamped -> 'b timestamped
-val ts_it : 'a timestamped -> 'a
-val ts_mk : 'a -> 'a timestamped
-val ts_eq : 'a timestamped -> 'a timestamped -> bool
-val ts_stamp : 'a timestamped -> int
-
-type 'a idstamped
-
-(* [ids_mod] gives a ['b stamped] with the same stamp *)
-val ids_mod : ('a -> 'b) -> 'a idstamped -> 'b idstamped
-val ids_it : 'a idstamped -> 'a
-val ids_mk : 'a -> 'a idstamped
-val ids_eq : 'a idstamped -> 'a idstamped -> bool
diff --git a/lib/util.ml b/lib/util.ml
index 503dfeda..89cfd6fc 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: util.ml 8867 2006-05-28 16:21:41Z herbelin $ *)
+(* $Id: util.ml 9225 2006-10-09 15:59:23Z herbelin $ *)
 
 open Pp
 
@@ -194,7 +194,7 @@ let list_map_i f =
 let list_map2_i f i l1 l2 =  
   let rec map_i i = function
     | ([], []) -> []
-    | ((h1::t1), (h2::t2)) -> (f i h1 h2) :: (map_i (succ i) (t1,t2))
+    | ((h1::t1), (h2::t2)) -> let v = f i h1 h2 in v :: map_i (succ i) (t1,t2)
     | (_, _) -> invalid_arg "map2_i"
   in 
   map_i i (l1,l2)
@@ -202,7 +202,7 @@ let list_map2_i f i l1 l2 =
 let list_map3 f l1 l2 l3 =
   let rec map = function
     | ([], [], []) -> []
-    | ((h1::t1), (h2::t2), (h3::t3)) -> (f h1 h2 h3) :: (map (t1,t2,t3))
+    | ((h1::t1), (h2::t2), (h3::t3)) -> let v = f h1 h2 h3 in v::map (t1,t2,t3)
     | (_, _, _) -> invalid_arg "map3"
   in 
   map (l1,l2,l3)
@@ -295,9 +295,11 @@ let list_try_find f =
   in 
   try_find_f
 
-let rec list_uniquize = function
-  | [] -> []
-  | h::t -> if List.mem h t then list_uniquize t else h::(list_uniquize t)
+let list_uniquize l =
+  let rec aux acc = function
+  | [] -> List.rev acc
+  | h::t -> if List.mem h acc then aux acc t else aux (h::acc) t
+  in aux [] l
 
 let rec list_distinct = function
   | h::t -> (not (List.mem h t)) && list_distinct t
@@ -473,6 +475,17 @@ let array_last v =
 
 let array_cons e v = Array.append [|e|] v
 
+let array_rev t = 
+  let n=Array.length t in
+    if n <=0 then () 
+    else
+      let tmp=ref t.(0) in
+      for i=0 to pred (n/2) do 
+	tmp:=t.((pred n)-i);
+	t.((pred n)-i)<- t.(i);
+	t.(i)<- !tmp
+      done
+
 let array_fold_right_i f v a =
   let rec fold a n =
     if n=0 then a
@@ -649,6 +662,17 @@ let array_fold_map2' f v1 v2 e =
   in
   (v',!e')
 
+let array_distinct v =
+  try
+    for i=0 to Array.length v-1 do
+      for j=i+1 to Array.length v-1 do
+	if v.(i)=v.(j) then raise Exit
+      done
+    done;
+    true
+  with Exit ->
+    false
+
 (* Matrices *)
 
 let matrix_transpose mat =
@@ -713,6 +737,10 @@ let option_fold_left2 f e a b = match (a,b) with
   | Some x, Some y -> f e x y
   | _ -> e
 
+let option_fold_left f e a = match a with
+  | Some x -> f e x
+  | _ -> e
+
 let option_fold_right f a e = match a with
   | Some x -> f x e
   | _ -> e
@@ -789,6 +817,8 @@ let prvect_with_sep sep elem v =
   let n = Array.length v in
   if n = 0 then mt () else pr (n - 1)
 
+let surround p = hov 1 (str"(" ++ p ++ str")")
+
 (*s Size of ocaml values. *)
 
 module Size = struct
diff --git a/lib/util.mli b/lib/util.mli
index 959ef802..b2d8f135 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 8867 2006-05-28 16:21:41Z herbelin $ i*)
+(*i $Id: util.mli 9225 2006-10-09 15:59:23Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -149,6 +149,7 @@ val array_hd : 'a array -> 'a
 val array_tl : 'a array -> 'a array
 val array_last : 'a array -> 'a
 val array_cons : 'a -> 'a array -> 'a array
+val array_rev : 'a array -> unit
 val array_fold_right_i : 
   (int -> 'b -> 'a -> 'a) -> 'b array -> 'a -> 'a
 val array_fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a
@@ -175,6 +176,7 @@ val array_map_left_pair : ('a -> 'b) -> 'a array -> ('c -> 'd) -> 'c array ->
 val array_fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
 val array_fold_map2' :
   ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
+val array_distinct : 'a array -> bool
 
 (*s Matrices *)
 
@@ -207,6 +209,7 @@ val out_some : 'a option -> 'a
 val option_map : ('a -> 'b) -> 'a option -> 'b option
 val option_cons : 'a option -> 'a list -> 'a list
 val option_fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
+val option_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b option -> 'a
 val option_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option ->
   'c option -> 'a
 val option_iter : ('a -> unit) -> 'a option -> unit
@@ -238,6 +241,8 @@ val prlist_with_sep :
 val prvect_with_sep :
    (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b array -> std_ppcmds
 val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
+val surround : std_ppcmds -> std_ppcmds
+
 
 (*s Size of an ocaml value (in words, bytes and kilobytes). *)