From 0d9a91113c4112eece0680e433f435fdfb39ea4b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 7 Jul 2017 16:33:47 +0200 Subject: Getting rid of simple calls to AUContext.instance. This function breaks the abstraction barrier of abstract universe contexts, as it provides a way to observe the bound names of such a context. We remove all the uses that can be easily get rid of with the current API. --- pretyping/evarconv.ml | 5 ++--- pretyping/reductionops.ml | 8 ++++---- 2 files changed, 6 insertions(+), 7 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index b5d195873c..2acf6bfe67 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -353,9 +353,8 @@ let exact_ise_stack2 env evd f sk1 sk2 = let check_leq_inductives evd cumi u u' = let u = EConstr.EInstance.kind evd u in let u' = EConstr.EInstance.kind evd u' in - let length_ind_instance = - Univ.Instance.length - (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)) + let length_ind_instance = + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in let ind_sbcst = Univ.ACumulativityInfo.subtyp_context cumi in if not ((length_ind_instance = Univ.Instance.length u) && diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index cc1709f1c2..3acefa1342 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1362,12 +1362,12 @@ let sigma_compare_instances ~flex i0 i1 sigma = raise Reduction.NotConvertible let sigma_check_inductive_instances cv_pb uinfind u u' sigma = - let ind_instance = - Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context uinfind) + let len_instance = + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context uinfind) in let ind_sbctx = Univ.ACumulativityInfo.subtyp_context uinfind in - if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && - (Univ.Instance.length ind_instance = Univ.Instance.length u')) then + if not ((len_instance = Univ.Instance.length u) && + (len_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else let comp_cst = -- cgit v1.2.3 From b8a7222e670f69e024d50394afd88204e15d1b29 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 10 Jul 2017 18:05:23 +0200 Subject: Less footguns in universe handling: remove subst_instance_context. This function was lurking around, waiting to bite anybody willing to use it. We use instead a better API, correct and much less error-prone. --- pretyping/evarconv.ml | 4 +--- pretyping/reductionops.ml | 6 ++---- 2 files changed, 3 insertions(+), 7 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 2acf6bfe67..87f29ba492 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -363,9 +363,7 @@ let check_leq_inductives evd cumi u u' = else begin let comp_subst = (Univ.Instance.append u u') in - let comp_cst = - Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbcst) - in + let comp_cst = Univ.AUContext.instantiate comp_subst ind_sbcst in Evd.add_constraints evd comp_cst end diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 3acefa1342..21ed8e0a23 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1372,15 +1372,13 @@ let sigma_check_inductive_instances cv_pb uinfind u u' sigma = else let comp_cst = let comp_subst = (Univ.Instance.append u u') in - Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbctx) + Univ.AUContext.instantiate comp_subst ind_sbctx in let comp_cst = match cv_pb with Reduction.CONV -> let comp_subst = (Univ.Instance.append u' u) in - let comp_cst' = - Univ.UContext.constraints(Univ.subst_instance_context comp_subst ind_sbctx) - in + let comp_cst' = Univ.AUContext.instantiate comp_subst ind_sbctx in Univ.Constraint.union comp_cst comp_cst' | Reduction.CUMUL -> comp_cst in -- cgit v1.2.3 From 012f5fb722a9d5dcef82c800aa54ed50c0a58957 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 10 Jul 2017 19:11:20 +0200 Subject: Safe API for accessing universe constraints of global references. Instead of returning either an instance or the set of constraints, we rather return the corresponding abstracted context. We also push back all uses of abstraction-breaking calls from these functions out of the kernel. --- pretyping/recordops.ml | 5 +++-- pretyping/typeclasses.ml | 4 ++-- pretyping/vnorm.ml | 4 ++-- 3 files changed, 7 insertions(+), 6 deletions(-) (limited to 'pretyping') diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 1cb694da66..9fc2573aca 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -198,7 +198,8 @@ let warn_projection_no_head_constant = let compute_canonical_projections warn (con,ind) = let env = Global.env () in let ctx = Environ.constant_context env con in - let u = Univ.UContext.instance ctx in + let u = Univ.AUContext.instance ctx in + let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in let v = (mkConstU (con,u)) in let ctx = Univ.ContextSet.of_context ctx in let c = Environ.constant_value_in env (con,u) in @@ -298,7 +299,7 @@ let error_not_structure ref = let check_and_decompose_canonical_structure ref = let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in let env = Global.env () in - let u = Environ.constant_instance env sp in + let u = Univ.AUContext.instance (Environ.constant_context env sp) in let vc = match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc | None -> error_not_structure ref in diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 201f79c39f..bae831b637 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -117,10 +117,10 @@ let typeclass_univ_instance (cl,u') = match cl.cl_impl with | ConstRef c -> let cb = Global.lookup_constant c in - Declareops.constant_polymorphic_instance cb + Univ.AUContext.instance (Declareops.constant_polymorphic_context cb) | IndRef c -> let mib,oib = Global.lookup_inductive c in - Declareops.inductive_polymorphic_instance mib + Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) | _ -> Univ.Instance.empty in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b3eaa3cb95..66cc42cb61 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -174,7 +174,7 @@ and nf_whd env sigma whd typ = | Vatom_stk(Aind ((mi,i) as ind), stk) -> let mib = Environ.lookup_mind mi env in let nb_univs = - Univ.Instance.length (Declareops.inductive_polymorphic_instance mib) + Univ.AUContext.size (Declareops.inductive_polymorphic_context mib) in let mk u = let pind = (ind, u) in (mkIndU pind, type_of_ind env pind) @@ -203,7 +203,7 @@ and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk = | ConstKey cst -> let cbody = Environ.lookup_constant cst env in let nb_univs = - Univ.Instance.length (Declareops.constant_polymorphic_instance cbody) + Univ.AUContext.size (Declareops.constant_polymorphic_context cbody) in let mk u = let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst) -- cgit v1.2.3