From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 21 Nov 2006 21:38:49 +0000 Subject: Imported Upstream version 8.1~gamma --- lib/options.ml | 3 ++- lib/options.mli | 3 ++- lib/stamps.ml | 28 ---------------------------- lib/stamps.mli | 28 ---------------------------- lib/util.ml | 42 ++++++++++++++++++++++++++++++++++++------ lib/util.mli | 7 ++++++- 6 files changed, 46 insertions(+), 65 deletions(-) delete mode 100644 lib/stamps.ml delete mode 100644 lib/stamps.mli (limited to 'lib') 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 *) -(* 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 *) -(* '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). *) -- cgit v1.2.3