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. --- kernel/mod_typing.mli | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) (limited to 'kernel/mod_typing.mli') diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index bc0e20205..d07d59dd9 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -14,9 +14,18 @@ open Names (** Main functions for translating module entries *) +(** [translate_module] produces a [module_body] out of a [module_entry]. + In the output fields: + - [mod_expr] is [Abstract] for a [MType] entry, or [Algebraic] for [MExpr]. + - [mod_type_alg] is [None] only for a [MExpr] without explicit signature. +*) + val translate_module : env -> module_path -> inline -> module_entry -> module_body +(** [translate_modtype] produces a [module_type_body] whose [mod_type_alg] + cannot be [None] (and of course [mod_expr] is [Abstract]). *) + val translate_modtype : env -> module_path -> inline -> module_type_entry -> module_type_body @@ -24,20 +33,21 @@ val translate_modtype : - We translate to a module when a [module_path] is given, otherwise to a module type. - The first output is the expanded signature - - The second output is the algebraic expression, kept for the extraction. - It is never None when translating to a module, but for module type - it could not be contain applications or functors. -*) + - The second output is the algebraic expression, kept mostly for + the extraction. *) type 'alg translation = - module_signature * 'alg option * delta_resolver * Univ.ContextSet.t + module_signature * 'alg * delta_resolver * Univ.ContextSet.t val translate_mse : env -> module_path option -> inline -> module_struct_entry -> module_alg_expr translation +(** From an already-translated (or interactive) implementation and + an (optional) signature entry, produces a final [module_body] *) + val finalize_module : - env -> module_path -> module_expression translation -> + env -> module_path -> (module_expression option) translation -> (module_type_entry * inline) option -> module_body @@ -46,4 +56,4 @@ val finalize_module : val translate_mse_incl : bool -> env -> module_path -> inline -> module_struct_entry -> - module_alg_expr translation + unit translation -- cgit v1.2.3