src/Tools/Metis/src/KeyMap.sig
author wenzelm
Mon, 13 Apr 2020 22:08:14 +0200
changeset 71751 abf3e80bd815
parent 45778 df6e210fb44c
child 72004 913162a47d9f
permissions -rw-r--r--
tuned NEWS;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     1
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     2
(* FINITE MAPS WITH A FIXED KEY TYPE                                         *)
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
signature KeyMap =
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 map keys.                                                       *)
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
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    14
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 39502
diff changeset
    15
val compareKey : key * key -> order
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 39502
diff changeset
    16
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 39502
diff changeset
    17
val equalKey : key -> key -> bool
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 39502
diff changeset
    18
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    19
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    20
(* A type of finite maps.                                                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    21
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    22
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    23
type 'a map
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
(* Constructors.                                                             *)
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
val new : unit -> 'a map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    30
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    31
val singleton : key * 'a -> 'a map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    32
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    33
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    34
(* Map size.                                                                 *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    35
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    36
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    37
val null : 'a map -> bool
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 size : 'a map -> int
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
(* Querying.                                                                 *)
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
val peekKey : 'a map -> key -> (key * 'a) option
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    46
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    47
val peek : 'a map -> key -> 'a option
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    48
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    49
val get : 'a map -> key -> 'a  (* raises Error *)
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 pick : 'a map -> key * 'a  (* an arbitrary key/value pair *)
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 nth : 'a map -> int -> key * 'a  (* in the range [0,size-1] *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    54
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    55
val random : 'a map -> key * 'a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    56
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    57
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    58
(* Adding.                                                                   *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    59
(* ------------------------------------------------------------------------- *)
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 insert : 'a map -> key * 'a -> '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 insertList : 'a map -> (key * 'a) list -> '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
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    66
(* Removing.                                                                 *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    67
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    68
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    69
val delete : 'a map -> key -> 'a map  (* must be present *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    70
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    71
val remove : 'a map -> key -> 'a map
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 deletePick : 'a map -> (key * 'a) * 'a map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    74
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    75
val deleteNth : 'a map -> int -> (key * 'a) * 'a map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    76
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    77
val deleteRandom : 'a map -> (key * 'a) * 'a 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
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    80
(* Joining (all join operations prefer keys in the second map).              *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    81
(* ------------------------------------------------------------------------- *)
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 merge :
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    84
    {first : key * 'a -> 'c option,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    85
     second : key * 'b -> 'c option,
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    86
     both : (key * 'a) * (key * 'b) -> 'c option} ->
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    87
    'a map -> 'b map -> 'c map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    88
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    89
val union :
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    90
    ((key * 'a) * (key * 'a) -> 'a option) ->
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    91
    'a map -> 'a map -> 'a map
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 intersect :
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    94
    ((key * 'a) * (key * 'b) -> 'c option) ->
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    95
    'a map -> 'b map -> 'c 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
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    98
(* Set operations on the domain.                                             *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    99
(* ------------------------------------------------------------------------- *)
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 inDomain : key -> 'a map -> bool
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 unionDomain : 'a map -> 'a map -> '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 unionListDomain : 'a map list -> 'a map
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 intersectDomain : 'a map -> 'a map -> 'a map
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 intersectListDomain : 'a map list -> 'a map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   110
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   111
val differenceDomain : 'a map -> 'a map -> 'a map
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 symmetricDifferenceDomain : 'a map -> 'a map -> 'a map
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 equalDomain : 'a map -> 'a map -> bool
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 subsetDomain : 'a map -> 'a map -> bool
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 disjointDomain : 'a map -> 'a map -> bool
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   120
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   121
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   122
(* Mapping and folding.                                                      *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   123
(* ------------------------------------------------------------------------- *)
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 mapPartial : (key * 'a -> 'b option) -> 'a map -> 'b map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   126
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   127
val map : (key * 'a -> 'b) -> 'a map -> 'b map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   128
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   129
val app : (key * 'a -> unit) -> 'a map -> unit
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   130
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   131
val transform : ('a -> 'b) -> 'a map -> 'b map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   132
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   133
val filter : (key * 'a -> bool) -> 'a map -> 'a map
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   134
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   135
val partition :
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   136
    (key * 'a -> bool) -> 'a map -> 'a map * 'a map
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 foldl : (key * 'a * 's -> 's) -> 's -> 'a map -> 's
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 foldr : (key * 'a * 's -> 's) -> 's -> 'a map -> 's
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   141
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   142
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   143
(* Searching.                                                                *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   144
(* ------------------------------------------------------------------------- *)
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 findl : (key * 'a -> bool) -> 'a map -> (key * 'a) option
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 findr : (key * 'a -> bool) -> 'a map -> (key * 'a) option
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   149
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   150
val firstl : (key * 'a -> 'b option) -> 'a map -> 'b option
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   151
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   152
val firstr : (key * 'a -> 'b option) -> 'a map -> 'b option
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 exists : (key * 'a -> bool) -> 'a map -> bool
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 all : (key * 'a -> bool) -> '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
val count : (key * 'a -> bool) -> 'a map -> int
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   159
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   160
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   161
(* Comparing.                                                                *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   162
(* ------------------------------------------------------------------------- *)
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 compare : ('a * 'a -> order) -> 'a map * 'a map -> order
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 equal : ('a -> 'a -> bool) -> 'a map -> 'a map -> bool
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   167
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   168
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   169
(* Converting to and from lists.                                             *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   170
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   171
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   172
val keys : 'a map -> key list
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 values : 'a map -> 'a list
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   175
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   176
val toList : 'a map -> (key * 'a) list
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   177
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   178
val fromList : (key * 'a) list -> 'a map
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
(* Pretty-printing.                                                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   182
(* ------------------------------------------------------------------------- *)
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 toString : 'a map -> string
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   185
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   186
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   187
(* Iterators over maps.                                                      *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   188
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   189
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   190
type 'a iterator
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   191
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   192
val mkIterator : 'a map -> 'a iterator option
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   193
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   194
val mkRevIterator : 'a map -> 'a iterator option
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   195
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   196
val readIterator : 'a iterator -> key * 'a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   197
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   198
val advanceIterator : 'a iterator -> 'a iterator option
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   199
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   200
end