From 5122a39888cfc6afd2383d59465324dd67b69f4a Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 21 Dec 2015 18:56:43 +0100 Subject: Inclusion of functors with restricted signature is now forbidden (fix #3746) The previous behavior was to include the interface of such a functor, possibly leading to the creation of unexpected axioms, see bug report #3746. In the case of non-functor module with restricted signature, we could simply refer to the original objects (strengthening), but for a functor, the inner objects have no existence yet. As said in the new error message, a simple workaround is hence to first instantiate the functor, then include the local instance: Module LocalInstance := Funct(Args). Include LocalInstance. By the way, the mod_type_alg field is now filled more systematically, cf new comments in declarations.mli. This way, we could use it to know whether a module had been given a restricted signature (via ":"). Earlier, some mod_type_alg were None in situations not handled by the extraction (MEapply of module type). Some code refactoring on the fly. --- plugins/extraction/extract_env.ml | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'plugins/extraction/extract_env.ml') diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 7014df83f..996428033 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -177,8 +177,7 @@ let factor_fix env l cb msb = let expand_mexpr env mp me = let inl = Some (Flags.get_inline_level()) in - let sign,_,_,_ = Mod_typing.translate_mse env (Some mp) inl me in - sign + Mod_typing.translate_mse env (Some mp) inl me (** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def]. To check with Elie. *) @@ -231,10 +230,9 @@ let rec extract_structure_spec env mp reso = function (* From [module_expression] to specifications *) -(* Invariant: the [me] given to [extract_mexpr_spec] should either come - from a [mod_type] or [type_expr] field, or their [_alg] counterparts. - This way, any encountered [MEident] should be a true module type. -*) +(* Invariant: the [me_alg] given to [extract_mexpr_spec] and + [extract_mexpression_spec] should come from a [mod_type_alg] field. + This way, any encountered [MEident] should be a true module type. *) and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with | MEident mp -> Visit.add_mp_all mp; MTident mp @@ -247,7 +245,9 @@ and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with | MEwith(me',WithMod(idl,mp))-> Visit.add_mp_all mp; MTwith(extract_mexpr_spec env mp1 (me_struct,me'), ML_With_module(idl,mp)) - | MEapply _ -> extract_msignature_spec env mp1 no_delta (*TODO*) me_struct + | MEapply _ -> + (* No higher-order module type in OCaml : we use the expanded version *) + extract_msignature_spec env mp1 no_delta (*TODO*) me_struct and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with | MoreFunctor (mbid, mtb, me_alg') -> @@ -335,7 +335,8 @@ and extract_mexpr env mp = function (* In Haskell/Scheme, we expand everything. For now, we also extract everything, dead code will be removed later (see [Modutil.optimize_struct]. *) - extract_msignature env mp no_delta ~all:true (expand_mexpr env mp me) + let sign,_,delta,_ = expand_mexpr env mp me in + extract_msignature env mp delta ~all:true sign | MEident mp -> if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false; Visit.add_mp_all mp; Miniml.MEident mp -- cgit v1.2.3