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