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