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