tables.mlw 33.3 KB
Newer Older
1
2
3

(** {1 Implementation of logarithmic-time ordered associative tables on top
       of AVL trees}
4

5
6
7
    Author: Martin Clochard *)


8
(** {2 Shared base implementation between set and map structures} *)
9
module MapBase
10

11
12
13
14
  use import int.Int
  use import avl.SelectionTypes
  use import option.Option
  use import ref.Ref
15
16
  use import seq.Seq
  use mach.peano.Peano as I
17

18
  (** {3 Implementation parameters *)
19

20
  (** The level of balancing is left abstract. *)
21
  val constant balancing : I.t
22
    ensures { result > 0 }
23

24
  (** Stored elements are identified by totally ordered keys *)
25
  scope D type t 'a end scope K type t end
26
  clone export key_type.KeyType with type t = D.t, type key = K.t
27
  clone preorder.Computable as CO with type t = K.t, axiom .
28
  scope D
29
    let function measure 'a : unit = ()
30
  end
31

32
33
  (** As we do not need any extra information in order to perform search
      for this particular instance, we instantiate the monoid by unit. *)
34
  scope M
35
36
37
38
39
40
41
42
43
44
45
46
47
    type t = unit
    constant zero : unit = ()
    function op (x y:unit) : unit = ()
    let lemma neutral_ (x:unit) : unit
      ensures { op zero x = x = op x zero }
    = match x with _ -> () end
    clone export monoid.Monoid with type t = t,
      constant zero = zero,function op = op,lemma assoc,lemma neutral
    clone export monoid.MonoidSumDef with type M.t = t,
      constant M.zero = zero,function M.op = op,goal M.assoc,goal M.neutral
    let zero () : unit ensures { result = () } = ()
    let op (x y:unit) : unit ensures { result = () } = ()
  end
48

49
50
51
  (** In associative tables, elements are selected
      with respect to their keys. *)
  type selector = K.t
52

53
  (** Efficient search for ordered keys can be carried out efficiently
54
55
56
      only in strictly increasing sequences. *)
  predicate selection_possible (_:'b) (s:seq (D.t 'a)) =
    forall i j. 0 <= i < j < length s -> CO.lt s[i].key s[j].key
57

