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