OCaml extraction now recursively extracts all dependencies

All files are extracted to the target repository, even those
corresponding to files from the Why3 standard library.
Some of these files may be empty (e.g. ref__Ref.ml) when everything
is overridden by the OCaml driver. You can ignore these files when
compiling the extracted OCaml code.
parent a1636bf3
......@@ -18,20 +18,28 @@ theory option.Option
syntax function Some "(Some %1)"
end
(* bool *)
theory Bool
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
end
theory bool.Ite
syntax function ite "(if %1 then %2 else %3)"
end
theory bool.Bool
syntax function andb "(%1 && %2)"
syntax function orb "(%1 || %2)"
(* syntax function xorb "(xorb %1 %2)" *)
syntax function xorb "(%1 <> %2)"
syntax function notb "(not %1)"
(* syntax function implb "(implb %1)" *)
syntax function implb "(not %1 || %2)"
end
(* int *)
theory int.Int
syntax constant zero "Why3__BigInt.zero"
syntax constant one "Why3__BigInt.one"
......@@ -71,6 +79,22 @@ theory int.ComputerDivision
syntax function mod "(Why3__BigInt.computer_mod %1 %2)"
end
theory int.Power
syntax function power "(Why3__BigInt.power %1 %2)"
end
theory int.Fact
syntax function fact "(Why3__BigInt.fact %1)"
end
theory int.Fibonacci
syntax function fib "(Why3__BigInt.fib %1)"
end
(* TODO number.Gcd *)
(* list *)
theory list.List
syntax type list "%1 list"
syntax function Nil "[]"
......@@ -81,6 +105,10 @@ theory list.Length
syntax function length "(List.length %1)"
end
theory list.Mem
syntax predicate mem "(List.mem %1 %2)"
end
theory list.Append
syntax function (++) "(List.append %1 %2)"
end
......@@ -89,6 +117,16 @@ theory list.Reverse
syntax function reverse "(List.rev %1)"
end
theory list.RevAppend
syntax function rev_append "(List.rev_append %1 %2)"
end
theory list.Combine
syntax function combine "(List.combine %1 %2)"
end
(* map *)
theory map.Map
syntax type map "((%1, %2) Why3__Map.map)"
syntax function const "(Why3__Map.const %1)"
......@@ -108,14 +146,6 @@ module ref.Ref
syntax val (:=) "Pervasives.(:=)"
end
module ref.Refint
syntax val incr "Why3__BigInt.incr"
syntax val decr "Why3__BigInt.decr"
syntax val ( += ) "Why3__BigInt.(+=)"
syntax val ( -= ) "Why3__BigInt.(-=)"
syntax val ( *= ) "Why3__BigInt.(*=)"
end
module array.Array
syntax type array "(%1 Why3__BigInt.Array.t)"
syntax function ([]) "(Why3__BigInt.Array.get %1 %2)"
......
int__Abs.ml
int__ComputerDivision.ml
int__Div2.ml
int__Int.ml
why3__Bool.ml
why3__BuiltIn.ml
why3__Prelude.ml
why3__Tuple0.ml
why3__Unit.ml
......@@ -36,6 +36,7 @@ $(ML): ../euler001.mlw
clean::
rm -f $(ML) *.cm[xio] *.o *.annot $(MAIN).opt $(MAIN).byte
rm -f why3__*.ml* euler001__*.ml* int__*.ml*
Makefile: Makefile.in ../../config.status
cd ../.. ; ./config.status chmod --file examples/euler001/Makefile
......
array__Array.ml
int__Int.ml
map__Map.ml
why3__Bool.ml
why3__BuiltIn.ml
why3__Prelude.ml
why3__Tuple0.ml
why3__Unit.ml
......@@ -42,5 +42,9 @@ $(ML): ../sudoku.mlw
ocamlc $(WHY3) -annot -g -c $<
clean::
rm -f $(ML) *.cm[xio] $(MAIN).opt $(MAIN).byte
rm -f $(ML) *.annot *.o *.cm[xio] $(MAIN).opt $(MAIN).byte
rm -f sudoku__*.ml why3__*.ml
rm -f int__Int.ml map__Map.ml array__Array.ml
......@@ -61,6 +61,16 @@ let to_int = int_of_big_int
(* the code below is to be used in OCaml extracted code (see ocaml.drv) *)
let power x y = try power_big x y with Invalid_argument _ -> zero
let rec fact n = if le n one then one else mul n (fact (pred n))
let fib n =
let n = to_int n in
if n = 0 then zero else if n = 1 then one else
let a = Array.make (n + 1) zero in
a.(1) <- one; for i = 2 to n do a.(i) <- add a.(i-2) a.(i-1) done; a.(n)
let rec for_loop_to x1 x2 body =
if le x1 x2 then begin
body x1;
......@@ -73,12 +83,6 @@ let rec for_loop_downto x1 x2 body =
for_loop_downto (pred x1) x2 body
end
let incr r = r := succ !r
let decr r = r := pred !r
let ( += ) r v = r := add !r v
let ( -= ) r v = r := sub !r v
let ( *= ) r v = r := mul !r v
module Array = struct
type 'a t = 'a array
let get a i = a.(to_int i)
......
......@@ -613,19 +613,44 @@ let extract_to ?fname th extract =
extract file ?old (formatter_of_out_channel cout);
close_out cout
let do_extract_theory edrv ?fname tname th =
let extract_to =
let visited = Ident.Hid.create 17 in
fun ?fname th extract ->
if not (Ident.Hid.mem visited th.th_name) then begin
Ident.Hid.add visited th.th_name ();
extract_to ?fname th extract
end
let use_iter f th =
List.iter (fun d -> match d.td_node with Use t -> f t | _ -> ()) th.th_decls
let rec do_extract_theory edrv ?fname th =
let extract file ?old fmt = ignore (old);
let tname = th.th_name.Ident.id_string in
Debug.dprintf Mlw_ocaml.debug "extract theory %s to file %s@." tname file;
Mlw_ocaml.extract_theory edrv ?old ?fname fmt th
in
extract_to ?fname th extract
extract_to ?fname th extract;
let extract_use th' =
let fname = if th'.th_path = [] then fname else None in
do_extract_theory edrv ?fname th' in
use_iter extract_use th
let do_extract_module edrv ?fname tname m =
let rec do_extract_module edrv ?fname m =
let extract file ?old fmt = ignore (old);
let tname = m.Mlw_module.mod_theory.th_name.Ident.id_string in
Debug.dprintf Mlw_ocaml.debug "extract module %s to file %s@." tname file;
Mlw_ocaml.extract_module edrv ?old ?fname fmt m
in
extract_to ?fname m.Mlw_module.mod_theory extract
extract_to ?fname m.Mlw_module.mod_theory extract;
let extract_use th' =
let fname = if th'.th_path = [] then fname else None in
match
try Some (Mlw_module.restore_module th') with Not_found -> None
with
| Some m' -> do_extract_module edrv ?fname m'
| None -> do_extract_theory edrv ?fname th' in
use_iter extract_use m.Mlw_module.mod_theory
let do_global_extract edrv (tname,p,t,_,_) =
let lib = edrv.Mlw_driver.drv_lib in
......@@ -633,15 +658,15 @@ let do_global_extract edrv (tname,p,t,_,_) =
let mm, thm = Env.read_lib_file lib p in
try
let m = Mstr.find t mm in
do_extract_module edrv tname m
do_extract_module edrv m
with Not_found ->
let th = Mstr.find t thm in
do_extract_theory edrv tname th
do_extract_theory edrv th
with Env.LibFileNotFound _ | Not_found -> try
let format = Opt.get_def "why" !opt_parser in
let env = Env.env_of_library lib in
let th = Env.read_theory ~format env p t in
do_extract_theory edrv tname th
do_extract_theory edrv th
with Env.LibFileNotFound _ | Env.TheoryNotFound _ ->
eprintf "Theory/module '%s' not found.@." tname;
exit 1
......@@ -651,13 +676,13 @@ let do_extract_theory_from env fname m (tname,_,t,_,_) =
eprintf "Theory '%s' not found in file '%s'.@." tname fname;
exit 1
in
do_extract_theory env ~fname tname th
do_extract_theory env ~fname th
let do_extract_module_from env fname mm thm (tname,_,t,_,_) =
try
let m = Mstr.find t mm in do_extract_module env ~fname tname m
let m = Mstr.find t mm in do_extract_module env ~fname m
with Not_found -> try
let th = Mstr.find t thm in do_extract_theory env ~fname tname th
let th = Mstr.find t thm in do_extract_theory env ~fname th
with Not_found ->
eprintf "Theory/module '%s' not found in file '%s'.@." tname fname;
exit 1
......@@ -668,9 +693,9 @@ let do_local_extract edrv fname cin tlist =
let mm, thm = Mlw_main.read_channel lib [] fname cin in
if Queue.is_empty tlist then begin
let do_m t m thm =
do_extract_module edrv ~fname t m; Mstr.remove t thm in
do_extract_module edrv ~fname m; Mstr.remove t thm in
let thm = Mstr.fold do_m mm thm in
Mstr.iter (fun t th -> do_extract_theory edrv ~fname t th) thm
Mstr.iter (fun _ th -> do_extract_theory edrv ~fname th) thm
end else
Queue.iter (do_extract_module_from edrv fname mm thm) tlist
end else begin
......@@ -678,7 +703,7 @@ let do_local_extract edrv fname cin tlist =
let m = Env.read_channel ?format:!opt_parser env fname cin in
if Queue.is_empty tlist then
let add_th t th mi = Ident.Mid.add th.th_name (t,th) mi in
let do_th _ (t,th) = do_extract_theory edrv ~fname t th in
let do_th _ (_,th) = do_extract_theory edrv ~fname th in
Ident.Mid.iter do_th (Mstr.fold add_th m Ident.Mid.empty)
else
Queue.iter (do_extract_theory_from edrv fname m) tlist
......
......@@ -71,6 +71,18 @@ let to_int = int_of_big_int
(* the code below is to be used in OCaml extracted code (see ocaml.drv) *)
let power x y =
try power_big_int_positive_big_int x y
with Invalid_argument _ -> zero
let rec fact n = if le n one then one else mul n (fact (pred n))
let fib n =
let n = to_int n in
if n = 0 then zero else if n = 1 then one else
let a = Array.make (n + 1) zero in
a.(1) <- one; for i = 2 to n do a.(i) <- add a.(i-2) a.(i-1) done; a.(n)
let rec for_loop_to x1 x2 body =
if le x1 x2 then begin
body x1;
......@@ -83,12 +95,6 @@ let rec for_loop_downto x1 x2 body =
for_loop_downto (pred x1) x2 body
end
let incr r = r := succ !r
let decr r = r := pred !r
let ( += ) r v = r := add !r v
let ( -= ) r v = r := sub !r v
let ( *= ) r v = r := mul !r v
module Array = struct
type 'a t = 'a array
let get a i = a.(to_int i)
......
......@@ -175,14 +175,19 @@ let empty_module env n p = {
muc_env = env;
}
let close_module uc =
let th = close_theory uc.muc_theory in (* catches errors *)
{ mod_theory = th;
mod_decls = List.rev uc.muc_decls;
mod_export = List.hd uc.muc_export;
mod_known = uc.muc_known;
mod_local = uc.muc_local;
mod_used = uc.muc_used; }
let close_module, restore_module =
let h = Hid.create 17 in
(fun uc ->
let th = close_theory uc.muc_theory in (* catches errors *)
let m = { mod_theory = th;
mod_decls = List.rev uc.muc_decls;
mod_export = List.hd uc.muc_export;
mod_known = uc.muc_known;
mod_local = uc.muc_local;
mod_used = uc.muc_used; } in
Hid.add h th.th_name m;
m),
(fun th -> Hid.find h th.th_name)
let get_theory uc = uc.muc_theory
let get_namespace uc = List.hd uc.muc_import
......@@ -386,6 +391,7 @@ let mod_prelude env =
let pd_exit = create_exn_decl xs_exit in
let pd_old = create_val_decl (LetV Mlw_wp.pv_old) in
let uc = empty_module env (id_fresh "Prelude") ["why3"] in
let uc = add_decl uc (Decl.create_ty_decl Mlw_wp.ts_mark) in
let uc = add_pdecl ~wp:false uc pd_old in
let uc = add_pdecl ~wp:false uc pd_exit in
close_module uc
......
......@@ -84,6 +84,10 @@ val restore_path : ident -> string list * string * string list
different modules, the first association is retained.
Raises Not_found if the ident was never declared in a module. *)
val restore_module : theory -> modul
(** retrieves a module from its underlying theory
raises [Not_found] if no such module exists *)
(** {2 Use and clone} *)
val use_export : module_uc -> modul -> module_uc
......
......@@ -753,6 +753,8 @@ let rec print_expr ?(paren=false) info fmt e =
(if dir = To then "to" else "downto")
(print_pv info) pvfrom (print_pv info) pvto
(print_pv info) pv (print_expr info) e
| Eraise (xs,_) when xs_equal xs xs_exit ->
fprintf fmt (protect_on paren "raise Pervasives.Exit")
| Eraise (xs,e) ->
begin match query_syntax info.info_syn xs.xs_name with
| Some s -> syntax_arguments s (print_expr info) fmt [e]
......@@ -811,6 +813,8 @@ and print_ebranch info fmt ({ppat_pattern=p}, e) =
and print_xbranch info fmt (xs, pv, e) =
begin match query_syntax info.info_syn xs.xs_name with
| Some s -> syntax_arguments s (print_pv info) fmt [pv]
| None when xs_equal xs xs_exit ->
fprintf fmt "@[<hov 4>| Pervasives.Exit ->@ %a@]" (print_expr info) e
| None when ity_equal xs.xs_ity ity_unit ->
fprintf fmt "@[<hov 4>| %a ->@ %a@]"
(print_xs info) xs (print_expr info) e
......@@ -914,6 +918,7 @@ let print_exn_decl info fmt xs =
(print_ity info) xs.xs_ity
let print_exn_decl info fmt xs =
if not (xs_equal xs xs_exit) then
if has_syntax info xs.xs_name then
fprintf fmt "(* symbol %a is overridden by driver *)"
(print_lident info) xs.xs_name
......@@ -990,6 +995,8 @@ let pdecl info fmt pd = match pd.pd_node with
print_list_next newline (print_pdata_decl info) fmt tl;
fprintf fmt "@\n@\n";
print_list nothing (print_pprojections info) fmt tl
| PDval (LetV pv) when pv_equal pv Mlw_wp.pv_old ->
()
| PDval lv ->
print_val_decl info fmt lv;
fprintf fmt "@\n@\n"
......
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