stdlib/fmap.mlw

   1
   2 (** {1 Finite Maps} *)
   3
   4 (** {2 Polymorphic maps to be used in spec/ghost only} *)
   5
   6 module Fmap
   7
   8   use int.Int
   9   use map.Map
  10   use set.Fset as S
  11
  12   type fmap 'k 'v = abstract {
  13     contents: 'k -> 'v;
  14       domain: S.fset 'k;
  15   }
  16   meta coercion function contents
  17
  18   predicate (==) (m1 m2: fmap 'k 'v) =
  19     S.(==) m1.domain m2.domain /\
  20     forall k. S.mem k m1.domain -> m1[k] = m2[k]
  21
  22   axiom extensionality:
  23     forall m1 m2: fmap 'k 'v. m1 == m2 -> m1 = m2
  24
  25   predicate mem (k: 'k) (m: fmap 'k 'v) =
  26     S.mem k m.domain
  27
  28   predicate mapsto (k: 'k) (v: 'v) (m: fmap 'k 'v) =
  29     mem k m /\ m[k] = v
  30
  31   lemma mem_mapsto:
  32     forall k: 'k, m: fmap 'k 'v. mem k m -> mapsto k m[k] m
  33
  34   predicate is_empty (m: fmap 'k 'v) =
  35     S.is_empty m.domain
  36
  37   function mk (d: S.fset 'k) (m: 'k -> 'v) : fmap 'k 'v
  38
  39   axiom mk_domain:
  40     forall d: S.fset 'k, m: 'k -> 'v. domain (mk d m) = d
  41
  42   axiom mk_contents:
  43     forall d: S.fset 'k, m: 'k -> 'v, k: 'k.
  44     S.mem k d -> (mk d m)[k] = m[k]
  45
  46   constant empty: fmap 'k 'v
  47
  48   axiom is_empty_empty: is_empty (empty: fmap 'k 'v)
  49
  50   function add (k: 'k) (v: 'v) (m: fmap 'k 'v) : fmap 'k 'v
  51
  52   function ([<-]) (m: fmap 'k 'v) (k: 'k) (v: 'v) : fmap 'k 'v =
  53     add k v m
  54
  55   (*FIXME? (add k v m).contents = m.contents[k <- v] *)
  56
  57   axiom add_contents_k:
  58     forall k v, m: fmap 'k 'v. (add k v m)[k] = v
  59
  60   axiom add_contents_other:
  61     forall k v, m: fmap 'k 'v, k1. mem k1 m -> k1 <> k -> (add k v m)[k1] = m[k1]
  62
  63   axiom add_domain:
  64     forall k v, m: fmap 'k 'v. (add k v m).domain = S.add k m.domain
  65
  66   (* FIXME? find_opt (k: 'k) (m: fmap 'k 'v) : option 'v *)
  67
  68   function find (k: 'k) (m: fmap 'k 'v) : 'v
  69
  70   axiom find_def:
  71     forall k, m: fmap 'k 'v. mem k m -> find k m = m[k]
  72
  73   function remove (k: 'k) (m: fmap 'k 'v) : fmap 'k 'v
  74
  75   axiom remove_contents:
  76     forall k, m: fmap 'k 'v, k1. mem k1 m -> k1 <> k -> (remove k m)[k1] = m[k1]
  77
  78   axiom remove_domain:
  79     forall k, m: fmap 'k 'v. (remove k m).domain = S.remove k m.domain
  80
  81   function size (m: fmap 'k 'v) : int =
  82     S.cardinal m.domain
  83
  84 end
  85
  86 (** {2 Finite monomorphic maps to be used in programs only}
  87
  88 A program function `eq` deciding equality on the `key` type must be provided when cloned.
  89 *)
  90
  91 (** {3 Applicative maps} *)
  92
  93 module MapApp
  94
  95   use int.Int
  96   use map.Map
  97   use export Fmap
  98
  99   type key
 100
 101   (* we enforce type `key` to have a decidable equality
 102      by requiring the following function *)
 103   val eq (x y: key) : bool
 104     ensures { result <-> x = y }
 105
 106   type t 'v = abstract {
 107     to_fmap: fmap key 'v;
 108   }
 109   meta coercion function to_fmap
 110
 111   val create () : t 'v
 112     ensures { result.to_fmap = empty }
 113
 114   val mem (k: key) (m: t 'v) : bool
 115     ensures { result <-> mem k m }
 116
 117   val is_empty (m: t 'v) : bool
 118     ensures { result <-> is_empty m }
 119
 120   val add (k: key) (v: 'v) (m: t 'v) : t 'v
 121     ensures { result = add k v m }
 122
 123   val find (k: key) (m: t 'v) : 'v
 124     requires { mem k m }
 125     ensures  { result = m[k] }
 126     ensures  { result = find k m }
 127
 128   use ocaml.Exceptions
 129
 130   val find_exn (k: key) (m: t 'v) : 'v
 131     ensures { S.mem k m.domain }
 132     ensures { result = m[k] }
 133     raises  { Not_found ->  not (S.mem k m.domain) }
 134
 135   val remove (k: key) (m: t 'v) : t 'v
 136     ensures { result = remove k m }
 137
 138   val size (m: t 'v) : int
 139     ensures { result = size m }
 140
 141 end
 142
 143 (** {3 Applicative maps of integers} *)
 144
 145 module MapAppInt
 146
 147   use int.Int
 148
 149   clone export MapApp with type key = int, val eq = Int.(=)
 150
 151 end
 152
 153 (** {3 Imperative maps} *)
 154
 155 module MapImp
 156
 157   use int.Int
 158   use map.Map
 159   use export Fmap
 160
 161   type key
 162
 163   val eq (x y: key) : bool
 164     ensures { result <-> x = y }
 165
 166   type t 'v = abstract {
 167     mutable to_fmap: fmap key 'v;
 168   }
 169   meta coercion function to_fmap
 170
 171   val create () : t 'v
 172     ensures { result.to_fmap = empty }
 173
 174   val mem (k: key) (m: t 'v) : bool
 175     ensures { result <-> mem k m }
 176
 177   val is_empty (m: t 'v) : bool
 178     ensures { result <-> is_empty m }
 179
 180   val add (k: key) (v: 'v) (m: t 'v) : unit
 181     writes  { m }
 182     ensures { m = add k v (old m) }
 183
 184   val find (k: key) (m: t 'v) : 'v
 185     requires { mem k m }
 186     ensures  { result = m[k] }
 187     ensures  { result = find k m }
 188
 189   use ocaml.Exceptions
 190
 191   val find_exn (k: key) (m: t 'v) : 'v
 192     ensures { S.mem k m.domain }
 193     ensures { result = m[k] }
 194     raises  { Not_found ->  not (S.mem k m.domain) }
 195
 196   val remove (k: key) (m: t 'v) : unit
 197     writes  { m }
 198     ensures { m = remove k (old m) }
 199
 200   val size (m: t 'v) : int
 201     ensures { result = size m }
 202
 203   val clear (m: t 'v) : unit
 204     writes  { m }
 205     ensures { m = empty }
 206
 207 end
 208
 209 (** {3 Imperative maps of integers} *)
 210
 211 module MapImpInt
 212
 213   use int.Int
 214
 215   clone export MapImp with type key = int, val eq = Int.(=)
 216
 217 end