1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226
(************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) open Univ module G = AcyclicGraph.Make(struct type t = Level.t module Set = LSet module Map = LMap module Constraint = Constraint let equal = Level.equal let compare = Level.compare type explanation = Univ.explanation let error_inconsistency d u v p = raise (UniverseInconsistency (d,Universe.make u, Universe.make v, p)) let pr = Level.pr end) [@@inlined] (* without inline, +1% ish on HoTT, compcert. See jenkins 594 vs 596 *) (* Do not include G to make it easier to control universe specific code (eg add_universe with a constraint vs G.add with no constraint) *) type t = { graph: G.t; sprop_cumulative : bool } type 'a check_function = t -> 'a -> 'a -> bool let g_map f g = let g' = f g.graph in if g.graph == g' then g else {g with graph=g'} let make_sprop_cumulative g = {g with sprop_cumulative=true} let check_smaller_expr g (u,n) (v,m) = let diff = n - m in match diff with | 0 -> G.check_leq g.graph u v | 1 -> G.check_lt g.graph u v | x when x < 0 -> G.check_leq g.graph u v | _ -> false let exists_bigger g ul l = Universe.exists (fun ul' -> check_smaller_expr g ul ul') l let real_check_leq g u v = Universe.for_all (fun ul -> exists_bigger g ul v) u let check_leq g u v = Universe.equal u v || (g.sprop_cumulative && Universe.is_sprop u) || (not (Universe.is_sprop u) && not (Universe.is_sprop v) && (is_type0m_univ u || real_check_leq g u v)) let check_eq g u v = Universe.equal u v || (not (Universe.is_sprop u || Universe.is_sprop v) && (real_check_leq g u v && real_check_leq g v u)) let check_eq_level g u v = u == v || (not (Level.is_sprop u || Level.is_sprop v) && G.check_eq g.graph u v) let empty_universes = {graph=G.empty; sprop_cumulative=false} let initial_universes = let big_rank = 1000000 in let g = G.empty in let g = G.add ~rank:big_rank Level.prop g in let g = G.add ~rank:big_rank Level.set g in {graph=G.enforce_lt Level.prop Level.set g; sprop_cumulative=false} let enforce_constraint (u,d,v) g = match d with | Le -> G.enforce_leq u v g | Lt -> G.enforce_lt u v g | Eq -> G.enforce_eq u v g let enforce_constraint (u,d,v as cst) g = match Level.is_sprop u, d, Level.is_sprop v with | false, _, false -> g_map (enforce_constraint cst) g | true, (Eq|Le), true -> g | true, Le, false when g.sprop_cumulative -> g | _ -> raise (UniverseInconsistency (d,Universe.make u, Universe.make v, None)) let merge_constraints csts g = Constraint.fold enforce_constraint csts g let check_constraint g (u,d,v) = match d with | Le -> G.check_leq g u v | Lt -> G.check_lt g u v | Eq -> G.check_eq g u v let check_constraint g (u,d,v as cst) = match Level.is_sprop u, d, Level.is_sprop v with | false, _, false -> check_constraint g.graph cst | true, (Eq|Le), true -> true | true, Le, false -> g.sprop_cumulative | _ -> false let check_constraints csts g = Constraint.for_all (check_constraint g) csts let leq_expr (u,m) (v,n) = let d = match m - n with | 1 -> Lt | diff -> assert (diff <= 0); Le in (u,d,v) let enforce_leq_alg u v g = let open Util in let enforce_one (u,v) = function | Inr _ as orig -> orig | Inl (cstrs,g) as orig -> if check_smaller_expr g u v then orig else (let c = leq_expr u v in match enforce_constraint c g with | g -> Inl (Constraint.add c cstrs,g) | exception (UniverseInconsistency _ as e) -> Inr e) in (* max(us) <= max(vs) <-> forall u in us, exists v in vs, u <= v *) let c = Universe.map (fun u -> Universe.map (fun v -> (u,v)) v) u in let c = List.cartesians enforce_one (Inl (Constraint.empty,g)) c in (* We pick a best constraint: smallest number of constraints, not an error if possible. *) let order x y = match x, y with | Inr _, Inr _ -> 0 | Inl _, Inr _ -> -1 | Inr _, Inl _ -> 1 | Inl (c,_), Inl (c',_) -> Int.compare (Constraint.cardinal c) (Constraint.cardinal c') in match List.min order c with | Inl x -> x | Inr e -> raise e (* sanity check wrapper *) let enforce_leq_alg u v g = let _,g as cg = enforce_leq_alg u v g in assert (check_leq g u v); cg exception AlreadyDeclared = G.AlreadyDeclared let add_universe u ~lbound ~strict g = let graph = G.add u g.graph in let d = if strict then Lt else Le in enforce_constraint (lbound,d,u) {g with graph} let add_universe_unconstrained u g = {g with graph=G.add u g.graph} exception UndeclaredLevel = G.Undeclared let check_declared_universes g l = G.check_declared g.graph (LSet.remove Level.sprop l) let constraints_of_universes g = G.constraints_of g.graph let constraints_for ~kept g = G.constraints_for ~kept:(LSet.remove Level.sprop kept) g.graph (** Subtyping of polymorphic contexts *) let check_subtype ~lbound univs ctxT ctx = if AUContext.size ctxT == AUContext.size ctx then let (inst, cst) = UContext.dest (AUContext.repr ctx) in let cstT = UContext.constraints (AUContext.repr ctxT) in let push accu v = add_universe v ~lbound ~strict:false accu in let univs = Array.fold_left push univs (Instance.to_array inst) in let univs = merge_constraints cstT univs in check_constraints cst univs else false (** Instances *) let check_eq_instances g t1 t2 = let t1 = Instance.to_array t1 in let t2 = Instance.to_array t2 in t1 == t2 || (Int.equal (Array.length t1) (Array.length t2) && let rec aux i = (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1)) in aux 0) let domain g = LSet.add Level.sprop (G.domain g.graph) let choose p g u = if Level.is_sprop u then if p u then Some u else None else G.choose p g.graph u let dump_universes f g = G.dump f g.graph let check_universes_invariants g = G.check_invariants ~required_canonical:Level.is_small g.graph let pr_universes prl g = G.pr prl g.graph let dummy_mp = Names.DirPath.make [Names.Id.of_string "Type"] let make_dummy i = Level.(make (UGlobal.make dummy_mp i)) let sort_universes g = g_map (G.sort make_dummy [Level.prop;Level.set]) g (** Profiling *) let merge_constraints = if Flags.profile then let key = CProfile.declare_profile "merge_constraints" in CProfile.profile2 key merge_constraints else merge_constraints let check_constraints = if Flags.profile then let key = CProfile.declare_profile "check_constraints" in CProfile.profile2 key check_constraints else check_constraints let check_eq = if Flags.profile then let check_eq_key = CProfile.declare_profile "check_eq" in CProfile.profile3 check_eq_key check_eq else check_eq let check_leq = if Flags.profile then let check_leq_key = CProfile.declare_profile "check_leq" in CProfile.profile3 check_leq_key check_leq else check_leq