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
|
(***********************************************************************)
(* 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 *)
(***********************************************************************)
(*i $Id$ i*)
(*i*)
open Pp
(*i*)
(* This module contains numerous utility functions on strings, lists,
arrays, etc. *)
(*s Errors. [Anomaly] is used for system errors and [UserError] for the
user's ones. *)
exception Anomaly of string * std_ppcmds
val anomaly : string -> 'a
val anomalylabstrm : string -> std_ppcmds -> 'a
exception UserError of string * std_ppcmds
val error : string -> 'a
val errorlabstrm : string -> std_ppcmds -> 'a
(* [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
type loc = int * int
type 'a located = loc * 'a
val dummy_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
(*s Chars. *)
val is_letter : char -> bool
val is_digit : char -> bool
(*s Strings. *)
val explode : string -> string list
val implode : string list -> string
val parse_loadpath : string -> string list
module Stringset : Set.S with type elt = string
module Stringmap : Map.S with type key = string
val stringmap_to_list : 'a Stringmap.t -> (string * 'a) list
val stringmap_dom : 'a Stringmap.t -> string list
(*s Lists. *)
val list_add_set : 'a -> 'a list -> 'a list
val list_intersect : 'a list -> 'a list -> 'a list
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)]] *)
val list_tabulate : (int -> 'a) -> int -> 'a list
val list_assign : 'a list -> int -> 'a -> 'a list
val list_distinct : 'a list -> bool
val list_filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> '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
val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
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_index : 'a -> 'a list -> int
val list_iter_i : (int -> 'a -> unit) -> 'a list -> unit
val list_fold_left_i : (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
val list_fold_right_and_left :
('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a
val list_for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
val list_except : 'a -> 'a list -> 'a list
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
val list_subset : 'a list -> 'a list -> bool
val list_splitby : ('a -> bool) -> 'a list -> 'a list * 'a list
val list_split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c 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_prefix_of : 'a list -> 'a list -> bool
(* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
val list_map_append : ('a -> 'b list) -> 'a list -> 'b list
(* 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
val list_join_map : ('a -> 'b list) -> 'a list -> 'b list
(* [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_map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
(*s Arrays. *)
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
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_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 :
('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c 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
val array_fold_right_from : int -> ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
val array_app_tl : 'a array -> 'a list -> 'a list
val array_list_of_tl : 'a array -> 'a list
val array_map_to_list : ('a -> 'b) -> 'a array -> 'b list
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 :
('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
(*s Matrices *)
val matrix_transpose : 'a list list -> 'a list list
(*s Functions. *)
val identity : 'a -> 'a
val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
val iterate : ('a -> 'a) -> int -> 'a -> 'a
val repeat : int -> ('a -> unit) -> 'a -> unit
val iterate_for : int -> int -> (int -> 'a -> 'a) -> 'a -> 'a
(*s Misc. *)
type ('a,'b) union = Inl of 'a | Inr of 'b
module Intset : Set.S with type elt = int
val intset_exists : (int -> bool) -> Intset.t -> bool
module Intmap : Map.S with type key = int
val intmap_in_dom : int -> 'a Intmap.t -> bool
val intmap_to_list : 'a Intmap.t -> (int * 'a) list
val intmap_inv : 'a Intmap.t -> 'a -> int list
val interval : int -> int -> int list
val in_some : 'a -> 'a option
val out_some : 'a option -> 'a
val option_app : ('a -> 'b) -> 'a option -> 'b option
val option_cons : 'a option -> 'a list -> 'a list
val option_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option ->
'c option -> 'a
val option_iter : ('a -> unit) -> 'a option -> unit
val option_compare : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool
val option_smartmap : ('a -> 'a) -> 'a option -> 'a option
(* 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. *)
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_semicolon : unit -> std_ppcmds
val pr_bar : unit -> std_ppcmds
val pr_ord : int -> std_ppcmds
val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
val prlist_with_sep :
(unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b list -> std_ppcmds
val prvect_with_sep :
(unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b array -> std_ppcmds
val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
(*s 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. *)
val heap_size : unit -> int
val heap_size_kb : unit -> int
(*s Coq interruption: set the following boolean reference to interrupt Coq
(it eventually raises [Break], simulating a Ctrl-C) *)
val interrupt : bool ref
val check_for_interrupt : unit -> unit
|
