Commit 6babfc4a authored by Mário Pereira's avatar Mário Pereira

Extraction: fixed problem with order in file extraction

parent a2bfc253
......@@ -100,8 +100,8 @@ module Print = struct
let s = sanitizer s in
let s = if is_ocaml_keyword s then s ^ "_renamed" else s in (* FIXME *)
let fname = if lp = [] then info.info_fname else None in
let m = Strings.capitalize (module_name ?fname lp t) in
fprintf fmt "%s.%s" m s
let m = Strings.capitalize (module_name ?fname lp t) in
fprintf fmt "%s.%s" m s
with Not_found ->
let s = id_unique ~sanitizer iprinter id in
fprintf fmt "%s" s
......@@ -325,7 +325,7 @@ module Print = struct
else
let ty_args = List.map (fun (_, ty, _) -> ty) args in
let id_args = List.map (fun (id, _, _) -> id) args in
fprintf fmt ": @[%a@]. @[%a@] ->@ %a@ =@ fun @[%a@]@ ->"
fprintf fmt ": @[@[%a@]. @[%a@] ->@ %a@ =@ @[fun @[%a@]@ ->@]@]"
print_svar s
(print_list arrow (print_ty ~paren:true info)) ty_args
(print_ty ~paren:true info) res
......@@ -533,28 +533,34 @@ module Print = struct
assert false (*TODO*)
let print_decl info fmt decl =
(* avoids printing the same decl for mutually recursive decls *)
let memo = Hashtbl.create 64 in
let decl_name = get_decl_name decl in
let decide_print id =
if query_syntax info.info_syn id = None then begin
print_decl info fmt decl;
if query_syntax info.info_syn id = None &&
not (Hashtbl.mem memo decl) then begin
Hashtbl.add memo decl (); print_decl info fmt decl;
fprintf fmt "@." end in
List.iter decide_print decl_name
end
let print_decl pargs ?old ?fname ~flat ({mod_theory = th} as m) fmt d =
ignore (old);
let info = {
info_syn = pargs.Pdriver.syntax;
info_convert = pargs.Pdriver.converter;
info_current_th = th;
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;
flat = flat;
} in
Print.print_decl info fmt d
let print_decl =
let memo = Hashtbl.create 16 in
fun pargs ?old ?fname ~flat ({mod_theory = th} as m) fmt d ->
ignore (old);
let info = {
info_syn = pargs.Pdriver.syntax;
info_convert = pargs.Pdriver.converter;
info_current_th = th;
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;
flat = flat;
} in
if not (Hashtbl.mem memo d) then begin
Hashtbl.add memo d (); Print.print_decl info fmt d end
let fg ?fname m =
let mod_name = m.mod_theory.th_name.id_string in
......
......@@ -150,15 +150,12 @@ let print_mdecls ?fname m mdecls =
if cout <> stdout then close_out cout end
let find_module_path mm path m = match path with
| [] ->
Mstr.find m mm
| path ->
let mm = Env.read_library Pmodule.mlw_language env path in
| [] -> Mstr.find m mm
| path -> let mm = Env.read_library Pmodule.mlw_language env path in
Mstr.find m mm
let find_module_id mm id =
let (path, m, _) = Pmodule.restore_path id in
find_module_path mm path m
let (path, m, _) = Pmodule.restore_path id in find_module_path mm path m
let translate_module =
let memo = Ident.Hid.create 16 in
......@@ -286,9 +283,9 @@ let rec visit mm id =
with Not_found -> ()
end
let visit mm id =
if opt_rec_single = Recursive then visit mm id
else toextract := id :: !toextract
(* let visit mm id = *)
(* if opt_rec_single = Recursive then visit mm id *)
(* else toextract := id :: !toextract *)
let flat_extraction mm = function
| File fname ->
......@@ -299,8 +296,6 @@ let flat_extraction mm = function
eprintf "multiple module '%s'; use -L . instead@." s;
exit 1
end;
let tm = translate_module m in
Ident.Mid.iter (fun id _ -> visit mm id) tm.ML.mod_known;
Mstr.add s m mm in
Mstr.fold do_m mmf mm
| Module (path, m) ->
......@@ -322,6 +317,9 @@ let () =
Queue.iter do_modular opt_queue
| Flat ->
let mm = Queue.fold flat_extraction Mstr.empty opt_queue in
let visit_m _ m = let tm = translate_module m in
Ident.Mid.iter (fun id _ -> visit mm id) tm.ML.mod_known in
Mstr.iter visit_m mm;
let (_fg, pargs, pr) = Pdriver.lookup_printer opt_driver in
let cout = match opt_output with
| None -> stdout
......
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