diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 78 |
1 files changed, 75 insertions, 3 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index c2a6483012..123c610166 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1313,8 +1313,8 @@ let pb_equal = function | Reduction.CUMUL -> Reduction.CONV | Reduction.CONV -> Reduction.CONV -let report_anomaly _ = - let e = UserError (None, Pp.str "Conversion test raised an anomaly") in +let report_anomaly e = + let e = UserError (None, Pp.(str "Conversion test raised an anomaly" ++ print e)) in let e = CErrors.push e in iraise e @@ -1361,9 +1361,81 @@ 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 ind_instance = + Univ.AUContext.instance (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 + anomaly (Pp.str "Invalid inductive subtyping encountered!") + else + let comp_cst = + let comp_subst = (Univ.Instance.append u u') in + Univ.UContext.constraints (Univ.subst_instance_context 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 + 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_univ_state = { Reduction.compare = sigma_compare_sorts; - Reduction.compare_instances = sigma_compare_instances } + Reduction.compare_instances = sigma_compare_instances; + Reduction.conv_inductives = sigma_conv_inductives; + Reduction.conv_constructors = sigma_conv_constructors} let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = |