1signature Lib = 2sig 3 datatype 'a delta = SAME | DIFF of 'a 4 datatype frag = datatype HOLPP.frag 5 datatype ('a, 'b) verdict = PASS of 'a | FAIL of 'b 6 type 'a cmp = 'a * 'a -> order 7 type 'a eqf = 'a -> 'a -> bool 8 type ('a, 'b) istream 9 type ('a, 'b) subst = {redex: 'a, residue: 'b} list 10 type 'a set = 'a HOLset.set 11 val $ : ('a -> 'b) * 'a -> 'b 12 val ## : ('a -> 'b) * ('c -> 'd) -> 'a * 'c -> 'b * 'd 13 val ?> : ('a, 'c)verdict * ('a -> ('b, 'c)verdict) -> ('b, 'c)verdict 14 val |-> : ('a * 'b) -> {redex: 'a, residue: 'b} 15 val |> : 'a * ('a -> 'b) -> 'b 16 val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c 17 val I : 'a -> 'a 18 val K : 'a -> 'b -> 'a 19 val S : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c 20 val U : ''a list list -> ''a list 21 val W : ('a -> 'a -> 'b) -> 'a -> 'b 22 val IN : 'a * 'a set -> bool 23 val Un : 'a set * 'a set -> 'a set 24 val Isct : 'a set * 'a set -> 'a set 25 val -- : 'a set * 'a set -> 'a set 26 27 val all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool 28 val all : ('a -> bool) -> 'a list -> bool 29 val apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c 30 val append : 'a list -> 'a list -> 'a list 31 val appi : (int -> 'a -> unit) -> 'a list -> unit 32 val apnth : ('a -> 'a) -> int -> 'a list -> 'a list 33 val apsnd : ('a -> 'b) -> 'c * 'a -> 'c * 'b 34 val assert : ('a -> bool) -> 'a -> 'a 35 val assert_exn : ('a -> bool) -> 'a -> exn -> 'a 36 val assoc1 : ''a -> (''a * 'b) list -> (''a * 'b) option 37 val assoc2 : ''a -> ('b * ''a) list -> ('b * ''a) option 38 val assoc : ''a -> (''a * 'b) list -> 'b 39 val bool_compare : bool cmp 40 val butlast : 'a list -> 'a list 41 val can : ('a -> 'b) -> 'a -> bool 42 val combine : 'a list * 'b list -> ('a * 'b) list 43 val commafy : string list -> string list 44 val cons : 'a -> 'a list -> 'a list 45 val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c 46 val deinitcomment : string -> string 47 val deinitcommentss : substring -> substring 48 val delete_trailing_wspace : string -> string 49 val delta_apply : ('a -> 'a delta) -> 'a -> 'a 50 val delta_map : ('a -> 'a delta) -> 'a list -> 'a list delta 51 val delta_pair : 52 ('a -> 'a delta) -> ('b -> 'b delta) -> 'a * 'b -> ('a * 'b) delta 53 val dict_topsort : ('a, 'a list) Redblackmap.dict -> 'a list 54 val el : int -> 'a list -> 'a 55 val end_itlist : ('a -> 'a -> 'a) -> 'a list -> 'a 56 val end_real_time : Timer.real_timer -> unit 57 val end_time : Timer.cpu_timer -> unit 58 val enumerate : int -> 'a list -> (int * 'a) list 59 val equal : ''a -> ''a -> bool 60 val exists : ('a -> bool) -> 'a list -> bool 61 val extract_pc : string -> string * int (* "pc" = "prime count" *) 62 val filter : ('a -> bool) -> 'a list -> 'a list 63 val first : ('a -> bool) -> 'a list -> 'a 64 val first_opt : (int -> 'a -> 'b option) -> 'a list -> 'b option 65 val flatten : 'a list list -> 'a list 66 val flip_cmp : 'a cmp -> 'a cmp 67 val flip_order : order -> order 68 val foldl_map : ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list 69 val for : int -> int -> (int -> 'a) -> 'a list 70 val for_se : int -> int -> (int -> unit) -> unit 71 val front_last : 'a list -> 'a list * 'a 72 val fst : 'a * 'b -> 'a 73 val funpow : int -> ('a -> 'a) -> 'a -> 'a 74 val get_first : ('a -> 'b option) -> 'a list -> 'b option 75 val hash : int -> string -> int * int -> int 76 val index : ('a -> bool) -> 'a list -> int 77 val insert : ''a -> ''a list -> ''a list 78 val int_sort : int list -> int list 79 val int_to_string : int -> string 80 val intersect : ''a list -> ''a list -> ''a list 81 val inv_img_cmp : ('b -> 'a) -> 'a cmp -> 'b cmp 82 val is_substring : string -> string -> bool 83 val itlist2 : ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c 84 val itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b 85 val last : 'a list -> 'a 86 val lex_cmp : ('b cmp * 'c cmp) -> (('a -> 'b) * ('a -> 'c)) -> 'a cmp 87 val list_compare : 'a cmp -> 'a list cmp 88 val list_eq : 'a eqf -> 'a list eqf 89 val list_of_pair : 'a * 'a -> 'a list 90 val list_of_quadruple : 'a * 'a * 'a * 'a -> 'a list 91 val list_of_singleton : 'a -> 'a list 92 val list_of_triple : 'a * 'a * 'a -> 'a list 93 val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list 94 val mapfilter : ('a -> 'b) -> 'a list -> 'b list 95 val mapi : (int -> 'a -> 'b) -> 'a list -> 'b list 96 val mapshape : int list -> ('a list -> 'b) list -> 'a list -> 'b list 97 val measure_cmp : ('a -> int) -> 'a cmp 98 val mem : ''a -> ''a list -> bool 99 val mk_istream : ('a -> 'a) -> 'a -> ('a -> 'b) -> ('a, 'b) istream 100 val mk_set : ''a list -> ''a list 101 val mlquote : string -> string 102 val next : ('a, 'b) istream -> ('a, 'b) istream 103 val null_intersection : ''a list -> ''a list -> bool 104 val op_U : ('a -> 'a -> bool) -> 'a list list -> 'a list 105 val op_assoc : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b 106 val op_assoc1 : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b option 107 val op_insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list 108 val op_intersect : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list 109 val op_mem : ('a -> 'a -> bool) -> 'a -> 'a list -> bool 110 val op_mk_set : ('a -> 'a -> bool) -> 'a list -> 'a list 111 val op_rev_assoc : ('a -> 'a -> bool) -> 'a -> ('b * 'a) list -> 'b 112 val op_set_diff : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list 113 val op_union : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list 114 val option_compare : 'a cmp -> 'a option cmp 115 val option_eq : 'a eqf -> 'a option eqf 116 val pair : 'a -> 'b -> 'a * 'b 117 val pair_compare : ('a cmp * 'b cmp) -> ('a * 'b) cmp 118 val pair_eq : 'a eqf -> 'b eqf -> ('a * 'b) eqf 119 val pair_of_list : 'a list -> 'a * 'a 120 val partial : exn -> ('a -> 'b option) -> 'a -> 'b 121 val partition : ('a -> bool) -> 'a list -> 'a list * 'a list 122 val pluck : ('a -> bool) -> 'a list -> 'a * 'a list 123 val ppstring : ('a -> HOLPP.pretty) -> 'a -> string 124 val prime : string -> string 125 val quadruple : 'a -> 'b -> 'c -> 'd -> 'a * 'b * 'c * 'd 126 val quadruple_of_list : 'a list -> 'a * 'a * 'a * 'a 127 val quote : string -> string 128 val real_time : ('a -> 'b) -> 'a -> 'b 129 val redres_eq : 'a eqf -> 'b eqf -> {redex:'a,residue:'b} eqf 130 val repeat : ('a -> 'a) -> 'a -> 'a 131 val reset : ('a, 'b) istream -> ('a, 'b) istream 132 val rev_assoc : ''a -> ('b * ''a) list -> 'b 133 val rev_itlist2 : ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c 134 val rev_itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b 135 val rpair : 'a -> 'b -> 'b * 'a 136 val say : string -> unit 137 val saying : bool ref 138 val separate : 'a -> 'a list -> 'a list 139 val set_diff : ''a list -> ''a list -> ''a list 140 val set_eq : ''a list -> ''a list -> bool 141 val single : 'a -> 'a list 142 val singleton_of_list : 'a list -> 'a 143 val snd : 'a * 'b -> 'b 144 val sort : ('a -> 'a -> bool) -> 'a list -> 'a list 145 val split : ('a * 'b) list -> 'a list * 'b list 146 val split_after : int -> 'a list -> 'a list * 'a list 147 val start_real_time : unit -> Timer.real_timer 148 val start_time : unit -> Timer.cpu_timer 149 val state : ('a, 'b) istream -> 'b 150 val str_all : (char -> bool) -> string -> bool 151 val strcat : string -> string -> string 152 val string_to_int : string -> int 153 val subst_assoc : ('a -> bool) -> ('a, 'b)subst -> 'b option 154 val subst_eq : 'a eqf -> 'b eqf -> ('a,'b) subst eqf 155 val subtract : ''a list -> ''a list -> ''a list 156 val swap : 'a * 'b -> 'b * 'a 157 val time : ('a -> 'b) -> 'a -> 'b 158 val time_to_string : Time.time -> string 159 val topsort : ('a -> 'a -> bool) -> 'a list -> 'a list 160 val total : ('a -> 'b) -> 'a -> 'b option 161 val triple : 'a -> 'b -> 'c -> 'a * 'b * 'c 162 val triple_of_list : 'a list -> 'a * 'a * 'a 163 val try : ('a -> 'b) -> 'a -> 'b 164 val trye : ('a -> 'b) -> 'a -> 'b 165 val tryfind : ('a -> 'b) -> 'a list -> 'b 166 val trypluck': ('a -> 'b option) -> 'a list -> ('b option * 'a list) 167 val trypluck : ('a -> 'b) -> 'a list -> 'b * 'a list 168 val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c 169 val union : ''a list -> ''a list -> ''a list 170 val unprefix : string -> string -> string 171 val unprime : string -> string 172 val unzip : ('a * 'b) list -> 'a list * 'b list 173 val upto : int -> int -> int list 174 val vector_topsort : int list vector -> int list 175 val verdict : ('a -> 'b) -> ('a -> 'c) -> 'a -> ('b, 'c * exn)verdict 176 val with_exn : ('a -> 'b) -> 'a -> exn -> 'b 177 val with_flag : 'a ref * 'a -> ('b -> 'c) -> 'b -> 'c 178 val words2 : string -> string -> string list 179 val zip : 'a list -> 'b list -> ('a * 'b) list 180end 181