From cc69a4697633e14fc00c9bd0858b38120645464b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 16:00:49 +0200 Subject: Univs: module constraints move to universe contexts as they might declare new universes (e.g. with). --- kernel/mod_typing.ml | 35 +++++++++++++++++------------------ 1 file changed, 17 insertions(+), 18 deletions(-) (limited to 'kernel/mod_typing.ml') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 4f20e5f62a..7da0958eaf 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.constraints + module_signature * 'alg option * delta_resolver * Univ.ContextSet.t let rec mp_from_mexpr = function | MEident mp -> mp @@ -52,7 +52,7 @@ let rec rebuild_mp mp l = | []-> mp | i::r -> rebuild_mp (MPdot(mp,Label.of_id i)) r -let (+++) = Univ.Constraint.union +let (+++) = Univ.ContextSet.union let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let lab,idl = match idl with @@ -75,30 +75,30 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let ccst = Declareops.constraints_of_constant (opaque_tables env) cb in let env' = Environ.add_constraints ccst env' in let newus, cst = Univ.UContext.dest ctx in + let ctxs = Univ.ContextSet.of_context ctx in let env' = Environ.add_constraints cst env' in - let c',cst = match cb.const_body with + let c',ctx' = match cb.const_body with | Undef _ | OpaqueDef _ -> let j = Typeops.infer env' c in let typ = Typeops.type_of_constant_type env' cb.const_type in let cst' = Reduction.infer_conv_leq env' (Environ.universes env') j.uj_type typ in - j.uj_val,cst' +++ cst + j.uj_val, Univ.ContextSet.add_constraints cst' ctxs | Def cs -> let cst' = Reduction.infer_conv env' (Environ.universes env') c (Mod_subst.force_constr cs) in let cst = (*FIXME MS: what to check here? subtyping of polymorphic constants... *) - if cb.const_polymorphic then cst' +++ cst - else cst' +++ cst + (* if cb.const_polymorphic then *)Univ.ContextSet.add_constraints cst' ctxs + (* else cst' +++ cst *) in c, cst in let def = Def (Mod_subst.from_val c') in - let ctx' = Univ.UContext.make (newus, cst) in let cb' = { cb with const_body = def; const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def); - const_universes = ctx' } + const_universes = Univ.ContextSet.to_context ctx' } in before@(lab,SFBconst(cb'))::after, c', ctx' else @@ -145,8 +145,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv = begin try let mtb_old = module_type_of_module old in - Subtyping.check_subtypes env' mtb_mp1 mtb_old - +++ old.mod_constraints + Univ.ContextSet.add_constraints (Subtyping.check_subtypes env' mtb_mp1 mtb_old) old.mod_constraints with Failure _ -> error_incorrect_with_constraint lab end | Algebraic (NoFunctor (MEident(mp'))) -> @@ -194,7 +193,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv = | Algebraic (NoFunctor (MEident mp0)) -> let mpnew = rebuild_mp mp0 idl in check_modpath_equiv env' mpnew mp; - before@(lab,spec)::after, equiv, Univ.Constraint.empty + before@(lab,spec)::after, equiv, Univ.ContextSet.empty | _ -> error_generative_module_expected lab end with @@ -207,8 +206,8 @@ 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',cst'))) in - (NoFunctor struc'),alg',reso, cst+++(Univ.UContext.constraints cst') + let alg' = mk_alg_with alg (WithDef (idl,(c',Univ.ContextSet.to_context cst'))) in + (NoFunctor struc'),alg',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 @@ -238,7 +237,7 @@ let rec translate_mse env mpo inl = function let mtb = lookup_modtype mp1 env in mtb.mod_type, mtb.mod_delta in - sign,Some (MEident mp1),reso,Univ.Constraint.empty + sign,Some (MEident mp1),reso,Univ.ContextSet.empty |MEapply (fe,mp1) -> translate_apply env inl (translate_mse env mpo inl fe) mp1 (mk_alg_app mpo) |MEwith(me, with_decl) -> @@ -256,7 +255,7 @@ and translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg = 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', cst1 +++ cst2 + 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)) @@ -301,7 +300,7 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with mk_mod mp impl sign None 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.Constraint.empty reso in + let auto_mtb = mk_modtype mp sign Univ.ContextSet.empty reso in let cst' = Subtyping.check_subtypes env auto_mtb res_mtb in let impl = match alg with Some e -> Algebraic e | None -> Struct sign in { res_mtb with @@ -309,7 +308,7 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with mod_expr = impl; (** cst from module body typing, cst' from subtyping, and constraints from module type. *) - mod_constraints = cst +++ cst' +++ res_mtb.mod_constraints } + mod_constraints = Univ.ContextSet.add_constraints cst' (cst +++ res_mtb.mod_constraints) } let translate_module env mp inl = function |MType (params,ty) -> @@ -324,7 +323,7 @@ let rec translate_mse_incl 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.Constraint.empty + sign,None,mb.mod_delta,Univ.ContextSet.empty |MEapply (fe,arg) -> let ftrans = translate_mse_incl env mp inl fe in translate_apply env inl ftrans arg (fun _ _ -> None) -- cgit v1.2.3 From d4869e059bfb73d99e1f5ef1b0a1f0906fa27056 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 1 Oct 2015 15:40:17 +0200 Subject: Univs: correct handling of with in modules For polymorphic and non-polymorphic parameters and definitions, fixes bugs #4298, #4294 --- kernel/mod_typing.ml | 73 +++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 52 insertions(+), 21 deletions(-) (limited to 'kernel/mod_typing.ml') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 7da0958eaf..3be89afbde 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -72,33 +72,64 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = (* In the spirit of subtyping.check_constant, we accept any implementations of parameters and opaques terms, as long as they have the right type *) - let ccst = Declareops.constraints_of_constant (opaque_tables env) cb in - let env' = Environ.add_constraints ccst env' in - let newus, cst = Univ.UContext.dest ctx in - let ctxs = Univ.ContextSet.of_context ctx in - let env' = Environ.add_constraints cst env' in - let c',ctx' = match cb.const_body with - | Undef _ | OpaqueDef _ -> - let j = Typeops.infer env' c in - let typ = Typeops.type_of_constant_type env' cb.const_type in - let cst' = Reduction.infer_conv_leq env' (Environ.universes env') - j.uj_type typ in - j.uj_val, Univ.ContextSet.add_constraints cst' ctxs - | Def cs -> - let cst' = Reduction.infer_conv env' (Environ.universes env') c - (Mod_subst.force_constr cs) in - let cst = (*FIXME MS: what to check here? subtyping of polymorphic constants... *) - (* if cb.const_polymorphic then *)Univ.ContextSet.add_constraints cst' ctxs - (* else cst' +++ cst *) + let uctx = Declareops.universes_of_constant (opaque_tables env) cb in + let uctx = (* Context of the spec *) + if cb.const_polymorphic then + Univ.instantiate_univ_context uctx + else uctx + in + let c', univs, ctx' = + if not cb.const_polymorphic then + let env' = Environ.push_context ~strict:true uctx env' in + let env' = Environ.push_context ~strict:true ctx env' in + let c',cst = match cb.const_body with + | Undef _ | OpaqueDef _ -> + let j = Typeops.infer env' c in + let typ = Typeops.type_of_constant_type env' cb.const_type in + let cst' = Reduction.infer_conv_leq env' (Environ.universes env') + j.uj_type typ in + j.uj_val, cst' + | Def cs -> + let c' = Mod_subst.force_constr cs in + c, Reduction.infer_conv env' (Environ.universes env') c c' + in c', ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx) + else + let cus, ccst = Univ.UContext.dest uctx in + let newus, cst = Univ.UContext.dest ctx in + let () = + if not (Univ.Instance.length cus == Univ.Instance.length newus) then + error_incorrect_with_constraint lab + in + let inst = Univ.Instance.append cus newus in + let csti = Univ.enforce_eq_instances cus newus cst in + let csta = Univ.Constraint.union csti ccst in + let env' = Environ.push_context ~strict:false (Univ.UContext.make (inst, csta)) env in + let () = if not (Univ.check_constraints cst (Environ.universes env')) then + error_incorrect_with_constraint lab + in + let cst = match cb.const_body with + | Undef _ | OpaqueDef _ -> + let j = Typeops.infer env' c in + let typ = Typeops.type_of_constant_type env' cb.const_type in + let cst' = Reduction.infer_conv_leq env' (Environ.universes env') + j.uj_type typ in + cst' + | Def cs -> + let c' = Vars.subst_instance_constr cus (Mod_subst.force_constr cs) in + let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in + cst' in - c, cst + if not (Univ.Constraint.is_empty cst) then + error_incorrect_with_constraint lab; + let subst, ctx = Univ.abstract_universes true ctx in + Vars.subst_univs_level_constr subst c, ctx, Univ.ContextSet.empty in let def = Def (Mod_subst.from_val c') in let cb' = { cb with const_body = def; - const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def); - const_universes = Univ.ContextSet.to_context ctx' } + const_universes = univs; + const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def) } in before@(lab,SFBconst(cb'))::after, c', ctx' else -- cgit v1.2.3 From 1d01533266b247cbc32903935963674acf7c6c54 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 1 Oct 2015 16:05:48 +0200 Subject: Univs: forgot a substitution in mod_typing. --- kernel/mod_typing.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel/mod_typing.ml') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 3be89afbde..922652287b 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -111,6 +111,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = | Undef _ | OpaqueDef _ -> let j = Typeops.infer env' c in let typ = Typeops.type_of_constant_type env' cb.const_type in + let typ = Vars.subst_instance_constr cus typ in let cst' = Reduction.infer_conv_leq env' (Environ.universes env') j.uj_type typ in cst' -- cgit v1.2.3 From 84add29c036735ceacde73ea98a9a5a454a5e3a0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 6 Oct 2015 19:09:10 +0200 Subject: Splitting kernel universe code in two modules. 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity. --- kernel/mod_typing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/mod_typing.ml') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 922652287b..0f3ea1d0a6 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -104,7 +104,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let csti = Univ.enforce_eq_instances cus newus cst in let csta = Univ.Constraint.union csti ccst in let env' = Environ.push_context ~strict:false (Univ.UContext.make (inst, csta)) env in - let () = if not (Univ.check_constraints cst (Environ.universes env')) then + let () = if not (UGraph.check_constraints cst (Environ.universes env')) then error_incorrect_with_constraint lab in let cst = match cb.const_body with -- cgit v1.2.3 From c2de48c3f59415eaf0f2cbb5cfe78f23e908a459 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sun, 25 Oct 2015 12:14:12 +0100 Subject: Minor module cleanup : error HigherOrderInclude was never happening When F is a Functor, doing an 'Include F' triggers the 'Include Self' mechanism: the current context is used as an pseudo-argument to F. This may fail with a subtype error if the current context isn't adequate. --- kernel/mod_typing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/mod_typing.ml') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 922652287b..eef83ce743 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -359,4 +359,4 @@ let rec translate_mse_incl env mp inl = function |MEapply (fe,arg) -> let ftrans = translate_mse_incl env mp inl fe in translate_apply env inl ftrans arg (fun _ _ -> None) - |_ -> Modops.error_higher_order_include () + |MEwith _ -> assert false (* No 'with' syntax for modules *) -- cgit v1.2.3 From 83e82ef7b42f47d63d3b40b2698695a0e7b2d685 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sun, 25 Oct 2015 14:58:39 +0100 Subject: Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331) --- kernel/mod_typing.ml | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'kernel/mod_typing.ml') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index eef83ce743..c03c5175fd 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -351,12 +351,20 @@ let translate_module env mp inl = function let restype = Option.map (fun ty -> ((params,ty),inl)) oty in finalize_module env mp t restype -let rec translate_mse_incl env mp inl = function +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 |MEapply (fe,arg) -> - let ftrans = translate_mse_incl env mp inl fe in + let ftrans = translate_mse_inclmod env mp inl fe in translate_apply env inl ftrans arg (fun _ _ -> None) |MEwith _ -> assert false (* No 'with' syntax for modules *) + +let translate_mse_incl is_mod env mp inl me = + if is_mod then + 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 -- cgit v1.2.3 From 7d9331a2a188842a98936278d02177f1a6fa7001 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Sat, 17 Oct 2015 21:40:49 -0700 Subject: Adds support for the virtual machine to perform reduction of universe polymorphic definitions. - This implementation passes universes in separate arguments and does not eagerly instanitate polymorphic definitions. - This means that it pays no cost on monomorphic definitions. --- kernel/mod_typing.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'kernel/mod_typing.ml') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index c03c5175fd..bd7ee7b339 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -126,11 +126,17 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = Vars.subst_univs_level_constr subst c, ctx, Univ.ContextSet.empty in let def = Def (Mod_subst.from_val c') in +(* let ctx' = Univ.UContext.make (newus, cst) in *) + let univs = + if cb.const_polymorphic then Some cb.const_universes + else None + in let cb' = { cb with const_body = def; - const_universes = univs; - const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def) } + const_universes = ctx ; + const_body_code = Option.map Cemitcodes.from_val + (compile_constant_body env' univs def) } in before@(lab,SFBconst(cb'))::after, c', ctx' else -- cgit v1.2.3 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.ml | 128 ++++++++++++++++++++++++++++----------------------- 1 file changed, 71 insertions(+), 57 deletions(-) (limited to 'kernel/mod_typing.ml') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index bd7ee7b339..8a1634881f 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 -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- kernel/mod_typing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/mod_typing.ml') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 8a1634881f..4fc777c4f5 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*