summaryrefslogtreecommitdiff
path: root/lib/util.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/util.ml')
-rw-r--r--lib/util.ml60
1 files changed, 43 insertions, 17 deletions
diff --git a/lib/util.ml b/lib/util.ml
index b5470e58..2e6e1279 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -1,12 +1,12 @@
-(************************************************************************)
-(* 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 *)
-(************************************************************************)
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
-(* $Id: util.ml,v 1.84.2.3 2004/07/29 15:00:04 herbelin Exp $ *)
+(* $Id: util.ml 8672 2006-03-29 21:06:33Z herbelin $ *)
open Pp
@@ -32,8 +32,9 @@ type 'a located = loc * 'a
let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm))
let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm))
let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s)
-let join_loc (deb1,_ as loc1) (_,fin2 as loc2) =
- if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc else (deb1,fin2)
+let join_loc loc1 loc2 =
+ if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
+ else (fst loc1, snd loc2)
(* Like Exc_located, but specifies the outermost file read, the filename
associated to the location of the error, and the error itself. *)
@@ -98,6 +99,8 @@ let string_string_contains ~where ~what =
with
Not_found -> false
+let plural n s = if n>1 then s^"s" else s
+
(* string parsing *)
let parse_loadpath s =
@@ -118,10 +121,6 @@ module Stringset = Set.Make(struct type t = string let compare = compare end)
module Stringmap = Map.Make(struct type t = string let compare = compare end)
-let stringmap_to_list m = Stringmap.fold (fun s y l -> (s,y)::l) m []
-
-let stringmap_dom m = Stringmap.fold (fun s _ l -> s::l) m []
-
(* Lists *)
let list_add_set x l = if List.mem x l then l else x::l
@@ -251,6 +250,13 @@ let list_for_all_i p =
let list_except x l = List.filter (fun y -> not (x = y)) l
+let list_remove = list_except (* Alias *)
+
+let rec list_remove_first a = function
+ | b::l when a = b -> l
+ | b::l -> b::list_remove_first a l
+ | [] -> raise Not_found
+
let list_for_all2eq f l1 l2 = try List.for_all2 f l1 l2 with Failure _ -> false
let list_map_i f =
@@ -362,12 +368,12 @@ let list_share_tails l1 l2 =
let list_join_map f l = List.flatten (List.map f l)
-let rec list_fold_map f e = function
+let rec list_fold_map f e = function
| [] -> (e,[])
- | h::t ->
+ | h::t ->
let e',h' = f e h in
let e'',t' = list_fold_map f e' t in
- e'',h'::t'
+ e'',h'::t'
(* (* tail-recursive version of the above function *)
let list_fold_map f e l =
@@ -379,6 +385,10 @@ let list_fold_map f e l =
(e',List.rev lrev)
*)
+(* The same, based on fold_right, with the effect accumulated on the right *)
+let list_fold_map' f l e =
+ List.fold_right (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) l ([],e)
+
let list_map_assoc f = List.map (fun (x,a) -> (x,f a))
(* Arrays *)
@@ -596,6 +606,20 @@ let array_map_left_pair f a g b =
r, s
end
+let pure_functional = false
+
+let array_fold_map' f v e =
+if pure_functional then
+ let (l,e) =
+ Array.fold_right
+ (fun x (l,e) -> let (y,e) = f x e in (y::l,e))
+ v ([],e) in
+ (Array.of_list l,e)
+else
+ let e' = ref e in
+ let v' = Array.map (fun x -> let (y,e) = f x !e' in e' := e; y) v in
+ (v',!e')
+
(* Matrices *)
let matrix_transpose mat =
@@ -693,6 +717,8 @@ let pr_str = str
let pr_coma () = str "," ++ spc ()
let pr_semicolon () = str ";" ++ spc ()
let pr_bar () = str "|" ++ spc ()
+let pr_arg pr x = spc () ++ pr x
+let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x
let pr_ord n =
let suff = match n mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in