diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-20 00:27:40 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-09 16:29:06 +0100 |
commit | db0918bfa5089f9ab44374504cbd0ddc758ea1e5 (patch) | |
tree | 5b68a2bd48fc961987a193f4361c46f7b9940b33 | |
parent | 17a0dccfe91d6f837ce285e62b8d843720f8c1a1 (diff) |
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.
-rw-r--r-- | engine/evarutil.ml | 28 | ||||
-rw-r--r-- | engine/evarutil.mli | 14 | ||||
-rw-r--r-- | kernel/reduction.ml | 21 | ||||
-rw-r--r-- | kernel/reduction.mli | 5 | ||||
-rw-r--r-- | kernel/univ.ml | 3 | ||||
-rw-r--r-- | kernel/univ.mli | 3 | ||||
-rw-r--r-- | pretyping/evarconv.ml | 29 | ||||
-rw-r--r-- | pretyping/reductionops.ml | 8 | ||||
-rw-r--r-- | test-suite/success/cumulativity.v | 13 |
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. |