From 17a0dccfe91d6f837ce285e62b8d843720f8c1a1 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 16 Feb 2018 15:44:44 +0100 Subject: Allow using cumulativity without forcing strict constraints. Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative inductive would try to generate a constraint [i = j] and use cumulativity only if this resulted in an inconsistency. This is confusingly different from the behaviour with [Type] and means cumulativity can only be used to lift between universes related by strict inequalities. (This isn't a kernel restriction so there might be some workaround to send the kernel the right constraints, but not in a nice way.) See modified test for more details of what is now possible. Technical notes: When universe constraints were inferred by comparing the shape of terms without reduction, cumulativity was not used and so too-strict equality constraints were generated. Then in order to use cumulativity we had to make this comparison fail to fall back to full conversion. When unifiying 2 instances of a cumulative inductive type, if there are any Irrelevant universes we try to unify them if they are flexible. --- test-suite/success/cumulativity.v | 56 ++++++--------------------------------- 1 file changed, 8 insertions(+), 48 deletions(-) (limited to 'test-suite/success') diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index 4dda36042..0394ea340 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -10,40 +10,16 @@ Set Printing Universes. Inductive List (A: Type) := nil | cons : A -> List A -> List A. -Section ListLift. - Universe i j. - - Constraint i < j. - - Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x. - -End ListLift. +Definition LiftL@{k i j|k <= i, k <= j} {A:Type@{k}} : List@{i} A -> List@{j} A := fun x => x. Lemma LiftL_Lem A (l : List A) : l = LiftL l. Proof. reflexivity. Qed. -Section ListLower. - Universe i j. - - Constraint i < j. - - Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x. - -End ListLower. - -Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l. -Proof. reflexivity. Qed. - Inductive Tp := tp : Type -> Tp. -Section TpLift. - Universe i j. +Definition LiftTp@{i j|i <= j} : Tp@{i} -> Tp@{j} := fun x => x. - Constraint i < j. - - Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x. - -End TpLift. +Fail Definition LowerTp@{i j|j < i} : Tp@{i} -> Tp@{j} := fun x => x. Record Tp' := { tp' : Tp }. @@ -51,22 +27,12 @@ Definition CTp := Tp. (* here we have to reduce a constant to infer the correct subtyping. *) Record Tp'' := { tp'' : CTp }. -Definition LiftTp'@{i j|i < j} : Tp'@{i} -> Tp'@{j} := fun x => x. -Definition LiftTp''@{i j|i < j} : Tp''@{i} -> Tp''@{j} := fun x => x. +Definition LiftTp'@{i j|i <= j} : Tp'@{i} -> Tp'@{j} := fun x => x. +Definition LiftTp''@{i j|i <= j} : Tp''@{i} -> Tp''@{j} := fun x => x. Lemma LiftC_Lem (t : Tp) : LiftTp t = t. Proof. reflexivity. Qed. -Section TpLower. - Universe i j. - - Constraint i < j. - - Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x. - -End TpLower. - - Section subtyping_test. Universe i j. Constraint i < j. @@ -82,14 +48,8 @@ Record B (X : A) : Type := { b : X; }. NonCumulative Inductive NCList (A: Type) := ncnil | nccons : A -> NCList A -> NCList A. -Section NCListLift. - Universe i j. - - Constraint i < j. - - Fail Definition LiftNCL {A} : NCList@{i} A -> NCList@{j} A := fun x => x. - -End NCListLift. +Fail Definition LiftNCL@{k i j|k <= i, k <= j} {A:Type@{k}} + : NCList@{i} A -> NCList@{j} A := fun x => x. Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x. @@ -114,7 +74,7 @@ Fail Definition arrow_lift@{i i' j j' | i' < i, j < j'} : Arrow@{i j} -> Arrow@{i' j'} := fun x => x. -Definition arrow_lift@{i i' j j' | i' = i, j < j'} +Definition arrow_lift@{i i' j j' | i' = i, j <= j'} : Arrow@{i j} -> Arrow@{i' j'} := fun x => x. -- cgit v1.2.3 From db0918bfa5089f9ab44374504cbd0ddc758ea1e5 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 20 Feb 2018 00:27:40 +0100 Subject: Cumulativity: improve treatment of irrelevant universes. In Reductionops.infer_conv we did not have enough information to properly try to unify irrelevant universes. This requires changing the Reduction.universe_compare type a bit. --- engine/evarutil.ml | 28 ++++++++++++++++++++++++++++ engine/evarutil.mli | 14 ++++++++++++++ kernel/reduction.ml | 21 ++++++++++++--------- kernel/reduction.mli | 5 +++-- kernel/univ.ml | 3 +++ kernel/univ.mli | 3 +++ pretyping/evarconv.ml | 29 ++++------------------------- pretyping/reductionops.ml | 8 ++++---- test-suite/success/cumulativity.v | 13 +++++++++++++ 9 files changed, 84 insertions(+), 40 deletions(-) (limited to 'test-suite/success') 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. -- cgit v1.2.3