diff options
Diffstat (limited to 'lib/util.mli')
| -rw-r--r-- | lib/util.mli | 51 |
1 files changed, 37 insertions, 14 deletions
diff --git a/lib/util.mli b/lib/util.mli index 97bda074..cd8e3135 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 13200 2010-06-25 22:36:25Z letouzey $ i*) +(*i $Id$ i*) (*i*) open Pp @@ -26,12 +26,19 @@ exception UserError of string * std_ppcmds val error : string -> 'a val errorlabstrm : string -> std_ppcmds -> 'a +exception AlreadyDeclared of std_ppcmds +val alreadydeclared : std_ppcmds -> 'a + +exception AnomalyOnError of string * exn + (* [todo] is for running of an incomplete code its implementation is "do nothing" (or print a message), but this function should not be used in a released code *) val todo : string -> unit +exception Timeout + type loc = Compat.loc type 'a located = loc * 'a @@ -57,6 +64,12 @@ exception Error_in_file of string * (bool * string * loc) * exn val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b +(* Mapping under triple *) + +val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd +val on_pi2 : ('a -> 'b) -> 'c * 'a * 'd -> 'c * 'b * 'd +val on_pi3 : ('a -> 'b) -> 'c * 'd * 'a -> 'c * 'd * 'b + (*s Projections from triplets *) val pi1 : 'a * 'b * 'c -> 'a @@ -75,6 +88,7 @@ val is_blank : char -> bool val explode : string -> string list val implode : string list -> string val strip : string -> string +val drop_simple_quotes : string -> string val string_index_from : string -> int -> string -> int val string_string_contains : where:string -> what:string -> bool val plural : int -> string -> string @@ -98,6 +112,7 @@ val ascii_of_ident : string -> string (*s Lists. *) +val list_compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int val list_add_set : 'a -> 'a list -> 'a list val list_eq_set : 'a list -> 'a list -> bool val list_intersect : 'a list -> 'a list -> 'a list @@ -119,16 +134,18 @@ val list_map_filter : ('a -> 'b option) -> 'a list -> 'b list val list_smartmap : ('a -> 'a) -> 'a list -> 'a list val list_map_left : ('a -> 'b) -> 'a list -> 'b list val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list -val list_map2_i : +val list_map2_i : (int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list val list_map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list val list_map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list +val list_filter_i : + (int -> 'a -> bool) -> 'a list -> 'a list (* [list_index] returns the 1st index of an element in a list (counting from 1) *) val list_index : 'a -> 'a list -> int (* [list_unique_index x l] returns [Not_found] if [x] doesn't occur exactly once *) -val list_unique_index : 'a -> 'a list -> int +val list_unique_index : 'a -> 'a list -> int (* [list_index0] behaves as [list_index] except that it starts counting at 0 *) val list_index0 : 'a -> 'a list -> int val list_iter3 : ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list -> 'c list -> unit @@ -151,16 +168,18 @@ val list_uniquize : 'a list -> 'a list (* merges two sorted lists and preserves the uniqueness property: *) val list_merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list val list_subset : 'a list -> 'a list -> bool -val list_split_at : ('a -> bool) -> 'a list -> 'a list * 'a list -val list_split_by : ('a -> bool) -> 'a list -> 'a list * 'a list +val list_split_at : int -> 'a list -> 'a list*'a list +val list_split_when : ('a -> bool) -> 'a list -> 'a list * 'a list val list_split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list val list_partition_by : ('a -> 'a -> bool) -> 'a list -> 'a list list val list_firstn : int -> 'a list -> 'a list val list_last : 'a list -> 'a val list_lastn : int -> 'a list -> 'a list -val list_skipn : int -> 'a list -> 'a list +val list_skipn : int -> 'a list -> 'a list +val list_skipn_at_least : int -> 'a list -> 'a list val list_addn : int -> 'a -> 'a list -> 'a list val list_prefix_of : 'a list -> 'a list -> bool +(* [list_drop_prefix p l] returns [t] if [l=p++t] else return [l] *) val list_drop_prefix : 'a list -> 'a list -> 'a list val list_drop_last : 'a list -> 'a list (* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *) @@ -174,11 +193,11 @@ val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list val list_fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list val list_fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a val list_map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list -(* A generic cartesian product: for any operator (**), - [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]], +(* A generic cartesian product: for any operator (**), + [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]], and so on if there are more elements in the lists. *) val list_cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list -(* [list_cartesians] is an n-ary cartesian product: it iterates +(* [list_cartesians] is an n-ary cartesian product: it iterates [list_cartesian] over a list of lists. *) val list_cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list (* list_combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *) @@ -193,6 +212,7 @@ val list_union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b (*s Arrays. *) +val array_compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int val array_exists : ('a -> bool) -> 'a array -> bool val array_for_all : ('a -> bool) -> 'a array -> bool val array_for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool @@ -201,19 +221,20 @@ val array_for_all3 : ('a -> 'b -> 'c -> bool) -> val array_for_all4 : ('a -> 'b -> 'c -> 'd -> bool) -> 'a array -> 'b array -> 'c array -> 'd array -> bool val array_for_all_i : (int -> 'a -> bool) -> int -> 'a array -> bool +val array_find_i : (int -> 'a -> bool) -> 'a array -> int option 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 : +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 val array_fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c -val array_fold_left2 : +val array_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a -val array_fold_left2_i : +val array_fold_left2_i : (int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a val array_fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a val array_fold_right_from : int -> ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b @@ -224,7 +245,7 @@ val array_chop : int -> 'a array -> 'a array * 'a array val array_smartmap : ('a -> 'a) -> 'a array -> 'a array val array_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array val array_map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array -val array_map3 : +val array_map3 : ('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array val array_map_left : ('a -> 'b) -> 'a array -> 'b array val array_map_left_pair : ('a -> 'b) -> 'a array -> ('c -> 'd) -> 'c array -> @@ -236,6 +257,7 @@ val array_fold_map2' : ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c val array_distinct : 'a array -> bool val array_union_map : ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b +val array_rev_to_list : 'a array -> 'a list (*s Matrices *) @@ -245,6 +267,7 @@ val matrix_transpose : 'a list list -> 'a list list val identity : 'a -> 'a val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b +val const : 'a -> 'b -> 'a val iterate : ('a -> 'a) -> int -> 'a -> 'a val repeat : int -> ('a -> unit) -> 'a -> unit val iterate_for : int -> int -> (int -> 'a -> 'a) -> 'a -> 'a @@ -275,7 +298,7 @@ val pr_spc : unit -> std_ppcmds val pr_fnl : unit -> std_ppcmds val pr_int : int -> std_ppcmds val pr_str : string -> std_ppcmds -val pr_coma : unit -> std_ppcmds +val pr_comma : unit -> std_ppcmds val pr_semicolon : unit -> std_ppcmds val pr_bar : unit -> std_ppcmds val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds |