diff options
| -rw-r--r-- | kernel/reduction.ml | 141 | ||||
| -rw-r--r-- | kernel/reduction.mli | 3 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 30 |
3 files changed, 69 insertions, 105 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index c77085067..dc46ac01b 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -202,8 +202,7 @@ type 'a universe_compare = { (* Might raise NotConvertible *) compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; - compare_cumul_instances : conv_pb -> Univ.abstract_cumulativity_info -> - Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a } + compare_cumul_instances : Univ.Constraint.t -> 'a -> 'a } type 'a universe_state = 'a * 'a universe_compare @@ -218,31 +217,58 @@ let sort_cmp_universes env pb s0 s1 (u, check) = constructors. *) let convert_instances ~flex u u' (s, check) = (check.compare_instances ~flex u u' s, check) - -let convert_inductives cv_pb (mind,ind) u1 sv1 u2 sv2 (s, check as univs) = + +let get_cumulativity_constraints cv_pb cumi u u' = + let length_ind_instance = + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) + in + let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in + if not ((length_ind_instance = Univ.Instance.length u) && + (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.AUContext.instantiate comp_subst ind_subtypctx + in + match cv_pb with + | CONV -> + let comp_cst' = + let comp_subst = (Univ.Instance.append u' u) in + Univ.AUContext.instantiate comp_subst ind_subtypctx + in + Univ.Constraint.union comp_cst comp_cst' + | CUMUL -> comp_cst + +let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2 s = match mind.Declarations.mind_universes with | Declarations.Monomorphic_ind _ -> assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0); - univs + s | Declarations.Polymorphic_ind _ -> - check.compare_instances ~flex:false u1 u2 s, check + cmp_instances u1 u2 s | 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 - check.compare_instances ~flex:false u1 u2 s, check + if not (Int.equal num_param_arity nargs) then + cmp_instances u1 u2 s else - check.compare_cumul_instances cv_pb cumi u1 u2 s, check + let csts = get_cumulativity_constraints cv_pb cumi u1 u2 in + cmp_cumul csts s -let convert_constructors (mind, ind, cns) u1 sv1 u2 sv2 (s, check as univs) = +let convert_inductives cv_pb ind nargs u1 u2 (s, check) = + convert_inductives_gen (check.compare_instances ~flex:false) check.compare_cumul_instances + cv_pb ind nargs u1 u2 s, check + +let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u2 s = match mind.Declarations.mind_universes with | Declarations.Monomorphic_ind _ -> assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0); - univs + s | Declarations.Polymorphic_ind _ -> - check.compare_instances ~flex:false u1 u2 s, check + cmp_instances u1 u2 s | Declarations.Cumulative_ind cumi -> let num_cnstr_args = let nparamsctxt = @@ -251,10 +277,15 @@ let convert_constructors (mind, ind, cns) u1 sv1 u2 sv2 (s, check as univs) = (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1) in - if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then - check.compare_instances ~flex:false u1 u2 s, check + if not (Int.equal num_cnstr_args nargs) then + cmp_instances u1 u2 s else - check.compare_cumul_instances CONV cumi u1 u2 s, check + let csts = get_cumulativity_constraints CONV cumi u1 u2 in + cmp_cumul csts s + +let convert_constructors ctor nargs u1 u2 (s, check) = + convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances + ctor nargs u1 u2 s, check let conv_table_key infos k1 k2 cuniv = if k1 == k2 then cuniv else @@ -537,13 +568,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else let mind = Environ.lookup_mind (fst ind1) (info_env infos) in - let cuniv = - convert_inductives cv_pb (mind, snd ind1) - u1 (CClosure.stack_args_size v1) - u2 (CClosure.stack_args_size v2) - cuniv - in - convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + let nargs = CClosure.stack_args_size v1 in + if not (Int.equal nargs (CClosure.stack_args_size v2)) + then raise NotConvertible + else + let cuniv = convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv in + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> @@ -553,13 +583,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else let mind = Environ.lookup_mind (fst ind1) (info_env infos) in - let cuniv = - convert_constructors (mind, snd ind1, j1) - u1 (CClosure.stack_args_size v1) - u2 (CClosure.stack_args_size v2) - cuniv - in - convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + let nargs = CClosure.stack_args_size v1 in + if not (Int.equal nargs (CClosure.stack_args_size v2)) + then raise NotConvertible + else + let cuniv = convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv in + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible (* Eta expansion of records *) @@ -676,31 +705,9 @@ let check_convert_instances ~flex u u' univs = else raise NotConvertible (* general conversion and inference functions *) -let check_inductive_instances cv_pb cumi u u' univs = - let length_ind_instance = - Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) - in - let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in - if not ((length_ind_instance = Univ.Instance.length u) && - (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.AUContext.instantiate comp_subst ind_subtypctx - in - let comp_cst = - match cv_pb with - CONV -> - let comp_cst' = - let comp_subst = (Univ.Instance.append u' u) in - Univ.AUContext.instantiate comp_subst ind_subtypctx - in - Univ.Constraint.union comp_cst comp_cst' - | CUMUL -> comp_cst - in - if (UGraph.check_constraints comp_cst univs) then univs - else raise NotConvertible +let check_inductive_instances csts univs = + if (UGraph.check_constraints csts univs) then univs + else raise NotConvertible let checked_universes = { compare_sorts = checked_sort_cmp_universes; @@ -748,30 +755,8 @@ let infer_convert_instances ~flex u u' (univs,cstrs) = else Univ.enforce_eq_instances u u' cstrs in (univs, cstrs') -let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) = - let length_ind_instance = - Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) - in - let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in - if not ((length_ind_instance = Univ.Instance.length u) && - (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.AUContext.instantiate comp_subst ind_subtypctx - in - let comp_cst = - match cv_pb with - CONV -> - let comp_cst' = - let comp_subst = (Univ.Instance.append u' u) in - Univ.AUContext.instantiate comp_subst ind_subtypctx - in - Univ.Constraint.union comp_cst comp_cst' - | CUMUL -> comp_cst - in - (univs, Univ.Constraint.union cstrs comp_cst) +let infer_inductive_instances csts (univs,csts') = + (univs, Univ.Constraint.union csts csts') let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = { compare_sorts = infer_cmp_universes; diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 0f1d681bc..059f259ae 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -39,8 +39,7 @@ type 'a universe_compare = { (* Might raise NotConvertible *) compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; - compare_cumul_instances : conv_pb -> Univ.abstract_cumulativity_info -> - Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a } + compare_cumul_instances : Univ.Constraint.t -> 'a -> 'a } type 'a universe_state = 'a * 'a universe_compare diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 5ecaf0da1..418ea271c 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1324,31 +1324,11 @@ 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_check_inductive_instances csts sigma = + try Evd.add_constraints sigma csts + with Evd.UniversesDiffer + | Univ.UniverseInconsistency _ -> + raise Reduction.NotConvertible let sigma_univ_state = let open Reduction in |