src/Pure/General/ord_list.ML
author wenzelm
Thu Jul 19 23:18:48 2007 +0200 (2007-07-19)
changeset 23863 8f3099589cfa
parent 22364 ddb91c9eb0fc
child 28354 c5fe7372ae4e
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/General/ord_list.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Ordered lists without duplicates -- a light-weight representation of
     6 finite sets, all operations take linear time and economize heap usage.
     7 *)
     8 
     9 signature ORD_LIST =
    10 sig
    11   val member: ('b * 'a -> order) -> 'a list -> 'b -> bool
    12   val insert: ('a * 'a -> order) -> 'a -> 'a list -> 'a list
    13   val remove: ('b * 'a -> order) -> 'b -> 'a list -> 'a list
    14   val subset: ('b * 'a -> order) -> 'b list * 'a list -> bool
    15   val union: ('a * 'a -> order) -> 'a list -> 'a list -> 'a list
    16   val inter: ('b * 'a -> order) -> 'b list -> 'a list -> 'a list
    17   val subtract: ('b * 'a -> order) -> 'b list -> 'a list -> 'a list
    18 end;
    19 
    20 structure OrdList: ORD_LIST =
    21 struct
    22 
    23 
    24 (* single elements *)
    25 
    26 fun find_index ord list x =
    27   let
    28     fun find i [] = ~ i
    29       | find i (y :: ys) =
    30           (case ord (x, y) of
    31             LESS => ~ i
    32           | EQUAL => i
    33           | GREATER => find (i + 1) ys);
    34   in find 1 list end;
    35 
    36 fun member ord list x = find_index ord list x > 0;
    37 
    38 fun insert ord x list =
    39   let
    40     fun insrt 1 ys = x :: ys
    41       | insrt i (y :: ys) = y :: insrt (i - 1) ys;
    42     val idx = find_index ord list x;
    43   in if idx > 0 then list else insrt (~ idx) list end;
    44 
    45 fun remove ord x list =
    46   let
    47     fun rmove 1 (_ :: ys) = ys
    48       | rmove i (y :: ys) = y :: rmove (i - 1) ys;
    49     val idx = find_index ord list x;
    50   in if idx > 0 then rmove idx list else list end;
    51 
    52 
    53 (* lists as sets *)
    54 
    55 nonfix subset;
    56 fun subset ord (list1, list2) =
    57   let
    58     fun sub [] _ = true
    59       | sub _ [] = false
    60       | sub (lst1 as x :: xs) (y :: ys) =
    61           (case ord (x, y) of
    62             LESS => false
    63           | EQUAL => sub xs ys
    64           | GREATER => sub lst1 ys);
    65   in sub list1 list2 end;
    66 
    67 
    68 (* algebraic operations *)
    69 
    70 exception SAME;
    71 fun handle_same f x = f x handle SAME => x;
    72 
    73 (*union: insert elements of first list into second list*)
    74 nonfix union;
    75 fun union ord list1 list2 =
    76   let
    77     fun unio [] _ = raise SAME
    78       | unio xs [] = xs
    79       | unio (lst1 as x :: xs) (lst2 as y :: ys) =
    80           (case ord (x, y) of
    81             LESS => x :: handle_same (unio xs) lst2
    82           | EQUAL => y :: unio xs ys
    83           | GREATER => y :: unio lst1 ys);
    84   in handle_same (unio list1) list2 end;
    85 
    86 (*intersection: filter second list for elements present in first list*)
    87 nonfix inter;
    88 fun inter ord list1 list2 =
    89   let
    90     fun intr _ [] = raise SAME
    91       | intr [] _ = []
    92       | intr (lst1 as x :: xs) (lst2 as y :: ys) =
    93           (case ord (x, y) of
    94             LESS => intr xs lst2
    95           | EQUAL => y :: intr xs ys
    96           | GREATER => handle_same (intr lst1) ys);
    97   in handle_same (intr list1) list2 end;
    98 
    99 (*subtraction: filter second list for elements NOT present in first list*)
   100 fun subtract ord list1 list2 =
   101   let
   102     fun subtr [] _ = raise SAME
   103       | subtr _ [] = raise SAME
   104       | subtr (lst1 as x :: xs) (lst2 as y :: ys) =
   105           (case ord (x, y) of
   106             LESS => subtr xs lst2
   107           | EQUAL => handle_same (subtr xs) ys
   108           | GREATER => y :: subtr lst1 ys);
   109   in handle_same (subtr list1) list2 end;
   110 
   111 end;