src/Pure/General/ord_list.ML
author haftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037 b22e44496dc2
parent 30572 8fbc355100f2
child 39687 4e9b6ada3a21
permissions -rw-r--r--
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
     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 inter: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
    18   val subtract: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
    19 end;
    20 
    21 structure OrdList: ORD_LIST =
    22 struct
    23 
    24 type 'a T = 'a list;
    25 fun make ord = sort_distinct ord;
    26 
    27 
    28 (* single elements *)
    29 
    30 fun find_index ord list x =
    31   let
    32     fun find i [] = ~ i
    33       | find i (y :: ys) =
    34           (case ord (x, y) of
    35             LESS => ~ i
    36           | EQUAL => i
    37           | GREATER => find (i + 1) ys);
    38   in find 1 list end;
    39 
    40 fun member ord list x = find_index ord list x > 0;
    41 
    42 fun insert ord x list =
    43   let
    44     fun insrt 1 ys = x :: ys
    45       | insrt i (y :: ys) = y :: insrt (i - 1) ys;
    46     val idx = find_index ord list x;
    47   in if idx > 0 then list else insrt (~ idx) list end;
    48 
    49 fun remove ord x list =
    50   let
    51     fun rmove 1 (_ :: ys) = ys
    52       | rmove i (y :: ys) = y :: rmove (i - 1) ys;
    53     val idx = find_index ord list x;
    54   in if idx > 0 then rmove idx list else list end;
    55 
    56 
    57 (* lists as sets *)
    58 
    59 fun subset ord (list1, list2) =
    60   let
    61     fun sub [] _ = true
    62       | sub _ [] = false
    63       | sub (lst1 as x :: xs) (y :: ys) =
    64           (case ord (x, y) of
    65             LESS => false
    66           | EQUAL => sub xs ys
    67           | GREATER => sub lst1 ys);
    68   in sub list1 list2 end;
    69 
    70 
    71 (* algebraic operations *)
    72 
    73 exception SAME;
    74 fun handle_same f x = f x handle SAME => x;
    75 
    76 (*union: insert elements of first list into second list*)
    77 fun union ord list1 list2 =
    78   let
    79     fun unio [] _ = raise SAME
    80       | unio xs [] = xs
    81       | unio (lst1 as x :: xs) (lst2 as y :: ys) =
    82           (case ord (x, y) of
    83             LESS => x :: handle_same (unio xs) lst2
    84           | EQUAL => y :: unio xs ys
    85           | GREATER => y :: unio lst1 ys);
    86   in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end;
    87 
    88 (*intersection: filter second list for elements present in first list*)
    89 fun inter ord list1 list2 =
    90   let
    91     fun intr _ [] = raise SAME
    92       | intr [] _ = []
    93       | intr (lst1 as x :: xs) (lst2 as y :: ys) =
    94           (case ord (x, y) of
    95             LESS => intr xs lst2
    96           | EQUAL => y :: intr xs ys
    97           | GREATER => handle_same (intr lst1) ys);
    98   in handle_same (intr list1) list2 end;
    99 
   100 (*subtraction: filter second list for elements NOT present in first list*)
   101 fun subtract ord list1 list2 =
   102   let
   103     fun subtr [] _ = raise SAME
   104       | subtr _ [] = raise SAME
   105       | subtr (lst1 as x :: xs) (lst2 as y :: ys) =
   106           (case ord (x, y) of
   107             LESS => subtr xs lst2
   108           | EQUAL => handle_same (subtr xs) ys
   109           | GREATER => y :: subtr lst1 ys);
   110   in handle_same (subtr list1) list2 end;
   111 
   112 end;