From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- kernel/mod_typing.ml | 119 +++++++++++++++++++++++++++++++++++---------------- 1 file changed, 83 insertions(+), 36 deletions(-) (limited to 'kernel/mod_typing.ml') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 26dd45f5..bd7ee7b3 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 @@ -72,33 +72,71 @@ 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 env' = Environ.add_constraints cst 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' +++ cst - | 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 + 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 typ = Vars.subst_instance_constr cus typ 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 ctx' = Univ.UContext.make (newus, cst) 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_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def); - const_universes = ctx' } + 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 @@ -145,8 +183,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 +231,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 +244,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 +275,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 +293,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,13 +338,15 @@ 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 mod_mp = mp; mod_expr = impl; - mod_constraints = cst +++ cst' } + (** 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) } let translate_module env mp inl = function |MType (params,ty) -> @@ -318,12 +357,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.Constraint.empty + 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) - |_ -> Modops.error_higher_order_include () + |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