Commit ba956b8f authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

new OCaml driver ocaml-unsafe-int

maps Why3 type int to OCaml type int
this is of course unsafe, unless one has proved absence of overflows
parent cd560bdc
(** 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
......
......@@ -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"
*)
let unsafe_int drv =
drv.Mlw_driver.drv_printer = Some "ocaml-unsafe-int"
let extract_theory drv ?old ?fname fmt th =
ignore (old); ignore (fname);
......@@ -1057,13 +1054,13 @@ let extract_theory drv ?old ?fname fmt th =
current_module = None;
th_known_map = th.th_known;
mo_known_map = Mid.empty;
fname = Opt.map clean_fname fname; } in
fname = Opt.map clean_fname fname;
unsafe_int = unsafe_int drv; } in
let decls = Translate.theory info th in
fprintf fmt
"(* This file has been generated from Why3 theory %a *)@\n@\n"
Print.print_theory_name th;
fprintf fmt
"open Why3extract@\n@\n";
if not info.unsafe_int then fprintf fmt "open Why3extract@\n@\n";
print_list nothing (Print.print_decl info) fmt decls;
fprintf fmt "@."
......@@ -1080,14 +1077,14 @@ let extract_module drv ?old ?fname fmt m =
current_module = Some m;
th_known_map = th.th_known;
mo_known_map = m.mod_known;
fname = Opt.map clean_fname fname; } in
fname = Opt.map clean_fname fname;
unsafe_int = unsafe_int drv; } in
let decls = Translate.theory info th in
let mdecls = Translate.module_ info m in
fprintf fmt
"(* This file has been generated from Why3 module %a *)@\n@\n"
Print.print_module_name m;
fprintf fmt
"open Why3extract@\n@\n";
if not info.unsafe_int then fprintf fmt "open Why3extract@\n@\n";
print_list nothing (Print.print_decl info) fmt decls;
print_list nothing (Print.print_decl info) fmt mdecls;
fprintf fmt "@."
......
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