src/Tools/Metis/src/Map.sig
author blanchet
Mon, 13 Sep 2010 21:11:59 +0200
changeset 39349 2d0a4361c3ef
parent 39348 6f9c9899f99f
child 39353 7f11d833d65b
permissions -rw-r--r--
change license, with Joe Hurd's permission
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     1
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     2
(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES                      *)
39349
2d0a4361c3ef change license, with Joe Hurd's permission
blanchet
parents: 39348
diff changeset
     3
(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License            *)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     4
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     5
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     6
signature Map =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     7
sig
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
(* A type of finite maps.                                                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    11
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    12
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    13
type ('key,'a) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    14
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    15
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    16
(* Constructors.                                                             *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    17
(* ------------------------------------------------------------------------- *)
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 new : ('key * 'key -> order) -> ('key,'a) map
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 singleton : ('key * 'key -> order) -> 'key * 'a -> ('key,'a) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    22
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    23
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    24
(* Map size.                                                                 *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    25
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    26
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    27
val null : ('key,'a) map -> bool
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    28
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    29
val size : ('key,'a) map -> int
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
(* Querying.                                                                 *)
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
val peekKey : ('key,'a) map -> 'key -> ('key * 'a) option
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 peek : ('key,'a) map -> 'key -> 'a option
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 get : ('key,'a) map -> 'key -> 'a  (* raises Error *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    40
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    41
val pick : ('key,'a) map -> 'key * 'a  (* an arbitrary key/value pair *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    42
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    43
val nth : ('key,'a) map -> int -> 'key * 'a  (* in the range [0,size-1] *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    44
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    45
val random : ('key,'a) map -> 'key * 'a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    46
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    47
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    48
(* Adding.                                                                   *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    49
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    50
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    51
val insert : ('key,'a) map -> 'key * 'a -> ('key,'a) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    52
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    53
val insertList : ('key,'a) map -> ('key * 'a) list -> ('key,'a) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    54
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    55
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    56
(* Removing.                                                                 *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    57
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    58
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    59
val delete : ('key,'a) map -> 'key -> ('key,'a) map  (* must be present *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    60
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    61
val remove : ('key,'a) map -> 'key -> ('key,'a) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    62
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    63
val deletePick : ('key,'a) map -> ('key * 'a) * ('key,'a) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    64
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    65
val deleteNth : ('key,'a) map -> int -> ('key * 'a) * ('key,'a) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    66
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    67
val deleteRandom : ('key,'a) map -> ('key * 'a) * ('key,'a) map
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
(* Joining (all join operations prefer keys in the second map).              *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    71
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    72
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    73
val merge :
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    74
    {first : 'key * 'a -> 'c option,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    75
     second : 'key * 'b -> 'c option,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    76
     both : ('key * 'a) * ('key * 'b) -> 'c option} ->
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    77
    ('key,'a) map -> ('key,'b) map -> ('key,'c) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    78
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    79
val union :
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    80
    (('key * 'a) * ('key * 'a) -> 'a option) ->
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    81
    ('key,'a) map -> ('key,'a) map -> ('key,'a) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    82
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    83
val intersect :
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    84
    (('key * 'a) * ('key * 'b) -> 'c option) ->
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    85
    ('key,'a) map -> ('key,'b) map -> ('key,'c) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    86
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    87
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    88
(* Set operations on the domain.                                             *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    89
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    90
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    91
val inDomain : 'key -> ('key,'a) map -> bool
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    92
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    93
val unionDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    94
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    95
val unionListDomain : ('key,'a) map list -> ('key,'a) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    96
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    97
val intersectDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    98
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    99
val intersectListDomain : ('key,'a) map list -> ('key,'a) map
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 differenceDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   102
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   103
val symmetricDifferenceDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   104
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   105
val equalDomain : ('key,'a) map -> ('key,'a) map -> bool
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   106
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   107
val subsetDomain : ('key,'a) map -> ('key,'a) map -> bool
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   108
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   109
val disjointDomain : ('key,'a) map -> ('key,'a) map -> bool
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   110
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   111
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   112
(* Mapping and folding.                                                      *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   113
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   114
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   115
val mapPartial : ('key * 'a -> 'b option) -> ('key,'a) map -> ('key,'b) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   116
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   117
val map : ('key * 'a -> 'b) -> ('key,'a) map -> ('key,'b) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   118
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   119
val app : ('key * 'a -> unit) -> ('key,'a) map -> unit
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   120
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   121
val transform : ('a -> 'b) -> ('key,'a) map -> ('key,'b) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   122
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   123
val filter : ('key * 'a -> bool) -> ('key,'a) map -> ('key,'a) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   124
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   125
val partition :
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   126
    ('key * 'a -> bool) -> ('key,'a) map -> ('key,'a) map * ('key,'a) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   127
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   128
val foldl : ('key * 'a * 's -> 's) -> 's -> ('key,'a) map -> 's
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   129
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   130
val foldr : ('key * 'a * 's -> 's) -> 's -> ('key,'a) map -> 's
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   131
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   132
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   133
(* Searching.                                                                *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   134
(* ------------------------------------------------------------------------- *)
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 findl : ('key * 'a -> bool) -> ('key,'a) map -> ('key * 'a) option
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   137
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   138
val findr : ('key * 'a -> bool) -> ('key,'a) map -> ('key * 'a) option
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   139
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   140
val firstl : ('key * 'a -> 'b option) -> ('key,'a) map -> 'b option
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   141
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   142
val firstr : ('key * 'a -> 'b option) -> ('key,'a) map -> 'b option
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   143
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   144
val exists : ('key * 'a -> bool) -> ('key,'a) map -> bool
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   145
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   146
val all : ('key * 'a -> bool) -> ('key,'a) map -> bool
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   147
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   148
val count : ('key * 'a -> bool) -> ('key,'a) map -> int
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   149
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   150
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   151
(* Comparing.                                                                *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   152
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   153
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   154
val compare : ('a * 'a -> order) -> ('key,'a) map * ('key,'a) map -> order
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   155
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   156
val equal : ('a -> 'a -> bool) -> ('key,'a) map -> ('key,'a) map -> bool
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   157
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   158
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   159
(* Converting to and from lists.                                             *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   160
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   161
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   162
val keys : ('key,'a) map -> 'key list
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   163
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   164
val values : ('key,'a) map -> 'a list
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   165
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   166
val toList : ('key,'a) map -> ('key * 'a) list
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   167
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   168
val fromList : ('key * 'key -> order) -> ('key * 'a) list -> ('key,'a) map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   169
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   170
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   171
(* Pretty-printing.                                                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   172
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   173
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   174
val toString : ('key,'a) map -> string
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   175
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   176
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   177
(* Iterators over maps.                                                      *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   178
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   179
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   180
type ('key,'a) iterator
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   181
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   182
val mkIterator : ('key,'a) map -> ('key,'a) iterator option
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   183
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   184
val mkRevIterator : ('key,'a) map -> ('key,'a) iterator option
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   185
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   186
val readIterator : ('key,'a) iterator -> 'key * 'a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   187
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   188
val advanceIterator : ('key,'a) iterator -> ('key,'a) iterator option
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   189
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   190
end