src/Tools/Metis/src/ElementSet.sml
author blanchet
Thu, 16 Sep 2010 07:30:15 +0200
changeset 39444 beabb8443ee4
parent 39443 e330437cd22a
child 39501 aaa7078fff55
permissions -rw-r--r--
MIT license -> BSD License
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                                     *)
39444
beabb8443ee4 MIT license -> BSD License
blanchet
parents: 39443
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
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     6
functor ElementSet (KM : KeyMap) :> ElementSet
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     7
where type element = KM.key and type 'a map = 'a KM.map =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     8
struct
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     9
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    10
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    11
(* A type of set elements.                                                   *)
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
type element = KM.key;
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
(* A type of finite sets.                                                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    18
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    19
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    20
type 'a map = 'a KM.map;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    21
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    22
datatype set = Set of unit map;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    23
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    24
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    25
(* Converting to and from maps.                                              *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    26
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    27
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    28
fun dest (Set m) = m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    29
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    30
fun mapPartial f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    31
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    32
      fun mf (elt,()) = f elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    33
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    34
      fn Set m => KM.mapPartial mf m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    35
    end;
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 map 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.map 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 domain m = Set (KM.transform (fn _ => ()) m);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    45
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    46
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    47
(* Constructors.                                                             *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    48
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    49
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    50
val empty = Set (KM.new ());
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    51
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    52
fun singleton elt = Set (KM.singleton (elt,()));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    53
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    54
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    55
(* Set size.                                                                 *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    56
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    57
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    58
fun null (Set m) = KM.null m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    59
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    60
fun size (Set m) = KM.size m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    61
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    62
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    63
(* Querying.                                                                 *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    64
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    65
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    66
fun peek (Set m) elt =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    67
    case KM.peekKey m elt of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    68
      SOME (elt,()) => SOME elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    69
    | NONE => NONE;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    70
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    71
fun member elt (Set m) = KM.inDomain elt m;
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 pick (Set m) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    74
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    75
      val (elt,_) = KM.pick m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    76
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    77
      elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    78
    end;
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 nth (Set m) n =
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.nth m n
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 random (Set m) =
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.random m
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
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    95
(* Adding.                                                                   *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    96
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    97
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    98
fun add (Set m) elt =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    99
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   100
      val m = KM.insert m (elt,())
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   101
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   102
      Set m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   103
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   104
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   105
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   106
  fun uncurriedAdd (elt,set) = add set elt;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   107
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   108
  fun addList set = List.foldl uncurriedAdd set;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   109
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   110
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   111
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   112
(* Removing.                                                                 *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   113
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   114
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   115
fun delete (Set m) elt =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   116
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   117
      val m = KM.delete m elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   118
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   119
      Set m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   120
    end;
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 remove (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.remove 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 deletePick (Set m) =
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 ((elt,()),m) = KM.deletePick m
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
      (elt, 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 deleteNth (Set m) n =
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.deleteNth m n
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 deleteRandom (Set m) =
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.deleteRandom m
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
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   151
(* Joining.                                                                  *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   152
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   153
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   154
fun union (Set m1) (Set m2) = Set (KM.unionDomain m1 m2);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   155
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   156
fun unionList sets =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   157
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   158
      val ms = List.map dest sets
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   159
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   160
      Set (KM.unionListDomain ms)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   161
    end;
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 intersect (Set m1) (Set m2) = Set (KM.intersectDomain m1 m2);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   164
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   165
fun intersectList sets =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   166
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   167
      val ms = List.map dest sets
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   168
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   169
      Set (KM.intersectListDomain ms)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   170
    end;
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 difference (Set m1) (Set m2) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   173
    Set (KM.differenceDomain m1 m2);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   174
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   175
fun symmetricDifference (Set m1) (Set m2) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   176
    Set (KM.symmetricDifferenceDomain m1 m2);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   177
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   178
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   179
(* Mapping and folding.                                                      *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   180
(* ------------------------------------------------------------------------- *)
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 filter pred =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   183
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   184
      fun mpred (elt,()) = pred elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   185
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   186
      fn Set m => Set (KM.filter mpred m)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   187
    end;
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 partition 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 =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   194
         let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   195
           val (m1,m2) = KM.partition mpred m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   196
         in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   197
           (Set m1, Set m2)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   198
         end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   199
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   200
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   201
fun app f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   202
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   203
      fun mf (elt,()) = f elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   204
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   205
      fn Set m => KM.app mf m
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 foldl 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,(),acc) = f (elt,acc)
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 acc => fn Set m => KM.foldl mf acc 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 foldr 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.foldr 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
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   223
(* Searching.                                                                *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   224
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   225
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   226
fun findl p =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   227
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   228
      fun mp (elt,()) = p elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   229
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   230
      fn Set m =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   231
         case KM.findl mp m of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   232
           SOME (elt,()) => SOME elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   233
         | NONE => NONE
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   234
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   235
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   236
fun findr p =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   237
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   238
      fun mp (elt,()) = p elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   239
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   240
      fn Set m =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   241
         case KM.findr mp m of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   242
           SOME (elt,()) => SOME elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   243
         | NONE => NONE
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   244
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   245
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   246
fun firstl f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   247
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   248
      fun mf (elt,()) = f elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   249
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   250
      fn Set m => KM.firstl mf m
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 firstr 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.firstr 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 exists p =
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 mp (elt,()) = p 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.exists mp 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 all 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.all 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 count 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.count 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
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   282
(* Comparing.                                                                *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   283
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   284
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   285
fun compareValue ((),()) = EQUAL;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   286
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   287
fun equalValue () () = true;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   288
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   289
fun compare (Set m1, Set m2) = KM.compare compareValue (m1,m2);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   290
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   291
fun equal (Set m1) (Set m2) = KM.equal equalValue m1 m2;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   292
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   293
fun subset (Set m1) (Set m2) = KM.subsetDomain m1 m2;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   294
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   295
fun disjoint (Set m1) (Set m2) = KM.disjointDomain m1 m2;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   296
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   297
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   298
(* Converting to and from lists.                                             *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   299
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   300
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   301
fun transform f =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   302
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   303
      fun inc (x,l) = f x :: l
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   304
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   305
      foldr inc []
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   306
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   307
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   308
fun toList (Set m) = KM.keys m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   309
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   310
fun fromList elts = addList empty elts;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   311
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   312
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   313
(* Pretty-printing.                                                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   314
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   315
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   316
fun toString set =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   317
    "{" ^ (if null set then "" else Int.toString (size set)) ^ "}";
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   318
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   319
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   320
(* Iterators over sets                                                       *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   321
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   322
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   323
type iterator = unit KM.iterator;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   324
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   325
fun mkIterator (Set m) = KM.mkIterator m;
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 mkRevIterator (Set m) = KM.mkRevIterator m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   328
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   329
fun readIterator iter =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   330
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   331
      val (elt,()) = KM.readIterator iter
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   332
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   333
      elt
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   334
    end;
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 advanceIterator iter = KM.advanceIterator iter;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   337
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   338
end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   339
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   340
structure IntSet =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   341
ElementSet (IntMap);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   342
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   343
structure IntPairSet =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   344
ElementSet (IntPairMap);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   345
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   346
structure StringSet =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   347
ElementSet (StringMap);