equal
deleted
inserted
replaced
212 val gen_rem: ('a * 'b -> bool) -> 'a list * 'b -> 'a list |
212 val gen_rem: ('a * 'b -> bool) -> 'a list * 'b -> 'a list |
213 val gen_rems: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list |
213 val gen_rems: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list |
214 val gen_distinct: ('a * 'a -> bool) -> 'a list -> 'a list |
214 val gen_distinct: ('a * 'a -> bool) -> 'a list -> 'a list |
215 val distinct: ''a list -> ''a list |
215 val distinct: ''a list -> ''a list |
216 val findrep: ''a list -> ''a list |
216 val findrep: ''a list -> ''a list |
217 val gen_duplicates: ('a * 'a -> bool) -> 'a list -> 'a list |
217 val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list |
218 val duplicates: ''a list -> ''a list |
|
219 val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool |
218 val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool |
220 |
219 |
221 (*lists as tables -- see also Pure/General/alist.ML*) |
220 (*lists as tables -- see also Pure/General/alist.ML*) |
222 val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list |
221 val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list |
223 val gen_merge_lists': ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list |
222 val gen_merge_lists': ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list |
231 val fold_bal: ('a * 'a -> 'a) -> 'a list -> 'a |
230 val fold_bal: ('a * 'a -> 'a) -> 'a list -> 'a |
232 val access_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> int -> 'a |
231 val access_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> int -> 'a |
233 val accesses_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> 'a list |
232 val accesses_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> 'a list |
234 |
233 |
235 (*orders*) |
234 (*orders*) |
|
235 val is_equal: order -> bool |
236 val rev_order: order -> order |
236 val rev_order: order -> order |
237 val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order |
237 val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order |
238 val eq_ord: ('a -> order) -> 'a -> bool |
238 val eq_ord: ('a -> order) -> 'a -> bool |
239 val int_ord: int * int -> order |
239 val int_ord: int * int -> order |
240 val string_ord: string * string -> order |
240 val string_ord: string * string -> order |
1023 | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs; |
1023 | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs; |
1024 |
1024 |
1025 |
1025 |
1026 (*returns a list containing all repeated elements exactly once; preserves |
1026 (*returns a list containing all repeated elements exactly once; preserves |
1027 order, takes first of equal elements*) |
1027 order, takes first of equal elements*) |
1028 fun gen_duplicates eq lst = |
1028 fun duplicates eq lst = |
1029 let |
1029 let |
1030 fun dups (rev_dups, []) = rev rev_dups |
1030 fun dups (rev_dups, []) = rev rev_dups |
1031 | dups (rev_dups, x :: xs) = |
1031 | dups (rev_dups, x :: xs) = |
1032 if member eq rev_dups x orelse not (member eq xs x) then |
1032 if member eq rev_dups x orelse not (member eq xs x) then |
1033 dups (rev_dups, xs) |
1033 dups (rev_dups, xs) |
1034 else dups (x :: rev_dups, xs); |
1034 else dups (x :: rev_dups, xs); |
1035 in |
1035 in dups ([], lst) end; |
1036 dups ([], lst) |
|
1037 end; |
|
1038 |
|
1039 fun duplicates l = gen_duplicates (op =) l; |
|
1040 |
1036 |
1041 fun has_duplicates eq = |
1037 fun has_duplicates eq = |
1042 let |
1038 let |
1043 fun dups [] = false |
1039 fun dups [] = false |
1044 | dups (x :: xs) = member eq xs x orelse dups xs; |
1040 | dups (x :: xs) = member eq xs x orelse dups xs; |
1097 in if 1<=n then acc n else raise Balance end; |
1093 in if 1<=n then acc n else raise Balance end; |
1098 |
1094 |
1099 |
1095 |
1100 |
1096 |
1101 (** orders **) |
1097 (** orders **) |
|
1098 |
|
1099 fun is_equal EQUAL = true |
|
1100 | is_equal _ = false; |
1102 |
1101 |
1103 fun rev_order LESS = GREATER |
1102 fun rev_order LESS = GREATER |
1104 | rev_order EQUAL = EQUAL |
1103 | rev_order EQUAL = EQUAL |
1105 | rev_order GREATER = LESS; |
1104 | rev_order GREATER = LESS; |
1106 |
1105 |