diff options
Diffstat (limited to 'kernel')
-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 |
7 files changed, 93 insertions, 331 deletions
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 |