diff options
| -rw-r--r-- | engine/termops.ml | 5 | ||||
| -rw-r--r-- | engine/universes.ml | 4 | ||||
| -rw-r--r-- | engine/universes.mli | 4 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 16 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 18 | ||||
| -rw-r--r-- | pretyping/unification.ml | 13 |
6 files changed, 37 insertions, 23 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 298302815a..04f55f2c35 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -609,7 +609,10 @@ let vars_of_global_reference env gr = [m] is appropriately lifted through abstractions of [t] *) let dependent_main noevar univs m t = - let eqc x y = if univs then fst (Universes.eq_constr_universes x y) else eq_constr_nounivs x y in + let eqc x y = + if univs then not (Option.is_empty (Universes.eq_constr_universes x y)) + else eq_constr_nounivs x y + in let rec deprec m t = if eqc m t then raise Occur diff --git a/engine/universes.ml b/engine/universes.ml index 0573dd2c60..6720fcef8f 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -199,7 +199,7 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu = if res then Some !cstrs else None let test_constr_universes leq m n = - if m == n then true, Constraints.empty + if m == n then Some Constraints.empty else let cstrs = ref Constraints.empty in let eq_universes strict l l' = @@ -229,7 +229,7 @@ let test_constr_universes leq m n = else Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in - res, !cstrs + if res then Some !cstrs else None let eq_constr_universes m n = test_constr_universes false m n let leq_constr_universes m n = test_constr_universes true m n diff --git a/engine/universes.mli b/engine/universes.mli index 0aeea91cdc..725c21d296 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -88,11 +88,11 @@ val leq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator -> (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and the universe constraints in [c]. *) -val eq_constr_universes : constr -> constr -> bool universe_constrained +val eq_constr_universes : constr -> constr -> universe_constraints option (** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo alpha, casts, application grouping and the universe constraints in [c]. *) -val leq_constr_universes : constr -> constr -> bool universe_constrained +val leq_constr_universes : constr -> constr -> universe_constraints option (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and the universe constraints in [c]. *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3ef0bb1b35..d06009dce5 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -401,14 +401,16 @@ 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 b,univs = Universes.eq_constr_universes term term' in - if b then + let univs = Universes.eq_constr_universes term term' in + match univs with + | Some univs -> ise_and evd [(fun i -> let cstrs = Universes.to_constraints (Evd.universes i) univs in try Success (Evd.add_constraints i cstrs) with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')] - else UnifFailure (evd,NotSameHead) + | None -> + UnifFailure (evd,NotSameHead) in let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM = let switch f a b = if on_left then f a b else f b a in @@ -650,14 +652,16 @@ 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 b,univs = Universes.eq_constr_universes term1 term2 in - if b then + let univs = Universes.eq_constr_universes term1 term2 in + match univs with + | Some univs -> ise_and i [(fun i -> try Success (Evd.add_universe_constraints i univs) with UniversesDiffer -> UnifFailure (i,NotSameHead) | Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] - else UnifFailure (i,NotSameHead) + | None -> + UnifFailure (i,NotSameHead) and f2 i = (try if not (snd ts) then raise Not_found diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 0ab941b346..a85e493eae 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -681,13 +681,17 @@ let magicaly_constant_of_fixbody env reference bd = function match constant_opt_value_in env (cst,u) with | None -> bd | Some t -> - let b, csts = Universes.eq_constr_universes t bd in - let subst = Universes.Constraints.fold (fun (l,d,r) acc -> - Univ.LMap.add (Option.get (Universe.level l)) (Option.get (Universe.level r)) acc) - csts Univ.LMap.empty - in - let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in - if b then mkConstU (cst,inst) else bd + let csts = Universes.eq_constr_universes 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) + csts Univ.LMap.empty + in + let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in + mkConstU (cst,inst) + | None -> bd + end with | Not_found -> bd diff --git a/pretyping/unification.ml b/pretyping/unification.ml index e73c5ffaf3..e2b3af7e97 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -558,19 +558,22 @@ let force_eqs c = c Universes.Constraints.empty let constr_cmp pb sigma flags t u = - let b, cstrs = + let cstrs = if pb == Reduction.CONV then Universes.eq_constr_universes t u else Universes.leq_constr_universes t u in - if b then - try Evd.add_universe_constraints sigma cstrs, b + match cstrs with + | Some cstrs -> + begin try Evd.add_universe_constraints sigma cstrs, true with Univ.UniverseInconsistency _ -> sigma, false | Evd.UniversesDiffer -> if is_rigid_head flags t then - try Evd.add_universe_constraints sigma (force_eqs cstrs), b + try Evd.add_universe_constraints sigma (force_eqs cstrs), true with Univ.UniverseInconsistency _ -> sigma, false else sigma, false - else sigma, b + end + | None -> + sigma, false let do_reduce ts (env, nb) sigma c = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state |