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