From 2e30531e78519a5b9c3773c2524e4fd4759cc5c8 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 1 Mar 2018 18:28:36 +0100 Subject: Delayed weak constraints for cumulative inductive types. When comparing 2 irrelevant universes [u] and [v] we add a "weak constraint" [UWeak(u,v)] to the UState. Then at minimization time a weak constraint between unrelated universes where one is flexible causes them to be unified. --- engine/eConstr.ml | 4 +-- engine/eConstr.mli | 2 -- engine/evarutil.ml | 20 +++++++-------- engine/termops.ml | 4 ++- engine/uState.ml | 69 +++++++++++++++++++++++++++++++++++----------------- engine/uState.mli | 4 +++ engine/universes.ml | 60 ++++++++++++++++++++++++++++++++++++--------- engine/universes.mli | 15 +++++++++--- 8 files changed, 126 insertions(+), 52 deletions(-) (limited to 'engine') diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 0d55b92c2..3ee072214 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -570,8 +570,6 @@ let compare_constr sigma cmp c1 c2 = let cmp nargs c1 c2 = cmp (of_constr c1) (of_constr c2) in compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2) -let cumul_weak_constraints = ref true - let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs = let open Universes in if not nargs_ok then enforce_eq_instances_univs false u u' cstrs @@ -580,7 +578,7 @@ let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs = (fun cstrs v u u' -> let open Univ.Variance in match v with - | Irrelevant -> if !cumul_weak_constraints then Constraints.add (ULub (u,u')) cstrs else cstrs + | Irrelevant -> Constraints.add (UWeak (u,u')) cstrs | Covariant -> let u = Univ.Universe.make u in let u' = Univ.Universe.make u' in diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 87531e116..28c9dd3c2 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -196,8 +196,6 @@ val whd_evar : Evd.evar_map -> constr -> constr (** {6 Equality} *) -val cumul_weak_constraints : bool ref - val eq_constr : Evd.evar_map -> t -> t -> bool val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool val eq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option diff --git a/engine/evarutil.ml b/engine/evarutil.ml index fdb14b725..9cf81ecce 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -813,20 +813,16 @@ let subterm_source evk (loc,k) = | _ -> evk in (loc,Evar_kinds.SubEvar evk) -let try_soft evd u u' = - let open Universes in - try Evd.add_universe_constraints evd (Constraints.singleton (ULub (u, u'))) - with UState.UniversesDiffer | Univ.UniverseInconsistency _ -> evd - (* Add equality constraints for covariant/invariant positions. For irrelevant positions, unify universes when flexible. *) let compare_cumulative_instances cv_pb variances u u' sigma = + let open Universes in let cstrs = Univ.Constraint.empty in - let soft = [] in + let soft = Constraints.empty in let cstrs, soft = Array.fold_left3 (fun (cstrs, soft) v u u' -> let open Univ.Variance in match v with - | Irrelevant -> cstrs, if !EConstr.cumul_weak_constraints then (u,u')::soft else soft + | Irrelevant -> cstrs, Constraints.add (UWeak (u,u')) soft | Covariant when cv_pb == Reduction.CUMUL -> Univ.Constraint.add (u,Univ.Le,u') cstrs, soft | Covariant | Invariant -> Univ.Constraint.add (u,Univ.Eq,u') cstrs, soft) @@ -834,12 +830,16 @@ let compare_cumulative_instances cv_pb variances u u' sigma = in match Evd.add_constraints sigma cstrs with | sigma -> - Inl (List.fold_left (fun sigma (u,u') -> try_soft sigma u u') sigma soft) + Inl (Evd.add_universe_constraints sigma soft) | exception Univ.UniverseInconsistency p -> Inr p let compare_constructor_instances evd u u' = - Array.fold_left2 try_soft - evd (Univ.Instance.to_array u) (Univ.Instance.to_array u') + let open Universes in + let soft = + Array.fold_left2 (fun cs u u' -> Constraints.add (UWeak (u,u')) cs) + Constraints.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') + in + Evd.add_universe_constraints evd soft (** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and [u] up to existential variable instantiation and equalisable diff --git a/engine/termops.ml b/engine/termops.ml index 20b6b3504..3dfb0c34f 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -302,7 +302,9 @@ let pr_evar_universe_context ctx = str"ALGEBRAIC UNIVERSES:"++brk(0,1)++ h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++ str"UNDEFINED UNIVERSES:"++brk(0,1)++ - h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl()) + h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++ + str "WEAK CONSTRAINTS:"++brk(0,1)++ + h 0 (UState.pr_weak prl ctx) ++ fnl ()) let print_env_short env = let print_constr = print_kconstr in diff --git a/engine/uState.ml b/engine/uState.ml index 8111ebffe..1dd8acd0d 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -20,6 +20,8 @@ type uinfo = { uloc : Loc.t option; } +module UPairSet = Universes.UPairSet + (* 2nd part used to check consistency on the fly. *) type t = { uctx_names : Universes.universe_binders * uinfo Univ.LMap.t; @@ -32,6 +34,7 @@ type t = algebraic universes as they appear in inferred types only. *) uctx_universes : UGraph.t; (** The current graph extended with the local constraints *) uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *) + uctx_weak_constraints : UPairSet.t } let empty = @@ -41,7 +44,8 @@ let empty = uctx_univ_variables = Univ.LMap.empty; uctx_univ_algebraic = Univ.LSet.empty; uctx_universes = UGraph.initial_universes; - uctx_initial_universes = UGraph.initial_universes; } + uctx_initial_universes = UGraph.initial_universes; + uctx_weak_constraints = UPairSet.empty; } let make u = { empty with @@ -69,6 +73,7 @@ let union ctx ctx' = let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local) (Univ.ContextSet.levels ctx.uctx_local) in let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in + let weak = UPairSet.union ctx.uctx_weak_constraints ctx'.uctx_weak_constraints in let declarenew g = Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) newus g in @@ -82,10 +87,11 @@ let union ctx ctx' = Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic; uctx_initial_universes = declarenew ctx.uctx_initial_universes; uctx_universes = - if local == ctx.uctx_local then ctx.uctx_universes - else - let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in - UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) } + (if local == ctx.uctx_local then ctx.uctx_universes + else + let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in + UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes)); + uctx_weak_constraints = weak} let context_set ctx = ctx.uctx_local @@ -142,14 +148,18 @@ let instantiate_variable l b v = exception UniversesDiffer +let drop_weak_constraints = ref false + let process_universe_constraints ctx cstrs = let open Univ in let open Universes in let univs = ctx.uctx_universes in let vars = ref ctx.uctx_univ_variables in + let weak = ref ctx.uctx_weak_constraints in let normalize = normalize_univ_variable_opt_subst vars in let nf_constraint = function | ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v) + | UWeak (u, v) -> UWeak (level_subst_of normalize u, level_subst_of normalize v) | UEq (u, v) -> UEq (subst_univs_universe normalize u, subst_univs_universe normalize v) | ULe (u, v) -> ULe (subst_univs_universe normalize u, subst_univs_universe normalize v) in @@ -226,12 +236,14 @@ let process_universe_constraints ctx cstrs = end | ULub (l, r) -> equalize_variables true (Universe.make l) l (Universe.make r) r local + | UWeak (l, r) -> + if not !drop_weak_constraints then weak := UPairSet.add (l,r) !weak; local | UEq (l, r) -> equalize_universes l r local in let local = Constraints.fold unify_universes cstrs Univ.Constraint.empty in - !vars, local + !vars, !weak, local let add_constraints ctx cstrs = let univs, local = ctx.uctx_local in @@ -245,20 +257,24 @@ let add_constraints ctx cstrs = in Universes.Constraints.add cstr' acc) cstrs Universes.Constraints.empty in - let vars, local' = process_universe_constraints ctx cstrs' in - { ctx with uctx_local = (univs, Univ.Constraint.union local local'); - uctx_univ_variables = vars; - uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } + let vars, weak, local' = process_universe_constraints ctx cstrs' in + { ctx with + uctx_local = (univs, Univ.Constraint.union local local'); + uctx_univ_variables = vars; + uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes; + uctx_weak_constraints = weak; } (* let addconstrkey = CProfile.declare_profile "add_constraints_context";; *) (* let add_constraints_context = CProfile.profile2 addconstrkey add_constraints_context;; *) let add_universe_constraints ctx cstrs = let univs, local = ctx.uctx_local in - let vars, local' = process_universe_constraints ctx cstrs in - { ctx with uctx_local = (univs, Univ.Constraint.union local local'); - uctx_univ_variables = vars; - uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } + let vars, weak, local' = process_universe_constraints ctx cstrs in + { ctx with + uctx_local = (univs, Univ.Constraint.union local local'); + uctx_univ_variables = vars; + uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes; + uctx_weak_constraints = weak; } let constrain_variables diff ctx = let univs, local = ctx.uctx_local in @@ -567,16 +583,18 @@ let fix_undefined_variables uctx = let refresh_undefined_univ_variables uctx = let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in - let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (Univ.subst_univs_level_level subst u) acc) + let subst_fn u = Univ.subst_univs_level_level subst u in + let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (subst_fn u) acc) uctx.uctx_univ_algebraic Univ.LSet.empty in let vars = Univ.LMap.fold (fun u v acc -> - Univ.LMap.add (Univ.subst_univs_level_level subst u) + Univ.LMap.add (subst_fn u) (Option.map (Univ.subst_univs_level_universe subst) v) acc) uctx.uctx_univ_variables Univ.LMap.empty in + let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.uctx_weak_constraints UPairSet.empty in let declare g = Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) (Univ.ContextSet.levels ctx') g in let initial = declare uctx.uctx_initial_universes in @@ -586,18 +604,20 @@ let refresh_undefined_univ_variables uctx = uctx_seff_univs = uctx.uctx_seff_univs; uctx_univ_variables = vars; uctx_univ_algebraic = alg; uctx_universes = univs; - uctx_initial_universes = initial } in + uctx_initial_universes = initial; + uctx_weak_constraints = weak; } in uctx', subst let minimize uctx = - let ((vars',algs'), us') = - Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables - uctx.uctx_univ_algebraic + let open Universes 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 in if Univ.ContextSet.equal us' uctx.uctx_local then uctx else let us', universes = - Universes.refresh_constraints uctx.uctx_initial_universes us' + refresh_constraints uctx.uctx_initial_universes us' in { uctx_names = uctx.uctx_names; uctx_local = us'; @@ -605,7 +625,8 @@ let minimize uctx = uctx_univ_variables = vars'; uctx_univ_algebraic = algs'; uctx_universes = universes; - uctx_initial_universes = uctx.uctx_initial_universes } + uctx_initial_universes = uctx.uctx_initial_universes; + uctx_weak_constraints = UPairSet.empty; (* weak constraints are consumed *) } let universe_of_name uctx s = UNameMap.find s (fst uctx.uctx_names) @@ -618,5 +639,9 @@ let update_sigma_env uctx env = in merge true univ_rigid eunivs eunivs.uctx_local +let pr_weak prl {uctx_weak_constraints=weak} = + let open Pp in + prlist_with_sep fnl (fun (u,v) -> prl u ++ str " ~ " ++ prl v) (UPairSet.elements weak) + (** Deprecated *) let normalize = minimize diff --git a/engine/uState.mli b/engine/uState.mli index 9a2bc706b..48c38fafc 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -72,6 +72,8 @@ val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes (** {5 Constraints handling} *) +val drop_weak_constraints : bool ref + val add_constraints : t -> Univ.Constraint.t -> t (** @raise UniversesDiffer when universes differ @@ -164,3 +166,5 @@ val update_sigma_env : t -> Environ.env -> t val pr_uctx_level : t -> Univ.Level.t -> Pp.t val reference_of_level : t -> Univ.Level.t -> Libnames.reference + +val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t diff --git a/engine/universes.ml b/engine/universes.ml index ae5eef067..ddc9beff4 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -18,6 +18,9 @@ open Univ open Globnames open Nametab +module UPairs = OrderedType.UnorderedPair(Univ.Level) +module UPairSet = Set.Make (UPairs) + let reference_of_level l = match Level.name l with | Some (d, n as na) -> @@ -118,6 +121,7 @@ type universe_constraint = | ULe of Universe.t * Universe.t | UEq of Universe.t * Universe.t | ULub of Level.t * Level.t + | UWeak of Level.t * Level.t module Constraints = struct module S = Set.Make( @@ -135,7 +139,7 @@ module Constraints = struct if Int.equal i 0 then Universe.compare v v' else if Universe.equal u v' && Universe.equal v u' then 0 else i - | ULub (u, v), ULub (u', v') -> + | ULub (u, v), ULub (u', v') | UWeak (u, v), UWeak (u', v') -> let i = Level.compare u u' in if Int.equal i 0 then Level.compare v v' else if Level.equal u v' && Level.equal v u' then 0 @@ -144,13 +148,15 @@ module Constraints = struct | _, ULe _ -> 1 | UEq _, _ -> -1 | _, UEq _ -> 1 + | ULub _, _ -> -1 + | _, ULub _ -> 1 end) include S let is_trivial = function | ULe (u, v) | UEq (u, v) -> Universe.equal u v - | ULub (u, v) -> Level.equal u v + | ULub (u, v) | UWeak (u, v) -> Level.equal u v let add cst s = if is_trivial cst then s @@ -160,6 +166,7 @@ module Constraints = struct | ULe (u, v) -> Universe.pr u ++ str " <= " ++ Universe.pr v | UEq (u, v) -> Universe.pr u ++ str " = " ++ Universe.pr v | ULub (u, v) -> Level.pr u ++ str " /\\ " ++ Level.pr v + | UWeak (u, v) -> Level.pr u ++ str " ~ " ++ Level.pr v let pr c = fold (fun cst pp_std -> @@ -231,19 +238,25 @@ let subst_univs_universe_constraint fn = function let u' = level_subst_of fn u and v' = level_subst_of fn v in if Level.equal u' v' then None else Some (ULub (u',v')) + | UWeak (u, v) -> + let u' = level_subst_of fn u and v' = level_subst_of fn v in + if Level.equal u' v' then None + else Some (UWeak (u',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 to_constraints ~force_weak g s = let invalid () = raise (Invalid_argument "to_constraints: non-trivial algebraic constraint between universes") in let tr cst acc = match cst with | ULub (l, l') -> Constraint.add (l, Eq, l') acc + | UWeak (l, l') when force_weak -> Constraint.add (l, Eq, l') acc + | UWeak _-> acc | ULe (l, l') -> begin match Universe.level l, Universe.level l' with | Some l, Some l' -> Constraint.add (l, Le, l') acc @@ -905,7 +918,7 @@ let minimize_univ_variables ctx us algs left right cstrs = else LSet.remove u ctx', us, LSet.remove u algs, seen, cstrs) us (ctx, us, algs, lbounds, cstrs) -let normalize_context_set ctx us algs = +let normalize_context_set g ctx us algs weak = let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in let uf = UF.create () in (** Keep the Prop/Set <= i constraints separate for minimization *) @@ -925,7 +938,7 @@ let normalize_context_set ctx us algs = else (smallles, Constraint.add cstr noneqs)) csts (Constraint.empty, Constraint.empty) in - let csts = + let csts = (* We first put constraints in a normal-form: all self-loops are collapsed to equalities. *) let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) @@ -963,7 +976,7 @@ let normalize_context_set ctx us algs = let noneqs = Constraint.union noneqs smallles in let partition = UF.partition uf in let flex x = LMap.mem x us in - let ctx, subst, us, eqs = List.fold_left (fun (ctx, subst, us, cstrs) s -> + 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 -> @@ -975,16 +988,41 @@ let normalize_context_set ctx us algs = Constraint.add (canon, Univ.Eq, g) cst) rigid cstrs in - let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in - let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst 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, subst, us, cstrs)) - (ctx, LMap.empty, us, Constraint.empty) partition + (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 = let us = ref us in 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 = subst_univs_level_constraints subst noneqs in + let noneqs = + let us = ref us in + 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 = diff --git a/engine/universes.mli b/engine/universes.mli index 4af944347..4823c5746 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -14,6 +14,9 @@ open Constr open Environ open Univ +(** Unordered pairs of universe levels (ie (u,v) = (v,u)) *) +module UPairSet : CSet.S with type elt = (Level.t * Level.t) + val set_minimization : bool ref val is_set_minimization : unit -> bool @@ -69,12 +72,15 @@ val new_sort_in_family : Sorts.family -> Sorts.t 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. + + UWeak constraints come from irrelevant universes in cumulative polymorphism. *) type universe_constraint = | ULe of Universe.t * Universe.t | UEq of Universe.t * Universe.t | ULub of Level.t * Level.t + | UWeak of Level.t * Level.t module Constraints : sig include Set.S with type elt = universe_constraint @@ -96,7 +102,9 @@ val subst_univs_universe_constraints : universe_subst_fn -> val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function -val to_constraints : UGraph.t -> Constraints.t -> Constraint.t +(** With [force_weak] UWeak constraints are turned into equalities, + otherwise they're forgotten. *) +val to_constraints : force_weak:bool -> UGraph.t -> Constraints.t -> Constraint.t (** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of {!eq_constr_univs_infer} taking kind-of-term functions, to expose @@ -167,9 +175,10 @@ val make_opt_subst : universe_opt_subst -> universe_subst_fn val subst_opt_univs_constr : universe_opt_subst -> constr -> constr -val normalize_context_set : ContextSet.t -> +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 *) -> + LSet.t (* univ variables that can be substituted by algebraics *) -> + UPairSet.t (* weak equality constraints *) -> (universe_opt_subst * LSet.t) in_universe_context_set val normalize_univ_variables : universe_opt_subst -> -- cgit v1.2.3