author  wenzelm 
Thu, 31 Jan 2019 16:32:41 +0100  
changeset 69769  c19a32cb9625 
parent 69468  54a95e1199cb 
child 70464  2d6a489adb01 
permissions  rwrr 
41
97aae241094b
added cons, rcons, last_elem, sort_strings, take_suffix;
wenzelm
parents:
24
diff
changeset

1 
(* Title: Pure/library.ML 
233  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
16188  3 
Author: Markus Wenzel, TU Muenchen 
0  4 

28732  5 
Basic library: functions, pairs, booleans, lists, integers, 
23424
d0580634f128
moved balanced tree operations to General/balanced_tree.ML;
wenzelm
parents:
23251
diff
changeset

6 
strings, lists as sets, orders, current directory, misc. 
21395
f34ac19659ae
moved some fundamental concepts to General/basics.ML;
wenzelm
parents:
21335
diff
changeset

7 

f34ac19659ae
moved some fundamental concepts to General/basics.ML;
wenzelm
parents:
21335
diff
changeset

8 
See also General/basics.ML for the most fundamental concepts. 
0  9 
*) 
10 

21395
f34ac19659ae
moved some fundamental concepts to General/basics.ML;
wenzelm
parents:
21335
diff
changeset

11 
infix 2 ? 
f34ac19659ae
moved some fundamental concepts to General/basics.ML;
wenzelm
parents:
21335
diff
changeset

12 
infix 3 o oo ooo oooo 
f34ac19659ae
moved some fundamental concepts to General/basics.ML;
wenzelm
parents:
21335
diff
changeset

13 
infix 4 ~~ upto downto 
36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
35976
diff
changeset

14 
infix orf andf 
5893  15 

15745  16 
signature BASIC_LIBRARY = 
4621  17 
sig 
18 
(*functions*) 

23860  19 
val undefined: 'a > 'b 
16842  20 
val I: 'a > 'a 
21 
val K: 'a > 'b > 'a 

