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