Commit 58425a2a authored by Mário Pereira's avatar Mário Pereira

Code extraction (wip)

Preparing for the new command line.
parent e27b988d
......@@ -183,24 +183,21 @@ module ML = struct
let add_known_decl id decl k_map =
Mid.add id decl k_map
let rec fold_deps_ty pmod = function
| Tvar _ -> []
| Tapp (id, ty_l) ->
let d = Mid.find id pmod.mod_known in
d :: List.concat (List.map (fold_deps_ty pmod) ty_l)
| Ttuple ty_l -> assert false
let fold_deps_typedef pmod = function
| Ddata constr_l -> assert false
| Drecord pjl -> assert false
| Dalias ty -> fold_deps_ty pmod ty
let fold_deps_its_defn pmod its_d = match its_d.its_def with
| None -> []
| Some typedef -> fold_deps_typedef pmod typedef
let fold_deps pmod = function
| Dtype its_dl -> List.concat (List.map (fold_deps_its_defn pmod) its_dl)
let rec iter_deps_ty f = function
| Tvar _ -> ()
| Tapp (id, ty_l) -> f id; List.iter (iter_deps_ty f) ty_l
| Ttuple ty_l -> List.iter (iter_deps_ty f) ty_l
let iter_deps_typedef f = function
| Ddata _constr_l -> assert false
| Drecord _pjl -> assert false
| Dalias ty -> iter_deps_ty f ty
let iter_deps_its_defn f its_d =
Opt.iter (iter_deps_typedef f) its_d.its_def
let iter_deps f = function
| Dtype its_dl -> List.iter (iter_deps_its_defn f) its_dl
| _ -> assert false (*TODO*)
let mk_expr e_node e_ity e_effect =
......@@ -648,6 +645,12 @@ module Translate = struct
let add_known = Mid.singleton xs.xs_name decl in
[decl, add_known]
let pdecl_m m pd =
let info = {
info_current_mo = Some m;
info_mo_known_map = m.mod_known; } in
pdecl info pd
(* unit module declarations *)
let mdecl info = function
| Udecl pd ->
......@@ -655,7 +658,10 @@ module Translate = struct
| _ -> (* TODO *) []
(* modules *)
let module_ info m =
let module_ m =
let info = {
info_current_mo = Some m;
info_mo_known_map = m.mod_known; } in
let known_m = ref Mid.empty in
let mk_decl_and_km (decl, known_m_new) =
known_m := Mid.set_union !known_m known_m_new;
......@@ -663,7 +669,7 @@ module Translate = struct
let comp munit =
let m = mdecl info munit in List.map mk_decl_and_km m in
let decl = List.map comp m.mod_units in
{ ML.mod_decl = List.concat decl; ML.mod_known = !known_m }
{ ML.mod_decl = List.concat decl; ML.mod_known = !known_m }, info
let () = Exn_printer.register (fun fmt e -> match e with
| ExtractionAny ->
......@@ -746,12 +752,12 @@ module Transform = struct
and rdef info subst r =
{ r with rec_exp = expr info subst r.rec_exp }
let decl info = function
let pdecl info = function
| Dtype _ | Dexn _ as d -> d
| Dlet def -> Dlet (let_def info Mpv.empty def)
let module_ info =
List.map (decl info)
let module_ info m =
{ m with mod_decl = List.map (pdecl info) m.mod_decl }
end
......
......@@ -79,12 +79,13 @@ let fg ?fname m =
open Format
let pr args ?old ?fname m fmt d =
let pr args ?old ?fname recursive m fmt d =
ignore(args);
ignore(old);
ignore(m);
ignore(d);
ignore(fname);
ignore(recursive);
fprintf fmt "#include <stdio.h>\n\
\n\
int main() {\n\
......
......@@ -33,6 +33,7 @@ type info = {
info_th_known_map : Decl.known_map;
info_mo_known_map : Pdecl.known_map;
info_fname : string option;
recursive : bool;
}
module Print = struct
......@@ -86,7 +87,7 @@ module Print = struct
fprintf fmt "%s" s
let print_qident ~sanitizer info fmt id =
try
try if not info.recursive then raise Not_found;
let lp, t, q =
try Pmodule.restore_path id
with Not_found -> Theory.restore_path id in
......@@ -458,7 +459,7 @@ module Print = struct
print_ident xs.xs_name (print_ty ~paren:true info) t
end
let print_decl pargs ?old ?fname ({mod_theory = th} as m) fmt d =
let print_decl pargs ?old ?fname recursive ({mod_theory = th} as m) fmt d =
ignore (old);
let info = {
info_syn = pargs.Pdriver.syntax;
......@@ -467,7 +468,8 @@ let print_decl pargs ?old ?fname ({mod_theory = th} as m) fmt d =
info_current_mo = Some m;
info_th_known_map = th.th_known;
info_mo_known_map = m.mod_known;
info_fname = Opt.map Compile.clean_name fname
info_fname = Opt.map Compile.clean_name fname;
recursive = recursive;
} in
Print.print_decl info fmt d;
fprintf fmt "@."
......
......@@ -221,8 +221,8 @@ open Stdlib
type filename_generator = ?fname:string -> Pmodule.pmodule -> string
type printer =
printer_args -> ?old:in_channel -> ?fname:string -> Pmodule.pmodule ->
Compile.ML.decl Pp.pp
printer_args -> ?old:in_channel -> ?fname:string -> bool ->
Pmodule.pmodule -> Compile.ML.decl Pp.pp
type reg_printer = Pp.formatted * filename_generator * printer
......
......@@ -38,8 +38,8 @@ val load_driver : Env.env -> string -> string list -> driver
@param string list additional drivers containing only theories/modules *)
type printer =
printer_args -> ?old:in_channel -> ?fname:string -> Pmodule.pmodule ->
Compile.ML.decl Pp.pp
printer_args -> ?old:in_channel -> ?fname:string -> bool ->
Pmodule.pmodule -> Compile.ML.decl Pp.pp
type filename_generator = ?fname:string -> Pmodule.pmodule -> string
......
......@@ -31,10 +31,9 @@ let opt_queue = Queue.create ()
let add_opt_file x =
let target =
if Sys.file_exists x then File x else match Strings.split '.' x with
| [f] -> File f (* FIXME *)
| [f;m] -> Module (f, m)
| [f;m;s] -> Symbol (f, m, s)
| _ -> Format.eprintf "Invalid input argument@."; exit 1 in
| _ -> Format.eprintf "Invalid input argument.@."; exit 1 in
Queue.push (Some target) opt_queue
let opt_parser = ref None
......@@ -66,21 +65,13 @@ let config, _, env =
let () =
if Queue.is_empty opt_queue then begin
eprintf "aqui@";
Whyconf.Args.exit_with_usage option_list usage_msg
end
let opt_recurs = !opt_recurs
type output = Empty | Dir of string
let get_output = function Empty -> assert false | Dir s -> s
(* FIXME: accept --mono without -o and use to standard output *)
let opt_output =
match !opt_output with
| None -> Empty
| Some d -> Dir d
let opt_output = !opt_output
let driver_file s =
if Sys.file_exists s || String.contains s '/' || String.contains s '.' then s
......@@ -97,36 +88,42 @@ let opt_driver =
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
let extract_to ?fname m =
let print_mdecls ?fname m mdecls =
let (fg,pargs,pr) = Pdriver.lookup_printer opt_driver in
let info = {
Translate.info_current_mo = Some m;
Translate.info_mo_known_map = m.mod_known;
} in
let mdecls = Translate.module_ info m in
let mdecls = Transform.module_ info mdecls.ML.mod_decl in
let file = Filename.concat (get_output opt_output) (fg ?fname m) in
let old =
if Sys.file_exists file then begin
let backup = file ^ ".bak" in
Sys.rename file backup;
Some (open_in backup)
end else None in
let cout = open_out file in
let fmt = formatter_of_out_channel cout in
let tname = m.mod_theory.Theory.th_name.Ident.id_string in
Debug.dprintf Pdriver.debug "extract module %s to file %s@." tname file;
List.iter (pr ?old ?fname pargs m fmt) mdecls;
close_out cout
let extract_to =
let visited = Ident.Hid.create 17 in
fun ?fname m ->
let cout, old = match opt_output with
| None ->
let tname = m.mod_theory.Theory.th_name.Ident.id_string in
Debug.dprintf Pdriver.debug "extract module %s to standard output" tname;
stdout, None
| Some f ->
let file = Filename.concat f (fg ?fname m) in
let tname = m.mod_theory.Theory.th_name.Ident.id_string in
Debug.dprintf Pdriver.debug "extract module %s to file %s@." tname file;
let old = if Sys.file_exists file then begin
let backup = file ^ ".bak" in
Sys.rename file backup;
Some (open_in backup) end else None in
open_out file, old in
let fmt = formatter_of_out_channel stdout in
let recursive = opt_recurs = Recursive in
List.iter (pr pargs ?old ?fname recursive m fmt) mdecls;
if cout <> stdout then close_out cout
let translate_module =
let memo = Ident.Hid.create 16 in
fun m ->
let name = m.mod_theory.Theory.th_name in
if not (Ident.Hid.mem visited name) then begin
Ident.Hid.add visited name ();
extract_to ?fname m
end
try Ident.Hid.find memo name with Not_found ->
let pm, info = Translate.module_ m in
let pm = Transform.module_ info pm in
Ident.Hid.add memo name pm;
pm
let extract_to ?fname ?decl m =
let mdecls = match decl with
| None -> (translate_module m).ML.mod_decl
| Some d -> List.map fst (Translate.pdecl_m m d) in
print_mdecls ?fname m mdecls
let rec use_iter f l =
List.iter
......@@ -157,33 +154,54 @@ let do_extract_module_from fname mm m =
eprintf "Module '%s' not found in file '%s'.@." m fname;
exit 1
let do_extract_symbol_from fname mm m s = () (*TODO*)
let get_symbol ns find str_symbol =
try let symbol = find ns [str_symbol] in Some symbol
with Not_found -> None
let do_extract_symbol_from fname mlw_file m str_symbol =
let pmod =
try Mstr.find m mlw_file with Not_found ->
eprintf "Module '%s' not found in the file '%s'.@." m fname;
exit 1 in
let ns = pmod.mod_export in
let id = match get_symbol ns ns_find_rs str_symbol with
| Some rs -> rs.Expr.rs_name
| None -> (* creative indentation *)
begin match get_symbol ns ns_find_its str_symbol with
| Some its -> its.Ity.its_ts.Ty.ts_name
| None -> (* creative indentation *)
begin match get_symbol ns ns_find_xs str_symbol with
| Some xs -> xs.Ity.xs_name
| None ->
eprintf "Symbol '%s' not found in module '%s' of file '%s'.@."
str_symbol m fname;
exit 1
end end in
let decl = Ident.Mid.find id pmod.mod_known in
extract_to ~fname ~decl pmod
let read_mlw_file ?format env fname =
let cin = open_in fname in
let mm = Env.read_channel ?format mlw_language env fname cin in
close_in cin;
mm
let do_local_extract target =
let env = opt_driver.Pdriver.drv_env in
let format = !opt_parser in
match target with
| File fname -> eprintf "ici@.";
let cin = open_in fname in
eprintf "before format@.";
let mm = Env.read_channel ?format mlw_language env fname cin in
eprintf "after format@.";
| File fname ->
let mm = read_mlw_file ?format env fname in
let do_m _ m = do_extract_module ~fname m in
Mstr.iter do_m mm;
close_in cin
| Module (fname, m) -> eprintf "ici2@.";
Mstr.iter do_m mm
| Module (fname, m) ->
let fname = fname ^ ".mlw" in
let mm = read_mlw_file ?format env fname in
do_extract_module_from fname mm m
| Symbol (fname, m, s) ->
let fname = fname ^ ".mlw" in
let cin = open_in fname in
eprintf "before format@.";
let mm = Env.read_channel ?format mlw_language env fname cin in
eprintf "after@.";
do_extract_module_from fname mm m;
close_in cin
| Symbol (fname, m, s) -> eprintf "ici3@.";
let cin = open_in fname in
let mm = Env.read_channel ?format mlw_language env fname cin in
do_extract_symbol_from fname mm m s;
close_in cin
let mm = read_mlw_file ?format env fname in
do_extract_symbol_from fname mm m s
let do_input = function
| None -> assert false (*TODO*)
......@@ -197,13 +215,16 @@ let toextract = ref []
let rec visit id =
if not (Hid.mem id visited) then begin
let d = Hid.find Compile.knownmap id in
let p = restore_path id in
let m = ... module Why3 ... in
let m = translate_module m in
let d = Hid.find m.mod_known id in
ML.iter_deps visit d;
Hid.add visited id ();
toextract := id :: !toextract
end
let monolithic () =
let flat_extraction () =
(* TODO call visit on all ids to extract *)
let (fg,pargs,pr) = Pdriver.lookup_printer opt_driver in
let extract id =
......@@ -215,9 +236,6 @@ let monolithic () =
let () =
try
Queue.iter do_input opt_queue;
(* begin match opt_recurs with *)
(* | Monolithic -> (\* monolithic () *\) assert false (\*TODO*\) *)
(* | Recursive | SingleModule -> () end *)
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
......
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