4621  22 
val curry: ('a * 'b > 'c) > 'a > 'b > 'c 
23 
val uncurry: ('a > 'b > 'c) > 'a * 'b > 'c 

21565  24 
val ? : bool * ('a > 'a) > 'a > 'a 
16721  25 
val oo: ('a > 'b) * ('c > 'd > 'a) > 'c > 'd > 'b 
26 
val ooo: ('a > 'b) * ('c > 'd > 'e > 'a) > 'c > 'd > 'e > 'b 

27 
val oooo: ('a > 'b) * ('c > 'd > 'e > 'f > 'a) > 'c > 'd > 'e > 'f > 'b 

16842  28 
val funpow: int > ('a > 'a) > 'a > 'a 
31250  29 
val funpow_yield: int > ('a > 'b * 'a) > 'a > 'b list * 'a 
1364
8ea1a962ad72
files now define a structure to allow SML/NJ to optimize the code
clasohm
parents:
1290
diff
changeset

30 

4621  31 
(*pairs*) 
32 
val pair: 'a > 'b > 'a * 'b 

33 
val rpair: 'a > 'b > 'b * 'a 

34 
val fst: 'a * 'b > 'a 

35 
val snd: 'a * 'b > 'b 

17498
d83af87bbdc5
improved eq_fst and eq_snd, removed some deprecated stuff
haftmann
parents:
17486
diff
changeset

36 
val eq_fst: ('a * 'c > bool) > ('a * 'b) * ('c * 'd) > bool 
d83af87bbdc5
improved eq_fst and eq_snd, removed some deprecated stuff
haftmann
parents:
17486
diff
changeset

37 
val eq_snd: ('b * 'd > bool) > ('a * 'b) * ('c * 'd) > bool 
19454
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
19424
diff
changeset

38 
val eq_pair: ('a * 'c > bool) > ('b * 'd > bool) > ('a * 'b) * ('c * 'd) > bool 
4621  39 
val swap: 'a * 'b > 'b * 'a 
40 
val apfst: ('a > 'b) > 'a * 'c > 'b * 'c 

41 
val apsnd: ('a > 'b) > 'c * 'a > 'c * 'b 

59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58635
diff
changeset

42 
val apply2: ('a > 'b) > 'a * 'a > 'b * 'b 
4621  43 

44 
(*booleans*) 

45 
val equal: ''a > ''a > bool 

46 
val not_equal: ''a > ''a > bool 

47 
val orf: ('a > bool) * ('a > bool) > 'a > bool 

48 
val andf: ('a > bool) * ('a > bool) > 'a > bool 

49 
val exists: ('a > bool) > 'a list > bool 

50 
val forall: ('a > bool) > 'a list > bool 

51 

52 
(*lists*) 

5285  53 
val single: 'a > 'a list 
20882  54 
val the_single: 'a list > 'a 
19273  55 
val singleton: ('a list > 'b list) > 'a > 'b 
25061  56 
val yield_singleton: ('a list > 'c > 'b list * 'c) > 'a > 'c > 'b * 'c 
25058  57 
val perhaps_apply: ('a > 'a option) list > 'a > 'a option 
58 
val perhaps_loop: ('a > 'a option) > 'a > 'a option 

25681  59 
val foldl1: ('a * 'a > 'a) > 'a list > 'a 
15760  60 
val foldr1: ('a * 'a > 'a) > 'a list > 'a 
46891  61 
val eq_list: ('a * 'a > bool) > 'a list * 'a list > bool 
21395
f34ac19659ae
moved some fundamental concepts to General/basics.ML;
wenzelm
parents:
21335
diff
changeset

62 
val maps: ('a > 'b list) > 'a list > 'b list 
25549  63 
val filter: ('a > bool) > 'a list > 'a list 
64 
val filter_out: ('a > bool) > 'a list > 'a list 

65 
val map_filter: ('a > 'b option) > 'a list > 'b list 

33955  66 
val take: int > 'a list > 'a list 
67 
val drop: int > 'a list > 'a list 

19011  68 
val chop: int > 'a list > 'a list * 'a list 
46891  69 
val chop_groups: int > 'a list > 'a list list 
18278  70 
val nth: 'a list > int > 'a 
46891  71 
val nth_list: 'a list list > int > 'a list 
18011
685d95c793ff
cleaned up nth, nth_update, nth_map and nth_string functions
haftmann
parents:
17952
diff
changeset

72 
val nth_map: int > ('a > 'a) > 'a list > 'a list 
24846  73 
val nth_drop: int > 'a list > 'a list 
18514  74 
val map_index: (int * 'a > 'b) > 'a list > 'b list 
75 
val fold_index: (int * 'a > 'b > 'b) > 'a list > 'b > 'b 

33063  76 
val map_range: (int > 'a) > int > 'a list 
52271
6f3771c00280
combinator fold_range, corresponding to map_range
haftmann
parents:
51990
diff
changeset

77 
val fold_range: (int > 'a > 'a) > int > 'a > 'a 
4621  78 
val split_last: 'a list > 'a list * 'a 
46891  79 
val find_first: ('a > bool) > 'a list > 'a option 
4621  80 
val find_index: ('a > bool) > 'a list > int 
46891  81 
val get_first: ('a > 'b option) > 'a list > 'b option 
19233
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19119
diff
changeset

82 
val get_index: ('a > 'b option) > 'a list > (int * 'b) option 
46891  83 
val flat: 'a list list > 'a list 
84 
val unflat: 'a list list > 'b list > 'b list list 

85 
val grouped: int > (('a list > 'b list) > 'c list list > 'd list list) > 

86 
('a > 'b) > 'c list > 'd list 

87 
val burrow: ('a list > 'b list) > 'a list list > 'b list list 

88 
val burrow_options: ('a list > 'b list) > 'a option list > 'b option list 

89 
val fold_burrow: ('a list > 'c > 'b list * 'd) > 'a list list > 'c > 'b list list * 'd 

90 
val separate: 'a > 'a list > 'a list 

91 
val surround: 'a > 'a list > 'a list 

92 
val replicate: int > 'a > 'a list 

93 
val map_product: ('a > 'b > 'c) > 'a list > 'b list > 'c list 

94 
val fold_product: ('a > 'b > 'c > 'c) > 'a list > 'b list > 'c > 'c 

18330  95 
val map2: ('a > 'b > 'c) > 'a list > 'b list > 'c list 
96 
val fold2: ('a > 'b > 'c > 'c) > 'a list > 'b list > 'c > 'c 

46891  97 
val map_split: ('a > 'b * 'c) > 'a list > 'b list * 'c list 
19799  98 
val zip_options: 'a list > 'b option list > ('a * 'b) list 
18330  99 
val ~~ : 'a list * 'b list > ('a * 'b) list 
100 
val split_list: ('a * 'b) list > 'a list * 'b list 

46891  101 
val burrow_fst: ('a list > 'b list) > ('a * 'c) list > ('b * 'c) list 
67522  102 
val take_prefix: ('a > bool) > 'a list > 'a list 
103 
val drop_prefix: ('a > bool) > 'a list > 'a list 

104 
val chop_prefix: ('a > bool) > 'a list > 'a list * 'a list 

105 
val take_suffix: ('a > bool) > 'a list > 'a list 

106 
val drop_suffix: ('a > bool) > 'a list > 'a list 

107 
val chop_suffix: ('a > bool) > 'a list > 'a list * 'a list 

18441  108 
val is_prefix: ('a * 'a > bool) > 'a list > 'a list > bool 
67521  109 
val chop_common_prefix: ('a * 'b > bool) > 'a list * 'b list > 'a list * ('a list * 'b list) 
12249  110 
val prefixes1: 'a list > 'a list list 
19011  111 
val prefixes: 'a list > 'a list list 
12249  112 
val suffixes1: 'a list > 'a list list 
19011  113 
val suffixes: 'a list > 'a list list 
61707  114 
val trim: ('a > bool) > 'a list > 'a list 
4621  115 

116 
(*integers*) 

117 
val upto: int * int > int list 

118 
val downto: int * int > int list 

68087  119 
val hex_digit: int > string 
4621  120 
val radixpand: int * int > int list 
121 
val radixstring: int * string * int > string 

122 
val string_of_int: int > string 

21942
d6218d0f9ec3
added signed_string_of_int (pruduces proper  instead of SML's ~);
wenzelm
parents:
21920
diff
changeset

123 
val signed_string_of_int: int > string 
4621  124 
val string_of_indexname: string * int > string 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24593
diff
changeset

125 
val read_radix_int: int > string list > int * string list 
14826
48cfe0fe53e2
output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
wenzelm
parents:
14797
diff
changeset

126 
val read_int: string list > int * string list 
48cfe0fe53e2
output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
wenzelm
parents:
14797
diff
changeset

127 
val oct_char: string > string 
4621  128 

129 
(*strings*) 

18011
685d95c793ff
cleaned up nth, nth_update, nth_map and nth_string functions
haftmann
parents:
17952
diff
changeset

130 
val nth_string: string > int > string 
16188  131 
val fold_string: (string > 'a > 'a) > string > 'a > 'a 
6312  132 
val exists_string: (string > bool) > string > bool 
16188  133 
val forall_string: (string > bool) > string > bool 
28025  134 
val first_field: string > string > (string * string) option 
4621  135 
val enclose: string > string > string > string 
6642  136 
val unenclose: string > string 
4621  137 
val quote: string > string 
55033  138 
val cartouche: string > string 
4621  139 
val space_implode: string > string list > string 
140 
val commas: string list > string 

141 
val commas_quote: string list > string 

142 
val cat_lines: string list > string 

143 
val space_explode: string > string > string list 

14826
48cfe0fe53e2
output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
wenzelm
parents:
14797
diff
changeset

144 
val split_lines: string > string list 
56038
0e2dec666152
tuned messages  in accordance to Isabelle/Scala;
wenzelm
parents:
55033
diff
changeset

145 
val plain_words: string > string 
5942  146 
val prefix_lines: string > string > string 
18681
3020496cff28
added exception ERROR, error, cat_error, sys_error, assert, deny, assert_all;
wenzelm
parents:
18549
diff
changeset

147 
val prefix: string > string > string 
5285  148 
val suffix: string > string > string 
18681
3020496cff28
added exception ERROR, error, cat_error, sys_error, assert, deny, assert_all;
wenzelm
parents:
18549
diff
changeset

149 
val unprefix: string > string > string 
5285  150 
val unsuffix: string > string > string 
47499
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate  avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
47060
diff
changeset

151 
val trim_line: string > string 
65904
8411f1a2272c
permissive trim_line as in Scala, e.g. relevant for poly/TextIO.print output on Windows;
wenzelm
parents:
64275
diff
changeset

152 
val trim_split_lines: string > string list 
67179  153 
val normalize_lines: string > string 
10951  154 
val replicate_string: int > string > string 
14926  155 
val translate_string: (string > string) > string > string 
65934  156 
val encode_lines: string > string 
157 
val decode_lines: string > string 

63304  158 
val align_right: string > int > string > string 
29882
29154e67731d
New command find_consts searching for constants by type (by Timothy Bourke).
kleing
parents:
29209
diff
changeset

159 
val match_string: string > string > bool 
4621  160 

41516
3a70387b5e01
smart_string_of_real: print integer values without fractional part;
wenzelm
parents:
41494
diff
changeset

161 
(*reals*) 
3a70387b5e01
smart_string_of_real: print integer values without fractional part;
wenzelm
parents:
41494
diff
changeset

162 
val string_of_real: real > string 
3a70387b5e01
smart_string_of_real: print integer values without fractional part;
wenzelm
parents:
41494
diff
changeset

163 
val signed_string_of_real: real > string 
3a70387b5e01
smart_string_of_real: print integer values without fractional part;
wenzelm
parents:
41494
diff
changeset

164 

16492  165 
(*lists as sets  see also Pure/General/ord_list.ML*) 
18923  166 
val member: ('b * 'a > bool) > 'a list > 'b > bool 
167 
val insert: ('a * 'a > bool) > 'a > 'a list > 'a list 

168 
val remove: ('b * 'a > bool) > 'b > 'a list > 'a list 

24049  169 
val update: ('a * 'a > bool) > 'a > 'a list > 'a list 
33042  170 
val union: ('a * 'a > bool) > 'a list > 'a list > 'a list 
19301  171 
val subtract: ('b * 'a > bool) > 'b list > 'a list > 'a list 
33049
c38f02fdf35d
curried inter as canonical list operation (beware of argument order)
haftmann
parents:
33040
diff
changeset

172 
val inter: ('a * 'b > bool) > 'b list > 'a list > 'a list 
18923  173 
val merge: ('a * 'a > bool) > 'a list * 'a list > 'a list 
33038  174 
val subset: ('a * 'b > bool) > 'a list * 'b list > bool 
42403
38b29c9fc742
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
wenzelm
parents:
41516
diff
changeset

175 
val eq_set: ('a * 'a > bool) > 'a list * 'a list > bool 
19046
bc5c6c9b114e
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
19011
diff
changeset

176 
val distinct: ('a * 'a > bool) > 'a list > 'a list 
18966  177 
val duplicates: ('a * 'a > bool) > 'a list > 'a list 
16878  178 
val has_duplicates: ('a * 'a > bool) > 'a list > bool 
46891  179 
val map_transpose: ('a list > 'b) > 'a list list > 'b list 
4621  180 

23220  181 
(*lists as multisets*) 
22142  182 
val remove1: ('b * 'a > bool) > 'b > 'a list > 'a list 
33078
3aea60ca3900
multiset operations with canonical argument order
haftmann
parents:
33063
diff
changeset

183 
val combine: ('a * 'a > bool) > 'a list > 'a list > 'a list 
33079  184 
val submultiset: ('a * 'b > bool) > 'a list * 'b list > bool 
4621  185 

186 
(*orders*) 

18966  187 
val is_equal: order > bool 
67560  188 
val is_less: order > bool 
189 
val is_less_equal: order > bool 

190 
val is_greater: order > bool 

191 
val is_greater_equal: order > bool 

4621  192 
val rev_order: order > order 
193 
val make_ord: ('a * 'a > bool) > 'a * 'a > order 

25224  194 
val bool_ord: bool * bool > order 
4621  195 
val int_ord: int * int > order 
196 
val string_ord: string * string > order 

16676  197 
val fast_string_ord: string * string > order 
16492  198 
val option_ord: ('a * 'b > order) > 'a option * 'b option > order 
4621  199 
val prod_ord: ('a * 'b > order) > ('c * 'd > order) > ('a * 'c) * ('b * 'd) > order 
200 
val dict_ord: ('a * 'b > order) > 'a list * 'b list > order 

201 
val list_ord: ('a * 'b > order) > 'a list * 'b list > order 

202 
val sort: ('a * 'a > order) > 'a list > 'a list 

18427  203 
val sort_distinct: ('a * 'a > order) > 'a list > 'a list 
4621  204 
val sort_strings: string list > string list 
60924
610794dff23c
tuned signature, in accordance to sortBy in Scala;
wenzelm
parents:
59469
diff
changeset

205 
val sort_by: ('a > string) > 'a list > 'a list 
30558
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30190
diff
changeset

206 
val tag_list: int > 'a list > (int * 'a) list 
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30190
diff
changeset

207 
val untag_list: (int * 'a) list > 'a list 
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30190
diff
changeset

208 
val order_list: (int * 'a) list > 'a list 
4621  209 

210 
(*misc*) 

19644
0b01436e1843
added divide_and_conquer combinator (by Amine Chaieb);
wenzelm
parents:
19596
diff
changeset

211 
val divide_and_conquer: ('a > 'a list * ('b list > 'b)) > 'a > 'b 
32978  212 
val divide_and_conquer': ('a > 'b > ('a list * ('c list * 'b > 'c * 'b)) * 'b) > 
213 
'a > 'b > 'c * 'b 

4621  214 
val partition_eq: ('a * 'a > bool) > 'a list > 'a list list 
215 
val partition_list: (int > 'a > bool) > int > int > 'a list > 'a list list 

40509  216 
type serial = int 
16439  217 
val serial: unit > serial 
19512  218 
val serial_string: unit > string 
45626
b4f374a45668
more abstract datatype stamp, which avoids pointless allocation of mutable cells;
wenzelm
parents:
44617
diff
changeset

219 
eqtype stamp 
b4f374a45668
more abstract datatype stamp, which avoids pointless allocation of mutable cells;
wenzelm
parents:
44617
diff
changeset

220 
val stamp: unit > stamp 
51368
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
50913
diff
changeset

221 
structure Any: sig type T = exn end 
43603  222 
val getenv: string > string 
223 
val getenv_strict: string > string 

4621  224 
end; 
225 

15745  226 
signature LIBRARY = 
15570  227 
sig 
15745  228 
include BASIC_LIBRARY 
15570  229 
val foldl: ('a * 'b > 'a) > 'a * 'b list > 'a 
230 
val foldr: ('a * 'b > 'b) > 'a list * 'b > 'b 

231 
end; 

232 

15745  233 
structure Library: LIBRARY = 
1364
8ea1a962ad72
files now define a structure to allow SML/NJ to optimize the code
clasohm
parents:
1290
diff
changeset

234 
struct 
0  235 

21395
f34ac19659ae
moved some fundamental concepts to General/basics.ML;
wenzelm
parents:
21335
diff
changeset

236 
(* functions *) 
0  237 

23860  238 
fun undefined _ = raise Match; 
239 

16842  240 
fun I x = x; 
241 
fun K x = fn _ => x; 

233  242 
fun curry f x y = f (x, y); 
243 
fun uncurry f (x, y) = f x y; 

0  244 

17141
4b0dc89de43b
added ? combinator for conditional transformations
haftmann
parents:
17101
diff
changeset

245 
(*conditional application*) 
21565  246 
fun b ? f = fn x => if b then f x else x; 
17141
4b0dc89de43b
added ? combinator for conditional transformations
haftmann
parents:
17101
diff
changeset

247 

16721  248 
(*composition with multiple args*) 
249 
fun (f oo g) x y = f (g x y); 

250 
fun (f ooo g) x y z = f (g x y z); 

251 
fun (f oooo g) x y z w = f (g x y z w); 

252 

31250  253 
(*function exponentiation: f (... (f x) ...) with n applications of f*) 
69769
c19a32cb9625
prefer tailrecursive version (despite 4b99b1214034);
wenzelm
parents:
69468
diff
changeset

254 
fun funpow (0: int) _ x = x 
c19a32cb9625
prefer tailrecursive version (despite 4b99b1214034);
wenzelm
parents:
69468
diff
changeset

255 
 funpow n f x = funpow (n  1) f (f x); 
160  256 

31250  257 
fun funpow_yield (0 : int) _ x = ([], x) 
258 
 funpow_yield n f x = x > f >> funpow_yield (n  1) f >> op ::; 

160  259 

40318
035b2afbeb2e
discontinued obsolete function sys_error and exception SYS_ERROR;
wenzelm
parents:
40291
diff
changeset

260 

21395
f34ac19659ae
moved some fundamental concepts to General/basics.ML;
wenzelm
parents:
21335
diff
changeset

261 
(* pairs *) 
233  262 

263 
fun pair x y = (x, y); 

264 
fun rpair x y = (y, x); 

265 

266 
fun fst (x, y) = x; 

267 
fun snd (x, y) = y; 

268 

17498
d83af87bbdc5
improved eq_fst and eq_snd, removed some deprecated stuff
haftmann
parents:
17486
diff
changeset

269 
fun eq_fst eq ((x1, _), (x2, _)) = eq (x1, x2); 
d83af87bbdc5
improved eq_fst and eq_snd, removed some deprecated stuff
haftmann
parents:
17486
diff
changeset

270 
fun eq_snd eq ((_, y1), (_, y2)) = eq (y1, y2); 
19454
46a7e133f802
moved coalesce to AList, added equality predicates to library
haftmann
parents:
19424
diff
changeset

271 
fun eq_pair eqx eqy ((x1, y1), (x2, y2)) = eqx (x1, x2) andalso eqy (y1, y2); 
233  272 

273 
fun swap (x, y) = (y, x); 

274 

275 
fun apfst f (x, y) = (f x, y); 

276 
fun apsnd f (x, y) = (x, f y); 

59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58635
diff
changeset

277 
fun apply2 f (x, y) = (f x, f y); 
233  278 

279 

21395
f34ac19659ae
moved some fundamental concepts to General/basics.ML;
wenzelm
parents:
21335
diff
changeset

280 
(* booleans *) 
233  281 

21395
f34ac19659ae
moved some fundamental concepts to General/basics.ML;
wenzelm
parents:
21335
diff
changeset

282 
(*polymorphic equality*) 
233  283 
fun equal x y = x = y; 
284 
fun not_equal x y = x <> y; 

285 

21395
f34ac19659ae
moved some fundamental concepts to General/basics.ML;
wenzelm
parents:
21335
diff
changeset

286 
(*combining predicates*) 
16721  287 
fun p orf q = fn x => p x orelse q x; 
288 
fun p andf q = fn x => p x andalso q x; 

233  289 

25752  290 
val exists = List.exists; 
291 
val forall = List.all; 

0  292 

19644
0b01436e1843
added divide_and_conquer combinator (by Amine Chaieb);
wenzelm
parents:
19596
diff
changeset

293 

21395
f34ac19659ae
moved some fundamental concepts to General/basics.ML;
wenzelm
parents:
21335
diff
changeset

294 

233  295 
(** lists **) 
296 

5285  297 
fun single x = [x]; 
233  298 

20882  299 
fun the_single [x] = x 
47060
e2741ec9ae36
prefer explicitly qualified exception List.Empty;
wenzelm
parents:
47023
diff
changeset

300 
 the_single _ = raise List.Empty; 
20882  301 

302 
fun singleton f x = the_single (f [x]); 

19273  303 

25061  304 
fun yield_singleton f x = f [x] #>> the_single; 
305 

25058  306 
fun perhaps_apply funs arg = 
307 
let 

308 
fun app [] res = res 

309 
 app (f :: fs) (changed, x) = 

310 
(case f x of 

311 
NONE => app fs (changed, x) 

312 
 SOME x' => app fs (true, x')); 

313 
in (case app funs (false, arg) of (false, _) => NONE  (true, arg') => SOME arg') end; 

314 

315 
fun perhaps_loop f arg = 

316 
let 

317 
fun loop (changed, x) = 

318 
(case f x of 

319 
NONE => (changed, x) 

320 
 SOME x' => loop (true, x')); 

321 
in (case loop (false, arg) of (false, _) => NONE  (true, arg') => SOME arg') end; 

322 

233  323 

21395
f34ac19659ae
moved some fundamental concepts to General/basics.ML;
wenzelm
parents:
21335
diff
changeset

324 
(* fold  old versions *) 
16691
539b9cc282fa
added combinatros '>' and '>>' and fold_map fitting nicely to ST combinator '>'
haftmann
parents:
16688
diff
changeset

325 

233  326 
(*the following versions of fold are designed to fit nicely with infixes*) 
0  327 

233  328 
(* (op @) (e, [x1, ..., xn]) ===> ((e @ x1) @ x2) ... @ xn 
329 
for operators that associate to the left (TAIL RECURSIVE)*) 

330 
fun foldl (f: 'a * 'b > 'a) : 'a * 'b list > 'a = 

331 
let fun itl (e, []) = e 

332 
 itl (e, a::l) = itl (f(e, a), l) 

333 
in itl end; 

334 

335 
(* (op @) ([x1, ..., xn], e) ===> x1 @ (x2 ... @ (xn @ e)) 

336 
for operators that associate to the right (not tail recursive)*) 

337 
fun foldr f (l, e) = 

338 
let fun itr [] = e 

339 
 itr (a::l) = f(a, itr l) 

340 
in itr l end; 

341 

25681  342 
(* (op @) [x1, ..., xn] ===> ((x1 @ x2) @ x3) ... @ xn 
343 
for operators that associate to the left (TAIL RECURSIVE)*) 

47060
e2741ec9ae36
prefer explicitly qualified exception List.Empty;
wenzelm
parents:
47023
diff
changeset

344 
fun foldl1 f [] = raise List.Empty 
25681  345 
 foldl1 f (x :: xs) = foldl f (x, xs); 
346 

233  347 
(* (op @) [x1, ..., xn] ===> x1 @ (x2 ... @ (x[n1] @ xn)) 
348 
for n > 0, operators that associate to the right (not tail recursive)*) 

47060
e2741ec9ae36
prefer explicitly qualified exception List.Empty;
wenzelm
parents:
47023
diff
changeset

349 
fun foldr1 f [] = raise List.Empty 
20510  350 
 foldr1 f l = 
20443  351 
let fun itr [x] = x 
20510  352 
 itr (x::l) = f(x, itr l) 
20443  353 
in itr l end; 
233  354 

355 

356 
(* basic list functions *) 

357 

20510  358 
fun eq_list eq (list1, list2) = 
42403
38b29c9fc742
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
wenzelm
parents:
41516
diff
changeset

359 
pointer_eq (list1, list2) orelse 
38b29c9fc742
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
wenzelm
parents:
41516
diff
changeset

360 
let 
38b29c9fc742
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
wenzelm
parents:
41516
diff
changeset

361 
fun eq_lst (x :: xs, y :: ys) = eq (x, y) andalso eq_lst (xs, ys) 
38b29c9fc742
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
wenzelm
parents:
41516
diff
changeset

362 
 eq_lst _ = true; 
38b29c9fc742
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
wenzelm
parents:
41516
diff
changeset

363 
in length list1 = length list2 andalso eq_lst (list1, list2) end; 
20348  364 

19483
55ee839198bd
renamed mapfilter to map_filter, made pervasive (again);
wenzelm
parents:
19474
diff
changeset

365 
fun maps f [] = [] 
55ee839198bd
renamed mapfilter to map_filter, made pervasive (again);
wenzelm
parents:
19474
diff
changeset

366 
 maps f (x :: xs) = f x @ maps f xs; 
55ee839198bd
renamed mapfilter to map_filter, made pervasive (again);
wenzelm
parents:
19474
diff
changeset

367 

25538  368 
val filter = List.filter; 
369 
fun filter_out f = filter (not o f); 

370 
val map_filter = List.mapPartial; 

371 

33955  372 
fun take (0: int) xs = [] 
373 
 take _ [] = [] 

34059  374 
 take n (x :: xs) = x :: take (n  1) xs; 
33955  375 

376 
fun drop (0: int) xs = xs 

377 
 drop _ [] = [] 

34059  378 
 drop n (x :: xs) = drop (n  1) xs; 
33955  379 

24593
1547ea587f5a
added some int constraints (ML_Parse.fix_ints not active here);
wenzelm
parents:
24148
diff
changeset

380 
fun chop (0: int) xs = ([], xs) 
23220  381 
 chop _ [] = ([], []) 
382 
 chop n (x :: xs) = chop (n  1) xs >> cons x; 

19011  383 

46891  384 
fun chop_groups n list = 
385 
(case chop (Int.max (n, 1)) list of 

386 
([], _) => [] 

387 
 (g, rest) => g :: chop_groups n rest); 

388 

389 

233  390 
(*return nth element of a list, where 0 designates the first element; 
18461  391 
raise Subscript if list too short*) 
18011
685d95c793ff
cleaned up nth, nth_update, nth_map and nth_string functions
haftmann
parents:
17952
diff
changeset

392 
fun nth xs i = List.nth (xs, i); 
233  393 

43278  394 
fun nth_list xss i = nth xss i handle General.Subscript => []; 
18461  395 

18011
685d95c793ff
cleaned up nth, nth_update, nth_map and nth_string functions
haftmann
parents:
17952
diff
changeset

396 
fun nth_map 0 f (x :: xs) = f x :: xs 
685d95c793ff
cleaned up nth, nth_update, nth_map and nth_string functions
haftmann
parents:
17952
diff
changeset

397 
 nth_map n f (x :: xs) = x :: nth_map (n  1) f xs 
24593
1547ea587f5a
added some int constraints (ML_Parse.fix_ints not active here);
wenzelm
parents:
24148
diff
changeset

398 
 nth_map (_: int) _ [] = raise Subscript; 
11773  399 

24846  400 
fun nth_drop n xs = 
401 
List.take (xs, n) @ List.drop (xs, n + 1); 

402 

18514  403 
fun map_index f = 
404 
let 

52271
6f3771c00280
combinator fold_range, corresponding to map_range
haftmann
parents:
51990
diff
changeset

405 
fun map_aux (_: int) [] = [] 
6f3771c00280
combinator fold_range, corresponding to map_range
haftmann
parents:
51990
diff
changeset

406 
 map_aux i (x :: xs) = f (i, x) :: map_aux (i + 1) xs 
6f3771c00280
combinator fold_range, corresponding to map_range
haftmann
parents:
51990
diff
changeset

407 
in map_aux 0 end; 
18514  408 

21118  409 
fun fold_index f = 
410 
let 

24593
1547ea587f5a
added some int constraints (ML_Parse.fix_ints not active here);
wenzelm
parents:
24148
diff
changeset

411 
fun fold_aux (_: int) [] y = y 
52271
6f3771c00280
combinator fold_range, corresponding to map_range
haftmann
parents:
51990
diff
changeset

412 
 fold_aux i (x :: xs) y = fold_aux (i + 1) xs (f (i, x) y) 
21118  413 
in fold_aux 0 end; 
414 

33063  415 
fun map_range f i = 
416 
let 

52271
6f3771c00280
combinator fold_range, corresponding to map_range
haftmann
parents:
51990
diff
changeset

417 
fun map_aux (k: int) = 
6f3771c00280
combinator fold_range, corresponding to map_range
haftmann
parents:
51990
diff
changeset

418 
if k < i then f k :: map_aux (k + 1) else [] 
6f3771c00280
combinator fold_range, corresponding to map_range
haftmann
parents:
51990
diff
changeset

419 
in map_aux 0 end; 
6f3771c00280
combinator fold_range, corresponding to map_range
haftmann
parents:
51990
diff
changeset

420 

6f3771c00280
combinator fold_range, corresponding to map_range
haftmann
parents:
51990
diff
changeset

421 
fun fold_range f i = 
6f3771c00280
combinator fold_range, corresponding to map_range
haftmann
parents:
51990
diff
changeset

422 
let 
6f3771c00280
combinator fold_range, corresponding to map_range
haftmann
parents:
51990
diff
changeset

423 
fun fold_aux (k: int) y = 
6f3771c00280
combinator fold_range, corresponding to map_range
haftmann
parents:
51990
diff
changeset

424 
if k < i then fold_aux (k + 1) (f k y) else y 
6f3771c00280
combinator fold_range, corresponding to map_range
haftmann
parents:
51990
diff
changeset

425 
in fold_aux 0 end; 
6f3771c00280
combinator fold_range, corresponding to map_range
haftmann
parents:
51990
diff
changeset

426 

33063  427 

3762  428 
(*rear decomposition*) 
47060
e2741ec9ae36
prefer explicitly qualified exception List.Empty;
wenzelm
parents:
47023
diff
changeset

429 
fun split_last [] = raise List.Empty 
3762  430 
 split_last [x] = ([], x) 
431 
 split_last (x :: xs) = apfst (cons x) (split_last xs); 

432 

46891  433 
(*find first element satisfying predicate*) 
434 
val find_first = List.find; 

435 

29209  436 
(*find position of first element satisfying a predicate*) 
4212  437 
fun find_index pred = 
24593
1547ea587f5a
added some int constraints (ML_Parse.fix_ints not active here);
wenzelm
parents:
24148
diff
changeset

438 
let fun find (_: int) [] = ~1 
4212  439 
 find n (x :: xs) = if pred x then n else find (n + 1) xs; 
440 
in find 0 end; 

3762  441 

4916
fe8b0c82691b
get_first: ('a > 'b option) > 'a list > 'b option;
wenzelm
parents:
4893
diff
changeset

442 
(*get first element by lookup function*) 
15531  443 
fun get_first _ [] = NONE 
4916
fe8b0c82691b
get_first: ('a > 'b option) > 'a list > 'b option;
wenzelm
parents:
4893
diff
changeset

444 
 get_first f (x :: xs) = 
fe8b0c82691b
get_first: ('a > 'b option) > 'a list > 'b option;
wenzelm
parents:
4893
diff
changeset

445 
(case f x of 
15531  446 
NONE => get_first f xs 
4916
fe8b0c82691b
get_first: ('a > 'b option) > 'a list > 'b option;
wenzelm
parents:
4893
diff
changeset

447 
 some => some); 
fe8b0c82691b
get_first: ('a > 'b option) > 'a list > 'b option;
wenzelm
parents:
4893
diff
changeset

448 

19233
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19119
diff
changeset

449 
fun get_index f = 
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19119
diff
changeset

450 
let 
69237  451 
fun get_aux (_: int) [] = NONE 
452 
 get_aux i (x :: xs) = 

46838  453 
(case f x of 
69237  454 
NONE => get_aux (i + 1) xs 
46838  455 
 SOME y => SOME (i, y)) 
69237  456 
in get_aux 0 end; 
19233
77ca20b0ed77
renamed HOL +  * etc. to HOL.plus HOL.minus HOL.times etc.
haftmann
parents:
19119
diff
changeset

457 

15531  458 
val flat = List.concat; 
233  459 

12136  460 
fun unflat (xs :: xss) ys = 
19424  461 
let val (ps, qs) = chop (length xs) ys 
13629  462 
in ps :: unflat xss qs end 
12136  463 
 unflat [] [] = [] 
40722
441260986b63
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
wenzelm
parents:
40721
diff
changeset

464 
 unflat _ _ = raise ListPair.UnequalLengths; 
12136  465 

46891  466 
fun grouped n comb f = chop_groups n #> comb (map f) #> flat; 
467 

21479
63e7eb863ae6
moved string_of_pair/list/option to structure ML_Syntax;
wenzelm
parents:
21395
diff
changeset

468 
fun burrow f xss = unflat xss (f (flat xss)); 
18359  469 

24864  470 
fun burrow_options f os = map (try hd) (burrow f (map the_list os)); 
471 

18549
5308a6ea3b96
rearranged burrow_split to fold_burrow to allow composition with fold_map
haftmann
parents:
18514
diff
changeset

472 
fun fold_burrow f xss s = 
5308a6ea3b96
rearranged burrow_split to fold_burrow to allow composition with fold_map
haftmann
parents:
18514
diff
changeset

473 
apfst (unflat xss) (f (flat xss) s); 
18359  474 

233  475 
(*separate s [x1, x2, ..., xn] ===> [x1, s, x2, s, ..., s, xn]*) 
476 
fun separate s (x :: (xs as _ :: _)) = x :: s :: separate s xs 

477 
 separate _ xs = xs; 

478 

25980  479 
fun surround s (x :: xs) = s :: x :: surround s xs 
480 
 surround s [] = [s]; 

481 

233  482 
(*make the list [x, x, ..., x] of length n*) 
24593
1547ea587f5a
added some int constraints (ML_Parse.fix_ints not active here);
wenzelm
parents:
24148
diff
changeset

483 
fun replicate (n: int) x = 
233  484 
let fun rep (0, xs) = xs 
485 
 rep (n, xs) = rep (n  1, x :: xs) 

486 
in 

15570  487 
if n < 0 then raise Subscript 
233  488 
else rep (n, []) 
489 
end; 

490 

4248
5e8a31c41d44
added get_error: 'a error > string option, get_ok: 'a error > 'a option;
wenzelm
parents:
4224
diff
changeset

491 

25549  492 
(* direct product *) 
493 

25538  494 
fun map_product f _ [] = [] 
495 
 map_product f [] _ = [] 

496 
 map_product f (x :: xs) ys = map (f x) ys @ map_product f xs ys; 

233  497 

25538  498 
fun fold_product f _ [] z = z 
499 
 fold_product f [] _ z = z 

500 
 fold_product f (x :: xs) ys z = z > fold (f x) ys > fold_product f xs ys; 

233  501 

25549  502 

503 
(* lists of pairs *) 

233  504 

18330  505 
fun map2 _ [] [] = [] 
506 
 map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys 

40722
441260986b63
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
wenzelm
parents:
40721
diff
changeset

507 
 map2 _ _ _ = raise ListPair.UnequalLengths; 
380  508 

58633  509 
fun fold2 _ [] [] z = z 
23220  510 
 fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z) 
58633  511 
 fold2 _ _ _ _ = raise ListPair.UnequalLengths; 
380  512 

58633  513 
fun map_split _ [] = ([], []) 
25943  514 
 map_split f (x :: xs) = 
515 
let 

516 
val (y, w) = f x; 

517 
val (ys, ws) = map_split f xs; 

518 
in (y :: ys, w :: ws) end; 

519 

19799  520 
fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys 
521 
 zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys 

522 
 zip_options _ [] = [] 

40722
441260986b63
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
wenzelm
parents:
40721
diff
changeset

523 
 zip_options [] _ = raise ListPair.UnequalLengths; 
4956
a7538e43896e
added foldl_map: ('a * 'b > 'a * 'c) > 'a * 'b list > 'a * 'c list;
wenzelm
parents:
4945
diff
changeset

524 

233  525 
(*combine two lists forming a list of pairs: 
526 
[x1, ..., xn] ~~ [y1, ..., yn] ===> [(x1, y1), ..., (xn, yn)]*) 

527 
fun [] ~~ [] = [] 

528 
 (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys) 

40722
441260986b63
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
wenzelm
parents:
40721
diff
changeset

529 
 _ ~~ _ = raise ListPair.UnequalLengths; 
233  530 

531 
(*inverse of ~~; the old 'split': 

532 
[(x1, y1), ..., (xn, yn)] ===> ([x1, ..., xn], [y1, ..., yn])*) 

15570  533 
val split_list = ListPair.unzip; 
233  534 

28347  535 
fun burrow_fst f xs = split_list xs >> f > op ~~; 
536 

233  537 

67522  538 
(* take, drop, chop, trim according to predicate *) 
539 

540 
fun take_prefix pred list = 

541 
let 

542 
fun take res (x :: xs) = if pred x then take (x :: res) xs else rev res 

543 
 take res [] = rev res; 

544 
in take [] list end; 

545 

546 
fun drop_prefix pred list = 

547 
let 

548 
fun drop (x :: xs) = if pred x then drop xs else x :: xs 

549 
 drop [] = []; 

550 
in drop list end; 

551 

552 
fun chop_prefix pred list = 

553 
let 

554 
val prfx = take_prefix pred list; 

555 
val sffx = drop (length prfx) list; 

556 
in (prfx, sffx) end; 

557 

558 
fun take_suffix pred list = 

559 
let 

560 
fun take res (x :: xs) = if pred x then take (x :: res) xs else res 

561 
 take res [] = res; 

562 
in take [] (rev list) end; 

563 

564 
fun drop_suffix pred list = 

565 
let 

566 
fun drop (x :: xs) = if pred x then drop xs else rev (x :: xs) 

567 
 drop [] = []; 

568 
in drop (rev list) end; 

569 

570 
fun chop_suffix pred list = 

571 
let 

572 
val prfx = drop_suffix pred list; 

573 
val sffx = drop (length prfx) list; 

574 
in (prfx, sffx) end; 

575 

576 
fun trim pred = drop_prefix pred #> drop_suffix pred; 

577 

578 

233  579 
(* prefixes, suffixes *) 
580 

18441  581 
fun is_prefix _ [] _ = true 
582 
 is_prefix eq (x :: xs) (y :: ys) = eq (x, y) andalso is_prefix eq xs ys 

583 
 is_prefix eq _ _ = false; 

233  584 

67521  585 
fun chop_common_prefix eq ([], ys) = ([], ([], ys)) 
586 
 chop_common_prefix eq (xs, []) = ([], (xs, [])) 

587 
 chop_common_prefix eq (xs as x :: xs', ys as y :: ys') = 

588 
if eq (x, y) then 

589 
let val (ps', xys'') = chop_common_prefix eq (xs', ys') 

590 
in (x :: ps', xys'') end 

591 
else ([], (xs, ys)); 

592 

12249  593 
fun prefixes1 [] = [] 
594 
 prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs); 

595 

19011  596 
fun prefixes xs = [] :: prefixes1 xs; 
597 

12249  598 
fun suffixes1 xs = map rev (prefixes1 (rev xs)); 
19011  599 
fun suffixes xs = [] :: suffixes1 xs; 
233  600 

23220  601 

69468  602 

233  603 
(** integers **) 
604 

605 
(* lists of integers *) 

606 

607 
(*make the list [from, from + 1, ..., to]*) 

24593
1547ea587f5a
added some int constraints (ML_Parse.fix_ints not active here);
wenzelm
parents:
24148
diff
changeset

608 
fun ((i: int) upto j) = 
21859  609 
if i > j then [] else i :: (i + 1 upto j); 
233  610 

611 
(*make the list [from, from  1, ..., to]*) 

24593
1547ea587f5a
added some int constraints (ML_Parse.fix_ints not active here);
wenzelm
parents:
24148
diff
changeset

612 
fun ((i: int) downto j) = 
21859  613 
if i < j then [] else i :: (i  1 downto j); 
233  614 

615 

616 
(* convert integers to strings *) 

617 

68087  618 
(*hexadecimal*) 
619 
fun hex_digit i = 

620 
if i < 10 then chr (Char.ord #"0" + i) else chr (Char.ord #"a" + i  10); 

621 

233  622 
(*expand the number in the given base; 
623 
example: radixpand (2, 8) gives [1, 0, 0, 0]*) 

624 
fun radixpand (base, num) : int list = 

625 
let 

626 
fun radix (n, tail) = 

627 
if n < base then n :: tail 

628 
else radix (n div base, (n mod base) :: tail) 

629 
in radix (num, []) end; 

630 

631 
(*expands a number into a string of characters starting from "zerochar"; 

632 
example: radixstring (2, "0", 8) gives "1000"*) 

633 
fun radixstring (base, zerochar, num) = 

634 
let val offset = ord zerochar; 

635 
fun chrof n = chr (offset + n) 

636 
in implode (map chrof (radixpand (base, num))) end; 

637 

638 

41492
7a4138cb46db
tuned string_of_int to avoid allocation for small integers;
wenzelm
parents:
41489
diff
changeset

639 
local 
64275
ac2abc987cf9
accomodate Poly/ML repository version, which treats singleton strings as boxed;
wenzelm
parents:
63304
diff
changeset

640 
val zero = Char.ord #"0"; 
57909
0fb331032f02
more compact representation of special string values;
wenzelm
parents:
57884
diff
changeset

641 
val small_int = 10000: int; 
0fb331032f02
more compact representation of special string values;
wenzelm
parents:
57884
diff
changeset

642 
val small_int_table = Vector.tabulate (small_int, Int.toString); 
41492
7a4138cb46db
tuned string_of_int to avoid allocation for small integers;
wenzelm
parents:
41489
diff
changeset

643 
in 
7a4138cb46db
tuned string_of_int to avoid allocation for small integers;
wenzelm
parents:
41489
diff
changeset

644 

7a4138cb46db
tuned string_of_int to avoid allocation for small integers;
wenzelm
parents:
41489
diff
changeset

645 
fun string_of_int i = 
7a4138cb46db
tuned string_of_int to avoid allocation for small integers;
wenzelm
parents:
41489
diff
changeset

646 
if i < 0 then Int.toString i 
7a4138cb46db
tuned string_of_int to avoid allocation for small integers;
wenzelm
parents:
41489
diff
changeset

647 
else if i < 10 then chr (zero + i) 
57909
0fb331032f02
more compact representation of special string values;
wenzelm
parents:
57884
diff
changeset

648 
else if i < small_int then Vector.sub (small_int_table, i) 
41492
7a4138cb46db
tuned string_of_int to avoid allocation for small integers;
wenzelm
parents:
41489
diff
changeset

649 
else Int.toString i; 
7a4138cb46db
tuned string_of_int to avoid allocation for small integers;
wenzelm
parents:
41489
diff
changeset

650 

7a4138cb46db
tuned string_of_int to avoid allocation for small integers;
wenzelm
parents:
41489
diff
changeset

651 
end; 
233  652 

21942
d6218d0f9ec3
added signed_string_of_int (pruduces proper  instead of SML's ~);
wenzelm
parents:
21920
diff
changeset

653 
fun signed_string_of_int i = 
d6218d0f9ec3
added signed_string_of_int (pruduces proper  instead of SML's ~);
wenzelm
parents:
21920
diff
changeset

654 
if i < 0 then "" ^ string_of_int (~ i) else string_of_int i; 
d6218d0f9ec3
added signed_string_of_int (pruduces proper  instead of SML's ~);
wenzelm
parents:
21920
diff
changeset

655 

23220  656 
fun string_of_indexname (a, 0) = a 
657 
 string_of_indexname (a, i) = a ^ "_" ^ string_of_int i; 

233  658 

659 

14826
48cfe0fe53e2
output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
wenzelm
parents:
14797
diff
changeset

660 
(* read integers *) 
48cfe0fe53e2
output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
wenzelm
parents:
14797
diff
changeset

661 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24593
diff
changeset

662 
fun read_radix_int radix cs = 
20095  663 
let 
64275
ac2abc987cf9
accomodate Poly/ML repository version, which treats singleton strings as boxed;
wenzelm
parents:
63304
diff
changeset

664 
val zero = Char.ord #"0"; 
20095  665 
val limit = zero + radix; 
666 
fun scan (num, []) = (num, []) 

667 
 scan (num, c :: cs) = 

50637  668 
if zero <= ord c andalso ord c < limit then 
669 
scan (radix * num + (ord c  zero), cs) 

670 
else (num, c :: cs); 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24593
diff
changeset

671 
in scan (0, cs) end; 
14826
48cfe0fe53e2
output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
wenzelm
parents:
14797
diff
changeset

672 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24593
diff
changeset

673 
val read_int = read_radix_int 10; 
14826
48cfe0fe53e2
output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
wenzelm
parents:
14797
diff
changeset

674 

40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40564
diff
changeset

675 
fun oct_char s = chr (#1 (read_radix_int 8 (raw_explode s))); 
14826
48cfe0fe53e2
output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
wenzelm
parents:
14797
diff
changeset

676 

48cfe0fe53e2
output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
wenzelm
parents:
14797
diff
changeset

677 

48cfe0fe53e2
output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
wenzelm
parents:
14797
diff
changeset

678 

233  679 
(** strings **) 
680 

16188  681 
(* functions tuned for strings, avoiding explode *) 
6312  682 

18011
685d95c793ff
cleaned up nth, nth_update, nth_map and nth_string functions
haftmann
parents:
17952
diff
changeset

683 
fun nth_string str i = 
6959  684 
(case try String.substring (str, i, 1) of 
15531  685 
SOME s => s 
15570  686 
 NONE => raise Subscript); 
6312  687 

16188  688 
fun fold_string f str x0 = 
6282  689 
let 
690 
val n = size str; 

16188  691 
fun iter (x, i) = 
692 
if i < n then iter (f (String.substring (str, i, 1)) x, i + 1) else x; 

693 
in iter (x0, 0) end; 

6282  694 

14968  695 
fun exists_string pred str = 
696 
let 

697 
val n = size str; 

698 
fun ex i = i < n andalso (pred (String.substring (str, i, 1)) orelse ex (i + 1)); 

699 
in ex 0 end; 

6312  700 

16188  701 
fun forall_string pred = not o exists_string (not o pred); 
702 

28025  703 
fun first_field sep str = 
28022  704 
let 
28025  705 
val n = size sep; 
28022  706 
val len = size str; 
707 
fun find i = 

708 
if i + n > len then NONE 

28025  709 
else if String.substring (str, i, n) = sep then SOME i 
28022  710 
else find (i + 1); 
28025  711 
in 
712 
(case find 0 of 

713 
NONE => NONE 

714 
 SOME i => SOME (String.substring (str, 0, i), String.extract (str, i + n, NONE))) 

715 
end; 

28022  716 

512
55755ed9fab9
Pure/library/enclose, Pure/Syntax/pretty/enclose: renamed from parents
lcp
parents:
410
diff
changeset

717 
(*enclose in brackets*) 
55755ed9fab9
Pure/library/enclose, Pure/Syntax/pretty/enclose: renamed from parents
lcp
parents:
410
diff
changeset

718 
fun enclose lpar rpar str = lpar ^ str ^ rpar; 
6642  719 
fun unenclose str = String.substring (str, 1, size str  2); 
255
ee132db91681
added if_none, parents, commas, gen_duplicates, duplicates, assoc2;
wenzelm
parents:
245
diff
changeset

720 

233  721 
(*simple quoting (does not escape special chars)*) 
512
55755ed9fab9
Pure/library/enclose, Pure/Syntax/pretty/enclose: renamed from parents
lcp
parents:
410
diff
changeset

722 
val quote = enclose "\"" "\""; 
233  723 

62529
8b7bdfc09f3b
clarified treatment of fragments of Isabelle symbols during bootstrap;
wenzelm
parents:
62491
diff
changeset

724 
val cartouche = enclose "\<open>" "\<close>"; 
55033  725 

59469  726 
val space_implode = String.concatWith; 
233  727 

255
ee132db91681
added if_none, parents, commas, gen_duplicates, duplicates, assoc2;
wenzelm
parents:
245
diff
changeset

728 
val commas = space_implode ", "; 
380  729 
val commas_quote = commas o map quote; 
255
ee132db91681
added if_none, parents, commas, gen_duplicates, duplicates, assoc2;
wenzelm
parents:
245
diff
changeset

730 

ee132db91681
added if_none, parents, commas, gen_duplicates, duplicates, assoc2;
wenzelm
parents:
245
diff
changeset

731 
val cat_lines = space_implode "\n"; 
233  732 

4212  733 
(*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*) 
3832
17a20a2af8f5
fixed space_explode, old one retained as BAD_space_explode;
wenzelm
parents:
3762
diff
changeset

734 
fun space_explode _ "" = [] 
21899  735 
 space_explode sep s = String.fields (fn c => str c = sep) s; 
3832
17a20a2af8f5
fixed space_explode, old one retained as BAD_space_explode;
wenzelm
parents:
3762
diff
changeset

736 

17a20a2af8f5
fixed space_explode, old one retained as BAD_space_explode;
wenzelm
parents:
3762
diff
changeset

737 
val split_lines = space_explode "\n"; 
17a20a2af8f5
fixed space_explode, old one retained as BAD_space_explode;
wenzelm
parents:
3762
diff
changeset

738 

56038
0e2dec666152
tuned messages  in accordance to Isabelle/Scala;
wenzelm
parents:
55033
diff
changeset

739 
fun plain_words s = space_explode "_" s > space_implode " "; 
0e2dec666152
tuned messages  in accordance to Isabelle/Scala;
wenzelm
parents:
55033
diff
changeset

740 

14826
48cfe0fe53e2
output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
wenzelm
parents:
14797
diff
changeset

741 
fun prefix_lines "" txt = txt 
48cfe0fe53e2
output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
wenzelm
parents:
14797
diff
changeset

742 
 prefix_lines prfx txt = txt > split_lines > map (fn s => prfx ^ s) > cat_lines; 
48cfe0fe53e2
output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
wenzelm
parents:
14797
diff
changeset

743 

18681
3020496cff28
added exception ERROR, error, cat_error, sys_error, assert, deny, assert_all;
wenzelm
parents:
18549
diff
changeset

744 
fun prefix prfx s = prfx ^ s; 
16188  745 
fun suffix sffx s = s ^ sffx; 
5285  746 

18681
3020496cff28
added exception ERROR, error, cat_error, sys_error, assert, deny, assert_all;
wenzelm
parents:
18549
diff
changeset

747 
fun unprefix prfx s = 
3020496cff28
added exception ERROR, error, cat_error, sys_error, assert, deny, assert_all;
wenzelm
parents:
18549
diff
changeset

748 
if String.isPrefix prfx s then String.substring (s, size prfx, size s  size prfx) 
3020496cff28
added exception ERROR, error, cat_error, sys_error, assert, deny, assert_all;
wenzelm
parents:
18549
diff
changeset

749 
else raise Fail "unprefix"; 
3020496cff28
added exception ERROR, error, cat_error, sys_error, assert, deny, assert_all;
wenzelm
parents:
18549
diff
changeset

750 

16188  751 
fun unsuffix sffx s = 
17061  752 
if String.isSuffix sffx s then String.substring (s, 0, size s  size sffx) 
753 
else raise Fail "unsuffix"; 

5285  754 

65904
8411f1a2272c
permissive trim_line as in Scala, e.g. relevant for poly/TextIO.print output on Windows;
wenzelm
parents:
64275
diff
changeset

755 
fun trim_line s = 
8411f1a2272c
permissive trim_line as in Scala, e.g. relevant for poly/TextIO.print output on Windows;
wenzelm
parents:
64275
diff
changeset

756 
if String.isSuffix "\r\n" s 
8411f1a2272c
permissive trim_line as in Scala, e.g. relevant for poly/TextIO.print output on Windows;
wenzelm
parents:
64275
diff
changeset

757 
then String.substring (s, 0, size s  2) 
8411f1a2272c
permissive trim_line as in Scala, e.g. relevant for poly/TextIO.print output on Windows;
wenzelm
parents:
64275
diff
changeset

758 
else if String.isSuffix "\r" s orelse String.isSuffix "\n" s 
8411f1a2272c
permissive trim_line as in Scala, e.g. relevant for poly/TextIO.print output on Windows;
wenzelm
parents:
64275
diff
changeset

759 
then String.substring (s, 0, size s  1) 
8411f1a2272c
permissive trim_line as in Scala, e.g. relevant for poly/TextIO.print output on Windows;
wenzelm
parents:
64275
diff
changeset

760 
else s; 
8411f1a2272c
permissive trim_line as in Scala, e.g. relevant for poly/TextIO.print output on Windows;
wenzelm
parents:
64275
diff
changeset

761 

8411f1a2272c
permissive trim_line as in Scala, e.g. relevant for poly/TextIO.print output on Windows;
wenzelm
parents:
64275
diff
changeset

762 
val trim_split_lines = trim_line #> split_lines #> map trim_line; 
47499
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate  avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
47060
diff
changeset

763 

67179  764 
fun normalize_lines str = 
765 
if exists_string (fn s => s = "\r") str then 

766 
split_lines str > map trim_line > cat_lines 

767 
else str; 

768 

24593
1547ea587f5a
added some int constraints (ML_Parse.fix_ints not active here);
wenzelm
parents:
24148
diff
changeset

769 
fun replicate_string (0: int) _ = "" 
10951  770 
 replicate_string 1 a = a 
771 
 replicate_string k a = 

772 
if k mod 2 = 0 then replicate_string (k div 2) (a ^ a) 

773 
else replicate_string (k div 2) (a ^ a) ^ a; 

774 

31250  775 
fun translate_string f = String.translate (f o String.str); 
776 

65934  777 
val encode_lines = translate_string (fn "\n" => "\v"  c => c); 
778 
val decode_lines = translate_string (fn "\v" => "\n"  c => c); 

779 

63304  780 
fun align_right c k s = 
781 
let 

782 
val _ = if size c <> 1 orelse size s > k 

783 
then raise Fail "align_right" else () 

784 
in replicate_string (k  size s) c ^ s end; 

785 

29882
29154e67731d
New command find_consts searching for constants by type (by Timothy Bourke).
kleing
parents:
29209
diff
changeset

786 
(*crude matching of str against simple glob pat*) 
29154e67731d
New command find_consts searching for constants by type (by Timothy Bourke).
kleing
parents:
29209
diff
changeset

787 
fun match_string pat str = 
29154e67731d
New command find_consts searching for constants by type (by Timothy Bourke).
kleing
parents:
29209
diff
changeset

788 
let 
29154e67731d
New command find_consts searching for constants by type (by Timothy Bourke).
kleing
parents:
29209
diff
changeset

789 
fun match [] _ = true 
29154e67731d
New command find_consts searching for constants by type (by Timothy Bourke).
kleing
parents:
29209
diff
changeset

790 
 match (p :: ps) s = 
29154e67731d
New command find_consts searching for constants by type (by Timothy Bourke).
kleing
parents:
29209
diff
changeset

791 
size p <= size s andalso 
29154e67731d
New command find_consts searching for constants by type (by Timothy Bourke).
kleing
parents:
29209
diff
changeset

792 
(case try (unprefix p) s of 
29154e67731d
New command find_consts searching for constants by type (by Timothy Bourke).
kleing
parents:
29209
diff
changeset

793 
SOME s' => match ps s' 
29154e67731d
New command find_consts searching for constants by type (by Timothy Bourke).
kleing
parents:
29209
diff
changeset

794 
 NONE => match (p :: ps) (String.substring (s, 1, size s  1))); 
29154e67731d
New command find_consts searching for constants by type (by Timothy Bourke).
kleing
parents:
29209
diff
changeset

795 
in match (space_explode "*" pat) str end; 
23220  796 

35976  797 

69468  798 

41516
3a70387b5e01
smart_string_of_real: print integer values without fractional part;
wenzelm
parents:
41494
diff
changeset

799 
(** reals **) 
3a70387b5e01
smart_string_of_real: print integer values without fractional part;
wenzelm
parents:
41494
diff
changeset

800 

3a70387b5e01
smart_string_of_real: print integer values without fractional part;
wenzelm
parents:
41494
diff
changeset

801 
val string_of_real = Real.fmt (StringCvt.GEN NONE); 
3a70387b5e01
smart_string_of_real: print integer values without fractional part;
wenzelm
parents:
41494
diff
changeset

802 

3a70387b5e01
smart_string_of_real: print integer values without fractional part;
wenzelm
parents:
41494
diff
changeset

803 
fun signed_string_of_real x = 
3a70387b5e01
smart_string_of_real: print integer values without fractional part;
wenzelm
parents:
41494
diff
changeset

804 
if x < 0.0 then "" ^ string_of_real (~ x) else string_of_real x; 
3a70387b5e01
smart_string_of_real: print integer values without fractional part;
wenzelm
parents:
41494
diff
changeset

805 

3a70387b5e01
smart_string_of_real: print integer values without fractional part;
wenzelm
parents:
41494
diff
changeset

806 

35976  807 

16492  808 
(** lists as sets  see also Pure/General/ord_list.ML **) 
233  809 

26439  810 
(* canonical operations *) 
811 

18923  812 
fun member eq list x = 
813 
let 

814 
fun memb [] = false 

815 
 memb (y :: ys) = eq (x, y) orelse memb ys; 

816 
in memb list end; 

1576
af8f43f742a0
Added some optimized versions of functions dealing with sets
berghofe
parents:
1460
diff
changeset

817 

18923  818 
fun insert eq x xs = if member eq xs x then xs else x :: xs; 
819 
fun remove eq x xs = if member eq xs x then filter_out (fn y => eq (x, y)) xs else xs; 

24049  820 
fun update eq x xs = cons x (remove eq x xs); 
233  821 

33049
c38f02fdf35d
curried inter as canonical list operation (beware of argument order)
haftmann
parents:
33040
diff
changeset

822 
fun inter eq xs = filter (member eq xs); 
c38f02fdf35d
curried inter as canonical list operation (beware of argument order)
haftmann
parents:
33040
diff
changeset

823 

33042  824 
fun union eq = fold (insert eq); 
19301  825 
fun subtract eq = fold (remove eq); 
826 

30572
8fbc355100f2
Library.merge/OrdList.union: optimize the important special case where the tables coincide  NOTE: this changes both the operational behaviour and the result for nonstandard eq/ord notion;
wenzelm
parents:
30570
diff
changeset

827 
fun merge eq (xs, ys) = 
8fbc355100f2
Library.merge/OrdList.union: optimize the important special case where the tables coincide  NOTE: this changes both the operational behaviour and the result for nonstandard eq/ord notion;
wenzelm
parents:
30570
diff
changeset

828 
if pointer_eq (xs, ys) then xs 
8fbc355100f2
Library.merge/OrdList.union: optimize the important special case where the tables coincide  NOTE: this changes both the operational behaviour and the result for nonstandard eq/ord notion;
wenzelm
parents:
30570
diff
changeset

829 
else if null xs then ys 
8fbc355100f2
Library.merge/OrdList.union: optimize the important special case where the tables coincide  NOTE: this changes both the operational behaviour and the result for nonstandard eq/ord notion;
wenzelm
parents:
30570
diff
changeset

830 
else fold_rev (insert eq) ys xs; 
0  831 

26439  832 

33050  833 
(* subset and set equality *) 
834 

33038  835 
fun subset eq (xs, ys) = forall (member eq ys) xs; 
1576
af8f43f742a0
Added some optimized versions of functions dealing with sets
berghofe
parents:
1460
diff
changeset

836 

33038  837 
fun eq_set eq (xs, ys) = 
20348  838 
eq_list eq (xs, ys) orelse 
33038  839 
(subset eq (xs, ys) andalso subset (eq o swap) (ys, xs)); 
19301  840 

265  841 

233  842 
(*makes a list of the distinct members of the input; preserves order, takes 
843 
first of equal elements*) 

19046
bc5c6c9b114e
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
19011
diff
changeset

844 
fun distinct eq lst = 
233  845 
let 
846 
fun dist (rev_seen, []) = rev rev_seen 

847 
 dist (rev_seen, x :: xs) = 

18923  848 
if member eq rev_seen x then dist (rev_seen, xs) 
233  849 
else dist (x :: rev_seen, xs); 
19046
bc5c6c9b114e
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
19011
diff
changeset

850 
in dist ([], lst) end; 
233  851 

255
ee132db91681
added if_none, parents, commas, gen_duplicates, duplicates, assoc2;
wenzelm
parents:
245
diff
changeset

852 
(*returns a list containing all repeated elements exactly once; preserves 
ee132db91681
added if_none, parents, commas, gen_duplicates, duplicates, assoc2;
wenzelm
parents:
245
diff
changeset

853 
order, takes first of equal elements*) 
18966  854 
fun duplicates eq lst = 
255
ee132db91681
added if_none, parents, commas, gen_duplicates, duplicates, assoc2;
wenzelm
parents:
245
diff
changeset

855 
let 
ee132db91681
added if_none, parents, commas, gen_duplicates, duplicates, assoc2;
wenzelm
parents:
245
diff
changeset

856 
fun dups (rev_dups, []) = rev rev_dups 
ee132db91681
added if_none, parents, commas, gen_duplicates, duplicates, assoc2;
wenzelm
parents:
245
diff
changeset

857 
 dups (rev_dups, x :: xs) = 
18923  858 
if member eq rev_dups x orelse not (member eq xs x) then 
255
ee132db91681
added if_none, parents, commas, gen_duplicates, duplicates, assoc2;
wenzelm
parents:
245
diff
changeset

859 
dups (rev_dups, xs) 
ee132db91681
added if_none, parents, commas, gen_duplicates, duplicates, assoc2;
wenzelm
parents:
245
diff
changeset

860 
else dups (x :: rev_dups, xs); 
18966  861 
in dups ([], lst) end; 
255
ee132db91681
added if_none, parents, commas, gen_duplicates, duplicates, assoc2;
wenzelm
parents:
245
diff
changeset

862 

16878  863 
fun has_duplicates eq = 
864 
let 

865 
fun dups [] = false 

866 
 dups (x :: xs) = member eq xs x orelse dups xs; 

867 
in dups end; 

868 

255
ee132db91681
added if_none, parents, commas, gen_duplicates, duplicates, assoc2;
wenzelm
parents:
245
diff
changeset

869 

32352  870 
(* matrices *) 
871 

872 
fun map_transpose f xss = 

873 
let 

40722
441260986b63
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
wenzelm
parents:
40721
diff
changeset

874 
val n = 
441260986b63
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
wenzelm
parents:
40721
diff
changeset

875 
(case distinct (op =) (map length xss) of 
441260986b63
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
wenzelm
parents:
40721
diff
changeset

876 
[] => 0 
32352  877 
 [n] => n 
40722
441260986b63
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
wenzelm
parents:
40721
diff
changeset

878 
 _ => raise ListPair.UnequalLengths); 
33206  879 
in map_range (fn m => f (map (fn xs => nth xs m) xss)) n end; 
32352  880 

881 

23220  882 

22142  883 
(** lists as multisets **) 
884 

33078
3aea60ca3900
multiset operations with canonical argument order
haftmann
parents:
33063
diff
changeset

885 
fun remove1 eq x [] = [] 
3aea60ca3900
multiset operations with canonical argument order
haftmann
parents:
33063
diff
changeset

886 
 remove1 eq x (y :: ys) = if eq (x, y) then ys else y :: remove1 eq x ys; 
22142  887 

33078
3aea60ca3900
multiset operations with canonical argument order
haftmann
parents:
33063
diff
changeset

888 
fun combine eq xs ys = fold (remove1 eq) ys xs @ ys; 
233  889 

33079  890 
fun submultiset _ ([], _) = true 
891 
 submultiset eq (x :: xs, ys) = member eq ys x andalso submultiset eq (xs, remove1 eq x ys); 

892 

0  893 

894 

2506  895 
(** orders **) 
896 

67560  897 
fun is_equal ord = ord = EQUAL; 
898 
fun is_less ord = ord = LESS; 

899 
fun is_less_equal ord = ord = LESS orelse ord = EQUAL; 

900 
fun is_greater ord = ord = GREATER; 

901 
fun is_greater_equal ord = ord = GREATER orelse ord = EQUAL; 

18966  902 

4445  903 
fun rev_order LESS = GREATER 
904 
 rev_order EQUAL = EQUAL 

905 
 rev_order GREATER = LESS; 

906 

4479  907 
(*assume rel is a linear strict order*) 
4445  908 
fun make_ord rel (x, y) = 
909 
if rel (x, y) then LESS 

910 
else if rel (y, x) then GREATER 

911 
else EQUAL; 

912 

25224  913 
fun bool_ord (false, true) = LESS 
914 
 bool_ord (true, false) = GREATER 

915 
 bool_ord _ = EQUAL; 

916 

15051
0dbbab9f77fe
int_ord = Int.compare, string_ord = String.compare;
wenzelm
parents:
15035
diff
changeset

917 
val int_ord = Int.compare; 
0dbbab9f77fe
int_ord = Int.compare, string_ord = String.compare;
wenzelm
parents:
15035
diff
changeset

918 
val string_ord = String.compare; 
2506  919 

16676  920 
fun fast_string_ord (s1, s2) = 
43793  921 
if pointer_eq (s1, s2) then EQUAL 
922 
else (case int_ord (size s1, size s2) of EQUAL => string_ord (s1, s2)  ord => ord); 

16676  923 

16492  924 
fun option_ord ord (SOME x, SOME y) = ord (x, y) 
925 
 option_ord _ (NONE, NONE) = EQUAL 

926 
 option_ord _ (NONE, SOME _) = LESS 

927 
 option_ord _ (SOME _, NONE) = GREATER; 

928 

4343  929 
(*lexicographic product*) 
930 
fun prod_ord a_ord b_ord ((x, y), (x', y')) = 

931 
(case a_ord (x, x') of EQUAL => b_ord (y, y')  ord => ord); 

932 

933 
(*dictionary order  in general NOT wellfounded!*) 

16984  934 
fun dict_ord elem_ord (x :: xs, y :: ys) = 
935 
(case elem_ord (x, y) of EQUAL => dict_ord elem_ord (xs, ys)  ord => ord) 

936 
 dict_ord _ ([], []) = EQUAL 

4343  937 
 dict_ord _ ([], _ :: _) = LESS 
16984  938 
 dict_ord _ (_ :: _, []) = GREATER; 
4343  939 

940 
(*lexicographic product of lists*) 

941 
fun list_ord elem_ord (xs, ys) = 

16676  942 
(case int_ord (length xs, length ys) of EQUAL => dict_ord elem_ord (xs, ys)  ord => ord); 
4343  943 

2506  944 

4621  945 
(* sorting *) 
946 

48271
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

947 
(*stable mergesort  preserves order of equal elements*) 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

948 
fun mergesort unique ord = 
4621  949 
let 
48271
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

950 
fun merge (xs as x :: xs') (ys as y :: ys') = 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

951 
(case ord (x, y) of 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

952 
LESS => x :: merge xs' ys 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

953 
 EQUAL => 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

954 
if unique then merge xs ys' 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

955 
else x :: merge xs' ys 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

956 
 GREATER => y :: merge xs ys') 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

957 
 merge [] ys = ys 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

958 
 merge xs [] = xs; 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

959 

b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

960 
fun merge_all [xs] = xs 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

961 
 merge_all xss = merge_all (merge_pairs xss) 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

962 
and merge_pairs (xs :: ys :: xss) = merge xs ys :: merge_pairs xss 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

963 
 merge_pairs xss = xss; 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

964 

b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

965 
fun runs (x :: y :: xs) = 
18427  966 
(case ord (x, y) of 
48271
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

967 
LESS => ascending y [x] xs 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

968 
 EQUAL => 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

969 
if unique then runs (x :: xs) 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

970 
else ascending y [x] xs 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

971 
 GREATER => descending y [x] xs) 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

972 
 runs xs = [xs] 
4621  973 

48271
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

974 
and ascending x xs (zs as y :: ys) = 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

975 
(case ord (x, y) of 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

976 
LESS => ascending y (x :: xs) ys 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

977 
 EQUAL => 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

978 
if unique then ascending x xs ys 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

979 
else ascending y (x :: xs) ys 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

980 
 GREATER => rev (x :: xs) :: runs zs) 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

981 
 ascending x xs [] = [rev (x :: xs)] 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

982 

b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

983 
and descending x xs (zs as y :: ys) = 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

984 
(case ord (x, y) of 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

985 
GREATER => descending y (x :: xs) ys 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

986 
 EQUAL => 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

987 
if unique then descending x xs ys 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

988 
else (x :: xs) :: runs zs 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

989 
 LESS => (x :: xs) :: runs zs) 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

990 
 descending x xs [] = [x :: xs]; 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

991 

b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

992 
in merge_all o runs end; 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

993 

b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

994 
fun sort ord = mergesort false ord; 
b28defd0b5a5
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
wenzelm
parents:
47499
diff
changeset

995 
fun sort_distinct ord = mergesort true ord; 
18427  996 

4621  997 
val sort_strings = sort string_ord; 
60924
610794dff23c
tuned signature, in accordance to sortBy in Scala;
wenzelm
parents:
59469
diff
changeset

998 
fun sort_by key xs = sort (string_ord o apply2 key) xs; 
4621  999 

1000 

30558
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30190
diff
changeset

1001 
(* items tagged by integer index *) 
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30190
diff
changeset

1002 

2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30190
diff
changeset

1003 
(*insert tags*) 
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30190
diff
changeset

1004 
fun tag_list k [] = [] 
30570  1005 
 tag_list k (x :: xs) = (k:int, x) :: tag_list (k + 1) xs; 
30558
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30190
diff
changeset

1006 

2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30190
diff
changeset

1007 
(*remove tags and suppress duplicates  list is assumed sorted!*) 
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30190
diff
changeset

1008 
fun untag_list [] = [] 
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30190
diff
changeset

1009 
 untag_list [(k: int, x)] = [x] 
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30190
diff
changeset

1010 
 untag_list ((k, x) :: (rest as (k', x') :: _)) = 
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30190
diff
changeset

1011 
if k = k' then untag_list rest 
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30190
diff
changeset

1012 
else x :: untag_list rest; 
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30190
diff
changeset

1013 

2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30190
diff
changeset

1014 
(*return list elements in original order*) 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58635
diff
changeset

1015 
fun order_list list = untag_list (sort (int_ord o apply2 fst) list); 
30558
2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30190
diff
changeset

1016 

2ef9892114fd
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
wenzelm
parents:
30190
diff
changeset

1017 

2506  1018 

4621  1019 
(** misc **) 
233  1020 

19644
0b01436e1843
added divide_and_conquer combinator (by Amine Chaieb);
wenzelm
parents:
19596
diff
changeset

1021 
fun divide_and_conquer decomp x = 
0b01436e1843
added divide_and_conquer combinator (by Amine Chaieb);
wenzelm
parents:
19596
diff
changeset

1022 
let val (ys, recomb) = decomp x 
0b01436e1843
added divide_and_conquer combinator (by Amine Chaieb);
wenzelm
parents:
19596
diff
changeset

1023 
in recomb (map (divide_and_conquer decomp) ys) end; 
0b01436e1843
added divide_and_conquer combinator (by Amine Chaieb);
wenzelm
parents:
19596
diff
changeset

1024 

32978  1025 
fun divide_and_conquer' decomp x s = 
1026 
let val ((ys, recomb), s') = decomp x s 

1027 
in recomb (fold_map (divide_and_conquer' decomp) ys s') end; 

1028 

0  1029 

233  1030 
(*Partition a list into buckets [ bi, b(i+1), ..., bj ] 
0  1031 
putting x in bk if p(k)(x) holds. Preserve order of elements if possible.*) 
1032 
fun partition_list p i j = 

37851  1033 
let 
1034 
fun part (k: int) xs = 

1035 
if k > j then 

1036 
(case xs of 

1037 
[] => [] 

1038 
 _ => raise Fail "partition_list") 

1039 
else 

1040 
let val (ns, rest) = List.partition (p k) xs 

1041 
in ns :: part (k + 1) rest end; 

1042 
in part (i: int) end; 

0  1043 

37851  1044 
fun partition_eq (eq: 'a * 'a > bool) = 
19691  1045 
let 
1046 
fun part [] = [] 

1047 
 part (x :: ys) = 

1048 
let val (xs, xs') = List.partition (fn y => eq (x, y)) ys 

37851  1049 
in (x :: xs) :: part xs' end; 
19691  1050 
in part end; 
1051 

1052 

45626
b4f374a45668
more abstract datatype stamp, which avoids pointless allocation of mutable cells;
wenzelm
parents:
44617
diff
changeset

1053 
(* serial numbers and abstract stamps *) 
16439  1054 

1055 
type serial = int; 

62918  1056 
val serial = Counter.make (); 
19512  1057 
val serial_string = string_of_int o serial; 
1058 

45626
b4f374a45668
more abstract datatype stamp, which avoids pointless allocation of mutable cells;
wenzelm
parents:
44617
diff
changeset

1059 
datatype stamp = Stamp of serial; 
b4f374a45668
more abstract datatype stamp, which avoids pointless allocation of mutable cells;
wenzelm
parents:
44617
diff
changeset

1060 
fun stamp () = Stamp (serial ()); 
b4f374a45668
more abstract datatype stamp, which avoids pointless allocation of mutable cells;
wenzelm
parents:
44617
diff
changeset

1061 

16535
86c9eada525b
added structure Object (from Pure/General/object.ML);
wenzelm
parents:
16492
diff
changeset

1062 

51368
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
50913
diff
changeset

1063 
(* values of any type *) 
16535
86c9eada525b
added structure Object (from Pure/General/object.ML);
wenzelm
parents:
16492
diff
changeset

1064 

86c9eada525b
added structure Object (from Pure/General/object.ML);
wenzelm
parents:
16492
diff
changeset

1065 
(*note that the builtin exception datatype may be extended by new 
86c9eada525b
added structure Object (from Pure/General/object.ML);
wenzelm
parents:
16492
diff
changeset

1066 
constructors at any time*) 
51368
2ea5c7c2d825
tuned signature  prefer terminology of Scala and Axiom;
wenzelm
parents:
50913
diff
changeset

1067 
structure Any = struct type T = exn end; 
16535
86c9eada525b
added structure Object (from Pure/General/object.ML);
wenzelm
parents:
16492
diff
changeset

1068 

43603  1069 

1070 
(* getenv *) 

1071 

1072 
fun getenv x = 

1073 
(case OS.Process.getEnv x of 

1074 
NONE => "" 

1075 
 SOME y => y); 

1076 

1077 
fun getenv_strict x = 

1078 
(case getenv x of 

1079 
"" => error ("Undefined Isabelle environment variable: " ^ quote x) 

1080 
 y => y); 

1081 

1364
8ea1a962ad72
files now define a structure to allow SML/NJ to optimize the code
clasohm
parents:
1290
diff
changeset

1082 
end; 
8ea1a962ad72
files now define a structure to allow SML/NJ to optimize the code
clasohm
parents:
1290
diff
changeset

1083 

32188  1084 
structure Basic_Library: BASIC_LIBRARY = Library; 
1085 
open Basic_Library; 