58
59
60
61
  predicate upper_bound_s (k:K.t) (s:seq (D.t 'a)) =
    forall i. 0 <= i < length s -> CO.lt s[i].key k
  predicate lower_bound_s (k:K.t) (s:seq (D.t 'a)) =
    forall i. 0 <= i < length s -> CO.lt k s[i].key
62

63
64
65
  (** Selected splits correspond to sorted sequence, in which:

      1) the left part precede the selector key
66

67
      2) the selector key precede the right part
68

69
      3) If it exists, the middle element has key equivalent to the selector *)
70
  predicate selected (k:K.t) (e:split (D.t 'a)) =
MARCHE Claude's avatar
MARCHE Claude committed
71
    let _s = rebuild e in
72
73
    upper_bound_s k e.left /\ lower_bound_s k e.right /\
    match e.middle with None -> true | Some d -> CO.eq k d.key end
74

75
  (** Comparison-based binary search *)
76
77
78
79
  let selected_part (ghost lseq rseq:seq (D.t 'a))
    (k:K.t) (l:'e) (d:D.t 'a) (r:'f) : part_base K.t
    requires { selection_possible k (lseq ++ cons d rseq) }
    returns { Here -> let e2 = { left = lseq;
80
        middle = Some d;
81
82
83
84
85
86
87
88
89
90
91
92
        right = rseq } in selected k e2
      | Left sl -> selection_possible sl lseq /\
        forall e. selected sl e /\ rebuild e = lseq ->
          selected k (right_extend e d rseq)
      | Right sr -> selection_possible sr rseq /\
        forall e. selected sr e /\ rebuild e = rseq ->
          selected k (left_extend lseq d e) }
  = let kd = d.key in
    let ghost s = (lseq ++ cons d rseq) in
    assert { forall i. 0 <= i < length rseq -> rseq[i] = s[i+length lseq+1] };
    assert { d = s[length lseq] };
    let cmp = CO.compare k kd in
93
    if cmp < 0
94
    then Left k
95
    else if cmp > 0
96
    then Right k
97
    else Here
98

99
100
101
102
103
104
  (** Full instantiation of the avl module. *)
  clone avl.AVL as Sel with type selector = selector,
    predicate selection_possible = selection_possible,
    predicate selected = selected,
    val selected_part = selected_part,
    goal selection_empty,
105
    val balancing = balancing,
106
107
108
109
110
111
112
    type D.t = D.t,
    val D.measure = D.measure,
    type M.t = M.t,
    constant M.zero = M.zero,
    function M.op = M.op,
    goal M.assoc,
    goal M.neutral,
113
114
115
116
    function M.agg = M.agg,
    goal M.agg_empty,
    goal M.agg_sing,
    goal M.agg_cat,
117
118
    val M.zero = M.zero,
    val M.op = M.op
119

120
  (** {3 Adaptation of the specification to associative tables} *)
121

122
123
  (** Extra invariant: sequence sorted *)
  type t 'a = { field : Sel.t 'a } invariant { selection_possible () field }
124
  by { field = Sel.empty () }
125

126
  type m 'a = {
127
128
    domn : K.t -> bool;
    func : K.t -> D.t 'a;
129
130
    card : int;
  }
131

132
133
134
135
136
137
138
  predicate domain (s:seq (D.t 'a)) (k:K.t) =
    exists i. 0 <= i < length s /\ CO.eq s[i].key k

  let ghost function make_func (s:seq (D.t 'a)) (k:K.t) : D.t 'a
    requires { selection_possible () s /\ domain s k }
    ensures { forall i. 0 <= i < length s /\ CO.eq s[i].key k -> result = s[i] }
  = let j = ref 0 in
139
    while not CO.eq s[!j].key k do
140
141
142
143
144
145
146
      invariant { 0 <= !j < length s }
      invariant { CO.le s[!j].key k }
      variant { length s - !j }
      j := !j + 1
    done;
    s[!j]

147
  function m (t:t 'a) : m 'a =
148
149
150
151
152
153
154
155
156
157
    { domn = fun y -> domain t.field y;
      func = fun y -> make_func t.field y;
      card = length t.field }
  meta coercion function m

  let lemma correction (t:t 'a)
    ensures { forall k1 k2. CO.eq k1 k2 -> t.domn k1 <-> t.domn k2 }
    ensures { forall k1 k2. CO.eq k1 k2 /\ t.domn k1 -> t.func k1 = t.func k2 }
    ensures { forall k. t.domn k -> CO.eq k (t.func k).key }
    ensures { t.card >= 0 }
158
  = ()
159

160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
  (* Link model and selection. *)
  let lemma selected_model (k0:K.t) (e:split (D.t 'a))
    requires { selection_possible k0 (rebuild e) }
    requires { selected k0 e }
    ensures {
      let s = rebuild e in
      match e.middle with
      | None -> forall k. CO.eq k k0 -> not domain s k
      | Some d -> forall k. CO.eq k k0 -> domain s k /\ make_func s k = d
        by s[length e.left] = d so CO.eq d.key k
      end
      /\ (forall k. CO.le k k0 -> not domain e.right k)
      /\ (forall k. CO.le k0 k -> not domain e.left k)
      /\ (forall k. CO.lt k0 k -> domain e.right k <-> domain s k)
      /\ (forall k. CO.lt k k0 -> domain e.left k <-> domain s k)
      /\ (forall k. CO.lt k0 k /\ domain e.right k ->
        make_func e.right k = make_func s k)
      /\ (forall k. CO.lt k k0 /\ domain e.left k ->
        make_func e.left k = make_func s k)
    }
  = ()

  (* Link selection and sortedness. *)
  let lemma selected_sorted (k0:K.t) (e:split (D.t 'a))
    requires { selected k0 e }
    ensures { selection_possible k0 (rebuild e) <->
      selection_possible k0 e.left /\ selection_possible k0 e.right }
187
  = ()
188

189
190
  (** Create an empty associative table. *)
  let empty () : t 'a
191
192
    ensures { result.card = 0 /\ forall k. not result.domn k }
  = { field = Sel.empty () }
193

194
195
  (** Create an associative table with a single element. *)
  let singleton (d:D.t 'a) : t 'a
196
197
198
199
    ensures { forall k. result.domn k <-> CO.eq k d.key }
    ensures { forall k. CO.eq k d.key -> result.func k = d }
    ensures { result.card = 1 }
  = { field = Sel.singleton d }
200

201
  (** Check emptyness of an associative table. *)
202
203
204
205
206
207
  let is_empty (ghost rk:ref K.t) (t:t 'a) : bool
    ensures { result -> forall k. not t.domn k }
    ensures { not result -> t.domn !rk }
    ensures { result <-> t.card = 0 }
  = let res = Sel.is_empty t.field in
    ghost if not res then rk := t.field.Sel.m.Sel.seq[0].key;
208
    res
209

210
211
212
213
214
215
216
217
218
219
220
221
  let min (t:t 'a) : D.t 'a
    requires { t.card > 0 }
    ensures  { t.domn result.key /\ t.func result.key = result }
    ensures  { forall k. t.domn k -> CO.le result.key k }
  = Sel.front t.field

  let max (t:t 'a) : D.t 'a
    requires { t.card > 0 }
    ensures  { t.domn result.key /\ t.func result.key = result }
    ensures  { forall k. t.domn k -> CO.le k result.key }
  = Sel.back t.field

222
223
  (** Get and extract the element with minimum key from the table. *)
  let decompose_min (t:t 'a) : option (D.t 'a,t 'a)
224
225
226
227
228
229
230
231
232
233
234
235
    returns { None -> t.card = 0 /\ forall k. not t.domn k
      | Some (d,r:t 'a) -> t.card = r.card + 1 /\
        t.domn d.key /\ t.func d.key = d /\ not r.domn d.key /\
        (forall k. CO.lt k d.key -> not t.domn k) /\
        (forall k. CO.eq k d.key -> t.func k = d) /\
        (forall k. CO.le k d.key -> not r.domn k) /\
        (forall k. CO.lt d.key k -> r.domn k <-> t.domn k) /\
        (forall k. CO.lt d.key k /\ r.domn k -> r.func k = t.func k) }
  = match Sel.decompose_front t.field with
    | None -> None
    | Some (d,r) -> Some (d,{ field = r })
    end
236

237
238
  (** Get and extract the element with maximum key from the table. *)
  let decompose_max (t:t 'a) : option (t 'a,D.t 'a)
239
240
241
242
243
244
245
246
247
248
249
250
    returns { None -> t.card = 0 /\ forall k. not t.domn k
      | Some (l:t 'a,d) -> t.card = l.card + 1 /\
        t.domn d.key /\ t.func d.key = d /\ not l.domn d.key /\
        (forall k. CO.lt d.key k -> not t.domn k) /\
        (forall k. CO.eq k d.key -> t.func k = d) /\
        (forall k. CO.le d.key k -> not l.domn k) /\
        (forall k. CO.lt k d.key -> l.domn k <-> t.domn k) /\
        (forall k. CO.lt k d.key /\ l.domn k -> l.func k = t.func k) }
  = match Sel.decompose_back t.field with
    | None -> None
    | Some (l,d) -> Some ({ field = l },d)
    end
251

252
253
  (** Optimized insertion of an element with minimum key. *)
  let add_min (d:D.t 'a) (t:t 'a) : t 'a
254
255
256
257
258
259
260
261
    requires { forall k. t.domn k -> CO.lt d.key k }
    ensures { result.card = t.card + 1 }
    ensures { forall k. CO.lt k d.key -> not result.domn k }
    ensures { forall k. CO.eq k d.key -> result.domn k /\ result.func k = d }
    ensures { forall k. CO.lt d.key k -> result.domn k <-> t.domn k }
    ensures { forall k. CO.lt d.key k /\ result.domn k ->
      result.func k = t.func k }
  = { field = Sel.cons d t.field }
262

263
264
  (** Optimized insertion of an element with maximal key. *)
  let add_max (t:t 'a) (d:D.t 'a) : t 'a
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
    requires { forall k. t.domn k -> CO.lt k d.key }
    ensures { result.card = t.card + 1 }
    ensures { forall k. CO.lt d.key k -> not result.domn k }
    ensures { forall k. CO.eq k d.key -> result.domn k /\ result.func k = d }
    ensures { forall k. CO.lt k d.key -> result.domn k <-> t.domn k }
    ensures { forall k. CO.lt k d.key /\ result.domn k ->
      result.func k = t.func k }
  = { field = Sel.snoc t.field d }

  (** Ordered union of two associative tables. *)
  let ordered_union (l r:t 'a) : t 'a
    requires { forall k1 k2. l.domn k1 /\ r.domn k2 -> CO.lt k1 k2 }
    ensures  { forall k. result.domn k <-> l.domn k \/ r.domn k }
    ensures  { forall k. result.domn k /\ l.domn k -> result.func k = l.func k }
    ensures  { forall k. result.domn k /\ r.domn k -> result.func k = r.func k }
    ensures  { result.card = l.card + r.card }
  = { field = Sel.concat l.field r.field }
282

283
284
  (** Get the value associated to a key in the table, if it exists. *)
  let get (k:K.t) (t:t 'a) : option (D.t 'a)
285
286
287
    returns { None -> not t.domn k
      | Some d -> t.card > 0 /\ CO.eq d.key k /\ t.domn k /\ t.func k = d }
  = Sel.get (Sel.default_split ()) k t.field
288

289
290
291
  (** Insert a value in the table. Erase binding if the key was
      already present. *)
  let insert (d:D.t 'a) (t:t 'a) : t 'a
292
293
294
295
296
297
298
299
300
301
302
303
304
    ensures { result.card = if t.domn d.key then t.card else t.card + 1 }
    ensures { forall k. CO.eq k d.key -> result.domn k /\ result.func k = d }
    ensures { result.domn d.key /\ result.func d.key = d }
    ensures { forall k. not CO.eq k d.key -> result.domn k <-> t.domn k }
    ensures { forall k. not CO.eq k d.key /\ result.domn k ->
      result.func k = t.func k }
  = let r0 = Sel.default_split () in
    let t2 = Sel.insert r0 d.key d t.field in
    selected_model d.key !r0;
    let r1 = { !r0 with middle = Some d } in
    assert { rebuild r1 = t2 };
    selected_model d.key r1;
    { field = t2 }
305

306
  (** Erase any binding associated to the given key. *)
307
308
309
310
311
312
313
314
  let remove (k0:K.t) (t:t 'a) : t 'a
    ensures { result.card = if t.domn k0 then t.card - 1 else t.card }
    ensures { forall k. CO.eq k k0 -> not result.domn k }
    ensures { not result.domn k0 }
    ensures { forall k. not CO.eq k k0 -> result.domn k <-> t.domn k }
    ensures { forall k. not CO.eq k k0 /\ result.domn k ->
      result.func k = t.func k }
  = { field = Sel.remove (Sel.default_split ()) k0 t.field }
315

316
317
318
  (** Split the table in three: elements before the key,
      element associated to the key (if exists),
      elements after the key. *)
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
  let split (k0:K.t) (t:t 'a) : (t 'a,option (D.t 'a),t 'a)
    returns { (lf:t 'a,o,rg:t 'a) ->
      (forall k. CO.lt k k0 -> lf.domn k <-> t.domn k) /\
      (forall k. CO.lt k k0 /\ lf.domn k -> lf.func k = t.func k) /\
      (forall k. CO.le k0 k -> not lf.domn k) /\
      (forall k. CO.lt k0 k -> rg.domn k <-> t.domn k) /\
      (forall k. CO.lt k0 k /\ rg.domn k -> rg.func k = t.func k) /\
      (forall k. CO.le k k0 -> not rg.domn k) /\
      match o with
      | None -> t.card = lf.card + rg.card /\
        (forall k. CO.eq k k0 -> not t.domn k) /\
        not t.domn k0
      | Some d -> t.card = lf.card + rg.card + 1 /\
        CO.eq d.key k0 /\
        (forall k. CO.eq k k0 -> t.domn k /\ t.func k = d)
        /\ t.domn k0 /\ t.func k0 = d
      end }
  = let lf,o,rg = Sel.split (Sel.default_split ()) k0 t.field in
    ({ field = lf }, o, { field = rg })
338

339
  (** {3 Extension with set-theoretic routines }
340

341
342
343
      Those routines go beyond single-call to the AVL trees function.
      Also, unlike previous routines they are not logarithmic-time but
      linear-time instead. *)
344

345
  (** Internal specification wrappers over the AVL view and join routines. *)
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
  type view 'a =
    | AEmpty
    | ANode (t 'a) (D.t 'a) (t 'a) I.t

  let view (t:t 'a) : view 'a
    returns { AEmpty -> t.card = 0 /\ forall k:K.t. not t.domn k
      | ANode l d r h ->
        t.card = 1 + l.card + r.card
        /\ h = t.field.Sel.hgt
        /\ let k0 = d.key in
           (forall k. CO.lt k k0 -> l.domn k <-> t.domn k)
        /\ (forall k. CO.lt k k0 /\ l.domn k -> l.func k = t.func k)
        /\ (forall k. CO.le k0 k -> not l.domn k)
        /\ (forall k. CO.lt k0 k -> r.domn k <-> t.domn k)
        /\ (forall k. CO.lt k0 k /\ r.domn k -> r.func k = t.func k)
        /\ (forall k. CO.le k k0 -> not r.domn k)
        /\ (forall k. CO.eq k k0 -> t.domn k /\ t.func k = d)
        /\ t.domn k0 /\ t.func k0 = d }
  = match Sel.view t.field with
    | Sel.AEmpty -> AEmpty
    | Sel.ANode l d r h _ -> ANode { field = l } d { field = r } h
    end
368

369
  let join (l:t 'a) (d:D.t 'a) (r:t 'a) : t 'a
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
    requires { forall k. l.domn k -> CO.lt k d.key }
    requires { forall k. r.domn k -> CO.lt d.key k }
    ensures { forall k. CO.lt k d.key -> result.domn k <-> l.domn k }
    ensures { forall k. CO.lt k d.key /\ result.domn k ->
      result.func k = l.func k }
    ensures { forall k. CO.lt d.key k -> result.domn k <-> r.domn k }
    ensures { forall k. CO.lt d.key k /\ result.domn k ->
      result.func k = r.func k }
    ensures { forall k. CO.eq k d.key -> result.domn k /\ result.func k = d }
    ensures { result.card = 1 + l.card + r.card }
  = let ghost s = { left = l.field.Sel.m.Sel.seq;
                    middle = Some d;
                    right = r.field.Sel.m.Sel.seq }
    in
    assert { selected d.key s };
    { field = Sel.join l.field d r.field }
386

387
  (** Add every element from `a` into `t`. *)
388
  let rec add_all (a:t 'a) (t:t 'a) : t 'a
389
390
391
392
393
    ensures { forall k. result.domn k <-> a.domn k \/ t.domn k }
    ensures { forall k. a.domn k -> result.func k = a.func k }
    ensures { forall k. t.domn k /\ not a.domn k -> result.func k = t.func k }
    ensures { result.card >= a.card /\ result.card >= t.card }
    ensures { result.card <= a.card + t.card }
394
395
    variant { a.m.card + t.m.card }
  = match view a with
396
397
398
399
400
    | AEmpty -> t
    | ANode al ad ar ah -> match view t with
      | AEmpty -> a
      | ANode tl td tr th -> if I.le ah th
        then let (al,ad,ar) = split td.key a in
401
402
403
404
405
406
407
          let ul = add_all al tl in
          let ur = add_all ar tr in
          let ud = match ad with
            | None -> td
            | Some ad -> ad
            end in
          join ul ud ur
408
        else let (tl,_,tr) = split ad.key t in
409
410
411
412
413
          let ul = add_all al tl in
          let ur = add_all ar tr in
          join ul ad ur
      end
    end
414

415
416
  (** Create the table with the elements of `a`
      whose key appear in `p`. *)
417
  let rec filter (p:t 'b) (a:t 'a) : t 'a
418
419
    ensures { forall k. result.domn k <-> a.domn k /\ p.domn k }
    ensures { forall k. result.domn k -> result.func k = a.func k }
420
421
422
    ensures { result.m.card <= a.m.card /\ result.m.card <= p.m.card }
    variant { a.m.card + p.m.card }
  = match view a with
423
424
425
426
427
    | AEmpty -> a
    | ANode al ad ar ah -> match view p with
      | AEmpty -> empty ()
      | ANode pl pd pr ph -> if I.le ah ph
        then let (al,ad,ar) = split pd.key a in
428
429
430
          let fl = filter pl al in
          let fr = filter pr ar in
          match ad with
431
          | None -> ordered_union fl fr
432
433
          | Some ad -> join fl ad fr
          end
434
        else let (pl,pd,pr) = split ad.key p in
435
436
437
          let fl = filter pl al in
          let fr = filter pr ar in
          match pd with
438
          | None -> ordered_union fl fr
439
440
441
442
          | _ -> join fl ad fr
          end
      end
    end
443

444
445
  (** Complement of `filter`: remove from `a` every element whose
      key appear in `p`. *)
446
  let rec remove_all (p:t 'b) (a:t 'a) : t 'a
447
448
449
    ensures { forall k. result.domn k <-> a.domn k /\ not p.domn k }
    ensures { forall k. result.domn k -> result.func k = a.func k }
    ensures { result.m.card <= a.m.card }
450
451
    variant { a.m.card + p.m.card }
  = match view a with
452
453
454
455
456
    | AEmpty -> a
    | ANode al ad ar ah -> match view p with
      | AEmpty -> a
      | ANode pl pd pr ph -> if I.le ah ph
        then let (al,_,ar) = split pd.key a in
457
458
          let fl = remove_all pl al in
          let fr = remove_all pr ar in
459
460
          ordered_union fl fr
        else let (pl,pd,pr) = split ad.key p in
461
462
463
464
          let fl = remove_all pl al in
          let fr = remove_all pr ar in
          match pd with
          | None -> join fl ad fr
465
          | _ -> ordered_union fl fr
466
467
468
          end
      end
    end
469

470
  (** Create a table with the elements that appear
471
      exactly in one of `a` and `b`, but not both. *)
472
  let rec symdiff (a b:t 'a) : t 'a
473
474
475
476
    ensures { forall k. result.domn k <-> not (a.domn k <-> b.domn k) }
    ensures { forall k. result.domn k /\ a.domn k -> result.func k = a.func k }
    ensures { forall k. result.domn k /\ b.domn k -> result.func k = b.func k }
    ensures { result.m.card <= a.m.card + b.m.card }
477
478
    variant { a.m.card + b.m.card }
  = match view a with
479
480
481
482
483
    | AEmpty -> b
    | ANode al ad ar ah -> match view b with
      | AEmpty -> a
      | ANode bl bd br bh -> if I.le ah bh
        then let (al,ad,ar) = split bd.key a in
484
485
486
487
          let sl = symdiff al bl in
          let sr = symdiff ar br in
          match ad with
          | None -> join sl bd sr
488
          | _ -> ordered_union sl sr
489
          end
490
        else let (bl,bd,br) = split ad.key b in
491
492
493
494
          let sl = symdiff al bl in
          let sr = symdiff ar br in
          match bd with
          | None -> join sl ad sr
495
          | _ -> ordered_union sl sr
496
497
498
          end
      end
    end
499

500
501
502
503
end

(** {2 Instantiation of the base to key-value ordered associative tables} *)
module Map
504

505
506
507
  use import int.Int
  use import option.Option
  use import ref.Ref
508
  use mach.peano.Peano as I
509

510
511
  val constant balancing : I.t
    ensures { result > 0 }
512

513
  (** Parameter: key type with computable total preorder. *)
514
  scope K type t end
515
  clone preorder.Computable as CO with type t = K.t, axiom .
516

517
  (** Elements are key-value pairs *)
518
  scope D
519
    type t 'a = (K.t,'a)
520
    let function key (t:t 'a) : K.t = let (a,_) = t in a
521
  end
522

523
524
(** Direct instantiation. *)
  clone MapBase as MB with val balancing = balancing,
525
526
    type K.t = K.t,
    type D.t = D.t,
527
    val key = D.key,
528
529
530
531
532
533
534
535
536
    predicate CO.le = CO.le,
    goal CO.Refl,
    goal CO.Trans,
    goal CO.Total,
    predicate CO.lt = CO.lt,
    goal CO.lt_def,
    predicate CO.eq = CO.eq,
    goal CO.eq_def,
    val CO.compare = CO.compare
537

538
539
  (** Slight adaptation of the logical model
      (get rid of keys in the output) *)
540
541
  type t 'a = MB.t 'a
  type m 'a = {
542
543
    domn : K.t -> bool;
    func : K.t -> 'a;
544
545
546
    card : int;
  }
  function m (t:t 'a) : m 'a =
547
548
    { domn = t.MB.domn;
      func = fun k -> let (_,v) = t.MB.func k in v;
549
      card = t.MB.m.MB.card }
550
  meta coercion function m
551

552
553
554
  let lemma correction (t:t 'a)
    ensures { forall k1 k2. CO.eq k1 k2 -> t.domn k1 <-> t.domn k2 }
    ensures { forall k1 k2. CO.eq k1 k2 /\ t.domn k1 -> t.func k1 = t.func k2 }
555
  = ()
556

557
  let empty () : t 'a
558
559
    ensures { forall k. not result.domn k }
    ensures { result.card = 0 }
560
  = MB.empty ()
561

562
  (** Create a table with a single key->value binding. *)
563
564
565
566
567
568
  let singleton (k0:K.t) (v:'a) : t 'a
    ensures { forall k. result.domn k <-> CO.eq k k0 }
    ensures { forall k. CO.eq k k0 -> result.func k = v }
    ensures { result.domn k0 /\ result.func k0 = v }
    ensures { result.card = 1 }
  = MB.singleton (k0,v)
569

570
  (** Check emptyness of a table. *)
571
572
573
  let is_empty (ghost rk:ref K.t) (t:t 'a) : bool
    ensures { result -> forall k. not t.domn k }
    ensures { not result -> t.domn !rk }
574
    ensures { result <-> t.m.card = 0 }
575
576
577
578
579
580
581
582
583
584
585
586
587
  = MB.is_empty rk t

  let min_binding (t:t 'a) : (K.t,'a)
    requires { t.card > 0 }
    returns  { (k,v) -> t.domn k /\ t.func k = v
      /\ forall k2. t.domn k2 -> CO.le k k2 }
  = MB.min t

  let max_binding (t:t 'a) : (K.t,'a)
    requires { t.card > 0 }
    returns  { (k,v) -> t.domn k /\ t.func k = v
      /\ forall k2. t.domn k2 -> CO.le k2 k }
  = MB.max t
588

589
590
  (** Get and extract the (key->value) binding with minimum key. *)
  let decompose_min (t:t 'a) : option ((K.t,'a),t 'a)
591
592
593
594
595
596
597
598
    returns { None -> t.card = 0 /\ forall k. not t.domn k
      | Some ((k0,v),r:t 'a) -> t.card = r.card + 1 /\
        t.domn k0 /\ t.func k0 = v /\ not r.domn k0 /\
        (forall k. CO.lt k k0 -> not t.domn k) /\
        (forall k. CO.eq k k0 -> t.func k = v) /\
        (forall k. CO.le k k0 -> not r.domn k) /\
        (forall k. CO.lt k0 k -> r.domn k <-> t.domn k) /\
        (forall k. CO.lt k0 k /\ r.domn k -> r.func k = t.func k) }
599
  = MB.decompose_min t
600

601
602
  (** Get and extract the (key->value) binding with maximum key. *)
  let decompose_max (t:t 'a) : option (t 'a,(K.t,'a))
603
604
605
606
607
608
609
610
    returns { None -> t.card = 0 /\ forall k. not t.domn k
      | Some (l:t 'a,(k0,v)) -> t.card = l.card + 1 /\
        t.domn k0 /\ t.func k0 = v /\ not l.domn k0 /\
        (forall k. CO.lt k0 k -> not t.domn k) /\
        (forall k. CO.eq k k0 -> t.func k = v) /\
        (forall k. CO.le k0 k -> not l.domn k) /\
        (forall k. CO.lt k k0 -> l.domn k <-> t.domn k) /\
        (forall k. CO.lt k k0 /\ l.domn k -> l.func k = t.func k) }
611
  = MB.decompose_max t
612

613
  (** Add a key->value binding with minimal key. *)
614
615
616
617
618
619
620
621
622
623
  let add_min_binding (k0:K.t) (v:'a) (t:t 'a) : t 'a
    requires { forall k. t.domn k -> CO.lt k0 k }
    ensures { result.card = t.card + 1 }
    ensures { forall k. CO.lt k k0 -> not result.domn k }
    ensures { forall k. CO.eq k k0 -> result.domn k /\ result.func k = v }
    ensures { forall k. CO.lt k0 k -> result.domn k <-> t.domn k }
    ensures { forall k. CO.lt k0 k /\ result.domn k ->
      result.func k = t.func k }
    ensures { result.domn k0 /\ result.func k0 = v }
  = MB.add_min (k0,v) t
624

625
  (** Add a key->value binding with maximal key. *)
626
627
628
629
630
631
632
633
634
635
  let add_max_binding (k0:K.t) (v:'a) (t:t 'a) : t 'a
    requires { forall k. t.domn k -> CO.lt k k0 }
    ensures { result.card = t.card + 1 }
    ensures { forall k. CO.lt k0 k -> not result.domn k }
    ensures { forall k. CO.eq k k0 -> result.domn k /\ result.func k = v }
    ensures { forall k. CO.lt k k0 -> result.domn k <-> t.domn k }
    ensures { forall k. CO.lt k k0 /\ result.domn k ->
      result.func k = t.func k }
    ensures { result.domn k0 /\ result.func k0 = v }
  = MB.add_max t (k0,v)
636

637
  (** Ordered fusion of two associative tables. *)
638
639
640
641
642
643
644
  let ordered_join (l r:t 'a) : t 'a
    requires { forall k1 k2. l.domn k1 /\ r.domn k2 -> CO.lt k1 k2 }
    ensures  { forall k. result.domn k <-> l.domn k \/ r.domn k }
    ensures  { forall k. result.domn k /\ l.domn k -> result.func k = l.func k }
    ensures  { forall k. result.domn k /\ r.domn k -> result.func k = r.func k }
    ensures  { result.card = l.card + r.card }
  = MB.ordered_union l r
645

646
647
  (** Extract the value associated to some key. *)
  let get (k:K.t) (t:t 'a) : option 'a
648
649
    returns { None -> not t.domn k
      | Some v -> t.card > 0 /\ t.domn k /\ t.func k = v }
650
651
652
653
  = match MB.get k t with
    | None -> None
    | Some (_,v) -> Some v
    end
654

655
  (** Set the binding for key `k`, erasing any such previous binding. *)
656
657
658
659
660
661
662
663
  let insert (k0:K.t) (v:'a) (t:t 'a) : t 'a
    ensures { result.card = if t.domn k0 then t.card else t.card + 1 }
    ensures { forall k. CO.eq k k0 -> result.domn k /\ result.func k = v }
    ensures { result.domn k0 /\ result.func k0 = v }
    ensures { forall k. not CO.eq k k0 -> result.domn k <-> t.domn k }
    ensures { forall k. not CO.eq k k0 /\ result.domn k ->
      result.func k = t.func k }
  = MB.insert (k0,v) t
664

665
  (** Erase any potential binding for key `k`. *)
666
667
668
669
670
671
672
673
  let remove (k0:K.t) (t:t 'a) : t 'a
    ensures { result.card = if t.domn k0 then t.card - 1 else t.card }
    ensures { forall k. CO.eq k k0 -> not result.domn k }
    ensures { not result.domn k0 }
    ensures { forall k. not CO.eq k k0 -> result.domn k <-> t.domn k }
    ensures { forall k. not CO.eq k k0 /\ result.domn k ->
      result.func k = t.func k }
  = MB.remove k0 t
674

675
  (** Split the table in three parts:
676
677
      Bindings with key lower than `k`, value associated to `k`,
      and bindings with key greater than `k`. *)
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
  let split (k0:K.t) (t:t 'a) : (t 'a,option 'a,t 'a)
    returns { (lf:t 'a,o,rg:t 'a) ->
      (forall k. CO.lt k k0 -> lf.domn k <-> t.domn k) /\
      (forall k. CO.lt k k0 /\ lf.domn k -> lf.func k = t.func k) /\
      (forall k. CO.le k0 k -> not lf.domn k) /\
      (forall k. CO.lt k0 k -> rg.domn k <-> t.domn k) /\
      (forall k. CO.lt k0 k /\ rg.domn k -> rg.func k = t.func k) /\
      (forall k. CO.le k k0 -> not rg.domn k) /\
      match o with
      | None -> t.card = lf.card + rg.card /\
        (forall k. CO.eq k k0 -> not t.domn k) /\
        not t.domn k0
      | Some v -> t.card = lf.card + rg.card + 1 /\
        (forall k. CO.eq k k0 -> t.domn k /\ t.func k = v)
        /\ t.domn k0 /\ t.func k0 = v
      end }
  = let (lf,o,rg) = MB.split k0 t in
    let o = match o with None -> None | Some (_,v) -> Some v end in
696
    (lf,o,rg)
697

698
699
700
701
end

(** {2 Instantiation of the base to ordered sets} *)
module Set
702

703
704
705
  use import int.Int
  use import option.Option
  use import ref.Ref
706
  use import mach.peano.Peano as I
707

708
  (** The balancing level is left abstract. *)
709
710
  val constant balancing : I.t
    ensures { result > 0 }
711

712
  (** Parameter: comparable elements. *)
713
  scope K type t end
714
  clone preorder.Computable as CO with type t = K.t, axiom .
715

716
  (** Elements are themselves the keys. *)
717
  scope D
718
    type t 'a = K.t
719
    let function key (x:'a) : 'a = x
720
  end
721

722
  (** Actual instantiation. *)
723
  clone MapBase as MB with val balancing = balancing,
724
725
    type K.t = K.t,
    type D.t = D.t,
726
    val key = D.key,
727
728
729
730
731
732
733
734
735
    predicate CO.le = CO.le,
    goal CO.Refl,
    goal CO.Trans,
    goal CO.Total,
    predicate CO.lt = CO.lt,
    goal CO.lt_def,
    predicate CO.eq = CO.eq,
    goal CO.eq_def,
    val CO.compare = CO.compare
736

737
738
739
740
  (** Minor adaptation of the logical model: only keep the set of elements.
      In fact, the functions from MapBase can been used as-is
      (but may be over-specifications)
      The following specifications wrappers are only given for demonstration. *)
741
  type t = MB.t unit
742
743
  function set (m:MB.m unit) : K.t -> bool = m.MB.domn
  function card (m:MB.m unit) : int = m.MB.card
744

745
746
  (** Invariant on the logical model. *)
  let lemma correction (t:t) : unit
747
748
    ensures { forall k1 k2:K.t. CO.eq k1 k2 -> t.set k1 <-> t.set k2 }
    ensures { t.card >= 0 }
749
  = ()
750

751
752
  (** Create an empty set. *)
  let empty () : t
753
754
    ensures { forall k. not result.set k }
    ensures { result.card = 0 }
755
  = MB.empty ()
756

757
  (** Create a singleton set. *)
758
759
760
761
762
  let singleton (k0:K.t) : t
    ensures { forall k. result.set k <-> CO.eq k k0 }
    ensures { result.set k0 }
    ensures { result.card = 1 }
  = MB.singleton k0
763

764
  (** Test emptyness of a set. *)
765
766
767
768
  let is_empty (ghost rk:ref K.t) (t:t) : bool
    ensures { result -> forall k. not t.set k }
    ensures { not result -> t.set !rk }
    ensures { result <-> t.card = 0 }
769
  = MB.is_empty rk t
770

771
772
773
774
775
776
777
778
779
780
781
782
783
784
  (** Minimum element of a set. *)
  let min_elt (t:t) : K.t
    requires { t.card > 0 }
    ensures  { t.set result }
    ensures  { forall k. t.set k -> CO.le result k }
  = MB.min t

  (** Maximum element of a set. *)
  let max_elt (t:t) : K.t
    requires { t.card > 0 }
    ensures  { t.set result }
    ensures  { forall k. t.set k -> CO.le k result }
  = MB.max t

785
786
  (** Get and remove minimum element from a set. *)
  let decompose_min (t:t) : option (K.t,t)
787
788
789
790
791
792
    returns { None -> t.card = 0 /\ forall k. not t.set k
      | Some (k0,r:t) -> t.card = r.card + 1 /\
        t.set k0 /\ not r.set k0 /\
        (forall k. CO.lt k k0 -> not t.set k) /\
        (forall k. CO.le k k0 -> not r.set k) /\
        (forall k. CO.lt k0 k -> r.set k <-> t.set k) }
793
  = MB.decompose_min t
794

795
796
  (** Get and remove maximum element from a set. *)
  let decompose_max (t:t) : option (t,K.t)
797
798
799
800
801
802
    returns { None -> t.card = 0 /\ forall k. not t.set k
      | Some (l:t,k0) -> t.card = l.card + 1 /\
        t.set k0 /\ not l.set k0 /\
        (forall k. CO.lt k0 k -> not t.set k) /\
        (forall k. CO.le k0 k -> not l.set k) /\
        (forall k. CO.lt k0 k -> l.set k <-> t.set k) }
803
  = MB.decompose_max t
804

805
  (** Add minimal element to a set. *)
806
807
808
809
810
811
  let add_min_elt (k0:K.t) (t:t) : t
    requires { forall k. t.set k -> CO.lt k0 k }
    ensures { result.card = t.card + 1 }
    ensures { forall k. CO.lt k k0 -> not result.set k }
    ensures { forall k. CO.lt k0 k -> result.set k <-> t.set k }
  = MB.add_min k0 t
812

813
  (** Add maximal element to a set. *)
814
815
816
817
818
819
  let add_max_elt (t:t) (k0:K.t) : t
    requires { forall k. t.set k -> CO.lt k k0 }
    ensures { result.card = t.card + 1 }
    ensures { forall k. CO.lt k0 k -> not result.set k }
    ensures { forall k. CO.lt k k0 -> result.set k <-> t.set k }
  = MB.add_max t k0
820

821
  (** Ordered union of two sets. *)
822
823
824
825
826
  let ordered_union (l r:t) : t
    requires { forall k1 k2. l.set k1 /\ r.set k2 -> CO.lt k1 k2 }
    ensures  { forall k. result.set k <-> l.set k \/ r.set k }
    ensures  { result.card = l.card + r.card }
  = MB.ordered_union l r
827

828
  (** Test membership of an element. *)
829
830
831
832
833
834
  let mem (k0:K.t) (t:t) : bool
    ensures { result <-> t.set k0 }
    ensures { result -> forall k. CO.eq k k0 -> t.set k }
    ensures { forall k. CO.eq k k0 /\ t.set k -> result }
    ensures { result -> t.card > 0 }
  = match MB.get k0 t with None -> false | _ -> true end
835

836
  (** Add an element to a set. *)
837
838
839
840
841
842
  let add (k0:K.t) (t:t) : t
    ensures { result.card = if t.set k0 then t.card else t.card + 1 }
    ensures { forall k. CO.eq k k0 -> result.set k }
    ensures { result.set k0 }
    ensures { forall k. not CO.eq k k0 -> result.set k <-> t.set k }
  = MB.insert k0 t
843

844
  (** Remove an element from a set. *)
845
846
847
848
849
850
  let remove (k0:K.t) (t:t) : t
    ensures { result.card = if t.set k0 then t.card - 1 else t.card }
    ensures { forall k. CO.eq k k0 -> not result.set k }
    ensures { not result.set k0 }
    ensures { forall k. not CO.eq k k0 -> result.set k <-> t.set k }
  = MB.remove k0 t
851

852
853
854
  (** Split the set into three parts: elements lower than `k`,
      elements equal to `k`,
      and elements bigger than `k` *)
855
856
857
858
859
860
861
862
863
864
865
866
867
868
  let split (k0:K.t) (t:t) : (t,bool,t)
    returns { (lf:t,b,rg:t) ->
      (forall k. CO.lt k k0 -> lf.set k <-> t.set k) /\
      (forall k. CO.le k0 k -> not lf.set k) /\
      (forall k. CO.lt k0 k -> rg.set k <-> t.set k) /\
      (forall k. CO.le k k0 -> not rg.set k) /\
      t.card = lf.card + rg.card + (if b then 1 else 0) /\
      (b <-> t.set k0) /\
      (b -> forall k. CO.eq k k0 -> t.set k) /\
      (forall k. CO.eq k k0 /\ t.set k -> b)
    }
  = let (lf,o,rg) = MB.split k0 t in
    let b = match o with None -> false | _ -> true end in
    (lf,b,rg)
869

870
  (** Extension: set-theoretic routines. *)
871

872
873
  (** Compute the union of two sets. *)
  let union (a b:t) : t
874
875
876
    ensures { forall k. result.set k <-> a.set k \/ b.set k }
    ensures { result.card >= a.card /\ result.card >= b.card }
    ensures { result.card <= a.card + b.card }
877
  = MB.add_all a b
878

879
880
  (** Compute the intersection of two sets. *)
  let inter (a b:t) : t
881
882
    ensures { forall k. result.set k <-> a.set k /\ b.set k }
    ensures { result.card <= a.card /\ result.card <= b.card }
883
  = MB.filter a b
884

885
886
  (** Compute the difference of two sets. *)
  let diff (a b:t) : t
887
888
    ensures { forall k. result.set k <-> a.set k /\ not b.set k }
    ensures { result.card <= a.card }
889
  = MB.remove_all b a
890

891
892
  (** Compute the symmetrical difference of two sets. *)
  let symdiff (a b:t) : t
893
894
    ensures { forall k. result.set k <-> not (a.set k <-> b.set k) }
    ensures { result.card <= a.card + b.card }
895
  = MB.symdiff a b
896

897
898
899
900
end

(** Example instances: integer keys/elements *)
module IMapAndSet
901

902
  use import int.Int
903
  use mach.peano.Peano as I
904

905
  scope K type t = int end
906

907
  let constant balancing : I.t = I.succ I.zero
908

909
910
911
  predicate le (x y:int) = x <= y
  predicate eq (x y:int) = x = y
  predicate lt (x y:int) = x < y
912

913
  let compare (x y:int) : int ensures { result = x - y } = x - y
914

915
  clone Map as M with val balancing = balancing,
916
917
918
919
920
921
922
923
924
925
    type K.t = K.t,
    predicate CO.le = le,
    predicate CO.lt = lt,
    predicate CO.eq = eq,
    goal CO.lt_def,
    goal CO.eq_def,
    goal CO.Refl,
    goal CO.Trans,
    goal CO.Total,
    val CO.compare = compare
926

927
  clone Set as S with val balancing = balancing,
928
929
930
931
932
933
934
935
936
937
    type K.t = K.t,
    predicate CO.le = le,
    predicate CO.lt = lt,
    predicate CO.eq = eq,
    goal CO.lt_def,
    goal CO.eq_def,
    goal CO.Refl,
    goal CO.Trans,
    goal CO.Total,
    val CO.compare = compare
938

939
940
end