|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
type 'a cmp = 'a -> 'a -> int
type 'a eq = 'a -> 'a -> bool
(** Module type [S] is the one from OCaml Stdlib. *)
module type S = module type of List
module type ExtS =
sig
include S
(** {6 Equality, testing} *)
val compare : 'a cmp -> 'a list cmp
(** Lexicographic order on lists. *)
val equal : 'a eq -> 'a list eq
(** Lift equality to list type. *)
val is_empty : 'a list -> bool
(** Check whether a list is empty *)
val mem_f : 'a eq -> 'a -> 'a list -> bool
(** Same as [List.mem], for some specific equality *)
val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
(** Same as [List.for_all] but with an index *)
val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
(** Same as [List.for_all2] but returning [false] when of different length *)
val prefix_of : 'a eq -> 'a list eq
(** [prefix_of eq l1 l2] returns [true] if [l1] is a prefix of [l2], [false]
otherwise. It uses [eq] to compare elements *)
(** {6 Creating lists} *)
val interval : int -> int -> int list
(** [interval i j] creates the list [[i; i + 1; ...; j]], or [[]] when
[j <= i]. *)
val make : int -> 'a -> 'a list
(** [make n x] returns a list made of [n] times [x]. Raise
[Invalid_argument _] if [n] is negative. *)
val addn : int -> 'a -> 'a list -> 'a list
(** [addn n x l] adds [n] times [x] on the left of [l]. *)
val init : int -> (int -> 'a) -> 'a list
(** [init n f] constructs the list [f 0; ... ; f (n - 1)]. Raise
[Invalid_argument _] if [n] is negative *)
val append : 'a list -> 'a list -> 'a list
(** Like OCaml's [List.append] but tail-recursive. *)
val concat : 'a list list -> 'a list
(** Like OCaml's [List.concat] but tail-recursive. *)
val flatten : 'a list list -> 'a list
(** Synonymous of [concat] *)
(** {6 Lists as arrays} *)
val assign : 'a list -> int -> 'a -> 'a list
(** [assign l i x] sets the [i]-th element of [l] to [x], starting
from [0]. Raise [Failure _] if [i] is out of range. *)
(** {6 Filtering} *)
val filter : ('a -> bool) -> 'a list -> 'a list
(** Like OCaml [List.filter] but tail-recursive and physically returns
the original list if the predicate holds for all elements. *)
val filter2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
(** Like [List.filter] but with 2 arguments, raise [Invalid_argument _]
if the lists are not of same length. *)
val filteri : (int -> 'a -> bool) -> 'a list -> 'a list
(** Like [List.filter] but with an index starting from [0] *)
val filter_with : bool list -> 'a list -> 'a list
(** [filter_with bl l] selects elements of [l] whose corresponding element in
[bl] is [true]. Raise [Invalid_argument _] if sizes differ. *)
val map_filter : ('a -> 'b option) -> 'a list -> 'b list
(** Like [map] but keeping only non-[None] elements *)
val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
(** Like [map_filter] but with an index starting from [0] *)
val partitioni : (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
(** Like [List.partition] but with an index starting from [0] *)
(** {6 Applying functorially} *)
val map : ('a -> 'b) -> 'a list -> 'b list
(** Like OCaml [List.map] but tail-recursive *)
val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
(** Like OCaml [List.map2] but tail-recursive *)
val map_left : ('a -> 'b) -> 'a list -> 'b list
(** As [map] but ensures the left-to-right order of evaluation. *)
val map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
(** Like OCaml [List.mapi] but tail-recursive. Alternatively, like
[map] but with an index *)
val map2_i :
(int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list
(** Like [map2] but with an index *)
val map3 :
('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
(** Like [map] but for 3 lists. *)
val map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list ->
'd list -> 'e list
(** Like [map] but for 4 lists. *)
val map_of_array : ('a -> 'b) -> 'a array -> 'b list
(** [map_of_array f a] behaves as [List.map f (Array.to_list a)] *)
val map_append : ('a -> 'b list) -> 'a list -> 'b list
(** [map_append f [x1; ...; xn]] returns [f x1 @ ... @ f xn]. *)
val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
(** Like [map_append] but for two lists; raises [Invalid_argument _]
if the two lists do not have the same length. *)
val extend : bool list -> 'a -> 'a list -> 'a list
(** [extend l a [a1..an]] assumes that the number of [true] in [l] is [n];
it extends [a1..an] by inserting [a] at the position of [false] in [l] *)
val count : ('a -> bool) -> 'a list -> int
(** Count the number of elements satisfying a predicate *)
(** {6 Finding position} *)
val index : 'a eq -> 'a -> 'a list -> int
(** [index] returns the 1st index of an element in a list (counting from 1). *)
val safe_index : 'a eq -> 'a -> 'a list -> int option
(** [safe_index] returns the 1st index of an element in a list (counting from 1)
and None otherwise. *)
val index0 : 'a eq -> 'a -> 'a list -> int
(** [index0] behaves as [index] except that it starts counting at 0. *)
(** {6 Folding} *)
val fold_left_until : ('c -> 'a -> 'c CSig.until) -> 'c -> 'a list -> 'c
(** acts like [fold_left f acc s] while [f] returns
[Cont acc']; it stops returning [c] as soon as [f] returns [Stop c]. *)
val fold_right_i : (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
(** Like [List.fold_right] but with an index *)
val fold_left_i : (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
(** Like [List.fold_left] but with an index *)
val fold_right_and_left : ('b -> 'a -> 'a list -> 'b) -> 'a list -> 'b -> 'b
(** [fold_right_and_left f [a1;...;an] hd] is
[f (f (... (f (f hd an [an-1;...;a1]) an-1 [an-2;...;a1]) ...) a2 [a1]) a1 []] *)
val fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b list -> 'c list -> 'd list -> 'a
(** Like [List.fold_left] but for 3 lists; raise [Invalid_argument _] if
not all lists of the same size *)
val fold_left2_set : exn -> ('a -> 'b -> 'c -> 'b list -> 'c list -> 'a) -> 'a -> 'b list -> 'c list -> 'a
(** Fold sets, i.e. lists up to order; the folding function tells
when elements match by returning a value and raising the given
exception otherwise; sets should have the same size; raise the
given exception if no pairing of the two sets is found;;
complexity in O(n^2) *)
val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
(** [fold_left_map f e_0 [a1;...;an]] is [e_n,[k_1...k_n]]
where [(e_i,k_i)] is [f e_{i-1} ai] for each i<=n *)
val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
(** Same, folding on the right *)
val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b list -> 'c list -> 'a * 'd list
(** Same with two lists, folding on the left *)
val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a
(** Same with two lists, folding on the right *)
val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list
(** Same with three lists, folding on the left *)
val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list
(** Same with four lists, folding on the left *)
(** {6 Splitting} *)
val except : 'a eq -> 'a -> 'a list -> 'a list
(** [except eq a l] Remove all occurrences of [a] in [l] *)
val remove : 'a eq -> 'a -> 'a list -> 'a list
(** Alias of [except] *)
val remove_first : ('a -> bool) -> 'a list -> 'a list
(** Remove the first element satisfying a predicate, or raise [Not_found] *)
val extract_first : ('a -> bool) -> 'a list -> 'a list * 'a
(** Remove and return the first element satisfying a predicate,
or raise [Not_found] *)
val find_map : ('a -> 'b option) -> 'a list -> 'b
(** Returns the first element that is mapped to [Some _]. Raise [Not_found] if
there is none. *)
exception IndexOutOfRange
val goto: int -> 'a list -> 'a list * 'a list
(** [goto i l] splits [l] into two lists [(l1,l2)] such that
[(List.rev l1)++l2=l] and [l1] has length [i]. It raises
[IndexOutOfRange] when [i] is negative or greater than the
length of [l]. *)
val split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
(** [split_when p l] splits [l] into two lists [(l1,a::l2)] such that
[l1++(a::l2)=l], [p a=true] and [p b = false] for every element [b] of [l1].
if there is no such [a], then it returns [(l,[])] instead. *)
val sep_last : 'a list -> 'a * 'a list
(** [sep_last l] returns [(a,l')] such that [l] is [l'@[a]].
It raises [Failure _] if the list is empty. *)
val drop_last : 'a list -> 'a list
(** Remove the last element of the list. It raises [Failure _] if the
list is empty. This is the second part of [sep_last]. *)
val last : 'a list -> 'a
(** Return the last element of the list. It raises [Failure _] if the
list is empty. This is the first part of [sep_last]. *)
val lastn : int -> 'a list -> 'a list
(** [lastn n l] returns the [n] last elements of [l]. It raises
[Failure _] if [n] is less than 0 or larger than the length of [l] *)
val chop : int -> 'a list -> 'a list * 'a list
(** [chop i l] splits [l] into two lists [(l1,l2)] such that
[l1++l2=l] and [l1] has length [i]. It raises [Failure _] when
[i] is negative or greater than the length of [l]. *)
val firstn : int -> 'a list -> 'a list
(** [firstn n l] Returns the [n] first elements of [l]. It raises
[Failure _] if [n] negative or too large. This is the first part
of [chop]. *)
val skipn : int -> 'a list -> 'a list
(** [skipn n l] drops the [n] first elements of [l]. It raises
[Failure _] if [n] is less than 0 or larger than the length of [l].
This is the second part of [chop]. *)
val skipn_at_least : int -> 'a list -> 'a list
(** Same as [skipn] but returns [] if [n] is larger than the list of
the list. *)
val drop_prefix : 'a eq -> 'a list -> 'a list -> 'a list
(** [drop_prefix eq l1 l] returns [l2] if [l=l1++l2] else return [l]. *)
val insert : 'a eq -> 'a -> 'a list -> 'a list
(** Insert at the (first) position so that if the list is ordered wrt to the
total order given as argument, the order is preserved *)
val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
(** [share_tails l1 l2] returns [(l1',l2',l)] such that [l1] is
[l1'\@l] and [l2] is [l2'\@l] and [l] is maximal amongst all such
decompositions *)
(** {6 Association lists} *)
val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
(** Applies a function on the codomain of an association list *)
val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b
(** Like [List.assoc] but using the equality given as argument *)
val remove_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> ('a * 'b) list
(** Remove first matching element; unchanged if no such element *)
val mem_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> bool
(** Like [List.mem_assoc] but using the equality given as argument *)
val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list
(** Create a list of associations from a list of pairs *)
(** {6 Operations on lists of tuples} *)
val split : ('a * 'b) list -> 'a list * 'b list
(** Like OCaml's [List.split] but tail-recursive. *)
val combine : 'a list -> 'b list -> ('a * 'b) list
(** Like OCaml's [List.combine] but tail-recursive. *)
val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
(** Like [split] but for triples *)
val split4 : ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list
(** Like [split] but for quads *)
val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
(** Like [combine] but for triples *)
(** {6 Operations on lists seen as sets, preserving uniqueness of elements} *)
val add_set : 'a eq -> 'a -> 'a list -> 'a list
(** [add_set x l] adds [x] in [l] if it is not already there, or returns [l]
otherwise. *)
val eq_set : 'a eq -> 'a list eq
(** Test equality up to permutation. It respects multiple occurrences
and thus works also on multisets. *)
val subset : 'a list eq
(** Tell if a list is a subset of another up to permutation. It expects
each element to occur only once. *)
val merge_set : 'a cmp -> 'a list -> 'a list -> 'a list
(** Merge two sorted lists and preserves the uniqueness property. *)
val intersect : 'a eq -> 'a list -> 'a list -> 'a list
(** Return the intersection of two lists, assuming and preserving
uniqueness of elements *)
val union : 'a eq -> 'a list -> 'a list -> 'a list
(** Return the union of two lists, assuming and preserving
uniqueness of elements *)
val unionq : 'a list -> 'a list -> 'a list
(** [union] specialized to physical equality *)
val subtract : 'a eq -> 'a list -> 'a list -> 'a list
(** Remove from the first list all elements from the second list. *)
val subtractq : 'a list -> 'a list -> 'a list
(** [subtract] specialized to physical equality *)
(** {6 Uniqueness and duplication} *)
val distinct : 'a list -> bool
(** Return [true] if all elements of the list are distinct. *)
val distinct_f : 'a cmp -> 'a list -> bool
(** Like [distinct] but using the equality given as argument *)
val duplicates : 'a eq -> 'a list -> 'a list
(** Return the list of unique elements which appear at least twice. Elements
are kept in the order of their first appearance. *)
val uniquize : 'a list -> 'a list
(** Return the list of elements without duplicates.
This is the list unchanged if there was none. *)
val sort_uniquize : 'a cmp -> 'a list -> 'a list
(** Return a sorted version of a list without duplicates
according to some comparison function. *)
val min : 'a cmp -> 'a list -> 'a
(** Return minimum element according to some comparison function.
@raise Not_found on an empty list. *)
(** {6 Cartesian product} *)
val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
(** A generic binary cartesian product: for any operator (**),
[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 cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
(** [cartesians op init l] is an n-ary cartesian product: it builds
the list of all [op a1 .. (op an init) ..] for [a1], ..., [an] in
the product of the elements of the lists *)
val combinations : 'a list list -> 'a list list
(** [combinations l] returns the list of [n_1] * ... * [n_p] tuples
[[a11;...;ap1];...;[a1n_1;...;apn_pd]] whenever [l] is a list
[[a11;..;a1n_1];...;[ap1;apn_p]]; otherwise said, it is
[cartesians (::) [] l] *)
val cartesians_filter :
('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
(** Like [cartesians op init l] but keep only the tuples for which
[op] returns [Some _] on all the elements of the tuple. *)
module Smart :
sig
val map : ('a -> 'a) -> 'a list -> 'a list
(** [Smart.map f [a1...an] = List.map f [a1...an]] but if for all i
[f ai == ai], then [Smart.map f l == l] *)
end
module type MonoS = sig
type elt
val equal : elt list -> elt list -> bool
val mem : elt -> elt list -> bool
val assoc : elt -> (elt * 'a) list -> 'a
val mem_assoc : elt -> (elt * 'a) list -> bool
val remove_assoc : elt -> (elt * 'a) list -> (elt * 'a) list
val mem_assoc_sym : elt -> ('a * elt) list -> bool
end
end
include ExtS
¤ Dauer der Verarbeitung: 0.41 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
