Commit c78bbf45 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Give a default ordering to range types (fix issue #56).

parent 72d90c94
......@@ -47,7 +47,7 @@ module VonNeumann16
let ghost bits_g = ref (0x80:t) in (* 2^{m-1} *)
let ghost res_g = ref (0:t) in (* res / 2^m *)
while not (eq !bits (0:t)) do
variant { t'int !bits }
variant { !bits }
(* 0 <= m <= 8 *)
invariant { ule !m (8:t) }
(* bits_g = 2^{m-1} ou 0 si m=0 *)
......@@ -94,11 +94,9 @@ module VonNeumann16
done;
!res
end
module VonNeumann32
use ref.Ref
......@@ -123,7 +121,7 @@ module VonNeumann32
let ghost bits_g = ref (0x8000:t) in (* 2^{m-1} *)
let ghost res_g = ref (0:t) in (* res / 2^m *)
while not (eq !bits (0:t)) do
variant { t'int !bits }
variant { !bits }
(* 0 <= m <= 16 *)
invariant { ule !m (16:t) }
(* bits_g = 2^{m-1} ou 0 si m=0 *)
......@@ -170,7 +168,6 @@ module VonNeumann32
done;
!res
end
......@@ -198,7 +195,7 @@ module VonNeumann64
let ghost bits_g = ref (0x8000_0000:t) in (* 2^{m-1} *)
let ghost res_g = ref (0:t) in (* res / 2^m *)
while not (eq !bits (0:t)) do
variant { t'int !bits }
variant { !bits }
(* 0 <= m <= 32 *)
invariant { ule !m (32:t) }
(* bits_g = 2^{m-1} or 0 if m=0 *)
......@@ -247,5 +244,4 @@ module VonNeumann64
assert { !bits = (0:t) };
!res
end
......@@ -371,14 +371,7 @@
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.58"/></proof>
</goal>
<goal name="VC isqrt64.19" expl="loop variant decrease" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC isqrt64.19.0" expl="VC for isqrt64" proved="true">
<proof prover="3"><result status="valid" time="0.43"/></proof>
</goal>
<goal name="VC isqrt64.19.1" expl="VC for isqrt64" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.17"/></proof>
</goal>
</transf>
<proof prover="3" timelimit="5"><result status="valid" time="1.01"/></proof>
</goal>
<goal name="VC isqrt64.20" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.36"/></proof>
......@@ -426,14 +419,7 @@
<proof prover="3"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="VC isqrt64.30" expl="loop variant decrease" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC isqrt64.30.0" expl="VC for isqrt64" proved="true">
<proof prover="3"><result status="valid" time="0.42"/></proof>
</goal>
<goal name="VC isqrt64.30.1" expl="VC for isqrt64" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.22"/></proof>
</goal>
</transf>
<proof prover="3" timelimit="5"><result status="valid" time="1.00"/></proof>
</goal>
<goal name="VC isqrt64.31" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.45"/></proof>
......
......@@ -23,7 +23,7 @@ module Compare
let i = ref sz in
try
while Int32.(>=) !i (Int32.of_int 1) do
variant { p2i !i }
variant { !i }
invariant { 0 <= !i <= sz }
invariant { forall j. !i <= j < sz ->
(pelts x)[x.offset+j] = (pelts y)[y.offset+j] }
......
......@@ -137,7 +137,7 @@ module Logical
let l, retval = lsld_ext !low cnt in
high := l;
while (Int32.(>) !i zero) do
variant { p2i !i }
variant { !i }
invariant { 0 <= !i < sz }
invariant { radix * value_sub (pelts r) (r.offset + 1 + !i) (r.offset + sz)
+ (power radix (sz - !i)) * retval + !high
......@@ -359,7 +359,7 @@ module Logical
high := l;
let ghost c = power 2 (l2i cnt) in
while (Int32.(>) !i 0) do
variant { p2i !i }
variant { !i }
invariant { 0 <= !i < sz }
invariant { radix * value_sub (pelts x) (x.offset + !i + 1) (x.offset + sz)
+ (power radix (sz - !i)) * retval + !high
......
......@@ -122,6 +122,12 @@ let mk_env env kn tuc =
let th_wf = Env.read_theory env ["relations"] "WellFounded" in
mk_env th_int th_wf kn tuc
let int_of_range env ty =
let td = Mts.find ty env.ts_ranges in
match td.Theory.td_node with
| Theory.Meta (_, [_; Theory.MAls s]) -> s
| _ -> assert false
(* explanation attributes *)
let expl_pre = Ident.create_attribute "expl:precondition"
......@@ -256,9 +262,18 @@ let decrease_alg env loc old_t t =
t_case old_t (List.map add_cs csl)
let decrease_def env loc old_t t =
if ty_equal (t_type old_t) ty_int && ty_equal (t_type t) ty_int
then t_and (ps_app env.ps_int_le [t_nat_const 0; old_t])
(ps_app env.ps_int_lt [t; old_t])
let ty = t_type t in
if ty_equal (t_type old_t) ty then
match ty.ty_node with
| Tyapp (ts,_) when ts_equal ts ts_int ->
t_and (ps_app env.ps_int_le [t_nat_const 0; old_t])
(ps_app env.ps_int_lt [t; old_t])
| Tyapp (ts, _) when is_range_type_def ts.ts_def ->
let ls = int_of_range env ts in
let proj t = fs_app ls [t] ty_int in
ps_app env.ps_int_lt [proj t; proj old_t]
| _ ->
decrease_alg env loc old_t t
else decrease_alg env loc old_t t
let decrease env loc attrs expl olds news =
......@@ -840,10 +855,7 @@ let rec k_expr env lps e res xmap =
| Tyapp (s,_) when ts_equal s ts_int ->
fun v -> t_var v.pv_vs
| Tyapp (s,_) ->
let td = Mts.find s env.ts_ranges in
let s = match td.Theory.td_node with
| Theory.Meta (_, [_; Theory.MAls s]) -> s
| _ -> assert false (* never *) in
let s = int_of_range env s in
fun v -> fs_app s [t_var v.pv_vs] ty_int
| Tyvar _ -> assert false (* never *) in
let a = int_of_pv a and i = t_var vi.pv_vs in
......
Markdown is supported
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