1signature Portable =
2sig
3  val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
4  val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c
5  val ## : ('a -> 'b) * ('c -> 'd) -> 'a * 'c -> 'b * 'd
6  val apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
7  val apsnd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
8  val $  : ('a -> 'b) * 'a -> 'b
9  val ?  : (bool * ('a -> 'a)) -> 'a -> 'a
10  val |> : 'a * ('a -> 'b) -> 'b
11  val |>> : ('a * 'b) * ('a -> 'c) -> ('c * 'b)
12  val ||> : ('a * 'b) * ('b -> 'c) -> ('a * 'c)
13  val ||-> : ('a * 'b) * ('a -> 'b -> 'c) -> 'c
14  val B2 : ('c -> 'd) -> ('a -> 'b -> 'c) -> 'a -> 'b -> 'd
15  val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
16  val I : 'a -> 'a
17  val K : 'a -> 'b -> 'a
18  val S : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c
19  val W : ('a -> 'a -> 'b) -> 'a -> 'b
20
21  val append : 'a list -> 'a list -> 'a list
22  val equal : ''a -> ''a -> bool
23  val strcat : string -> string -> string
24  val cons : 'a -> 'a list -> 'a list
25  val pair : 'a -> 'b -> 'a * 'b
26
27  val rpair : 'a -> 'b -> 'b * 'a
28  val swap : 'a * 'b -> 'b * 'a
29  val fst : 'a * 'b -> 'a
30  val snd : 'a * 'b -> 'b
31  val triple : 'a -> 'b -> 'c -> 'a * 'b * 'c
32  val quadruple : 'a -> 'b -> 'c -> 'd -> 'a * 'b * 'c * 'd
33
34  val can : ('a -> 'b) -> 'a -> bool
35  val total : ('a -> 'b) -> 'a -> 'b option
36  val partial : exn -> ('a -> 'b option) -> 'a -> 'b
37  val these : 'a list option -> 'a list
38
39  val assert_exn : ('a -> bool) -> 'a -> exn -> 'a
40  val with_exn : ('a -> 'b) -> 'a -> exn -> 'b
41  val finally : (unit -> unit) -> ('a -> 'b) -> ('a -> 'b)
42     (* first argument (the finally finisher) must terminate, and preferably
43        quickly, or you may mask/hide user-generated Interrupt exceptions *)
44
45  val list_of_singleton : 'a -> 'a list
46  val single : 'a -> 'a list (* synonym of list_of_singleton *)
47  val the_single : 'a list -> 'a        (* exn List.Empty if list length <> 1 *)
48  val singleton : ('a list -> 'b list) -> 'a -> 'b
49                (* singleton f x raises exn List.Empty if length (f [x]) <> 1 *)
50  val list_of_pair : 'a * 'a -> 'a list
51  val list_of_triple : 'a * 'a * 'a -> 'a list
52  val list_of_quadruple : 'a * 'a * 'a * 'a -> 'a list
53  val the_list : 'a option -> 'a list
54  val the_default : 'a -> 'a option -> 'a
55
56  val all : ('a -> bool) -> 'a list -> bool
57  val exists : ('a -> bool) -> 'a list -> bool
58  val first_opt : (int -> 'a -> 'b option) -> 'a list -> 'b option
59  val itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
60  val rev_itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
61  val foldl' : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
62  val foldr' : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
63  val foldl2' : ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
64                                              (* exn ListPair.UnequalLengths *)
65  val foldr2' : ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
66                                              (* exn ListPair.UnequalLengths *)
67  val foldl_map : ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
68  val zip3 : 'a list * 'b list * 'c list -> ('a * 'b * 'c) list
69                                              (* exn ListPair.UnequalLengths *)
70  val separate : 'a -> 'a list -> 'a list
71  val front_last : 'a list -> 'a list * 'a
72  val filter : ('a -> bool) -> 'a list -> 'a list
73  val filter_out : ('a -> bool) -> 'a list -> 'a list
74  val partition : ('a -> bool) -> 'a list -> 'a list * 'a list
75  val unzip : ('a * 'b) list -> 'a list * 'b list
76  val split : ('a * 'b) list -> 'a list * 'b list
77  val mapfilter : ('a -> 'b) -> 'a list -> 'b list
78  val flatten : 'a list list -> 'a list
79  val trypluck': ('a -> 'b option) -> 'a list -> ('b option * 'a list)
80  val funpow : int -> ('a -> 'a) -> 'a -> 'a
81  val repeat : ('a -> 'a) -> 'a -> 'a
82  val enumerate : int -> 'a list -> (int * 'a) list
83  val upto : int -> int -> int list
84  val appi : (int -> 'a -> unit) -> 'a list -> unit
85  val mapi : (int -> 'a -> 'b) -> 'a list -> 'b list
86
87  type 'a cmp = 'a * 'a -> order
88  val flip_order : order -> order
89  val flip_cmp : 'a cmp -> 'a cmp
90  val bool_compare : bool cmp
91  val list_compare : 'a cmp -> 'a list cmp
92  val option_compare : 'a cmp -> 'a option cmp
93  val pair_compare : ('a cmp * 'b cmp) -> ('a * 'b) cmp
94  val measure_cmp : ('a -> int) -> 'a cmp
95  val inv_img_cmp : ('b -> 'a) -> 'a cmp -> 'b cmp
96  val lex_cmp : ('b cmp * 'c cmp) -> (('a -> 'b) * ('a -> 'c)) -> 'a cmp
97
98  val for : int -> int -> (int -> 'a) -> 'a list
99  val for_se : int -> int -> (int -> unit) -> unit
100  val make_counter : {init:int,inc:int} -> unit -> int
101  val syncref : 'a -> {get:unit -> 'a, upd:('a -> 'b * 'a) -> 'b}
102
103  val assoc1 : ''a -> (''a * 'b) list -> (''a * 'b) option
104  val assoc2 : ''a -> ('b * ''a) list -> ('b * ''a) option
105
106  val sort : ('a -> 'a -> bool) -> 'a list -> 'a list
107  val int_sort : int list -> int list
108  val vector_topsort : int list vector -> int list
109
110  type ('a, 'b) subst = {redex: 'a, residue: 'b} list
111  val subst_assoc : ('a -> bool) -> ('a, 'b)subst -> 'b option
112  val |-> : ('a * 'b) -> {redex: 'a, residue: 'b}
113
114  val mem : ''a -> ''a list -> bool
115  val insert : ''a -> ''a list -> ''a list
116  val mk_set : ''a list -> ''a list
117  val union : ''a list -> ''a list -> ''a list
118  val U : ''a list list -> ''a list
119  val set_diff : ''a list -> ''a list -> ''a list
120  val subtract : ''a list -> ''a list -> ''a list
121  val intersect : ''a list -> ''a list -> ''a list
122  val null_intersection : ''a list -> ''a list -> bool
123  val set_eq : ''a list -> ''a list -> bool
124
125  type 'a eqf = 'a -> 'a -> bool
126  val pair_eq : 'a eqf -> 'b eqf -> ('a * 'b) eqf
127  val fst_eq : 'a eqf -> ('a * 'b) eqf
128  val inv_img_eq : ('a -> 'b) -> 'b eqf -> 'a eqf
129  val option_eq : 'a eqf -> 'a option eqf
130  val list_eq : 'a eqf -> 'a list eqf
131  val redres_eq : 'a eqf -> 'b eqf -> {redex:'a,residue:'b} eqf
132
133  val op_assoc1 : 'a eqf -> 'a -> ('a * 'b) list -> 'b option
134  val op_mem : ('a -> 'a -> bool) -> 'a -> 'a list -> bool
135  val op_insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
136  val op_mk_set : ('a -> 'a -> bool) -> 'a list -> 'a list
137  val op_union : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
138  val op_U : ('a -> 'a -> bool) -> 'a list list -> 'a list
139  val op_intersect : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
140  val op_set_diff : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
141  val op_remove : ('a -> 'b -> bool) -> 'a -> 'b list -> 'b list
142  val op_update : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
143
144  val int_to_string : int -> string
145  val quote : string -> string
146  val mlquote : string -> string
147  val enclose : string -> string -> string -> string (* enclose ld rd mid *)
148  val is_substring : string -> string -> bool
149  val prime : string -> string
150  val commafy : string list -> string list
151  val words2 : string -> string -> string list
152  val str_all : (char -> bool) -> string -> bool
153
154  val hash : int -> string -> int * int -> int
155
156  val with_flag : 'a ref * 'a -> ('b -> 'c) -> 'b -> 'c
157
158  type ('a, 'b) istream
159  val mk_istream : ('a -> 'a) -> 'a -> ('a -> 'b) -> ('a, 'b) istream
160  val next : ('a, 'b) istream -> ('a, 'b) istream
161  val state : ('a, 'b) istream -> 'b
162  val reset : ('a, 'b) istream -> ('a, 'b) istream
163
164  datatype 'a delta = SAME | DIFF of 'a
165  val delta_apply : ('a -> 'a delta) -> 'a -> 'a
166  val delta_map : ('a -> 'a delta) -> 'a list -> 'a list delta
167  val delta_pair :
168    ('a -> 'a delta) -> ('b -> 'b delta) -> 'a * 'b -> ('a * 'b) delta
169
170  val deinitcomment : string -> string
171  val deinitcommentss : substring -> substring
172
173  datatype ('a, 'b) verdict = PASS of 'a | FAIL of 'b
174  val verdict : ('a -> 'b) -> ('a -> 'c) -> 'a -> ('b, 'c * exn)verdict
175  val ?> : ('a, 'c)verdict * ('a -> ('b, 'c)verdict) -> ('b, 'c)verdict
176
177  type time      = Time.time
178  type instream  = TextIO.instream
179  type outstream = TextIO.outstream
180
181  datatype frag = datatype HOLPP.frag
182  datatype break_style = datatype HOLPP.break_style
183  val with_ppstream : OldPP.ppstream
184                       -> {add_break      : int * int -> unit,
185                           add_newline    : unit -> unit,
186                           add_string     : string -> unit,
187                           begin_block    : HOLPP.break_style -> int -> unit,
188                           clear_ppstream : unit -> unit,
189                           end_block      : unit -> unit,
190                           flush_ppstream : unit -> unit}
191
192  val dec: int ref -> unit
193  val inc: int ref -> unit
194
195  val pull_prefix : ('a -> bool) list -> 'a list -> 'a list
196
197  val explode: string -> string list
198  val implode: string list -> string
199  val ordof: string * int -> int
200  val replace_string : {from:string,to:string} -> string -> string
201
202  val time_eq: time -> time -> bool
203  val timestamp: unit -> time
204  val mk_time: {sec : Arbnum.num, usec : Arbnum.num} -> time
205  val time_to_string: time -> string
206  val dest_time: time -> {sec : Arbnum.num, usec : Arbnum.num}
207  val time_lt: time -> time -> bool
208  val time_max : time * time -> time
209  val time_maxl : time list -> time
210  val time : ('a -> 'b) -> 'a -> 'b
211  val realtime : ('a -> 'b) -> 'a -> 'b
212
213  val getEnv: string -> string option
214  val getArgs: unit -> string list
215  val argv: unit -> string list
216  val system: string -> int
217  val cd: string -> unit
218  val pwd: unit -> string
219  val listDir: string -> string list
220  val exit: unit -> 'a
221
222  val pointer_eq : 'a * 'a -> bool
223  val ref_to_int : 'a ref -> int
224
225  val end_of_stream: instream -> bool
226  val flush_out: outstream -> unit
227  val stdin   : instream
228  val std_out : outstream
229  val close_out: outstream -> unit
230  val output: outstream * string -> unit
231  val close_in: instream -> unit
232  val open_out: string -> outstream
233  val outputc: outstream -> string -> unit
234  val input_line: instream -> string
235  val open_in : string -> instream
236  exception Io of string
237
238  exception Mod
239  exception Div
240  exception Interrupt
241
242  type 'a quotation = 'a HOLPP.quotation
243  val pprint : 'a HOLPP.pprinter -> 'a -> unit
244  val norm_quote : 'a quotation -> 'a quotation
245  val quote_to_string : ('a -> string) -> 'a quotation -> string
246  val quote_to_string_list : string quotation -> string list
247
248  val catch_SIGINT : unit -> unit
249  val md5sum : string -> string
250
251  structure HOLSusp : sig
252    type 'a susp
253    val delay : (unit -> 'a) -> 'a susp
254    val force : 'a susp -> 'a
255  end
256
257  val reraise : exn -> 'a
258end
259