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