--- a/src/Pure/General/ord_list.ML Mon Jun 20 22:14:10 2005 +0200
+++ b/src/Pure/General/ord_list.ML Mon Jun 20 22:14:11 2005 +0200
@@ -3,7 +3,7 @@
Author: Makarius
Ordered lists without duplicates -- a light-weight representation of
-finite sets.
+finite sets, all operations take linear time and economize heap usage.
*)
signature ORD_LIST =
@@ -12,12 +12,16 @@
val insert: ('a * 'a -> order) -> 'a -> 'a list -> 'a list
val remove: ('b * 'a -> order) -> 'b -> 'a list -> 'a list
val union: ('a * 'a -> order) -> 'a list -> 'a list -> 'a list
- val inter: ('a * 'a -> order) -> 'a list -> 'a list -> 'a list
+ val inter: ('b * 'a -> order) -> 'b list -> 'a list -> 'a list
+ val subtract: ('b * 'a -> order) -> 'b list -> 'a list -> 'a list
end;
structure OrdList: ORD_LIST =
struct
+exception SAME;
+fun handle_same f x = f x handle SAME => x;
+
fun member ord list x =
let
fun memb [] = false
@@ -28,8 +32,6 @@
| GREATER => memb ys);
in memb list end;
-exception SAME;
-
fun insert ord x list =
let
fun insrt [] = [x]
@@ -38,7 +40,7 @@
LESS => x :: lst
| EQUAL => raise SAME
| GREATER => y :: insrt ys);
- in insrt list handle SAME => list end;
+ in handle_same insrt list end;
fun remove ord x list =
let
@@ -48,24 +50,44 @@
LESS => raise SAME
| EQUAL => ys
| GREATER => y :: rmove ys);
- in rmove list handle SAME => list end;
+ in handle_same rmove list end;
+(*union: insert elements of first list into second list*)
nonfix union;
-fun union _ xs [] = xs
- | union _ [] ys = ys
- | union ord (lst1 as x :: xs) (lst2 as y :: ys) =
- (case ord (x, y) of
- LESS => x :: union ord xs lst2
- | EQUAL => x :: union ord xs ys
- | GREATER => y :: union ord lst1 ys);
+fun union ord list1 list2 =
+ let
+ fun unio [] _ = raise SAME
+ | unio xs [] = xs
+ | unio (lst1 as x :: xs) (lst2 as y :: ys) =
+ (case ord (x, y) of
+ LESS => x :: handle_same (unio xs) lst2
+ | EQUAL => y :: unio xs ys
+ | GREATER => y :: unio lst1 ys);
+ in handle_same (unio list1) list2 end;
+(*intersection: filter second list for elements present in first list*)
nonfix inter;
-fun inter _ _ [] = []
- | inter _ [] _ = []
- | inter ord (lst1 as x :: xs) (lst2 as y :: ys) =
- (case ord (x, y) of
- LESS => inter ord xs lst2
- | EQUAL => x :: inter ord xs ys
- | GREATER => inter ord lst1 ys);
+fun inter ord list1 list2 =
+ let
+ fun intr _ [] = raise SAME
+ | intr [] _ = []
+ | intr (lst1 as x :: xs) (lst2 as y :: ys) =
+ (case ord (x, y) of
+ LESS => intr xs lst2
+ | EQUAL => y :: intr xs ys
+ | GREATER => handle_same (intr lst1) ys);
+ in handle_same (intr list1) list2 end;
+
+(*subtraction: filter second list for elements NOT present in first list*)
+fun subtract ord list1 list2 =
+ let
+ fun subtr [] _ = raise SAME
+ | subtr _ [] = raise SAME
+ | subtr (lst1 as x :: xs) (lst2 as y :: ys) =
+ (case ord (x, y) of
+ LESS => subtr xs lst2
+ | EQUAL => handle_same (subtr xs) ys
+ | GREATER => y :: subtr lst1 ys);
+ in handle_same (subtr list1) list2 end;
end;