Commit 68d0207b authored by Martin Clochard's avatar Martin Clochard

AVL example: cleanup+alpha-renaming

parent 32b418b9
...@@ -931,7 +931,7 @@ ...@@ -931,7 +931,7 @@
memlimit="1000" memlimit="1000"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="1.53"/> <result status="valid" time="1.80"/>
</proof> </proof>
</goal> </goal>
<goal <goal
...@@ -992,7 +992,7 @@ ...@@ -992,7 +992,7 @@
memlimit="1000" memlimit="1000"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="1.23"/> <result status="valid" time="0.93"/>
</proof> </proof>
</goal> </goal>
<goal <goal
......
...@@ -130,8 +130,8 @@ module AssocSorted ...@@ -130,8 +130,8 @@ module AssocSorted
let lemma model_cut (k:key) (l r:list (t 'a)) : unit let lemma model_cut (k:key) (l r:list (t 'a)) : unit
requires { S.increasing r } requires { S.increasing r }
requires { S.increasing l } requires { S.increasing l }
requires { S.majorate k l } requires { S.upper_bound k l }
requires { S.minorate k r } requires { S.lower_bound k r }
ensures { forall k2. eq k k2 -> model (l++r) k2 = None } ensures { forall k2. eq k k2 -> model (l++r) k2 = None }
ensures { forall k2. lt k k2 -> model (l++r) k2 = model r k2 } ensures { forall k2. lt k k2 -> model (l++r) k2 = model r k2 }
ensures { forall k2. le k2 k -> model r k2 = None } ensures { forall k2. le k2 k -> model r k2 = None }
...@@ -160,8 +160,8 @@ module AssocSorted ...@@ -160,8 +160,8 @@ module AssocSorted
let lemma model_split (d:t 'a) (l r:list (t 'a)) : unit let lemma model_split (d:t 'a) (l r:list (t 'a)) : unit
requires { S.increasing l } requires { S.increasing l }
requires { S.increasing r } requires { S.increasing r }
requires { S.majorate d.key l } requires { S.upper_bound d.key l }
requires { S.minorate d.key r } requires { S.lower_bound d.key r }
ensures { forall k2. eq d.key k2 -> model (l++Cons d r) k2 = Some d } ensures { forall k2. eq d.key k2 -> model (l++Cons d r) k2 = Some d }
ensures { forall k2. lt d.key k2 -> model (l++Cons d r) k2 = model r k2 } ensures { forall k2. lt d.key k2 -> model (l++Cons d r) k2 = model r k2 }
ensures { forall k2. le k2 d.key -> model r k2 = None } ensures { forall k2. le k2 d.key -> model r k2 = None }
......
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
...@@ -43,20 +43,20 @@ module MapBase ...@@ -43,20 +43,20 @@ module MapBase
type m = unit type m = unit
type t = unit type t = unit
constant zero : unit = () constant zero : unit = ()
function add (x y:unit) : unit = () function op (x y:unit) : unit = ()
let lemma neutral_ (x:unit) : unit let lemma neutral_ (x:unit) : unit
ensures { add zero x = x = add x zero } ensures { op zero x = x = op x zero }
= match x with _ -> () end = match x with _ -> () end
clone export monoid.Monoid with type t = m, clone export monoid.Monoid with type t = m,
constant zero = zero,function add = add,lemma assoc,lemma neutral constant zero = zero,function op = op,lemma assoc,lemma neutral
clone export monoid.MonoidListDef with type M.t = m, clone export monoid.MonoidListDef with type M.t = m,
constant M.zero = zero,function M.add = add,goal M.assoc,goal M.neutral constant M.zero = zero,function M.op = op,goal M.assoc,goal M.neutral
function m (x:'a) : 'a = x function m (x:'a) : 'a = x
predicate c (x:'a) = true predicate c (x:'a) = true
let zero () : unit let zero () : unit
ensures { result = () } ensures { result = () }
= () = ()
let add (x y:unit) : unit let op (x y:unit) : unit
ensures { result = () } ensures { result = () }
= () = ()
end end
...@@ -67,18 +67,21 @@ module MapBase ...@@ -67,18 +67,21 @@ module MapBase
(* Correction of a selector with respect to a list: (* Correction of a selector with respect to a list:
The list is sorted. *) The list is sorted. *)
predicate selector_correct (s:K.t) (l:list (D.m 'b)) = predicate selection_possible (s:K.t) (l:list (D.m 'b)) =
A.S.increasing l /\ K.c s A.S.increasing l /\ K.c s
predicate selected (s:K.t) (e:position (D.m 'b)) (l:list (D.m 'b)) = predicate selected (s:K.t) (e:split (D.m 'b)) (l:list (D.m 'b)) =
(A.S.majorate s.K.m e.left /\ A.S.minorate s.K.m e.right /\ (A.S.upper_bound s.K.m e.left /\ A.S.lower_bound s.K.m e.right /\
A.S.increasing e.left /\ A.S.increasing e.right /\
match e.middle with match e.middle with
| None -> true | None -> true
| Some d2 -> CO.eq s.K.m d2.key | Some d2 -> CO.eq s.K.m d2.key
end) /\ rebuild e = l /\ selector_correct s l end)
(* Strictly speaking, not necessary because derivable from the context,
but makes easier to write some lemmas. *)
/\ A.S.increasing e.left /\ A.S.increasing e.right /\
rebuild e = l /\ selection_possible s l
predicate selected_sem (s:K.t) (e:position (D.m 'b)) (l:list (D.m 'b)) = predicate selected_sem (s:K.t) (e:split (D.m 'b)) (l:list (D.m 'b)) =
forall k:K.m. (CO.lt k s.K.m -> A.model l k = A.model e.left k) /\ forall k:K.m. (CO.lt k s.K.m -> A.model l k = A.model e.left k) /\
(CO.lt s.K.m k -> A.model l k = A.model e.right k) /\ (CO.lt s.K.m k -> A.model l k = A.model e.right k) /\
(CO.eq k s.K.m -> A.model l k = e.middle) /\ (CO.eq k s.K.m -> A.model l k = e.middle) /\
...@@ -86,7 +89,7 @@ module MapBase ...@@ -86,7 +89,7 @@ module MapBase
(CO.le k s.K.m -> A.model e.right k = None) (CO.le k s.K.m -> A.model e.right k = None)
let lemma selected_sem (s:K.t) let lemma selected_sem (s:K.t)
(e:position (D.m 'b)) (l:list (D.m 'b)) : unit (e:split (D.m 'b)) (l:list (D.m 'b)) : unit
requires { selected s e l } requires { selected s e l }
ensures { selected_sem s e l } ensures { selected_sem s e l }
= match e.middle with = match e.middle with
...@@ -94,22 +97,21 @@ module MapBase ...@@ -94,22 +97,21 @@ module MapBase
| Some dm -> A.model_split dm e.left e.right | Some dm -> A.model_split dm e.left e.right
end end
let selected_way (ghost p:type_params 'a 'b) let selected_part (ghost p:type_params 'a 'b)
(ghost base:list (D.m 'b)) (ghost base:list (D.m 'b))
(ghost llis:list (D.m 'b)) (ghost llis:list (D.m 'b))
(ghost rlis:list (D.m 'b)) (ghost rlis:list (D.m 'b))
(s:K.t) (l:'e) (d:D.t 'a 'b) (r:'f) : way_base K.t (s:K.t) (l:'e) (d:D.t 'a 'b) (r:'f) : part_base K.t
requires { p.D.mp.inv d } requires { p.D.mp.inv d }
requires { base = llis ++ Cons (p.D.mp.mdl d) rlis } requires { base = llis ++ Cons (p.D.mp.mdl d) rlis }
requires { selector_correct s base } requires { selection_possible s base }
(* A selected position can be found by following the given way. *)
returns { Here -> let e2 = { left = llis; returns { Here -> let e2 = { left = llis;
middle = Some (p.D.mp.mdl d); middle = Some (p.D.mp.mdl d);
right = rlis } in selected s e2 base right = rlis } in selected s e2 base
| Left sl -> selector_correct sl llis /\ | Left sl -> selection_possible sl llis /\
forall e. selected sl e llis -> forall e. selected sl e llis ->
selected s (right_extend e (p.D.mp.mdl d) rlis) base selected s (right_extend e (p.D.mp.mdl d) rlis) base
| Right sr -> selector_correct sr rlis /\ | Right sr -> selection_possible sr rlis /\
forall e. selected sr e rlis -> forall e. selected sr e rlis ->
selected s (left_extend llis (p.D.mp.mdl d) e) base } selected s (left_extend llis (p.D.mp.mdl d) e) base }
= let kd = get_key p d in = let kd = get_key p d in
...@@ -122,10 +124,10 @@ module MapBase ...@@ -122,10 +124,10 @@ module MapBase
(* Full clone of the avl module. *) (* Full clone of the avl module. *)
clone avl.AVL as Sel with type selector = selector, clone avl.AVL as Sel with type selector = selector,
predicate selector_correct = selector_correct, predicate selection_possible = selection_possible,
predicate selected = selected, predicate selected = selected,
val selected_way = selected_way, val selected_part = selected_part,
goal selector_correct_empty, goal selection_empty,
constant balancing = balancing, constant balancing = balancing,
goal balancing_positive, goal balancing_positive,
type D.t = D.t, type D.t = D.t,
...@@ -138,14 +140,14 @@ module MapBase ...@@ -138,14 +140,14 @@ module MapBase
function M.m = M.m, function M.m = M.m,
predicate M.c = M.c, predicate M.c = M.c,
constant M.zero = M.zero, constant M.zero = M.zero,
function M.add = M.add, function M.op = M.op,
goal M.assoc, goal M.assoc,
goal M.neutral, goal M.neutral,
function M.sum = M.sum, function M.sum = M.sum,
goal M.sum_def_nil, goal M.sum_def_nil,
goal M.sum_def_cons, goal M.sum_def_cons,
val M.zero = M.zero, val M.zero = M.zero,
val M.add = M.add val M.op = M.op
type t 'a 'b = Sel.t 'a 'b type t 'a 'b = Sel.t 'a 'b
...@@ -300,10 +302,10 @@ module MapBase ...@@ -300,10 +302,10 @@ module MapBase
| Some d -> t.dprm.inv d /\ t.m.card > 0 /\ let dm = t.dprm.mdl d in | Some d -> t.dprm.inv d /\ t.m.card > 0 /\ let dm = t.dprm.mdl d in
CO.eq dm.key k.K.m /\ (forall k2. CO.eq k.K.m k2 -> CO.eq dm.key k.K.m /\ (forall k2. CO.eq k.K.m k2 ->
t.m.func k2 = Some dm) && t.m.func k.K.m = Some dm = t.m.func dm.key } t.m.func k2 = Some dm) && t.m.func k.K.m = Some dm = t.m.func dm.key }
= let r = Sel.default_position () in = let r = Sel.default_split () in
Sel.get r k t Sel.get r k t
let add (d:D.t 'a 'b) (t:t 'a 'b) : t 'a 'b let insert (d:D.t 'a 'b) (t:t 'a 'b) : t 'a 'b
requires { c t /\ t.dprm.inv d } requires { c t /\ t.dprm.inv d }
ensures { c result /\ result.prm = t.prm } ensures { c result /\ result.prm = t.prm }
ensures { let dm = t.dprm.mdl d in ensures { let dm = t.dprm.mdl d in
...@@ -313,9 +315,9 @@ module MapBase ...@@ -313,9 +315,9 @@ module MapBase
(forall k:K.m. (CO.eq k dm.key -> result.m.func k = Some dm) /\ (forall k:K.m. (CO.eq k dm.key -> result.m.func k = Some dm) /\
(not CO.eq k dm.key -> result.m.func k = t.m.func k)) && (not CO.eq k dm.key -> result.m.func k = t.m.func k)) &&
result.m.func dm.key = Some dm } result.m.func dm.key = Some dm }
= let r = Sel.default_position () in = let r = Sel.default_split () in
let k = get_key t.prm d in let k = get_key t.prm d in
Sel.add r k d t Sel.insert r k d t
let remove (k:K.t) (t:t 'a 'b) : t 'a 'b let remove (k:K.t) (t:t 'a 'b) : t 'a 'b
requires { c t /\ K.c k } requires { c t /\ K.c k }
...@@ -326,7 +328,7 @@ module MapBase ...@@ -326,7 +328,7 @@ module MapBase
(forall k2:K.m. (CO.eq k2 k.K.m -> result.m.func k2 = None) /\ (forall k2:K.m. (CO.eq k2 k.K.m -> result.m.func k2 = None) /\
(not CO.eq k2 k.K.m -> result.m.func k2 = t.m.func k2)) && (not CO.eq k2 k.K.m -> result.m.func k2 = t.m.func k2)) &&
result.m.func k.K.m = None } result.m.func k.K.m = None }
= let r = Sel.default_position () in = let r = Sel.default_split () in
Sel.remove r k t Sel.remove r k t
let split (k:K.t) (t:t 'a 'b) : (t 'a 'b,option (D.t 'a 'b),t 'a 'b) let split (k:K.t) (t:t 'a 'b) : (t 'a 'b,option (D.t 'a 'b),t 'a 'b)
...@@ -348,10 +350,12 @@ module MapBase ...@@ -348,10 +350,12 @@ module MapBase
(forall k2:K.m. CO.le k.K.m k2 -> lf.m.func k2 = None) /\ (forall k2:K.m. CO.le k.K.m k2 -> lf.m.func k2 = None) /\
(forall k2:K.m. CO.lt k.K.m k2 -> rg.m.func k2 = t.m.func k2) /\ (forall k2:K.m. CO.lt k.K.m k2 -> rg.m.func k2 = t.m.func k2) /\
(forall k2:K.m. CO.le k2 k.K.m -> rg.m.func k2 = None) } (forall k2:K.m. CO.le k2 k.K.m -> rg.m.func k2 = None) }
= let r = Sel.default_position () in = let r = Sel.default_split () in
Sel.split r k t Sel.split r k t
(* Internal, but makes set-theoretic routines easier. *) (* Extension: set-theoretic-like routines. *)
(* Internal, but makes those routines easier. *)
let view (t:t 'a 'b) : Sel.view 'a 'b let view (t:t 'a 'b) : Sel.view 'a 'b
requires { c t } requires { c t }
...@@ -660,7 +664,8 @@ module Map ...@@ -660,7 +664,8 @@ module Map
t.m.func k.K.m = None && t.m.func k.K.m = None &&
result.m.func k.K.m = Some vm } result.m.func k.K.m = Some vm }
ensures { result.m.card = 1 + t.m.card } ensures { result.m.card = 1 + t.m.card }
= MB.add_min (k,v) t = assert { t.prm.D.mp.mdl (k,v) = (K.m k,t.prm.mdl v) };
MB.add_min (k,v) t
let add_max (t:t 'a 'b) (k:K.t) (v:'a) : t 'a 'b let add_max (t:t 'a 'b) (k:K.t) (v:'a) : t 'a 'b
requires { c t /\ K.c k /\ t.prm.inv v } requires { c t /\ K.c k /\ t.prm.inv v }
...@@ -671,7 +676,8 @@ module Map ...@@ -671,7 +676,8 @@ module Map
(CO.eq k.K.m k2 -> result.m.func k2 = Some vm) /\ (CO.eq k.K.m k2 -> result.m.func k2 = Some vm) /\
(not CO.eq k2 k.K.m -> result.m.func k2 = t.m.func k2) } (not CO.eq k2 k.K.m -> result.m.func k2 = t.m.func k2) }
ensures { result.m.card = 1 + t.m.card } ensures { result.m.card = 1 + t.m.card }
= MB.add_max t (k,v) = assert { t.prm.D.mp.mdl (k,v) = (K.m k,t.prm.mdl v) };
MB.add_max t (k,v)
let concat (l r:t 'a 'b) : t 'a 'b let concat (l r:t 'a 'b) : t 'a 'b
requires { c l /\ c r /\ l.prm = r.prm } requires { c l /\ c r /\ l.prm = r.prm }
...@@ -703,7 +709,7 @@ module Map ...@@ -703,7 +709,7 @@ module Map
| Some (_,v) -> Some v | Some (_,v) -> Some v
end end
let add (k:K.t) (v:'a) (t:t 'a 'b) : t 'a 'b let insert (k:K.t) (v:'a) (t:t 'a 'b) : t 'a 'b
requires { c t /\ K.c k /\ t.prm.inv v } requires { c t /\ K.c k /\ t.prm.inv v }
ensures { c result /\ result.prm = t.prm } ensures { c result /\ result.prm = t.prm }
ensures { let vm = t.prm.mdl v in result.m.card >= t.m.card /\ ensures { let vm = t.prm.mdl v in result.m.card >= t.m.card /\
...@@ -714,7 +720,7 @@ module Map ...@@ -714,7 +720,7 @@ module Map
(not CO.eq k2 k.K.m -> result.m.func k2 = t.m.func k2)) && (not CO.eq k2 k.K.m -> result.m.func k2 = t.m.func k2)) &&
result.m.func k.K.m = Some vm } result.m.func k.K.m = Some vm }
= let d = (k,v) in = let d = (k,v) in
let res = MB.add (k,v) t in let res = MB.insert (k,v) t in
assert { t.MB.dprm.mdl d = (k.K.m,t.prm.mdl v) }; assert { t.MB.dprm.mdl d = (k.K.m,t.prm.mdl v) };
res res
...@@ -922,7 +928,7 @@ module Set ...@@ -922,7 +928,7 @@ module Set
(t.m.set k2 -> result.m.set k2) /\ (t.m.set k2 -> result.m.set k2) /\
(not CO.eq k2 k.K.m -> result.m.set k2 -> t.m.set k2)) && (not CO.eq k2 k.K.m -> result.m.set k2 -> t.m.set k2)) &&
result.m.set k.K.m } result.m.set k.K.m }
= MB.add k t = MB.insert k t
let remove (k:K.t) (t:t) : t let remove (k:K.t) (t:t) : t
requires { c t /\ K.c k } requires { c t /\ K.c k }
...@@ -957,6 +963,8 @@ module Set ...@@ -957,6 +963,8 @@ module Set
match o with None -> false | _ -> true end end in match o with None -> false | _ -> true end end in
(lf,o,rg) (lf,o,rg)
(* Extension: set-theoretic routines. *)
let union (a b:t) : t let union (a b:t) : t
requires { c a /\ c b } requires { c a /\ c b }
ensures { c result } ensures { c result }
......
...@@ -4,10 +4,10 @@ module Monoid ...@@ -4,10 +4,10 @@ module Monoid
type t type t
constant zero : t constant zero : t
function add (a b:t) : t function op (a b:t) : t
axiom assoc : forall a b c:t. add a (add b c) = add (add a b) c axiom assoc : forall a b c:t. op a (op b c) = op (op a b) c
axiom neutral : forall x:t. add x zero = x = add zero x axiom neutral : forall x:t. op x zero = x = op zero x
end end
...@@ -21,10 +21,10 @@ module MonoidList ...@@ -21,10 +21,10 @@ module MonoidList
function sum (f:'a -> t) (l:list 'a) : t function sum (f:'a -> t) (l:list 'a) : t
axiom sum_def_nil : forall f:'a -> t. sum f Nil = zero axiom sum_def_nil : forall f:'a -> t. sum f Nil = zero
axiom sum_def_cons : forall f:'a -> t,x,q. axiom sum_def_cons : forall f:'a -> t,x,q.
sum f (Cons x q) = add (f x) (sum f q) sum f (Cons x q) = op (f x) (sum f q)
let rec lemma sum_append (f:'a -> t) (l r:list 'a) : unit let rec lemma sum_append (f:'a -> t) (l r:list 'a) : unit
ensures { sum f (l ++ r) = add (sum f l) (sum f r) } ensures { sum f (l ++ r) = op (sum f l) (sum f r) }
variant { l } variant { l }
= match l with Cons _ q -> sum_append f q r | _ -> () end = match l with Cons _ q -> sum_append f q r | _ -> () end
...@@ -37,14 +37,14 @@ module MonoidListDef ...@@ -37,14 +37,14 @@ module MonoidListDef
namespace M namespace M
type t type t
constant zero : t constant zero : t
function add (a b:t) : t function op (a b:t) : t
end end
function sum (f:'a -> M.t) (l:list 'a) : M.t = match l with function sum (f:'a -> M.t) (l:list 'a) : M.t = match l with
| Nil -> M.zero | Nil -> M.zero
| Cons x q -> M.add (f x) (sum f q) | Cons x q -> M.op (f x) (sum f q)
end end
clone export MonoidList with type M.t = M.t,constant M.zero = M.zero, clone export MonoidList with type M.t = M.t,constant M.zero = M.zero,
function M.add = M.add,function sum = sum, function M.op = M.op,function sum = sum,
goal sum_def_nil,goal sum_def_cons goal sum_def_nil,goal sum_def_cons
end end
...@@ -58,9 +58,9 @@ module ComputableMonoid ...@@ -58,9 +58,9 @@ module ComputableMonoid
val zero () : t val zero () : t
ensures { c result /\ result.m = zero } ensures { c result /\ result.m = zero }
val add (a b:t) : t val op (a b:t) : t
requires { c a /\ c b } requires { c a /\ c b }
ensures { c result /\ result.m = add a.m b.m } ensures { c result /\ result.m = op a.m b.m }
end end
(* Parameterize program types by their invariants and logical model.
This additional parameterization is rather administrative. *)
module TypeParams module TypeParams
use import HighOrd use import HighOrd
...@@ -18,6 +21,8 @@ module TypeParams ...@@ -18,6 +21,8 @@ module TypeParams
(* For purely logical types. *) (* For purely logical types. *)
constant default_params : type_params 'a 'a constant default_params : type_params 'a 'a
(* Definition axiomatized to avoid a very harmful effect
due to combination of inlining and higher-order. *)
axiom default_params_def : (default_params:type_params 'a 'a) = { axiom default_params_def : (default_params:type_params 'a 'a) = {
inv = \n. true; inv = \n. true;
mdl = \x. x; mdl = \x. x;
......
...@@ -18,17 +18,17 @@ module RAL ...@@ -18,17 +18,17 @@ module RAL
type m = int type m = int
type t = int type t = int
constant zero : int = 0 constant zero : int = 0
function add (x y:int) : int = x + y function op (x y:int) : int = x + y
clone export monoid.Monoid with type t = m, clone export monoid.Monoid with type t = m,
constant zero = zero,function add = add,lemma assoc,lemma neutral constant zero = zero,function op = op,lemma assoc,lemma neutral
clone export monoid.MonoidListDef with type M.t = m, clone export monoid.MonoidListDef with type M.t = m,
constant M.zero = zero,function M.add = add,goal M.assoc,goal M.neutral constant M.zero = zero,function M.op = op,goal M.assoc,goal M.neutral
function m (x:'a) : 'a = x function m (x:'a) : 'a = x
predicate c (_:'a) = true predicate c (_:'a) = true
let zero () : int let zero () : int
ensures { result = 0 } ensures { result = 0 }
= 0 = 0
let add (x y:int) : int let op (x y:int) : int
ensures { result = x + y } ensures { result = x + y }
= x + y = x + y
end end
...@@ -38,9 +38,8 @@ module RAL ...@@ -38,9 +38,8 @@ module RAL
type t 'a 'b = 'a type t 'a 'b = 'a
type m 'b = 'b type m 'b = 'b
function mp (p:'a) : 'a = p function mp (p:'a) : 'a = p
(* Feel shameful, but this is the only way right now that the function (* Axiomatized definition because of a harmful interference between
doesn't get inlined where it should not, which severly mess up automatic inlining and higher-order encoding. *)
with the HO encoding. *)
function measure 'b : int function measure 'b : int
axiom measure_def : forall x:'b. measure x = 1 axiom measure_def : forall x:'b. measure x = 1
let measure (ghost _:'c) (x:'a) : int let measure (ghost _:'c) (x:'a) : int
...@@ -58,32 +57,31 @@ module RAL ...@@ -58,32 +57,31 @@ module RAL
(* Correctness predicate for selector with respect to a list: (* Correctness predicate for selector with respect to a list:
between bounds. *) between bounds. *)
predicate selector_correct (s:selector) (l:list 'b) = predicate selection_possible (s:selector) (l:list 'b) =
0 <= s.index && (if s.hole then s.index <= length l else s.index < length l) 0 <= s.index && (if s.hole then s.index <= length l else s.index < length l)
(* Selection predicate: We are exactly at the index-th position of the (* Selection predicate: We are exactly at the index-th position of the
rebuild list, and there is an element in the middle iff we are rebuild list, and there is an element in the middle iff we are
not trying to select a hole. *) not trying to select a hole. *)
predicate selected (s:selector) (e:position 'b) (l:list 'b) = predicate selected (s:selector) (e:split 'b) (l:list 'b) =
s.index = length e.left /\ (s.hole <-> e.middle = None) s.index = length e.left /\ (s.hole <-> e.middle = None)
let selected_way (ghost p:type_params 'a 'b) let selected_part (ghost p:type_params 'a 'b)
(ghost base:list 'b) (ghost base:list 'b)
(ghost llis:list 'b) (ghost llis:list 'b)
(ghost rlis:list 'b) (ghost rlis:list 'b)
(s:selector) (sl:int) (d:'a) (sr:int) : way_base selector (s:selector) (sl:int) (d:'a) (sr:int) : part_base selector
requires { p.inv d } requires { p.inv d }
requires { base = llis ++ Cons (p.mdl d) rlis } requires { base = llis ++ Cons (p.mdl d) rlis }
requires { selector_correct s base } requires { selection_possible s base }
requires { sl = length llis /\ sr = length rlis } requires { sl = length llis /\ sr = length rlis }
(* A selected position can be found by following the given way. *)
returns { Here -> let e2 = { left = llis; returns { Here -> let e2 = { left = llis;
middle = Some (p.mdl d); middle = Some (p.mdl d);
right = rlis } in selected s e2 base right = rlis } in selected s e2 base
| Left sl -> selector_correct sl llis /\ | Left sl -> selection_possible sl llis /\
forall e. selected sl e llis -> forall e. selected sl e llis ->
selected s (right_extend e (p.mdl d) rlis) base selected s (right_extend e (p.mdl d) rlis) base
| Right sr -> selector_correct sr rlis /\ | Right sr -> selection_possible sr rlis /\
forall e. selected sr e rlis -> forall e. selected sr e rlis ->
selected s (left_extend llis (p.mdl d) e) base } selected s (left_extend llis (p.mdl d) e) base }
= (* Use the size information to decide = (* Use the size information to decide
...@@ -99,10 +97,10 @@ module RAL ...@@ -99,10 +97,10 @@ module RAL
(* Full clone of the avl module. *) (* Full clone of the avl module. *)
clone avl.AVL as Sel with type selector = selector, clone avl.AVL as Sel with type selector = selector,
predicate selector_correct = selector_correct, predicate selection_possible = selection_possible,
predicate selected = selected, predicate selected = selected,
val selected_way = selected_way, val selected_part = selected_part,
goal selector_correct_empty, goal selection_empty,
constant balancing = balancing, constant balancing = balancing,
goal balancing_positive, goal balancing_positive,
type D.t = D.t, type D.t = D.t,
...@@ -115,14 +113,14 @@ module RAL ...@@ -115,14 +113,14 @@ module RAL
function M.m = M.m, function M.m = M.m,
predicate M.c = M.c, predicate M.c = M.c,
constant M.zero = M.zero, constant M.zero = M.zero,
function M.add = M.add, function M.op = M.op,
goal M.assoc, goal M.assoc,
goal M.neutral, goal M.neutral,
function M.sum = M.sum, function M.sum = M.sum,
goal M.sum_def_nil, goal M.sum_def_nil,
goal M.sum_def_cons, goal M.sum_def_cons,
val M.zero = M.zero, val M.zero = M.zero,
val M.add = M.add val M.op = M.op
type t 'a 'b = Sel.t 'a 'b type t 'a 'b = Sel.t 'a 'b
(* There should be no need to talk about the height anymore, (* There should be no need to talk about the height anymore,
...@@ -220,8 +218,8 @@ module RAL ...@@ -220,8 +218,8 @@ module RAL
ensures { length result.m = length l.m } ensures { length result.m = length l.m }
ensures { forall i:int. i <> n -> nth i result.m = nth i l.m } ensures { forall i:int. i <> n -> nth i result.m = nth i l.m }
ensures { nth n result.m = Some (l.prm.mdl d) } ensures { nth n result.m = Some (l.prm.mdl d) }
= let ghost r = Sel.default_position () in = let ghost r = Sel.default_split () in
Sel.add r { index = n; hole = false } d l Sel.insert r { index = n; hole = false } d l
(* Get the n-th element. *) (* Get the n-th element. *)
let get (n:int) (l:t 'a 'b) : 'a let get (n:int) (l:t 'a 'b) : 'a
...@@ -229,7 +227,7 @@ module RAL ...@@ -229,7 +227,7 @@ module RAL
ensures { match nth n l.m with None -> false ensures { match nth n l.m with None -> false
| Some d -> d = l.prm.mdl result end } | Some d -> d = l.prm.mdl result end }
ensures { l.prm.inv result } ensures { l.prm.inv result }
= let ghost r = Sel.default_position () in = let ghost r = Sel.default_split () in
match Sel.get r { index = n; hole = false } l with match Sel.get r { index = n; hole = false } l with
| None -> absurd | None -> absurd
| Some d -> d | Some d -> d
...@@ -245,8 +243,8 @@ module RAL ...@@ -245,8 +243,8 @@ module RAL
ensures { forall i:int. i < n -> nth i result.m = nth i l.m } ensures { forall i:int. i < n -> nth i result.m = nth i l.m }
ensures { forall i:int. i > n -> nth i result.m = nth (i-1) l.m } ensures { forall i:int. i > n -> nth i result.m = nth (i-1) l.m }
ensures { nth n result.m = Some (l.prm.mdl d) } ensures { nth n result.m = Some (l.prm.mdl d) }
= let ghost r = Sel.default_position () in = let ghost r = Sel.default_split () in
Sel.add r { index = n; hole = true } d l Sel.insert r { index = n; hole = true } d l
let remove (n:int) (l:t 'a 'b) : t 'a 'b let remove (n:int) (l:t 'a 'b) : t 'a 'b
requires { 0 <= n < length l.m } requires { 0 <= n < length l.m }
...@@ -255,7 +253,7 @@ module RAL ...@@ -255,7 +253,7 @@ module RAL
ensures { length result.m = length l.m - 1 } ensures { length result.m = length l.m - 1 }
ensures { forall i:int. i < n -> nth i result.m = nth i l.m } ensures { forall i:int. i < n -> nth i result.m = nth i l.m }
ensures { forall i:int. i >= n -> nth i result.m = nth (i+1) l.m } ensures { forall i:int. i >= n -> nth i result.m = nth (i+1) l.m }
= let ghost r = Sel.default_position () in = let ghost r = Sel.default_split () in
Sel.remove r { index = n; hole = false } l Sel.remove r { index = n; hole = false } l
(* Cut the list between the (n-1)-th and n-th elements. *) (* Cut the list between the (n-1)-th and n-th elements. *)
...@@ -263,7 +261,7 @@ module RAL ...@@ -263,7 +261,7 @@ module RAL
requires { 0 <= n <= length l.m /\ c l } requires { 0 <= n <= length l.m /\ c l }
returns { (lf,rg) -> l.m = lf.m ++ rg.m /\ returns { (lf,rg) -> l.m = lf.m ++ rg.m /\
c lf /\ c rg /\ lf.prm = l.prm = rg.prm } c lf /\ c rg /\ lf.prm = l.prm = rg.prm }
= let ghost r = Sel.default_position () in = let ghost r = Sel.default_split () in
let sel = { index = n; hole = true } in let sel = { index = n; hole = true } in
let (lf,_,rg) = Sel.split r sel l in let (lf,_,rg) = Sel.split r sel l in
(lf,rg) (lf,rg)
...@@ -273,7 +271,7 @@ module RAL ...@@ -273,7 +271,7 @@ module RAL
requires { 0 <= n < length l.m /\ c l } requires { 0 <= n < length l.m /\ c l }
returns { (lf,md,rg) -> l.m = lf.m ++ Cons (l.prm.mdl md) rg.m /\ returns { (lf,md,rg) -> l.m = lf.m ++ Cons (l.prm.mdl md) rg.m /\
c lf /\ c rg /\ l.prm.inv md /\ lf.prm = l.prm = rg.prm } c lf /\ c rg /\ l.prm.inv md /\ lf.prm = l.prm = rg.prm }
= let ghost r = Sel.default_position () in = let ghost r = Sel.default_split () in
let sel = { index = n; hole = false } in let sel = { index = n; hole = false } in
let (lf,md,rg) = Sel.split r sel l in let (lf,md,rg) = Sel.split r sel l in
match md with None -> absurd | Some md -> (lf,md,rg) end match md with None -> absurd | Some md -> (lf,md,rg) end
......
...@@ -9,20 +9,20 @@ theory Base ...@@ -9,20 +9,20 @@ theory Base
clone import key_type.KeyType as K clone import key_type.KeyType as K
clone import relations.Transitive as O with type t = key clone import relations.Transitive as O with type t = key
predicate minorate (x:key) (l:list (t 'a)) = predicate lower_bound (x:key) (l:list (t 'a)) =
(forall y. mem y l -> rel x y.key) (forall y. mem y l -> rel x y.key)
predicate majorate (x:key) (l:list (t 'a)) =