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