author wenzelm Tue Jun 21 09:35:31 2005 +0200 (2005-06-21) changeset 16511 dad516b121cd parent 16510 606d919ad3c3 child 16512 1fa048f2a590
tuned insert/remove: avoid garbage;
```     1.1 --- a/src/Pure/General/ord_list.ML	Tue Jun 21 09:35:30 2005 +0200
1.2 +++ b/src/Pure/General/ord_list.ML	Tue Jun 21 09:35:31 2005 +0200
1.3 @@ -11,6 +11,8 @@
1.4    val member: ('b * 'a -> order) -> 'a list -> 'b -> bool
1.5    val insert: ('a * 'a -> order) -> 'a -> 'a list -> 'a list
1.6    val remove: ('b * 'a -> order) -> 'b -> 'a list -> 'a list
1.7 +  val subset: ('b * 'a -> order) -> 'b list * 'a list -> bool
1.8 +  val eq_set: ('b * 'a -> order) -> 'b list * 'a list -> bool
1.9    val union: ('a * 'a -> order) -> 'a list -> 'a list -> 'a list
1.10    val inter: ('b * 'a -> order) -> 'b list -> 'a list -> 'a list
1.11    val subtract: ('b * 'a -> order) -> 'b list -> 'a list -> 'a list
1.12 @@ -19,38 +21,58 @@
1.13  structure OrdList: ORD_LIST =
1.14  struct
1.15
1.16 -exception SAME;
1.17 -fun handle_same f x = f x handle SAME => x;
1.18 +
1.19 +(* single elements *)
1.20 +
1.21 +exception ABSENT of int;
1.22 +
1.23 +fun find_index ord list x =
1.24 +  let
1.25 +    fun find i [] = raise ABSENT i
1.26 +      | find i (y :: ys) =
1.27 +          (case ord (x, y) of
1.28 +            LESS => raise ABSENT i
1.29 +          | EQUAL => i
1.30 +          | GREATER => find (i + 1) ys);
1.31 +  in find 0 list end;
1.32
1.33  fun member ord list x =
1.34 -  let
1.35 -    fun memb [] = false
1.36 -      | memb (y :: ys) =
1.37 -          (case ord (x, y) of
1.38 -            LESS => false
1.39 -          | EQUAL => true
1.40 -          | GREATER => memb ys);
1.41 -  in memb list end;
1.42 +  (find_index ord list x; true) handle ABSENT _ => false;
1.43
1.44  fun insert ord x list =
1.45    let
1.46 -    fun insrt [] = [x]
1.47 -      | insrt (lst as y :: ys) =
1.48 -          (case ord (x, y) of
1.49 -            LESS => x :: lst
1.50 -          | EQUAL => raise SAME
1.51 -          | GREATER => y :: insrt ys);
1.52 -  in handle_same insrt list end;
1.53 +    fun insrt 0 ys = x :: ys
1.54 +      | insrt i (y :: ys) = y :: insrt (i - 1) ys;
1.55 +  in (find_index ord list x; list) handle ABSENT i => insrt i list end;
1.56
1.57  fun remove ord x list =
1.58    let
1.59 -    fun rmove [] = raise SAME
1.60 -      | rmove (y :: ys) =
1.61 +    fun rmove 0 (_ :: ys) = ys
1.62 +      | rmove i (y :: ys) = y :: rmove (i - 1) ys;
1.63 +  in rmove (find_index ord list x) list handle ABSENT _ => list end;
1.64 +
1.65 +
1.66 +(* lists as sets *)
1.67 +
1.68 +nonfix subset;
1.69 +fun subset ord (list1, list2) =
1.70 +  let
1.71 +    fun sub [] _ = true
1.72 +      | sub _ [] = false
1.73 +      | sub (lst1 as x :: xs) (y :: ys) =
1.74            (case ord (x, y) of
1.75 -            LESS => raise SAME
1.76 -          | EQUAL => ys
1.77 -          | GREATER => y :: rmove ys);
1.78 -  in handle_same rmove list end;
1.79 +            LESS => false
1.80 +          | EQUAL => sub xs ys
1.81 +          | GREATER => sub lst1 ys);
1.82 +  in sub list1 list2 end;
1.83 +
1.84 +fun eq_set ord lists = list_ord ord lists = EQUAL;
1.85 +
1.86 +
1.87 +(* algebraic operations *)
1.88 +
1.89 +exception SAME;
1.90 +fun handle_same f x = f x handle SAME => x;
1.91
1.92  (*union: insert elements of first list into second list*)
1.93  nonfix union;
```