From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 kernel/uGraph.ml | 96 ++++++++++++++++++++++++++++++++++++++++++++------------
 1 file changed, 76 insertions(+), 20 deletions(-)

(limited to 'kernel/uGraph.ml')

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
+
-- 
cgit v1.2.3