diff options
Diffstat (limited to 'kernel/mod_typing.ml')
| -rw-r--r-- | kernel/mod_typing.ml | 72 |
1 files changed, 32 insertions, 40 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index ff44f0f540..d2b41aae98 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -72,71 +72,58 @@ 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 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 c', univs, ctx' = + match cb.const_universes with + | Monomorphic_const _ -> + (** We do not add the deferred constraints of the body in the + environment, because they do not appear in the type of the + definition. Any inconsistency will be raised at a later stage + when joining the environment. *) 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 typ = 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 (UGraph.check_constraints cst (Environ.universes env')) then - error_incorrect_with_constraint lab - in + in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx) + | Polymorphic_const uctx -> + let subst, ctx = Univ.abstract_universes ctx in + let c = Vars.subst_univs_level_constr subst c in + let () = + if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then + error_incorrect_with_constraint lab + in + (** Terms are compared in a context with De Bruijn universe indices *) + let env' = Environ.push_context ~strict:false (Univ.AUContext.repr uctx) env 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 typ = 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 c' = Mod_subst.force_constr cs in let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in cst' in 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 + c, Polymorphic_const 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 = ctx ; + const_universes = univs ; const_body_code = Option.map Cemitcodes.from_val - (compile_constant_body env' univs def) } + (compile_constant_body env' cb.const_universes def) } in before@(lab,SFBconst(cb'))::after, c', ctx' else @@ -277,7 +264,9 @@ let rec translate_mse env mpo inl = function |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 + |None -> + let mt = lookup_modtype mp1 env in + module_body_of_type mt.mod_mp mt in mb.mod_type, me, mb.mod_delta, Univ.ContextSet.empty |MEapply (fe,mp1) -> @@ -294,9 +283,11 @@ let mk_mod mp e ty cst reso = mod_type_alg = None; mod_constraints = cst; mod_delta = reso; - mod_retroknowledge = [] } + mod_retroknowledge = ModBodyRK []; } -let mk_modtype mp ty cst reso = mk_mod mp Abstract ty cst reso +let mk_modtype mp ty cst reso = + let mb = mk_mod mp Abstract ty cst reso in + { mb with mod_expr = (); mod_retroknowledge = ModTypeRK } let rec translate_mse_funct env mpo inl mse = function |[] -> @@ -332,6 +323,7 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with { res_mtb with mod_mp = mp; mod_expr = impl; + mod_retroknowledge = ModBodyRK []; (** cst from module body typing, cst' from subtyping, constraints from module type. *) |