aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/evarutil.ml28
-rw-r--r--engine/evarutil.mli14
-rw-r--r--kernel/reduction.ml21
-rw-r--r--kernel/reduction.mli5
-rw-r--r--kernel/univ.ml3
-rw-r--r--kernel/univ.mli3
-rw-r--r--pretyping/evarconv.ml29
-rw-r--r--pretyping/reductionops.ml8
-rw-r--r--test-suite/success/cumulativity.v13
9 files changed, 84 insertions, 40 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 6b3ce048f..8db603715 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -813,6 +813,34 @@ let subterm_source evk (loc,k) =
| _ -> evk in
(loc,Evar_kinds.SubEvar evk)
+let try_soft evd u u' =
+ let open Universes in
+ let make = Univ.Universe.make in
+ try Evd.add_universe_constraints evd (Constraints.singleton (make u,ULub,make u'))
+ with UState.UniversesDiffer | Univ.UniverseInconsistency _ -> evd
+
+(* Add equality constraints for covariant/invariant positions. For
+ irrelevant positions, unify universes when flexible. *)
+let compare_cumulative_instances cv_pb variances u u' sigma =
+ let cstrs = Univ.Constraint.empty in
+ let soft = [] in
+ let cstrs, soft = Array.fold_left3 (fun (cstrs, soft) v u u' ->
+ let open Univ.Variance in
+ match v with
+ | Irrelevant -> cstrs, (u,u')::soft
+ | Covariant when cv_pb == Reduction.CUMUL ->
+ Univ.Constraint.add (u,Univ.Le,u') cstrs, soft
+ | Covariant | Invariant -> Univ.Constraint.add (u,Univ.Eq,u') cstrs, soft)
+ (cstrs,soft) variances (Univ.Instance.to_array u) (Univ.Instance.to_array u')
+ in
+ match Evd.add_constraints sigma cstrs with
+ | sigma ->
+ Inl (List.fold_left (fun sigma (u,u') -> try_soft sigma u u') sigma soft)
+ | exception Univ.UniverseInconsistency p -> Inr p
+
+let compare_constructor_instances evd u u' =
+ Array.fold_left2 try_soft
+ evd (Univ.Instance.to_array u) (Univ.Instance.to_array u')
(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
[u] up to existential variable instantiation and equalisable
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 373875bd0..e289ca169 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -203,6 +203,20 @@ val kind_of_term_upto : evar_map -> Constr.constr ->
assumed to be an extention of those in [sigma1]. *)
val eq_constr_univs_test : evar_map -> evar_map -> Constr.constr -> Constr.constr -> bool
+(** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns
+ [Inl sigma'] where [sigma'] is [sigma] augmented with universe
+ constraints such that [u1 cv_pb? u2] according to [variance].
+ Additionally flexible universes in irrelevant positions are unified
+ if possible. Returns [Inr p] when the former is impossible. *)
+val compare_cumulative_instances : Reduction.conv_pb -> Univ.Variance.t array ->
+ Univ.Instance.t -> Univ.Instance.t -> evar_map ->
+ (evar_map, Univ.univ_inconsistency) Util.union
+
+(** We should only compare constructors at convertible types, so this
+ is only an opportunity to unify universes. *)
+val compare_constructor_instances : evar_map ->
+ Univ.Instance.t -> Univ.Instance.t -> evar_map
+
(** {6 Removing hyps in evars'context}
raise OccurHypInSimpleClause if the removal breaks dependencies *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index b3e689414..78b9e8c10 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -204,7 +204,8 @@ 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 : Univ.Constraint.t -> 'a -> 'a }
+ compare_cumul_instances : conv_pb -> Univ.Variance.t array ->
+ Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a }
type 'a universe_state = 'a * 'a universe_compare
@@ -220,12 +221,12 @@ let sort_cmp_universes env pb s0 s1 (u, check) =
let convert_instances ~flex u u' (s, check) =
(check.compare_instances ~flex u u' s, check)
-let get_cumulativity_constraints cv_pb cumi u u' =
+let get_cumulativity_constraints cv_pb variance u u' =
match cv_pb with
| CONV ->
- Univ.ACumulativityInfo.eq_constraints cumi u u' Univ.Constraint.empty
+ Univ.enforce_eq_variance_instances variance u u' Univ.Constraint.empty
| CUMUL ->
- Univ.ACumulativityInfo.leq_constraints cumi u u' Univ.Constraint.empty
+ Univ.enforce_leq_variance_instances variance u u' Univ.Constraint.empty
let inductive_cumulativity_arguments (mind,ind) =
mind.Declarations.mind_nparams +
@@ -243,8 +244,7 @@ let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2
if not (Int.equal num_param_arity nargs) then
cmp_instances u1 u2 s
else
- let csts = get_cumulativity_constraints cv_pb cumi u1 u2 in
- cmp_cumul csts s
+ cmp_cumul cv_pb (Univ.ACumulativityInfo.variance cumi) u1 u2 s
let convert_inductives cv_pb ind nargs u1 u2 (s, check) =
convert_inductives_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
@@ -271,7 +271,8 @@ let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u
else
(** By invariant, both constructors have a common supertype,
so they are convertible _at that type_. *)
- s
+ let variance = Array.make (Univ.Instance.length u1) Univ.Variance.Irrelevant in
+ cmp_cumul CONV variance u1 u2 s
let convert_constructors ctor nargs u1 u2 (s, check) =
convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
@@ -708,7 +709,8 @@ let check_convert_instances ~flex u u' univs =
else raise NotConvertible
(* general conversion and inference functions *)
-let check_inductive_instances csts univs =
+let check_inductive_instances cv_pb variance u1 u2 univs =
+ let csts = get_cumulativity_constraints cv_pb variance u1 u2 in
if (UGraph.check_constraints csts univs) then univs
else raise NotConvertible
@@ -758,7 +760,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 csts (univs,csts') =
+let infer_inductive_instances cv_pb variance u1 u2 (univs,csts') =
+ let csts = get_cumulativity_constraints cv_pb variance u1 u2 in
(univs, Univ.Constraint.union csts csts')
let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index ad52c93f6..14e4270b7 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -41,7 +41,8 @@ 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 : Univ.Constraint.t -> 'a -> 'a }
+ compare_cumul_instances : conv_pb -> Univ.Variance.t array ->
+ Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a }
type 'a universe_state = 'a * 'a universe_compare
@@ -49,7 +50,7 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a
type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
-val get_cumulativity_constraints : conv_pb -> Univ.ACumulativityInfo.t ->
+val get_cumulativity_constraints : conv_pb -> Univ.Variance.t array ->
Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t
val inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 584593e2f..be21381b7 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -914,6 +914,9 @@ let enforce_eq_instances x y =
(Pp.str " instances of different lengths."));
CArray.fold_right2 enforce_eq_level ax ay
+let enforce_eq_variance_instances = Variance.eq_constraints
+let enforce_leq_variance_instances = Variance.leq_constraints
+
let subst_instance_level s l =
match l.Level.data with
| Level.Var n -> s.(n)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index ce617932c..629d83fb8 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -312,6 +312,9 @@ type universe_instance = Instance.t
val enforce_eq_instances : Instance.t constraint_function
+val enforce_eq_variance_instances : Variance.t array -> Instance.t constraint_function
+val enforce_leq_variance_instances : Variance.t array -> Instance.t constraint_function
+
type 'a puniverses = 'a * Instance.t
val out_punivs : 'a puniverses -> 'a
val in_punivs : 'a -> 'a puniverses
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 130aa8cd7..d37090a65 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -352,34 +352,13 @@ let exact_ise_stack2 env evd f sk1 sk2 =
ise_stack2 evd (List.rev sk1) (List.rev sk2)
else UnifFailure (evd, (* Dummy *) NotSameHead)
-let try_soft evd u u' =
- let open Universes in
- let make = Univ.Universe.make in
- try Evd.add_universe_constraints evd (Constraints.singleton (make u,ULub,make u'))
- with UState.UniversesDiffer | Univ.UniverseInconsistency _ -> evd
-
(* Add equality constraints for covariant/invariant positions. For
irrelevant positions, unify universes when flexible. *)
let compare_cumulative_instances evd variances u u' =
- let cstrs = Univ.Constraint.empty in
- let soft = [] in
- let cstrs, soft = Array.fold_left3 (fun (cstrs, soft) v u u' ->
- let open Univ.Variance in
- match v with
- | Irrelevant -> cstrs, (u,u')::soft
- | Covariant | Invariant -> Univ.Constraint.add (u,Univ.Eq,u') cstrs, soft)
- (cstrs,soft) variances (Univ.Instance.to_array u) (Univ.Instance.to_array u')
- in
- match Evd.add_constraints evd cstrs with
- | evd ->
- Success (List.fold_left (fun evd (u,u') -> try_soft evd u u') evd soft)
- | exception Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
-
-(* We should only compare constructors at convertible types, so this
- is only an opportunity to unify universes. *)
-let compare_constructor_instances evd u u' =
- Array.fold_left2 try_soft
- evd (Univ.Instance.to_array u) (Univ.Instance.to_array u')
+ match Evarutil.compare_cumulative_instances CONV variances u u' evd with
+ | Inl evd ->
+ Success evd
+ | Inr p -> UnifFailure (evd, UnifUnivInconsistency p)
let rec evar_conv_x ts env evd pbty term1 term2 =
let term1 = whd_head_evar evd term1 in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 0a28f1fb8..47e2ba93b 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1313,10 +1313,10 @@ let sigma_compare_instances ~flex i0 i1 sigma =
| Univ.UniverseInconsistency _ ->
raise Reduction.NotConvertible
-let sigma_check_inductive_instances csts sigma =
- try Evd.add_constraints sigma csts
- with Evd.UniversesDiffer
- | Univ.UniverseInconsistency _ ->
+let sigma_check_inductive_instances cv_pb variance u1 u2 sigma =
+ match Evarutil.compare_cumulative_instances cv_pb variance u1 u2 sigma with
+ | Inl sigma -> sigma
+ | Inr _ ->
raise Reduction.NotConvertible
let sigma_univ_state =
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index 0394ea340..dfa305dc6 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -115,3 +115,16 @@ Definition checkcumul :=
(* They can only be compared at the highest type *)
Fail Definition checkcumul' :=
eq_refl _ : @eq twotys@{i k l} (twoconstr@{i j k} Tyi Tyi) (twoconstr@{j i k} Tyi Tyi).
+
+(* An inductive type with an irrelevant universe *)
+Inductive foo@{i} : Type@{i} := mkfoo { }.
+
+Definition bar := foo.
+
+(* The universe on mkfoo is flexible and should be unified with i. *)
+Definition foo1@{i} : foo@{i} := let x := mkfoo in x. (* fast path for conversion *)
+Definition foo2@{i} : bar@{i} := let x := mkfoo in x. (* must reduce *)
+
+(* Rigid universes however should not be unified unnecessarily. *)
+Definition foo3@{i j|} : foo@{i} := let x := mkfoo@{j} in x.
+Definition foo4@{i j|} : bar@{i} := let x := mkfoo@{j} in x.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 18:30:26 +0000