diff options
| -rw-r--r-- | dev/top_printers.ml | 2 | ||||
| -rw-r--r-- | kernel/constr.ml | 61 | ||||
| -rw-r--r-- | kernel/constr.mli | 37 | ||||
| -rw-r--r-- | kernel/reduction.ml | 2 | ||||
| -rw-r--r-- | kernel/term.ml | 2 | ||||
| -rw-r--r-- | kernel/term.mli | 16 | ||||
| -rw-r--r-- | kernel/univ.ml | 241 | ||||
| -rw-r--r-- | kernel/univ.mli | 65 | ||||
| -rw-r--r-- | library/universes.ml | 192 | ||||
| -rw-r--r-- | library/universes.mli | 142 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 2 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 6 | ||||
| -rw-r--r-- | pretyping/evd.ml | 28 | ||||
| -rw-r--r-- | pretyping/evd.mli | 2 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 8 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 2 | ||||
| -rw-r--r-- | pretyping/termops.ml | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 12 | ||||
| -rw-r--r-- | printing/ppconstr.ml | 7 | ||||
| -rw-r--r-- | proofs/refiner.ml | 3 | ||||
| -rw-r--r-- | proofs/refiner.mli | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
22 files changed, 418 insertions, 417 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index c35d04e9d..fb8509c50 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -191,7 +191,7 @@ let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l) let ppevar_universe_context l = pp (Evd.pr_evar_universe_context l) let ppconstraints_map c = pp (Universes.pr_constraints_map c) let ppconstraints c = pp (pr_constraints c) -let ppuniverseconstraints c = pp (UniverseConstraints.pr c) +let ppuniverseconstraints c = pp (Universes.Constraints.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx diff --git a/kernel/constr.ml b/kernel/constr.ml index 532d44d9e..9be04c765 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -578,9 +578,9 @@ let leq_constr_univs univs m n = compare_leq m n let eq_constr_univs_infer univs m n = - if m == n then true, UniverseConstraints.empty + if m == n then true, Constraint.empty else - let cstrs = ref UniverseConstraints.empty in + let cstrs = ref Constraint.empty in let eq_universes strict = Univ.Instance.check_eq univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true @@ -588,7 +588,7 @@ let eq_constr_univs_infer univs m n = let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in if Univ.check_eq univs u1 u2 then true else - (cstrs := Univ.UniverseConstraints.add (u1, Univ.UEq, u2) !cstrs; + (cstrs := Univ.enforce_eq u1 u2 !cstrs; true) in let rec eq_constr' m n = @@ -598,16 +598,16 @@ let eq_constr_univs_infer univs m n = res, !cstrs let leq_constr_univs_infer univs m n = - if m == n then true, UniverseConstraints.empty + if m == n then true, Constraint.empty else - let cstrs = ref UniverseConstraints.empty in + let cstrs = ref Constraint.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 if Univ.check_eq univs u1 u2 then true - else (cstrs := Univ.UniverseConstraints.add (u1, Univ.UEq, u2) !cstrs; + else (cstrs := Univ.enforce_eq u1 u2 !cstrs; true) in let leq_sorts s1 s2 = @@ -616,7 +616,7 @@ let leq_constr_univs_infer univs m n = let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in if Univ.check_leq univs u1 u2 then true else - (cstrs := Univ.UniverseConstraints.add (u1, Univ.ULe, u2) !cstrs; + (cstrs := Univ.enforce_leq u1 u2 !cstrs; true) in let rec eq_constr' m n = @@ -628,53 +628,6 @@ let leq_constr_univs_infer univs m n = let res = compare_leq m n in res, !cstrs -let eq_constr_universes m n = - if m == n then true, UniverseConstraints.empty - else - let cstrs = ref UniverseConstraints.empty in - let eq_universes strict l l' = - cstrs := Univ.enforce_eq_instances_univs strict l l' !cstrs; true in - let eq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else - (cstrs := Univ.UniverseConstraints.add - (Sorts.univ_of_sort s1, Univ.UEq, Sorts.univ_of_sort s2) !cstrs; - true) - in - let rec eq_constr' m n = - m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n - in - let res = compare_head_gen eq_universes eq_sorts eq_constr' m n in - res, !cstrs - -let leq_constr_universes m n = - if m == n then true, UniverseConstraints.empty - else - let cstrs = ref UniverseConstraints.empty in - let eq_universes strict l l' = - cstrs := Univ.enforce_eq_instances_univs strict l l' !cstrs; true in - let eq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else (cstrs := Univ.UniverseConstraints.add - (Sorts.univ_of_sort s1,Univ.UEq,Sorts.univ_of_sort s2) !cstrs; - true) - in - let leq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else - (cstrs := Univ.UniverseConstraints.add - (Sorts.univ_of_sort s1,Univ.ULe,Sorts.univ_of_sort s2) !cstrs; - true) - in - let rec eq_constr' m n = - m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n - in - let rec compare_leq m n = - compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n - and leq_constr' m n = m == n || compare_leq m n in - let res = compare_leq m n in - res, !cstrs - let always_true _ _ = true let rec eq_constr_nounivs m n = diff --git a/kernel/constr.mli b/kernel/constr.mli index c57c4c59b..58f248b03 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -212,19 +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.universe_constrained +val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.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.universe_constrained - -(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, - application grouping and the universe equalities in [c]. *) -val eq_constr_universes : constr -> constr -> bool Univ.universe_constrained - -(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo - alpha, casts, application grouping and the universe inequalities in [c]. *) -val leq_constr_universes : constr -> constr -> bool Univ.universe_constrained +val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.constrained (** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and ignoring universe instances. *) @@ -281,6 +273,31 @@ val iter_with_binders : val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool +(** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare + the immediate subterms of [c1] of [c2] if needed, [u] to compare universe + instances (the first boolean tells if they belong to a constant), [s] to + compare sorts; Cast's, binders name and Cases annotations are not taken + into account *) + +val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> + (Sorts.t -> Sorts.t -> bool) -> + (constr -> constr -> bool) -> + constr -> constr -> bool + +(** [compare_head_gen_leq u s sle f fle c1 c2] compare [c1] and [c2] + using [f] to compare the immediate subterms of [c1] of [c2] for + conversion, [fle] for cumulativity, [u] to compare universe + instances (the first boolean tells if they belong to a constant), + [s] to compare sorts for equality and [sle] for subtyping; Cast's, + binders name and Cases annotations are not taken into account *) + +val compare_head_gen_leq : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> + (Sorts.t -> Sorts.t -> bool) -> + (Sorts.t -> Sorts.t -> bool) -> + (constr -> constr -> bool) -> + (constr -> constr -> bool) -> + constr -> constr -> bool + (** {6 Hashconsing} *) val hash : constr -> int diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 6a8f3ddd7..a6e107d3f 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -664,7 +664,7 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = 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 (Univ.to_constraints univs cstrs) + if b then 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 diff --git a/kernel/term.ml b/kernel/term.ml index b85c525d1..3b6b69a28 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -140,8 +140,6 @@ let mkCoFix = Constr.mkCoFix let eq_constr = Constr.equal let eq_constr_univs = Constr.eq_constr_univs let leq_constr_univs = Constr.leq_constr_univs -let eq_constr_universes = Constr.eq_constr_universes -let leq_constr_universes = Constr.leq_constr_universes let eq_constr_nounivs = Constr.eq_constr_nounivs let kind_of_term = Constr.kind diff --git a/kernel/term.mli b/kernel/term.mli index 2d3df6e1e..5ff5f9ba1 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -421,22 +421,14 @@ val mkCoFix : cofixpoint -> constr val eq_constr : constr -> constr -> bool (** Alias for [Constr.equal] *) -(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, - application grouping and the universe equalities in [c]. *) +(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, + application grouping and the universe constraints in [u]. *) val eq_constr_univs : constr Univ.check_function -(** [leq_constr_univs a b] [true, c] if [a] is convertible to [b] modulo - alpha, casts, application grouping and the universe inequalities in [c]. *) +(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo + alpha, casts, application grouping and the universe constraints in [u]. *) val leq_constr_univs : constr Univ.check_function -(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, - application grouping and the universe equalities in [c]. *) -val eq_constr_universes : constr -> constr -> bool Univ.universe_constrained - -(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo - alpha, casts, application grouping and the universe inequalities in [c]. *) -val leq_constr_universes : constr -> constr -> bool Univ.universe_constrained - (** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and ignoring universe instances. *) val eq_constr_nounivs : constr -> constr -> bool diff --git a/kernel/univ.ml b/kernel/univ.ml index bb034c56f..18064d246 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -712,13 +712,20 @@ end type universe = Universe.t -open Universe +(* The level of predicative Set *) +let type0m_univ = Universe.type0m +let type0_univ = Universe.type0 +let type1_univ = Universe.type1 +let is_type0m_univ = Universe.is_type0m +let is_type0_univ = Universe.is_type0 +let is_univ_variable l = Universe.level l != None +let is_small_univ = Universe.is_small +let pr_uni = Universe.pr -(* type universe_list = UList.t *) -(* let pr_universe_list = UList.pr *) +let sup = Universe.sup +let super = Universe.super -let pr_uni = Universe.pr -let is_small_univ = Universe.is_small +open Universe let universe_level = Universe.level @@ -760,20 +767,6 @@ let enter_equiv_arc u v g = let enter_arc ca g = UMap.add ca.univ (Canonical ca) g -let is_type0m_univ = Universe.is_type0m - -(* The level of predicative Set *) -let type0m_univ = Universe.type0m -let type0_univ = Universe.type0 -let type1_univ = Universe.type1 - -let sup = Universe.sup -let super = Universe.super - -let is_type0_univ = Universe.is_type0 - -let is_univ_variable l = Universe.level l != None - (* Every Level.t has a unique canonical arc representative *) (* repr : universes -> Level.t -> canonical_arc *) @@ -1075,12 +1068,6 @@ let check_eq_univs g l1 l2 = let check_eq g u v = Universe.equal u v || check_eq_univs g u v -let check_eq = - if Flags.profile then - let check_eq_key = Profile.declare_profile "check_eq" in - Profile.profile3 check_eq_key check_eq - else check_eq - let check_smaller_expr g (u,n) (v,m) = let diff = n - m in match diff with @@ -1101,12 +1088,6 @@ let check_leq g u v = Universe.is_type0m u || check_eq_univs g u v || real_check_leq g u v -let check_leq = - if Flags.profile then - let check_leq_key = Profile.declare_profile "check_leq" in - Profile.profile3 check_leq_key check_leq - else check_leq - (** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *) (** To speed up tests of Set </<= i *) @@ -1297,7 +1278,6 @@ let pr_constraint_type op = | Eq -> " = " in str op_str - module UConstraintOrd = struct type t = univ_constraint @@ -1356,60 +1336,6 @@ module Hconstraints = let hcons_constraint = Hashcons.simple_hcons Hconstraint.generate Level.hcons let hcons_constraints = Hashcons.simple_hcons Hconstraints.generate hcons_constraint -type universe_constraint_type = ULe | UEq | ULub - -type universe_constraint = universe * universe_constraint_type * universe -module UniverseConstraints = struct - module S = Set.Make( - struct - type t = universe_constraint - - let compare_type c c' = - match c, c' with - | ULe, ULe -> 0 - | ULe, _ -> -1 - | _, ULe -> 1 - | UEq, UEq -> 0 - | UEq, _ -> -1 - | ULub, ULub -> 0 - | ULub, _ -> 1 - - let compare (u,c,v) (u',c',v') = - let i = compare_type c c' in - if Int.equal i 0 then - let i' = Universe.compare u u' in - if Int.equal i' 0 then Universe.compare v v' - else - if c != ULe && Universe.compare u v' = 0 && Universe.compare v u' = 0 then 0 - else i' - else i - end) - - include S - - let add (l,d,r as cst) s = - if Universe.equal l r then s - else add cst s - - let tr_dir = function - | ULe -> Le - | UEq -> Eq - | ULub -> Eq - - let op_str = function ULe -> " <= " | UEq -> " = " | ULub -> " /\\ " - - let pr c = - fold (fun (u1,op,u2) pp_std -> - pp_std ++ Universe.pr u1 ++ str (op_str op) ++ - Universe.pr u2 ++ fnl ()) c (str "") - - let equal x y = - x == y || equal x y - -end - -type universe_constraints = UniverseConstraints.t -type 'a universe_constrained = 'a * universe_constraints (** A value with universe constraints. *) type 'a constrained = 'a * constraints @@ -1506,22 +1432,6 @@ struct let hash = HInstancestruct.hash let share a = (a, hash a) - - (* let len = Array.length a in *) - (* if Int.equal len 0 then (empty, 0) *) - (* else begin *) - (* let accu = ref 0 in *) - (* for i = 0 to len - 1 do *) - (* let l = Array.unsafe_get a i in *) - (* let l', h = Level.hcons l, Level.hash l in *) - (* accu := Hashset.Combine.combine !accu h; *) - (* if l' == l then () *) - (* else Array.unsafe_set a i l' *) - (* done; *) - (* (\* [h] must be positive. *\) *) - (* let h = !accu land 0x3FFFFFFF in *) - (* (a, h) *) - (* end *) let empty = hcons [||] @@ -1563,11 +1473,6 @@ struct (* Necessary as universe instances might come from different modules and unmarshalling doesn't preserve sharing *)) - (* if b then *) - (* (prerr_endline ("Not physically equal but equal:" ^(Pp.string_of_ppcmds (pr t)) *) - (* ^ " and " ^ (Pp.string_of_ppcmds (pr u))); b) *) - (* else b) *) - let check_eq g t1 t2 = t1 == t2 || (Int.equal (Array.length t1) (Array.length t2) && @@ -1677,29 +1582,6 @@ let pr_universe_level_subst = let constraints_of (_, cst) = cst -let remove_dangling_constraints dangling cst = - Constraint.fold (fun (l,d,r as cstr) cst' -> - if List.mem l dangling || List.mem r dangling then cst' - else - (** Unnecessary constraints Prop <= u *) - if Level.equal l Level.prop && d == Le then cst' - else Constraint.add cstr cst') cst Constraint.empty - -let check_context_subset (univs, cst) (univs', cst') = - let newunivs, dangling = List.partition (fun u -> LSet.mem u univs) (Instance.to_list univs') in - (* Some universe variables that don't appear in the term - are still mentionned in the constraints. This is the - case for "fake" universe variables that correspond to +1s. *) - (* if not (CList.is_empty dangling) then *) - (* todo ("A non-empty set of inferred universes do not appear in the term or type"); *) - (* (not (constraints_depend cst' dangling));*) - (* TODO: check implication *) - (** Remove local universes that do not appear in any constraint, they - are really entirely parametric. *) - (* let newunivs, dangling' = List.partition (fun u -> constraints_depend cst [u]) newunivs in *) - let cst' = remove_dangling_constraints dangling cst in - Instance.of_list newunivs, cst' - (** Substitutions. *) let make_universe_subst inst (ctx, csts) = @@ -1721,12 +1603,6 @@ let subst_univs_level_level subst l = try LMap.find l subst with Not_found -> l -let rec normalize_univs_level_level subst l = - try - let l' = LMap.find l subst in - normalize_univs_level_level subst l' - with Not_found -> l - let subst_univs_level_universe subst u = let f x = Universe.Expr.map (fun u -> subst_univs_level_level subst u) x in let u' = Universe.smartmap f u in @@ -1744,10 +1620,6 @@ let subst_univs_level_constraints subst csts = (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c)) csts Constraint.empty -(* let subst_univs_level_constraint_key = Profile.declare_profile "subst_univs_level_constraint";; *) -(* let subst_univs_level_constraint = *) -(* Profile.profile2 subst_univs_level_constraint_key subst_univs_level_constraint *) - (** With level to universe substitutions. *) type universe_subst_fn = universe_level -> universe @@ -1782,11 +1654,6 @@ let subst_univs_constraint fn (u,d,v) = if d != Lt && Universe.equal u' v' then None else Some (u',d,v') -let subst_univs_universe_constraint fn (u,d,v) = - let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in - if Universe.equal u' v' then None - else Some (u',d,v') - (** Constraint functions. *) type 'a constraint_function = 'a -> 'a -> constraints -> constraints @@ -1850,29 +1717,13 @@ let enforce_leq_level u v c = let enforce_eq_instances x y = let ax = Instance.to_array x and ay = Instance.to_array y in if Array.length ax != Array.length ay then - anomaly (Pp.str "Invalid argument: enforce_eq_instances called with instances of different lengths"); + anomaly (Pp.(++) (Pp.str "Invalid argument: enforce_eq_instances called with") + (Pp.str " instances of different lengths")); CArray.fold_right2 enforce_eq_level ax ay - -type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints - -let enforce_eq_instances_univs strict x y c = - let d = if strict then ULub else UEq in - let ax = Instance.to_array x and ay = Instance.to_array y in - if Array.length ax != Array.length ay then - anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with instances of different lengths"); - CArray.fold_right2 - (fun x y -> UniverseConstraints.add (Universe.make x, d, Universe.make y)) - ax ay c let merge_constraints c g = Constraint.fold enforce_constraint c g -let merge_constraints = - if Flags.profile then - let key = Profile.declare_profile "merge_constraints" in - Profile.profile2 key merge_constraints - else merge_constraints - let check_constraint g (l,d,r) = match d with | Eq -> check_equal g l r @@ -1882,12 +1733,6 @@ let check_constraint g (l,d,r) = let check_constraints c g = Constraint.for_all (check_constraint g) c -let check_constraints = - if Flags.profile then - let key = Profile.declare_profile "check_constraints" in - Profile.profile2 key check_constraints - else check_constraints - let enforce_univ_constraint (u,d,v) = match d with | Eq -> enforce_eq u v @@ -1899,41 +1744,10 @@ let subst_univs_constraints subst csts = (fun c -> Option.fold_right enforce_univ_constraint (subst_univs_constraint subst c)) csts Constraint.empty -(* let subst_univs_constraints_key = Profile.declare_profile "subst_univs_constraints";; *) -(* let subst_univs_constraints = *) -(* Profile.profile2 subst_univs_constraints_key subst_univs_constraints *) - -let subst_univs_universe_constraints subst csts = - UniverseConstraints.fold - (fun c -> Option.fold_right UniverseConstraints.add (subst_univs_universe_constraint subst c)) - csts UniverseConstraints.empty - -(* let subst_univs_universe_constraints_key = Profile.declare_profile "subst_univs_universe_constraints";; *) -(* let subst_univs_universe_constraints = *) -(* Profile.profile2 subst_univs_universe_constraints_key subst_univs_universe_constraints *) - (** Substitute instance inst for ctx in csts *) let instantiate_univ_context subst (_, csts) = subst_univs_level_constraints subst csts -let check_consistent_constraints (ctx,cstrs) cstrs' = - (* TODO *) () - -let to_constraints g s = - let tr (x,d,y) acc = - let add l d l' acc = Constraint.add (l,UniverseConstraints.tr_dir d,l') acc in - match Universe.level x, d, Universe.level y with - | Some l, (ULe | UEq | ULub), Some l' -> add l d l' acc - | _, ULe, Some l' -> enforce_leq x y acc - | _, ULub, _ -> acc - | _, d, _ -> - let f = if d == ULe then check_leq else check_eq in - if f g x y then acc else - raise (Invalid_argument - "to_constraints: non-trivial algebraic constraint between universes") - in UniverseConstraints.fold tr s Constraint.empty - - (* Normalization *) let lookup_level u g = @@ -2288,3 +2102,30 @@ let explain_universe_inconsistency (o,u,v,p) = let compare_levels = Level.compare let eq_levels = Level.equal let equal_universes = Universe.equal + + +(* + +let merge_constraints = + if Flags.profile then + let key = Profile.declare_profile "merge_constraints" in + Profile.profile2 key merge_constraints + else merge_constraints +let check_constraints = + if Flags.profile then + let key = Profile.declare_profile "check_constraints" in + Profile.profile2 key check_constraints + else check_constraints + +let check_eq = + if Flags.profile then + let check_eq_key = Profile.declare_profile "check_eq" in + Profile.profile3 check_eq_key check_eq + else check_eq + +let check_leq = + if Flags.profile then + let check_leq_key = Profile.declare_profile "check_leq" in + Profile.profile3 check_leq_key check_leq + else check_leq +*) diff --git a/kernel/univ.mli b/kernel/univ.mli index 74bd01610..3fc2c7dc2 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -182,6 +182,9 @@ val initial_universes : universes val is_initial_universes : universes -> bool +val sort_universes : universes -> universes + +(** Adds a universe to the graph, ensuring it is >= Prop. *) val add_universe : universe_level -> universes -> universes (** {6 Substitution} *) @@ -267,6 +270,8 @@ val eq_constraint : constraints -> constraints -> bool (** A value with universe constraints. *) type 'a constrained = 'a * constraints +(** Constrained *) +val constraints_of : 'a constrained -> constraints (** A list of universes with universe constraints, representiong local universe variables and constraints *) @@ -307,8 +312,7 @@ sig val add_constraints : t -> constraints -> t val add_universes : Instance.t -> t -> t - (** Arbitrary choice of linear order of the variables - and normalization of the constraints *) + (** Arbitrary choice of linear order of the variables *) val to_context : t -> universe_context val of_context : universe_context -> t @@ -326,77 +330,39 @@ type universe_context_set = ContextSet.t type 'a in_universe_context = 'a * universe_context type 'a in_universe_context_set = 'a * universe_context_set -(** {6 Constraints for type inference} - - When doing conversion of universes, not only do we have =/<= constraints but - also Lub constraints which correspond to unification of two levels that might - not be necessary if unfolding is performed. - *) - -type universe_constraint_type = ULe | UEq | ULub - -type universe_constraint = universe * universe_constraint_type * universe -module UniverseConstraints : sig - include Set.S with type elt = universe_constraint - - val pr : t -> Pp.std_ppcmds -end - -type universe_constraints = UniverseConstraints.t -type 'a universe_constrained = 'a * universe_constraints - - -(** Constrained *) -val constraints_of : 'a constrained -> constraints - - -(** [check_context_subset s s'] checks that [s] is implied by [s'] as a set of constraints, - and shrinks [s'] to the set of variables declared in [s]. -. *) -val check_context_subset : universe_context_set -> universe_context -> universe_context - -(** Make a universe level substitution: the list must match the context variables. *) -val make_universe_subst : Instance.t -> universe_context -> universe_level_subst - val empty_level_subst : universe_level_subst val is_empty_level_subst : universe_level_subst -> bool -(** Get the instantiated graph. *) -val instantiate_univ_context : universe_level_subst -> universe_context -> constraints - (** Substitution of universes. *) val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level val subst_univs_level_universe : universe_level_subst -> universe -> universe val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints -val normalize_univs_level_level : universe_level_subst -> universe_level -> universe_level +(** Make a universe level substitution: the instances must match. *) +val make_universe_subst : Instance.t -> universe_context -> universe_level_subst +(** Get the instantiated graph. *) +val instantiate_univ_context : universe_level_subst -> universe_context -> constraints +(** Level to universe substitutions. *) val empty_subst : universe_subst val is_empty_subst : universe_subst -> bool val make_subst : universe_subst -> universe_subst_fn -(* val subst_univs_level_fail : universe_subst_fn -> universe_level -> universe_level *) val subst_univs_level : universe_subst_fn -> universe_level -> universe val subst_univs_universe : universe_subst_fn -> universe -> universe val subst_univs_constraints : universe_subst_fn -> constraints -> constraints -val subst_univs_universe_constraints : universe_subst_fn -> universe_constraints -> universe_constraints -(** Raises universe inconsistency if not compatible. *) -val check_consistent_constraints : universe_context_set -> constraints -> unit +(** Enforcing constraints. *) type 'a constraint_function = 'a -> 'a -> constraints -> constraints -val enforce_leq : universe constraint_function val enforce_eq : universe constraint_function +val enforce_leq : universe constraint_function val enforce_eq_level : universe_level constraint_function val enforce_leq_level : universe_level constraint_function val enforce_eq_instances : universe_instance constraint_function -type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints - -val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_function - (** {6 ... } *) (** Merge of constraints in a universes graph. The function [merge_constraints] merges a set of constraints in a given @@ -422,16 +388,12 @@ exception UniverseInconsistency of univ_inconsistency val enforce_constraint : univ_constraint -> universes -> universes val merge_constraints : constraints -> universes -> universes -val sort_universes : universes -> universes val constraints_of_universes : universes -> constraints -val to_constraints : universes -> universe_constraints -> constraints - val check_constraint : universes -> univ_constraint -> bool val check_constraints : constraints -> universes -> bool - (** {6 Support for sort-polymorphism } *) val solve_constraints_system : universe option array -> universe array -> universe array -> @@ -455,7 +417,6 @@ val univ_depends : universe -> universe -> bool val pr_universes : universes -> Pp.std_ppcmds val pr_constraint_type : constraint_type -> Pp.std_ppcmds val pr_constraints : constraints -> Pp.std_ppcmds -(* val pr_universe_list : universe_list -> Pp.std_ppcmds *) val pr_universe_context : universe_context -> Pp.std_ppcmds val pr_universe_context_set : universe_context_set -> Pp.std_ppcmds val pr_universe_level_subst : universe_level_subst -> Pp.std_ppcmds diff --git a/library/universes.ml b/library/universes.ml index 765d34f98..11ab849c5 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -15,6 +15,198 @@ open Environ open Locus open Univ +type universe_constraint_type = ULe | UEq | ULub + +type universe_constraint = universe * universe_constraint_type * universe + +module Constraints = struct + module S = Set.Make( + struct + type t = universe_constraint + + let compare_type c c' = + match c, c' with + | ULe, ULe -> 0 + | ULe, _ -> -1 + | _, ULe -> 1 + | UEq, UEq -> 0 + | UEq, _ -> -1 + | ULub, ULub -> 0 + | ULub, _ -> 1 + + let compare (u,c,v) (u',c',v') = + let i = compare_type c c' in + if Int.equal i 0 then + let i' = Universe.compare u u' in + if Int.equal i' 0 then Universe.compare v v' + else + if c != ULe && Universe.compare u v' = 0 && Universe.compare v u' = 0 then 0 + else i' + else i + end) + + include S + + let add (l,d,r as cst) s = + if Universe.equal l r then s + else add cst s + + let tr_dir = function + | ULe -> Le + | UEq -> Eq + | ULub -> Eq + + let op_str = function ULe -> " <= " | UEq -> " = " | ULub -> " /\\ " + + let pr c = + fold (fun (u1,op,u2) pp_std -> + pp_std ++ Universe.pr u1 ++ str (op_str op) ++ + Universe.pr u2 ++ fnl ()) c (str "") + + let equal x y = + x == y || equal x y + +end + +type universe_constraints = Constraints.t +type 'a universe_constrained = 'a * universe_constraints + +type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints + +let enforce_eq_instances_univs strict x y c = + let d = if strict then ULub else UEq in + let ax = Instance.to_array x and ay = Instance.to_array y in + if Array.length ax != Array.length ay then + Errors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++ + Pp.str " instances of different lengths"); + CArray.fold_right2 + (fun x y -> Constraints.add (Universe.make x, d, Universe.make y)) + ax ay c + +let subst_univs_universe_constraint fn (u,d,v) = + let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in + if Universe.equal u' v' then None + else Some (u',d,v') + +let subst_univs_universe_constraints subst csts = + Constraints.fold + (fun c -> Option.fold_right Constraints.add (subst_univs_universe_constraint subst c)) + csts Constraints.empty + + +let to_constraints g s = + let tr (x,d,y) acc = + let add l d l' acc = Constraint.add (l,Constraints.tr_dir d,l') acc in + match Universe.level x, d, Universe.level y with + | Some l, (ULe | UEq | ULub), Some l' -> add l d l' acc + | _, ULe, Some l' -> enforce_leq x y acc + | _, ULub, _ -> acc + | _, d, _ -> + let f = if d == ULe then check_leq else check_eq in + if f g x y then acc else + raise (Invalid_argument + "to_constraints: non-trivial algebraic constraint between universes") + in Constraints.fold tr s Constraint.empty + +let eq_constr_univs_infer univs m n = + if m == n then true, Constraints.empty + else + let cstrs = ref Constraints.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 + if Univ.check_eq univs u1 u2 then true + else + (cstrs := Constraints.add (u1, UEq, u2) !cstrs; + true) + in + let rec eq_constr' m n = + m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n + in + let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in + res, !cstrs + +let leq_constr_univs_infer univs m n = + if m == n then true, Constraints.empty + else + let cstrs = ref Constraints.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 + if Univ.check_eq univs u1 u2 then true + else (cstrs := Constraints.add (u1, 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 + if Univ.check_leq univs u1 u2 then true + else + (cstrs := Constraints.add (u1, ULe, u2) !cstrs; + true) + in + let rec eq_constr' m n = + m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n + in + let rec compare_leq m n = + Constr.compare_head_gen_leq eq_universes eq_sorts leq_sorts + eq_constr' leq_constr' m n + and leq_constr' m n = m == n || compare_leq m n in + let res = compare_leq m n in + res, !cstrs + +let eq_constr_universes m n = + if m == n then true, Constraints.empty + else + let cstrs = ref Constraints.empty in + let eq_universes strict l l' = + cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in + let eq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + (cstrs := Constraints.add + (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs; + true) + in + let rec eq_constr' m n = + m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n + in + let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in + res, !cstrs + +let leq_constr_universes m n = + if m == n then true, Constraints.empty + else + let cstrs = ref Constraints.empty in + let eq_universes strict l l' = + cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in + let eq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else (cstrs := Constraints.add + (Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs; + true) + in + let leq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + (cstrs := Constraints.add + (Sorts.univ_of_sort s1,ULe,Sorts.univ_of_sort s2) !cstrs; + true) + in + let rec eq_constr' m n = + m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n + in + let rec compare_leq m n = + Constr.compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n + and leq_constr' m n = m == n || compare_leq m n in + let res = compare_leq m n in + res, !cstrs + (* Generator of levels *) let new_univ_level, set_remote_new_univ_level = RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1) diff --git a/library/universes.mli b/library/universes.mli index e5d3ded58..4cc92543b 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -16,12 +16,64 @@ open Locus open Univ (** Universes *) -val new_univ_level : Names.dir_path -> universe_level + +(** The global universe counter *) val set_remote_new_univ_level : universe_level RemoteCounter.installer + +(** Side-effecting functions creating new universe levels. *) + +val new_univ_level : Names.dir_path -> universe_level val new_univ : Names.dir_path -> universe val new_Type : Names.dir_path -> types val new_Type_sort : Names.dir_path -> sorts +val new_global_univ : unit -> universe in_universe_context_set +val new_sort_in_family : sorts_family -> sorts + +(** {6 Constraints for type inference} + + When doing conversion of universes, not only do we have =/<= constraints but + also Lub constraints which correspond to unification of two levels which might + not be necessary if unfolding is performed. +*) + +type universe_constraint_type = ULe | UEq | ULub + +type universe_constraint = universe * universe_constraint_type * universe +module Constraints : sig + include Set.S with type elt = universe_constraint + + val pr : t -> Pp.std_ppcmds +end + +type universe_constraints = Constraints.t +type 'a universe_constrained = 'a * universe_constraints +type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints + +val subst_univs_universe_constraints : universe_subst_fn -> + universe_constraints -> universe_constraints + +val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_function + +val to_constraints : universes -> universe_constraints -> constraints + +(** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts, + application grouping, the universe constraints in [u] and additional constraints [c]. *) +val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained + +(** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b] + modulo alpha, casts, application grouping, the universe constraints + in [u] and additional constraints [c]. *) +val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained + +(** [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 + +(** [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 + (** Build a fresh instance for a given context, its associated substitution and the instantiated constraints. *) @@ -31,9 +83,6 @@ val fresh_instance_from_context : universe_context -> val fresh_instance_from : universe_context -> universe_instance option -> (universe_instance * universe_level_subst) in_universe_context_set -val new_global_univ : unit -> universe in_universe_context_set -val new_sort_in_family : sorts_family -> sorts - val fresh_sort_in_family : env -> sorts_family -> sorts in_universe_context_set val fresh_constant_instance : env -> constant -> @@ -49,6 +98,11 @@ val fresh_global_instance : ?names:Univ.Instance.t -> env -> Globnames.global_re val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> constr in_universe_context_set +(** Get fresh variables for the universe context. + Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) +val fresh_universe_context_set_instance : universe_context_set -> + universe_level_subst * universe_context_set + (** Raises [Not_found] if not a global reference. *) val global_of_constr : constr -> Globnames.global_reference puniverses @@ -78,39 +132,6 @@ val make_opt_subst : universe_opt_subst -> universe_subst_fn val subst_opt_univs_constr : universe_opt_subst -> constr -> constr -val choose_canonical : universe_set -> (Level.t -> bool) (* flexibles *) -> universe_set -> universe_set -> - universe_level * (universe_set * universe_set * universe_set) - -val instantiate_with_lbound : - Univ.LMap.key -> - Univ.universe -> - bool -> - bool -> - Univ.LSet.t * Univ.universe option Univ.LMap.t * - Univ.LSet.t * - (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints -> - (Univ.LSet.t * Univ.universe option Univ.LMap.t * - Univ.LSet.t * - (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints) * - (bool * bool * Univ.universe) - -val compute_lbound : (constraint_type * Univ.universe) list -> universe option - -type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t - -val pr_constraints_map : constraints_map -> Pp.std_ppcmds - -val minimize_univ_variables : - Univ.LSet.t -> - Univ.universe option Univ.LMap.t -> - Univ.LSet.t -> - constraints_map -> constraints_map -> - Univ.constraints -> - Univ.LSet.t * Univ.universe option Univ.LMap.t * - Univ.LSet.t * - (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints - - val normalize_context_set : universe_context_set -> universe_opt_subst (* The defined and undefined variables *) -> universe_set (* univ variables that can be substituted by algebraics *) -> @@ -141,7 +162,6 @@ val normalize_universe_subst : universe_subst ref -> the constraints should be properly added to an evd. See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for the proper way to get a fresh copy of a global reference. *) - val constr_of_global : Globnames.global_reference -> constr (** ** DEPRECATED ** synonym of [constr_of_global] *) @@ -171,13 +191,6 @@ val nf_evars_and_universes_local : (existential -> constr option) -> universe_le val nf_evars_and_universes_opt_subst : (existential -> constr option) -> universe_opt_subst -> constr -> constr -(** Get fresh variables for the universe context. - Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) -val fresh_universe_context_set_instance : universe_context_set -> - universe_level_subst * universe_context_set - -val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds - (** Shrink a universe context to a restricted set of variables *) val universes_of_constr : constr -> universe_set @@ -189,3 +202,42 @@ val simplify_universe_context : universe_context_set -> val refresh_constraints : universes -> universe_context_set -> universe_context_set * universes val remove_trivial_constraints : universe_context_set -> universe_context_set + +(** Pretty-printing *) + +val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds + +(* For tracing *) + +type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t + +val pr_constraints_map : constraints_map -> Pp.std_ppcmds + +val choose_canonical : universe_set -> (Level.t -> bool) (* flexibles *) -> universe_set -> universe_set -> + universe_level * (universe_set * universe_set * universe_set) + +val compute_lbound : (constraint_type * Univ.universe) list -> universe option + +val instantiate_with_lbound : + Univ.LMap.key -> + Univ.universe -> + bool -> + bool -> + Univ.LSet.t * Univ.universe option Univ.LMap.t * + Univ.LSet.t * + (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints -> + (Univ.LSet.t * Univ.universe option Univ.LMap.t * + Univ.LSet.t * + (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints) * + (bool * bool * Univ.universe) + +val minimize_univ_variables : + Univ.LSet.t -> + Univ.universe option Univ.LMap.t -> + Univ.LSet.t -> + constraints_map -> constraints_map -> + Univ.constraints -> + Univ.LSet.t * Univ.universe option Univ.LMap.t * + Univ.LSet.t * + (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints + diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 86fa5518c..be343b987 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -153,7 +153,7 @@ GEXTEND Gram [ [ "Set" -> GSet | "Prop" -> GProp | "Type" -> GType None - | "Type"; "{"; id = ident; "}" -> GType (Some (Id.to_string id)) + | "Type"; "@{"; id = ident; "}" -> GType (Some (Id.to_string id)) ] ] ; lconstr: diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 7df4dabcd..8c4ca1d82 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -369,10 +369,10 @@ 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 = eq_constr_universes term term' in + let b,univs = Universes.eq_constr_universes term term' in if b then ise_and evd [(fun i -> - let cstrs = Univ.to_constraints (Evd.universes i) univs in + let cstrs = Universes.to_constraints (Evd.universes i) univs in try let i = Evd.add_constraints i cstrs in Success i with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); @@ -485,7 +485,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 b,univs = eq_constr_universes term1 term2 in + let b,univs = Universes.eq_constr_universes term1 term2 in if b then ise_and i [(fun i -> try Success (Evd.add_universe_constraints i univs) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index e125a1c6e..adcc7bf38 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -393,7 +393,7 @@ let process_universe_constraints univs vars alg templ cstrs = | None -> Inl x | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l alg) in - if d == Univ.ULe then + if d == Universes.ULe then if Univ.check_leq univs l r then (** Keep Prop/Set <= var around if var might be instantiated by prop or set later. *) @@ -415,19 +415,19 @@ let process_universe_constraints univs vars alg templ cstrs = 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 + unify_universes fo l Universes.UEq r local else Univ.enforce_leq l r local - else if d == Univ.ULub then + else if d == Universes.ULub then match varinfo l, varinfo r with | (Inr (l, true, _), Inr (r, _, _)) | (Inr (r, _, _), Inr (l, true, _)) -> instantiate_variable l (Univ.Universe.make r) vars; Univ.enforce_eq_level l r local | Inr (_, _, _), Inr (_, _, _) -> - unify_universes true l Univ.UEq r local + unify_universes true l Universes.UEq r local | _, _ -> assert false - else (* d = Univ.UEq *) + else (* d = Universes.UEq *) match varinfo l, varinfo r with | Inr (l', lloc, _), Inr (r', rloc, _) -> let () = @@ -450,7 +450,7 @@ let process_universe_constraints univs vars alg templ cstrs = 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) + Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local) cstrs Univ.Constraint.empty in !vars, local @@ -460,10 +460,10 @@ let add_constraints_context ctx cstrs = let cstrs' = Univ.Constraint.fold (fun (l,d,r) acc -> let l = Univ.Universe.make l and r = Univ.Universe.make r in let cstr' = - if d == Univ.Lt then (Univ.Universe.super l, Univ.ULe, r) - else (l, (if d == Univ.Le then Univ.ULe else Univ.UEq), r) - in Univ.UniverseConstraints.add cstr' acc) - cstrs Univ.UniverseConstraints.empty + if d == Univ.Lt then (Univ.Universe.super l, Universes.ULe, r) + else (l, (if d == Univ.Le then Universes.ULe else Universes.UEq), r) + in Universes.Constraints.add cstr' acc) + cstrs Universes.Constraints.empty in let vars, local' = process_universe_constraints ctx.uctx_universes @@ -1135,7 +1135,7 @@ let set_eq_sort d s1 s2 = match is_eq_sort s1 s2 with | None -> d | Some (u1, u2) -> add_universe_constraints d - (Univ.UniverseConstraints.singleton (u1,Univ.UEq,u2)) + (Universes.Constraints.singleton (u1,Universes.UEq,u2)) let has_lub evd u1 u2 = (* let normalize = Universes.normalize_universe_opt_subst (ref univs.uctx_univ_variables) in *) @@ -1143,7 +1143,7 @@ let has_lub evd u1 u2 = (* let u1 = normalize u1 and u2 = normalize u2 in *) if Univ.Universe.equal u1 u2 then evd else add_universe_constraints evd - (Univ.UniverseConstraints.singleton (u1,Univ.ULub,u2)) + (Universes.Constraints.singleton (u1,Universes.ULub,u2)) let set_eq_level d u1 u2 = add_constraints d (Univ.enforce_eq_level u1 u2 Univ.Constraint.empty) @@ -1153,7 +1153,7 @@ let set_leq_level d u1 u2 = let set_eq_instances ?(flex=false) d u1 u2 = add_universe_constraints d - (Univ.enforce_eq_instances_univs flex u1 u2 Univ.UniverseConstraints.empty) + (Universes.enforce_eq_instances_univs flex u1 u2 Universes.Constraints.empty) let set_leq_sort evd s1 s2 = let s1 = normalize_sort evd s1 @@ -1167,7 +1167,7 @@ let set_leq_sort evd s1 s2 = (* 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)) + add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2)) let check_eq evd s s' = Univ.check_eq evd.universes.uctx_universes s s' diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 8bdfccb6b..3b58910e1 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -265,7 +265,7 @@ val set_eq_sort : evar_map -> sorts -> sorts -> evar_map exception UniversesDiffer -val add_universe_constraints : evar_map -> Univ.universe_constraints -> evar_map +val add_universe_constraints : evar_map -> Universes.universe_constraints -> evar_map (** Add the given universe unification constraints to the evar map. @raises UniversesDiffer in case a first-order unification fails. @raises UniverseInconsistency diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index f75da1383..74f14aa14 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -630,8 +630,8 @@ let magicaly_constant_of_fixbody env bd = function match constant_opt_value env (cst,u) with | None -> bd | Some (t,cstrs) -> - let b, csts = eq_constr_universes t bd in - let subst = UniverseConstraints.fold (fun (l,d,r) acc -> + 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 @@ -1170,9 +1170,9 @@ let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y let b, sigma = let b, cstrs = if pb == Reduction.CUMUL then - Constr.leq_constr_univs_infer (Evd.universes sigma) x y + Universes.leq_constr_univs_infer (Evd.universes sigma) x y else - Constr.eq_constr_univs_infer (Evd.universes sigma) x y + Universes.eq_constr_univs_infer (Evd.universes sigma) x y in if b then try true, Evd.add_universe_constraints sigma cstrs diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 8b2532a5f..93e1060ab 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1058,7 +1058,7 @@ let compute = cbv_betadeltaiota let make_eq_univs_test evd c = { match_fun = (fun evd c' -> - let b, cst = eq_constr_universes c c' in + let b, cst = Universes.eq_constr_universes c c' in if b then try Evd.add_universe_constraints evd cst with Evd.UniversesDiffer -> raise NotUnifiable diff --git a/pretyping/termops.ml b/pretyping/termops.ml index d728f1bff..363292ec0 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -559,7 +559,7 @@ let collect_vars c = [m] is appropriately lifted through abstractions of [t] *) let dependent_main noevar univs m t = - let eqc x y = if univs then fst (eq_constr_universes x y) else eq_constr_nounivs x y in + let eqc x y = if univs then fst (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/pretyping/unification.ml b/pretyping/unification.ml index 4936ba426..574088f42 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -391,16 +391,16 @@ let is_rigid_head flags t = | _ -> false let force_eqs c = - Univ.UniverseConstraints.fold + Universes.Constraints.fold (fun ((l,d,r) as c) acc -> - let c' = if d == Univ.ULub then (l,Univ.UEq,r) else c in - Univ.UniverseConstraints.add c' acc) - c Univ.UniverseConstraints.empty + 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 b, cstrs = - if pb == Reduction.CONV then eq_constr_universes t u - else leq_constr_universes t u + 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 diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 22c89af8a..3369e658b 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -108,12 +108,12 @@ let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c) let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" -let pr_in_braces pr x = str "{" ++ pr x ++ str "}" +let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" let pr_glob_sort = function | GProp -> str "Prop" | GSet -> str "Set" - | GType u -> hov 0 (str "Type" ++ pr_opt_no_spc (pr_in_braces str) u) + | GType u -> hov 0 (str "Type" ++ pr_opt_no_spc (pr_univ_annot str) u) let pr_id = pr_id let pr_name = pr_name @@ -129,8 +129,7 @@ let pr_glob_sort_instance = function | None -> str "Type") let pr_universe_instance l = - pr_opt_no_spc (fun i -> - str"@" ++ pr_in_braces (prlist_with_sep spc pr_glob_sort_instance) i) l + pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l let pr_cref ref us = pr_reference ref ++ pr_universe_instance us diff --git a/proofs/refiner.ml b/proofs/refiner.ml index f0e8bf3ec..b47e16a3c 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -337,9 +337,6 @@ let tclPUSHEVARUNIVCONTEXT ctx gl = let tclPUSHCONSTRAINTS cst gl = tclEVARS (Evd.add_constraints (project gl) cst) gl -let tclPUSHUNIVERSECONSTRAINTS cst gl = - tclEVARS (Evd.add_universe_constraints (project gl) cst) gl - (* Check that holes in arguments have been resolved *) let check_evars env sigma extsigma origsigma = diff --git a/proofs/refiner.mli b/proofs/refiner.mli index a74d8a46d..171b008d1 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -39,7 +39,6 @@ val tclPUSHCONTEXT : Evd.rigid -> Univ.universe_context_set -> tactic -> tactic val tclPUSHEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic val tclPUSHCONSTRAINTS : Univ.constraints -> tactic -val tclPUSHUNIVERSECONSTRAINTS : Univ.UniverseConstraints.t -> tactic (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies [tac2] to every resulting subgoals *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 65326774f..f043e8f16 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1969,7 +1969,7 @@ let interp ?(verbosely=true) ?proof (loc,c) = Flags.program_mode := orig_program_mode end with - | reraise when (match reraise with Timeout _ -> true | e -> Errors.noncritical e) -> + | reraise when (match reraise with Timeout -> true | e -> Errors.noncritical e) -> let e = Errors.push reraise in let e = locate_if_not_already loc e in let () = restore_timeout () in |