diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 154 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 2 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 37 | ||||
| -rw-r--r-- | pretyping/unification.ml | 33 |
4 files changed, 102 insertions, 124 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index fe2e86a48..d37090a65 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -352,10 +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 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') +(* Add equality constraints for covariant/invariant positions. For + irrelevant positions, unify universes when flexible. *) +let compare_cumulative_instances evd variances u 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 @@ -446,103 +449,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 +745,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 +1052,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 0e66ff0b6..9e3e68f05 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -29,6 +29,16 @@ exception Elimconst their parameters in its stack. *) +let _ = Goptions.declare_bool_option { + Goptions.optdepr = false; + Goptions.optname = + "Generate weak constraints between Irrelevant universes"; + Goptions.optkey = ["Cumulativity";"Weak";"Constraints"]; + Goptions.optread = (fun () -> not !UState.drop_weak_constraints); + Goptions.optwrite = (fun a -> UState.drop_weak_constraints:=not a); +} + + (** Support for reduction effects *) open Mod_subst @@ -691,18 +701,25 @@ let reducible_mind_case sigma c = match EConstr.kind sigma c with let magicaly_constant_of_fixbody env sigma reference bd = function | Name.Anonymous -> bd | Name.Name id -> + let open Universes in try let (cst_mod,cst_sect,_) = Constant.repr3 reference in let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in - let (cst, u), ctx = Universes.fresh_constant_instance env cst in + let (cst, u), ctx = fresh_constant_instance env cst in 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 -> - Univ.LMap.add (Option.get (Universe.level l)) (Option.get (Universe.level r)) acc) + let subst = Constraints.fold (fun cst acc -> + let l, r = match cst with + | ULub (u, v) | UWeak (u, v) -> u, v + | UEq (u, v) | ULe (u, v) -> + let get u = Option.get (Universe.level u) in + get u, get v + in + Univ.LMap.add l r acc) csts Univ.LMap.empty in let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in @@ -1315,10 +1332,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 = @@ -1334,9 +1351,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..f2f922fd5 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -561,17 +561,22 @@ let is_rigid_head sigma flags t = | Lambda (_, _, _) | LetIn (_, _, _, _) | App (_, _) | Case (_, _, _, _) | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *) -let force_eqs c = - Universes.Constraints.fold - (fun ((l,d,r) as c) acc -> - let c' = if d == Universes.ULub then (l,Universes.UEq,r) else c in - Universes.Constraints.add c' acc) - c Universes.Constraints.empty - -let constr_cmp pb sigma flags t u = +let force_eqs c = + let open Universes in + Constraints.fold + (fun c acc -> + let c' = match c with + (* Should we be forcing weak constraints? *) + | ULub (l, r) | UWeak (l, r) -> UEq (Univ.Universe.make l,Univ.Universe.make r) + | ULe _ | UEq _ -> c + in + Constraints.add c' acc) + c Constraints.empty + +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 -> @@ -579,7 +584,7 @@ let constr_cmp pb sigma flags t u = with Univ.UniverseInconsistency _ -> sigma, false | Evd.UniversesDiffer -> if is_rigid_head sigma flags t then - try Evd.add_universe_constraints sigma (force_eqs cstrs), true + try Evd.add_universe_constraints sigma (force_eqs cstrs), true with Univ.UniverseInconsistency _ -> sigma, false else sigma, false end @@ -736,7 +741,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 +923,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 +1092,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) -> |