generalized type of inter;
authorwenzelm
Mon Jun 20 22:14:11 2005 +0200 (2005-06-20)
changeset 16497474472ca4e4d
parent 16496 8144814dc6a1
child 16498 9d265401fee0
generalized type of inter;
added substract;
economize heap usage;
src/Pure/General/ord_list.ML
     1.1 --- a/src/Pure/General/ord_list.ML	Mon Jun 20 22:14:10 2005 +0200
     1.2 +++ b/src/Pure/General/ord_list.ML	Mon Jun 20 22:14:11 2005 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Makarius
     1.5  
     1.6  Ordered lists without duplicates -- a light-weight representation of
     1.7 -finite sets.
     1.8 +finite sets, all operations take linear time and economize heap usage.
     1.9  *)
    1.10  
    1.11  signature ORD_LIST =
    1.12 @@ -12,12 +12,16 @@
    1.13    val insert: ('a * 'a -> order) -> 'a -> 'a list -> 'a list
    1.14    val remove: ('b * 'a -> order) -> 'b -> 'a list -> 'a list
    1.15    val union: ('a * 'a -> order) -> 'a list -> 'a list -> 'a list
    1.16 -  val inter: ('a * 'a -> order) -> 'a list -> 'a list -> 'a list
    1.17 +  val inter: ('b * 'a -> order) -> 'b list -> 'a list -> 'a list
    1.18 +  val subtract: ('b * 'a -> order) -> 'b list -> 'a list -> 'a list
    1.19  end;
    1.20  
    1.21  structure OrdList: ORD_LIST =
    1.22  struct
    1.23  
    1.24 +exception SAME;
    1.25 +fun handle_same f x = f x handle SAME => x;
    1.26 +
    1.27  fun member ord list x =
    1.28    let
    1.29      fun memb [] = false
    1.30 @@ -28,8 +32,6 @@
    1.31            | GREATER => memb ys);
    1.32    in memb list end;
    1.33  
    1.34 -exception SAME;
    1.35 -
    1.36  fun insert ord x list =
    1.37    let
    1.38      fun insrt [] = [x]
    1.39 @@ -38,7 +40,7 @@
    1.40              LESS => x :: lst
    1.41            | EQUAL => raise SAME
    1.42            | GREATER => y :: insrt ys);
    1.43 -  in insrt list handle SAME => list end;
    1.44 +  in handle_same insrt list end;
    1.45  
    1.46  fun remove ord x list =
    1.47    let
    1.48 @@ -48,24 +50,44 @@
    1.49              LESS => raise SAME
    1.50            | EQUAL => ys
    1.51            | GREATER => y :: rmove ys);
    1.52 -  in rmove list handle SAME => list end;
    1.53 +  in handle_same rmove list end;
    1.54  
    1.55 +(*union: insert elements of first list into second list*)
    1.56  nonfix union;
    1.57 -fun union _ xs [] = xs
    1.58 -  | union _ [] ys = ys
    1.59 -  | union ord (lst1 as x :: xs) (lst2 as y :: ys) =
    1.60 -      (case ord (x, y) of
    1.61 -        LESS => x :: union ord xs lst2
    1.62 -      | EQUAL => x :: union ord xs ys
    1.63 -      | GREATER => y :: union ord lst1 ys);
    1.64 +fun union ord list1 list2 =
    1.65 +  let
    1.66 +    fun unio [] _ = raise SAME
    1.67 +      | unio xs [] = xs
    1.68 +      | unio (lst1 as x :: xs) (lst2 as y :: ys) =
    1.69 +          (case ord (x, y) of
    1.70 +            LESS => x :: handle_same (unio xs) lst2
    1.71 +          | EQUAL => y :: unio xs ys
    1.72 +          | GREATER => y :: unio lst1 ys);
    1.73 +  in handle_same (unio list1) list2 end;
    1.74  
    1.75 +(*intersection: filter second list for elements present in first list*)
    1.76  nonfix inter;
    1.77 -fun inter _ _ [] = []
    1.78 -  | inter _ [] _ = []
    1.79 -  | inter ord (lst1 as x :: xs) (lst2 as y :: ys) =
    1.80 -      (case ord (x, y) of
    1.81 -        LESS => inter ord xs lst2
    1.82 -      | EQUAL => x :: inter ord xs ys
    1.83 -      | GREATER => inter ord lst1 ys);
    1.84 +fun inter ord list1 list2 =
    1.85 +  let
    1.86 +    fun intr _ [] = raise SAME
    1.87 +      | intr [] _ = []
    1.88 +      | intr (lst1 as x :: xs) (lst2 as y :: ys) =
    1.89 +          (case ord (x, y) of
    1.90 +            LESS => intr xs lst2
    1.91 +          | EQUAL => y :: intr xs ys
    1.92 +          | GREATER => handle_same (intr lst1) ys);
    1.93 +  in handle_same (intr list1) list2 end;
    1.94 +
    1.95 +(*subtraction: filter second list for elements NOT present in first list*)
    1.96 +fun subtract ord list1 list2 =
    1.97 +  let
    1.98 +    fun subtr [] _ = raise SAME
    1.99 +      | subtr _ [] = raise SAME
   1.100 +      | subtr (lst1 as x :: xs) (lst2 as y :: ys) =
   1.101 +          (case ord (x, y) of
   1.102 +            LESS => subtr xs lst2
   1.103 +          | EQUAL => handle_same (subtr xs) ys
   1.104 +          | GREATER => y :: subtr lst1 ys);
   1.105 +  in handle_same (subtr list1) list2 end;
   1.106  
   1.107  end;