From 748a33cee41900d285897b24b4d8e29dd9eb2a3d Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 28 Apr 2018 21:36:57 +0200 Subject: Split off Universes functions for minimization. This finishes the splitting of Universes. --- engine/engine.mllib | 1 + engine/uState.ml | 4 +- engine/univMinim.ml | 383 +++++++++++++++++++++++++++++++++++++++++++++++++++ engine/univMinim.mli | 32 +++++ engine/universes.ml | 379 +------------------------------------------------- engine/universes.mli | 44 ++---- 6 files changed, 438 insertions(+), 405 deletions(-) create mode 100644 engine/univMinim.ml create mode 100644 engine/univMinim.mli (limited to 'engine') diff --git a/engine/engine.mllib b/engine/engine.mllib index befd49dc9..37e83b623 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -2,6 +2,7 @@ UnivNames UnivGen UnivSubst UnivProblem +UnivMinim Universes Univops UState diff --git a/engine/uState.ml b/engine/uState.ml index dbf5d48aa..844eb390b 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -20,7 +20,7 @@ type uinfo = { uloc : Loc.t option; } -module UPairSet = Universes.UPairSet +module UPairSet = UnivMinim.UPairSet (* 2nd part used to check consistency on the fly. *) type t = @@ -630,7 +630,7 @@ let refresh_undefined_univ_variables uctx = uctx', subst let minimize uctx = - let open Universes in + let open UnivMinim in let ((vars',algs'), us') = normalize_context_set uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic uctx.uctx_weak_constraints diff --git a/engine/univMinim.ml b/engine/univMinim.ml new file mode 100644 index 000000000..f10e6d2ec --- /dev/null +++ b/engine/univMinim.ml @@ -0,0 +1,383 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + LMap.add u [t] map + +(** Precondition: flexible <= ctx *) +let choose_canonical ctx flexible algs s = + let global = LSet.diff s ctx in + let flexible, rigid = LSet.partition flexible (LSet.inter s ctx) in + (** If there is a global universe in the set, choose it *) + if not (LSet.is_empty global) then + let canon = LSet.choose global in + canon, (LSet.remove canon global, rigid, flexible) + else (** No global in the equivalence class, choose a rigid one *) + if not (LSet.is_empty rigid) then + let canon = LSet.choose rigid in + canon, (global, LSet.remove canon rigid, flexible) + else (** There are only flexible universes in the equivalence + class, choose a non-algebraic. *) + let algs, nonalgs = LSet.partition (fun x -> LSet.mem x algs) flexible in + if not (LSet.is_empty nonalgs) then + let canon = LSet.choose nonalgs in + canon, (global, rigid, LSet.remove canon flexible) + else + let canon = LSet.choose algs in + canon, (global, rigid, LSet.remove canon flexible) + +(* Eq < Le < Lt *) +let compare_constraint_type d d' = + match d, d' with + | Eq, Eq -> 0 + | Eq, _ -> -1 + | _, Eq -> 1 + | Le, Le -> 0 + | Le, _ -> -1 + | _, Le -> 1 + | Lt, Lt -> 0 + +type lowermap = constraint_type LMap.t + +let lower_union = + let merge k a b = + match a, b with + | Some _, None -> a + | None, Some _ -> b + | None, None -> None + | Some l, Some r -> + if compare_constraint_type l r >= 0 then a + else b + in LMap.merge merge + +let lower_add l c m = + try let c' = LMap.find l m in + if compare_constraint_type c c' > 0 then + LMap.add l c m + else m + with Not_found -> LMap.add l c m + +let lower_of_list l = + List.fold_left (fun acc (d,l) -> LMap.add l d acc) LMap.empty l + +type lbound = { enforce : bool; alg : bool; lbound: Universe.t; lower : lowermap } + +exception Found of Level.t * lowermap +let find_inst insts v = + try LMap.iter (fun k {enforce;alg;lbound=v';lower} -> + if not alg && enforce && Universe.equal v' v then raise (Found (k, lower))) + insts; raise Not_found + with Found (f,l) -> (f,l) + +let compute_lbound left = + (** The universe variable was not fixed yet. + Compute its level using its lower bound. *) + let sup l lbound = + match lbound with + | None -> Some l + | Some l' -> Some (Universe.sup l l') + in + List.fold_left (fun lbound (d, l) -> + if d == Le (* l <= ?u *) then sup l lbound + else (* l < ?u *) + (assert (d == Lt); + if not (Universe.level l == None) then + sup (Universe.super l) lbound + else None)) + None left + +let instantiate_with_lbound u lbound lower ~alg ~enforce (ctx, us, algs, insts, cstrs) = + if enforce then + let inst = Universe.make u in + let cstrs' = enforce_leq lbound inst cstrs in + (ctx, us, LSet.remove u algs, + LMap.add u {enforce;alg;lbound;lower} insts, cstrs'), + {enforce; alg; lbound=inst; lower} + else (* Actually instantiate *) + (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs, + LMap.add u {enforce;alg;lbound;lower} insts, cstrs), + {enforce; alg; lbound; lower} + +type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t + +let _pr_constraints_map (cmap:constraints_map) = + let open Pp in + LMap.fold (fun l cstrs acc -> + Level.pr l ++ str " => " ++ + prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ + fnl () ++ acc) + cmap (mt ()) + +let remove_alg l (ctx, us, algs, insts, cstrs) = + (ctx, us, LSet.remove l algs, insts, cstrs) + +let not_lower lower (d,l) = + (* We're checking if (d,l) is already implied by the lower + constraints on some level u. If it represents l < u (d is Lt + or d is Le and i > 0, the i < 0 case is impossible due to + invariants of Univ), and the lower constraints only have l <= + u then it is not implied. *) + Univ.Universe.exists + (fun (l,i) -> + let d = + if i == 0 then d + else match d with + | Le -> Lt + | d -> d + in + try let d' = LMap.find l lower in + (* If d is stronger than the already implied lower + * constraints we must keep it. *) + compare_constraint_type d d' > 0 + with Not_found -> + (** No constraint existing on l *) true) l + +exception UpperBoundedAlg +(** [enforce_uppers upper lbound cstrs] interprets [upper] as upper + constraints to [lbound], adding them to [cstrs]. + + @raise UpperBoundedAlg if any [upper] constraints are strict and + [lbound] algebraic. *) +let enforce_uppers upper lbound cstrs = + List.fold_left (fun cstrs (d, r) -> + if d == Univ.Le then + enforce_leq lbound (Universe.make r) cstrs + else + match Universe.level lbound with + | Some lev -> Constraint.add (lev, d, r) cstrs + | None -> raise UpperBoundedAlg) + cstrs upper + +let minimize_univ_variables ctx us algs left right cstrs = + let left, lbounds = + Univ.LMap.fold (fun r lower (left, lbounds as acc) -> + if Univ.LMap.mem r us || not (Univ.LSet.mem r ctx) then acc + else (* Fixed universe, just compute its glb for sharing *) + let lbounds = + match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with + | None -> lbounds + | Some lbound -> LMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower} + lbounds + in (Univ.LMap.remove r left, lbounds)) + left (left, Univ.LMap.empty) + in + let rec instance (ctx, us, algs, insts, cstrs as acc) u = + let acc, left, lower = + match LMap.find u left with + | exception Not_found -> acc, [], LMap.empty + | l -> + let acc, left, newlow, lower = + List.fold_left + (fun (acc, left, newlow, lower') (d, l) -> + let acc', {enforce=enf;alg;lbound=l';lower} = aux acc l in + let l' = + if enf then Universe.make l + else l' + in acc', (d, l') :: left, + lower_add l d newlow, lower_union lower lower') + (acc, [], LMap.empty, LMap.empty) l + in + let left = CList.uniquize (List.filter (not_lower lower) left) in + (acc, left, LMap.union newlow lower) + in + let instantiate_lbound lbound = + let alg = LSet.mem u algs in + if alg then + (* u is algebraic: we instantiate it with its lower bound, if any, + or enforce the constraints if it is bounded from the top. *) + let lower = LSet.fold LMap.remove (Universe.levels lbound) lower in + instantiate_with_lbound u lbound lower ~alg:true ~enforce:false acc + else (* u is non algebraic *) + match Universe.level lbound with + | Some l -> (* The lowerbound is directly a level *) + (* u is not algebraic but has no upper bounds, + we instantiate it with its lower bound if it is a + different level, otherwise we keep it. *) + let lower = LMap.remove l lower in + if not (Level.equal l u) then + (* Should check that u does not + have upper constraints that are not already in right *) + let acc = remove_alg l acc in + instantiate_with_lbound u lbound lower ~alg:false ~enforce:false acc + else acc, {enforce=true; alg=false; lbound; lower} + | None -> + begin match find_inst insts lbound with + | can, lower -> + (* Another universe represents the same lower bound, + we can share them with no harm. *) + let lower = LMap.remove can lower in + instantiate_with_lbound u (Universe.make can) lower ~alg:false ~enforce:false acc + | exception Not_found -> + (* We set u as the canonical universe representing lbound *) + instantiate_with_lbound u lbound lower ~alg:false ~enforce:true acc + end + in + let enforce_uppers ((ctx,us,algs,insts,cstrs), b as acc) = + match LMap.find u right with + | exception Not_found -> acc + | upper -> + let upper = List.filter (fun (d, r) -> not (LMap.mem r us)) upper in + let cstrs = enforce_uppers upper b.lbound cstrs in + (ctx, us, algs, insts, cstrs), b + in + if not (LSet.mem u ctx) + then enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower}) + else + let lbound = compute_lbound left in + match lbound with + | None -> (* Nothing to do *) + enforce_uppers (acc, {enforce=true;alg=false;lbound=Universe.make u; lower}) + | Some lbound -> + try enforce_uppers (instantiate_lbound lbound) + with UpperBoundedAlg -> + enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower}) + and aux (ctx, us, algs, seen, cstrs as acc) u = + try acc, LMap.find u seen + with Not_found -> instance acc u + in + LMap.fold (fun u v (ctx, us, algs, seen, cstrs as acc) -> + if v == None then fst (aux acc u) + else LSet.remove u ctx, us, LSet.remove u algs, seen, cstrs) + us (ctx, us, algs, lbounds, cstrs) + +module UPairs = OrderedType.UnorderedPair(Univ.Level) +module UPairSet = Set.Make (UPairs) + +let normalize_context_set g ctx us algs weak = + let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in + (** Keep the Prop/Set <= i constraints separate for minimization *) + let smallles, csts = + Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts + in + let smallles = if is_set_minimization () + then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles + else Constraint.empty + in + let csts, partition = + (* We first put constraints in a normal-form: all self-loops are collapsed + to equalities. *) + let g = LSet.fold (fun v g -> UGraph.add_universe v false g) + ctx UGraph.initial_universes + in + let add_soft u g = + if not (Level.is_small u || LSet.mem u ctx) + then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g + else g + in + let g = Constraint.fold + (fun (l, d, r) g -> add_soft r (add_soft l g)) + csts g + in + let g = UGraph.merge_constraints csts g in + UGraph.constraints_of_universes g + in + (* We ignore the trivial Prop/Set <= i constraints. *) + let noneqs = + Constraint.filter + (fun (l,d,r) -> not ((d == Le && Level.is_small l) || + (Level.is_prop l && d == Lt && Level.is_set r))) + csts + in + let noneqs = Constraint.union noneqs smallles in + let flex x = LMap.mem x us in + let ctx, us, eqs = List.fold_left (fun (ctx, us, cstrs) s -> + let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in + (* Add equalities for globals which can't be merged anymore. *) + let cstrs = LSet.fold (fun g cst -> + Constraint.add (canon, Eq, g) cst) global + cstrs + in + (* Also add equalities for rigid variables *) + let cstrs = LSet.fold (fun g cst -> + Constraint.add (canon, Eq, g) cst) rigid + cstrs + in + let canonu = Some (Universe.make canon) in + let us = LSet.fold (fun f -> LMap.add f canonu) flexible us in + (LSet.diff ctx flexible, us, cstrs)) + (ctx, us, Constraint.empty) partition + in + (* Process weak constraints: when one side is flexible and the 2 + universes are unrelated unify them. *) + let ctx, us, g = UPairSet.fold (fun (u,v) (ctx, us, g as acc) -> + let norm = level_subst_of (normalize_univ_variable_opt_subst us) in + let u = norm u and v = norm v in + let set_to a b = + (LSet.remove a ctx, + LMap.add a (Some (Universe.make b)) us, + UGraph.enforce_constraint (a,Eq,b) g) + in + if UGraph.check_constraint g (u,Le,v) || UGraph.check_constraint g (v,Le,u) + then acc + else + if LMap.mem u us + then set_to u v + else if LMap.mem v us + then set_to v u + else acc) + weak (ctx, us, g) in + (* Noneqs is now in canonical form w.r.t. equality constraints, + and contains only inequality constraints. *) + let noneqs = + let norm = level_subst_of (normalize_univ_variable_opt_subst us) in + Constraint.fold (fun (u,d,v) noneqs -> + let u = norm u and v = norm v in + if d != Lt && Level.equal u v then noneqs + else Constraint.add (u,d,v) noneqs) + noneqs Constraint.empty + in + (* Compute the left and right set of flexible variables, constraints + mentionning other variables remain in noneqs. *) + let noneqs, ucstrsl, ucstrsr = + Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) -> + let lus = LMap.mem l us and rus = LMap.mem r us in + let ucstrsl' = + if lus then add_list_map l (d, r) ucstrsl + else ucstrsl + and ucstrsr' = + add_list_map r (d, l) ucstrsr + in + let noneqs = + if lus || rus then noneq + else Constraint.add cstr noneq + in (noneqs, ucstrsl', ucstrsr')) + noneqs (Constraint.empty, LMap.empty, LMap.empty) + in + (* Now we construct the instantiation of each variable. *) + let ctx', us, algs, inst, noneqs = + minimize_univ_variables ctx us algs ucstrsr ucstrsl noneqs + in + let us = normalize_opt_subst us in + (us, algs), (ctx', Constraint.union noneqs eqs) + +(* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *) +(* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *) diff --git a/engine/univMinim.mli b/engine/univMinim.mli new file mode 100644 index 000000000..9f80b7acb --- /dev/null +++ b/engine/univMinim.mli @@ -0,0 +1,32 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* ContextSet.t -> + universe_opt_subst (* The defined and undefined variables *) -> + LSet.t (* univ variables that can be substituted by algebraics *) -> + UPairSet.t (* weak equality constraints *) -> + (universe_opt_subst * LSet.t) in_universe_context_set diff --git a/engine/universes.ml b/engine/universes.ml index e3b661770..70601987c 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -8,381 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Util open Univ -open UnivSubst - -(* To disallow minimization to Set *) - -let set_minimization = ref true -let is_set_minimization () = !set_minimization - -let _ = - Goptions.(declare_bool_option - { optdepr = false; - optname = "minimization to Set"; - optkey = ["Universe";"Minimization";"ToSet"]; - optread = is_set_minimization; - optwrite = (:=) set_minimization }) - - -(** Simplification *) - -let add_list_map u t map = - try - let l = LMap.find u map in - LMap.set u (t :: l) map - with Not_found -> - LMap.add u [t] map - -(** Precondition: flexible <= ctx *) -let choose_canonical ctx flexible algs s = - let global = LSet.diff s ctx in - let flexible, rigid = LSet.partition flexible (LSet.inter s ctx) in - (** If there is a global universe in the set, choose it *) - if not (LSet.is_empty global) then - let canon = LSet.choose global in - canon, (LSet.remove canon global, rigid, flexible) - else (** No global in the equivalence class, choose a rigid one *) - if not (LSet.is_empty rigid) then - let canon = LSet.choose rigid in - canon, (global, LSet.remove canon rigid, flexible) - else (** There are only flexible universes in the equivalence - class, choose a non-algebraic. *) - let algs, nonalgs = LSet.partition (fun x -> LSet.mem x algs) flexible in - if not (LSet.is_empty nonalgs) then - let canon = LSet.choose nonalgs in - canon, (global, rigid, LSet.remove canon flexible) - else - let canon = LSet.choose algs in - canon, (global, rigid, LSet.remove canon flexible) - -(* Eq < Le < Lt *) -let compare_constraint_type d d' = - match d, d' with - | Eq, Eq -> 0 - | Eq, _ -> -1 - | _, Eq -> 1 - | Le, Le -> 0 - | Le, _ -> -1 - | _, Le -> 1 - | Lt, Lt -> 0 - -type lowermap = constraint_type LMap.t - -let lower_union = - let merge k a b = - match a, b with - | Some _, None -> a - | None, Some _ -> b - | None, None -> None - | Some l, Some r -> - if compare_constraint_type l r >= 0 then a - else b - in LMap.merge merge - -let lower_add l c m = - try let c' = LMap.find l m in - if compare_constraint_type c c' > 0 then - LMap.add l c m - else m - with Not_found -> LMap.add l c m - -let lower_of_list l = - List.fold_left (fun acc (d,l) -> LMap.add l d acc) LMap.empty l - -type lbound = { enforce : bool; alg : bool; lbound: Universe.t; lower : lowermap } - -exception Found of Level.t * lowermap -let find_inst insts v = - try LMap.iter (fun k {enforce;alg;lbound=v';lower} -> - if not alg && enforce && Universe.equal v' v then raise (Found (k, lower))) - insts; raise Not_found - with Found (f,l) -> (f,l) - -let compute_lbound left = - (** The universe variable was not fixed yet. - Compute its level using its lower bound. *) - let sup l lbound = - match lbound with - | None -> Some l - | Some l' -> Some (Universe.sup l l') - in - List.fold_left (fun lbound (d, l) -> - if d == Le (* l <= ?u *) then sup l lbound - else (* l < ?u *) - (assert (d == Lt); - if not (Universe.level l == None) then - sup (Universe.super l) lbound - else None)) - None left - -let instantiate_with_lbound u lbound lower ~alg ~enforce (ctx, us, algs, insts, cstrs) = - if enforce then - let inst = Universe.make u in - let cstrs' = enforce_leq lbound inst cstrs in - (ctx, us, LSet.remove u algs, - LMap.add u {enforce;alg;lbound;lower} insts, cstrs'), - {enforce; alg; lbound=inst; lower} - else (* Actually instantiate *) - (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs, - LMap.add u {enforce;alg;lbound;lower} insts, cstrs), - {enforce; alg; lbound; lower} - -type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t - -let _pr_constraints_map (cmap:constraints_map) = - let open Pp in - LMap.fold (fun l cstrs acc -> - Level.pr l ++ str " => " ++ - prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ - fnl () ++ acc) - cmap (mt ()) - -let remove_alg l (ctx, us, algs, insts, cstrs) = - (ctx, us, LSet.remove l algs, insts, cstrs) - -let not_lower lower (d,l) = - (* We're checking if (d,l) is already implied by the lower - constraints on some level u. If it represents l < u (d is Lt - or d is Le and i > 0, the i < 0 case is impossible due to - invariants of Univ), and the lower constraints only have l <= - u then it is not implied. *) - Univ.Universe.exists - (fun (l,i) -> - let d = - if i == 0 then d - else match d with - | Le -> Lt - | d -> d - in - try let d' = LMap.find l lower in - (* If d is stronger than the already implied lower - * constraints we must keep it. *) - compare_constraint_type d d' > 0 - with Not_found -> - (** No constraint existing on l *) true) l - -exception UpperBoundedAlg -(** [enforce_uppers upper lbound cstrs] interprets [upper] as upper - constraints to [lbound], adding them to [cstrs]. - - @raise UpperBoundedAlg if any [upper] constraints are strict and - [lbound] algebraic. *) -let enforce_uppers upper lbound cstrs = - List.fold_left (fun cstrs (d, r) -> - if d == Univ.Le then - enforce_leq lbound (Universe.make r) cstrs - else - match Universe.level lbound with - | Some lev -> Constraint.add (lev, d, r) cstrs - | None -> raise UpperBoundedAlg) - cstrs upper - -let minimize_univ_variables ctx us algs left right cstrs = - let left, lbounds = - Univ.LMap.fold (fun r lower (left, lbounds as acc) -> - if Univ.LMap.mem r us || not (Univ.LSet.mem r ctx) then acc - else (* Fixed universe, just compute its glb for sharing *) - let lbounds = - match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with - | None -> lbounds - | Some lbound -> LMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower} - lbounds - in (Univ.LMap.remove r left, lbounds)) - left (left, Univ.LMap.empty) - in - let rec instance (ctx, us, algs, insts, cstrs as acc) u = - let acc, left, lower = - match LMap.find u left with - | exception Not_found -> acc, [], LMap.empty - | l -> - let acc, left, newlow, lower = - List.fold_left - (fun (acc, left, newlow, lower') (d, l) -> - let acc', {enforce=enf;alg;lbound=l';lower} = aux acc l in - let l' = - if enf then Universe.make l - else l' - in acc', (d, l') :: left, - lower_add l d newlow, lower_union lower lower') - (acc, [], LMap.empty, LMap.empty) l - in - let left = List.uniquize (List.filter (not_lower lower) left) in - (acc, left, LMap.union newlow lower) - in - let instantiate_lbound lbound = - let alg = LSet.mem u algs in - if alg then - (* u is algebraic: we instantiate it with its lower bound, if any, - or enforce the constraints if it is bounded from the top. *) - let lower = LSet.fold LMap.remove (Universe.levels lbound) lower in - instantiate_with_lbound u lbound lower ~alg:true ~enforce:false acc - else (* u is non algebraic *) - match Universe.level lbound with - | Some l -> (* The lowerbound is directly a level *) - (* u is not algebraic but has no upper bounds, - we instantiate it with its lower bound if it is a - different level, otherwise we keep it. *) - let lower = LMap.remove l lower in - if not (Level.equal l u) then - (* Should check that u does not - have upper constraints that are not already in right *) - let acc = remove_alg l acc in - instantiate_with_lbound u lbound lower ~alg:false ~enforce:false acc - else acc, {enforce=true; alg=false; lbound; lower} - | None -> - begin match find_inst insts lbound with - | can, lower -> - (* Another universe represents the same lower bound, - we can share them with no harm. *) - let lower = LMap.remove can lower in - instantiate_with_lbound u (Universe.make can) lower ~alg:false ~enforce:false acc - | exception Not_found -> - (* We set u as the canonical universe representing lbound *) - instantiate_with_lbound u lbound lower ~alg:false ~enforce:true acc - end - in - let enforce_uppers ((ctx,us,algs,insts,cstrs), b as acc) = - match LMap.find u right with - | exception Not_found -> acc - | upper -> - let upper = List.filter (fun (d, r) -> not (LMap.mem r us)) upper in - let cstrs = enforce_uppers upper b.lbound cstrs in - (ctx, us, algs, insts, cstrs), b - in - if not (LSet.mem u ctx) - then enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower}) - else - let lbound = compute_lbound left in - match lbound with - | None -> (* Nothing to do *) - enforce_uppers (acc, {enforce=true;alg=false;lbound=Universe.make u; lower}) - | Some lbound -> - try enforce_uppers (instantiate_lbound lbound) - with UpperBoundedAlg -> - enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower}) - and aux (ctx, us, algs, seen, cstrs as acc) u = - try acc, LMap.find u seen - with Not_found -> instance acc u - in - LMap.fold (fun u v (ctx, us, algs, seen, cstrs as acc) -> - if v == None then fst (aux acc u) - else LSet.remove u ctx, us, LSet.remove u algs, seen, cstrs) - us (ctx, us, algs, lbounds, cstrs) - -module UPairs = OrderedType.UnorderedPair(Univ.Level) -module UPairSet = Set.Make (UPairs) - -let normalize_context_set g ctx us algs weak = - let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in - (** Keep the Prop/Set <= i constraints separate for minimization *) - let smallles, csts = - Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts - in - let smallles = if is_set_minimization () - then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles - else Constraint.empty - in - let csts, partition = - (* We first put constraints in a normal-form: all self-loops are collapsed - to equalities. *) - let g = LSet.fold (fun v g -> UGraph.add_universe v false g) - ctx UGraph.initial_universes - in - let add_soft u g = - if not (Level.is_small u || LSet.mem u ctx) - then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g - else g - in - let g = Constraint.fold - (fun (l, d, r) g -> add_soft r (add_soft l g)) - csts g - in - let g = UGraph.merge_constraints csts g in - UGraph.constraints_of_universes g - in - (* We ignore the trivial Prop/Set <= i constraints. *) - let noneqs = - Constraint.filter - (fun (l,d,r) -> not ((d == Le && Level.is_small l) || - (Level.is_prop l && d == Lt && Level.is_set r))) - csts - in - let noneqs = Constraint.union noneqs smallles in - let flex x = LMap.mem x us in - let ctx, us, eqs = List.fold_left (fun (ctx, us, cstrs) s -> - let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in - (* Add equalities for globals which can't be merged anymore. *) - let cstrs = LSet.fold (fun g cst -> - Constraint.add (canon, Eq, g) cst) global - cstrs - in - (* Also add equalities for rigid variables *) - let cstrs = LSet.fold (fun g cst -> - Constraint.add (canon, Eq, g) cst) rigid - cstrs - in - let canonu = Some (Universe.make canon) in - let us = LSet.fold (fun f -> LMap.add f canonu) flexible us in - (LSet.diff ctx flexible, us, cstrs)) - (ctx, us, Constraint.empty) partition - in - (* Process weak constraints: when one side is flexible and the 2 - universes are unrelated unify them. *) - let ctx, us, g = UPairSet.fold (fun (u,v) (ctx, us, g as acc) -> - let norm = level_subst_of (normalize_univ_variable_opt_subst us) in - let u = norm u and v = norm v in - let set_to a b = - (LSet.remove a ctx, - LMap.add a (Some (Universe.make b)) us, - UGraph.enforce_constraint (a,Eq,b) g) - in - if UGraph.check_constraint g (u,Le,v) || UGraph.check_constraint g (v,Le,u) - then acc - else - if LMap.mem u us - then set_to u v - else if LMap.mem v us - then set_to v u - else acc) - weak (ctx, us, g) in - (* Noneqs is now in canonical form w.r.t. equality constraints, - and contains only inequality constraints. *) - let noneqs = - let norm = level_subst_of (normalize_univ_variable_opt_subst us) in - Constraint.fold (fun (u,d,v) noneqs -> - let u = norm u and v = norm v in - if d != Lt && Level.equal u v then noneqs - else Constraint.add (u,d,v) noneqs) - noneqs Constraint.empty - in - (* Compute the left and right set of flexible variables, constraints - mentionning other variables remain in noneqs. *) - let noneqs, ucstrsl, ucstrsr = - Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) -> - let lus = LMap.mem l us and rus = LMap.mem r us in - let ucstrsl' = - if lus then add_list_map l (d, r) ucstrsl - else ucstrsl - and ucstrsr' = - add_list_map r (d, l) ucstrsr - in - let noneqs = - if lus || rus then noneq - else Constraint.add cstr noneq - in (noneqs, ucstrsl', ucstrsr')) - noneqs (Constraint.empty, LMap.empty, LMap.empty) - in - (* Now we construct the instantiation of each variable. *) - let ctx', us, algs, inst, noneqs = - minimize_univ_variables ctx us algs ucstrsr ucstrsl noneqs - in - let us = normalize_opt_subst us in - (us, algs), (ctx', Constraint.union noneqs eqs) - -(* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *) -(* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *) (** Deprecated *) @@ -464,3 +90,8 @@ let subst_univs_universe_constraints = UnivProblem.Set.subst_univs let enforce_eq_instances_univs = UnivProblem.enforce_eq_instances_univs let to_constraints = UnivProblem.to_constraints let eq_constr_univs_infer_with = UnivProblem.eq_constr_univs_infer_with + +(** UnivMinim *) +module UPairSet = UnivMinim.UPairSet + +let normalize_context_set = UnivMinim.normalize_context_set diff --git a/engine/universes.mli b/engine/universes.mli index 4d7105e72..46ff33a47 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -12,37 +12,11 @@ open Names open Constr open Environ open Univ -open UnivSubst - -(** Unordered pairs of universe levels (ie (u,v) = (v,u)) *) -module UPairSet : CSet.S with type elt = (Level.t * Level.t) - -(** Universes *) - -(** Simplification and pruning of constraints: - [normalize_context_set ctx us] - - - Instantiate the variables in [us] with their most precise - universe levels respecting the constraints. - - - Normalizes the context [ctx] w.r.t. equality constraints, - choosing a canonical universe in each equivalence class - (a global one if there is one) and transitively saturate - the constraints w.r.t to the equalities. *) - -val normalize_context_set : UGraph.t -> ContextSet.t -> - universe_opt_subst (* The defined and undefined variables *) -> - LSet.t (* univ variables that can be substituted by algebraics *) -> - UPairSet.t (* weak equality constraints *) -> - (universe_opt_subst * LSet.t) in_universe_context_set - -(** *********************************** Deprecated *) +(** ************************************** *) +(** This entire module is deprecated. **** *) +(** ************************************** *) [@@@ocaml.warning "-3"] -val set_minimization : bool ref -[@@ocaml.deprecated "Becoming internal."] -val is_set_minimization : unit -> bool -[@@ocaml.deprecated "Becoming internal."] (** ****** Deprecated: moved to [UnivNames] *) @@ -250,3 +224,15 @@ val eq_constr_univs_infer_with : (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option [@@ocaml.deprecated "Use [UnivProblem.eq_constr_univs_infer_with]"] + +(** ****** Deprecated: moved to [UnivMinim] *) + +module UPairSet = UnivMinim.UPairSet +[@@ocaml.deprecated "Use [UnivMinim.UPairSet]"] + +val normalize_context_set : UGraph.t -> ContextSet.t -> + universe_opt_subst (* The defined and undefined variables *) -> + LSet.t (* univ variables that can be substituted by algebraics *) -> + UPairSet.t (* weak equality constraints *) -> + (universe_opt_subst * LSet.t) in_universe_context_set +[@@ocaml.deprecated "Use [UnivMinim.normalize_context_set]"] -- cgit v1.2.3