1signature aiLib =
2sig
3
4  include Abbrev
5
6  (* misc *)
7  val number_fst : int -> 'a list -> (int * 'a) list
8  val number_snd : int -> 'a list -> ('a * int) list
9  val print_endline : string -> unit
10  val vector_to_list : 'a vector -> 'a list
11  val hash_string : string -> int
12  val hash_string_mod : int -> string -> int
13
14  (* comparisons *)
15  val cpl_compare :
16    ('a * 'b -> order) ->
17    ('c * 'd -> order) ->
18    ('a * 'c) * ('b * 'd) -> order
19  val triple_compare :
20    ('a * 'b -> order) ->
21    ('c * 'd -> order) ->
22    ('e * 'f -> order) ->
23    ('a * 'c * 'e) * ('b * 'd * 'f) -> order
24  val fst_compare : ('a * 'b -> 'c) -> ('a * 'd) * ('b * 'e) -> 'c
25  val snd_compare : ('a * 'b -> 'c) -> ('d * 'a) * ('e * 'b) -> 'c
26  val goal_compare : goal * goal -> order
27  val compare_rmin : (('a * real) * ('a * real)) -> order
28  val compare_rmax : (('a * real) * ('a * real)) -> order
29  val compare_imin : (('a * int) * ('a * int)) -> order
30  val compare_imax : (('a * int) * ('a * int)) -> order
31  val list_rmax : real list -> real
32  val list_imax : int list -> int
33  val list_imin : int list -> int
34  val tmsize_compare : term * term -> order
35  val all_subterms : term -> term list
36  val div_equal : int -> int -> int list
37
38  (* time *)
39  val add_time : ('a -> 'b) -> 'a -> 'b * real
40  val print_time : string -> real -> unit
41  val total_time : real ref -> ('a -> 'b) -> 'a -> 'b
42
43  (* commands *)
44  val mkDir_err : string -> unit
45  val run_cmd : string -> unit
46  val cmd_in_dir : string -> string -> unit
47  val exists_file : string -> bool
48  val remove_file : string -> unit
49  val clean_dir : string -> unit
50  val clean_rec_dir : string -> unit
51
52  (* dictionnary *)
53  val dfind  : 'a -> ('a, 'b) Redblackmap.dict -> 'b
54  val dmem   : 'a -> ('a, 'b) Redblackmap.dict -> bool
55  val drem   : 'a -> ('a, 'b) Redblackmap.dict -> ('a, 'b) Redblackmap.dict
56  val dadd   :
57    'a -> 'b -> ('a, 'b) Redblackmap.dict -> ('a, 'b) Redblackmap.dict
58  val daddl  :
59    ('a * 'b) list -> ('a, 'b) Redblackmap.dict -> ('a, 'b) Redblackmap.dict
60  val dempty : ('a * 'a -> order) -> ('a, 'b) Redblackmap.dict
61  val dnew   : ('a * 'a -> order) -> ('a * 'b) list ->
62    ('a, 'b) Redblackmap.dict
63  val dlist  : ('a, 'b) Redblackmap.dict -> ('a * 'b) list
64  val dlength : ('a, 'b) Redblackmap.dict -> int
65  val dapp : ('a * 'b -> unit) -> ('a, 'b) Redblackmap.dict -> unit
66  val dkeys : ('a, 'b) Redblackmap.dict -> 'a list
67  val dmap  : ('a * 'b -> 'c) ->
68    ('a, 'b) Redblackmap.dict -> ('a, 'c) Redblackmap.dict
69  val dfoldl : ('a * 'b * 'c -> 'c) -> 'c -> ('a, 'b) Redblackmap.dict -> 'c
70  val inv_dict :
71    ('a * 'a -> order) ->
72    ('b, 'a) Redblackmap.dict -> ('a, 'b) Redblackmap.dict
73  val dregroup : ('a * 'a -> order) -> ('a * 'b) list ->
74    ('a, 'b list) Redblackmap.dict
75  val distrib : ('a * 'b list) list -> ('a * 'b) list
76  val dappend : 'a * 'b ->
77    ('a, 'b list) Redblackmap.dict -> ('a, 'b list) Redblackmap.dict
78  val dappendl : ('a * 'b) list ->
79    ('a, 'b list) Redblackmap.dict -> ('a, 'b list) Redblackmap.dict
80  val dconcat : ('a * 'a -> order) ->
81    ('a, 'b list) Redblackmap.dict list -> ('a, 'b list) Redblackmap.dict
82
83  val dset : ('a * 'a -> order) -> 'a list ->
84    ('a, unit) Redblackmap.dict
85  val daddset : 'a list ->
86    ('a, unit) Redblackmap.dict -> ('a, unit) Redblackmap.dict
87  val union_dict : ('a * 'a -> order) ->
88     ('a, 'b) Redblackmap.dict list -> ('a, 'b) Redblackmap.dict
89  val count_dict :
90    ('a, int) Redblackmap.dict -> 'a list -> ('a, int) Redblackmap.dict
91
92  (* list *)
93  val is_singleton : 'a list -> bool
94  val range : (int * int) * (int -> 'a) -> 'a list
95  val one_in_n : int -> int -> 'a list -> 'a list
96  val map_snd : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
97  val map_fst : ('a -> 'b) -> ('a * 'c) list -> ('b * 'c) list
98  val map_assoc : ('a -> 'b) -> 'a list -> ('a * 'b) list
99  val all_pairs : 'a list -> ('a * 'a) list
100  val cartesian_product : 'a list -> 'b list -> ('a * 'b) list
101  val cartesian_productl : 'a list list -> 'a list list
102  val findSome  : ('a -> 'b option) -> 'a list -> 'b option
103  val first_n   : int -> 'a list -> 'a list
104  val first_test_n : ('a -> bool) -> int -> 'a list -> 'a list
105  val part_n : int -> 'a list -> ('a list * 'a list)
106  val part_pct :  real -> 'a list -> 'a list * 'a list
107  val part_group : int list -> 'a list -> 'a list list
108  val number_list : int -> 'a list -> (int * 'a) list
109  val list_diff : ''a list -> ''a list -> ''a list
110  val subset : ''a list -> ''a list -> bool
111  val mk_fast_set : ('a * 'a -> order) -> 'a list -> 'a list
112  val mk_string_set : string list -> string list
113  val mk_term_set : term list -> term list
114  val mk_type_set : hol_type list -> hol_type list
115  val mk_sameorder_set : ('a * 'a -> order) -> 'a list -> 'a list
116  val dict_sort : ('a * 'a -> order) -> 'a list -> 'a list
117  val topo_sort : ('a * 'a -> order) -> ('a * 'a list) list -> 'a list
118  val sort_thyl : string list -> string list
119  val fold_left : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
120  val mk_batch : int -> 'a list -> 'a list list
121  val mk_batch_full : int -> 'a list -> 'a list list
122  val cut_n : int -> 'a list -> 'a list list
123  val cut_modulo : int -> 'a list -> 'a list list
124  val number_partition : int -> int -> int list list
125  val duplicate : int -> 'a list -> 'a list
126  val indent: int -> string
127  val list_combine : 'a list list -> 'a list list
128  val combine_triple : 'a list * 'b list * 'c list -> ('a * 'b * 'c) list
129  val split_triple : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
130  val quintuple_of_list : 'a list -> 'a * 'a * 'a * 'a * 'a
131  val interleave : int -> 'a list -> 'a list -> 'a list
132  val inter_increasing : int list -> int list -> int list
133  val best_n : ('a * 'a -> order) -> int -> 'a list -> 'a list
134  val best_n_rmaxu : ('a * 'a -> order) -> int -> ('a * real) list -> 'a list
135
136  (* randomness, probability and distributions *)
137  val random_real : unit -> real
138  val shuffle   : 'a list -> 'a list
139  val random_elem : 'a list -> 'a
140  val random_int : (int * int) -> int (* uses random_elem *)
141  val random_subset : int -> 'a list -> 'a list
142  val mk_cumul : ('a * real) list -> ('a * real) list * real
143  val select_in_cumul : ('a * real) list * real -> 'a
144  val select_in_distrib : ('a * real) list -> 'a
145  val select_in_distrib_seeded : real -> ('a * real) list -> 'a
146  val best_in_distrib : ('a * real) list -> 'a
147  val uniform_proba : int -> real list
148  val normalize_proba : real list -> real list
149  val uniform_distrib : 'a  list -> ('a * real) list
150  val normalize_distrib : ('a * real) list -> ('a * real) list
151
152  (* input/output *)
153  val reall_to_string : real list -> string
154  val realll_to_string : real list list -> string
155  val string_to_reall : string -> real list
156  val string_to_realll : string -> real list list
157  val string_of_goal : goal -> string
158  val string_of_goal_noquote : goal -> string
159  val trace_tacl : tactic list -> goal -> unit
160  val readl : string -> string list
161  val bare_readl : string -> string list
162  val readl_empty : string -> string list
163  val append_file : string -> string -> unit
164  val write_file : string -> string -> unit
165  val erase_file : string -> unit
166  val append_endline : string -> string -> unit
167  val writel : string -> string list -> unit
168  val writel_path : string -> string -> string list -> unit
169  val debug_flag  : bool ref
170  val debug : string -> unit
171  val debugf : string -> ('a -> string) -> 'a -> unit
172  val stream_to_string :
173    string -> (TextIO.outstream -> unit) -> string list
174  val write_texgraph :
175    string -> string * string -> (int * int) list -> unit
176  val readl_rm : string -> string list
177  val writel_atomic : string -> string list -> unit
178  val listDir : string -> string list
179
180  (* parse *)
181  val hd_string : string -> char
182  val tl_string : string -> string
183  val unquote_string : string -> string
184  val drop_sig : string -> string
185  val subst_sl : (string * string) -> string list -> string list
186  val split_sl : ''a -> ''a list -> ''a list * ''a list
187  val rpt_split_sl : ''a -> ''a list -> ''a list list
188  val split_level : string -> string list -> (string list * string list)
189  val rpt_split_level : string -> string list -> string list list
190  val split_string : string -> string -> (string * string)
191  val rm_prefix : string -> string -> string
192  val rm_squote : string -> string
193  val rm_space  : string -> string
194  datatype lisp = Lterm of lisp list | Lstring of string
195  val lisp_lexer : string -> string list
196  val lisp_parser : string -> lisp list
197  val term_of_lisp : lisp -> term
198
199  (* escape *)
200  val escape : string -> string
201  val unescape : string -> string
202
203  (* statistics *)
204  val incr : int ref -> unit
205  val decr : int ref -> unit
206  val sum_real : real list -> real
207  val average_real : real list -> real
208  val average_int: int list -> real
209  val standard_deviation : real list -> real
210  val absolute_deviation : real list -> real
211  val sum_int : int list -> int
212  val int_div : int -> int -> real
213  val int_pow : int -> int -> int
214  val int_product : int list -> int
215  val bin_rep : int -> int -> real list
216  val pow : real -> int -> real
217  val approx : int -> real -> real
218  val percent : real -> real
219  val pad : int -> string -> string -> string
220  val tts : term -> string
221  val its : int -> string
222  val rts : real -> string
223  val bts : bool -> string
224  val string_to_bool : string -> bool
225  val rts_round : int -> real -> string
226  val pretty_real : real -> string
227  val epsilon : real
228  val interval : real -> real * real -> real list
229
230  (* term *)
231  val rename_bvarl : (string -> string) -> term -> term
232  val rename_allvar : term -> term
233  val all_bvar : term -> term list
234  val strip_type : hol_type -> (hol_type list * hol_type)
235  val strip_type_n : int -> hol_type -> (hol_type list * hol_type)
236  val rpt_fun_type : int -> hol_type -> hol_type
237  val has_boolty : term -> bool
238  val only_concl : thm -> term
239  val list_mk_binop : term -> term list -> term
240  val strip_binop : term -> term -> term list
241  val arity_of : term -> int
242
243  (* term data *)
244  val enc_real : real -> HOLsexp_dtype.t
245  val dec_real : HOLsexp_dtype.t -> real option
246  val write_tmdata :
247    ((term -> HOLsexp_dtype.t) -> 'a HOLsexp.encoder) * ('a -> term list) ->
248    string -> 'a -> unit
249  val read_tmdata :
250    ((HOLsexp_dtype.t -> term option) -> HOLsexp_dtype.t -> 'a option) ->
251    string -> 'a
252  val write_data : ('a -> HOLsexp_dtype.t) -> string -> 'a -> unit
253  val read_data : (HOLsexp_dtype.t -> 'a option) -> string -> 'a
254  val export_terml : string -> term list -> unit
255  val import_terml : string -> term list
256  val export_goal : string -> goal -> unit
257  val import_goal : string -> goal
258
259  (* thread *)
260  val interruptkill : Thread.thread -> unit
261
262  (* sigobj *)
263  val sigobj_theories : unit -> string list
264  val load_sigobj : unit -> unit
265  val link_sigobj : string -> unit
266
267end
268