164 val unsuffix: string -> string -> string |
164 val unsuffix: string -> string -> string |
165 val unprefix: string -> string -> string |
165 val unprefix: string -> string -> string |
166 val replicate_string: int -> string -> string |
166 val replicate_string: int -> string -> string |
167 val translate_string: (string -> string) -> string -> string |
167 val translate_string: (string -> string) -> string -> string |
168 |
168 |
169 (*lists as sets*) |
169 (*lists as sets -- see also Pure/General/ord_list.ML*) |
170 val mem: ''a * ''a list -> bool |
170 val mem: ''a * ''a list -> bool |
171 val mem_int: int * int list -> bool |
171 val mem_int: int * int list -> bool |
172 val mem_string: string * string list -> bool |
172 val mem_string: string * string list -> bool |
173 val gen_mem: ('a * 'b -> bool) -> 'a * 'b list -> bool |
173 val gen_mem: ('a * 'b -> bool) -> 'a * 'b list -> bool |
174 val ins: ''a * ''a list -> ''a list |
174 val ins: ''a * ''a list -> ''a list |
175 val ins_int: int * int list -> int list |
175 val ins_int: int * int list -> int list |
176 val ins_string: string * string list -> string list |
176 val ins_string: string * string list -> string list |
177 val gen_ins: ('a * 'a -> bool) -> 'a * 'a list -> 'a list |
177 val gen_ins: ('a * 'a -> bool) -> 'a * 'a list -> 'a list |
|
178 val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool |
178 val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list |
179 val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list |
179 val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list |
180 val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list |
180 val union: ''a list * ''a list -> ''a list |
181 val union: ''a list * ''a list -> ''a list |
181 val union_int: int list * int list -> int list |
182 val union_int: int list * int list -> int list |
182 val union_string: string list * string list -> string list |
183 val union_string: string list * string list -> string list |
229 (*orders*) |
230 (*orders*) |
230 val rev_order: order -> order |
231 val rev_order: order -> order |
231 val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order |
232 val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order |
232 val int_ord: int * int -> order |
233 val int_ord: int * int -> order |
233 val string_ord: string * string -> order |
234 val string_ord: string * string -> order |
|
235 val option_ord: ('a * 'b -> order) -> 'a option * 'b option -> order |
234 val prod_ord: ('a * 'b -> order) -> ('c * 'd -> order) -> ('a * 'c) * ('b * 'd) -> order |
236 val prod_ord: ('a * 'b -> order) -> ('c * 'd -> order) -> ('a * 'c) * ('b * 'd) -> order |
235 val dict_ord: ('a * 'b -> order) -> 'a list * 'b list -> order |
237 val dict_ord: ('a * 'b -> order) -> 'a list * 'b list -> order |
236 val list_ord: ('a * 'b -> order) -> 'a list * 'b list -> order |
238 val list_ord: ('a * 'b -> order) -> 'a list * 'b list -> order |
237 val sort: ('a * 'a -> order) -> 'a list -> 'a list |
239 val sort: ('a * 'a -> order) -> 'a list -> 'a list |
238 val sort_strings: string list -> string list |
240 val sort_strings: string list -> string list |
815 if k mod 2 = 0 then replicate_string (k div 2) (a ^ a) |
817 if k mod 2 = 0 then replicate_string (k div 2) (a ^ a) |
816 else replicate_string (k div 2) (a ^ a) ^ a; |
818 else replicate_string (k div 2) (a ^ a) ^ a; |
817 |
819 |
818 |
820 |
819 |
821 |
820 (** lists as sets **) |
822 (** lists as sets -- see also Pure/General/ord_list.ML **) |
821 |
823 |
822 (*membership in a list*) |
824 (*membership in a list*) |
823 fun x mem [] = false |
825 fun x mem [] = false |
824 | x mem (y :: ys) = x = y orelse x mem ys; |
826 | x mem (y :: ys) = x = y orelse x mem ys; |
825 |
827 |
833 |
835 |
834 (*generalized membership test*) |
836 (*generalized membership test*) |
835 fun gen_mem eq (x, []) = false |
837 fun gen_mem eq (x, []) = false |
836 | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys); |
838 | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys); |
837 |
839 |
838 (*insert and remove*) |
840 (*member, insert, and remove -- with canonical argument order*) |
|
841 fun member eq xs x = gen_mem eq (x, xs); |
839 fun insert eq x xs = if gen_mem eq (x, xs) then xs else x :: xs; |
842 fun insert eq x xs = if gen_mem eq (x, xs) then xs else x :: xs; |
840 fun remove eq x xs = if gen_mem eq (x, xs) then filter_out (fn y => eq (x, y)) xs else xs; |
843 fun remove eq x xs = if gen_mem eq (x, xs) then filter_out (fn y => eq (x, y)) xs else xs; |
841 |
844 |
842 (*insertion into list if not already there*) |
845 (*insertion into list if not already there*) |
843 fun (x ins xs) = if x mem xs then xs else x :: xs; |
846 fun (x ins xs) = if x mem xs then xs else x :: xs; |
1082 else if rel (y, x) then GREATER |
1085 else if rel (y, x) then GREATER |
1083 else EQUAL; |
1086 else EQUAL; |
1084 |
1087 |
1085 val int_ord = Int.compare; |
1088 val int_ord = Int.compare; |
1086 val string_ord = String.compare; |
1089 val string_ord = String.compare; |
|
1090 |
|
1091 fun option_ord ord (SOME x, SOME y) = ord (x, y) |
|
1092 | option_ord _ (NONE, NONE) = EQUAL |
|
1093 | option_ord _ (NONE, SOME _) = LESS |
|
1094 | option_ord _ (SOME _, NONE) = GREATER; |
1087 |
1095 |
1088 (*lexicographic product*) |
1096 (*lexicographic product*) |
1089 fun prod_ord a_ord b_ord ((x, y), (x', y')) = |
1097 fun prod_ord a_ord b_ord ((x, y), (x', y')) = |
1090 (case a_ord (x, x') of EQUAL => b_ord (y, y') | ord => ord); |
1098 (case a_ord (x, x') of EQUAL => b_ord (y, y') | ord => ord); |
1091 |
1099 |