From e123ec7621d06cde2b65755bab75b438b9f02664 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 3 Jul 2017 15:54:02 +0200 Subject: Do not add original constraints to the environment in 'with Definition' check. This was useless, because immediate constraints are assumed to already be in the current environment, while deferred constraints are useless for the conversion check of the definition types, as they only appear in the opaque body. This also clarifies a bit what is going on in the typing of module constraints w.r.t. global universes. --- kernel/mod_typing.ml | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) (limited to 'kernel') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 79016735bc..20ca615306 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -72,16 +72,13 @@ 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 *) + let c', univs, ctx' = match cb.const_universes with - | Monomorphic_const _ -> uctx - | Polymorphic_const auctx -> - Univ.instantiate_univ_context auctx - in - let c', univs, ctx' = - if not (Declareops.constant_is_polymorphic cb) then - let env' = Environ.push_context ~strict:true uctx env' in + | 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 _ -> @@ -94,7 +91,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let c' = Mod_subst.force_constr cs in c, Reduction.infer_conv env' (Environ.universes env') c c' in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx) - else + | Polymorphic_const uctx -> + let uctx = Univ.instantiate_univ_context uctx in let cus, ccst = Univ.UContext.dest uctx in let newus, cst = Univ.UContext.dest ctx in let () = -- cgit v1.2.3 From 6aeda23a14a5a5dfca259fe99a19d7bcb42d1052 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 3 Jul 2017 16:47:55 +0200 Subject: Removing a few suspicious functions from the kernel. These functions were messing with the deferred universe constraints in an error-prone way, and were only used for printing as of today. We inline the one used by the printer instead. --- kernel/declareops.ml | 31 ------------------------------- kernel/declareops.mli | 4 ---- kernel/subtyping.ml | 10 ++++++---- 3 files changed, 6 insertions(+), 39 deletions(-) (limited to 'kernel') diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 72b4907680..4ec8d43e73 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -67,37 +67,6 @@ let type_of_constant cb = if t' == t then x else RegularArity t' | TemplateArity _ as x -> x -let constraints_of_constant otab cb = - match cb.const_universes with - | Polymorphic_const ctx -> - Univ.UContext.constraints (Univ.instantiate_univ_context ctx) - | Monomorphic_const ctx -> - Univ.Constraint.union - (Univ.UContext.constraints ctx) - (match cb.const_body with - | Undef _ -> Univ.empty_constraint - | Def c -> Univ.empty_constraint - | OpaqueDef o -> - Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o)) - -let universes_of_constant otab cb = - match cb.const_body with - | Undef _ | Def _ -> - begin - match cb.const_universes with - | Monomorphic_const ctx -> ctx - | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx - end - | OpaqueDef o -> - let body_uctxs = Opaqueproof.force_constraints otab o in - match cb.const_universes with - | Monomorphic_const ctx -> - let uctxs = Univ.ContextSet.of_context ctx in - Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs) - | Polymorphic_const ctx -> - assert(Univ.ContextSet.is_empty body_uctxs); - Univ.instantiate_univ_context ctx - let universes_of_polymorphic_constant otab cb = match cb.const_universes with | Monomorphic_const _ -> Univ.UContext.empty diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 811a28aa65..7db2050b73 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -39,10 +39,6 @@ val constant_is_polymorphic : constant_body -> bool val body_of_constant : Opaqueproof.opaquetab -> constant_body -> Term.constr option val type_of_constant : constant_body -> constant_type -val constraints_of_constant : - Opaqueproof.opaquetab -> constant_body -> Univ.constraints -val universes_of_constant : - Opaqueproof.opaquetab -> constant_body -> Univ.universe_context (** Return the universe context, in case the definition is polymorphic, otherwise the context is empty. *) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 1bd9d6e495..d3fb4ef58b 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -368,8 +368,9 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let u1 = inductive_polymorphic_instance mind1 in let arity1,cst1 = constrained_type_of_inductive env ((mind1,mind1.mind_packets.(i)),u1) in - let cst2 = - Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in + let cst2 = assert false in +(* let cst2 = *) +(* Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in *) let typ2 = Typeops.type_of_constant_type env cb2.const_type in let cst = Constraint.union cst (Constraint.union cst1 cst2) in let error = NotConvertibleTypeField (env, arity1, typ2) in @@ -384,8 +385,9 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = if Declareops.constant_has_body cb2 then error DefinitionFieldExpected; let u1 = inductive_polymorphic_instance mind1 in let ty1,cst1 = constrained_type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in - let cst2 = - Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in + let cst2 = assert false in +(* let cst2 = *) +(* Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in *) let ty2 = Typeops.type_of_constant_type env cb2.const_type in let cst = Constraint.union cst (Constraint.union cst1 cst2) in let error = NotConvertibleTypeField (env, ty1, ty2) in -- cgit v1.2.3 From 78f536c7fa1af8a61c3dbc5eafae74ad436958ef Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 4 Jul 2017 11:36:32 +0200 Subject: Removing dead code in Subtyping. This code was a sketch of what to do when we properly implement module-level handling of instanciation of definitions by inductive types. It was completely dead code, called after an error, and somewhat incorrect. Instead of letting it bitrot, we remove it. --- kernel/subtyping.ml | 33 +++++---------------------------- 1 file changed, 5 insertions(+), 28 deletions(-) (limited to 'kernel') diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index d3fb4ef58b..ce4448c706 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -358,40 +358,17 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let c2 = Mod_subst.force_constr lc2 in check_conv NotConvertibleBodyField cst poly u infer_conv env' c1 c2)) | IndType ((kn,i),mind1) -> - ignore (CErrors.user_err Pp.(str @@ + CErrors.user_err Pp.(str @@ "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ - "name.")); - let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in - if Declareops.constant_has_body cb2 then error DefinitionFieldExpected; - let u1 = inductive_polymorphic_instance mind1 in - let arity1,cst1 = constrained_type_of_inductive env - ((mind1,mind1.mind_packets.(i)),u1) in - let cst2 = assert false in -(* let cst2 = *) -(* Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in *) - let typ2 = Typeops.type_of_constant_type env cb2.const_type in - let cst = Constraint.union cst (Constraint.union cst1 cst2) in - let error = NotConvertibleTypeField (env, arity1, typ2) in - check_conv error cst false Univ.Instance.empty infer_conv_leq env arity1 typ2 - | IndConstr (((kn,i),j) as cstr,mind1) -> - ignore (CErrors.user_err Pp.(str @@ + "name.") + | IndConstr (((kn,i),j),mind1) -> + CErrors.user_err Pp.(str @@ "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ - "name.")); - let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in - if Declareops.constant_has_body cb2 then error DefinitionFieldExpected; - let u1 = inductive_polymorphic_instance mind1 in - let ty1,cst1 = constrained_type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in - let cst2 = assert false in -(* let cst2 = *) -(* Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in *) - let ty2 = Typeops.type_of_constant_type env cb2.const_type in - let cst = Constraint.union cst (Constraint.union cst1 cst2) in - let error = NotConvertibleTypeField (env, ty1, ty2) in - check_conv error cst false Univ.Instance.empty infer_conv env ty1 ty2 + "name.") let rec check_modules cst env msb1 msb2 subst1 subst2 = let mty1 = module_type_of_module msb1 in -- cgit v1.2.3