diff options
Diffstat (limited to 'lib/util.mli')
| -rw-r--r-- | lib/util.mli | 146 |
1 files changed, 89 insertions, 57 deletions
diff --git a/lib/util.mli b/lib/util.mli index e5b5f8c6..1fec2295 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -1,21 +1,19 @@ -(***********************************************************************) -(* 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 *) -(***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) -(*i $Id: util.mli 13492 2010-10-04 21:20:01Z herbelin $ i*) - -(*i*) open Pp -(*i*) +open Compat -(* This module contains numerous utility functions on strings, lists, +(** This module contains numerous utility functions on strings, lists, arrays, etc. *) -(*s Errors. [Anomaly] is used for system errors and [UserError] for the +(** {6 ... } *) +(** Errors. [Anomaly] is used for system errors and [UserError] for the user's ones. *) exception Anomaly of string * std_ppcmds @@ -29,9 +27,7 @@ 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 +(** [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 *) @@ -39,57 +35,59 @@ val todo : string -> unit exception Timeout -type loc = Compat.loc +type loc = Loc.t type 'a located = loc * 'a val unloc : loc -> int * int val make_loc : int * int -> loc val dummy_loc : loc +val join_loc : loc -> loc -> loc + val anomaly_loc : loc * string * std_ppcmds -> 'a val user_err_loc : loc * string * std_ppcmds -> 'a val invalid_arg_loc : loc * string -> 'a -val join_loc : loc -> loc -> loc val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit val down_located : ('a -> 'b) -> 'a located -> 'b -(* Like [Exc_located], but specifies the outermost file read, the +(** Like [Exc_located], but specifies the outermost file read, the input buffer associated to the location of the error (or the module name if boolean is true), and the error itself. *) exception Error_in_file of string * (bool * string * loc) * exn -(* Mapping under pairs *) +(** Mapping under pairs *) val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b +val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b -(* Going down pairs *) +(** Going down pairs *) val down_fst : ('a -> 'b) -> 'a * 'c -> 'b val down_snd : ('a -> 'b) -> 'c * 'a -> 'b -(* Mapping under triple *) +(** 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 *) +(** {6 Projections from triplets } *) val pi1 : 'a * 'b * 'c -> 'a val pi2 : 'a * 'b * 'c -> 'b val pi3 : 'a * 'b * 'c -> 'c -(*s Chars. *) +(** {6 Chars. } *) val is_letter : char -> bool val is_digit : char -> bool val is_ident_tail : char -> bool val is_blank : char -> bool -(*s Strings. *) +(** {6 Strings. } *) val explode : string -> string list val implode : string list -> string @@ -116,9 +114,10 @@ val check_ident_soft : string -> unit val lowercase_first_char_utf8 : string -> string val ascii_of_ident : string -> string -(*s Lists. *) +(** {6 Lists. } *) val list_compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int +val list_equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool 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 @@ -126,8 +125,8 @@ val list_union : 'a list -> 'a list -> 'a list val list_unionq : 'a list -> 'a list -> 'a list val list_subtract : 'a list -> 'a list -> 'a list val list_subtractq : 'a list -> 'a list -> 'a list -val list_chop : int -> 'a list -> 'a list * 'a list -(* [list_tabulate f n] builds [[f 0; ...; f (n-1)]] *) + +(** [list_tabulate f n] builds [[f 0; ...; f (n-1)]] *) val list_tabulate : (int -> 'a) -> int -> 'a list val list_make : int -> 'a -> 'a list val list_assign : 'a list -> int -> 'a -> 'a list @@ -135,7 +134,9 @@ val list_distinct : 'a list -> bool val list_duplicates : 'a list -> 'a list val list_filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list val list_map_filter : ('a -> 'b option) -> 'a list -> 'b list -(* [list_smartmap f [a1...an] = List.map f [a1...an]] but if for all i +val list_map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list + +(** [list_smartmap f [a1...an] = List.map f [a1...an]] but if for all i [ f ai == ai], then [list_smartmap f l==l] *) val list_smartmap : ('a -> 'a) -> 'a list -> 'a list val list_map_left : ('a -> 'b) -> 'a list -> 'b list @@ -148,12 +149,21 @@ 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) *) + +(** [list_smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i + [f ai = true], then [list_smartfilter f l==l] *) +val list_smartfilter : ('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_index_f : ('a -> 'a -> bool) -> '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 -(* [list_index0] behaves as [list_index] except that it starts counting at 0 *) + +(** [list_index0] behaves as [list_index] except that it starts counting at 0 *) val list_index0 : 'a -> 'a list -> int +val list_index0_f : ('a -> 'a -> bool) -> 'a -> 'a list -> int val list_iter3 : ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list -> 'c list -> unit val list_iter_i : (int -> 'a -> unit) -> 'a list -> unit val list_fold_right_i : (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b @@ -166,15 +176,18 @@ val list_except : 'a -> 'a list -> 'a list val list_remove : 'a -> 'a list -> 'a list val list_remove_first : 'a -> 'a list -> 'a list val list_remove_assoc_in_triple : 'a -> ('a * 'b * 'c) list -> ('a * 'b * 'c) list +val list_assoc_snd_in_triple : 'a -> ('a * 'b * 'c) list -> 'b val list_for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool val list_sep_last : 'a list -> 'a * 'a list val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b val list_try_find : ('a -> 'b) -> 'a list -> 'b val list_uniquize : 'a list -> 'a list -(* merges two sorted lists and preserves the uniqueness property: *) + +(** 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 : int -> 'a list -> 'a list*'a list +val list_chop : int -> 'a list -> 'a list * 'a list +(* former [list_split_at] was a duplicate of [list_chop] *) val list_split_when : ('a -> bool) -> 'a list -> 'a list * 'a list val list_split_by : ('a -> bool) -> 'a list -> 'a list * 'a list val list_split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list @@ -186,28 +199,36 @@ 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] *) + +(** [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)] *) + +(** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *) val list_map_append : ('a -> 'b list) -> 'a list -> 'b list val list_join_map : ('a -> 'b list) -> 'a list -> 'b list -(* raises [Invalid_argument] if the two lists don't have the same length *) + +(** raises [Invalid_argument] if the two lists don't have the same length *) val list_map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list -(* [list_fold_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]] + +(** [list_fold_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]] where [(e_i,k_i)=f e_{i-1} l_i] *) 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 (**), +val list_assoc_f : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b + +(** 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]] *) + +(** list_combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *) val list_combinations : 'a list list -> 'a list list val list_combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list @@ -219,9 +240,10 @@ val list_cartesians_filter : val list_union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b -(*s Arrays. *) +(** {6 Arrays. } *) val array_compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int +val array_equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool 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 @@ -243,6 +265,8 @@ val array_fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c val array_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a +val array_fold_left3 : + ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'a 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 @@ -268,11 +292,16 @@ 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 *) +(** {6 Streams. } *) + +val stream_nth : int -> 'a Stream.t -> 'a +val stream_njunk : int -> 'a Stream.t -> unit + +(** {6 Matrices. } *) val matrix_transpose : 'a list list -> 'a list list -(*s Functions. *) +(** {6 Functions. } *) val identity : 'a -> 'a val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b @@ -302,12 +331,12 @@ val intmap_inv : 'a Intmap.t -> 'a -> int list val interval : int -> int -> int list -(* In [map_succeed f l] an element [a] is removed if [f a] raises *) -(* [Failure _] otherwise behaves as [List.map f l] *) +(** In [map_succeed f l] an element [a] is removed if [f a] raises + [Failure _] otherwise behaves as [List.map f l] *) val map_succeed : ('a -> 'b) -> 'a list -> 'b list -(*s Pretty-printing. *) +(** {6 Pretty-printing. } *) val pr_spc : unit -> std_ppcmds val pr_fnl : unit -> std_ppcmds @@ -322,7 +351,8 @@ val pr_opt_no_spc : ('a -> std_ppcmds) -> 'a option -> std_ppcmds val nth : int -> std_ppcmds val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds -(* unlike all other functions below, [prlist] works lazily. + +(** unlike all other functions below, [prlist] works lazily. if a strict behavior is needed, use [prlist_strict] instead. *) val prlist_strict : ('a -> std_ppcmds) -> 'a list -> std_ppcmds val prlist_with_sep : @@ -339,34 +369,36 @@ 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. *) +(** {6 Memoization. } *) -(* General comments on 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 *) + + 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) *) + +(** 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]. *) +(** 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). *) +(** {6 Size of an ocaml value (in words, bytes and kilobytes). } *) val size_w : 'a -> int val size_b : 'a -> int val size_kb : 'a -> int -(*s Total size of the allocated ocaml heap. *) +(** {6 Total size of the allocated ocaml heap. } *) val heap_size : unit -> int val heap_size_kb : unit -> int -(*s Coq interruption: set the following boolean reference to interrupt Coq +(** {6 ... } *) +(** Coq interruption: set the following boolean reference to interrupt Coq (it eventually raises [Break], simulating a Ctrl-C) *) val interrupt : bool ref |