Skip to content
Snippets Groups Projects
Commit 08afcef7 authored by François Bobot's avatar François Bobot
Browse files

Add interval first part

parent c4bf7062
No related branches found
No related tags found
1 merge request!20Better reccursive function handling
Expand all Hide whitespace changes
Inline Side-by-side
src_common/union.mlw
+ 341
− 2
View file @ 08afcef7
...@@ -64,7 +64,7 @@ module Union ...@@ -64,7 +64,7 @@ module Union
length_off l length_off l
end end
predicate lt_bound_on (x:Q.t) (l:on) = predicate lt_bound_on (x:real) (l:on) =
match l with match l with
| OnSin q l -> | OnSin q l ->
x <. q /\ lt_bound_on x l x <. q /\ lt_bound_on x l
...@@ -73,7 +73,7 @@ module Union ...@@ -73,7 +73,7 @@ module Union
| OnInf -> true | OnInf -> true
end end
with lt_bound_off (x:Q.t) (l:off) = with lt_bound_off (x:real) (l:off) =
match l with match l with
| OffSin q l -> | OffSin q l ->
x <. q /\ lt_bound_off x l x <. q /\ lt_bound_off x l
...@@ -781,5 +781,344 @@ module Union ...@@ -781,5 +781,344 @@ module Union
end end
let add_cst l x
ensures {
forall q. (mem q l.a) <-> mem (q+.x) result.a
}
=
let rec add_cst_on (x:Q.t) (l:on) : on
requires { ordered_on l }
ensures { ordered_on result }
ensures { forall q. (lt_bound_on q l) -> (lt_bound_on (q+.x) result) }
ensures { forall q. (mem_on q l) <-> mem_on (q+.x) result }
variant { length_on l }
=
match l with
| OnSin q l' -> OnSin Q.(q+x) (add_cst_on x l')
| OnEnd q bv l' ->
lt_bound_is_not_mem_off q l';
OnEnd Q.(q+x) bv (add_cst_off x l')
| OnInf -> OnInf
end
with add_cst_off (x:Q.t) (l:off)
requires { ordered_off l }
ensures { ordered_off result }
ensures { forall q. (lt_bound_off q l) -> (lt_bound_off (q+.x) result) }
ensures { forall q. (mem_off q l) <-> mem_off (q+.x) result }
variant { length_off l }
=
match l with
| OffSin q l' ->
lt_bound_is_not_mem_off q l';
OffSin Q.(q+x) (add_cst_off x l')
| OffEnd q b l' -> OffEnd Q.(q+x) b (add_cst_on x l')
| OffInf -> OffInf
end
in
match l.a with
| On l ->
{ a = On (add_cst_on x l) }
| Off l_off ->
let v = not_bottom l in
let l = (add_cst_off x l_off) in
assert { mem_off (v+.x) l };
{ a = Off l }
end
let function add_bound b1 b2 =
match b1, b2 with
| Large, Large -> Large
| Large, Strict -> Strict
| Strict, Large -> Strict
| Strict, Strict -> Strict
end
let ghost function lt_bound_on_give_space (q:real) (l:on) : real
requires { lt_bound_on q l }
ensures { q <. result }
ensures { forall q'. q' <. result -> mem_on q' l } =
match l with
| OnSin q _ -> Q.real q
| OnEnd q _ _ -> Q.real q
| OnInf -> q +. 1.0
end
use real.MinMax
let add_interval l (bu:Bound.t) (u:Q.t) (v:Q.t) (bv:Bound.t): (result:t',ghost fq':real -> real)
requires { Q.(u < v) }
ensures {
forall q q'. (mem q l.a /\ cmp u bu q' /\ cmp q' bv v) -> mem (q+.q') result.a
}
ensures {
forall q. mem q result.a -> (mem (fq' q) l.a /\ cmp u bu (q-.(fq' q)) /\ cmp (q-.(fq' q)) bv v)
}
=
let rec add_interval_on (bu:Bound.t) (u:Q.t) (v:Q.t) (bv:Bound.t) (l:on) : (result:on,ghost fq':real -> real)
requires { Q.(u < v) }
requires { ordered_on l }
ensures { ordered_on result }
ensures { forall q. (lt_bound_on q l) -> (lt_bound_on (q+.u) result) }
ensures { forall q q'. (mem_on q l /\ cmp u bu q' /\ cmp q' bv v) -> mem_on (q+.q') result }
ensures { forall q. mem_on q result -> (mem_on (fq' q) l /\ cmp u bu (q-.(fq' q)) /\ cmp (q-.(fq' q)) bv v) }
variant { length_on l }
=
match l with
| OnSin qs l' ->
assert { forall q'. mem_on q' l -> mem_on q' l'};
let res,fq' = add_interval_on bu u v bv l' in
let ghost space_right = lt_bound_on_give_space (Q.real qs) l' in
let ghost fq'' (q:real)
ensures { mem_on q res -> (mem_on result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v) }
=
let q' = fq' q in
if pure { q' = Q.real qs } then
if pure { (q-.q') = v } then
if pure { (space_right-.qs) <. (v-.u) } then
pure { qs +. ((space_right-.qs)*.0.5) }
else
pure {qs +. ((v-.u) *.0.5) }
else
pure { q' -. (v -. (q-.q'))*.0.5 }
else q'
in
(res,fq'')
| OnEnd qs bq l' ->
lt_bound_is_not_mem_off qs l';
let br = add_bound bq bv in
let r = Q.(qs+v) in
let res, fq = add_interval_off_remain bu u v bv r br l' in
let ghost fq' (q:real) : real
ensures { mem_on q res -> (mem_on result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v) }
=
if pure { cmp q br r }
then if pure { q = qs+.v } then Q.real qs
else if pure { q <. qs+.v*.0.5+.u*.0.5 } then pure { q -. (v*.0.5+.u*.0.5)} else let d = Q.real qs+.Q.real v-.q in Q.real qs -. d*.0.5
else fq q
in
res, fq'
| OnInf -> (OnInf,ghost fun q -> q-.Q.real u*.0.5-.Q.real v*.0.5)
end
with add_interval_off (bu:Bound.t) (u:Q.t) (v:Q.t) (bv:Bound.t) (l:off) : (result:off,ghost fq':real -> real)
requires { Q.(u < v) }
requires { ordered_off l }
ensures { ordered_off result }
ensures { forall q. (lt_bound_off q l) -> (lt_bound_off (q+.u) result) }
ensures { forall q q'. (mem_off q l /\ cmp u bu q' /\ cmp q' bv v) -> mem_off (q+.q') result }
ensures { forall q. mem_off q result -> (mem_off (fq' q) l /\ cmp u bu (q-.(fq' q)) /\ cmp (q-.(fq' q)) bv v) }
variant { length_off l }
=
match l with
| OffSin qs l' ->
lt_bound_is_not_mem_off qs l';
let r = Q.(qs+v) in
let res, fq = (add_interval_off_remain bu u v bv r bv l') in
let res = OffEnd Q.(qs+u) bu res in
let ghost function fq' (q:real) : real
ensures { mem_off q res -> (mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v) }
=
if pure { cmp q bv r }
then pure { Q.real qs }
else fq q
in
res, fq'
| OffEnd qs b l' ->
let bbu = add_bound b bu in
let ghost space_right = lt_bound_on_give_space (Q.real qs) l' in
let res0, fq = (add_interval_on bu u v bv l') in
let res = OffEnd Q.(qs+u) bbu res0 in
let ghost function fq' (q:real) : real
ensures { mem_off q res -> (mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v) }
=
if pure { cmp qs b (fq q) } then fq q else begin
if pure { q = (qs+.u) } then Q.real qs
else
let p = pure { min (qs*.0.5+.space_right*.0.5) (qs+.(v-.u)) } in
if pure { q-.p <=. u } then pure { qs*.0.5+.(q-.u)*.0.5 } else p
end
in
res, fq'
| OffInf -> OffInf, (ghost fun _ -> 0.)
end
with add_interval_off_remain (bu:Bound.t) (u:Q.t) (v:Q.t) (bv:Bound.t) (r:Q.t) (br:Bound.t) (l:off) : (result:on,ghost fq':real -> real)
requires { Q.(u < v) }
requires { lt_bound_off (r-.v) l }
requires { br = Large -> bv = Large }
requires { ordered_off l }
ensures { ordered_on result }
ensures { forall q. (lt_bound_off q l) -> (q+.u <. r) -> (lt_bound_on (q+.u) result) }
ensures { forall q q'. (mem_off q l /\ cmp u bu q' /\ cmp q' bv v) -> mem_on (q+.q') result }
ensures { forall q. cmp q br r -> mem_on q result }
ensures { forall q. mem_on q result ->
((mem_off (fq' q) l /\ cmp u bu (q-.(fq' q)) /\ cmp (q-.(fq' q)) bv v)
\/ cmp q br r) }
variant { length_off l }
=
match l with
| OffSin qs l' ->
lt_bound_is_not_mem_off qs l';
let qu = Q.(qs+u) in
match Q.compare r qu with
| Ord.Lt ->
smaller_lt_bound_off Q.(r-u) qs l';
let r' = Q.(qs+v) in
let res, fq = (add_interval_off_remain bu u v bv r' bv l') in
let res = OnEnd r br (OffEnd qu bu res) in
let ghost fq' (q:real)
ensures { mem_on q res -> ((mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v)
\/ cmp q br r) }
=
if pure { cmp qu bu q } then
if pure { cmp q bv r' } then Q.real qs else (fq q)
else 0.
in
res, fq'
| Ord.Gt ->
let r' = Q.(qs+v) in
let res, fq = add_interval_off_remain bu u v bv r' bv l' in
let ghost fq' (q:real)
ensures { mem_on q res -> ((mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v)
\/ cmp q br r) }
=
if pure { cmp qu bu q } then
if pure { cmp q bv r' } then Q.real qs else (fq q)
else 0.
in
res, fq'
| Ord.Eq ->
match br, bu with
| Strict, Strict ->
let r' = Q.(qs+v) in
let res, fq = (add_interval_off_remain bu u v bv r' bv l') in
let res = OnSin qu res in
let ghost fq' (q:real)
ensures { mem_on q res -> ((mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v)
\/ cmp q br r) }
=
if pure { cmp qu bu q } then
if pure { cmp q bv r' } then Q.real qs else (fq q)
else 0.
in
res, fq'
| _ ->
let r' = Q.(qs+v) in
let res, fq = (add_interval_off_remain bu u v bv r' bv l') in
let res = res in
let ghost fq' (q:real)
ensures { mem_on q res -> ((mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v)
\/ cmp q br r) }
=
if pure { cmp qu bu q } then
if pure { cmp q bv r' } then Q.real qs else (fq q)
else 0.
in
res, fq'
end
end
| OffEnd qs b l' ->
let qu = Q.(qs+u) in
let bbu = add_bound b bu in
let ghost space_right = lt_bound_on_give_space (Q.real qs) l' in
match Q.compare r qu with
| Ord.Lt ->
smaller_lt_bound_on Q.(r-u) qs l';
let res, fq = (add_interval_on bu u v bv l') in
let res = OnEnd r br (OffEnd qu bbu res) in
let ghost fq' (q:real) : real
ensures { mem_on q res -> ((mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v)
\/ cmp q br r) }
=
if pure { cmp qu bu q } then
if pure { cmp qs b (fq q) } then fq q else begin
if pure { q = qu } then Q.real qs
else
let p = pure { min (qs*.0.5+.space_right*.0.5) (qs+.(v-.u)) } in
if pure { q-.p <=. u } then pure { qs*.0.5+.(q-.u)*.0.5 } else p
end
else 0.
in
res, fq'
| Ord.Gt ->
let res, fq = add_interval_on bu u v bv l' in
let ghost fq' (q:real)
ensures { mem_on q res -> ((mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v)
\/ cmp q br r) }
=
if pure { cmp qu bu q } then
if pure { cmp qs b (fq q) } then fq q else begin
if pure { q = qu } then Q.real qs
else
let p = pure { min (qs*.0.5+.space_right*.0.5) (qs+.(v-.u)) } in
if pure { q-.p <=. u } then pure { qs*.0.5+.(q-.u)*.0.5 } else p
end
else 0.
in
(* assert { forall mem_on (r-.v) l'};
assert { mem_on r res}; *)
let ghost p = pure { 0.5 *. min (qs-.(r-.v)) (v-.u) } in
assert { forall q. cmp q br r -> cmp (q-.v+.p) b qs };
assert { forall q. cmp q br r -> (mem_on (q-.(v-.p)) l' /\ cmp u bu (v-.p) /\ cmp (v-.p) bv v) };
assert { forall q. cmp q br r -> mem_on ((q-.(v-.p))+.(v-.p)) res };
assert { forall q. cmp q br r -> mem_on q res };
res, fq'
| Ord.Eq ->
match br, bbu with
| Strict, Strict ->
let res, fq = (add_interval_on bu u v bv l') in
let res = OnSin qu res in
let ghost fq' (q:real)
ensures { mem_on q res -> ((mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v)
\/ cmp q br r) }
=
if pure { cmp qu bu q } then
if pure { cmp qs b (fq q) } then fq q else begin
if pure { q = qu } then Q.real qs
else
let p = pure { min (qs*.0.5+.space_right*.0.5) (qs+.(v-.u)) } in
if pure { q-.p <=. u } then pure { qs*.0.5+.(q-.u)*.0.5 } else p
end
else 0.
in
res, fq'
| _ ->
let res, fq = (add_interval_on bu u v bv l') in
let res = res in
let ghost fq' (q:real)
ensures { mem_on q res -> ((mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v)
\/ cmp q br r) }
=
if pure { cmp qu bu q } then
if pure { cmp qs b (fq q) } then fq q else begin
if pure { q = qu } then Q.real qs
else
let p = pure { min (qs*.0.5+.space_right*.0.5) (qs+.(v-.u)) } in
if pure { q-.p <=. u } then pure { qs*.0.5+.(q-.u)*.0.5 } else p
end
else 0.
in
res, fq'
end
end
| OffInf -> OnEnd r br OffInf,(ghost fun _ -> 0.)
end
in
match l.a with
| On l ->
let res, fq = add_interval_on bu u v bv l in
{ a = On res }, fq
| Off l_off ->
let w = not_bottom l in
let l, fq = (add_interval_off bu u v bv l_off) in
assert { mem_off (w+.(u*.0.5+.v*.0.5)) l };
{ a = Off l }, fq
end
end end
src_common/union/why3session.xml
+ 989
− 48
View file @ 08afcef7
This diff is collapsed.
src_common/union__Union.ml
+ 103
− 0
View file @ 08afcef7
...@@ -434,3 +434,106 @@ let except (l: t') (x: Q.t) : t' option = ...@@ -434,3 +434,106 @@ let except (l: t') (x: Q.t) : t' option =
| l' -> Some (Off l') | l' -> Some (Off l')
end end
let add_cst (l: t') (x: Q.t) : t' =
let rec add_cst_on (x1: Q.t) (l1: on) : on =
match l1 with
| OnSin (q, l') -> OnSin ((Q.(+) q x1), add_cst_on x1 l')
| OnEnd (q, bv, l') -> OnEnd ((Q.(+) q x1), bv, add_cst_off x1 l')
| OnInf -> OnInf
and add_cst_off (x1: Q.t) (l1: off) : off =
match l1 with
| OffSin (q, l') -> OffSin ((Q.(+) q x1), add_cst_off x1 l')
| OffEnd (q, b, l') -> OffEnd ((Q.(+) q x1), b, add_cst_on x1 l')
| OffInf -> OffInf in
match l with
| On l1 -> On (add_cst_on x l1)
| Off l_off -> (let l1 = add_cst_off x l_off in Off l1)
let add_bound (b1: Interval__Bound.t) (b2: Interval__Bound.t) :
Interval__Bound.t =
match (b1, b2) with
| (Interval__Bound.Large, Interval__Bound.Large) -> Interval__Bound.Large
| (Interval__Bound.Large, Interval__Bound.Strict) -> Interval__Bound.Strict
| (Interval__Bound.Strict, Interval__Bound.Large) -> Interval__Bound.Strict
| (Interval__Bound.Strict,
Interval__Bound.Strict) ->
Interval__Bound.Strict
let add_interval (l: t') (bu: Interval__Bound.t) (u: Q.t) (v: Q.t)
(bv: Interval__Bound.t) : t' =
let rec add_interval_on (bu1: Interval__Bound.t) (u1: Q.t) (v1: Q.t)
(bv1: Interval__Bound.t) (l1: on) : on =
match l1 with
| OnSin (qs, l') -> (let res = add_interval_on bu1 u1 v1 bv1 l' in res)
| OnEnd (qs,
bq,
l') ->
(let br = add_bound bq bv1 in let r = (Q.(+) qs v1) in
let res = add_interval_off_remain bu1 u1 v1 bv1 r br l' in res)
| OnInf -> OnInf
and add_interval_off (bu1: Interval__Bound.t) (u6: Q.t) (v6: Q.t)
(bv1: Interval__Bound.t) (l1: off) : off =
match l1 with
| OffSin (qs,
l') ->
(let r = (Q.(+) qs v6) in
let res = add_interval_off_remain bu1 u6 v6 bv1 r bv1 l' in
let res1 = OffEnd ((Q.(+) qs u6), bu1, res) in res1)
| OffEnd (qs,
b,
l') ->
(let bbu = add_bound b bu1 in
let res0 = add_interval_on bu1 u6 v6 bv1 l' in
let res = OffEnd ((Q.(+) qs u6), bbu, res0) in res)
| OffInf -> OffInf
and add_interval_off_remain (bu1: Interval__Bound.t) (u10: Q.t) (v10: Q.t)
(bv1: Interval__Bound.t) (r: Q.t)
(br: Interval__Bound.t) (l1: off) : on =
match l1 with
| OffSin (qs,
l') ->
(let qu = (Q.(+) qs u10) in
match (Q_extra.compare r qu) with
| Ord.Lt ->
(let r' = (Q.(+) qs v10) in
let res = add_interval_off_remain bu1 u10 v10 bv1 r' bv1 l' in
let res1 = OnEnd (r, br, OffEnd (qu, bu1, res)) in res1)
| Ord.Gt ->
(let r' = (Q.(+) qs v10) in
let res = add_interval_off_remain bu1 u10 v10 bv1 r' bv1 l' in res)
| Ord.Eq ->
begin match (br, bu1) with
| (Interval__Bound.Strict,
Interval__Bound.Strict) ->
(let r' = (Q.(+) qs v10) in
let res = add_interval_off_remain bu1 u10 v10 bv1 r' bv1 l' in
let res1 = OnSin (qu, res) in res1)
| _ ->
(let r' = (Q.(+) qs v10) in
let res = add_interval_off_remain bu1 u10 v10 bv1 r' bv1 l' in
let res1 = res in res1)
end)
| OffEnd (qs,
b,
l') ->
(let qu = (Q.(+) qs u10) in let bbu = add_bound b bu1 in
match (Q_extra.compare r qu) with
| Ord.Lt ->
(let res = add_interval_on bu1 u10 v10 bv1 l' in
let res1 = OnEnd (r, br, OffEnd (qu, bbu, res)) in res1)
| Ord.Gt -> (let res = add_interval_on bu1 u10 v10 bv1 l' in res)
| Ord.Eq ->
begin match (br, bbu) with
| (Interval__Bound.Strict,
Interval__Bound.Strict) ->
(let res = add_interval_on bu1 u10 v10 bv1 l' in
let res1 = OnSin (qu, res) in res1)
| _ ->
(let res = add_interval_on bu1 u10 v10 bv1 l' in let res1 = res in
res1)
end)
| OffInf -> OnEnd (r, br, OffInf) in
match l with
| On l1 -> (let res = add_interval_on bu u v bv l1 in On res)
| Off l_off -> (let l1 = add_interval_off bu u v bv l_off in Off l1)
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment