diff options
Diffstat (limited to 'kernel/uGraph.ml')
| -rw-r--r-- | kernel/uGraph.ml | 96 |
1 files changed, 76 insertions, 20 deletions
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 4884d0de..5d5c4831 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 *) +(* // * 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 Pp @@ -132,7 +134,7 @@ let rec repr g u = let a = try UMap.find u g.entries with Not_found -> CErrors.anomaly ~label:"Univ.repr" - (str"Universe " ++ Level.pr u ++ str" undefined") + (str"Universe " ++ Level.pr u ++ str" undefined.") in match a with | Equiv v -> repr g v @@ -354,13 +356,15 @@ let get_new_edges g to_merge = UMap.empty to_merge in let ltle = - UMap.fold (fun _ n acc -> - UMap.merge (fun _ strict1 strict2 -> - match strict1, strict2 with - | Some true, _ | _, Some true -> Some true - | _, _ -> Some false) - acc n.ltle) - to_merge_lvl UMap.empty + let fold _ n acc = + let fold u strict acc = + if strict then UMap.add u strict acc + else if UMap.mem u acc then acc + else UMap.add u false acc + in + UMap.fold fold n.ltle acc + in + UMap.fold fold to_merge_lvl UMap.empty in let ltle, _ = clean_ltle g ltle in let ltle = @@ -738,6 +742,45 @@ let check_constraint g (l,d,r) = let check_constraints c g = Constraint.for_all (check_constraint g) c +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 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 + (* Normalization *) (** [normalize_universes g] returns a graph where all edges point @@ -828,6 +871,18 @@ let sort_universes g = in normalize_universes g +(** Subtyping of polymorphic contexts *) + +let check_subtype 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 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 = @@ -876,23 +931,24 @@ let dump_universes output g = let merge_constraints = if Flags.profile then - let key = Profile.declare_profile "merge_constraints" in - Profile.profile2 key merge_constraints + 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 = Profile.declare_profile "check_constraints" in - Profile.profile2 key check_constraints + 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 = Profile.declare_profile "check_eq" in - Profile.profile3 check_eq_key check_eq + 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 = Profile.declare_profile "check_leq" in - Profile.profile3 check_leq_key check_leq + let check_leq_key = CProfile.declare_profile "check_leq" in + CProfile.profile3 check_leq_key check_leq else check_leq + |