aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2015-12-21 18:56:43 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2015-12-22 15:05:47 +0100
commit5122a39888cfc6afd2383d59465324dd67b69f4a (patch)
treeecfecd5ee4f2d89b6d61ab3638a30dfce6048af2 /kernel
parent840cefca77a48ad68641539cd26d8d2e8c9dc031 (diff)
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.
Diffstat (limited to 'kernel')
-rw-r--r--kernel/declarations.mli23
-rw-r--r--kernel/mod_typing.ml128
-rw-r--r--kernel/mod_typing.mli24
-rw-r--r--kernel/modops.ml7
-rw-r--r--kernel/modops.mli5
-rw-r--r--kernel/safe_typing.ml2
6 files changed, 112 insertions, 77 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index dc5c17a75..0b8272b43 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -238,17 +238,26 @@ and module_body =
{ mod_mp : module_path; (** absolute path of the module *)
mod_expr : module_implementation; (** implementation *)
mod_type : module_signature; (** expanded type *)
- (** algebraic type, kept if it's relevant for extraction *)
- mod_type_alg : module_expression option;
- (** set of all universes constraints in the module *)
- mod_constraints : Univ.ContextSet.t;
- (** quotiented set of equivalent constants and inductive names *)
- mod_delta : Mod_subst.delta_resolver;
+ mod_type_alg : module_expression option; (** algebraic type *)
+ mod_constraints : Univ.ContextSet.t; (**
+ set of all universes constraints in the module *)
+ mod_delta : Mod_subst.delta_resolver; (**
+ quotiented set of equivalent constants and inductive names *)
mod_retroknowledge : Retroknowledge.action list }
+(** For a module, there are five possible situations:
+ - [Declare Module M : T] then [mod_expr = Abstract; mod_type_alg = Some T]
+ - [Module M := E] then [mod_expr = Algebraic E; mod_type_alg = None]
+ - [Module M : T := E] then [mod_expr = Algebraic E; mod_type_alg = Some T]
+ - [Module M. ... End M] then [mod_expr = FullStruct; mod_type_alg = None]
+ - [Module M : T. ... End M] then [mod_expr = Struct; mod_type_alg = Some T]
+ And of course, all these situations may be functors or not. *)
+
(** A [module_type_body] is just a [module_body] with no
implementation ([mod_expr] always [Abstract]) and also
- an empty [mod_retroknowledge] *)
+ an empty [mod_retroknowledge]. Its [mod_type_alg] contains
+ the algebraic definition of this module type, or [None]
+ if it has been built interactively. *)
and module_type_body = module_body
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index bd7ee7b33..8a1634881 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -21,7 +21,7 @@ open Modops
open Mod_subst
type 'alg translation =
- module_signature * 'alg option * delta_resolver * Univ.ContextSet.t
+ module_signature * 'alg * delta_resolver * Univ.ContextSet.t
let rec mp_from_mexpr = function
| MEident mp -> mp
@@ -183,8 +183,11 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
begin
try
let mtb_old = module_type_of_module old in
- Univ.ContextSet.add_constraints (Subtyping.check_subtypes env' mtb_mp1 mtb_old) old.mod_constraints
- with Failure _ -> error_incorrect_with_constraint lab
+ let chk_cst = Subtyping.check_subtypes env' mtb_mp1 mtb_old in
+ Univ.ContextSet.add_constraints chk_cst old.mod_constraints
+ with Failure _ ->
+ (* TODO: where can a Failure come from ??? *)
+ error_incorrect_with_constraint lab
end
| Algebraic (NoFunctor (MEident(mp'))) ->
check_modpath_equiv env' mp1 mp';
@@ -238,104 +241,89 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
| Not_found -> error_no_such_label lab
| Reduction.NotConvertible -> error_incorrect_with_constraint lab
-let mk_alg_with alg wd = Option.map (fun a -> MEwith (a,wd)) alg
-
let check_with env mp (sign,alg,reso,cst) = function
|WithDef(idl,c) ->
let struc = destr_nofunctor sign in
let struc',c',cst' = check_with_def env struc (idl,c) mp reso in
- let alg' = mk_alg_with alg (WithDef (idl,(c',Univ.ContextSet.to_context cst'))) in
- (NoFunctor struc'),alg',reso, cst+++cst'
+ let wd' = WithDef (idl,(c',Univ.ContextSet.to_context cst')) in
+ NoFunctor struc', MEwith (alg,wd'), reso, cst+++cst'
|WithMod(idl,mp1) as wd ->
let struc = destr_nofunctor sign in
let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in
- let alg' = mk_alg_with alg wd in
- (NoFunctor struc'),alg',reso', cst+++cst'
+ NoFunctor struc', MEwith (alg,wd), reso', cst+++cst'
-let mk_alg_app mpo alg arg = match mpo, alg with
- | Some _, Some alg -> Some (MEapply (alg,arg))
- | _ -> None
+let translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
+ let farg_id, farg_b, fbody_b = destr_functor sign in
+ let mtb = module_type_of_module (lookup_module mp1 env) in
+ let cst2 = Subtyping.check_subtypes env mtb farg_b in
+ let mp_delta = discr_resolver mtb in
+ let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in
+ let subst = map_mbid farg_id mp1 mp_delta in
+ let body = subst_signature subst fbody_b in
+ let alg' = mkalg alg mp1 in
+ let reso' = subst_codom_delta_resolver subst reso in
+ body,alg',reso', Univ.ContextSet.add_constraints cst2 cst1
(** Translation of a module struct entry :
- 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 [SEBapply] or [SEBfunctor].
*)
+let mk_alg_app alg arg = MEapply (alg,arg)
+
let rec translate_mse env mpo inl = function
- |MEident mp1 ->
- let sign,reso = match mpo with
- |Some mp ->
- let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp false in
- mb.mod_type, mb.mod_delta
- |None ->
- let mtb = lookup_modtype mp1 env in
- mtb.mod_type, mtb.mod_delta
+ |MEident mp1 as me ->
+ let mb = match mpo with
+ |Some mp -> strengthen_and_subst_mb (lookup_module mp1 env) mp false
+ |None -> lookup_modtype mp1 env
in
- sign,Some (MEident mp1),reso,Univ.ContextSet.empty
+ mb.mod_type, me, mb.mod_delta, Univ.ContextSet.empty
|MEapply (fe,mp1) ->
- translate_apply env inl (translate_mse env mpo inl fe) mp1 (mk_alg_app mpo)
+ translate_apply env inl (translate_mse env mpo inl fe) mp1 mk_alg_app
|MEwith(me, with_decl) ->
assert (mpo == None); (* No 'with' syntax for modules *)
let mp = mp_from_mexpr me in
check_with env mp (translate_mse env None inl me) with_decl
-and translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
- let farg_id, farg_b, fbody_b = destr_functor sign in
- let mtb = module_type_of_module (lookup_module mp1 env) in
- let cst2 = Subtyping.check_subtypes env mtb farg_b in
- let mp_delta = discr_resolver mtb in
- let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in
- let subst = map_mbid farg_id mp1 mp_delta in
- let body = subst_signature subst fbody_b in
- let alg' = mkalg alg mp1 in
- let reso' = subst_codom_delta_resolver subst reso in
- body,alg',reso', Univ.ContextSet.add_constraints cst2 cst1
-
-let mk_alg_funct mpo mbid mtb alg = match mpo, alg with
- | Some _, Some alg -> Some (MoreFunctor (mbid,mtb,alg))
- | _ -> None
-
-let mk_mod mp e ty ty' cst reso =
+let mk_mod mp e ty cst reso =
{ mod_mp = mp;
mod_expr = e;
mod_type = ty;
- mod_type_alg = ty';
+ mod_type_alg = None;
mod_constraints = cst;
mod_delta = reso;
mod_retroknowledge = [] }
-let mk_modtype mp ty cst reso = mk_mod mp Abstract ty None cst reso
+let mk_modtype mp ty cst reso = mk_mod mp Abstract ty cst reso
let rec translate_mse_funct env mpo inl mse = function
|[] ->
let sign,alg,reso,cst = translate_mse env mpo inl mse in
- sign, Option.map (fun a -> NoFunctor a) alg, reso, cst
+ sign, NoFunctor alg, reso, cst
|(mbid, ty) :: params ->
let mp_id = MPbound mbid in
let mtb = translate_modtype env mp_id inl ([],ty) in
let env' = add_module_type mp_id mtb env in
let sign,alg,reso,cst = translate_mse_funct env' mpo inl mse params in
- let alg' = mk_alg_funct mpo mbid mtb alg in
+ let alg' = MoreFunctor (mbid,mtb,alg) in
MoreFunctor (mbid, mtb, sign), alg',reso, cst +++ mtb.mod_constraints
and translate_modtype env mp inl (params,mte) =
let sign,alg,reso,cst = translate_mse_funct env None inl mte params in
let mtb = mk_modtype (mp_from_mexpr mte) sign cst reso in
let mtb' = subst_modtype_and_resolver mtb mp in
- { mtb' with mod_type_alg = alg }
+ { mtb' with mod_type_alg = Some alg }
(** [finalize_module] :
- from an already-translated (or interactive) implementation
- and a signature entry, produce a final [module_expr] *)
+ from an already-translated (or interactive) implementation and
+ an (optional) signature entry, produces a final [module_body] *)
let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
|None ->
let impl = match alg with Some e -> Algebraic e | None -> FullStruct in
- mk_mod mp impl sign None cst reso
+ mk_mod mp impl sign cst reso
|Some (params_mte,inl) ->
let res_mtb = translate_modtype env mp inl params_mte in
let auto_mtb = mk_modtype mp sign Univ.ContextSet.empty reso in
@@ -344,33 +332,59 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
{ res_mtb with
mod_mp = mp;
mod_expr = impl;
- (** cst from module body typing, cst' from subtyping,
- and constraints from module type. *)
- mod_constraints = Univ.ContextSet.add_constraints cst' (cst +++ res_mtb.mod_constraints) }
+ (** cst from module body typing,
+ cst' from subtyping,
+ constraints from module type. *)
+ mod_constraints =
+ Univ.ContextSet.add_constraints cst' (cst +++ res_mtb.mod_constraints) }
let translate_module env mp inl = function
|MType (params,ty) ->
let mtb = translate_modtype env mp inl (params,ty) in
module_body_of_type mp mtb
|MExpr (params,mse,oty) ->
- let t = translate_mse_funct env (Some mp) inl mse params in
+ let (sg,alg,reso,cst) = translate_mse_funct env (Some mp) inl mse params in
let restype = Option.map (fun ty -> ((params,ty),inl)) oty in
- finalize_module env mp t restype
+ finalize_module env mp (sg,Some alg,reso,cst) restype
+
+(** We now forbid any Include of functors with restricted signatures.
+ Otherwise, we could end with the creation of undesired axioms
+ (see #3746). Note that restricted non-functorized modules are ok,
+ thanks to strengthening. *)
+
+let rec unfunct = function
+ |NoFunctor me -> me
+ |MoreFunctor(_,_,me) -> unfunct me
+
+let rec forbid_incl_signed_functor env = function
+ |MEapply(fe,_) -> forbid_incl_signed_functor env fe
+ |MEwith _ -> assert false (* No 'with' syntax for modules *)
+ |MEident mp1 ->
+ let mb = lookup_module mp1 env in
+ match mb.mod_type, mb.mod_type_alg, mb.mod_expr with
+ |MoreFunctor _, Some _, _ ->
+ (* functor + restricted signature = error *)
+ error_include_restricted_functor mp1
+ |MoreFunctor _, None, Algebraic me ->
+ (* functor, no signature yet, a definition which may be restricted *)
+ forbid_incl_signed_functor env (unfunct me)
+ |_ -> ()
let rec translate_mse_inclmod env mp inl = function
|MEident mp1 ->
let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in
let sign = clean_bounded_mod_expr mb.mod_type in
- sign,None,mb.mod_delta,Univ.ContextSet.empty
+ sign,(),mb.mod_delta,Univ.ContextSet.empty
|MEapply (fe,arg) ->
let ftrans = translate_mse_inclmod env mp inl fe in
- translate_apply env inl ftrans arg (fun _ _ -> None)
+ translate_apply env inl ftrans arg (fun _ _ -> ())
|MEwith _ -> assert false (* No 'with' syntax for modules *)
let translate_mse_incl is_mod env mp inl me =
if is_mod then
+ let () = forbid_incl_signed_functor env me in
translate_mse_inclmod env mp inl me
else
let mtb = translate_modtype env mp inl ([],me) in
let sign = clean_bounded_mod_expr mtb.mod_type in
- sign,None,mtb.mod_delta,mtb.mod_constraints
+ sign,(),mtb.mod_delta,mtb.mod_constraints
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
diff --git a/kernel/modops.ml b/kernel/modops.ml
index cbb796331..341c3993a 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -67,15 +67,13 @@ type module_typing_error =
| IncorrectWithConstraint of Label.t
| GenerativeModuleExpected of Label.t
| LabelMissing of Label.t * string
+ | IncludeRestrictedFunctor of module_path
exception ModuleTypingError of module_typing_error
let error_existing_label l =
raise (ModuleTypingError (LabelAlreadyDeclared l))
-let error_application_to_not_path mexpr =
- raise (ModuleTypingError (ApplicationToNotPath mexpr))
-
let error_not_a_functor () =
raise (ModuleTypingError NotAFunctor)
@@ -112,6 +110,9 @@ let error_generative_module_expected l =
let error_no_such_label_sub l l1 =
raise (ModuleTypingError (LabelMissing (l,l1)))
+let error_include_restricted_functor mp =
+ raise (ModuleTypingError (IncludeRestrictedFunctor mp))
+
(** {6 Operations on functors } *)
let is_functor = function
diff --git a/kernel/modops.mli b/kernel/modops.mli
index a335ad9b4..86aae598c 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -126,13 +126,12 @@ type module_typing_error =
| IncorrectWithConstraint of Label.t
| GenerativeModuleExpected of Label.t
| LabelMissing of Label.t * string
+ | IncludeRestrictedFunctor of module_path
exception ModuleTypingError of module_typing_error
val error_existing_label : Label.t -> 'a
-val error_application_to_not_path : module_struct_entry -> 'a
-
val error_incompatible_modtypes :
module_type_body -> module_type_body -> 'a
@@ -152,3 +151,5 @@ val error_incorrect_with_constraint : Label.t -> 'a
val error_generative_module_expected : Label.t -> 'a
val error_no_such_label_sub : Label.t->string->'a
+
+val error_include_restricted_functor : module_path -> 'a
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e0a07dcc3..036555309 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -746,7 +746,7 @@ let end_modtype l senv =
let add_include me is_module inl senv =
let open Mod_typing in
let mp_sup = senv.modpath in
- let sign,_,resolver,cst =
+ let sign,(),resolver,cst =
translate_mse_incl is_module senv.env mp_sup inl me
in
let senv = add_constraints (Now (false, cst)) senv in