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