src/Pure/General/ord_list.ML
author wenzelm
Fri Nov 25 18:37:14 2011 +0100 (2011-11-25 ago)
changeset 45633 2cb7e34f6096
parent 44334 605381e7c7c5
permissions -rw-r--r--
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
     1 (*  Title:      Pure/General/ord_list.ML
     2     Author:     Makarius
     3 
     4 Ordered lists without duplicates -- a light-weight representation of
     5 finite sets, all operations take linear time and economize heap usage.
     6 *)
     7 
     8 signature ORD_LIST =
     9 sig
    10   type 'a T = 'a list
    11   val make: ('a * 'a -> order) -> 'a list -> 'a T
    12   val member: ('b * 'a -> order) -> 'a T -> 'b -> bool
    13   val insert: ('a * 'a -> order) -> 'a -> 'a T -> 'a T
    14   val remove: ('b * 'a -> order) -> 'b -> 'a T -> 'a T
    15   val subset: ('b * 'a -> order) -> 'b T * 'a T -> bool
    16   val union: ('a * 'a -> order) -> 'a T -> 'a T -> 'a T
    17   val unions: ('a * 'a -> order) -> 'a T list -> 'a T
    18   val merge: ('a * 'a -> order) -> 'a T * 'a T -> 'a T
    19   val inter: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
    20   val subtract: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
    21 end;
    22 
    23 structure Ord_List: ORD_LIST =
    24 struct
    25 
    26 type 'a T = 'a list;
    27 fun make ord = sort_distinct ord;
    28 
    29 
    30 (* single elements *)
    31 
    32 fun find_index ord list x =
    33   let
    34     fun find i [] = ~ i
    35       | find i (y :: ys) =
    36           (case ord (x, y) of
    37             LESS => ~ i
    38           | EQUAL => i
    39           | GREATER => find (i + 1) ys);
    40   in find 1 list end;
    41 
    42 fun member ord list x = find_index ord list x > 0;
    43 
    44 fun insert ord x list =
    45   let
    46     fun insrt 1 ys = x :: ys
    47       | insrt i (y :: ys) = y :: insrt (i - 1) ys;
    48     val idx = find_index ord list x;
    49   in if idx > 0 then list else insrt (~ idx) list end;
    50 
    51 fun remove ord x list =
    52   let
    53     fun rmove 1 (_ :: ys) = ys
    54       | rmove i (y :: ys) = y :: rmove (i - 1) ys;
    55     val idx = find_index ord list x;
    56   in if idx > 0 then rmove idx list else list end;
    57 
    58 
    59 (* lists as sets *)
    60 
    61 fun subset ord (list1, list2) =
    62   let
    63     fun sub [] _ = true
    64       | sub _ [] = false
    65       | sub (lst1 as x :: xs) (y :: ys) =
    66           (case ord (x, y) of
    67             LESS => false
    68           | EQUAL => sub xs ys
    69           | GREATER => sub lst1 ys);
    70   in sub list1 list2 end;
    71 
    72 
    73 (* algebraic operations *)
    74 
    75 exception SAME;
    76 fun handle_same f x = f x handle SAME => x;
    77 
    78 (*union: insert elements of first list into second list*)
    79 fun union ord list1 list2 =
    80   let
    81     fun unio [] _ = raise SAME
    82       | unio xs [] = xs
    83       | unio (lst1 as x :: xs) (lst2 as y :: ys) =
    84           (case ord (x, y) of
    85             LESS => x :: handle_same (unio xs) lst2
    86           | EQUAL => y :: unio xs ys
    87           | GREATER => y :: unio lst1 ys);
    88   in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end;
    89 
    90 fun unions ord lists =
    91   let
    92     fun unios (xs :: ys :: rest) acc = unios rest (union ord xs ys :: acc)
    93       | unios [xs] (ys :: acc) = unios (union ord xs ys :: acc) []
    94       | unios [xs] [] = xs
    95       | unios [] [] = []
    96       | unios [] acc = unios acc [];
    97   in unios lists [] end;
    98 
    99 fun merge ord (list1, list2) = union ord list2 list1;
   100 
   101 (*intersection: filter second list for elements present in first list*)
   102 fun inter ord list1 list2 =
   103   let
   104     fun intr _ [] = raise SAME
   105       | intr [] _ = []
   106       | intr (lst1 as x :: xs) (lst2 as y :: ys) =
   107           (case ord (x, y) of
   108             LESS => intr xs lst2
   109           | EQUAL => y :: intr xs ys
   110           | GREATER => handle_same (intr lst1) ys);
   111   in handle_same (intr list1) list2 end;
   112 
   113 (*subtraction: filter second list for elements NOT present in first list*)
   114 fun subtract ord list1 list2 =
   115   let
   116     fun subtr [] _ = raise SAME
   117       | subtr _ [] = raise SAME
   118       | subtr (lst1 as x :: xs) (lst2 as y :: ys) =
   119           (case ord (x, y) of
   120             LESS => subtr xs lst2
   121           | EQUAL => handle_same (subtr xs) ys
   122           | GREATER => y :: subtr lst1 ys);
   123   in handle_same (subtr list1) list2 end;
   124 
   125 end;