# HG changeset patch
# User wenzelm
# Date 1119339331 -7200
# Node ID dad516b121cdefa291b564b50fb5a7c32e1b8db0
# Parent  606d919ad3c3d8c5ad5c436b1aeee55b6560544d
added subset, eq_set;
tuned insert/remove: avoid garbage;

diff -r 606d919ad3c3 -r dad516b121cd src/Pure/General/ord_list.ML
--- a/src/Pure/General/ord_list.ML	Tue Jun 21 09:35:30 2005 +0200
+++ b/src/Pure/General/ord_list.ML	Tue Jun 21 09:35:31 2005 +0200
@@ -11,6 +11,8 @@
   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 subset: ('b * 'a -> order) -> 'b list * 'a list -> bool
+  val eq_set: ('b * 'a -> order) -> 'b list * 'a list -> bool
   val union: ('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
@@ -19,38 +21,58 @@
 structure OrdList: ORD_LIST =
 struct
 
-exception SAME;
-fun handle_same f x = f x handle SAME => x;
+
+(* single elements *)
+
+exception ABSENT of int;
+
+fun find_index ord list x =
+  let
+    fun find i [] = raise ABSENT i
+      | find i (y :: ys) =
+          (case ord (x, y) of
+            LESS => raise ABSENT i
+          | EQUAL => i
+          | GREATER => find (i + 1) ys);
+  in find 0 list end;
 
 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;
+  (find_index ord list x; true) handle ABSENT _ => false;
 
 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 handle_same insrt list end;
+    fun insrt 0 ys = x :: ys
+      | insrt i (y :: ys) = y :: insrt (i - 1) ys;
+  in (find_index ord list x; list) handle ABSENT i => insrt i list end;
 
 fun remove ord x list =
   let
-    fun rmove [] = raise SAME
-      | rmove (y :: ys) =
+    fun rmove 0 (_ :: ys) = ys
+      | rmove i (y :: ys) = y :: rmove (i - 1) ys;
+  in rmove (find_index ord list x) list handle ABSENT _ => list end;
+
+
+(* lists as sets *)
+
+nonfix subset;
+fun subset ord (list1, list2) =
+  let
+    fun sub [] _ = true
+      | sub _ [] = false
+      | sub (lst1 as x :: xs) (y :: ys) =
           (case ord (x, y) of
-            LESS => raise SAME
-          | EQUAL => ys
-          | GREATER => y :: rmove ys);
-  in handle_same rmove list end;
+            LESS => false
+          | EQUAL => sub xs ys
+          | GREATER => sub lst1 ys);
+  in sub list1 list2 end;
+
+fun eq_set ord lists = list_ord ord lists = EQUAL;
+
+
+(* algebraic operations *)
+
+exception SAME;
+fun handle_same f x = f x handle SAME => x;
 
 (*union: insert elements of first list into second list*)
 nonfix union;