OCaml extraction: fixed filenames and ident names

parent 266e5156
......@@ -33,6 +33,8 @@ theory list.List
end
theory int.Int
(* TODO: make a for_num prelude function *)
syntax function zero "(Num.num_of_int 0)"
syntax function one "(Num.num_of_int 1)"
......
......@@ -522,18 +522,8 @@ let do_local_theory env drv fname m (tname,_,t,glist) =
(* program extraction *)
let extract_to ?fname th extract =
let dir = match !opt_output with Some dir -> dir | None -> assert false in
let _fname = match fname, th.th_path with
| Some fname, _ ->
let fname = Filename.basename fname in
(try Filename.chop_extension fname with _ -> fname)
| None, [] -> assert false
| None, path -> List.hd (List.rev path)
in
(* FIXME: use fname to forge the OCaml filename *)
let mname = (* fname ^ "__" ^ *) th.th_name.Ident.id_string ^ ".ml" in
(* let mname = String.uncapitalize mname in *)
let file = Filename.concat dir mname in
let dir = Util.of_option !opt_output in
let file = Filename.concat dir (Mlw_ocaml.extract_filename ?fname th) in
let old =
if Sys.file_exists file then begin
let backup = file ^ ".bak" in
......@@ -545,16 +535,16 @@ let extract_to ?fname th extract =
close_out cout
let do_extract_theory env ?fname tname th =
let extract fname ?old fmt = ignore (old);
Debug.dprintf Mlw_ocaml.debug "extract theory %s to file %s@." tname fname;
Mlw_ocaml.extract_theory env ?old fmt th
let extract file ?old fmt = ignore (old);
Debug.dprintf Mlw_ocaml.debug "extract theory %s to file %s@." tname file;
Mlw_ocaml.extract_theory env ?old ?fname fmt th
in
extract_to ?fname th extract
let do_extract_module env ?fname tname m =
let extract fname ?old fmt = ignore (old);
Debug.dprintf Mlw_ocaml.debug "extract module %s to file %s@." tname fname;
Mlw_ocaml.extract_module env ?old fmt m
let extract file ?old fmt = ignore (old);
Debug.dprintf Mlw_ocaml.debug "extract module %s to file %s@." tname file;
Mlw_ocaml.extract_module env ?old ?fname fmt m
in
extract_to ?fname m.Mlw_module.mod_theory extract
......
......@@ -33,6 +33,24 @@ let debug =
Debug.register_info_flag
~desc:"Print details on program extraction." "extraction"
let clean_fname fname =
let fname = Filename.basename fname in
(try Filename.chop_extension fname with _ -> fname)
let modulename ?fname th =
let fname = match fname, th.th_path with
| Some fname, _ -> clean_fname fname
| None, [] -> assert false
| None, path -> String.concat "__" path
in
fname ^ "__" ^ th.th_name.Ident.id_string
let extract_filename ?fname th =
(modulename ?fname th) ^ ".ml"
let modulename path t =
String.capitalize ((String.concat "__" path) ^ "__" ^ t)
(** Driver *)
(* (path,id) -> string Hid *)
......@@ -73,8 +91,9 @@ let forget_all () =
type info = {
info_syn: syntax_map;
current_theory: string;
current_theory: Theory.theory;
known_map: Decl.known_map;
fname: string option;
(* symbol_printers : (string * ident_printer) Mid.t; *)
}
......@@ -105,15 +124,18 @@ let print_ident fmt id =
let print_path = print_list dot pp_print_string
let print_qident ~sanitizer info fmt id =
let s = id_unique ~sanitizer iprinter id in
try
let _lp, t, _p = Theory.restore_path id in
(* fprintf fmt "%a/%s/%a" print_path lp t print_path p *)
if t = info.current_theory then
let lp, t, p = Theory.restore_path id in
let lp = if lp <> [] then lp else [Util.def_option "Builtin" info.fname] in
let s = String.concat "__" p in
let s = Ident.sanitizer char_to_alpha char_to_alnumus s in
let s = sanitizer s in
if Sid.mem id info.current_theory.th_local then
fprintf fmt "%s" s
else
fprintf fmt "%s.%s" t s
fprintf fmt "%s.%s" (modulename lp t) s
with Not_found ->
let s = id_unique ~sanitizer iprinter id in
fprintf fmt "%s" s
let print_lident = print_qident ~sanitizer:String.uncapitalize
......@@ -495,13 +517,14 @@ let ocaml_driver env =
eprintf "cannot find driver 'ocaml'@.";
raise e
let extract_theory env ?old fmt th =
ignore (old);
let extract_theory env ?old ?fname fmt th =
ignore (old); ignore (fname);
let sm = ocaml_driver env in
let info = {
info_syn = sm;
current_theory = th.th_name.id_string;
known_map = Task.task_known (Task.use_export None th) } in
current_theory = th;
known_map = Task.task_known (Task.use_export None th);
fname = Util.option_map clean_fname fname; } in
fprintf fmt
"(* This file has been generated from Why3 theory %a *)@\n@\n"
print_theory_name th;
......@@ -708,14 +731,15 @@ let pdecl info fmt pd = match pd.pd_node with
(** Modules *)
let extract_module env ?old fmt m =
ignore (old);
let extract_module env ?old ?fname fmt m =
ignore (old); ignore (fname);
let sm = ocaml_driver env in
let th = m.mod_theory in
let info = {
info_syn = sm;
current_theory = th.th_name.id_string;
known_map = Task.task_known (Task.use_export None th) } in
current_theory = th;
known_map = Task.task_known (Task.use_export None th);
fname = Util.option_map clean_fname fname; } in
fprintf fmt
"(* This file has been generated from Why3 module %a *)@\n@\n"
print_module_name m;
......
......@@ -24,11 +24,13 @@ open Why3
val debug: Debug.flag
val extract_filename: ?fname:string -> Theory.theory -> string
val extract_theory:
Env.env -> ?old:Pervasives.in_channel -> Format.formatter ->
Theory.theory -> unit
Env.env -> ?old:Pervasives.in_channel -> ?fname:string ->
Format.formatter -> Theory.theory -> unit
val extract_module:
Env.env -> ?old:Pervasives.in_channel -> Format.formatter ->
Mlw_module.modul -> unit
Env.env -> ?old:Pervasives.in_channel -> ?fname:string ->
Format.formatter -> Mlw_module.modul -> unit
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