aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/cList.mli
blob: 19eeb2509a66b3a7cd837409967c0670e5fd7f0e (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
(***********************************************************************)
(*  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       *)
(***********************************************************************)

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

  val compare : 'a cmp -> 'a list cmp
  (** Lexicographic order on lists. *)

  val equal : 'a eq -> 'a list eq
  (** Lifts equality to list type. *)

  val is_empty : 'a list -> bool
  (** Checks whether a list is empty *)

  val init : int -> (int -> 'a) -> 'a list
  (** [init n f] constructs the list [f 0; ... ; f (n - 1)]. *)

  val mem_f : 'a eq -> 'a -> 'a list -> bool
  (* Same as [List.mem], for some specific equality *)

  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 (but considering multiple occurrences) *)

  val intersect : 'a eq -> 'a list -> 'a list -> 'a list
  val union : 'a eq -> 'a list -> 'a list -> 'a list
  val unionq : 'a list -> 'a list -> 'a list
  val subtract : 'a eq -> 'a list -> 'a list -> 'a list
  val subtractq : 'a list -> 'a list -> 'a list

  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 "List.make"] if [n] is negative. *)

  val assign : 'a list -> int -> 'a -> 'a list
  (** [assign l i x] set the [i]-th element of [l] to [x], starting from [0]. *)

  val distinct : 'a list -> bool
  (** Return [true] if all elements of the list are distinct. *)

  val distinct_f : 'a cmp -> 'a list -> bool

  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 filter2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
  val map_filter : ('a -> 'b option) -> 'a list -> 'b list
  val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list

  val filter_with : bool list -> 'a list -> 'a list
  (** [filter_with b a] selects elements of [a] whose corresponding element in
      [b] is [true]. Raise [Invalid_argument _] when sizes differ. *)

  val smartmap : ('a -> 'a) -> 'a list -> 'a list
  (** [smartmap f [a1...an] = List.map f [a1...an]] but if for all i
    [f ai == ai], then [smartmap f l == l] *)

  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
  (** As [map] but with the index, which starts from [0]. *)

  val map2_i :
    (int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list
  val map3 :
    ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
  val map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list ->
    'd list -> 'e list
  val filteri : (int -> 'a -> bool) -> 'a list -> 'a list

  val smartfilter : ('a -> bool) -> 'a list -> 'a list
  (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
    [f ai = true], then [smartfilter f l == l] *)

  val index : 'a eq -> 'a -> 'a list -> int
  (** [index] returns the 1st index of an element in a list (counting from 1). *)

  val index0 : 'a eq -> 'a -> 'a list -> int
  (** [index0] behaves as [index] except that it starts counting at 0. *)

  val iteri :  (int -> 'a -> unit) -> 'a list -> unit
  (** As [iter] but with the index argument (starting from 0). *)

  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
  val fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
  val fold_right_and_left :
      ('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a
  val fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b list -> 'c list -> 'd list -> 'a
  val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
  val except : 'a eq -> 'a -> 'a list -> 'a list
  val remove : 'a eq -> 'a -> 'a list -> 'a list

  val remove_first : ('a -> bool) -> 'a list -> 'a list
  (** Remove the first element satisfying a predicate, or raise [Not_found] *)

  val insert : ('a -> 'a -> bool) -> '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 for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
  val sep_last : 'a list -> 'a * 'a list

  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. *)

  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 and de-duplicated version of a list,
      according to some comparison function. *)

  val merge_uniq : 'a cmp -> 'a list -> 'a list -> 'a list
  (** Merge two sorted lists and preserves the uniqueness property. *)

  val subset : 'a list -> 'a list -> bool

  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] *)

  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
  val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
  val firstn : int -> 'a list -> 'a list
  val last : 'a list -> 'a
  val lastn : int -> 'a list -> 'a list
  val skipn : int -> 'a list -> 'a list
  val skipn_at_least : int -> 'a list -> 'a list

  val addn : int -> 'a -> 'a list -> 'a list
  (** [addn n x l] adds [n] times [x] on the left of [l]. *)

  val prefix_of : 'a eq -> 'a list -> 'a list -> bool
  (** [prefix_of l1 l2] returns [true] if [l1] is a prefix of [l2], [false]
      otherwise. *)

  val drop_prefix : 'a eq -> 'a list -> 'a list -> 'a list
  (** [drop_prefix p l] returns [t] if [l=p++t] else return [l]. *)

  val drop_last : 'a list -> 'a list

  val map_append : ('a -> 'b list) -> 'a list -> 'b list
  (** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)]. *)

  val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
  (** As [map_append]. Raises [Invalid_argument _] if the two lists don't have 
      the same length. *)

  val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list

  val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c 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 fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
  val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
  val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b
  val remove_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> ('a * 'b) list
  val mem_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> bool

  val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
  (** A generic 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] is an n-ary cartesian product: it iterates
    [cartesian] over a list of lists.  *)

  val combinations : 'a list list -> 'a list list
  (** combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)

  val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list

  val cartesians_filter :
    ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
  (** Keep only those products that do not return None *)

  val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list

  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