From 17559d528cf7ff92a089d1b966c500424ba45099 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 18 Nov 2016 13:24:39 +0100
Subject: Slightly more efficient [Univ.super] implem

---
 kernel/univ.ml | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 9224ec48d7..c863fac0eb 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -471,12 +471,17 @@ struct
 	
     let super (u,n as x) (v,n' as y) =
       let cmp = Level.compare u v in
-	if Int.equal cmp 0 then 
-	  if n < n' then Inl true
-	  else Inl false
-	else if is_prop x then Inl true
-	else if is_prop y then Inl false
-	else Inr cmp
+	if Int.equal cmp 0 then Inl (n < n')
+	else
+	  match x, y with
+	  | (l,0), (l',0) ->
+	     let open RawLevel in
+	     (match Level.data l, Level.data l' with
+	      | Prop, Prop -> Inl false
+	      | Prop, _ -> Inl true
+	      | _, Prop -> Inl false
+	      | _, _ -> Inr cmp)
+	  | _, _ -> Inr cmp
 
     let to_string (v, n) =
       if Int.equal n 0 then Level.to_string v
-- 
cgit v1.2.3


From 25c82d55497db43bf2cd131f10d2ef366758bbe1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 18 Nov 2016 13:25:05 +0100
Subject: Fix UGraph.check_eq!

Universes are kept in normal form w.r.t. equality but not the <=
relation, so the previous check worked almost always but was actually
too strict! In cases like (max(Set,u) = u) when u is declared >= Set it
was failing to find an equality. Applying the KISS principle:
u = v <-> u <= v /\ v <= u.

Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of
a colon in a typing judgment), this was not the case when an algebraic
universe instantiated an evar that appeared in the term. We force their
universe variable status to change in refresh_universes to avoid this.

Fix ind sort inference: Use syntactic universe equality for inductive
sort inference instead of check_leq (which now correctly takes
constraints into account) and simplify code
---
 kernel/uGraph.ml | 21 +++++++--------------
 1 file changed, 7 insertions(+), 14 deletions(-)

(limited to 'kernel')

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index e2712615be..4884d0deb1 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -638,19 +638,6 @@ let check_smaller g strict u v =
 
 type 'a check_function = universes -> 'a -> 'a -> bool
 
-let check_equal_expr g x y =
-  x == y || (let (u, n) = x and (v, m) = y in 
-               Int.equal n m && check_equal g u v)
-
-let check_eq_univs g l1 l2 =
-  let f x1 x2 = check_equal_expr g x1 x2 in
-  let exists x1 l = Universe.exists (fun x2 -> f x1 x2) l in
-    Universe.for_all (fun x1 -> exists x1 l2) l1
-    && Universe.for_all (fun x2 -> exists x2 l1) l2
-
-let check_eq g u v =
-  Universe.equal u v || check_eq_univs g u v
-
 let check_smaller_expr g (u,n) (v,m) =
   let diff = n - m in
     match diff with
@@ -669,7 +656,13 @@ let real_check_leq g u v =
 let check_leq g u v =
   Universe.equal u v ||
     is_type0m_univ u ||
-    check_eq_univs g u v || real_check_leq g u v
+    real_check_leq g u v
+
+let check_eq_univs g l1 l2 =
+  real_check_leq g l1 l2 && real_check_leq g l2 l1
+
+let check_eq g u v =
+  Universe.equal u v || check_eq_univs g u v
 
 (* enforce_univ_eq g u v will force u=v if possible, will fail otherwise *)
 
-- 
cgit v1.2.3


From d06211803146dec998b414d215d4d93190e2001f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 28 Nov 2016 18:36:10 +0100
Subject: Univs: fix bug #5180

In the kernel's generic conversion, backtrack on UniverseInconsistency
for the unfolding heuristic (single backtracking point in reduction).
This exception can be raised in the univ_compare structure to produce
better error messages when the generic conversion function is called
from higher level code in reductionops.ml, which itself is called during
unification in evarconv.ml.
Inside the kernel, the infer and check variants of conversion never
raise UniverseInconsistency though, so this does not change the behavior
of the kernel.
---
 kernel/reduction.ml  | 2 +-
 kernel/reduction.mli | 8 +++++++-
 2 files changed, 8 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 6c664f7918..1ae89347ad 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -316,7 +316,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
       (try
 	 let cuniv = conv_table_key infos fl1 fl2 cuniv in
 	   convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
-       with NotConvertible ->
+       with NotConvertible | Univ.UniverseInconsistency _ ->
            (* else the oracle tells which constant is to be expanded *)
 	 let oracle = CClosure.oracle_of_infos infos in
          let (app1,app2) =
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 9812c45f7b..8a2b2469d6 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -36,7 +36,7 @@ type 'a extended_conversion_function =
 type conv_pb = CONV | CUMUL
 
 type 'a universe_compare = 
-  { (* Might raise NotConvertible *)
+  { (* Might raise NotConvertible or UnivInconsistency *)
     compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
     compare_instances: flex:bool -> 
 		       Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
@@ -56,9 +56,12 @@ constructors. *)
 val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t ->
   'a * 'a universe_compare -> 'a * 'a universe_compare
 
+(** These two never raise UnivInconsistency, inferred_universes
+    just gathers the constraints. *)
 val checked_universes : UGraph.t universe_compare
 val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare
 
+(** These two functions can only raise NotConvertible *)
 val conv : constr extended_conversion_function
 
 val conv_leq : types extended_conversion_function
@@ -70,6 +73,9 @@ val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) ->
 val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> 
   ?ts:Names.transparent_state -> types infer_conversion_function
 
+(** Depending on the universe state functions, this might raise
+  [UniverseInconsistency] in addition to [NotConvertible] (for better error
+  messages). *)
 val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) ->
   Names.transparent_state -> (constr,'a) generic_conversion_function
 
-- 
cgit v1.2.3


From 0ea7bdc2e315da9a0a8338e5099dfcaad0bac9ef Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 2 Dec 2016 15:48:30 +0100
Subject: Fix #5242 - Dubious unsilenceable warning on invalid identifier

We make this warning configurable and disabled by default.
---
 kernel/names.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index 9267a64d61..1eb9a31751 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -34,9 +34,15 @@ struct
 
   let hash = String.hash
 
+  let warn_invalid_identifier =
+    CWarnings.create ~name:"invalid-identifier" ~category:"parsing"
+                     ~default:CWarnings.Disabled
+                     (fun s -> str s)
+
   let check_soft ?(warn = true) x =
     let iter (fatal, x) =
-      if fatal then CErrors.error x else if warn then Feedback.msg_warning (str x)
+      if fatal then CErrors.error x else
+        if warn then warn_invalid_identifier x
     in
     Option.iter iter (Unicode.ident_refutation x)
 
-- 
cgit v1.2.3


From b8c0f76e507dc0c5dbae3ea7a89d78f16b4a7acb Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 2 Dec 2016 18:00:18 +0100
Subject: Document changes

---
 kernel/univ.ml | 54 ++++++++++++++++++++++++++++++++++--------------------
 1 file changed, 34 insertions(+), 20 deletions(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index c863fac0eb..09f884ecd0 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -468,20 +468,32 @@ struct
       else if Level.is_prop u then
 	hcons (Level.set,n+k)
       else hcons (u,n+k)
-	
+
+    type super_result =
+	SuperSame of bool
+        (* The level expressions are in cumulativity relation. boolean
+           indicates if left is smaller than right?  *)
+      | SuperDiff of int
+        (* The level expressions are unrelated, the comparison result
+           is canonical *)
+
+    (** [super u v] compares two level expressions,
+       returning [SuperSame] if they refer to the same level at potentially different
+       increments or [SuperDiff] if they are different. The booleans indicate if the
+       left expression is "smaller" than the right one in both cases. *)
     let super (u,n as x) (v,n' as y) =
       let cmp = Level.compare u v in
-	if Int.equal cmp 0 then Inl (n < n')
+	if Int.equal cmp 0 then SuperSame (n < n')
 	else
 	  match x, y with
 	  | (l,0), (l',0) ->
 	     let open RawLevel in
 	     (match Level.data l, Level.data l' with
-	      | Prop, Prop -> Inl false
-	      | Prop, _ -> Inl true
-	      | _, Prop -> Inl false
-	      | _, _ -> Inr cmp)
-	  | _, _ -> Inr cmp
+	      | Prop, Prop -> SuperSame false
+	      | Prop, _ -> SuperSame true
+	      | _, Prop -> SuperSame false
+	      | _, _ -> SuperDiff cmp)
+	  | _, _ -> SuperDiff cmp
 
     let to_string (v, n) =
       if Int.equal n 0 then Level.to_string v
@@ -603,24 +615,26 @@ struct
     | Nil, _ -> l2
     | _, Nil -> l1
     | Cons (h1, _, t1), Cons (h2, _, t2) ->
-      (match Expr.super h1 h2 with
-      | Inl true (* h1 < h2 *) -> merge_univs t1 l2
-      | Inl false -> merge_univs l1 t2
-      | Inr c -> 
-        if c <= 0 (* h1 < h2 is name order *)
-	then cons h1 (merge_univs t1 l2)
-	else cons h2 (merge_univs l1 t2))
+       let open Expr in
+       (match super h1 h2 with
+	| SuperSame true (* h1 < h2 *) -> merge_univs t1 l2
+	| SuperSame false -> merge_univs l1 t2
+	| SuperDiff c ->
+           if c <= 0 (* h1 < h2 is name order *)
+	   then cons h1 (merge_univs t1 l2)
+	   else cons h2 (merge_univs l1 t2))
 
   let sort u =
     let rec aux a l = 
       match l with
       | Cons (b, _, l') ->
-        (match Expr.super a b with
-	| Inl false -> aux a l'
-	| Inl true -> l
-	| Inr c ->
-	  if c <= 0 then cons a l
-	  else cons b (aux a l'))
+	let open Expr in
+        (match super a b with
+	 | SuperSame false -> aux a l'
+	 | SuperSame true -> l
+	 | SuperDiff c ->
+	    if c <= 0 then cons a l
+	    else cons b (aux a l'))
       | Nil -> cons a l
     in 
       fold (fun a acc -> aux a acc) u nil
-- 
cgit v1.2.3


From 40cffd816b7adbf8f136f62f6f891fb5be9b96a6 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 6 Dec 2016 16:56:42 +0100
Subject: Fix #5248 - test-suite fails in 8.6beta1

This was yet another bug in the VM long multiplication, that
I unfortunately introduced in ebc509ed2. It was impacting only 32-bit
architectures.

In the future, I'll try to make sure that
1) we provide unit tests for integer arithmetic (my int63 branch ships
   with such tests)
2) our continuous testing infrastructure runs the test suite on a 32-bit
   architecture. I tried to set up such an instance, but failed. Waiting
   for support reply.
---
 kernel/byterun/coq_interp.c | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 47df22807f..5dec3b785c 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -23,9 +23,9 @@
 #include "coq_values.h" 
 
 /* spiwack: I append here a few macros for value/number manipulation */
-#define uint32_of_value(val) ((uint32_t)(val) >> 1)
-#define value_of_uint32(i)   ((value)(((uint32_t)(i) << 1) | 1))
-#define UI64_of_uint32(lo) ((uint64_t)(lo))
+#define uint32_of_value(val) (((uint32_t)(val)) >> 1)
+#define value_of_uint32(i)   ((value)((((uint32_t)(i)) << 1) | 1))
+#define UI64_of_uint32(lo) ((uint64_t)((uint32_t)(lo)))
 #define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val)))
 /* /spiwack */
 
-- 
cgit v1.2.3