Ordered lists without duplicates.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/ord_list.ML	Sat Jun 18 22:40:51 2005 +0200
@@ -0,0 +1,71 @@
+(*  Title:      Pure/General/ord_list.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Ordered lists without duplicates -- a light-weight representation of
+finite sets.
+*)
+
+signature ORD_LIST =
+sig
+  val member: ('b * 'a -> order) -> 'a list -> 'b -> bool
+  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
+end;
+
+structure OrdList: ORD_LIST =
+struct
+
+fun member ord list x =
+  let
+    fun memb [] = false
+      | memb (y :: ys) =
+          (case ord (x, y) of
+            LESS => false
+          | EQUAL => true
+          | GREATER => memb ys);
+  in memb list end;
+
+exception SAME;
+
+fun insert ord x list =
+  let
+    fun insrt [] = [x]
+      | insrt (lst as y :: ys) =
+          (case ord (x, y) of
+            LESS => x :: lst
+          | EQUAL => raise SAME
+          | GREATER => y :: insrt ys);
+  in insrt list handle SAME => list end;
+
+fun remove ord x list =
+  let
+    fun rmove [] = []
+      | rmove (lst as y :: ys) =
+          (case ord (x, y) of
+            LESS => raise SAME
+          | EQUAL => ys
+          | GREATER => y :: rmove ys);
+  in rmove list handle SAME => list end;
+
+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);
+
+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);
+
+end;