src/Tools/Metis/src/ElementSet.sml
author wenzelm
Wed, 16 Apr 2014 13:28:21 +0200
changeset 56603 4f45570e532d
parent 45778 df6e210fb44c
child 72004 913162a47d9f
permissions -rw-r--r--
more uniform treatment of word case for check / complete;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     1
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     2
(* FINITE SETS WITH A FIXED ELEMENT TYPE                                     *)
39502
cffceed8e7fa fix license
blanchet
parents: 39501
diff changeset
     3
(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License            *)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     4
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     5
43269
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
     6
functor ElementSet (
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
     7
  KM : KeyMap
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
     8
) :> ElementSet
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
     9
where type element = KM.key
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
    10
and type 'a map = 'a KM.map =
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    11
struct
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    12
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    13
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    14
(* A type of set elements.                                                   *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    15
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    16
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    17
type element = KM.key;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    18
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
    19
val compareElement = KM.compareKey;
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
    20
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
    21
val equalElement = KM.equalKey;
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 43269
diff changeset
    22
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    23
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    24
(* A type of finite sets.                                                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    25
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    26
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    27
type 'a map = 'a KM.map;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    28
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    29
datatype set = Set of unit map;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    30
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    31
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    32
(* Converting to and from maps.                                              *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    33
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    34
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    35
fun dest (Set m) = m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    36
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    37
fun mapPartial f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    38
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    39
      fun mf (elt,()) = f elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    40
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    41
      fn Set m => KM.mapPartial mf m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    42
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    43
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    44
fun map f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    45
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    46
      fun mf (elt,()) = f elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    47
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    48
      fn Set m => KM.map mf m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    49
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    50
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    51
fun domain m = Set (KM.transform (fn _ => ()) m);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    52
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    53
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    54
(* Constructors.                                                             *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    55
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    56
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    57
val empty = Set (KM.new ());
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    58
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    59
fun singleton elt = Set (KM.singleton (elt,()));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    60
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    61
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    62
(* Set size.                                                                 *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    63
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    64
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    65
fun null (Set m) = KM.null m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    66
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    67
fun size (Set m) = KM.size m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    68
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    69
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    70
(* Querying.                                                                 *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    71
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    72
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    73
fun peek (Set m) elt =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    74
    case KM.peekKey m elt of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    75
      SOME (elt,()) => SOME elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    76
    | NONE => NONE;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    77
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    78
fun member elt (Set m) = KM.inDomain elt m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    79
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    80
fun pick (Set m) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    81
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    82
      val (elt,_) = KM.pick m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    83
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    84
      elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    85
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    86
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    87
fun nth (Set m) n =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    88
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    89
      val (elt,_) = KM.nth m n
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    90
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    91
      elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    92
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    93
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    94
fun random (Set m) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    95
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    96
      val (elt,_) = KM.random m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    97
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    98
      elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    99
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   100
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   101
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   102
(* Adding.                                                                   *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   103
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   104
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   105
fun add (Set m) elt =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   106
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   107
      val m = KM.insert m (elt,())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   108
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   109
      Set m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   110
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   111
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   112
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   113
  fun uncurriedAdd (elt,set) = add set elt;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   114
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   115
  fun addList set = List.foldl uncurriedAdd set;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   116
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   117
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   118
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   119
(* Removing.                                                                 *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   120
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   121
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   122
fun delete (Set m) elt =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   123
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   124
      val m = KM.delete m elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   125
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   126
      Set m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   127
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   128
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   129
fun remove (Set m) elt =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   130
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   131
      val m = KM.remove m elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   132
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   133
      Set m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   134
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   135
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   136
fun deletePick (Set m) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   137
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   138
      val ((elt,()),m) = KM.deletePick m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   139
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   140
      (elt, Set m)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   141
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   142
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   143
fun deleteNth (Set m) n =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   144
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   145
      val ((elt,()),m) = KM.deleteNth m n
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   146
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   147
      (elt, Set m)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   148
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   149
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   150
fun deleteRandom (Set m) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   151
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   152
      val ((elt,()),m) = KM.deleteRandom m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   153
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   154
      (elt, Set m)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   155
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   156
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   157
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   158
(* Joining.                                                                  *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   159
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   160
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   161
fun union (Set m1) (Set m2) = Set (KM.unionDomain m1 m2);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   162
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   163
fun unionList sets =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   164
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   165
      val ms = List.map dest sets
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   166
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   167
      Set (KM.unionListDomain ms)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   168
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   169
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   170
fun intersect (Set m1) (Set m2) = Set (KM.intersectDomain m1 m2);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   171
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   172
fun intersectList sets =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   173
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   174
      val ms = List.map dest sets
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   175
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   176
      Set (KM.intersectListDomain ms)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   177
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   178
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   179
fun difference (Set m1) (Set m2) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   180
    Set (KM.differenceDomain m1 m2);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   181
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   182
fun symmetricDifference (Set m1) (Set m2) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   183
    Set (KM.symmetricDifferenceDomain m1 m2);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   184
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   185
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   186
(* Mapping and folding.                                                      *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   187
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   188
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   189
fun filter pred =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   190
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   191
      fun mpred (elt,()) = pred elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   192
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   193
      fn Set m => Set (KM.filter mpred m)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   194
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   195
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   196
fun partition pred =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   197
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   198
      fun mpred (elt,()) = pred elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   199
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   200
      fn Set m =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   201
         let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   202
           val (m1,m2) = KM.partition mpred m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   203
         in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   204
           (Set m1, Set m2)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   205
         end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   206
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   207
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   208
fun app f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   209
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   210
      fun mf (elt,()) = f elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   211
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   212
      fn Set m => KM.app mf m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   213
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   214
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   215
fun foldl f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   216
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   217
      fun mf (elt,(),acc) = f (elt,acc)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   218
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   219
      fn acc => fn Set m => KM.foldl mf acc m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   220
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   221
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   222
fun foldr f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   223
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   224
      fun mf (elt,(),acc) = f (elt,acc)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   225
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   226
      fn acc => fn Set m => KM.foldr mf acc m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   227
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   228
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   229
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   230
(* Searching.                                                                *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   231
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   232
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   233
fun findl p =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   234
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   235
      fun mp (elt,()) = p elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   236
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   237
      fn Set m =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   238
         case KM.findl mp m of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   239
           SOME (elt,()) => SOME elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   240
         | NONE => NONE
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   241
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   242
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   243
fun findr p =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   244
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   245
      fun mp (elt,()) = p elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   246
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   247
      fn Set m =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   248
         case KM.findr mp m of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   249
           SOME (elt,()) => SOME elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   250
         | NONE => NONE
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   251
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   252
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   253
fun firstl f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   254
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   255
      fun mf (elt,()) = f elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   256
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   257
      fn Set m => KM.firstl mf m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   258
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   259
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   260
fun firstr f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   261
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   262
      fun mf (elt,()) = f elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   263
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   264
      fn Set m => KM.firstr mf m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   265
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   266
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   267
fun exists p =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   268
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   269
      fun mp (elt,()) = p elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   270
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   271
      fn Set m => KM.exists mp m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   272
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   273
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   274
fun all p =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   275
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   276
      fun mp (elt,()) = p elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   277
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   278
      fn Set m => KM.all mp m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   279
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   280
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   281
fun count p =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   282
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   283
      fun mp (elt,()) = p elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   284
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   285
      fn Set m => KM.count mp m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   286
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   287
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   288
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   289
(* Comparing.                                                                *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   290
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   291
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   292
fun compareValue ((),()) = EQUAL;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   293
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   294
fun equalValue () () = true;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   295
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   296
fun compare (Set m1, Set m2) = KM.compare compareValue (m1,m2);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   297
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   298
fun equal (Set m1) (Set m2) = KM.equal equalValue m1 m2;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   299
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   300
fun subset (Set m1) (Set m2) = KM.subsetDomain m1 m2;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   301
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   302
fun disjoint (Set m1) (Set m2) = KM.disjointDomain m1 m2;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   303
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   304
(* ------------------------------------------------------------------------- *)
43269
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
   305
(* Closing under an operation.                                               *)
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
   306
(* ------------------------------------------------------------------------- *)
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
   307
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
   308
fun closedAdd f =
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
   309
    let
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
   310
      fun adds acc set = foldl check acc set
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
   311
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
   312
      and check (elt,acc) =
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
   313
          if member elt acc then acc
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
   314
          else expand (add acc elt) elt
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
   315
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
   316
      and expand acc elt = adds acc (f elt)
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
   317
    in
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
   318
      adds
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
   319
    end;
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
   320
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
   321
fun close f = closedAdd f empty;
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
   322
3535f16d9714 new Metis version
blanchet
parents: 39502
diff changeset
   323
(* ------------------------------------------------------------------------- *)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   324
(* Converting to and from lists.                                             *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   325
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   326
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   327
fun transform f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   328
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   329
      fun inc (x,l) = f x :: l
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   330
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   331
      foldr inc []
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   332
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   333
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   334
fun toList (Set m) = KM.keys m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   335
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   336
fun fromList elts = addList empty elts;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   337
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   338
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   339
(* Pretty-printing.                                                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   340
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   341
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   342
fun toString set =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   343
    "{" ^ (if null set then "" else Int.toString (size set)) ^ "}";
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   344
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   345
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   346
(* Iterators over sets                                                       *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   347
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   349
type iterator = unit KM.iterator;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   350
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   351
fun mkIterator (Set m) = KM.mkIterator m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   352
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   353
fun mkRevIterator (Set m) = KM.mkRevIterator m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   354
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   355
fun readIterator iter =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   356
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   357
      val (elt,()) = KM.readIterator iter
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   358
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   359
      elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   360
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   361
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   362
fun advanceIterator iter = KM.advanceIterator iter;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   363
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   364
end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   365
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   366
structure IntSet =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   367
ElementSet (IntMap);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   368
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   369
structure IntPairSet =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   370
ElementSet (IntPairMap);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   371
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   372
structure StringSet =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   373
ElementSet (StringMap);