src/Tools/Metis/src/KeyMap.sml
author blanchet
Mon, 13 Sep 2010 21:11:59 +0200
changeset 39349 2d0a4361c3ef
parent 39348 6f9c9899f99f
child 39353 7f11d833d65b
permissions -rw-r--r--
change license, with Joe Hurd's permission
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 MAPS WITH A FIXED KEY TYPE                                         *)
39349
2d0a4361c3ef change license, with Joe Hurd's permission
blanchet
parents: 39348
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 KeyMap (Key : Ordered) :> KeyMap where type key = Key.t =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     7
struct
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     8
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     9
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    10
(* Importing from the input signature.                                       *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    11
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    12
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    13
type key = Key.t;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    14
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    15
val compareKey = Key.compare;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    16
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    17
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    18
(* Importing useful functionality.                                           *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    19
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    20
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    21
exception Bug = Useful.Bug;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    22
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    23
exception Error = Useful.Error;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    24
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    25
val pointerEqual = Portable.pointerEqual;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    26
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    27
val K = Useful.K;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    28
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    29
val randomInt = Portable.randomInt;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    30
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    31
val randomWord = Portable.randomWord;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    32
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    33
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    34
(* Converting a comparison function to an equality function.                 *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    35
(* ------------------------------------------------------------------------- *)
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 equalKey key1 key2 = compareKey (key1,key2) = EQUAL;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    38
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    39
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    40
(* Priorities.                                                               *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    41
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    42
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    43
type priority = Word.word;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    44
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    45
val randomPriority = randomWord;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    46
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    47
val comparePriority = Word.compare;
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
(* Priority search trees.                                                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    51
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    52
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    53
datatype 'value tree =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    54
    E
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    55
  | T of 'value node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    56
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    57
and 'value node =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    58
    Node of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    59
      {size : int,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    60
       priority : priority,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    61
       left : 'value tree,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    62
       key : key,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    63
       value : 'value,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    64
       right : 'value tree};
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 lowerPriorityNode node1 node2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    67
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    68
      val Node {priority = p1, ...} = node1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    69
      and Node {priority = p2, ...} = node2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    70
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    71
      comparePriority (p1,p2) = LESS
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    72
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    73
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    74
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    75
(* Tree debugging functions.                                                 *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    76
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    77
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    78
(*BasicDebug
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    79
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    80
  fun checkSizes tree =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    81
      case tree of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    82
        E => 0
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    83
      | T (Node {size,left,right,...}) =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    84
        let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    85
          val l = checkSizes left
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    86
          and r = checkSizes right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    87
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    88
          val () = if l + 1 + r = size then () else raise Bug "wrong size"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    89
        in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    90
          size
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    91
        end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    92
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    93
  fun checkSorted x tree =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    94
      case tree of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    95
        E => x
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    96
      | T (Node {left,key,right,...}) =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    97
        let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    98
          val x = checkSorted x left
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    99
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   100
          val () =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   101
              case x of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   102
                NONE => ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   103
              | SOME k =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   104
                case compareKey (k,key) of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   105
                  LESS => ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   106
                | EQUAL => raise Bug "duplicate keys"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   107
                | GREATER => raise Bug "unsorted"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   108
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   109
          val x = SOME key
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   110
        in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   111
          checkSorted x right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   112
        end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   113
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   114
  fun checkPriorities tree =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   115
      case tree of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   116
        E => NONE
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   117
      | T node =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   118
        let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   119
          val Node {left,right,...} = node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   120
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   121
          val () =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   122
              case checkPriorities left of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   123
                NONE => ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   124
              | SOME lnode =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   125
                if not (lowerPriorityNode node lnode) then ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   126
                else raise Bug "left child has greater priority"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   127
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   128
          val () =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   129
              case checkPriorities right of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   130
                NONE => ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   131
              | SOME rnode =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   132
                if not (lowerPriorityNode node rnode) then ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   133
                else raise Bug "right child has greater priority"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   134
        in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   135
          SOME node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   136
        end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   137
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   138
  fun treeCheckInvariants tree =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   139
      let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   140
        val _ = checkSizes tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   141
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   142
        val _ = checkSorted NONE tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   143
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   144
        val _ = checkPriorities tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   145
      in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   146
        tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   147
      end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   148
      handle Error err => raise Bug err;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   149
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   150
*)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   151
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   152
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   153
(* Tree operations.                                                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   154
(* ------------------------------------------------------------------------- *)
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 treeNew () = E;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   157
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   158
fun nodeSize (Node {size = x, ...}) = x;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   159
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   160
fun treeSize tree =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   161
    case tree of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   162
      E => 0
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   163
    | T x => nodeSize x;
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 mkNode priority left key value right =
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 size = treeSize left + 1 + treeSize right
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
      Node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   170
        {size = size,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   171
         priority = priority,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   172
         left = left,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   173
         key = key,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   174
         value = value,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   175
         right = right}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   176
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   177
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   178
fun mkTree priority left key value right =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   179
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   180
      val node = mkNode priority left key value right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   181
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   182
      T node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   183
    end;
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
(* Extracting the left and right spines of a tree.                           *)
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 treeLeftSpine acc tree =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   190
    case tree of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   191
      E => acc
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   192
    | T node => nodeLeftSpine acc node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   193
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   194
and nodeLeftSpine acc node =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   195
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   196
      val Node {left,...} = node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   197
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   198
      treeLeftSpine (node :: acc) left
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 treeRightSpine acc tree =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   202
    case tree of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   203
      E => acc
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   204
    | T node => nodeRightSpine acc node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   205
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   206
and nodeRightSpine acc node =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   207
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   208
      val Node {right,...} = node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   209
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   210
      treeRightSpine (node :: acc) right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   211
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   212
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   213
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   214
(* Singleton trees.                                                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   215
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   216
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   217
fun mkNodeSingleton priority key value =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   218
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   219
      val size = 1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   220
      and left = E
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   221
      and right = E
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   222
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   223
      Node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   224
        {size = size,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   225
         priority = priority,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   226
         left = left,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   227
         key = key,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   228
         value = value,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   229
         right = right}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   230
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   231
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   232
fun nodeSingleton (key,value) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   233
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   234
      val priority = randomPriority ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   235
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   236
      mkNodeSingleton priority key value
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   237
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   238
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   239
fun treeSingleton key_value =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   240
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   241
      val node = nodeSingleton key_value
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   242
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   243
      T node
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
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   247
(* Appending two trees, where every element of the first tree is less than   *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   248
(* every element of the second tree.                                         *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   249
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   250
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   251
fun treeAppend tree1 tree2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   252
    case tree1 of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   253
      E => tree2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   254
    | T node1 =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   255
      case tree2 of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   256
        E => tree1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   257
      | T node2 =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   258
        if lowerPriorityNode node1 node2 then
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   259
          let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   260
            val Node {priority,left,key,value,right,...} = node2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   261
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   262
            val left = treeAppend tree1 left
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
            mkTree priority left key value right
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
        else
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   267
          let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   268
            val Node {priority,left,key,value,right,...} = node1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   269
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   270
            val right = treeAppend right tree2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   271
          in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   272
            mkTree priority left key value right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   273
          end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   274
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   275
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   276
(* Appending two trees and a node, where every element of the first tree is  *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   277
(* less than the node, which in turn is less than every element of the       *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   278
(* second tree.                                                              *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   279
(* ------------------------------------------------------------------------- *)
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 treeCombine left node right =
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
      val left_node = treeAppend left (T node)
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
      treeAppend left_node right
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
(* Searching a tree for a value.                                             *)
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 treePeek pkey tree =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   293
    case tree of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   294
      E => NONE
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   295
    | T node => nodePeek pkey node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   296
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   297
and nodePeek pkey node =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   298
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   299
      val Node {left,key,value,right,...} = node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   300
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   301
      case compareKey (pkey,key) of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   302
        LESS => treePeek pkey left
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   303
      | EQUAL => SOME value
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   304
      | GREATER => treePeek pkey right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   305
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   306
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   307
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   308
(* Tree paths.                                                               *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   309
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   310
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   311
(* Generating a path by searching a tree for a key/value pair *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   312
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   313
fun treePeekPath pkey path tree =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   314
    case tree of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   315
      E => (path,NONE)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   316
    | T node => nodePeekPath pkey path node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   317
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   318
and nodePeekPath pkey path node =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   319
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   320
      val Node {left,key,right,...} = node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   321
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   322
      case compareKey (pkey,key) of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   323
        LESS => treePeekPath pkey ((true,node) :: path) left
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   324
      | EQUAL => (path, SOME node)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   325
      | GREATER => treePeekPath pkey ((false,node) :: path) right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   326
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   327
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   328
(* A path splits a tree into left/right components *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   329
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   330
fun addSidePath ((wentLeft,node),(leftTree,rightTree)) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   331
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   332
      val Node {priority,left,key,value,right,...} = node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   333
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   334
      if wentLeft then (leftTree, mkTree priority rightTree key value right)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   335
      else (mkTree priority left key value leftTree, rightTree)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   336
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   337
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   338
fun addSidesPath left_right = List.foldl addSidePath left_right;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   339
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   340
fun mkSidesPath path = addSidesPath (E,E) path;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   341
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   342
(* Updating the subtree at a path *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   343
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   344
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   345
  fun updateTree ((wentLeft,node),tree) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   346
      let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   347
        val Node {priority,left,key,value,right,...} = node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   348
      in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   349
        if wentLeft then mkTree priority tree key value right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   350
        else mkTree priority left key value tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   351
      end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   352
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   353
  fun updateTreePath tree = List.foldl updateTree tree;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   354
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   355
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   356
(* Inserting a new node at a path position *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   357
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   358
fun insertNodePath node =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   359
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   360
      fun insert left_right path =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   361
          case path of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   362
            [] =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   363
            let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   364
              val (left,right) = left_right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   365
            in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   366
              treeCombine left node right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   367
            end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   368
          | (step as (_,snode)) :: rest =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   369
            if lowerPriorityNode snode node then
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   370
              let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   371
                val left_right = addSidePath (step,left_right)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   372
              in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   373
                insert left_right rest
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   374
              end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   375
            else
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   376
              let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   377
                val (left,right) = left_right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   378
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   379
                val tree = treeCombine left node right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   380
              in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   381
                updateTreePath tree path
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   382
              end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   383
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   384
      insert (E,E)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   385
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   386
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   387
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   388
(* Using a key to split a node into three components: the keys comparing     *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   389
(* less than the supplied key, an optional equal key, and the keys comparing *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   390
(* greater.                                                                  *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   391
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   392
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   393
fun nodePartition pkey node =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   394
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   395
      val (path,pnode) = nodePeekPath pkey [] node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   396
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   397
      case pnode of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   398
        NONE =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   399
        let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   400
          val (left,right) = mkSidesPath path
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   401
        in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   402
          (left,NONE,right)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   403
        end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   404
      | SOME node =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   405
        let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   406
          val Node {left,key,value,right,...} = node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   407
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   408
          val (left,right) = addSidesPath (left,right) path
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   409
        in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   410
          (left, SOME (key,value), right)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   411
        end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   412
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   413
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   414
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   415
(* Searching a tree for a key/value pair.                                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   416
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   417
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   418
fun treePeekKey pkey tree =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   419
    case tree of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   420
      E => NONE
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   421
    | T node => nodePeekKey pkey node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   422
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   423
and nodePeekKey pkey node =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   424
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   425
      val Node {left,key,value,right,...} = node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   426
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   427
      case compareKey (pkey,key) of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   428
        LESS => treePeekKey pkey left
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   429
      | EQUAL => SOME (key,value)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   430
      | GREATER => treePeekKey pkey right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   431
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   432
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   433
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   434
(* Inserting new key/values into the tree.                                   *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   435
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   436
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   437
fun treeInsert key_value tree =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   438
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   439
      val (key,value) = key_value
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   440
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   441
      val (path,inode) = treePeekPath key [] tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   442
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   443
      case inode of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   444
        NONE =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   445
        let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   446
          val node = nodeSingleton (key,value)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   447
        in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   448
          insertNodePath node path
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   449
        end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   450
      | SOME node =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   451
        let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   452
          val Node {size,priority,left,right,...} = node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   453
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   454
          val node =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   455
              Node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   456
                {size = size,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   457
                 priority = priority,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   458
                 left = left,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   459
                 key = key,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   460
                 value = value,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   461
                 right = right}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   462
        in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   463
          updateTreePath (T node) path
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   464
        end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   465
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   466
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   467
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   468
(* Deleting key/value pairs: it raises an exception if the supplied key is   *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   469
(* not present.                                                              *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   470
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   471
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   472
fun treeDelete dkey tree =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   473
    case tree of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   474
      E => raise Bug "KeyMap.delete: element not found"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   475
    | T node => nodeDelete dkey node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   476
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   477
and nodeDelete dkey node =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   478
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   479
      val Node {size,priority,left,key,value,right} = node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   480
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   481
      case compareKey (dkey,key) of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   482
        LESS =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   483
        let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   484
          val size = size - 1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   485
          and left = treeDelete dkey left
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   486
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   487
          val node =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   488
              Node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   489
                {size = size,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   490
                 priority = priority,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   491
                 left = left,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   492
                 key = key,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   493
                 value = value,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   494
                 right = right}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   495
        in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   496
          T node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   497
        end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   498
      | EQUAL => treeAppend left right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   499
      | GREATER =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   500
        let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   501
          val size = size - 1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   502
          and right = treeDelete dkey right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   503
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   504
          val node =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   505
              Node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   506
                {size = size,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   507
                 priority = priority,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   508
                 left = left,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   509
                 key = key,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   510
                 value = value,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   511
                 right = right}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   512
        in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   513
          T node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   514
        end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   515
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   516
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   517
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   518
(* Partial map is the basic operation for preserving tree structure.         *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   519
(* It applies its argument function to the elements *in order*.              *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   520
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   521
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   522
fun treeMapPartial f tree =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   523
    case tree of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   524
      E => E
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   525
    | T node => nodeMapPartial f node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   526
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   527
and nodeMapPartial f (Node {priority,left,key,value,right,...}) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   528
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   529
      val left = treeMapPartial f left
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   530
      and vo = f (key,value)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   531
      and right = treeMapPartial f right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   532
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   533
      case vo of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   534
        NONE => treeAppend left right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   535
      | SOME value => mkTree priority left key value right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   536
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   537
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   538
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   539
(* Mapping tree values.                                                      *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   540
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   541
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   542
fun treeMap f tree =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   543
    case tree of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   544
      E => E
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   545
    | T node => T (nodeMap f node)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   546
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   547
and nodeMap f node =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   548
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   549
      val Node {size,priority,left,key,value,right} = node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   550
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   551
      val left = treeMap f left
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   552
      and value = f (key,value)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   553
      and right = treeMap f right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   554
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   555
      Node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   556
        {size = size,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   557
         priority = priority,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   558
         left = left,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   559
         key = key,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   560
         value = value,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   561
         right = right}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   562
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   563
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   564
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   565
(* Merge is the basic operation for joining two trees. Note that the merged  *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   566
(* key is always the one from the second map.                                *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   567
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   568
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   569
fun treeMerge f1 f2 fb tree1 tree2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   570
    case tree1 of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   571
      E => treeMapPartial f2 tree2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   572
    | T node1 =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   573
      case tree2 of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   574
        E => treeMapPartial f1 tree1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   575
      | T node2 => nodeMerge f1 f2 fb node1 node2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   576
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   577
and nodeMerge f1 f2 fb node1 node2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   578
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   579
      val Node {priority,left,key,value,right,...} = node2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   580
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   581
      val (l,kvo,r) = nodePartition key node1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   582
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   583
      val left = treeMerge f1 f2 fb l left
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   584
      and right = treeMerge f1 f2 fb r right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   585
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   586
      val vo =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   587
          case kvo of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   588
            NONE => f2 (key,value)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   589
          | SOME kv => fb (kv,(key,value))
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   590
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   591
      case vo of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   592
        NONE => treeAppend left right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   593
      | SOME value =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   594
        let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   595
          val node = mkNodeSingleton priority key value
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   596
        in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   597
          treeCombine left node right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   598
        end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   599
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   600
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   601
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   602
(* A union operation on trees.                                               *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   603
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   604
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   605
fun treeUnion f f2 tree1 tree2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   606
    case tree1 of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   607
      E => tree2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   608
    | T node1 =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   609
      case tree2 of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   610
        E => tree1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   611
      | T node2 => nodeUnion f f2 node1 node2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   612
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   613
and nodeUnion f f2 node1 node2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   614
    if pointerEqual (node1,node2) then nodeMapPartial f2 node1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   615
    else
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   616
      let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   617
        val Node {priority,left,key,value,right,...} = node2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   618
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   619
        val (l,kvo,r) = nodePartition key node1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   620
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   621
        val left = treeUnion f f2 l left
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   622
        and right = treeUnion f f2 r right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   623
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   624
        val vo =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   625
            case kvo of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   626
              NONE => SOME value
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   627
            | SOME kv => f (kv,(key,value))
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   628
      in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   629
        case vo of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   630
          NONE => treeAppend left right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   631
        | SOME value =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   632
          let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   633
            val node = mkNodeSingleton priority key value
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   634
          in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   635
            treeCombine left node right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   636
          end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   637
      end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   638
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   639
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   640
(* An intersect operation on trees.                                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   641
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   642
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   643
fun treeIntersect f t1 t2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   644
    case t1 of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   645
      E => E
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   646
    | T n1 =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   647
      case t2 of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   648
        E => E
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   649
      | T n2 => nodeIntersect f n1 n2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   650
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   651
and nodeIntersect f n1 n2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   652
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   653
      val Node {priority,left,key,value,right,...} = n2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   654
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   655
      val (l,kvo,r) = nodePartition key n1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   656
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   657
      val left = treeIntersect f l left
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   658
      and right = treeIntersect f r right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   659
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   660
      val vo =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   661
          case kvo of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   662
            NONE => NONE
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   663
          | SOME kv => f (kv,(key,value))
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   664
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   665
      case vo of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   666
        NONE => treeAppend left right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   667
      | SOME value => mkTree priority left key value right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   668
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   669
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   670
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   671
(* A union operation on trees which simply chooses the second value.         *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   672
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   673
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   674
fun treeUnionDomain tree1 tree2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   675
    case tree1 of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   676
      E => tree2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   677
    | T node1 =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   678
      case tree2 of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   679
        E => tree1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   680
      | T node2 =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   681
        if pointerEqual (node1,node2) then tree2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   682
        else nodeUnionDomain node1 node2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   683
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   684
and nodeUnionDomain node1 node2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   685
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   686
      val Node {priority,left,key,value,right,...} = node2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   687
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   688
      val (l,_,r) = nodePartition key node1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   689
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   690
      val left = treeUnionDomain l left
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   691
      and right = treeUnionDomain r right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   692
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   693
      val node = mkNodeSingleton priority key value
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   694
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   695
      treeCombine left node right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   696
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   697
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   698
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   699
(* An intersect operation on trees which simply chooses the second value.    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   700
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   701
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   702
fun treeIntersectDomain tree1 tree2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   703
    case tree1 of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   704
      E => E
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   705
    | T node1 =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   706
      case tree2 of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   707
        E => E
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   708
      | T node2 =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   709
        if pointerEqual (node1,node2) then tree2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   710
        else nodeIntersectDomain node1 node2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   711
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   712
and nodeIntersectDomain node1 node2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   713
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   714
      val Node {priority,left,key,value,right,...} = node2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   715
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   716
      val (l,kvo,r) = nodePartition key node1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   717
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   718
      val left = treeIntersectDomain l left
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   719
      and right = treeIntersectDomain r right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   720
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   721
      if Option.isSome kvo then mkTree priority left key value right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   722
      else treeAppend left right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   723
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   724
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   725
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   726
(* A difference operation on trees.                                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   727
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   728
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   729
fun treeDifferenceDomain t1 t2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   730
    case t1 of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   731
      E => E
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   732
    | T n1 =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   733
      case t2 of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   734
        E => t1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   735
      | T n2 => nodeDifferenceDomain n1 n2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   736
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   737
and nodeDifferenceDomain n1 n2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   738
    if pointerEqual (n1,n2) then E
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   739
    else
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   740
      let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   741
        val Node {priority,left,key,value,right,...} = n1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   742
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   743
        val (l,kvo,r) = nodePartition key n2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   744
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   745
        val left = treeDifferenceDomain left l
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   746
        and right = treeDifferenceDomain right r
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   747
      in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   748
        if Option.isSome kvo then treeAppend left right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   749
        else mkTree priority left key value right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   750
      end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   751
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   752
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   753
(* A subset operation on trees.                                              *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   754
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   755
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   756
fun treeSubsetDomain tree1 tree2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   757
    case tree1 of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   758
      E => true
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   759
    | T node1 =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   760
      case tree2 of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   761
        E => false
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   762
      | T node2 => nodeSubsetDomain node1 node2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   763
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   764
and nodeSubsetDomain node1 node2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   765
    pointerEqual (node1,node2) orelse
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   766
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   767
      val Node {size,left,key,right,...} = node1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   768
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   769
      size <= nodeSize node2 andalso
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   770
      let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   771
        val (l,kvo,r) = nodePartition key node2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   772
      in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   773
        Option.isSome kvo andalso
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   774
        treeSubsetDomain left l andalso
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   775
        treeSubsetDomain right r
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   776
      end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   777
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   778
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   779
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   780
(* Picking an arbitrary key/value pair from a tree.                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   781
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   782
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   783
fun nodePick node =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   784
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   785
      val Node {key,value,...} = node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   786
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   787
      (key,value)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   788
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   789
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   790
fun treePick tree =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   791
    case tree of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   792
      E => raise Bug "KeyMap.treePick"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   793
    | T node => nodePick node;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   794
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   795
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   796
(* Removing an arbitrary key/value pair from a tree.                         *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   797
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   798
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   799
fun nodeDeletePick node =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   800
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   801
      val Node {left,key,value,right,...} = node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   802
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   803
      ((key,value), treeAppend left right)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   804
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   805
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   806
fun treeDeletePick tree =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   807
    case tree of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   808
      E => raise Bug "KeyMap.treeDeletePick"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   809
    | T node => nodeDeletePick node;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   810
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   811
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   812
(* Finding the nth smallest key/value (counting from 0).                     *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   813
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   814
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   815
fun treeNth n tree =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   816
    case tree of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   817
      E => raise Bug "KeyMap.treeNth"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   818
    | T node => nodeNth n node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   819
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   820
and nodeNth n node =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   821
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   822
      val Node {left,key,value,right,...} = node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   823
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   824
      val k = treeSize left
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   825
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   826
      if n = k then (key,value)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   827
      else if n < k then treeNth n left
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   828
      else treeNth (n - (k + 1)) right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   829
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   830
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   831
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   832
(* Removing the nth smallest key/value (counting from 0).                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   833
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   834
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   835
fun treeDeleteNth n tree =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   836
    case tree of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   837
      E => raise Bug "KeyMap.treeDeleteNth"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   838
    | T node => nodeDeleteNth n node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   839
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   840
and nodeDeleteNth n node =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   841
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   842
      val Node {size,priority,left,key,value,right} = node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   843
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   844
      val k = treeSize left
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   845
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   846
      if n = k then ((key,value), treeAppend left right)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   847
      else if n < k then
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   848
        let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   849
          val (key_value,left) = treeDeleteNth n left
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   850
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   851
          val size = size - 1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   852
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   853
          val node =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   854
              Node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   855
                {size = size,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   856
                 priority = priority,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   857
                 left = left,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   858
                 key = key,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   859
                 value = value,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   860
                 right = right}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   861
        in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   862
          (key_value, T node)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   863
        end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   864
      else
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   865
        let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   866
          val n = n - (k + 1)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   867
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   868
          val (key_value,right) = treeDeleteNth n right
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   869
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   870
          val size = size - 1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   871
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   872
          val node =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   873
              Node
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   874
                {size = size,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   875
                 priority = priority,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   876
                 left = left,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   877
                 key = key,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   878
                 value = value,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   879
                 right = right}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   880
        in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   881
          (key_value, T node)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   882
        end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   883
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   884
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   885
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   886
(* Iterators.                                                                *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   887
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   888
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   889
datatype 'value iterator =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   890
    LR of (key * 'value) * 'value tree * 'value node list
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   891
  | RL of (key * 'value) * 'value tree * 'value node list;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   892
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   893
fun fromSpineLR nodes =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   894
    case nodes of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   895
      [] => NONE
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   896
    | Node {key,value,right,...} :: nodes =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   897
      SOME (LR ((key,value),right,nodes));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   898
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   899
fun fromSpineRL nodes =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   900
    case nodes of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   901
      [] => NONE
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   902
    | Node {key,value,left,...} :: nodes =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   903
      SOME (RL ((key,value),left,nodes));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   904
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   905
fun addLR nodes tree = fromSpineLR (treeLeftSpine nodes tree);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   906
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   907
fun addRL nodes tree = fromSpineRL (treeRightSpine nodes tree);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   908
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   909
fun treeMkIterator tree = addLR [] tree;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   910
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   911
fun treeMkRevIterator tree = addRL [] tree;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   912
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   913
fun readIterator iter =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   914
    case iter of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   915
      LR (key_value,_,_) => key_value
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   916
    | RL (key_value,_,_) => key_value;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   917
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   918
fun advanceIterator iter =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   919
    case iter of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   920
      LR (_,tree,nodes) => addLR nodes tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   921
    | RL (_,tree,nodes) => addRL nodes tree;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   922
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   923
fun foldIterator f acc io =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   924
    case io of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   925
      NONE => acc
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   926
    | SOME iter =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   927
      let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   928
        val (key,value) = readIterator iter
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   929
      in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   930
        foldIterator f (f (key,value,acc)) (advanceIterator iter)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   931
      end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   932
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   933
fun findIterator pred io =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   934
    case io of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   935
      NONE => NONE
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   936
    | SOME iter =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   937
      let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   938
        val key_value = readIterator iter
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   939
      in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   940
        if pred key_value then SOME key_value
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   941
        else findIterator pred (advanceIterator iter)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   942
      end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   943
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   944
fun firstIterator f io =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   945
    case io of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   946
      NONE => NONE
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   947
    | SOME iter =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   948
      let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   949
        val key_value = readIterator iter
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   950
      in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   951
        case f key_value of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   952
          NONE => firstIterator f (advanceIterator iter)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   953
        | s => s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   954
      end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   955
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   956
fun compareIterator compareValue io1 io2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   957
    case (io1,io2) of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   958
      (NONE,NONE) => EQUAL
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   959
    | (NONE, SOME _) => LESS
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   960
    | (SOME _, NONE) => GREATER
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   961
    | (SOME i1, SOME i2) =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   962
      let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   963
        val (k1,v1) = readIterator i1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   964
        and (k2,v2) = readIterator i2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   965
      in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   966
        case compareKey (k1,k2) of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   967
          LESS => LESS
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   968
        | EQUAL =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   969
          (case compareValue (v1,v2) of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   970
             LESS => LESS
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   971
           | EQUAL =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   972
             let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   973
               val io1 = advanceIterator i1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   974
               and io2 = advanceIterator i2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   975
             in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   976
               compareIterator compareValue io1 io2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   977
             end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   978
           | GREATER => GREATER)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   979
        | GREATER => GREATER
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   980
      end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   981
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   982
fun equalIterator equalValue io1 io2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   983
    case (io1,io2) of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   984
      (NONE,NONE) => true
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   985
    | (NONE, SOME _) => false
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   986
    | (SOME _, NONE) => false
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   987
    | (SOME i1, SOME i2) =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   988
      let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   989
        val (k1,v1) = readIterator i1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   990
        and (k2,v2) = readIterator i2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   991
      in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   992
        equalKey k1 k2 andalso
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   993
        equalValue v1 v2 andalso
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   994
        let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   995
          val io1 = advanceIterator i1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   996
          and io2 = advanceIterator i2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   997
        in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   998
          equalIterator equalValue io1 io2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   999
        end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1000
      end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1001
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1002
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1003
(* A type of finite maps.                                                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1004
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1005
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1006
datatype 'value map =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1007
    Map of 'value tree;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1008
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1009
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1010
(* Map debugging functions.                                                  *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1011
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1012
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1013
(*BasicDebug
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1014
fun checkInvariants s m =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1015
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1016
      val Map tree = m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1017
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1018
      val _ = treeCheckInvariants tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1019
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1020
      m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1021
    end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1022
    handle Bug bug => raise Bug (s ^ "\n" ^ "KeyMap.checkInvariants: " ^ bug);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1023
*)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1024
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1025
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1026
(* Constructors.                                                             *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1027
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1028
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1029
fun new () =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1030
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1031
      val tree = treeNew ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1032
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1033
      Map tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1034
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1035
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1036
fun singleton key_value =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1037
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1038
      val tree = treeSingleton key_value
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1039
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1040
      Map tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1041
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1042
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1043
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1044
(* Map size.                                                                 *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1045
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1046
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1047
fun size (Map tree) = treeSize tree;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1048
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1049
fun null m = size m = 0;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1050
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1051
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1052
(* Querying.                                                                 *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1053
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1054
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1055
fun peekKey (Map tree) key = treePeekKey key tree;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1056
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1057
fun peek (Map tree) key = treePeek key tree;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1058
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1059
fun inDomain key m = Option.isSome (peek m key);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1060
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1061
fun get m key =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1062
    case peek m key of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1063
      NONE => raise Error "KeyMap.get: element not found"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1064
    | SOME value => value;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1065
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1066
fun pick (Map tree) = treePick tree;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1067
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1068
fun nth (Map tree) n = treeNth n tree;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1069
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1070
fun random m =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1071
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1072
      val n = size m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1073
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1074
      if n = 0 then raise Bug "KeyMap.random: empty"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1075
      else nth m (randomInt n)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1076
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1077
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1078
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1079
(* Adding.                                                                   *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1080
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1081
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1082
fun insert (Map tree) key_value =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1083
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1084
      val tree = treeInsert key_value tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1085
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1086
      Map tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1087
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1088
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1089
(*BasicDebug
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1090
val insert = fn m => fn kv =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1091
    checkInvariants "KeyMap.insert: result"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1092
      (insert (checkInvariants "KeyMap.insert: input" m) kv);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1093
*)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1094
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1095
fun insertList m =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1096
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1097
      fun ins (key_value,acc) = insert acc key_value
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1098
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1099
      List.foldl ins m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1100
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1101
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1102
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1103
(* Removing.                                                                 *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1104
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1105
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1106
fun delete (Map tree) dkey =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1107
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1108
      val tree = treeDelete dkey tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1109
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1110
      Map tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1111
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1112
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1113
(*BasicDebug
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1114
val delete = fn m => fn k =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1115
    checkInvariants "KeyMap.delete: result"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1116
      (delete (checkInvariants "KeyMap.delete: input" m) k);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1117
*)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1118
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1119
fun remove m key = if inDomain key m then delete m key else m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1120
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1121
fun deletePick (Map tree) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1122
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1123
      val (key_value,tree) = treeDeletePick tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1124
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1125
      (key_value, Map tree)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1126
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1127
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1128
(*BasicDebug
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1129
val deletePick = fn m =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1130
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1131
      val (kv,m) = deletePick (checkInvariants "KeyMap.deletePick: input" m)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1132
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1133
      (kv, checkInvariants "KeyMap.deletePick: result" m)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1134
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1135
*)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1136
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1137
fun deleteNth (Map tree) n =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1138
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1139
      val (key_value,tree) = treeDeleteNth n tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1140
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1141
      (key_value, Map tree)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1142
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1143
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1144
(*BasicDebug
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1145
val deleteNth = fn m => fn n =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1146
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1147
      val (kv,m) = deleteNth (checkInvariants "KeyMap.deleteNth: input" m) n
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1148
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1149
      (kv, checkInvariants "KeyMap.deleteNth: result" m)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1150
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1151
*)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1152
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1153
fun deleteRandom m =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1154
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1155
      val n = size m
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1156
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1157
      if n = 0 then raise Bug "KeyMap.deleteRandom: empty"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1158
      else deleteNth m (randomInt n)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1159
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1160
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1161
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1162
(* Joining (all join operations prefer keys in the second map).              *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1163
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1164
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1165
fun merge {first,second,both} (Map tree1) (Map tree2) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1166
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1167
      val tree = treeMerge first second both tree1 tree2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1168
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1169
      Map tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1170
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1171
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1172
(*BasicDebug
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1173
val merge = fn f => fn m1 => fn m2 =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1174
    checkInvariants "KeyMap.merge: result"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1175
      (merge f
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1176
         (checkInvariants "KeyMap.merge: input 1" m1)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1177
         (checkInvariants "KeyMap.merge: input 2" m2));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1178
*)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1179
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1180
fun union f (Map tree1) (Map tree2) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1181
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1182
      fun f2 kv = f (kv,kv)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1183
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1184
      val tree = treeUnion f f2 tree1 tree2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1185
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1186
      Map tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1187
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1188
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1189
(*BasicDebug
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1190
val union = fn f => fn m1 => fn m2 =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1191
    checkInvariants "KeyMap.union: result"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1192
      (union f
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1193
         (checkInvariants "KeyMap.union: input 1" m1)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1194
         (checkInvariants "KeyMap.union: input 2" m2));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1195
*)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1196
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1197
fun intersect f (Map tree1) (Map tree2) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1198
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1199
      val tree = treeIntersect f tree1 tree2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1200
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1201
      Map tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1202
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1203
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1204
(*BasicDebug
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1205
val intersect = fn f => fn m1 => fn m2 =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1206
    checkInvariants "KeyMap.intersect: result"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1207
      (intersect f
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1208
         (checkInvariants "KeyMap.intersect: input 1" m1)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1209
         (checkInvariants "KeyMap.intersect: input 2" m2));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1210
*)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1211
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1212
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1213
(* Iterators over maps.                                                      *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1214
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1215
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1216
fun mkIterator (Map tree) = treeMkIterator tree;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1217
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1218
fun mkRevIterator (Map tree) = treeMkRevIterator tree;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1219
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1220
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1221
(* Mapping and folding.                                                      *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1222
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1223
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1224
fun mapPartial f (Map tree) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1225
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1226
      val tree = treeMapPartial f tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1227
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1228
      Map tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1229
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1230
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1231
(*BasicDebug
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1232
val mapPartial = fn f => fn m =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1233
    checkInvariants "KeyMap.mapPartial: result"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1234
      (mapPartial f (checkInvariants "KeyMap.mapPartial: input" m));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1235
*)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1236
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1237
fun map f (Map tree) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1238
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1239
      val tree = treeMap f tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1240
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1241
      Map tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1242
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1243
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1244
(*BasicDebug
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1245
val map = fn f => fn m =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1246
    checkInvariants "KeyMap.map: result"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1247
      (map f (checkInvariants "KeyMap.map: input" m));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1248
*)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1249
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1250
fun transform f = map (fn (_,value) => f value);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1251
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1252
fun filter pred =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1253
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1254
      fun f (key_value as (_,value)) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1255
          if pred key_value then SOME value else NONE
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1256
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1257
      mapPartial f
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1258
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1259
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1260
fun partition p =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1261
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1262
      fun np x = not (p x)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1263
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1264
      fn m => (filter p m, filter np m)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1265
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1266
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1267
fun foldl f b m = foldIterator f b (mkIterator m);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1268
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1269
fun foldr f b m = foldIterator f b (mkRevIterator m);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1270
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1271
fun app f m = foldl (fn (key,value,()) => f (key,value)) () m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1272
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1273
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1274
(* Searching.                                                                *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1275
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1276
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1277
fun findl p m = findIterator p (mkIterator m);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1278
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1279
fun findr p m = findIterator p (mkRevIterator m);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1280
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1281
fun firstl f m = firstIterator f (mkIterator m);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1282
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1283
fun firstr f m = firstIterator f (mkRevIterator m);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1284
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1285
fun exists p m = Option.isSome (findl p m);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1286
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1287
fun all p =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1288
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1289
      fun np x = not (p x)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1290
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1291
      fn m => not (exists np m)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1292
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1293
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1294
fun count pred =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1295
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1296
      fun f (k,v,acc) = if pred (k,v) then acc + 1 else acc
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1297
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1298
      foldl f 0
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1299
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1300
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1301
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1302
(* Comparing.                                                                *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1303
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1304
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1305
fun compare compareValue (m1,m2) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1306
    if pointerEqual (m1,m2) then EQUAL
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1307
    else
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1308
      case Int.compare (size m1, size m2) of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1309
        LESS => LESS
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1310
      | EQUAL =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1311
        let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1312
          val Map _ = m1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1313
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1314
          val io1 = mkIterator m1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1315
          and io2 = mkIterator m2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1316
        in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1317
          compareIterator compareValue io1 io2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1318
        end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1319
      | GREATER => GREATER;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1320
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1321
fun equal equalValue m1 m2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1322
    pointerEqual (m1,m2) orelse
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1323
    (size m1 = size m2 andalso
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1324
     let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1325
       val Map _ = m1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1326
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1327
       val io1 = mkIterator m1
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1328
       and io2 = mkIterator m2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1329
     in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1330
       equalIterator equalValue io1 io2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1331
     end);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1332
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1333
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1334
(* Set operations on the domain.                                             *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1335
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1336
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1337
fun unionDomain (Map tree1) (Map tree2) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1338
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1339
      val tree = treeUnionDomain tree1 tree2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1340
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1341
      Map tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1342
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1343
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1344
(*BasicDebug
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1345
val unionDomain = fn m1 => fn m2 =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1346
    checkInvariants "KeyMap.unionDomain: result"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1347
      (unionDomain
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1348
         (checkInvariants "KeyMap.unionDomain: input 1" m1)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1349
         (checkInvariants "KeyMap.unionDomain: input 2" m2));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1350
*)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1351
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1352
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1353
  fun uncurriedUnionDomain (m,acc) = unionDomain acc m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1354
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1355
  fun unionListDomain ms =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1356
      case ms of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1357
        [] => raise Bug "KeyMap.unionListDomain: no sets"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1358
      | m :: ms => List.foldl uncurriedUnionDomain m ms;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1359
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1360
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1361
fun intersectDomain (Map tree1) (Map tree2) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1362
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1363
      val tree = treeIntersectDomain tree1 tree2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1364
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1365
      Map tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1366
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1367
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1368
(*BasicDebug
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1369
val intersectDomain = fn m1 => fn m2 =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1370
    checkInvariants "KeyMap.intersectDomain: result"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1371
      (intersectDomain
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1372
         (checkInvariants "KeyMap.intersectDomain: input 1" m1)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1373
         (checkInvariants "KeyMap.intersectDomain: input 2" m2));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1374
*)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1375
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1376
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1377
  fun uncurriedIntersectDomain (m,acc) = intersectDomain acc m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1378
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1379
  fun intersectListDomain ms =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1380
      case ms of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1381
        [] => raise Bug "KeyMap.intersectListDomain: no sets"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1382
      | m :: ms => List.foldl uncurriedIntersectDomain m ms;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1383
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1384
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1385
fun differenceDomain (Map tree1) (Map tree2) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1386
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1387
      val tree = treeDifferenceDomain tree1 tree2
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1388
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1389
      Map tree
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1390
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1391
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1392
(*BasicDebug
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1393
val differenceDomain = fn m1 => fn m2 =>
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1394
    checkInvariants "KeyMap.differenceDomain: result"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1395
      (differenceDomain
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1396
         (checkInvariants "KeyMap.differenceDomain: input 1" m1)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1397
         (checkInvariants "KeyMap.differenceDomain: input 2" m2));
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1398
*)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1399
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1400
fun symmetricDifferenceDomain m1 m2 =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1401
    unionDomain (differenceDomain m1 m2) (differenceDomain m2 m1);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1402
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1403
fun equalDomain m1 m2 = equal (K (K true)) m1 m2;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1404
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1405
fun subsetDomain (Map tree1) (Map tree2) =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1406
    treeSubsetDomain tree1 tree2;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1407
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1408
fun disjointDomain m1 m2 = null (intersectDomain m1 m2);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1409
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1410
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1411
(* Converting to and from lists.                                             *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1412
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1413
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1414
fun keys m = foldr (fn (key,_,l) => key :: l) [] m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1415
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1416
fun values m = foldr (fn (_,value,l) => value :: l) [] m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1417
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1418
fun toList m = foldr (fn (key,value,l) => (key,value) :: l) [] m;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1419
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1420
fun fromList l =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1421
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1422
      val m = new ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1423
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1424
      insertList m l
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1425
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1426
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1427
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1428
(* Pretty-printing.                                                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1429
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1430
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1431
fun toString m = "<" ^ (if null m then "" else Int.toString (size m)) ^ ">";
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1432
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1433
end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1434
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1435
structure IntMap =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1436
KeyMap (IntOrdered);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1437
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1438
structure IntPairMap =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1439
KeyMap (IntPairOrdered);
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1440
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1441
structure StringMap =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
  1442
KeyMap (StringOrdered);