# HG changeset patch
# User wenzelm
# Date 1119298451 -7200
# Node ID 474472ca4e4dff0517addccdaa70ed786935dce7
# Parent  8144814dc6a1f4d94cfa8194c5ac5df503190802
generalized type of inter;
added substract;
economize heap usage;

diff -r 8144814dc6a1 -r 474472ca4e4d src/Pure/General/ord_list.ML
--- 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;