mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
1331 lines
53 KiB
Plaintext
1331 lines
53 KiB
Plaintext
|
|
module MapBase
|
|
|
|
use int.Int
|
|
use import avl.Base as B
|
|
use avl.SelectionTypes
|
|
use program_type.TypeParams
|
|
use option.Option
|
|
use ref.Ref
|
|
use list.List
|
|
use list.Append
|
|
use list.Mem
|
|
use list.Length
|
|
|
|
(* Move remaining parameters here. *)
|
|
constant balancing : int
|
|
axiom balancing_positive : balancing > 0
|
|
|
|
clone export key_type.ProgramKeyType
|
|
clone preorder.ComputableParam as CO with namespace T = K
|
|
|
|
(* Full clone of association_list. *)
|
|
clone association_list.AssocSorted as A with type K.t = D.m,
|
|
type K.key = K.m,
|
|
function K.key = key,
|
|
type O.order = CO.O.m,
|
|
predicate O.correct_for = CO.correct_for,
|
|
predicate O.le = CO.le,
|
|
goal O.refl,
|
|
goal O.trans,
|
|
predicate O.eq = CO.eq,
|
|
goal O.eq_def,
|
|
predicate O.lt = CO.lt,
|
|
goal O.lt_def
|
|
|
|
(* Selector: key with respect to an order. *)
|
|
type selector 'a 'b 'c 'd = { o : CO.O.t 'a 'b; k : K.t 'a 'b }
|
|
|
|
(* Correction of a selector with respect to an avl:
|
|
1) the selector key is correct with respect to the ordering,
|
|
2) The avl is sorted with respect to the ordering. *)
|
|
|
|
predicate selector_correct (p1:type_params 'a 'b) (p2:type_params 'c 'd)
|
|
(s:selector 'a 'b 'c 'd)
|
|
(t:B.t (D.t 'a 'b 'c 'd) (D.m 'b 'd)) =
|
|
let om = (CO.O.make_params p1).mdl s.o in
|
|
let km = (K.make_params p1).mdl s.k in
|
|
CO.correct_for om km /\ A.S.increasing om t.m.lis /\
|
|
(CO.O.make_params p1).inv s.o /\
|
|
(K.make_params p1).inv s.k
|
|
|
|
predicate selected (p1:type_params 'a 'b) (p2:type_params 'c 'd)
|
|
(s:selector 'a 'b 'c 'd) (e:position (D.m 'b 'd))
|
|
(t:B.t (D.t 'a 'b 'c 'd) (D.m 'b 'd)) =
|
|
let om = (CO.O.make_params p1).mdl s.o in
|
|
let km = (K.make_params p1).mdl s.k in
|
|
(A.S.majorate om km e.left /\ A.S.minorate om km e.right /\
|
|
A.S.increasing om e.left /\ A.S.increasing om e.right /\
|
|
match e.middle with
|
|
| None -> true
|
|
| Some d2 -> let k2 = key d2 in
|
|
CO.correct_for om k2 /\ CO.eq om km k2
|
|
end) /\
|
|
rebuild e = t.m.lis /\
|
|
selector_correct p1 p2 s t
|
|
predicate selected_sem (p1:type_params 'a 'b) (p2:type_params 'c 'd)
|
|
(s:selector 'a 'b 'c 'd) (e:position (D.m 'b 'd))
|
|
(t:B.t (D.t 'a 'b 'c 'd) (D.m 'b 'd)) =
|
|
let om = (CO.O.make_params p1).mdl s.o in
|
|
let km = (K.make_params p1).mdl s.k in
|
|
forall k:K.m 'b. CO.correct_for om k ->
|
|
(CO.lt om k km -> A.model om t.m.lis k = A.model om e.left k) /\
|
|
(CO.lt om km k -> A.model om t.m.lis k = A.model om e.right k) /\
|
|
(CO.eq om k km -> A.model om t.m.lis k = e.middle) /\
|
|
(CO.le om km k -> A.model om e.left k = None) /\
|
|
(CO.le om k km -> A.model om e.right k = None)
|
|
|
|
let lemma selected_sem (p1:type_params 'a 'b) (p2:type_params 'c 'd)
|
|
(s:selector 'a 'b 'c 'd) (e:position (D.m 'b 'd))
|
|
(t:B.t (D.t 'a 'b 'c 'd) (D.m 'b 'd)) : unit
|
|
requires { selected p1 p2 s e t }
|
|
ensures { selected_sem p1 p2 s e t }
|
|
= let om = p1.CO.O.make_params.mdl s.o in
|
|
let km = p1.K.make_params.mdl s.k in
|
|
match e.middle with
|
|
| None -> A.model_cut om km e.left e.right
|
|
| Some dm -> A.model_split om dm e.left e.right
|
|
end
|
|
|
|
let selected_way (ghost p1:type_params 'a 'b)
|
|
(ghost p2:type_params 'c 'd)
|
|
(s:selector 'a 'b 'c 'd)
|
|
(ghost base:B.t (D.t 'a 'b 'c 'd) (D.m 'b 'd))
|
|
(l:B.t (D.t 'a 'b 'c 'd) (D.m 'b 'd))
|
|
(d:D.t 'a 'b 'c 'd)
|
|
(r:B.t (D.t 'a 'b 'c 'd) (D.m 'b 'd)) : way_base (selector 'a 'b 'c 'd)
|
|
requires { exists b. c_balancing b l /\ c_balancing b r /\
|
|
c_balancing b base }
|
|
requires { l.prm = r.prm = base.prm /\ l.prm.inv d }
|
|
requires { l.prm = D.make_params p1 p2 }
|
|
requires { let l0 = node_model l.m.lis (l.prm.mdl d) r.m.lis in
|
|
base.m.lis = l0 /\ selector_correct p1 p2 s base }
|
|
returns { Here -> let e2 = { left = l.m.lis;
|
|
middle = Some (l.prm.mdl d);
|
|
right = r.m.lis } in selected p1 p2 s e2 base /\
|
|
rebuild e2 = node_model l.m.lis (l.prm.mdl d) r.m.lis
|
|
| Left sl -> selector_correct p1 p2 sl l /\
|
|
forall e. selected p1 p2 sl e l /\ rebuild e = l.m.lis ->
|
|
let e2 = { e with right = node_model e.right (l.prm.mdl d) r.m.lis }
|
|
in selected p1 p2 s e2 base /\ rebuild e2 = base.m.lis
|
|
| Right sr -> selector_correct p1 p2 sr r /\
|
|
forall e. selected p1 p2 sr e r /\ rebuild e = r.m.lis ->
|
|
let e2 = { e with left = node_model l.m.lis (l.prm.mdl d) e.left } in
|
|
selected p1 p2 s e2 base /\ rebuild e2 = base.m.lis }
|
|
= let kd = get_key p1 p2 d in
|
|
let cmp = CO.compare p1 s.o s.k kd in
|
|
if cmp < 0
|
|
then begin
|
|
assert { let mk = p1.K.make_params.mdl in
|
|
let om = p1.CO.O.make_params.mdl s.o in
|
|
(forall e. rebuild e = l.m.lis -> A.S.majorate om (mk kd) l.m.lis &&
|
|
A.S.majorate om (mk kd) e.right &&
|
|
A.S.increasing om (node_model e.right (l.prm.mdl d) r.m.lis)) };
|
|
Left s
|
|
end else if cmp > 0
|
|
then begin
|
|
assert { let mk = p1.K.make_params.mdl in
|
|
let om = p1.CO.O.make_params.mdl s.o in
|
|
(forall e. rebuild e = r.m.lis -> A.S.minorate om (mk kd) r.m.lis &&
|
|
A.S.minorate om (mk kd) e.left &&
|
|
A.S.increasing om (node_model l.m.lis (l.prm.mdl d) e.left)) };
|
|
Right s
|
|
end else Here
|
|
|
|
(* Full clone of the avl selection module. *)
|
|
clone avl.Selection as Sel with namespace D = D,
|
|
type selector = selector,
|
|
predicate selector_correct = selector_correct,
|
|
predicate selected = selected,
|
|
val selected_way = selected_way,
|
|
goal selector_correct_empty,
|
|
constant balancing = balancing,
|
|
goal balancing_positive
|
|
|
|
type t 'a 'b 'c 'd = {
|
|
repr : B.t (D.t 'a 'b 'c 'd) (D.m 'b 'd);
|
|
order : CO.O.t 'a 'b;
|
|
ghost prm1 : type_params 'a 'b;
|
|
ghost prm2 : type_params 'c 'd;
|
|
}
|
|
|
|
(* Model: a finite association with respect to an ordering parameter.
|
|
The cardinal expose the finite part, and is mainly intended for
|
|
user variants. *)
|
|
type m 'b 'd = {
|
|
func : K.m 'b -> option (D.m 'b 'd);
|
|
card : int;
|
|
ord : CO.O.m 'b;
|
|
}
|
|
|
|
function prm (t:t 'a 'b 'c 'd) : (type_params 'a 'b,type_params 'c 'd) =
|
|
(t.prm1,t.prm2)
|
|
function oprm (t:t 'a 'b 'c 'd) : type_params (CO.O.t 'a 'b) (CO.O.m 'b) =
|
|
t.prm1.CO.O.make_params
|
|
let ghost oprm (t:t 'a 'b 'c 'd) : type_params (CO.O.t 'a 'b) (CO.O.m 'b)
|
|
ensures { result = t.oprm }
|
|
= t.prm1.CO.O.make_params
|
|
function kprm (t:t 'a 'b 'c 'd) : type_params (K.t 'a 'b) (K.m 'b) =
|
|
t.prm1.K.make_params
|
|
let ghost kprm (t:t 'a 'b 'c 'd) : type_params (K.t 'a 'b) (K.m 'b)
|
|
ensures { result = t.kprm }
|
|
= t.prm1.K.make_params
|
|
function dprm (t:t 'a 'b 'c 'd) : type_params (D.t 'a 'b 'c 'd) (D.m 'b 'd) =
|
|
D.make_params t.prm1 t.prm2
|
|
let ghost dprm (t:t 'a 'b 'c 'd) : type_params (D.t 'a 'b 'c 'd) (D.m 'b 'd)
|
|
ensures { result = t.dprm }
|
|
= D.make_params t.prm1 t.prm2
|
|
|
|
function m (t:t 'a 'b 'c 'd) : m 'b 'd =
|
|
{ func = A.model (t.oprm.mdl t.order) t.repr.B.m.B.lis;
|
|
card = length t.repr.B.m.B.lis;
|
|
ord = t.oprm.mdl t.order }
|
|
let ghost m (t:t 'a 'b 'c 'd) : m 'b 'd
|
|
ensures { result = t.m }
|
|
= { func = A.model (t.prm1.CO.O.make_params.mdl t.order) t.repr.B.m.B.lis;
|
|
card = length t.repr.B.m.B.lis;
|
|
ord = t.prm1.CO.O.make_params.mdl t.order }
|
|
|
|
predicate c (t:t 'a 'b 'c 'd) =
|
|
Sel.c t.repr /\
|
|
t.repr.B.prm = t.dprm /\
|
|
A.S.increasing (t.oprm.mdl t.order) t.repr.B.m.B.lis /\
|
|
t.oprm.inv t.order
|
|
|
|
clone export program_type.Type2Prm with type t = t, type m = m,
|
|
function m = m,predicate c = c,function prm1 = prm1,function prm2 = prm2
|
|
|
|
(* Should be the exported part of the invariant. *)
|
|
let lemma correction (t:t 'a 'b 'c 'd) : unit
|
|
requires { c t }
|
|
ensures { forall k1 k2:K.m 'b. CO.correct_for t.m.ord k1 /\
|
|
CO.correct_for t.m.ord k2 /\ CO.eq t.m.ord k1 k2 ->
|
|
t.m.func k1 = t.m.func k2 }
|
|
ensures { forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
match t.m.func k with
|
|
| None -> true
|
|
| Some d -> CO.correct_for t.m.ord (key d) /\ CO.eq t.m.ord (key d) k
|
|
end }
|
|
ensures { t.m.card >= 0 }
|
|
= ()
|
|
|
|
let empty (ghost p1:type_params 'a 'b)
|
|
(ghost p2:type_params 'c 'd) (o:CO.O.t 'a 'b) : t 'a 'b 'c 'd
|
|
requires { p1.CO.O.make_params.inv o }
|
|
ensures { result.prm1 = p1 /\ result.prm2 = p2 }
|
|
ensures { c result }
|
|
ensures { p1.CO.O.make_params.mdl o = result.m.ord }
|
|
ensures { forall k:K.m 'b. CO.correct_for result.m.ord k ->
|
|
result.m.func k = None }
|
|
ensures { result.m.card = 0 }
|
|
= { repr = Sel.empty (D.make_params p1 p2); order = o; prm1 = p1; prm2 = p2 }
|
|
|
|
let singleton (ghost p1:type_params 'a 'b) (ghost p2:type_params 'c 'd)
|
|
(o:CO.O.t 'a 'b) (d:D.t 'a 'b 'c 'd) : t 'a 'b 'c 'd
|
|
requires { p1.CO.O.make_params.inv o }
|
|
requires { (D.make_params p1 p2).inv d }
|
|
requires { CO.correct_for (p1.CO.O.make_params.mdl o)
|
|
(key ((D.make_params p1 p2).mdl d)) }
|
|
ensures { result.prm1 = p1 /\ result.prm2 = p2 }
|
|
ensures { c result }
|
|
ensures { p1.CO.O.make_params.mdl o = result.m.ord }
|
|
ensures { forall k:K.m 'b. CO.correct_for result.m.ord k ->
|
|
if CO.eq result.m.ord k (key (result.dprm.mdl d))
|
|
then result.m.func k = Some (result.dprm.mdl d)
|
|
else result.m.func k = None }
|
|
ensures { result.m.card = 1 }
|
|
= let res = { repr = Sel.singleton (D.make_params p1 p2) d;
|
|
order = o;
|
|
prm1 = p1;
|
|
prm2 = p2 } in
|
|
res
|
|
|
|
let is_empty (ghost rd:ref (D.m 'b 'd)) (t:t 'a 'b 'c 'd) : bool
|
|
requires { c t }
|
|
ensures { result -> forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
t.m.func k = None }
|
|
ensures { not result -> CO.correct_for t.m.ord (key !rd) /\
|
|
t.m.func (key !rd) = Some !rd }
|
|
ensures { result <-> t.m.card = 0 }
|
|
= let res = Sel.is_empty t.repr in
|
|
ghost if not res
|
|
then match t.repr.B.m.B.lis with
|
|
| Nil -> absurd
|
|
| Cons d _ -> rd := d
|
|
end;
|
|
res
|
|
|
|
let param_copy (t:t 'a 'b 'c 'd)
|
|
(u:B.t (D.t 'a 'b 'c 'd) (D.m 'b 'd)) : t 'a 'b 'c 'd
|
|
ensures { result.repr = u }
|
|
ensures { result.order = t.order /\ result.m.ord = t.m.ord }
|
|
ensures { result.prm1 = t.prm1 }
|
|
ensures { result.prm2 = t.prm2 }
|
|
= { repr = u; order = t.order; prm1 = t.prm1; prm2 = t.prm2 }
|
|
|
|
let decompose_min (t:t 'a 'b 'c 'd) : option (D.t 'a 'b 'c 'd,t 'a 'b 'c 'd)
|
|
requires { c t }
|
|
returns { None -> (forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
t.m.func k = None) /\ t.m.card = 0
|
|
| Some (d,r) -> let dm = r.dprm.mdl d in
|
|
r.prm = t.prm /\ r.m.ord = t.m.ord /\ t.dprm.inv d /\
|
|
CO.correct_for t.m.ord dm.key /\
|
|
t.m.card = r.m.card + 1 /\
|
|
forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.lt t.m.ord k dm.key -> t.m.func k = None) /\
|
|
(CO.eq t.m.ord k dm.key -> t.m.func k = Some dm) /\
|
|
(CO.le r.m.ord k dm.key -> r.m.func k = None) /\
|
|
(not CO.eq r.m.ord dm.key k -> r.m.func k = t.m.func k) }
|
|
= match Sel.decompose_front t.repr with
|
|
| None -> None
|
|
| Some (d,r) -> let r = param_copy t r in
|
|
assert { let om = r.m.ord in let dm = r.dprm.mdl d in
|
|
let lt = t.repr.B.m.B.lis in let lr = r.repr.B.m.B.lis in
|
|
lt = (Cons dm Nil) ++ lr && A.S.minorate om dm.key lr &&
|
|
A.S.increasing om lr };
|
|
Some (d,r)
|
|
end
|
|
|
|
let decompose_max (t:t 'a 'b 'c 'd) : option (t 'a 'b 'c 'd,D.t 'a 'b 'c 'd)
|
|
requires { c t }
|
|
returns { None -> (forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
t.m.func k = None) /\ t.m.card = 0
|
|
| Some (l,d) -> let dm = l.dprm.mdl d in
|
|
l.prm = t.prm /\ l.m.ord = t.m.ord /\ t.dprm.inv d /\
|
|
CO.correct_for t.m.ord dm.key /\
|
|
t.m.card = l.m.card + 1 /\
|
|
forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.lt t.m.ord dm.key k -> t.m.func k = None) /\
|
|
(CO.eq t.m.ord dm.key k -> t.m.func k = Some dm) /\
|
|
(CO.le l.m.ord dm.key k -> l.m.func k = None) /\
|
|
(not CO.eq l.m.ord k dm.key -> l.m.func k = t.m.func k) }
|
|
= match Sel.decompose_back t.repr with
|
|
| None -> None
|
|
| Some (l,d) -> let l = param_copy t l in
|
|
assert { let om = l.m.ord in let dm = l.dprm.mdl d in
|
|
let lt = t.repr.B.m.B.lis in let ll = l.repr.B.m.B.lis in
|
|
lt = ll ++ (Cons dm Nil) && A.S.majorate om dm.key ll &&
|
|
A.S.increasing om ll };
|
|
Some (l,d)
|
|
end
|
|
|
|
let add_min (d:D.t 'a 'b 'c 'd) (t:t 'a 'b 'c 'd) : t 'a 'b 'c 'd
|
|
requires { c t /\ t.dprm.inv d }
|
|
requires { CO.correct_for t.m.ord (t.dprm.mdl d).key }
|
|
requires { forall k:K.m 'b. CO.correct_for t.m.ord k /\
|
|
CO.le t.m.ord k (t.dprm.mdl d).key -> t.m.func k = None }
|
|
ensures { c result /\ result.prm = t.prm /\ result.m.ord = t.m.ord }
|
|
ensures { let dm = t.dprm.mdl d in
|
|
forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.lt t.m.ord k dm.key -> result.m.func k = None) /\
|
|
(CO.eq t.m.ord k dm.key -> result.m.func k = Some dm) /\
|
|
(not CO.eq t.m.ord dm.key k -> result.m.func k = t.m.func k) }
|
|
ensures { result.m.card = t.m.card + 1 }
|
|
= let res = param_copy t (Sel.cons d t.repr) in
|
|
assert { let lt = t.repr.B.m.B.lis in
|
|
let lr = res.repr.B.m.B.lis in
|
|
let om = t.m.ord in let dm = t.dprm.mdl d in
|
|
lr = (Cons dm Nil) ++ lt && A.S.minorate om dm.key lt &&
|
|
A.S.increasing om lr };
|
|
res
|
|
|
|
let add_max (t:t 'a 'b 'c 'd) (d:D.t 'a 'b 'c 'd) : t 'a 'b 'c 'd
|
|
requires { c t /\ t.dprm.inv d }
|
|
requires { CO.correct_for t.m.ord (t.dprm.mdl d).key }
|
|
requires { forall k:K.m 'b. CO.correct_for t.m.ord k /\
|
|
CO.le t.m.ord (t.dprm.mdl d).key k -> t.m.func k = None }
|
|
ensures { c result /\ result.prm = t.prm /\ result.m.ord = t.m.ord }
|
|
ensures { let dm = t.dprm.mdl d in
|
|
forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.lt t.m.ord dm.key k -> result.m.func k = None) /\
|
|
(CO.eq t.m.ord k dm.key -> result.m.func k = Some dm) /\
|
|
(not CO.eq t.m.ord dm.key k -> result.m.func k = t.m.func k) }
|
|
ensures { result.m.card = t.m.card + 1 }
|
|
= let res = param_copy t (Sel.snoc t.repr d) in
|
|
assert { let lt = t.repr.B.m.B.lis in
|
|
let lr = res.repr.B.m.B.lis in
|
|
let om = t.m.ord in let dm = t.dprm.mdl d in
|
|
lr = lt ++ (Cons dm Nil) && A.S.majorate om dm.key lt &&
|
|
A.S.increasing om lr };
|
|
res
|
|
|
|
let concat (l r:t 'a 'b 'c 'd) : t 'a 'b 'c 'd
|
|
requires { c l /\ c r /\ l.prm = r.prm /\ l.m.ord = r.m.ord }
|
|
requires { forall k1 k2. CO.correct_for l.m.ord k1 /\
|
|
CO.correct_for r.m.ord k2 /\ l.m.func k1 <> None /\
|
|
r.m.func k2 <> None -> CO.lt l.m.ord k1 k2 }
|
|
ensures { c result /\ result.prm = l.prm /\ result.m.ord = l.m.ord }
|
|
ensures { forall k. CO.correct_for l.m.ord k ->
|
|
match l.m.func k with None -> result.m.func k = r.m.func k
|
|
| s -> result.m.func k = s end }
|
|
ensures { forall k. CO.correct_for l.m.ord k ->
|
|
match r.m.func k with None -> result.m.func k = l.m.func k
|
|
| s -> result.m.func k = s end }
|
|
ensures { forall k. CO.correct_for l.m.ord k -> (result.m.func k = None <->
|
|
l.m.func k = None /\ r.m.func k = None) }
|
|
ensures { result.m.card = l.m.card + r.m.card }
|
|
= let res = param_copy l (Sel.concat l.repr r.repr) in
|
|
assert { let ll = l.repr.B.m.B.lis in let lr = r.repr.B.m.B.lis in
|
|
let om = l.m.ord in
|
|
(not A.S.precede om ll lr -> (forall d1 d2. mem d1 ll /\ mem d2 lr ->
|
|
A.appear om d1.key ll && A.appear om d2.key lr) && false) &&
|
|
A.S.increasing om (ll++lr) && res.m.func = A.model om (ll++lr) };
|
|
res
|
|
|
|
let get (k:K.t 'a 'b) (t:t 'a 'b 'c 'd) : option (D.t 'a 'b 'c 'd)
|
|
requires { c t /\ t.kprm.inv k }
|
|
requires { CO.correct_for t.m.ord (t.kprm.mdl k) }
|
|
returns { None -> let km = t.kprm.mdl k in
|
|
(forall k2. CO.correct_for t.m.ord k2 /\ CO.eq t.m.ord km k2 ->
|
|
t.m.func k2 = None) && t.m.func km = None
|
|
| Some d -> t.dprm.inv d /\ t.m.card > 0 /\ let km = t.kprm.mdl k in
|
|
let dm = t.dprm.mdl d in
|
|
CO.correct_for t.m.ord dm.key /\ CO.eq t.m.ord dm.key km /\
|
|
(forall k2. CO.correct_for t.m.ord k2 /\ CO.eq t.m.ord km k2 ->
|
|
t.m.func k2 = Some dm) && t.m.func km = Some dm = t.m.func dm.key }
|
|
= let r = Sel.default_position () in
|
|
let s = { o = t.order; k = k } in
|
|
let res = Sel.get t.prm1 t.prm2 r s t.repr in
|
|
res
|
|
|
|
let add (d:D.t 'a 'b 'c 'd) (t:t 'a 'b 'c 'd) : t 'a 'b 'c 'd
|
|
requires { c t /\ t.dprm.inv d }
|
|
requires { CO.correct_for t.m.ord (t.dprm.mdl d).key }
|
|
ensures { c result /\ result.prm = t.prm /\ result.m.ord = t.m.ord }
|
|
ensures { let dm = t.dprm.mdl d in
|
|
t.m.card <= result.m.card /\
|
|
(if t.m.func dm.key = None then result.m.card = t.m.card + 1
|
|
else result.m.card = t.m.card) /\
|
|
(forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.eq t.m.ord k dm.key -> result.m.func k = Some dm) /\
|
|
(not CO.eq t.m.ord k dm.key -> result.m.func k = t.m.func k)) &&
|
|
result.m.func dm.key = Some dm }
|
|
= let r = Sel.default_position () in
|
|
let s = { o = t.order; k = get_key t.prm1 t.prm2 d } in
|
|
let res = param_copy t (Sel.add t.prm1 t.prm2 r s d t.repr) in
|
|
let r2 = { !r with middle = Some (t.dprm.mdl d) } in
|
|
assert { selected t.prm1 t.prm2 s r2 res.repr &&
|
|
selected_sem t.prm1 t.prm2 s r2 res.repr &&
|
|
selected_sem t.prm1 t.prm2 s !r t.repr };
|
|
res
|
|
|
|
let remove (k:K.t 'a 'b) (t:t 'a 'b 'c 'd) : t 'a 'b 'c 'd
|
|
requires { c t /\ t.kprm.inv k }
|
|
requires { CO.correct_for t.m.ord (t.kprm.mdl k) }
|
|
ensures { c result /\ result.prm = t.prm /\ result.m.ord = t.m.ord }
|
|
ensures { let km = t.kprm.mdl k in
|
|
result.m.card <= t.m.card /\
|
|
(if t.m.func km = None then t.m.card = result.m.card
|
|
else t.m.card = result.m.card + 1) /\
|
|
(forall k2:K.m 'b. CO.correct_for t.m.ord k2 ->
|
|
(CO.eq t.m.ord k2 km -> result.m.func k2 = None) /\
|
|
(not CO.eq t.m.ord k2 km -> result.m.func k2 = t.m.func k2)) &&
|
|
result.m.func km = None }
|
|
= let r = Sel.default_position () in
|
|
let s = { o = t.order; k = k } in
|
|
let res = param_copy t (Sel.remove t.prm1 t.prm2 r s t.repr) in
|
|
let r2 = { !r with middle = None } in
|
|
assert { selected t.prm1 t.prm2 s r2 res.repr &&
|
|
selected_sem t.prm1 t.prm2 s r2 res.repr &&
|
|
selected_sem t.prm1 t.prm2 s !r t.repr };
|
|
res
|
|
|
|
let split (k:K.t 'a 'b) (t:t 'a 'b 'c 'd) :
|
|
(t 'a 'b 'c 'd,option (D.t 'a 'b 'c 'd),t 'a 'b 'c 'd)
|
|
requires { c t /\ t.kprm.inv k }
|
|
requires { CO.correct_for t.m.ord (t.kprm.mdl k) }
|
|
returns { (lf,o,rg) ->
|
|
lf.prm = t.prm = rg.prm /\ lf.m.ord = t.m.ord = rg.m.ord /\
|
|
c lf /\ c rg /\
|
|
let om = t.m.ord in
|
|
let km = t.kprm.mdl k in
|
|
match o with
|
|
| None -> (forall k2:K.m 'b. CO.correct_for om k2 /\ CO.eq om km k2 ->
|
|
t.m.func k2 = None) && t.m.func km = None
|
|
| Some d -> t.dprm.inv d /\ let dm = t.dprm.mdl d in
|
|
CO.correct_for om dm.key /\ CO.eq om km dm.key /\
|
|
(forall k2:K.m 'b. CO.correct_for om k2 /\ CO.eq om km k2 ->
|
|
t.m.func k2 = Some dm) && t.m.func km = Some dm = t.m.func dm.key
|
|
end /\
|
|
((if o = None
|
|
then t.m.card = lf.m.card + rg.m.card
|
|
else t.m.card = 1 + (lf.m.card + rg.m.card)) &&
|
|
t.m.card >= lf.m.card + rg.m.card) /\
|
|
(forall k2:K.m 'b. CO.correct_for om k2 /\ CO.lt om k2 km ->
|
|
lf.m.func k2 = t.m.func k2) /\
|
|
(forall k2:K.m 'b. CO.correct_for om k2 /\ CO.le om km k2 ->
|
|
lf.m.func k2 = None) /\
|
|
(forall k2:K.m 'b. CO.correct_for om k2 /\ CO.lt om km k2 ->
|
|
rg.m.func k2 = t.m.func k2) /\
|
|
(forall k2:K.m 'b. CO.correct_for om k2 /\ CO.le om k2 km ->
|
|
rg.m.func k2 = None) }
|
|
= let r = Sel.default_position () in
|
|
let s = { o = t.order; k = k } in
|
|
let (lf0,o,rg0) = Sel.split t.prm1 t.prm2 r s t.repr in
|
|
let lf = param_copy t lf0 in let rg = param_copy t rg0 in
|
|
assert { selected_sem t.prm1 t.prm2 s !r t.repr };
|
|
(lf,o,rg)
|
|
|
|
(* Internal, but makes set-theoretic routines easier. *)
|
|
type view 'a 'b 'c 'd =
|
|
| VEmpty
|
|
| VNode (t 'a 'b 'c 'd) (D.t 'a 'b 'c 'd) (t 'a 'b 'c 'd) int
|
|
|
|
let view (t:t 'a 'b 'c 'd) : view 'a 'b 'c 'd
|
|
requires { c t }
|
|
returns { VEmpty -> t.m.card = 0 /\
|
|
forall k:K.m 'b. CO.correct_for t.m.ord k -> t.m.func k = None
|
|
| VNode l d r _ -> let dm = t.dprm.mdl d in
|
|
c l /\ c r /\ t.dprm.inv d /\ CO.correct_for t.m.ord dm.key /\
|
|
l.prm = t.prm = r.prm /\ l.m.ord = t.m.ord = r.m.ord /\
|
|
t.m.card = 1 + l.m.card + r.m.card /\
|
|
forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.lt t.m.ord k dm.key -> t.m.func k = l.m.func k) /\
|
|
(CO.lt t.m.ord dm.key k -> t.m.func k = r.m.func k) /\
|
|
(CO.eq t.m.ord k dm.key -> t.m.func k = Some dm) /\
|
|
(CO.le t.m.ord dm.key k -> l.m.func k = None) /\
|
|
(CO.le t.m.ord k dm.key -> r.m.func k = None) }
|
|
= match Sel.view t.repr with
|
|
| Sel.AEmpty -> VEmpty
|
|
| Sel.ANode l d r h ->
|
|
A.model_split t.m.ord (t.dprm.mdl d) l.B.m.B.lis r.B.m.B.lis;
|
|
assert { t.repr.B.m.B.lis =
|
|
node_model l.B.m.B.lis (t.dprm.mdl d) r.B.m.B.lis };
|
|
VNode (param_copy t l) d (param_copy t r) h
|
|
end
|
|
|
|
let join (l:t 'a 'b 'c 'd)
|
|
(d:D.t 'a 'b 'c 'd)
|
|
(r:t 'a 'b 'c 'd) : t 'a 'b 'c 'd
|
|
requires { c l /\ c r /\ l.prm = r.prm /\ l.m.ord = r.m.ord }
|
|
requires { l.dprm.inv d /\ CO.correct_for l.m.ord (l.dprm.mdl d).key }
|
|
requires { let dm = l.dprm.mdl d in
|
|
forall k:K.m 'b. CO.correct_for l.m.ord k ->
|
|
(l.m.func k <> None -> CO.lt l.m.ord k dm.key) /\
|
|
(r.m.func k <> None -> CO.lt l.m.ord dm.key k) }
|
|
ensures { c result /\ result.prm = l.prm /\ result.m.ord = r.m.ord }
|
|
ensures { let dm = l.dprm.mdl d in
|
|
forall k:K.m 'b. CO.correct_for l.m.ord k ->
|
|
(CO.lt l.m.ord k dm.key -> result.m.func k = l.m.func k) /\
|
|
(CO.lt l.m.ord dm.key k -> result.m.func k = r.m.func k) /\
|
|
(CO.eq l.m.ord k dm.key -> result.m.func k = Some dm) }
|
|
ensures { result.m.card = 1 + l.m.card + r.m.card }
|
|
= let res = param_copy l (Sel.join l.repr d r.repr) in
|
|
A.model_split l.m.ord (l.dprm.mdl d) l.repr.B.m.B.lis r.repr.B.m.B.lis;
|
|
res
|
|
|
|
let rec add_all (a:t 'a 'b 'c 'd) (t:t 'a 'b 'c 'd) : t 'a 'b 'c 'd
|
|
requires { c a /\ c t /\ a.prm = t.prm /\ a.m.ord = t.m.ord }
|
|
ensures { c result /\ result.prm = t.prm /\ result.m.ord = t.m.ord }
|
|
ensures { forall k. CO.correct_for a.m.ord k ->
|
|
if a.m.func k = None
|
|
then result.m.func k = t.m.func k
|
|
else result.m.func k = a.m.func k }
|
|
ensures { result.m.card >= a.m.card }
|
|
ensures { result.m.card >= t.m.card }
|
|
variant { a.m.card + t.m.card }
|
|
= match view a with
|
|
| VEmpty -> t
|
|
| VNode al ad ar ah -> match view t with
|
|
| VEmpty -> a
|
|
| VNode tl td tr th -> if ah <= th
|
|
then let tk = get_key t.prm1 t.prm2 td in
|
|
let (al,ad,ar) = split tk a in
|
|
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
|
|
else let ak = get_key a.prm1 a.prm2 ad in
|
|
let (tl,_,tr) = split ak t in
|
|
let ul = add_all al tl in
|
|
let ur = add_all ar tr in
|
|
join ul ad ur
|
|
end
|
|
end
|
|
|
|
let rec filter (p:t 'a 'b 'e 'f) (a:t 'a 'b 'c 'd) : t 'a 'b 'c 'd
|
|
requires { c a /\ c p /\ a.prm1 = p.prm1 /\ a.m.ord = p.m.ord }
|
|
ensures { c result /\ result.prm = a.prm /\ result.m.ord = a.m.ord }
|
|
ensures { forall k. CO.correct_for a.m.ord k ->
|
|
if p.m.func k = None
|
|
then result.m.func k = None
|
|
else result.m.func k = a.m.func k }
|
|
ensures { result.m.card <= a.m.card }
|
|
ensures { result.m.card <= p.m.card }
|
|
variant { a.m.card + p.m.card }
|
|
= match view a with
|
|
| VEmpty -> a
|
|
| VNode al ad ar ah -> match view p with
|
|
| VEmpty -> empty a.prm1 a.prm2 a.order
|
|
| VNode pl pd pr ph -> if ah <= ph
|
|
then let pk = get_key p.prm1 p.prm2 pd in
|
|
let (al,ad,ar) = split pk a in
|
|
let fl = filter pl al in
|
|
let fr = filter pr ar in
|
|
match ad with
|
|
| None -> concat fl fr
|
|
| Some ad -> join fl ad fr
|
|
end
|
|
else let ak = get_key a.prm1 a.prm2 ad in
|
|
let (pl,pd,pr) = split ak p in
|
|
let fl = filter pl al in
|
|
let fr = filter pr ar in
|
|
match pd with
|
|
| None -> concat fl fr
|
|
| _ -> join fl ad fr
|
|
end
|
|
end
|
|
end
|
|
|
|
let rec remove_all (p:t 'a 'b 'e 'f) (a:t 'a 'b 'c 'd) : t 'a 'b 'c 'd
|
|
requires { c a /\ c p /\ a.prm1 = p.prm1 /\ a.m.ord = p.m.ord }
|
|
ensures { c result /\ result.prm = a.prm /\ result.m.ord = a.m.ord }
|
|
ensures { forall k. CO.correct_for a.m.ord k ->
|
|
if p.m.func k = None
|
|
then result.m.func k = a.m.func k
|
|
else result.m.func k = None }
|
|
ensures { result.m.card <= a.m.card }
|
|
variant { a.m.card + p.m.card }
|
|
= match view a with
|
|
| VEmpty -> a
|
|
| VNode al ad ar ah -> match view p with
|
|
| VEmpty -> a
|
|
| VNode pl pd pr ph -> if ah <= ph
|
|
then let pk = get_key p.prm1 p.prm2 pd in
|
|
let (al,_,ar) = split pk a in
|
|
let fl = remove_all pl al in
|
|
let fr = remove_all pr ar in
|
|
concat fl fr
|
|
else let ak = get_key a.prm1 a.prm2 ad in
|
|
let (pl,pd,pr) = split ak p in
|
|
let fl = remove_all pl al in
|
|
let fr = remove_all pr ar in
|
|
match pd with
|
|
| None -> join fl ad fr
|
|
| _ -> concat fl fr
|
|
end
|
|
end
|
|
end
|
|
|
|
let rec symdiff (a b:t 'a 'b 'c 'd) : t 'a 'b 'c 'd
|
|
requires { c a /\ c b /\ a.prm = b.prm /\ a.m.ord = b.m.ord }
|
|
ensures { c result /\ result.prm = a.prm /\ result.m.ord = a.m.ord }
|
|
ensures { forall k. CO.correct_for a.m.ord k ->
|
|
(a.m.func k = None -> result.m.func k = b.m.func k) /\
|
|
(b.m.func k = None -> result.m.func k = a.m.func k) /\
|
|
(a.m.func k <> None /\ b.m.func k <> None -> result.m.func k = None) }
|
|
variant { a.m.card + b.m.card }
|
|
= match view a with
|
|
| VEmpty -> b
|
|
| VNode al ad ar ah -> match view b with
|
|
| VEmpty -> a
|
|
| VNode bl bd br bh -> if ah <= bh
|
|
then let bk = get_key b.prm1 b.prm2 bd in
|
|
let (al,ad,ar) = split bk a in
|
|
let sl = symdiff al bl in
|
|
let sr = symdiff ar br in
|
|
match ad with
|
|
| None -> join sl bd sr
|
|
| _ -> concat sl sr
|
|
end
|
|
else let ak = get_key a.prm1 a.prm2 ad in
|
|
let (bl,bd,br) = split ak b in
|
|
let sl = symdiff al bl in
|
|
let sr = symdiff ar br in
|
|
match bd with
|
|
| None -> join sl ad sr
|
|
| _ -> concat sl sr
|
|
end
|
|
end
|
|
end
|
|
|
|
end
|
|
|
|
module Map
|
|
|
|
use int.Int
|
|
use program_type.TypeParams
|
|
use option.Option
|
|
use ref.Ref
|
|
|
|
(* Parameters. *)
|
|
constant balancing : int
|
|
axiom balancing_positive : balancing > 0
|
|
|
|
(* Comparable key type. *)
|
|
clone program_type.Type1 as K
|
|
clone preorder.ComputableParam as CO with namespace T = K
|
|
|
|
(* stored type is a pair. *)
|
|
namespace D
|
|
|
|
type t 'a 'b 'c 'd = (K.t 'a 'b,'c)
|
|
type m 'b 'd = (K.m 'b,'d)
|
|
function make_params (p1:type_params 'a 'b) (p2:type_params 'c 'd) :
|
|
type_params (t 'a 'b 'c 'd) (m 'b 'd) =
|
|
{ inv = \p. let (a,b) = p in p1.K.make_params.inv a /\ p2.inv b;
|
|
mdl = \p. let (a,b) = p in (p1.K.make_params.mdl a,p2.mdl b) }
|
|
function key (t:m 'b 'd) : K.m 'b = let (a,_) = t in a
|
|
let get_key (ghost p1:type_params 'a 'b) (ghost p2:type_params 'c 'd)
|
|
(t:t 'a 'b 'c 'd) : K.t 'a 'b
|
|
requires { (make_params p1 p2).inv t }
|
|
ensures { (K.make_params p1).inv result }
|
|
ensures { key ((make_params p1 p2).mdl t) =
|
|
(K.make_params p1).mdl result }
|
|
= let (a,_) = t in a
|
|
|
|
end
|
|
|
|
clone MapBase as MB with constant balancing = balancing,
|
|
goal balancing_positive,
|
|
namespace K = K,
|
|
namespace D = D,
|
|
function key = D.key,
|
|
val get_key = D.get_key,
|
|
namespace CO = CO,
|
|
goal CO.lt_def,
|
|
goal CO.eq_def,
|
|
goal CO.refl,
|
|
goal CO.trans,
|
|
goal CO.total
|
|
|
|
type t 'a 'b 'c 'd = MB.t 'a 'b 'c 'd
|
|
type m 'b 'd = {
|
|
func : K.m 'b -> option 'd;
|
|
card : int;
|
|
ord : CO.O.m 'b;
|
|
}
|
|
predicate c (t:t 'a 'b 'c 'd) = MB.c t
|
|
function prm1 (t:t 'a 'b 'c 'd) : type_params 'a 'b = t.MB.prm1
|
|
function prm2 (t:t 'a 'b 'c 'd) : type_params 'c 'd = t.MB.prm2
|
|
function prm (t:t 'a 'b 'c 'd) : (type_params 'a 'b,type_params 'c 'd) =
|
|
(t.prm1,t.prm2)
|
|
function kprm (t:t 'a 'b 'c 'd) : type_params (K.t 'a 'b) (K.m 'b) =
|
|
t.prm1.K.make_params
|
|
function oprm (t:t 'a 'b 'c 'd) : type_params (CO.O.t 'a 'b) (CO.O.m 'b) =
|
|
t.prm1.CO.O.make_params
|
|
function oproj (o:option ('a,'b)) : option 'b = match o with
|
|
| None -> None
|
|
| Some (_,v) -> Some v
|
|
end
|
|
function m (t:t 'a 'b 'c 'd) : m 'b 'd =
|
|
{ func = \k. oproj (t.MB.m.MB.func k);
|
|
ord = t.MB.m.MB.ord;
|
|
card = t.MB.m.MB.card }
|
|
|
|
let lemma m_def (t:t 'a 'b 'c 'd) : unit
|
|
ensures { forall k. t.m.func k = None <-> t.MB.m.MB.func k = None }
|
|
ensures { forall k k2 v. t.MB.m.MB.func k = Some (k2,v) ->
|
|
t.m.func k = Some v }
|
|
ensures { t.m.ord = t.MB.m.MB.ord }
|
|
ensures { t.m.card = t.MB.m.MB.card }
|
|
= ()
|
|
|
|
let lemma correction (t:t 'a 'b 'c 'd) : unit
|
|
requires { c t }
|
|
ensures { forall k1 k2:K.m 'b. CO.correct_for t.m.ord k1 /\
|
|
CO.correct_for t.m.ord k2 /\ CO.eq t.m.ord k1 k2 ->
|
|
t.m.func k1 = t.m.func k2 }
|
|
ensures { t.m.card >= 0 }
|
|
= ()
|
|
|
|
let empty (ghost p1:type_params 'a 'b)
|
|
(ghost p2:type_params 'c 'd) (o:CO.O.t 'a 'b) : t 'a 'b 'c 'd
|
|
requires { p1.CO.O.make_params.inv o }
|
|
ensures { result.prm1 = p1 /\ result.prm2 = p2 }
|
|
ensures { c result }
|
|
ensures { p1.CO.O.make_params.mdl o = result.m.ord }
|
|
ensures { forall k:K.m 'b. CO.correct_for result.m.ord k ->
|
|
result.m.func k = None }
|
|
ensures { result.m.card = 0 }
|
|
= MB.empty p1 p2 o
|
|
|
|
let singleton (ghost p1:type_params 'a 'b) (ghost p2:type_params 'c 'd)
|
|
(o:CO.O.t 'a 'b) (k:K.t 'a 'b) (v:'c) : t 'a 'b 'c 'd
|
|
requires { p1.CO.O.make_params.inv o }
|
|
requires { p1.K.make_params.inv k /\ p2.inv v }
|
|
requires { CO.correct_for (p1.CO.O.make_params.mdl o)
|
|
(p1.K.make_params.mdl k) }
|
|
ensures { result.prm1 = p1 /\ result.prm2 = p2 }
|
|
ensures { c result }
|
|
ensures { p1.CO.O.make_params.mdl o = result.m.ord }
|
|
ensures { forall k2:K.m 'b. CO.correct_for result.m.ord k2 ->
|
|
if CO.eq result.m.ord k2 (result.kprm.mdl k)
|
|
then result.m.func k2 = Some (result.prm2.mdl v)
|
|
else result.m.func k2 = None }
|
|
ensures { result.m.card = 1 }
|
|
= let d = (k,v) in
|
|
let km = p1.K.make_params.mdl k in
|
|
let dm = (D.make_params p1 p2).mdl d in
|
|
let res = MB.singleton p1 p2 o d in
|
|
assert { forall k2:K.m 'b. CO.correct_for res.m.ord k2 ->
|
|
if CO.eq res.m.ord k2 km
|
|
then res.MB.m.MB.func k2 = Some dm
|
|
else res.MB.m.MB.func k2 = None };
|
|
res
|
|
|
|
let is_empty (ghost rk:ref (K.m 'b)) (ghost rv:ref 'd)
|
|
(t:t 'a 'b 'c 'd) : bool
|
|
requires { c t }
|
|
ensures { result -> forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
t.m.func k = None }
|
|
ensures { not result -> CO.correct_for t.m.ord !rk /\
|
|
t.m.func !rk = Some !rv }
|
|
ensures { result <-> t.m.card = 0 }
|
|
= let r = ref (!rk,!rv) in
|
|
let res = MB.is_empty r t in
|
|
let (a,b) = !r in rk := a;rv := b;res
|
|
|
|
let decompose_min (t:t 'a 'b 'c 'd) : option ((K.t 'a 'b,'c),t 'a 'b 'c 'd)
|
|
requires { c t }
|
|
returns { None -> (forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
t.m.func k = None) /\ t.m.card = 0
|
|
| Some ((k,v),r) -> let vm = t.prm2.mdl v in
|
|
let km = r.kprm.mdl k in
|
|
r.prm = t.prm /\ r.m.ord = t.m.ord /\ t.kprm.inv k /\ t.prm2.inv v /\
|
|
CO.correct_for t.m.ord km /\ t.m.card = 1 + r.m.card /\
|
|
forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.lt t.m.ord k km -> t.m.func k = None) /\
|
|
(CO.eq t.m.ord k km -> t.m.func k = Some vm) /\
|
|
(CO.le r.m.ord k km -> r.m.func k = None) /\
|
|
(not CO.eq r.m.ord km k -> r.m.func k = t.m.func k) }
|
|
= let res = MB.decompose_min t in
|
|
ghost match res with None -> ()
|
|
| Some (d,r) -> let (k,v) = d in
|
|
assert { let km = t.kprm.mdl k in let vm = t.prm2.mdl v in
|
|
let dm = (D.make_params t.prm1 t.prm2).mdl d in dm = (km,vm) &&
|
|
t.kprm.inv k && t.prm2.inv v && CO.correct_for t.m.ord km &&
|
|
(forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.lt t.m.ord k km -> t.MB.m.MB.func k = None) /\
|
|
(CO.eq t.m.ord k km -> t.MB.m.MB.func k = Some dm) /\
|
|
(CO.le r.m.ord k km -> r.MB.m.MB.func k = None) /\
|
|
(not CO.eq r.m.ord km k -> r.MB.m.MB.func k = t.MB.m.MB.func k &&
|
|
r.m.func k = t.m.func k)) }
|
|
end; res
|
|
|
|
let decompose_max (t:t 'a 'b 'c 'd) : option (t 'a 'b 'c 'd,(K.t 'a 'b,'c))
|
|
requires { c t }
|
|
returns { None -> (forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
t.m.func k = None) /\ t.m.card = 0
|
|
| Some (l,(k,v)) -> let vm = t.prm2.mdl v in
|
|
let km = l.kprm.mdl k in
|
|
l.prm = t.prm /\ l.m.ord = t.m.ord /\ t.kprm.inv k /\ t.prm2.inv v /\
|
|
CO.correct_for t.m.ord km /\ t.m.card = 1 + l.m.card /\
|
|
forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.lt t.m.ord km k -> t.m.func k = None) /\
|
|
(CO.eq t.m.ord km k -> t.m.func k = Some vm) /\
|
|
(CO.le l.m.ord km k -> l.m.func k = None) /\
|
|
(not CO.eq l.m.ord k km -> l.m.func k = t.m.func k) }
|
|
= let res = MB.decompose_max t in
|
|
ghost match res with None -> ()
|
|
| Some (l,d) -> let (k,v) = d in
|
|
assert { let km = t.kprm.mdl k in let vm = t.prm2.mdl v in
|
|
let dm = (D.make_params t.prm1 t.prm2).mdl d in dm = (km,vm) &&
|
|
t.kprm.inv k && t.prm2.inv v && CO.correct_for t.m.ord km &&
|
|
(forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.lt t.m.ord km k -> t.MB.m.MB.func k = None) /\
|
|
(CO.eq t.m.ord km k -> t.MB.m.MB.func k = Some dm) /\
|
|
(CO.le l.m.ord km k -> l.MB.m.MB.func k = None) /\
|
|
(not CO.eq l.m.ord k km -> l.MB.m.MB.func k = t.MB.m.MB.func k)) }
|
|
end; res
|
|
|
|
let add_min (k:K.t 'a 'b) (v:'c) (t:t 'a 'b 'c 'd) : t 'a 'b 'c 'd
|
|
requires { c t /\ t.kprm.inv k /\ t.prm2.inv v }
|
|
requires { CO.correct_for t.m.ord (t.kprm.mdl k) }
|
|
requires { forall k2:K.m 'b. CO.correct_for t.m.ord k2 /\
|
|
CO.le t.m.ord k2 (t.kprm.mdl k) -> t.m.func k2 = None }
|
|
ensures { c result /\ result.prm = t.prm /\ result.m.ord = t.m.ord }
|
|
ensures { let km = t.kprm.mdl k in let vm = t.prm2.mdl v in
|
|
forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.lt t.m.ord k km -> result.m.func k = None) /\
|
|
(CO.eq t.m.ord k km -> result.m.func k = Some vm) /\
|
|
(not CO.eq t.m.ord km k -> result.m.func k = t.m.func k) }
|
|
ensures { result.m.card = 1 + t.m.card }
|
|
= let d = (k,v) in
|
|
let res = MB.add_min d t in
|
|
assert { let km = t.kprm.mdl k in let vm = t.prm2.mdl v in
|
|
let dm = (D.make_params t.prm1 t.prm2).mdl d in dm = (km,vm) &&
|
|
forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.lt t.m.ord k km -> res.MB.m.MB.func k = None) /\
|
|
(CO.eq t.m.ord k km -> res.MB.m.MB.func k = Some dm) /\
|
|
(not CO.eq t.m.ord km k -> res.MB.m.MB.func k = t.MB.m.MB.func k) };
|
|
res
|
|
|
|
let add_max (t:t 'a 'b 'c 'd) (k:K.t 'a 'b) (v:'c) : t 'a 'b 'c 'd
|
|
requires { c t /\ t.kprm.inv k /\ t.prm2.inv v }
|
|
requires { CO.correct_for t.m.ord (t.kprm.mdl k) }
|
|
requires { forall k2:K.m 'b. CO.correct_for t.m.ord k2 /\
|
|
CO.le t.m.ord (t.kprm.mdl k) k2 -> t.m.func k2 = None }
|
|
ensures { c result /\ result.prm = t.prm /\ result.m.ord = t.m.ord }
|
|
ensures { let km = t.kprm.mdl k in let vm = t.prm2.mdl v in
|
|
forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.lt t.m.ord km k -> result.m.func k = None) /\
|
|
(CO.eq t.m.ord km k -> result.m.func k = Some vm) /\
|
|
(not CO.eq t.m.ord k km -> result.m.func k = t.m.func k) }
|
|
ensures { result.m.card = 1 + t.m.card }
|
|
= let d = (k,v) in
|
|
let res = MB.add_max t d in
|
|
assert { let km = t.kprm.mdl k in let vm = t.prm2.mdl v in
|
|
let dm = (D.make_params t.prm1 t.prm2).mdl d in dm = (km,vm) &&
|
|
forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.lt t.m.ord km k -> res.MB.m.MB.func k = None) /\
|
|
(CO.eq t.m.ord km k -> res.MB.m.MB.func k = Some dm) /\
|
|
(not CO.eq t.m.ord k km -> res.MB.m.MB.func k = t.MB.m.MB.func k) };
|
|
res
|
|
|
|
let concat (l r:t 'a 'b 'c 'd) : t 'a 'b 'c 'd
|
|
requires { c l /\ c r /\ l.prm = r.prm /\ l.m.ord = r.m.ord }
|
|
requires { forall k1 k2. CO.correct_for l.m.ord k1 /\
|
|
CO.correct_for r.m.ord k2 /\ l.m.func k1 <> None /\
|
|
r.m.func k2 <> None -> CO.lt l.m.ord k1 k2 }
|
|
ensures { c result /\ result.prm = l.prm /\ result.m.ord = l.m.ord }
|
|
ensures { forall k. CO.correct_for l.m.ord k ->
|
|
match l.m.func k with None -> result.m.func k = r.m.func k
|
|
| s -> result.m.func k = s end }
|
|
ensures { forall k. CO.correct_for l.m.ord k ->
|
|
match r.m.func k with None -> result.m.func k = l.m.func k
|
|
| s -> result.m.func k = s end }
|
|
ensures { forall k. CO.correct_for l.m.ord k -> (result.m.func k = None <->
|
|
l.m.func k = None /\ r.m.func k = None) }
|
|
ensures { result.m.card = l.m.card + r.m.card }
|
|
= MB.concat l r
|
|
|
|
let get (k:K.t 'a 'b) (t:t 'a 'b 'c 'd) : option 'c
|
|
requires { c t /\ t.kprm.inv k }
|
|
requires { CO.correct_for t.m.ord (t.kprm.mdl k) }
|
|
returns { None -> let km = t.kprm.mdl k in
|
|
(forall k2. CO.correct_for t.m.ord k2 /\ CO.eq t.m.ord km k2 ->
|
|
t.m.func k2 = None) && t.m.func km = None
|
|
| Some v -> t.prm2.inv v /\ t.m.card > 0 /\ let km = t.kprm.mdl k in
|
|
let vm = t.prm2.mdl v in
|
|
(forall k2. CO.correct_for t.m.ord k2 /\ CO.eq t.m.ord km k2 ->
|
|
t.m.func k2 = Some vm) && t.m.func km = Some vm }
|
|
= match MB.get k t with
|
|
| None -> None
|
|
| Some (_,v) -> Some v
|
|
end
|
|
|
|
let add (k:K.t 'a 'b) (v:'c) (t:t 'a 'b 'c 'd) : t 'a 'b 'c 'd
|
|
requires { c t /\ t.kprm.inv k /\ t.prm2.inv v }
|
|
requires { CO.correct_for t.m.ord (t.kprm.mdl k) }
|
|
ensures { c result /\ result.prm = t.prm /\ result.m.ord = t.m.ord }
|
|
ensures { let vm = t.prm2.mdl v in let km = t.kprm.mdl k in
|
|
result.m.card >= t.m.card /\
|
|
(if t.m.func km = None
|
|
then result.m.card = t.m.card + 1
|
|
else result.m.card = t.m.card) /\
|
|
(forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.eq t.m.ord k km -> result.m.func k = Some vm) /\
|
|
(not CO.eq t.m.ord k km -> result.m.func k = t.m.func k)) &&
|
|
result.m.func km = Some vm }
|
|
= let d = (k,v) in let res = MB.add d t in
|
|
assert { let km = t.kprm.mdl k in let vm = t.prm2.mdl v in
|
|
let dm = (D.make_params t.prm1 t.prm2).mdl d in dm = (km,vm) &&
|
|
forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(not CO.eq t.m.ord k km -> res.MB.m.MB.func k = t.MB.m.MB.func k) };
|
|
res
|
|
|
|
let remove (k:K.t 'a 'b) (t:t 'a 'b 'c 'd) : t 'a 'b 'c 'd
|
|
requires { c t /\ t.kprm.inv k }
|
|
requires { CO.correct_for t.m.ord (t.kprm.mdl k) }
|
|
ensures { c result /\ result.prm = t.prm /\ result.m.ord = t.m.ord }
|
|
ensures { let km = t.kprm.mdl k in
|
|
result.m.card <= t.m.card /\
|
|
(if t.m.func km = None
|
|
then result.m.card = t.m.card
|
|
else 1 + result.m.card = t.m.card) /\
|
|
(forall k2:K.m 'b. CO.correct_for t.m.ord k2 ->
|
|
(CO.eq t.m.ord k2 km -> result.m.func k2 = None) /\
|
|
(not CO.eq t.m.ord k2 km -> result.m.func k2 = t.m.func k2)) &&
|
|
result.m.func km = None }
|
|
= MB.remove k t
|
|
|
|
let split (k:K.t 'a 'b) (t:t 'a 'b 'c 'd) :
|
|
(t 'a 'b 'c 'd,option 'c,t 'a 'b 'c 'd)
|
|
requires { c t /\ t.kprm.inv k }
|
|
requires { CO.correct_for t.m.ord (t.kprm.mdl k) }
|
|
returns { (lf,o,rg) ->
|
|
lf.prm = t.prm = rg.prm /\ lf.m.ord = t.m.ord = rg.m.ord /\
|
|
c lf /\ c rg /\
|
|
let om = t.m.ord in
|
|
let km = t.kprm.mdl k in
|
|
match o with
|
|
| None -> (forall k2:K.m 'b. CO.correct_for om k2 /\ CO.eq om km k2 ->
|
|
t.m.func k2 = None) && t.m.func km = None
|
|
| Some v -> t.prm2.inv v /\ let vm = t.prm2.mdl v in
|
|
(forall k2:K.m 'b. CO.correct_for om k2 /\ CO.eq om km k2 ->
|
|
t.m.func k2 = Some vm) && t.m.func km = Some vm
|
|
end /\
|
|
t.m.card >= lf.m.card + rg.m.card /\
|
|
(if o = None
|
|
then t.m.card = lf.m.card + rg.m.card
|
|
else t.m.card = 1 + (lf.m.card + rg.m.card)) /\
|
|
(forall k2:K.m 'b. CO.correct_for om k2 /\ CO.lt om k2 km ->
|
|
lf.m.func k2 = t.m.func k2) /\
|
|
(forall k2:K.m 'b. CO.correct_for om k2 /\ CO.le om km k2 ->
|
|
lf.m.func k2 = None) /\
|
|
(forall k2:K.m 'b. CO.correct_for om k2 /\ CO.lt om km k2 ->
|
|
rg.m.func k2 = t.m.func k2) /\
|
|
(forall k2:K.m 'b. CO.correct_for om k2 /\ CO.le om k2 km ->
|
|
rg.m.func k2 = None) }
|
|
= let (lf,o,rg) = MB.split k t in
|
|
let o = abstract ensures { match o with None -> result = None
|
|
| Some (_,v) -> result = Some v end }
|
|
match o with None -> None | Some (_,v) -> Some v end end in
|
|
(lf,o,rg)
|
|
|
|
end
|
|
|
|
module Set
|
|
|
|
use int.Int
|
|
use program_type.TypeParams
|
|
use option.Option
|
|
use ref.Ref
|
|
|
|
(* Parameters. *)
|
|
constant balancing : int
|
|
axiom balancing_positive : balancing > 0
|
|
|
|
(* Comparable key type. *)
|
|
clone program_type.Type1 as K
|
|
clone preorder.ComputableParam as CO with namespace T = K
|
|
|
|
(* stored type is only the key. *)
|
|
namespace D
|
|
|
|
type t 'a 'b 'c 'd = K.t 'a 'b
|
|
type m 'b 'd = K.m 'b
|
|
function make_params (p1:type_params 'a 'b) (p2:type_params 'c 'd) :
|
|
type_params (t 'a 'b 'c 'd) (m 'b 'd) = p1.K.make_params
|
|
function key (t:m 'b 'd) : K.m 'b = t
|
|
let get_key (ghost p1:type_params 'a 'b) (ghost p2:type_params 'c 'd)
|
|
(t:t 'a 'b 'c 'd) : K.t 'a 'b
|
|
requires { (make_params p1 p2).inv t }
|
|
ensures { (K.make_params p1).inv result }
|
|
ensures { key ((make_params p1 p2).mdl t) =
|
|
(K.make_params p1).mdl result }
|
|
= t
|
|
|
|
end
|
|
|
|
clone MapBase as MB with constant balancing = balancing,
|
|
goal balancing_positive,
|
|
namespace K = K,
|
|
namespace D = D,
|
|
function key = D.key,
|
|
val get_key = D.get_key,
|
|
namespace CO = CO,
|
|
goal CO.lt_def,
|
|
goal CO.eq_def,
|
|
goal CO.refl,
|
|
goal CO.trans,
|
|
goal CO.total
|
|
|
|
type t 'a 'b = MB.t 'a 'b 'a 'b
|
|
type m 'b = {
|
|
set : K.m 'b -> bool;
|
|
card : int;
|
|
ord : CO.O.m 'b;
|
|
}
|
|
predicate c (t:t 'a 'b) = MB.c t /\ t.MB.prm1 = t.MB.prm2
|
|
function prm (t:t 'a 'b) : type_params 'a 'b = t.MB.prm1
|
|
function kprm (t:t 'a 'b) : type_params (K.t 'a 'b) (K.m 'b) =
|
|
t.prm.K.make_params
|
|
function oprm (t:t 'a 'b) : type_params (CO.O.t 'a 'b) (CO.O.m 'b) =
|
|
t.prm.CO.O.make_params
|
|
function oproj (o:option 'a) : bool = match o with
|
|
| None -> false
|
|
| Some _ -> true
|
|
end
|
|
function m (t:t 'a 'b) : m 'b =
|
|
{ set = \k. oproj (t.MB.m.MB.func k);
|
|
ord = t.MB.m.MB.ord;
|
|
card = t.MB.m.MB.card }
|
|
|
|
let lemma m_def (t:t 'a 'b) : unit
|
|
ensures { forall k. not t.m.set k <-> t.MB.m.MB.func k = None }
|
|
ensures { forall k v. t.MB.m.MB.func k = Some v ->
|
|
t.m.set k }
|
|
ensures { t.m.ord = t.MB.m.MB.ord }
|
|
ensures { t.m.card = t.MB.m.MB.card }
|
|
= ()
|
|
|
|
let lemma correction (t:t 'a 'b) : unit
|
|
requires { c t }
|
|
ensures { forall k1 k2:K.m 'b. CO.correct_for t.m.ord k1 /\
|
|
CO.correct_for t.m.ord k2 /\ CO.eq t.m.ord k1 k2 ->
|
|
t.m.set k1 <-> t.m.set k2 }
|
|
ensures { t.m.card >= 0 }
|
|
= ()
|
|
|
|
let empty (ghost p:type_params 'a 'b) (o:CO.O.t 'a 'b) : t 'a 'b
|
|
requires { p.CO.O.make_params.inv o }
|
|
ensures { result.prm = p }
|
|
ensures { c result }
|
|
ensures { p.CO.O.make_params.mdl o = result.m.ord }
|
|
ensures { forall k:K.m 'b. CO.correct_for result.m.ord k ->
|
|
not result.m.set k }
|
|
ensures { result.m.card = 0 }
|
|
= MB.empty p p o
|
|
|
|
let singleton (ghost p:type_params 'a 'b) (o:CO.O.t 'a 'b)
|
|
(k:K.t 'a 'b) : t 'a 'b
|
|
requires { p.CO.O.make_params.inv o }
|
|
requires { p.K.make_params.inv k }
|
|
requires { CO.correct_for (p.CO.O.make_params.mdl o)
|
|
(p.K.make_params.mdl k) }
|
|
ensures { result.prm = p }
|
|
ensures { c result }
|
|
ensures { p.CO.O.make_params.mdl o = result.m.ord }
|
|
ensures { forall k2:K.m 'b. CO.correct_for result.m.ord k2 ->
|
|
result.m.set k2 <-> CO.eq result.m.ord k2 (result.kprm.mdl k) }
|
|
ensures { result.m.card = 1 }
|
|
= MB.singleton p p o k
|
|
|
|
let is_empty (ghost rk:ref (K.m 'b)) (t:t 'a 'b) : bool
|
|
requires { c t }
|
|
ensures { result -> forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
not t.m.set k }
|
|
ensures { not result -> CO.correct_for t.m.ord !rk /\
|
|
t.m.set !rk }
|
|
ensures { result <-> t.m.card = 0 }
|
|
= MB.is_empty rk t
|
|
|
|
let decompose_min (t:t 'a 'b) : option (K.t 'a 'b,t 'a 'b)
|
|
requires { c t }
|
|
returns { None -> t.m.card = 0 /\
|
|
forall k:K.m 'b. CO.correct_for t.m.ord k -> not t.m.set k
|
|
| Some (k,r) -> let km = r.kprm.mdl k in
|
|
r.prm = t.prm /\ r.m.ord = t.m.ord /\ t.kprm.inv k /\
|
|
CO.correct_for t.m.ord km /\ t.m.card = 1 + r.m.card /\
|
|
forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.lt t.m.ord k km -> not t.m.set k) /\
|
|
(CO.eq t.m.ord k km -> t.m.set k) /\
|
|
(CO.le r.m.ord k km -> not r.m.set k) /\
|
|
(not CO.eq r.m.ord km k -> r.m.set k <-> t.m.set k) }
|
|
= MB.decompose_min t
|
|
|
|
let decompose_max (t:t 'a 'b) : option (t 'a 'b,K.t 'a 'b)
|
|
requires { c t }
|
|
returns { None -> t.m.card = 0 /\
|
|
forall k:K.m 'b. CO.correct_for t.m.ord k -> not t.m.set k
|
|
| Some (l,k) -> let km = l.kprm.mdl k in
|
|
l.prm = t.prm /\ l.m.ord = t.m.ord /\ t.kprm.inv k /\
|
|
CO.correct_for t.m.ord km /\ t.m.card = 1 + l.m.card /\
|
|
forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.lt t.m.ord km k -> not t.m.set k) /\
|
|
(CO.eq t.m.ord km k -> t.m.set k) /\
|
|
(CO.le l.m.ord km k -> not l.m.set k) /\
|
|
(not CO.eq l.m.ord k km -> l.m.set k <-> t.m.set k) }
|
|
= MB.decompose_max t
|
|
|
|
let add_min (k:K.t 'a 'b) (t:t 'a 'b) : t 'a 'b
|
|
requires { c t /\ t.kprm.inv k }
|
|
requires { CO.correct_for t.m.ord (t.kprm.mdl k) }
|
|
requires { forall k2:K.m 'b. CO.correct_for t.m.ord k2 /\
|
|
CO.le t.m.ord k2 (t.kprm.mdl k) -> not t.m.set k2 }
|
|
ensures { c result /\ result.prm = t.prm /\ result.m.ord = t.m.ord }
|
|
ensures { let km = t.kprm.mdl k in
|
|
forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.lt t.m.ord k km -> not result.m.set k) /\
|
|
(CO.eq t.m.ord k km -> result.m.set k) /\
|
|
(not CO.eq t.m.ord km k -> result.m.set k <-> t.m.set k) }
|
|
ensures { result.m.card = 1 + t.m.card }
|
|
= MB.add_min k t
|
|
|
|
let add_max (t:t 'a 'b) (k:K.t 'a 'b) : t 'a 'b
|
|
requires { c t /\ t.kprm.inv k }
|
|
requires { CO.correct_for t.m.ord (t.kprm.mdl k) }
|
|
requires { forall k2:K.m 'b. CO.correct_for t.m.ord k2 /\
|
|
CO.le t.m.ord (t.kprm.mdl k) k2 -> not t.m.set k2 }
|
|
ensures { c result /\ result.prm = t.prm /\ result.m.ord = t.m.ord }
|
|
ensures { let km = t.kprm.mdl k in
|
|
forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.lt t.m.ord km k -> not result.m.set k) /\
|
|
(CO.eq t.m.ord km k -> result.m.set k) /\
|
|
(not CO.eq t.m.ord k km -> result.m.set k <-> t.m.set k) }
|
|
ensures { result.m.card = 1 + t.m.card }
|
|
= MB.add_max t k
|
|
|
|
let concat (l r:t 'a 'b) : t 'a 'b
|
|
requires { c l /\ c r /\ l.prm = r.prm /\ l.m.ord = r.m.ord }
|
|
requires { forall k1 k2. CO.correct_for l.m.ord k1 /\
|
|
CO.correct_for r.m.ord k2 /\ l.m.set k1 /\ r.m.set k2 ->
|
|
CO.lt l.m.ord k1 k2 }
|
|
ensures { c result /\ result.prm = l.prm /\ result.m.ord = l.m.ord }
|
|
ensures { forall k. CO.correct_for l.m.ord k -> result.m.set k <->
|
|
(r.m.set k \/ l.m.set k) }
|
|
ensures { result.m.card = l.m.card + r.m.card }
|
|
= MB.concat l r
|
|
|
|
let mem (k:K.t 'a 'b) (t:t 'a 'b) : bool
|
|
requires { c t /\ t.kprm.inv k }
|
|
requires { CO.correct_for t.m.ord (t.kprm.mdl k) }
|
|
ensures { result <-> t.m.set (t.kprm.mdl k) }
|
|
ensures { result <-> (forall k2. CO.correct_for t.m.ord k2 /\
|
|
CO.eq t.m.ord k2 (t.kprm.mdl k) -> t.m.set k2) }
|
|
ensures { result -> t.m.card > 0 }
|
|
= match MB.get k t with None -> false | _ -> true end
|
|
|
|
let add (k:K.t 'a 'b) (t:t 'a 'b) : t 'a 'b
|
|
requires { c t /\ t.kprm.inv k }
|
|
requires { CO.correct_for t.m.ord (t.kprm.mdl k) }
|
|
ensures { c result /\ result.prm = t.prm /\ result.m.ord = t.m.ord }
|
|
ensures { let km = t.kprm.mdl k in
|
|
result.m.card >= t.m.card /\
|
|
(if t.m.set km
|
|
then result.m.card = t.m.card
|
|
else result.m.card = t.m.card + 1) /\
|
|
(forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.eq t.m.ord k km -> result.m.set k) /\
|
|
(t.m.set k -> result.m.set k) /\
|
|
(not CO.eq t.m.ord k km -> result.m.set k -> t.m.set k)) &&
|
|
result.m.set km }
|
|
= MB.add k t
|
|
|
|
let remove (k:K.t 'a 'b) (t:t 'a 'b) : t 'a 'b
|
|
requires { c t /\ t.kprm.inv k }
|
|
requires { CO.correct_for t.m.ord (t.kprm.mdl k) }
|
|
ensures { c result /\ result.prm = t.prm /\ result.m.ord = t.m.ord }
|
|
ensures { let km = t.kprm.mdl k in
|
|
result.m.card <= t.m.card /\
|
|
(if t.m.set km
|
|
then 1 + result.m.card = t.m.card
|
|
else result.m.card = t.m.card) /\
|
|
(forall k:K.m 'b. CO.correct_for t.m.ord k ->
|
|
(CO.eq t.m.ord k km -> not result.m.set k) /\
|
|
(result.m.set k -> t.m.set k) /\
|
|
(not CO.eq t.m.ord k km -> t.m.set k -> result.m.set k)) &&
|
|
not result.m.set km }
|
|
= MB.remove k t
|
|
|
|
let split (k:K.t 'a 'b) (t:t 'a 'b) : (t 'a 'b,bool,t 'a 'b)
|
|
requires { c t /\ t.kprm.inv k }
|
|
requires { CO.correct_for t.m.ord (t.kprm.mdl k) }
|
|
returns { (lf,b,rg) ->
|
|
lf.prm = t.prm = rg.prm /\ lf.m.ord = t.m.ord = rg.m.ord /\
|
|
c lf /\ c rg /\
|
|
let om = t.m.ord in let km = t.kprm.mdl k in
|
|
(b <-> t.m.set km) /\
|
|
(b <-> (forall k. CO.correct_for om k /\ CO.eq om k km ->
|
|
t.m.set km)) /\
|
|
t.m.card >= lf.m.card + rg.m.card /\
|
|
(if b
|
|
then t.m.card = 1 + (lf.m.card + rg.m.card)
|
|
else t.m.card = lf.m.card + rg.m.card) /\
|
|
(forall k. CO.correct_for om k /\ lf.m.set k -> t.m.set k) /\
|
|
(forall k. CO.correct_for om k /\ rg.m.set k -> t.m.set k) /\
|
|
(forall k. CO.correct_for om k /\ CO.lt om k km ->
|
|
t.m.set k -> lf.m.set k) /\
|
|
(forall k. CO.correct_for om k /\ CO.lt om km k ->
|
|
t.m.set k -> rg.m.set k) /\
|
|
(forall k. CO.correct_for om k /\ CO.le om km k ->
|
|
not lf.m.set k) /\
|
|
(forall k. CO.correct_for om k /\ CO.le om k km ->
|
|
not rg.m.set k) }
|
|
= let (lf,o,rg) = MB.split k t in
|
|
let o = abstract ensures { result <-> o <> None }
|
|
match o with None -> false | _ -> true end end in
|
|
(lf,o,rg)
|
|
|
|
let union (a b:t 'a 'b) : t 'a 'b
|
|
requires { c a /\ c b /\ a.prm = b.prm /\ a.m.ord = b.m.ord }
|
|
ensures { c result /\ result.prm = a.prm /\ result.m.ord = a.m.ord }
|
|
ensures { forall k. CO.correct_for a.m.ord k ->
|
|
(result.m.set k <-> a.m.set k \/ b.m.set k) }
|
|
ensures { result.m.card >= a.m.card /\ result.m.card >= b.m.card }
|
|
= MB.add_all a b
|
|
|
|
let inter (a b:t 'a 'b) : t 'a 'b
|
|
requires { c a /\ c b /\ a.prm = b.prm /\ a.m.ord = b.m.ord }
|
|
ensures { c result /\ result.prm = a.prm /\ result.m.ord = a.m.ord }
|
|
ensures { forall k. CO.correct_for a.m.ord k ->
|
|
(result.m.set k <-> a.m.set k /\ b.m.set k) }
|
|
ensures { result.m.card <= a.m.card /\ result.m.card <= b.m.card }
|
|
= MB.filter a b
|
|
|
|
let diff (a b:t 'a 'b) : t 'a 'b
|
|
requires { c a /\ c b /\ a.prm = b.prm /\ a.m.ord = b.m.ord }
|
|
ensures { c result /\ result.prm = a.prm /\ result.m.ord = a.m.ord }
|
|
ensures { forall k. CO.correct_for a.m.ord k ->
|
|
(result.m.set k <-> a.m.set k /\ not b.m.set k) }
|
|
ensures { result.m.card <= a.m.card }
|
|
= MB.remove_all b a
|
|
|
|
let symdiff (a b:t 'a 'b) : t 'a 'b
|
|
requires { c a /\ c b /\ a.prm = b.prm /\ a.m.ord = b.m.ord }
|
|
ensures { c result /\ result.prm = a.prm /\ result.m.ord = a.m.ord }
|
|
ensures { forall k. CO.correct_for a.m.ord k ->
|
|
(result.m.set k <-> not (a.m.set k <-> b.m.set k)) }
|
|
= MB.symdiff a b
|
|
|
|
end
|
|
|
|
(* Example with integer keys and fixed ordering. *)
|
|
module IMapAndSet
|
|
|
|
use int.Int
|
|
use program_type.TypeParams
|
|
|
|
namespace K
|
|
type t 'a 'b = int
|
|
type m 'b = int
|
|
function make_params (p:type_params 'a 'b) : type_params int int =
|
|
default_params
|
|
end
|
|
|
|
namespace O
|
|
type t 'a 'b = unit
|
|
type m 'b = unit
|
|
function make_params (p:type_params 'a 'b) : type_params unit unit =
|
|
default_params
|
|
end
|
|
|
|
constant balancing : int = 1
|
|
|
|
predicate le unit (x y:int) = x <= y
|
|
predicate eq unit (x y:int) = x = y
|
|
predicate lt unit (x y:int) = x < y
|
|
predicate correct_for unit int = true
|
|
|
|
let compare (ghost p:type_params 'a 'b) (o:unit) (x y:int) : int
|
|
ensures { result = x - y }
|
|
= x - y
|
|
|
|
clone Map as M with constant balancing = balancing,
|
|
goal balancing_positive,
|
|
namespace K = K,
|
|
namespace CO.O = O,
|
|
predicate CO.le = le,
|
|
predicate CO.lt = lt,
|
|
predicate CO.eq = eq,
|
|
predicate CO.correct_for = correct_for,
|
|
goal CO.lt_def,
|
|
goal CO.eq_def,
|
|
goal CO.refl,
|
|
goal CO.trans,
|
|
goal CO.total,
|
|
val CO.compare = compare
|
|
|
|
clone Set as S with constant balancing = balancing,
|
|
goal balancing_positive,
|
|
namespace K = K,
|
|
namespace CO.O = O,
|
|
predicate CO.le = le,
|
|
predicate CO.lt = lt,
|
|
predicate CO.eq = eq,
|
|
predicate CO.correct_for = correct_for,
|
|
goal CO.lt_def,
|
|
goal CO.eq_def,
|
|
goal CO.refl,
|
|
goal CO.trans,
|
|
goal CO.total,
|
|
val CO.compare = compare
|
|
|
|
end
|
|
|