diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 80 |
1 files changed, 9 insertions, 71 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 1893018a95..418ea271cd 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1324,79 +1324,17 @@ let sigma_compare_instances ~flex i0 i1 sigma = | Univ.UniverseInconsistency _ -> raise Reduction.NotConvertible -let sigma_check_inductive_instances cv_pb uinfind u u' sigma = - let len_instance = - Univ.AUContext.size (Univ.ACumulativityInfo.univ_context uinfind) - in - let ind_sbctx = Univ.ACumulativityInfo.subtyp_context uinfind in - 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 = - let comp_subst = (Univ.Instance.append u u') in - 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.AUContext.instantiate comp_subst ind_sbctx in - Univ.Constraint.union comp_cst comp_cst' - | Reduction.CUMUL -> comp_cst - in - try Evd.add_constraints sigma comp_cst - with Evd.UniversesDiffer - | Univ.UniverseInconsistency _ -> - raise Reduction.NotConvertible - -let sigma_conv_inductives - cv_pb (mind, ind) u1 sv1 u2 sv2 sigma = - try sigma_compare_instances ~flex:false u1 u2 sigma with - Reduction.NotConvertible -> - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - raise Reduction.NotConvertible - | Declarations.Polymorphic_ind _ -> - raise Reduction.NotConvertible - | Declarations.Cumulative_ind cumi -> - let num_param_arity = - mind.Declarations.mind_nparams + - mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs - in - if not (num_param_arity = sv1 && num_param_arity = sv2) then - raise Reduction.NotConvertible - else - sigma_check_inductive_instances cv_pb cumi u1 u2 sigma - -let sigma_conv_constructors - (mind, ind, cns) u1 sv1 u2 sv2 sigma = - try sigma_compare_instances ~flex:false u1 u2 sigma with - Reduction.NotConvertible -> - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - raise Reduction.NotConvertible - | Declarations.Polymorphic_ind _ -> - raise Reduction.NotConvertible - | Declarations.Cumulative_ind cumi -> - let num_cnstr_args = - let nparamsctxt = - mind.Declarations.mind_nparams + - mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs - in - nparamsctxt + - mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1) - in - if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then - raise Reduction.NotConvertible - else - sigma_check_inductive_instances Reduction.CONV cumi u1 u2 sigma +let sigma_check_inductive_instances csts sigma = + try Evd.add_constraints sigma csts + with Evd.UniversesDiffer + | Univ.UniverseInconsistency _ -> + raise Reduction.NotConvertible let sigma_univ_state = - { Reduction.compare = sigma_compare_sorts; - Reduction.compare_instances = sigma_compare_instances; - Reduction.conv_inductives = sigma_conv_inductives; - Reduction.conv_constructors = sigma_conv_constructors} + let open Reduction in + { compare_sorts = sigma_compare_sorts; + compare_instances = sigma_compare_instances; + compare_cumul_instances = sigma_check_inductive_instances; } let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = |