Commit 0dbd3f2e authored by Mário Pereira's avatar Mário Pereira

Extraction of sub-modules (wip)

parent 724c540b
......@@ -45,16 +45,23 @@ module ML = struct
open Expr
open Mltree
let get_decl_name = function
let rec get_decl_name = function
| Dtype itdefl -> List.map (fun {its_name = id} -> id) itdefl
| Dlet (Lrec rdef) -> List.map (fun {rec_sym = rs} -> rs.rs_name) rdef
| Dlet (Lvar ({pv_vs={vs_name=id}}, _))
| Dlet (Lsym ({rs_name=id}, _, _, _))
| Dexn ({xs_name=id}, _) -> [id]
| Dmodule (_, dl) -> List.concat (List.map get_decl_name dl)
| Dclone _ -> [] (* FIXME? *)
let add_known_decl decl k_map id =
Mid.add id decl k_map
let rec add_known_decl decl k_map id =
match decl with (* FIXME? keep this block *)
| Dmodule (_, dl) ->
let add_decl k_map d =
let idl = get_decl_name d in
List.fold_left (add_known_decl d) k_map idl in
List.fold_left add_decl k_map dl
| _ -> Mid.add id decl k_map
let rec iter_deps_ty f = function
| Tvar _ -> ()
......@@ -158,7 +165,7 @@ module ML = struct
| Dlet (Lvar (_, e)) -> iter_deps_expr f e
| Dexn (_, None) -> ()
| Dexn (_, Some ty) -> iter_deps_ty f ty
| Dclone (_, dl) -> List.iter (iter_deps f) dl
| Dclone (_, dl) | Dmodule (_, dl) -> List.iter (iter_deps f) dl
let mk_expr e_node e_ity e_effect e_label =
{ e_node = e_node; e_ity = e_ity; e_effect = e_effect; e_label = e_label; }
......@@ -729,13 +736,15 @@ module Translate = struct
else [Mltree.Dexn (xs, Some (mlty_of_ity xs.xs_mask xs.xs_ity))]
let pdecl_m m pd =
let info = { Mltree.from_mod = Some m; Mltree.from_km = m.mod_known; } in
let info = { Mltree.from_mod = Some m; Mltree.from_km = m.mod_known; } in
pdecl Sid.empty info pd
(* unit module declarations *)
let rec mdecl pids info = function
| Udecl pd -> pdecl pids info pd
| Uscope (_, l) -> List.concat (List.map (mdecl pids info) l)
| Uscope (_, ([Uuse _] | [Uclone _])) -> []
| Uscope (s, dl) -> let dl = List.concat (List.map (mdecl pids info) dl) in
[Mltree.Dmodule (s, dl)]
| Uuse _ | Uclone _ | Umeta _ -> []
let abstract_or_alias_type itd =
......@@ -786,13 +795,12 @@ module Translate = struct
let pids = List.fold_left ids_of_params Sid.empty params in
let mod_decl = List.concat (List.map (mdecl pids from) m.mod_units) in
let mod_decl = List.map (make_param from) params @ mod_decl in
let add known_map decl =
let idl = ML.get_decl_name decl in
let add_decl known_map decl = let idl = ML.get_decl_name decl in
List.fold_left (ML.add_known_decl decl) known_map idl in
let mod_known = List.fold_left add Mid.empty mod_decl in {
let mod_known = List.fold_left add_decl Mid.empty mod_decl in {
Mltree.mod_from = from;
Mltree.mod_decl = mod_decl;
Mltree.mod_known = mod_known
Mltree.mod_known = mod_known;
}
(* let () = Exn_printer.register (fun fmt e -> match e with *)
......@@ -926,12 +934,12 @@ module Transform = struct
let rec_exp, spv = expr info subst r.rec_exp in
{ r with rec_exp = rec_exp }, spv
let pdecl info = function
let rec pdecl info = function
| Dtype _ | Dexn _ | Dclone _ as d -> d
| Dmodule (id, dl) -> let dl = List.map (pdecl info) dl in Dmodule (id, dl)
| Dlet def ->
(* for top-level symbols we can forget the set of inlined variables *)
let e, _ = let_def info Mpv.empty def in
Dlet e
let e, _ = let_def info Mpv.empty def in Dlet e
let module_ m =
let mod_decl = List.map (pdecl m.mod_from) m.mod_decl in
......
......@@ -89,19 +89,22 @@ type decl =
| Dlet of let_def
| Dexn of xsymbol * ty option
| Dclone of ident * decl list
| Dmodule of string * decl list
(*
| Dfunctor of ident * (ident * decl list) list * decl list
*)
type known_map = decl Mid.t
type namespace = (ident * decl list) list
type from_module = {
from_mod: Pmodule.pmodule option;
from_km : Pdecl.known_map;
}
type known_map = decl Mid.t
type pmodule = {
mod_from : from_module;
mod_decl : decl list;
mod_known : known_map;
mod_from : from_module; (* information about original Why3 module *)
mod_decl : decl list; (* module declarations *)
mod_known : known_map; (* known identifiers *)
}
......@@ -85,26 +85,36 @@ module Print = struct
let s = id_unique iprinter id in
fprintf fmt "%s" s
let is_local_id info id =
let is_local_id info id = (* FIXME : take scopes into account *)
Sid.mem id info.info_current_th.th_local ||
Opt.fold (fun _ m -> Sid.mem id m.Pmodule.mod_local)
false info.info_current_mo
exception Local
let mk_s ~sanitizer ~sanitize q sep =
let s = String.concat sep q in
let s = if sanitize then
let s = Ident.sanitizer char_to_alpha char_to_alnumus s in sanitizer s
else s in
if is_ocaml_keyword s then s ^ "_renamed" else s (* FIXME *)
let print_qident ~sanitizer info fmt id =
try
if info.flat || is_local_id info id then raise Not_found;
let lp, t, q =
try Pmodule.restore_path id
with Not_found -> Theory.restore_path id in
let s = String.concat "__" q in
let s = Ident.sanitizer char_to_alpha char_to_alnumus s in
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
try if info.flat then raise Not_found;
if is_local_id info id then raise Local;
let p, t, q = try Pmodule.restore_path id with Not_found ->
Theory.restore_path id in
let s = mk_s ~sanitizer ~sanitize:true q "__" in
let fname = if p = [] then info.info_fname else None in
let m = Strings.capitalize (module_name ?fname p t) in
fprintf fmt "%s.%s" m s
with Not_found ->
let s = id_unique ~sanitizer iprinter id in
with
| Not_found -> let s = id_unique ~sanitizer iprinter id in
fprintf fmt "%s" s
| Local -> let _, _, q = try Pmodule.restore_path id with Not_found ->
Theory.restore_path id in
List.iter (fun q -> eprintf "%s. " q) q; eprintf "@.";
let s = mk_s ~sanitizer ~sanitize:false q "." in
fprintf fmt "%s" s
let print_lident = print_qident ~sanitizer:Strings.uncapitalize
......@@ -525,18 +535,19 @@ module Print = struct
(if fst then "type" else "and") print_tv_args its.its_args
(print_lident info) its.its_name print_def its.its_def
let print_decl info fmt = function
let rec print_decl info fmt = function
| Dlet ldef ->
print_let_def info fmt ldef;
fprintf fmt "@\n"
print_let_def info fmt ldef
| Dtype dl ->
print_list_next newline (print_type_decl info) fmt dl;
fprintf fmt "@\n"
print_list_next newline (print_type_decl info) fmt dl
| Dexn (xs, None) ->
fprintf fmt "exception %a@\n" (print_uident info) xs.xs_name
fprintf fmt "exception %a" (print_uident info) xs.xs_name
| Dexn (xs, Some t)->
fprintf fmt "@[<hov 2>exception %a of %a@]@\n"
fprintf fmt "@[<hov 2>exception %a of %a@]"
(print_uident info) xs.xs_name (print_ty ~paren:true info) t
| Dmodule (s, dl) ->
fprintf fmt "module %s =@\n@[<hov 2>struct@\n%a@]@\nend"
s (print_list newline (print_decl info)) dl
| Dclone _ ->
assert false (*TODO*)
......@@ -567,8 +578,8 @@ let print_decl =
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
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
......
......@@ -146,7 +146,8 @@ let print_mdecls ?fname m mdecls =
let cout, old = get_cout_old fg m ?fname in
let fmt = formatter_of_out_channel cout in
let flat = opt_modu_flat = Flat in
List.iter (pr pargs ?old ?fname ~flat m fmt) mdecls;
let pr_decl fmt d = fprintf fmt "%a" (pr pargs ?old ?fname ~flat m) d in
Pp.print_list Pp.newline pr_decl fmt mdecls;
if cout <> stdout then close_out cout end
let find_module_path mm path m = match path with
......@@ -167,7 +168,7 @@ let translate_module =
Ident.Hid.add memo name pm;
pm
let not_extractable_theories = ["why3"; "map";]
let not_extractable_theories = ["why3"; "map"; ]
let is_not_extractable_theory =
let h = Hstr.create 16 in
......@@ -204,11 +205,6 @@ let rec do_extract_module ?fname m =
end;
extract_to ?fname m
(* let do_global_extract (_,p,t) = *)
(* let env = opt_driver.Pdriver.drv_env in *)
(* let m = read_module env p t in *)
(* do_extract_module m *)
let do_extract_module_from fname mm m =
try
let m = Mstr.find m mm in do_extract_module ~fname m
......@@ -311,10 +307,8 @@ let flat_extraction mm = function
let () =
try
match opt_modu_flat with
| Modular ->
Queue.iter do_modular opt_queue
| Flat ->
let mm = Queue.fold flat_extraction Mstr.empty opt_queue in
| Modular -> 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
let visit_id id _ = visit ~recurs:true mm id in
Ident.Mid.iter visit_id tm.Mltree.mod_known in
......@@ -340,14 +334,8 @@ let () =
let idl = match opt_rec_single with
| Single -> List.filter is_local idl
| Recursive -> idl in
List.iter (extract fmt) idl;
Pp.print_list Pp.newline extract fmt idl;
if cout <> stdout then close_out cout
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3extract.opt"
End:
*)
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