added subset, eq_set;
authorwenzelm
Tue Jun 21 09:35:31 2005 +0200 (2005-06-21)
changeset 16511dad516b121cd
parent 16510 606d919ad3c3
child 16512 1fa048f2a590
added subset, eq_set;
tuned insert/remove: avoid garbage;
src/Pure/General/ord_list.ML
     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;