From 5484ba750ef4526dde29ffc1474ca5d145f3ec04 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sat, 4 Feb 2017 01:01:05 +0100 Subject: Extraction: fix complexity issue #5310 A double call to pp_module_type inside Ocaml.pp_specif was causing an complexity blowup when pretty-printing heavily modular extracted code. I wasn't able to figure out why this double call is there. It could be the leftover of some intermediate work in 2007 before commit 350398eae (which introduced global printing phases Pre/Impl/Intf). Anyway I'm reasonably sure that today these two pp_module_type calls produce the exact same pretty-printed signature (even if there's a large bunch of imperative states around). Moreover, this duplicated signature is actually slightly wrong: when we alias a module M with a unambiguous name like Coq__123, the type of Coq__123 should not be an exact copy of the type of M, but rather a "strengthened" version of it (with equality between inductive types). So the best solution is now to use this funny feature of OCaml introduced in 3.12 : module Coq__123 : module type of struct include M end This "module type of struct include" is slightly awkward, but short, correct, and trivial to produce :-). And I doubt anybody will object to the (rare) use of some 3.12 features in extracted code of 2017... --- plugins/extraction/ocaml.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'plugins/extraction/ocaml.ml') diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 1c29a9bc24..5d10cb939d 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -618,12 +618,13 @@ let rec pp_specif = function with Not_found -> pp_spec s) | (l,Smodule mt) -> let def = pp_module_type [] mt in - let def' = pp_module_type [] mt in let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 (str "module " ++ name ++ str " :" ++ fnl () ++ def) ++ (try let ren = Common.check_duplicate (top_visible_mp ()) l in - fnl () ++ hov 1 (str ("module "^ren^" :") ++ fnl () ++ def') + fnl () ++ + hov 1 (str ("module "^ren^" :") ++ spc () ++ + str "module type of struct include " ++ name ++ str " end") with Not_found -> Pp.mt ()) | (l,Smodtype mt) -> let def = pp_module_type [] mt in -- cgit v1.2.3 From af4962a9211a707943e7b0627439a731c3e7d23f Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sat, 4 Feb 2017 19:29:15 +0100 Subject: Extraction : get_duplicates (via option) instead of check_duplicates (via Not_found) This clarifies the execution flow --- plugins/extraction/ocaml.ml | 45 +++++++++++++++++++++------------------------ 1 file changed, 21 insertions(+), 24 deletions(-) (limited to 'plugins/extraction/ocaml.ml') diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 5d10cb939d..31e481d123 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -610,30 +610,29 @@ let pp_alias_spec ren = function let rec pp_specif = function | (_,Spec (Sval _ as s)) -> pp_spec s | (l,Spec s) -> - (try - let ren = Common.check_duplicate (top_visible_mp ()) l in + (match Common.get_duplicate (top_visible_mp ()) l with + | None -> pp_spec s + | Some ren -> hov 1 (str ("module "^ren^" : sig") ++ fnl () ++ pp_spec s) ++ fnl () ++ str "end" ++ fnl () ++ - pp_alias_spec ren s - with Not_found -> pp_spec s) + pp_alias_spec ren s) | (l,Smodule mt) -> let def = pp_module_type [] mt in let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 (str "module " ++ name ++ str " :" ++ fnl () ++ def) ++ - (try - let ren = Common.check_duplicate (top_visible_mp ()) l in + (match Common.get_duplicate (top_visible_mp ()) l with + | None -> Pp.mt () + | Some ren -> fnl () ++ hov 1 (str ("module "^ren^" :") ++ spc () ++ - str "module type of struct include " ++ name ++ str " end") - with Not_found -> Pp.mt ()) + str "module type of struct include " ++ name ++ str " end")) | (l,Smodtype mt) -> let def = pp_module_type [] mt in let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++ - (try - let ren = Common.check_duplicate (top_visible_mp ()) l in - fnl () ++ str ("module type "^ren^" = ") ++ name - with Not_found -> Pp.mt ()) + (match Common.get_duplicate (top_visible_mp ()) l with + | None -> Pp.mt () + | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name) and pp_module_type params = function | MTident kn -> @@ -682,12 +681,12 @@ let is_short = function MEident _ | MEapply _ -> true | _ -> false let rec pp_structure_elem = function | (l,SEdecl d) -> - (try - let ren = Common.check_duplicate (top_visible_mp ()) l in + (match Common.get_duplicate (top_visible_mp ()) l with + | None -> pp_decl d + | Some ren -> hov 1 (str ("module "^ren^" = struct") ++ fnl () ++ pp_decl d) ++ fnl () ++ str "end" ++ fnl () ++ - pp_alias_decl ren d - with Not_found -> pp_decl d) + pp_alias_decl ren d) | (l,SEmodule m) -> let typ = (* virtual printing of the type, in order to have a correct mli later*) @@ -700,18 +699,16 @@ let rec pp_structure_elem = function hov 1 (str "module " ++ name ++ typ ++ str " =" ++ (if is_short m.ml_mod_expr then spc () else fnl ()) ++ def) ++ - (try - let ren = Common.check_duplicate (top_visible_mp ()) l in - fnl () ++ str ("module "^ren^" = ") ++ name - with Not_found -> mt ()) + (match Common.get_duplicate (top_visible_mp ()) l with + | Some ren -> fnl () ++ str ("module "^ren^" = ") ++ name + | None -> mt ()) | (l,SEmodtype m) -> let def = pp_module_type [] m in let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++ - (try - let ren = Common.check_duplicate (top_visible_mp ()) l in - fnl () ++ str ("module type "^ren^" = ") ++ name - with Not_found -> mt ()) + (match Common.get_duplicate (top_visible_mp ()) l with + | None -> mt () + | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name) and pp_module_expr params = function | MEident mp -> pp_modname mp -- cgit v1.2.3 From 8ef3bc0e8a65b3a0338da39aa54cd75b1c2c1bb7 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sat, 4 Feb 2017 19:55:18 +0100 Subject: Extraction: simplify the generated code for difficult name conflicts No more pp_alias_spec et pp_alias_decl. Instead, we use "include" and "module type of". The extracted code might hence need OCaml 3.12 (quite rarely) --- plugins/extraction/ocaml.ml | 33 ++------------------------------- 1 file changed, 2 insertions(+), 31 deletions(-) (limited to 'plugins/extraction/ocaml.ml') diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 31e481d123..404939cff9 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -555,24 +555,6 @@ let pp_decl = function | Dfix (rv,defs,typs) -> pp_Dfix (rv,defs,typs) -let pp_alias_decl ren = function - | Dind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren } - | Dtype (r, l, _) -> - let name = pp_global Type r in - let l = rename_tvars keywords l in - let ids = pp_parameters l in - hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ - str (ren^".") ++ name) - | Dterm (r, a, t) -> - let name = pp_global Term r in - hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) - | Dfix (rv, _, _) -> - prvecti (fun i r -> if is_inline_custom r then mt () else - let name = pp_global Term r in - hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) ++ - fnl ()) - rv - let pp_spec = function | Sval (r,_) when is_inline_custom r -> mt () | Stype (r,_,_) when is_inline_custom r -> mt () @@ -597,16 +579,6 @@ let pp_spec = function in hov 2 (str "type " ++ ids ++ name ++ def) -let pp_alias_spec ren = function - | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren } - | Stype (r,l,_) -> - let name = pp_global Type r in - let l = rename_tvars keywords l in - let ids = pp_parameters l in - hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ - str (ren^".") ++ name) - | Sval _ -> assert false - let rec pp_specif = function | (_,Spec (Sval _ as s)) -> pp_spec s | (l,Spec s) -> @@ -615,7 +587,7 @@ let rec pp_specif = function | Some ren -> hov 1 (str ("module "^ren^" : sig") ++ fnl () ++ pp_spec s) ++ fnl () ++ str "end" ++ fnl () ++ - pp_alias_spec ren s) + str ("include module type of struct include "^ren^" end")) | (l,Smodule mt) -> let def = pp_module_type [] mt in let name = pp_modname (MPdot (top_visible_mp (), l)) in @@ -685,8 +657,7 @@ let rec pp_structure_elem = function | None -> pp_decl d | Some ren -> hov 1 (str ("module "^ren^" = struct") ++ fnl () ++ pp_decl d) ++ - fnl () ++ str "end" ++ fnl () ++ - pp_alias_decl ren d) + fnl () ++ str "end" ++ fnl () ++ str ("include "^ren)) | (l,SEmodule m) -> let typ = (* virtual printing of the type, in order to have a correct mli later*) -- cgit v1.2.3 From df14dac0e6e9d9819dcc3b1601e150af7c142597 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sun, 5 Feb 2017 02:12:36 +0100 Subject: Extraction cosmetic: no whitespaces in printing empty modules --- plugins/extraction/ocaml.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'plugins/extraction/ocaml.ml') diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 404939cff9..d89bf95ee8 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -625,8 +625,10 @@ and pp_module_type params = function let l = List.rev l in pop_visible (); str "sig" ++ fnl () ++ - v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ - fnl () ++ str "end" + (if List.is_empty l then mt () + else + v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ()) + ++ str "end" | MTwith(mt,ML_With_type(idl,vl,typ)) -> let ids = pp_parameters (rename_tvars keywords vl) in let mp_mt = msid_of_mt mt in @@ -701,8 +703,10 @@ and pp_module_expr params = function let l = List.rev l in pop_visible (); str "struct" ++ fnl () ++ - v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ - fnl () ++ str "end" + (if List.is_empty l then mt () + else + v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ()) + ++ str "end" let rec prlist_sep_nonempty sep f = function | [] -> mt () -- cgit v1.2.3