diff options
| -rw-r--r-- | kernel/constr.ml | 25 | ||||
| -rw-r--r-- | kernel/constr.mli | 4 | ||||
| -rw-r--r-- | kernel/nativeconv.ml | 2 | ||||
| -rw-r--r-- | kernel/reduction.ml | 200 | ||||
| -rw-r--r-- | kernel/reduction.mli | 24 | ||||
| -rw-r--r-- | kernel/univ.ml | 50 | ||||
| -rw-r--r-- | kernel/vconv.ml | 4 | ||||
| -rw-r--r-- | pretyping/evd.ml | 30 | ||||
| -rw-r--r-- | pretyping/evd.mli | 3 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 50 |
10 files changed, 253 insertions, 139 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index fbcdc886b..532d44d9e 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -578,16 +578,18 @@ let leq_constr_univs univs m n = compare_leq m n let eq_constr_univs_infer univs m n = - if m == n then true, Constraint.empty + if m == n then true, UniverseConstraints.empty else - let cstrs = ref Constraint.empty in + let cstrs = ref UniverseConstraints.empty in let eq_universes strict = Univ.Instance.check_eq univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - (cstrs := Univ.enforce_eq u1 u2 !cstrs; - true) + if Univ.check_eq univs u1 u2 then true + else + (cstrs := Univ.UniverseConstraints.add (u1, Univ.UEq, u2) !cstrs; + true) in let rec eq_constr' m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n @@ -596,23 +598,26 @@ let eq_constr_univs_infer univs m n = res, !cstrs let leq_constr_univs_infer univs m n = - if m == n then true, Constraint.empty + if m == n then true, UniverseConstraints.empty else - let cstrs = ref Constraint.empty in + let cstrs = ref UniverseConstraints.empty in let eq_universes strict l l' = Univ.Instance.check_eq univs l l' in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - (cstrs := Univ.enforce_eq u1 u2 !cstrs; - true) + if Univ.check_eq univs u1 u2 then true + else (cstrs := Univ.UniverseConstraints.add (u1, Univ.UEq, u2) !cstrs; + true) in let leq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - (cstrs := Univ.enforce_leq u1 u2 !cstrs; - true) + if Univ.check_leq univs u1 u2 then true + else + (cstrs := Univ.UniverseConstraints.add (u1, Univ.ULe, u2) !cstrs; + true) in let rec eq_constr' m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n diff --git a/kernel/constr.mli b/kernel/constr.mli index e9f736903..c57c4c59b 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -212,11 +212,11 @@ val leq_constr_univs : constr Univ.check_function (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, application grouping and the universe equalities in [u]. *) -val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.constrained +val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.universe_constrained (** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo alpha, casts, application grouping and the universe inequalities in [u]. *) -val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.constrained +val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.universe_constrained (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and the universe equalities in [c]. *) diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 766e6513c..5964ed70e 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -70,7 +70,7 @@ and conv_atom pb lvl a1 a2 cu = if not (eq_constant c1 c2) then raise NotConvertible; cu | Asort s1, Asort s2 -> - ignore(sort_cmp_universes pb s1 s2 (cu, None)); cu + check_sort_cmp_universes pb s1 s2 cu; cu | Avar id1, Avar id2 -> if not (Id.equal id1 id2) then raise NotConvertible; cu diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 5024675bf..b62ca2045 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -153,25 +153,51 @@ type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_fun type 'a universe_conversion_function = env -> Univ.universes -> 'a -> 'a -> unit type 'a trans_universe_conversion_function = Names.transparent_state -> 'a universe_conversion_function + +exception NotConvertible +exception NotConvertibleVect of int + + +(* Convertibility of sorts *) + +(* The sort cumulativity is + + Prop <= Set <= Type 1 <= ... <= Type i <= ... + + and this holds whatever Set is predicative or impredicative +*) + +type conv_pb = + | CONV + | CUMUL + +let is_cumul = function CUMUL -> true | CONV -> false +let is_pos = function Pos -> true | Null -> false + +type 'a universe_compare = + { (* Might raise NotConvertible *) + compare : conv_pb -> sorts -> sorts -> 'a -> 'a; + compare_instances: bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; + } + +type 'a universe_state = 'a * 'a universe_compare + +type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b + type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints type conv_universes = Univ.universes * Univ.constraints option -exception NotConvertible -exception NotConvertibleVect of int +let sort_cmp_universes pb s0 s1 (u, check) = + (check.compare pb s0 s1 u, check) + +let convert_instances flex u u' (s, check) = + (check.compare_instances flex u u' s, check) -let convert_universes (univs,cstrs as cuniv) u u' = - if Univ.Instance.check_eq univs u u' then cuniv - else - (match cstrs with - | None -> raise NotConvertible - | Some cstrs -> - (univs, Some (Univ.enforce_eq_instances u u' cstrs))) - let conv_table_key k1 k2 cuniv = match k1, k2 with | ConstKey (cst, u), ConstKey (cst', u') when eq_constant_key cst cst' -> - convert_universes cuniv u u' + convert_instances true u u' cuniv | _ -> raise NotConvertible let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = @@ -199,59 +225,6 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv else raise NotConvertible -(* Convertibility of sorts *) - -(* The sort cumulativity is - - Prop <= Set <= Type 1 <= ... <= Type i <= ... - - and this holds whatever Set is predicative or impredicative -*) - -type conv_pb = - | CONV - | CUMUL - -let is_cumul = function CUMUL -> true | CONV -> false -let is_pos = function Pos -> true | Null -> false - -let check_eq (univs, cstrs as cuniv) u u' = - match cstrs with - | None -> if check_eq univs u u' then cuniv else raise NotConvertible - | Some cstrs -> - univs, Some (Univ.enforce_eq u u' cstrs) - -let check_leq ?(record=false) (univs, cstrs as cuniv) u u' = - match cstrs with - | None -> if check_leq univs u u' then cuniv else raise NotConvertible - | Some cstrs -> - let cstrs' = Univ.enforce_leq u u' cstrs in - let cstrs' = if record then - Univ.Constraint.add (Option.get (Univ.Universe.level u),Univ.Le, - Option.get (Univ.Universe.level u')) cstrs' - else cstrs' - in - univs, Some cstrs' - -let sort_cmp_universes pb s0 s1 univs = - match (s0,s1) with - | (Prop c1, Prop c2) when is_cumul pb -> - begin match c1, c2 with - | Null, _ | _, Pos -> univs (* Prop <= Set *) - | _ -> raise NotConvertible - end - | (Prop c1, Prop c2) -> if c1 == c2 then univs else raise NotConvertible - | (Prop c1, Type u) -> - let u0 = univ_of_sort s0 in - (match pb with - | CUMUL -> check_leq ~record:true univs u0 u - | CONV -> check_eq univs u0 u) - | (Type u, Prop c) -> raise NotConvertible - | (Type u1, Type u2) -> - (match pb with - | CUMUL -> check_leq univs u1 u2 - | CONV -> check_eq univs u1 u2) - let rec no_arg_available = function | [] -> true | Zupdate _ :: stk -> no_arg_available stk @@ -489,14 +462,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FInd (ind1,u1), FInd (ind2,u2)) -> if eq_ind ind1 ind2 then - (let cuniv = convert_universes cuniv u1 u2 in + (let cuniv = convert_instances false u1 u2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv) else raise NotConvertible | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> if Int.equal j1 j2 && eq_ind ind1 ind2 then - (let cuniv = convert_universes cuniv u1 u2 in + (let cuniv = convert_instances false u1 u2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv) else raise NotConvertible @@ -577,6 +550,80 @@ let clos_fconv trans cv_pb l2r evars env univs t1 t2 = let infos = create_clos_infos ~evars reds env in ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs + +let check_eq univs u u' = + if not (check_eq univs u u') then raise NotConvertible + +let check_leq univs u u' = + if not (check_leq univs u u') then raise NotConvertible + +let check_sort_cmp_universes pb s0 s1 univs = + match (s0,s1) with + | (Prop c1, Prop c2) when is_cumul pb -> + begin match c1, c2 with + | Null, _ | _, Pos -> () (* Prop <= Set *) + | _ -> raise NotConvertible + end + | (Prop c1, Prop c2) -> if c1 != c2 then raise NotConvertible + | (Prop c1, Type u) -> + let u0 = univ_of_sort s0 in + (match pb with + | CUMUL -> check_leq univs u0 u + | CONV -> check_eq univs u0 u) + | (Type u, Prop c) -> raise NotConvertible + | (Type u1, Type u2) -> + (match pb with + | CUMUL -> check_leq univs u1 u2 + | CONV -> check_eq univs u1 u2) + +let checked_sort_cmp_universes pb s0 s1 univs = + check_sort_cmp_universes pb s0 s1 univs; univs + +let check_convert_instances _flex u u' univs = + if Univ.Instance.check_eq univs u u' then univs + else raise NotConvertible + +let checked_universes = + { compare = checked_sort_cmp_universes; + compare_instances = check_convert_instances } + +let infer_eq (univs, cstrs as cuniv) u u' = + if Univ.check_eq univs u u' then cuniv + else + univs, (Univ.enforce_eq u u' cstrs) + +let infer_leq (univs, cstrs as cuniv) u u' = + if Univ.check_leq univs u u' then cuniv + else + let cstrs' = Univ.enforce_leq u u' cstrs in + univs, cstrs' + +let infer_cmp_universes pb s0 s1 univs = + match (s0,s1) with + | (Prop c1, Prop c2) when is_cumul pb -> + begin match c1, c2 with + | Null, _ | _, Pos -> univs (* Prop <= Set *) + | _ -> raise NotConvertible + end + | (Prop c1, Prop c2) -> if c1 == c2 then univs else raise NotConvertible + | (Prop c1, Type u) -> + let u0 = univ_of_sort s0 in + (match pb with + | CUMUL -> infer_leq univs u0 u + | CONV -> infer_eq univs u0 u) + | (Type u, Prop c) -> raise NotConvertible + | (Type u1, Type u2) -> + (match pb with + | CUMUL -> infer_leq univs u1 u2 + | CONV -> infer_eq univs u1 u2) + +let infer_convert_instances flex u u' (univs,cstrs) = + (univs, Univ.enforce_eq_instances u u' cstrs) + +let infered_universes : (Univ.universes * Univ.Constraint.t) universe_compare = + { compare = infer_cmp_universes; + compare_instances = infer_convert_instances } + let trans_fconv_universes reds cv_pb l2r evars env univs t1 t2 = let b = if cv_pb = CUMUL then leq_constr_univs univs t1 t2 @@ -584,7 +631,7 @@ let trans_fconv_universes reds cv_pb l2r evars env univs t1 t2 = in if b then () else - let _ = clos_fconv reds cv_pb l2r evars env (univs, None) t1 t2 in + let _ = clos_fconv reds cv_pb l2r evars env (univs, checked_universes) t1 t2 in () (* Profiling *) @@ -621,16 +668,21 @@ let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 = v1 v2 +let generic_conv cv_pb l2r evars reds env univs t1 t2 = + let (s, _) = + clos_fconv reds cv_pb l2r evars env univs t1 t2 + in s + let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = - let b, cstrs = - if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2 + let b, cstrs = + if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2 else Constr.eq_constr_univs_infer univs t1 t2 in - if b then cstrs - else - let (u, cstrs) = - clos_fconv reds cv_pb l2r evars env (univs, Some Constraint.empty) t1 t2 - in Option.get cstrs + if b then (Univ.to_constraints univs cstrs) + else + let univs = ((univs, Univ.Constraint.empty), infered_universes) in + let ((_,cstrs), _) = clos_fconv reds cv_pb l2r evars env univs t1 t2 in + cstrs (* Profiling *) let infer_conv_universes = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index b9bd41f28..b45dca03e 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -26,20 +26,29 @@ val nf_betaiota : env -> constr -> constr exception NotConvertible exception NotConvertibleVect of int -type conv_universes = Univ.universes * Univ.constraints option - type 'a conversion_function = env -> 'a -> 'a -> unit type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_function type 'a universe_conversion_function = env -> Univ.universes -> 'a -> 'a -> unit type 'a trans_universe_conversion_function = Names.transparent_state -> 'a universe_conversion_function -type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints - type conv_pb = CONV | CUMUL -val sort_cmp_universes : - conv_pb -> sorts -> sorts -> conv_universes -> conv_universes +type 'a universe_compare = + { (* Might raise NotConvertible *) + compare : conv_pb -> sorts -> sorts -> 'a -> 'a; + compare_instances: bool (* Instance of a flexible constant? *) -> + Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; + } + +type 'a universe_state = 'a * 'a universe_compare + +type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b + +type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints + +val check_sort_cmp_universes : + conv_pb -> sorts -> sorts -> Univ.universes -> unit (* val sort_cmp : *) (* conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints *) @@ -71,6 +80,9 @@ val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> ?ts:Names.transparent_state -> types infer_conversion_function +val generic_conv : conv_pb -> bool -> (existential->constr option) -> + Names.transparent_state -> (constr,'a) generic_conversion_function + (** option for conversion *) val set_vm_conv : (conv_pb -> types conversion_function) -> unit val vm_conv : conv_pb -> types conversion_function diff --git a/kernel/univ.ml b/kernel/univ.ml index 46857ab27..1c60f2c3a 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -401,6 +401,12 @@ module Level = struct | Prop -> true | _ -> false + let is_set x = + match data x with + | Set -> true + | _ -> false + + (* A specialized comparison function: we compare the [int] part first. This way, most of the time, the [DirPath.t] part is not considered. @@ -774,9 +780,10 @@ type canonical_arc = { univ: Level.t; lt: Level.t list; le: Level.t list; - rank : int} + rank : int; + predicative : bool} -let terminal u = {univ=u; lt=[]; le=[]; rank=0} +let terminal u = {univ=u; lt=[]; le=[]; rank=0; predicative=false} module UMap : sig @@ -1088,10 +1095,9 @@ let check_equal g u v = let _, arcv = safe_repr g v in arcu == arcv -let set_arc g = - snd (safe_repr g Level.set) - -let prop_arc g = snd (safe_repr g Level.prop) +let is_set_arc u = Level.is_set u.univ +let is_prop_arc u = Level.is_prop u.univ +let get_prop_arc g = snd (safe_repr g Level.prop) let check_smaller g strict u v = let g, arcu = safe_repr g u in @@ -1099,10 +1105,9 @@ let check_smaller g strict u v = if strict then is_lt g arcu arcv else - let proparc = prop_arc g in - arcu == proparc || - ((arcv != proparc && arcu == set_arc g) || - is_leq g arcu arcv) + is_prop_arc arcu + || (is_set_arc arcu && arcv.predicative) + || is_leq g arcu arcv (** Then, checks on universes *) @@ -1166,12 +1171,20 @@ let check_leq = (** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *) +(** To speed up tests of Set </<= i *) +let set_predicative g arcv = + enter_arc {arcv with predicative = true} g + (* setlt : Level.t -> Level.t -> reason -> unit *) (* forces u > v *) (* this is normally an update of u in g rather than a creation. *) let setlt g arcu arcv = let arcu' = {arcu with lt=arcv.univ::arcu.lt} in - enter_arc arcu' g, arcu' + let g = + if is_set_arc arcu then set_predicative g arcv + else g + in + enter_arc arcu' g, arcu' (* checks that non-redundant *) let setlt_if (g,arcu) v = @@ -1184,8 +1197,12 @@ let setlt_if (g,arcu) v = (* this is normally an update of u in g rather than a creation. *) let setleq g arcu arcv = let arcu' = {arcu with le=arcv.univ::arcu.le} in - enter_arc arcu' g, arcu' - + let g = + if is_set_arc arcu' then + set_predicative g arcv + else g + in + enter_arc arcu' g, arcu' (* checks that non-redundant *) let setleq_if (g,arcu) v = @@ -1321,7 +1338,7 @@ let is_initial_universes g = UMap.equal (==) g initial_universes let add_universe vlev g = let v = terminal vlev in - let proparc = prop_arc g in + let proparc = get_prop_arc g in enter_arc {proparc with le=vlev::proparc.le} (enter_arc v g) @@ -1433,8 +1450,6 @@ module UniverseConstraints = struct include S let add (l,d,r as cst) s = - if (Option.is_empty (Universe.level r)) then - prerr_endline "Algebraic universe on the right"; if Universe.equal l r then s else add cst s @@ -2028,6 +2043,7 @@ let normalize_universes g = lt = LSet.elements lt; le = LSet.elements le; rank = rank; + predicative = false; } in UMap.mapi canonicalize g @@ -2155,7 +2171,7 @@ let sort_universes orig = let fold i accu u = if 0 < i then let pred = types.(i - 1) in - let arc = {univ = u; lt = [pred]; le = []; rank = 0} in + let arc = {univ = u; lt = [pred]; le = []; rank = 0; predicative = false} in UMap.add u (Canonical arc) accu else accu in diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 8e623415e..0e91c7972 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -50,7 +50,7 @@ let rec conv_val pb k v1 v2 cu = and conv_whd pb k whd1 whd2 cu = match whd1, whd2 with - | Vsort s1, Vsort s2 -> ignore(sort_cmp_universes pb s1 s2 (cu,None)); cu + | Vsort s1, Vsort s2 -> check_sort_cmp_universes pb s1 s2 cu; cu | Vprod p1, Vprod p2 -> let cu = conv_val CONV k (dom p1) (dom p2) cu in conv_fun pb k (codom p1) (codom p2) cu @@ -188,7 +188,7 @@ let rec conv_eq pb t1 t2 cu = if Int.equal m1 m2 then cu else raise NotConvertible | Var id1, Var id2 -> if Id.equal id1 id2 then cu else raise NotConvertible - | Sort s1, Sort s2 -> ignore(sort_cmp_universes pb s1 s2 (cu,None)); cu + | Sort s1, Sort s2 -> check_sort_cmp_universes pb s1 s2 cu; cu | Cast (c1,_,_), _ -> conv_eq pb c1 t2 cu | _, Cast (c2,_,_) -> conv_eq pb t1 c2 cu | Prod (_,t1,c1), Prod (_,t2,c2) -> diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 038b91ec6..e125a1c6e 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -408,11 +408,12 @@ let process_universe_constraints univs vars alg templ cstrs = | None -> error ("Algebraic universe on the right") | Some rl -> if Univ.Level.is_small rl then - (if Univ.LSet.for_all (fun l -> - Univ.Level.is_small l || Univ.LMap.mem l !vars) - (Univ.Universe.levels l) then - Univ.enforce_leq l r local - else raise (Univ.UniverseInconsistency (Univ.Le, l, r, []))) + let levels = Univ.Universe.levels l in + Univ.LSet.fold (fun l local -> + if Univ.Level.is_small l || Univ.LMap.mem l !vars then + Univ.enforce_eq (Univ.Universe.make l) r local + else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, []))) + levels local else if Univ.LSet.mem rl templ && Univ.Universe.is_level l then unify_universes fo l Univ.UEq r local else @@ -446,8 +447,7 @@ let process_universe_constraints univs vars alg templ cstrs = Univ.enforce_eq_level l' r' local | _, _ (* One of the two is algebraic or global *) -> if Univ.check_eq univs l r then local - else - raise UniversesDiffer + else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, [])) in let local = Univ.UniverseConstraints.fold (fun (l,d,r) local -> unify_universes false l d r local) @@ -1151,9 +1151,9 @@ let set_eq_level d u1 u2 = let set_leq_level d u1 u2 = add_constraints d (Univ.enforce_leq_level u1 u2 Univ.Constraint.empty) -let set_eq_instances d u1 u2 = +let set_eq_instances ?(flex=false) d u1 u2 = add_universe_constraints d - (Univ.enforce_eq_instances_univs false u1 u2 Univ.UniverseConstraints.empty) + (Univ.enforce_eq_instances_univs flex u1 u2 Univ.UniverseConstraints.empty) let set_leq_sort evd s1 s2 = let s1 = normalize_sort evd s1 @@ -1161,12 +1161,12 @@ let set_leq_sort evd s1 s2 = match is_eq_sort s1 s2 with | None -> evd | Some (u1, u2) -> - if Univ.is_type0_univ u2 then - if Univ.is_small_univ u1 then evd - else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) - else if Univ.is_type0m_univ u2 then - raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) - else + (* if Univ.is_type0_univ u2 then *) + (* if Univ.is_small_univ u1 then evd *) + (* else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *) + (* else if Univ.is_type0m_univ u2 then *) + (* raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *) + (* else *) add_universe_constraints evd (Univ.UniverseConstraints.singleton (u1,Univ.ULe,u2)) let check_eq evd s s' = diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 8a9753e5b..8bdfccb6b 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -458,7 +458,8 @@ val set_eq_sort : evar_map -> sorts -> sorts -> evar_map val has_lub : evar_map -> Univ.universe -> Univ.universe -> evar_map val set_eq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map val set_leq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map -val set_eq_instances : evar_map -> Univ.universe_instance -> Univ.universe_instance -> evar_map +val set_eq_instances : ?flex:bool -> + evar_map -> Univ.universe_instance -> Univ.universe_instance -> evar_map val check_eq : evar_map -> Univ.universe -> Univ.universe -> bool val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 2d8e935bb..f75da1383 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1124,7 +1124,7 @@ let pb_equal = function | Reduction.CONV -> Reduction.CONV let sort_cmp cv_pb s1 s2 u = - ignore(Reduction.sort_cmp_universes cv_pb s1 s2 (u, None)) + Reduction.check_sort_cmp_universes cv_pb s1 s2 u let test_trans_conversion (f: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y = try @@ -1145,22 +1145,50 @@ let is_fconv = function | Reduction.CONV -> is_conv | Reduction.CUMUL -> is_conv let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = let f = match pb with | Reduction.CONV -> Reduction.trans_conv_universes - | Reduction.CUMUL -> Reduction.trans_conv_leq_universes in + | Reduction.CUMUL -> Reduction.trans_conv_leq_universes + in try f ~evars:(safe_evar_value sigma) ts env (Evd.universes sigma) x y; true with Reduction.NotConvertible -> false | Univ.UniverseInconsistency _ -> false | e when is_anomaly e -> error "Conversion test raised an anomaly" +let sigma_compare_sorts pb s0 s1 sigma = + match pb with + | Reduction.CONV -> Evd.set_eq_sort sigma s0 s1 + | Reduction.CUMUL -> Evd.set_leq_sort sigma s0 s1 + +let sigma_compare_instances flex i0 i1 sigma = + try Evd.set_eq_instances ~flex sigma i0 i1 + with Evd.UniversesDiffer -> raise Reduction.NotConvertible + +let sigma_univ_state = + { Reduction.compare = sigma_compare_sorts; + Reduction.compare_instances = sigma_compare_instances } + let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = - let f = match pb with - | Reduction.CONV -> Reduction.infer_conv - | Reduction.CUMUL -> Reduction.infer_conv_leq in - try - let cstrs = f ~evars:(safe_evar_value sigma) ~ts env (Evd.universes sigma) x y in - Evd.add_constraints sigma cstrs, true - with Reduction.NotConvertible -> sigma, false - | Univ.UniverseInconsistency _ -> sigma, false - | e when is_anomaly e -> error "Conversion test raised an anomaly" + try + let b, sigma = + let b, cstrs = + if pb == Reduction.CUMUL then + Constr.leq_constr_univs_infer (Evd.universes sigma) x y + else + Constr.eq_constr_univs_infer (Evd.universes sigma) x y + in + if b then + try true, Evd.add_universe_constraints sigma cstrs + with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> false, sigma + else false, sigma + in + if b then sigma, true + else + let sigma' = + Reduction.generic_conv pb false (safe_evar_value sigma) ts + env (sigma, sigma_univ_state) x y in + sigma', true + with + | Reduction.NotConvertible -> sigma, false + | Univ.UniverseInconsistency _ -> sigma, false + | e when is_anomaly e -> error "Conversion test raised an anomaly" (********************************************************************) (* Special-Purpose Reduction *) |