aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-16 15:44:44 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-03-09 16:29:06 +0100
commit17a0dccfe91d6f837ce285e62b8d843720f8c1a1 (patch)
tree605a2dae6692cec6503ab5fcdce7c90421db26f0 /pretyping
parent3d86afb36517c9ba4200289e169239f7fa54fca1 (diff)
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.
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/evarconv.ml175
-rw-r--r--pretyping/evarsolve.ml2
-rw-r--r--pretyping/reductionops.ml6
-rw-r--r--pretyping/unification.ml12
4 files changed, 86 insertions, 109 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index fe2e86a48..130aa8cd7 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -352,10 +352,34 @@ let exact_ise_stack2 env evd f sk1 sk2 =
ise_stack2 evd (List.rev sk1) (List.rev sk2)
else UnifFailure (evd, (* Dummy *) NotSameHead)
-let check_leq_inductives evd cumi u u' =
- let u = EConstr.EInstance.kind evd u in
- let u' = EConstr.EInstance.kind evd u' in
- Evd.add_constraints evd (Reduction.get_cumulativity_constraints CUMUL cumi u u')
+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')
let rec evar_conv_x ts env evd pbty term1 term2 =
let term1 = whd_head_evar evd term1 in
@@ -446,103 +470,56 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
else evar_eqappr_x ts env' evd CONV out2 out1
in
let rigids env evd sk term sk' term' =
- let check_strict () =
- let univs = EConstr.eq_constr_universes evd term term' in
- match univs with
- | Some univs ->
- begin
- let cstrs = Universes.to_constraints (Evd.universes evd) univs in
- try Success (Evd.add_constraints evd cstrs)
- with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
- end
- | None ->
- UnifFailure (evd, NotSameHead)
+ let check_strict evd u u' =
+ let cstrs = Univ.enforce_eq_instances u u' Univ.Constraint.empty in
+ try Success (Evd.add_constraints evd cstrs)
+ with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
in
- let first_try_strict_check cond u u' try_subtyping_constraints =
- if cond then
- let univs = EConstr.eq_constr_universes evd term term' in
- match univs with
- | Some univs ->
- begin
- let cstrs = Universes.to_constraints (Evd.universes evd) univs in
- try Success (Evd.add_constraints evd cstrs)
- with Univ.UniverseInconsistency p -> try_subtyping_constraints ()
- end
- | None ->
- UnifFailure (evd, NotSameHead)
- else
- UnifFailure (evd, NotSameHead)
- in
- let compare_heads evd =
+ let compare_heads evd =
match EConstr.kind evd term, EConstr.kind evd term' with
- | Const (c, u), Const (c', u') ->
- check_strict ()
- | Ind (ind, u), Ind (ind', u') ->
- let check_subtyping_constraints () =
- let nparamsaplied = Stack.args_size sk in
- let nparamsaplied' = Stack.args_size sk' in
- begin
- let mind = Environ.lookup_mind (fst ind) env in
- match mind.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
- UnifFailure (evd, NotSameHead)
- | Declarations.Cumulative_ind cumi ->
- begin
- let num_param_arity =
- mind.Declarations.mind_nparams +
- mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
- in
- if not (num_param_arity = nparamsaplied
- && num_param_arity = nparamsaplied') then
- UnifFailure (evd, NotSameHead)
- else
- begin
- let evd' = check_leq_inductives evd cumi u u' in
- Success (check_leq_inductives evd' cumi u' u)
- end
- end
+ | Const (c, u), Const (c', u') when Constant.equal c c' ->
+ let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+ check_strict evd u u'
+ | Const _, Const _ -> UnifFailure (evd, NotSameHead)
+ | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.eq_ind ind ind' ->
+ if EInstance.is_empty u && EInstance.is_empty u' then Success evd
+ else
+ let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+ let mind = Environ.lookup_mind mi env in
+ let open Declarations in
+ begin match mind.mind_universes with
+ | Monomorphic_ind _ -> assert false
+ | Polymorphic_ind _ -> check_strict evd u u'
+ | Cumulative_ind cumi ->
+ let nparamsaplied = Stack.args_size sk in
+ let nparamsaplied' = Stack.args_size sk' in
+ let needed = Reduction.inductive_cumulativity_arguments (mind,i) in
+ if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed)
+ then check_strict evd u u'
+ else
+ compare_cumulative_instances evd (Univ.ACumulativityInfo.variance cumi) u u'
end
- in
- first_try_strict_check (Names.eq_ind ind ind') u u' check_subtyping_constraints
- | Construct (cons, u), Construct (cons', u') ->
- let check_subtyping_constraints () =
- let ind, ind' = fst cons, fst cons' in
- let j, j' = snd cons, snd cons' in
- let nparamsaplied = Stack.args_size sk in
- let nparamsaplied' = Stack.args_size sk' in
- let mind = Environ.lookup_mind (fst ind) env in
- match mind.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
- UnifFailure (evd, NotSameHead)
- | Declarations.Cumulative_ind cumi ->
- begin
- let num_cnstr_args =
- let nparamsctxt =
- mind.Declarations.mind_nparams +
- mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
- in
- nparamsctxt +
- mind.Declarations.mind_packets.(snd ind).
- Declarations.mind_consnrealargs.(j - 1)
- in
- if not (num_cnstr_args = nparamsaplied
- && num_cnstr_args = nparamsaplied') then
- UnifFailure (evd, NotSameHead)
+ | Ind _, Ind _ -> UnifFailure (evd, NotSameHead)
+ | Construct (((mi,ind),ctor as cons), u), Construct (cons', u')
+ when Names.eq_constructor cons cons' ->
+ if EInstance.is_empty u && EInstance.is_empty u' then Success evd
+ else
+ let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+ let mind = Environ.lookup_mind mi env in
+ let open Declarations in
+ begin match mind.mind_universes with
+ | Monomorphic_ind _ -> assert false
+ | Polymorphic_ind _ -> check_strict evd u u'
+ | Cumulative_ind cumi ->
+ let nparamsaplied = Stack.args_size sk in
+ let nparamsaplied' = Stack.args_size sk' in
+ let needed = Reduction.constructor_cumulativity_arguments (mind,ind,ctor) in
+ if not (Int.equal nparamsaplied needed && Int.equal nparamsaplied' needed)
+ then check_strict evd u u'
else
- begin
- (** Both constructors should be liftable to the same supertype
- at which we compare them, but we don't have access to that type in
- untyped unification. We hence try to enforce that one is lower
- than the other, also unifying more universes in the process.
- If this fails we just leave the universes as is, as in conversion. *)
- try Success (check_leq_inductives evd cumi u u')
- with Univ.UniverseInconsistency _ ->
- try Success (check_leq_inductives evd cumi u' u)
- with Univ.UniverseInconsistency e -> Success evd
- end
- end
- in
- first_try_strict_check (Names.eq_constructor cons cons') u u' check_subtyping_constraints
+ Success (compare_constructor_instances evd u u')
+ end
+ | Construct _, Construct _ -> UnifFailure (evd, NotSameHead)
| _, _ -> anomaly (Pp.str "")
in
ise_and evd [(fun i ->
@@ -789,7 +766,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
allow this identification (first-order unification of universes). Otherwise
fallback to unfolding.
*)
- let univs = EConstr.eq_constr_universes evd term1 term2 in
+ let univs = EConstr.eq_constr_universes env evd term1 term2 in
match univs with
| Some univs ->
ise_and i [(fun i ->
@@ -1096,7 +1073,7 @@ let apply_on_subterm env evdref f c t =
(* By using eq_constr, we make an approximation, for instance, we *)
(* could also be interested in finding a term u convertible to t *)
(* such that c occurs in u *)
- let eq_constr c1 c2 = match EConstr.eq_constr_universes !evdref c1 c2 with
+ let eq_constr c1 c2 = match EConstr.eq_constr_universes env !evdref c1 c2 with
| None -> false
| Some cstr ->
try ignore (Evd.add_universe_constraints !evdref cstr); true
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index c9030be2d..96d80741a 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1337,7 +1337,7 @@ type conv_fun_bool =
let solve_refl ?(can_drop=false) conv_algo env evd pbty evk argsv1 argsv2 =
let evdref = ref evd in
- let eq_constr c1 c2 = match EConstr.eq_constr_universes !evdref c1 c2 with
+ let eq_constr c1 c2 = match EConstr.eq_constr_universes env !evdref c1 c2 with
| None -> false
| Some cstr ->
try ignore (Evd.add_universe_constraints !evdref cstr); true
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 44a69d1c1..0a28f1fb8 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -698,7 +698,7 @@ let magicaly_constant_of_fixbody env sigma reference bd = function
match constant_opt_value_in env (cst,u) with
| None -> bd
| Some t ->
- let csts = EConstr.eq_constr_universes sigma (EConstr.of_constr t) bd in
+ let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in
begin match csts with
| Some csts ->
let subst = Universes.Constraints.fold (fun (l,d,r) acc ->
@@ -1332,9 +1332,9 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
let b, sigma =
let ans =
if pb == Reduction.CUMUL then
- EConstr.leq_constr_universes sigma x y
+ EConstr.leq_constr_universes env sigma x y
else
- EConstr.eq_constr_universes sigma x y
+ EConstr.eq_constr_universes env sigma x y
in
let ans = match ans with
| None -> None
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f4269a2c5..1cd8d3940 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -568,10 +568,10 @@ let force_eqs c =
Universes.Constraints.add c' acc)
c Universes.Constraints.empty
-let constr_cmp pb sigma flags t u =
+let constr_cmp pb env sigma flags t u =
let cstrs =
- if pb == Reduction.CONV then EConstr.eq_constr_universes sigma t u
- else EConstr.leq_constr_universes sigma t u
+ if pb == Reduction.CONV then EConstr.eq_constr_universes env sigma t u
+ else EConstr.leq_constr_universes env sigma t u
in
match cstrs with
| Some cstrs ->
@@ -736,7 +736,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
| Evar (evk,_ as ev), Evar (evk',_)
when not (Evar.Set.mem evk flags.frozen_evars)
&& Evar.equal evk evk' ->
- let sigma',b = constr_cmp cv_pb sigma flags cM cN in
+ let sigma',b = constr_cmp cv_pb env sigma flags cM cN in
if b then
sigma',metasubst,evarsubst
else
@@ -918,7 +918,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn : subst0) cM cN =
try canonical_projections curenvnb pb opt cM cN substn
with ex when precatchable_exception ex ->
- let sigma', b = constr_cmp cv_pb sigma flags cM cN in
+ let sigma', b = constr_cmp cv_pb env sigma flags cM cN in
if b then (sigma', metas, evars)
else
try reduce curenvnb pb opt substn cM cN
@@ -1087,7 +1087,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
else
let sigma, b = match flags.modulo_conv_on_closed_terms with
| Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n
- | _ -> constr_cmp cv_pb sigma flags m n in
+ | _ -> constr_cmp cv_pb env sigma flags m n in
if b then Some sigma
else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
| Some (cv_id, cv_k), (dl_id, dl_k) ->