55 val not_equal: ''a -> ''a -> bool |
55 val not_equal: ''a -> ''a -> bool |
56 val orf: ('a -> bool) * ('a -> bool) -> 'a -> bool |
56 val orf: ('a -> bool) * ('a -> bool) -> 'a -> bool |
57 val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool |
57 val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool |
58 val exists: ('a -> bool) -> 'a list -> bool |
58 val exists: ('a -> bool) -> 'a list -> bool |
59 val forall: ('a -> bool) -> 'a list -> bool |
59 val forall: ('a -> bool) -> 'a list -> bool |
60 val set: bool ref -> bool |
60 val setmp_noncritical: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c |
61 val reset: bool ref -> bool |
61 val setmp: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c |
62 val toggle: bool ref -> bool |
|
63 val change: 'a ref -> ('a -> 'a) -> unit |
|
64 val change_result: 'a ref -> ('a -> 'b * 'a) -> 'b |
|
65 val setmp_noncritical: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c |
|
66 val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c |
|
67 val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c |
62 val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c |
68 |
63 |
69 (*lists*) |
64 (*lists*) |
70 exception UnequalLengths |
65 exception UnequalLengths |
71 val single: 'a -> 'a list |
66 val single: 'a -> 'a list |
121 val prefixes: 'a list -> 'a list list |
116 val prefixes: 'a list -> 'a list list |
122 val suffixes1: 'a list -> 'a list list |
117 val suffixes1: 'a list -> 'a list list |
123 val suffixes: 'a list -> 'a list list |
118 val suffixes: 'a list -> 'a list list |
124 |
119 |
125 (*integers*) |
120 (*integers*) |
126 val inc: int ref -> int |
|
127 val dec: int ref -> int |
|
128 val upto: int * int -> int list |
121 val upto: int * int -> int list |
129 val downto: int * int -> int list |
122 val downto: int * int -> int list |
130 val radixpand: int * int -> int list |
123 val radixpand: int * int -> int list |
131 val radixstring: int * string * int -> string |
124 val radixstring: int * string * int -> string |
132 val string_of_int: int -> string |
125 val string_of_int: int -> string |
324 val forall = List.all; |
317 val forall = List.all; |
325 |
318 |
326 |
319 |
327 (* flags *) |
320 (* flags *) |
328 |
321 |
329 fun set flag = (flag := true; true); |
|
330 fun reset flag = (flag := false; false); |
|
331 fun toggle flag = (flag := not (! flag); ! flag); |
|
332 |
|
333 fun change r f = r := f (! r); |
|
334 fun change_result r f = let val (x, y) = f (! r) in r := y; x end; |
|
335 |
|
336 (*temporarily set flag during execution*) |
322 (*temporarily set flag during execution*) |
337 fun setmp_noncritical flag value f x = |
323 fun setmp_noncritical flag value f x = |
338 uninterruptible (fn restore_attributes => fn () => |
324 uninterruptible (fn restore_attributes => fn () => |
339 let |
325 let |
340 val orig_value = ! flag; |
326 val orig_value = ! flag; |
640 fun suffixes xs = [] :: suffixes1 xs; |
626 fun suffixes xs = [] :: suffixes1 xs; |
641 |
627 |
642 |
628 |
643 |
629 |
644 (** integers **) |
630 (** integers **) |
645 |
|
646 fun inc i = (i := ! i + (1: int); ! i); |
|
647 fun dec i = (i := ! i - (1: int); ! i); |
|
648 |
|
649 |
631 |
650 (* lists of integers *) |
632 (* lists of integers *) |
651 |
633 |
652 (*make the list [from, from + 1, ..., to]*) |
634 (*make the list [from, from + 1, ..., to]*) |
653 fun ((i: int) upto j) = |
635 fun ((i: int) upto j) = |
1053 fun rmod x y = x - y * Real.realFloor (x / y); |
1035 fun rmod x y = x - y * Real.realFloor (x / y); |
1054 |
1036 |
1055 local |
1037 local |
1056 val a = 16807.0; |
1038 val a = 16807.0; |
1057 val m = 2147483647.0; |
1039 val m = 2147483647.0; |
1058 val random_seed = ref 1.0; |
1040 val random_seed = Unsynchronized.ref 1.0; |
1059 in |
1041 in |
1060 |
1042 |
1061 fun random () = CRITICAL (fn () => |
1043 fun random () = CRITICAL (fn () => |
1062 let val r = rmod (a * ! random_seed) m |
1044 let val r = rmod (a * ! random_seed) m |
1063 in (random_seed := r; r) end); |
1045 in (random_seed := r; r) end); |
1119 else chr (ord "0" + i - 52); |
1101 else chr (ord "0" + i - 52); |
1120 |
1102 |
1121 val char_vec = Vector.tabulate (62, gensym_char); |
1103 val char_vec = Vector.tabulate (62, gensym_char); |
1122 fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n))); |
1104 fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n))); |
1123 |
1105 |
1124 val gensym_seed = ref (0: int); |
1106 val gensym_seed = Unsynchronized.ref (0: int); |
1125 |
1107 |
1126 in |
1108 in |
1127 fun gensym pre = pre ^ newid (NAMED_CRITICAL "gensym" (fn () => inc gensym_seed)); |
1109 fun gensym pre = |
|
1110 pre ^ newid (NAMED_CRITICAL "gensym" (fn () => Unsynchronized.inc gensym_seed)); |
1128 end; |
1111 end; |
1129 |
1112 |
1130 |
1113 |
1131 (* stamps and serial numbers *) |
1114 (* stamps and serial numbers *) |
1132 |
1115 |
1133 type stamp = unit ref; |
1116 type stamp = unit Unsynchronized.ref; |
1134 val stamp: unit -> stamp = ref; |
1117 val stamp: unit -> stamp = Unsynchronized.ref; |
1135 |
1118 |
1136 type serial = int; |
1119 type serial = int; |
1137 val serial = Multithreading.serial; |
1120 val serial = Multithreading.serial; |
1138 val serial_string = string_of_int o serial; |
1121 val serial_string = string_of_int o serial; |
1139 |
1122 |