From d640b676282285d52ac19038d693080e64eb5ea7 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 1 Mar 2018 15:19:52 +0100 Subject: Statically enforce that ULub is only between levels. --- engine/eConstr.ml | 21 ++++---- engine/evarutil.ml | 3 +- engine/evd.ml | 9 +--- engine/evd.mli | 1 - engine/uState.ml | 38 +++++++------ engine/universes.ml | 148 ++++++++++++++++++++++++++++++--------------------- engine/universes.mli | 8 ++- 7 files changed, 128 insertions(+), 100 deletions(-) (limited to 'engine') diff --git a/engine/eConstr.ml b/engine/eConstr.ml index e832a0688..0d55b92c2 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -579,15 +579,18 @@ let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs = CArray.fold_left3 (fun cstrs v u u' -> let open Univ.Variance in - let u = Univ.Universe.make u in - let u' = Univ.Universe.make u' in match v with - | Irrelevant -> if !cumul_weak_constraints then Constraints.add (u,ULub,u') cstrs else cstrs + | Irrelevant -> if !cumul_weak_constraints then Constraints.add (ULub (u,u')) cstrs else cstrs | Covariant -> + let u = Univ.Universe.make u in + let u' = Univ.Universe.make u' in (match cv_pb with - | Reduction.CONV -> Constraints.add (u,UEq,u') cstrs - | Reduction.CUMUL -> Constraints.add (u,ULe,u') cstrs) - | Invariant -> Constraints.add (u,UEq,u') cstrs) + | Reduction.CONV -> Constraints.add (UEq (u,u')) cstrs + | Reduction.CUMUL -> Constraints.add (ULe (u,u')) cstrs) + | Invariant -> + let u = Univ.Universe.make u in + let u' = Univ.Universe.make u' in + Constraints.add (UEq (u,u')) cstrs) cstrs variances (Univ.Instance.to_array u) (Univ.Instance.to_array u') let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs = @@ -648,7 +651,7 @@ let test_constr_universes env sigma leq m n = let s2 = ESorts.kind sigma (ESorts.make s2) in if Sorts.equal s1 s2 then true else (cstrs := Constraints.add - (Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs; + (UEq (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs; true) in let leq_sorts s1 s2 = @@ -657,7 +660,7 @@ let test_constr_universes env sigma leq m n = if Sorts.equal s1 s2 then true else (cstrs := Constraints.add - (Sorts.univ_of_sort s1,ULe,Sorts.univ_of_sort s2) !cstrs; + (ULe (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs; true) in let rec eq_constr' nargs m n = compare_gen kind eq_universes eq_sorts eq_constr' nargs m n in @@ -703,7 +706,7 @@ let eq_constr_universes_proj env sigma m n = if Sorts.equal s1 s2 then true else (cstrs := Constraints.add - (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs; + (UEq (Sorts.univ_of_sort s1, Sorts.univ_of_sort s2)) !cstrs; true) in let rec eq_constr' nargs m n = diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 2b6913c0b..fdb14b725 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -815,8 +815,7 @@ let subterm_source evk (loc,k) = let try_soft evd u u' = let open Universes in - let make = Univ.Universe.make in - try Evd.add_universe_constraints evd (Constraints.singleton (make u,ULub,make u')) + 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 diff --git a/engine/evd.ml b/engine/evd.ml index b7b87370e..f6e13e1f4 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -857,15 +857,10 @@ let set_eq_sort env d s1 s2 = | Some (u1, u2) -> if not (type_in_type env) then add_universe_constraints d - (Universes.Constraints.singleton (u1,Universes.UEq,u2)) + (Universes.Constraints.singleton (Universes.UEq (u1,u2))) else d -let has_lub evd u1 u2 = - if Univ.Universe.equal u1 u2 then evd - else add_universe_constraints evd - (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) @@ -883,7 +878,7 @@ let set_leq_sort env evd s1 s2 = | None -> evd | Some (u1, u2) -> if not (type_in_type env) then - add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2)) + add_universe_constraints evd (Universes.Constraints.singleton (Universes.ULe (u1,u2))) else evd let check_eq evd s s' = diff --git a/engine/evd.mli b/engine/evd.mli index bd9d75c6b..911799c44 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -583,7 +583,6 @@ val normalize_universe_instance : evar_map -> Univ.Instance.t -> Univ.Instance.t val set_leq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map val set_eq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map -val has_lub : evar_map -> Univ.Universe.t -> Univ.Universe.t -> evar_map val set_eq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map val set_leq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map val set_eq_instances : ?flex:bool -> diff --git a/engine/uState.ml b/engine/uState.ml index e57afd743..8111ebffe 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -144,9 +144,15 @@ exception UniversesDiffer 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 normalize = Universes.normalize_universe_opt_subst vars 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) + | 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 let is_local l = Univ.LMap.mem l !vars in let varinfo x = match Univ.Universe.level x with @@ -185,12 +191,12 @@ let process_universe_constraints ctx cstrs = if UGraph.check_eq univs l r then local else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) in - let unify_universes (l, d, r) local = - let l = normalize l and r = normalize r in - if Univ.Universe.equal l r then local + let unify_universes cst local = + let cst = nf_constraint cst in + if Constraints.is_trivial cst then local else - match d with - | Universes.ULe -> + match cst with + | ULe (l, r) -> if UGraph.check_leq univs l r then (** Keep Prop/Set <= var around if var might be instantiated by prop or set later. *) @@ -218,16 +224,12 @@ let process_universe_constraints ctx cstrs = else Univ.enforce_leq l r local end - | Universes.ULub -> - begin match Universe.level l, Universe.level r with - | Some l', Some r' -> - equalize_variables true l l' r r' local - | _, _ -> assert false - end - | Universes.UEq -> equalize_universes l r local + | ULub (l, r) -> + equalize_variables true (Universe.make l) l (Universe.make r) r local + | UEq (l, r) -> equalize_universes l r local in let local = - Universes.Constraints.fold unify_universes cstrs Univ.Constraint.empty + Constraints.fold unify_universes cstrs Univ.Constraint.empty in !vars, local @@ -235,9 +237,11 @@ let add_constraints ctx cstrs = let univs, local = ctx.uctx_local in 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, Universes.ULe, r) - else (l, (if d == Univ.Le then Universes.ULe else Universes.UEq), r) + let cstr' = match d with + | Univ.Lt -> + Universes.ULe (Univ.Universe.super l, r) + | Univ.Le -> Universes.ULe (l, r) + | Univ.Eq -> Universes.UEq (l, r) in Universes.Constraints.add cstr' acc) cstrs Universes.Constraints.empty in diff --git a/engine/universes.ml b/engine/universes.ml index 70ed6311e..ae5eef067 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -114,53 +114,56 @@ let universe_binders_with_opt_names ref levels = function let set_minimization = ref true let is_set_minimization () = !set_minimization -type universe_constraint_type = ULe | UEq | ULub - -type universe_constraint = Universe.t * universe_constraint_type * Universe.t +type universe_constraint = + | ULe of Universe.t * Universe.t + | UEq of Universe.t * Universe.t + | ULub of Level.t * Level.t 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 + let compare x y = + match x, y with + | ULe (u, v), ULe (u', v') -> + let i = Universe.compare u u' in + if Int.equal i 0 then Universe.compare v v' + else i + | UEq (u, v), UEq (u', v') -> + let i = Universe.compare u u' in + 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') -> + 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 + else i + | ULe _, _ -> -1 + | _, ULe _ -> 1 + | UEq _, _ -> -1 + | _, UEq _ -> 1 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 is_trivial = function + | ULe (u, v) | UEq (u, v) -> Universe.equal u v + | ULub (u, v) -> Level.equal u v - let op_str = function ULe -> " <= " | UEq -> " = " | ULub -> " /\\ " + let add cst s = + if is_trivial cst then s + else add cst s + + let pr_one = function + | 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 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 "") + fold (fun cst pp_std -> + pp_std ++ pr_one cst ++ fnl ()) c (str "") let equal x y = x == y || equal x y @@ -174,13 +177,13 @@ 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 mk u v = if strict then ULub (u, v) else UEq (Universe.make u, Universe.make v) in let ax = Instance.to_array x and ay = Instance.to_array y in if Array.length ax != Array.length ay then CErrors.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)) + (fun x y -> Constraints.add (mk x y)) ax ay c let enforce_univ_constraint (u,d,v) = @@ -207,30 +210,59 @@ let subst_univs_constraints subst csts = (fun c cstrs -> subst_univs_constraint subst c cstrs) csts Constraint.empty -let subst_univs_universe_constraint fn (u,d,v) = - let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in +let level_subst_of f = + fun l -> + try let u = f l in + match Universe.level u with + | None -> l + | Some l -> l + with Not_found -> l + +let subst_univs_universe_constraint fn = function + | ULe (u, 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') + else Some (ULe (u',v')) + | UEq (u, 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 (ULe (u',v')) + | ULub (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 (ULub (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 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 UGraph.check_leq else UGraph.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 to_constraints 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 + | ULe (l, l') -> + begin match Universe.level l, Universe.level l' with + | Some l, Some l' -> Constraint.add (l, Le, l') acc + | None, Some _ -> enforce_leq l l' acc + | _, None -> + if UGraph.check_leq g l l' + then acc + else invalid () + end + | UEq (l, l') -> + begin match Universe.level l, Universe.level l' with + | Some l, Some l' -> Constraint.add (l, Eq, l') acc + | None, _ | _, None -> + if UGraph.check_eq g l l' + then acc + else invalid () + end + in + Constraints.fold tr s Constraint.empty (** Variant of [eq_constr_univs_infer] taking kind-of-term functions, to expose subterms of [m] and [n], arguments. *) @@ -247,7 +279,7 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with + match fold (Constraints.singleton (UEq (u1, u2))) !cstrs with | None -> false | Some accu -> cstrs := accu; true in @@ -512,14 +544,6 @@ let choose_canonical ctx flexible algs s = let canon = LSet.choose algs in canon, (global, rigid, LSet.remove canon flexible) -let level_subst_of f = - fun l -> - try let u = f l in - match Universe.level u with - | None -> l - | Some l -> l - with Not_found -> l - let subst_univs_fn_constr f c = let changed = ref false in let fu = Univ.subst_univs_universe f in diff --git a/engine/universes.mli b/engine/universes.mli index a86b9779b..4af944347 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -71,12 +71,16 @@ val new_sort_in_family : Sorts.family -> Sorts.t not be necessary if unfolding is performed. *) -type universe_constraint_type = ULe | UEq | ULub +type universe_constraint = + | ULe of Universe.t * Universe.t + | UEq of Universe.t * Universe.t + | ULub of Level.t * Level.t -type universe_constraint = Universe.t * universe_constraint_type * Universe.t module Constraints : sig include Set.S with type elt = universe_constraint + val is_trivial : universe_constraint -> bool + val pr : t -> Pp.t end -- cgit v1.2.3