Commit 0c0c5860 authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'master' into feature/const_in_separate_theory

Conflicts:
	examples/warshall_algorithm/why3session.xml
	examples/warshall_algorithm/why3shapes.gz
	modules/matrix.mlw
parents 3496a127 4e8fef7e
......@@ -129,7 +129,7 @@ theory matrix.Matrix
syntax type matrix "(matrix %1)"
syntax function get "(matrix_get %1 %2)"
syntax function get "(matrix_get %1 %2 %3)"
syntax function rows "(nrows %1 : int)"
syntax function columns "(ncols %1 : int)"
syntax function elts "(matrix_get_curry %1)"
......
(** OCaml driver with Why3 type int being mapped to OCaml type int.
This is of course unsafe, yet useful to run your code is you
have an independant argument regarding the absence of arithmetic
This is of course unsafe, yet useful to run your code when you
have an independent argument for the absence of arithmetic
overflows. *)
printer "ocaml"
printer "ocaml-unsafe-int"
theory BuiltIn
syntax type int "int"
(* meta "ocaml arithmetic" "unsafe int" *)
syntax predicate (=) "(%1 = %2)"
end
......@@ -127,6 +126,23 @@ module array.Array
syntax val blit "Array.blit"
end
module matrix.Matrix
syntax type matrix "(%1 array array)"
syntax exception OutOfBounds "(Invalid_argument \"index out of bounds\")"
syntax function rows "(Array.length %1)"
syntax function columns "(Array.length %1.(0))"
syntax val rows "Array.length"
syntax val columns "(fun m -> Array.length m.(0))"
syntax val get "(fun m (i,j) -> m.(i).(j))"
syntax val set "(fun m (i,j) v -> m.(i).(j) <- v)"
syntax val defensive_get "(fun m (i,j) -> m.(i).(j))"
syntax val defensive_set "(fun m (i,j) v -> m.(i).(j) <- v)"
syntax val make "Array.make_matrix"
syntax val copy "(Array.map Array.copy)"
end
module mach.int.Int31
syntax val of_int "(fun x -> x)"
syntax converter of_int "%1"
......@@ -147,6 +163,26 @@ module mach.int.Int31
syntax val (>=) "(>=)"
syntax val (>) "(>)"
end
module mach.int.Int63
syntax val of_int "(fun x -> x)"
syntax converter of_int "%1"
syntax function to_int "(%1)"
syntax type int63 "int"
syntax val ( + ) "( + )"
syntax val ( - ) "( - )"
syntax val (-_) "( ~- )"
syntax val ( * ) "( * )"
syntax val ( / ) "( / )"
syntax val ( % ) "(mod)"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val (<=) "(<=)"
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
end
(* TODO
other mach.int.XXX modules *)
......@@ -165,6 +201,20 @@ module mach.array.Array31
syntax val blit "Array.blit"
syntax val self_blit "Array.blit"
end
module mach.array.Array63
syntax type array "(%1 array)"
syntax val make "Array.make"
syntax val ([]) "Array.get"
syntax val ([]<-) "Array.set"
syntax val length "Array.length"
syntax val append "Array.append"
syntax val sub "Array.sub"
syntax val copy "Array.copy"
syntax val fill "Array.fill"
syntax val blit "Array.blit"
syntax val self_blit "Array.blit"
end
(* TODO
module string.Char
......
......@@ -223,6 +223,38 @@ module Zeckendorf
done;
!l
(* unicity proof *)
function snoc (l:list int) (x:int) : list int = match l with
| Nil -> Cons x Nil
| Cons y q -> Cons y (snoc q x)
end
let rec lemma zeckendorf_unique (l1 l2:list int) : unit
requires { wf 2 l1 /\ wf 2 l2 }
requires { sum l1 = sum l2 }
ensures { l1 = l2 }
variant { sum l1 }
= let rec decomp (k acc:int) (lc lb:list int) : (int,list int)
requires { wf k lc }
requires { k >= 2 /\ lc <> Nil }
requires { 0 <= acc = sum lb - sum lc < fib (k-1) }
returns { (x,p) -> fib x <= sum lb = acc + fib x + sum p < fib (x+1) }
returns { (x,p) -> wf k p /\ x >= k /\ lc = snoc p x }
variant { lc }
= match lc with
| Nil -> absurd
| Cons x Nil -> (x,Nil)
| Cons x q -> let (y,p) = decomp (x+2) (acc+fib x) q lb in (y,Cons x p)
end in
match l1 , l2 with
| Nil , Nil -> ()
| Nil , l | l , Nil -> let _ = decomp 2 0 l l in absurd
| _ , _ -> let (a1,q1) = decomp 2 0 l1 l1 in
let (a2,q2) = decomp 2 0 l2 l2 in
zeckendorf_unique q1 q2
end
end
theory Mat22 "2x2 integer matrices"
......
This diff is collapsed.
module TestMatrix
use import int.Int
use import matrix.Syntax
use import matrix.Matrix
let test1 () =
let m1 = make 3 3 2 in
assert { m1[(0,0)] = 2 };
m1[(0,0)] <- 4;
assert { m1[(0,0)] = 4 };
assert { m1[(0,1)] = 2 };
assert { m1[(1,0)] = 2 };
assert { get m1 0 0 = 2 };
set m1 0 0 4;
assert { get m1 0 0 = 4 };
assert { get m1 0 1 = 2 };
assert { get m1 1 0 = 2 };
()
end
......
......@@ -18,7 +18,7 @@ module WarshallAlgorithm
inductive path (matrix bool) int int int =
| Path_empty:
forall m: matrix bool, i j k: int.
get m (i,j) -> path m i j k
get m i j -> path m i j k
| Path_cons:
forall m: matrix bool, i x j k: int.
0 <= x < k -> path m i x k -> path m x j k -> path m i j k
......@@ -35,26 +35,26 @@ module WarshallAlgorithm
requires { m.rows = m.columns }
ensures { let n = m.rows in
forall x y: int. 0 <= x < n -> 0 <= y < n ->
get result (x,y) <-> path m x y n }
get result x y <-> path m x y n }
=
let t = copy m in
let n = m.rows in
for k = 0 to n - 1 do
invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
get t (x,y) <-> path m x y k }
get t x y <-> path m x y k }
for i = 0 to n - 1 do
invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
get t (x,y) <->
get t x y <->
if x < i
then path m x y (k+1)
else path m x y k }
for j = 0 to n - 1 do
invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
get t (x,y) <->
get t x y <->
if x < i \/ (x = i /\ y < j)
then path m x y (k+1)
else path m x y k }
set t (i,j) (get t (i,j) || get t (i,k) && get t (k,j))
set t i j (get t i j || get t i k && get t k j)
done
done
done;
......
......@@ -39,30 +39,18 @@ Definition rows {a:Type} {a_WT:WhyType a} (v:(matrix a)): Z :=
end.
(* Why3 assumption *)
Definition index := (Z* Z)%type.
Definition get {a:Type} {a_WT:WhyType a} (a1:(matrix a)) (r:Z) (c:Z): a :=
(map.Map.get (map.Map.get (elts a1) r) c).
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:(matrix a)) (i:(Z*
Z)%type): a :=
match i with
| (r, c) => (map.Map.get (map.Map.get (elts a1) r) c)
end.
Definition set {a:Type} {a_WT:WhyType a} (a1:(matrix a)) (r:Z) (c:Z)
(v:a): (matrix a) := (mk_matrix (rows a1) (columns a1)
(map.Map.set (elts a1) r (map.Map.set (map.Map.get (elts a1) r) c v))).
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(matrix a)) (i:(Z* Z)%type)
(v:a): (matrix a) :=
match i with
| (r, c) => (mk_matrix (rows a1) (columns a1) (map.Map.set (elts a1) r
(map.Map.set (map.Map.get (elts a1) r) c v)))
end.
(* Why3 assumption *)
Definition valid_index {a:Type} {a_WT:WhyType a} (a1:(matrix a)) (i:(Z*
Z)%type): Prop :=
match i with
| (r, c) => ((0%Z <= r)%Z /\ (r < (rows a1))%Z) /\ ((0%Z <= c)%Z /\
(c < (columns a1))%Z)
end.
Definition valid_index {a:Type} {a_WT:WhyType a} (a1:(matrix a)) (r:Z)
(c:Z): Prop := ((0%Z <= r)%Z /\ (r < (rows a1))%Z) /\ ((0%Z <= c)%Z /\
(c < (columns a1))%Z).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a} (r:Z) (c:Z) (v:a): (matrix a) :=
......@@ -71,8 +59,8 @@ Definition make {a:Type} {a_WT:WhyType a} (r:Z) (c:Z) (v:a): (matrix a) :=
(* Why3 assumption *)
Inductive path: (matrix bool) -> Z -> Z -> Z -> Prop :=
| Path_empty : forall (m:(matrix bool)) (i:Z) (j:Z) (k:Z), ((get m (i,
j)) = true) -> (path m i j k)
| Path_empty : forall (m:(matrix bool)) (i:Z) (j:Z) (k:Z), ((get m i
j) = true) -> (path m i j k)
| Path_cons : forall (m:(matrix bool)) (i:Z) (x:Z) (j:Z) (k:Z),
((0%Z <= x)%Z /\ (x < k)%Z) -> ((path m i x k) -> ((path m x j k) ->
(path m i j k))).
......@@ -80,6 +68,7 @@ Inductive path: (matrix bool) -> Z -> Z -> Z -> Prop :=
(* Why3 goal *)
Theorem weakening : forall (m:(matrix bool)) (i:Z) (j:Z) (k1:Z) (k2:Z),
((0%Z <= k1)%Z /\ (k1 <= k2)%Z) -> ((path m i j k1) -> (path m i j k2)).
(* Why3 intros m i j k1 k2 (h1,h2) h3. *)
intros m i j k1 k2 (h1,h2) h3.
induction h3.
apply Path_empty; auto.
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.4pl4" timelimit="6" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../warshall_algorithm.mlw" expanded="true">
<theory name="WarshallAlgorithm" sum="35775684806f223a227238d2ab0704d5" expanded="true">
<goal name="weakening" expanded="true">
<proof prover="0" edited="warshall_algorithm_WarshallAlgorithm_weakening_1.v"><result status="valid" time="0.97"/></proof>
</goal>
<goal name="decomposition" expanded="true">
<proof prover="0" edited="warshall_algorithm_WarshallAlgorithm_decomposition_1.v"><result status="valid" time="1.53"/></proof>
</goal>
<goal name="WP_parameter transitive_closure" expl="VC for transitive_closure">
<transf name="split_goal_wp">
<goal name="WP_parameter transitive_closure.1" expl="1. postcondition">
<proof prover="2"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.2" expl="2. loop invariant init">
<proof prover="2"><result status="valid" time="0.03" steps="33"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.3" expl="3. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.4" expl="4. loop invariant init">
<proof prover="2"><result status="valid" time="0.08" steps="51"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.5" expl="5. loop invariant preservation">
<transf name="split_goal_wp">
<goal name="WP_parameter transitive_closure.5.1" expl="1. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.07" steps="18"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.5.2" expl="2. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.5.3" expl="3. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.00" steps="16"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter transitive_closure.6" expl="6. loop invariant init">
<proof prover="2"><result status="valid" time="0.06" steps="106"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.7" expl="7. type invariant">
<proof prover="2"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.8" expl="8. precondition">
<proof prover="2"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.9" expl="9. precondition">
<proof prover="2"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.10" expl="10. loop invariant preservation">
<transf name="split_goal_wp">
<goal name="WP_parameter transitive_closure.10.1" expl="1. loop invariant preservation">
<transf name="split_all_full">
<goal name="WP_parameter transitive_closure.10.1.1" expl="1. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.02" steps="29"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.10.1.2" expl="2. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.03" steps="49"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter transitive_closure.10.2" expl="2. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.03" steps="34"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.10.3" expl="3. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.04" steps="75"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter transitive_closure.11" expl="11. precondition">
<proof prover="2"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.12" expl="12. precondition">
<proof prover="2"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.13" expl="13. precondition">
<proof prover="2"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.14" expl="14. loop invariant preservation">
<transf name="split_goal_wp">
<goal name="WP_parameter transitive_closure.14.1" expl="1. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.14.2" expl="2. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.07" steps="37"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.14.3" expl="3. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.07"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter transitive_closure.15" expl="15. precondition">
<proof prover="2"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.16" expl="16. loop invariant preservation">
<transf name="split_goal_wp">
<goal name="WP_parameter transitive_closure.16.1" expl="1. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.16.2" expl="2. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.04" steps="36"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.16.3" expl="3. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter transitive_closure.17" expl="17. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.10" steps="202"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.18" expl="18. loop invariant preservation">
<transf name="split_goal_wp">
<goal name="WP_parameter transitive_closure.18.1" expl="1. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.18.2" expl="2. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter transitive_closure.19" expl="19. type invariant">
<proof prover="2"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.20" expl="20. postcondition">
<proof prover="2"><result status="valid" time="0.06" steps="17"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -9,26 +9,23 @@ module Matrix
model { rows: int; columns: int; mutable elts: map int (map int 'a) }
invariant { 0 <= self.rows /\ 0 <= self.columns }
type index = (int, int)
function get (a: matrix 'a) (r c: int) : 'a =
M.get (M.get a.elts r) c
function get (a: matrix 'a) (i: index) : 'a =
let r,c = i in M.get (M.get a.elts r) c
function set (a: matrix 'a) (i: index) (v: 'a) : matrix 'a =
let r,c = i in
function set (a: matrix 'a) (r c: int) (v: 'a) : matrix 'a =
{ a with elts = M.set a.elts r (M.set (M.get a.elts r) c v) }
predicate valid_index (a: matrix 'a) (i: index) =
let r,c = i in 0 <= r < a.rows /\ 0 <= c < a.columns
predicate valid_index (a: matrix 'a) (r c: int) =
0 <= r < a.rows /\ 0 <= c < a.columns
val get (a: matrix 'a) (i: index) : 'a
requires { valid_index a i }
ensures { result = get a i }
val get (a: matrix 'a) (r c: int) : 'a
requires { valid_index a r c }
ensures { result = get a r c }
val set (a: matrix 'a) (i: index) (v: 'a) : unit writes {a}
requires { valid_index a i }
ensures { let r,c = i in
a.elts = M.set (old a.elts) r (M.set (M.get (old a.elts) r) c v) }
val set (a: matrix 'a) (r c: int) (v: 'a) : unit
requires { valid_index a r c }
writes {a}
ensures { a.elts = M.set (old a.elts) r (M.set (M.get (old a.elts) r) c v)}
val rows (a: matrix 'a) : int ensures { result = a.rows }
val columns (a: matrix 'a) : int ensures { result = a.columns }
......@@ -36,51 +33,30 @@ module Matrix
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
let defensive_get (a: matrix 'a) (i: index)
ensures { valid_index a i /\ result = get a i }
raises { OutOfBounds -> not (valid_index a i) }
= let r,c = i in
if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
get a i
let defensive_get (a: matrix 'a) (r c: int) : 'a
ensures { valid_index a r c }
ensures { result = get a r c }
raises { OutOfBounds -> not (valid_index a r c) }
= if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
get a r c
let defensive_set (a: matrix 'a) (i: index) (v: 'a)
ensures { valid_index a i /\ a = set (old a) i v }
raises { OutOfBounds -> not (valid_index a i) /\ a = old a }
= let r,c = i in
if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
set a i v
let defensive_set (a: matrix 'a) (r c: int) (v: 'a) : unit
ensures { valid_index a r c }
ensures { a.elts = M.set (old a.elts) r (M.set (M.get (old a.elts) r) c v)}
raises { OutOfBounds -> not (valid_index a r c) /\ a = old a }
= if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
set a r c v
val make (r c: int) (v: 'a) : matrix 'a
requires { r >= 0 /\ c >= 0 }
ensures { result.rows = r }
ensures { result.columns = c }
ensures { forall i j. 0 <= i < r /\ 0 <= j < c -> get result (i,j) = v }
ensures { forall i j. 0 <= i < r /\ 0 <= j < c -> get result i j = v }
val copy (a: matrix 'a) : matrix 'a
ensures { result.rows = a.rows /\ result.columns = a.columns }
ensures { forall r:int. 0 <= r < result.rows ->
forall c:int. 0 <= c < result.columns ->
get result (r,c) = get a (r,c) }
end
(* {2 Square bracket syntax in both logic and programs} *)
module Syntax
use import int.Int
use export Matrix
function ([]) (a: matrix 'a) (i: index) : 'a = get a i
function ([<-]) (a: matrix 'a) (i: index) (v: 'a) : matrix 'a = set a i v
val ([]) (a: matrix 'a) (i: index) : 'a
requires { valid_index a i }
ensures { result = get a i }
val ([]<-) (a: matrix 'a) (i: index) (v: 'a) : unit writes {a}
requires { let r,c = i in 0 <= r < a.rows /\ 0 <= c < a.columns }
ensures { let r,c = i in
a.elts = M.set (old a.elts) r (M.set (M.get (old a.elts) r) c v) }
get result r c = get a r c }
end
......@@ -587,11 +587,11 @@ let rec intros_hyp n fmt f =
match f.t_node with
| Tbinop(Tand,f1,f2) ->
fprintf fmt "(";
let m = intros_hyp n fmt f1 in
let (m,vsl1) = intros_hyp n fmt f1 in
fprintf fmt ",";
let k = intros_hyp m fmt f2 in
let (k,vsl2) = intros_hyp m fmt f2 in
fprintf fmt ")";
k
(k,vsl1@vsl2)
| Tquant(Texists,fq) ->
let vsl,_trl,f = t_open_quant fq in
let rec aux n vsl =
......@@ -603,12 +603,10 @@ let rec intros_hyp n fmt f =
fprintf fmt ")";
m
in
let m = aux n vsl in
List.iter forget_var vsl;
m
aux n vsl
| _ ->
fprintf fmt "h%d" n;
n+1
(n+1,[])
let rec do_intros n fmt fmla =
match fmla.t_node with
......@@ -625,8 +623,9 @@ let rec do_intros n fmt fmla =
List.iter forget_var vsl
| Tbinop(Timplies, f1, f2) ->
fprintf fmt "@ ";
let m = intros_hyp n fmt f1 in
do_intros m fmt f2
let m,vsl = intros_hyp n fmt f1 in
do_intros m fmt f2;
List.iter forget_var vsl
| _ -> ()
let intros_params fmt params =
......
......@@ -26,20 +26,10 @@
- singleton types
record/constructor fields of type unit
- preludes
- command line
- drivers:
- ghost code
remove it as much as possible (in types and function arguments)
we'd like to use both ocaml64.drv from the lib and a local
driver (specific to the files being extracted) but currently
- only one driver is allowed on the extraction command line
- import "ocaml64" in the local driver fails, because it's looking
for a file ocaml64 in the local directory (and not for ocaml64.drv
in the library)
- preludes
*)
......@@ -173,6 +163,7 @@ type info = {
th_known_map: Decl.known_map;
mo_known_map: Mlw_decl.known_map;
fname: string option;
unsafe_int: bool;
}
module Translate = struct
......@@ -358,8 +349,8 @@ module Translate = struct
assert false
| Tapp (fs, tl) when is_fs_tuple fs ->
ML.etuple (List.map (term info) tl)
| Tapp (fs, [t1; t2])
when ls_equal fs ps_equ && oty_equal t1.t_ty oty_int ->
| Tapp (fs, [t1; t2]) when not info.unsafe_int
&& ls_equal fs ps_equ && oty_equal t1.t_ty oty_int ->
ML.Esyntax ("(Why3__BigInt.eq %1 %2)", [term info t1; term info t2])
| Tapp (fs, tl) ->
begin match query_syntax info.info_syn fs.ls_name with
......@@ -885,6 +876,8 @@ module Print = struct
print_lident info fmt v
| Ebool b ->
fprintf fmt "%b" b
| Econst c when info.unsafe_int ->
fprintf fmt "%s" (BigInt.to_string (Number.compute_int c))
| Econst c ->
print_const ~paren fmt c
| Etuple el ->
......@@ -950,6 +943,12 @@ module Print = struct
| Ewhile (e1, e2) ->
fprintf fmt "@[<hv>while %a do@;<1 2>@[%a@]@ done@]"
(print_expr info) e1 (print_expr info) e2
| Efor (x, vfrom, dir, vto, e1) when info.unsafe_int ->
fprintf fmt
"@[<hov 2>for %a = %a %s %a do@\n%a@\ndone@]"
(print_lident info) x (print_lident info) vfrom
(if dir = To then "to" else "downto") (print_lident info) vto
(print_expr info) e1
| Efor (x, vfrom, dir, vto, e1) ->
fprintf fmt
"@[<hov 2>(Why3__IntAux.for_loop_%s %a %a@ (fun %a ->@ %a))@]"
......@@ -1042,10 +1041,8 @@ end
let extract_filename ?fname th =
(modulename ?fname th.th_path th.th_name.Ident.id_string) ^ ".ml"
(*
let arith_meta = register_meta "ocaml arithmetic" [MTstring]
~desc:"Specify@ OCaml@ arithmetic:@ 32, 64, or unsafe"