From dab5c4c642ee9b25d488c476d55db232cf74006b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 30 Jun 2015 15:43:14 +0200
Subject: Further simplification of the graph traversal in Univ.

We passed the arc to be marked as visited to the functions pushing the
neighbours on the remaining stack, but this can be actually done before
pushing them, as the [process_le] and [process_lt] functions do not rely
on the visited flag. This exposes more clearly the invariants of the
algorithm.
---
 kernel/univ.ml | 25 ++++++++++++-------------
 1 file changed, 12 insertions(+), 13 deletions(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index fce9e28d36..1d82be63b9 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -925,7 +925,8 @@ let fast_compare_neq strict g arcu arcv =
     if arc_is_lt arc then
       cmp c to_revert lt_todo le_todo
     else
-      process_lt c to_revert lt_todo le_todo arc arc.lt arc.le
+      let () = arc.status <- SetLt in
+      process_lt c (arc :: to_revert) lt_todo le_todo arc.lt arc.le
   | [], arc::le_todo ->
     if arc == arcv then
       (* No need to continue inspecting universes above arc:
@@ -937,40 +938,38 @@ let fast_compare_neq strict g arcu arcv =
       if arc_is_le arc then
         cmp c to_revert [] le_todo
       else
-        process_le c to_revert [] le_todo arc arc.lt
+        let () = arc.status <- SetLe in
+        process_le c (arc :: to_revert) [] le_todo arc.lt arc.le
 
-  and process_lt c to_revert lt_todo le_todo arc0 lt le = match le with
+  and process_lt c to_revert lt_todo le_todo lt le = match le with
   | [] ->
     begin match lt with
-    | [] ->
-      let () = arc0.status <- SetLt in
-      cmp c (arc0 :: to_revert) lt_todo le_todo
+    | [] -> cmp c to_revert lt_todo le_todo
     | u :: lt ->
       let arc = repr g u in
       if arc == arcv then
         if strict then (to_revert, FastLT) else (to_revert, FastLE)
-      else process_lt c to_revert (arc :: lt_todo) le_todo arc0 lt le
+      else process_lt c to_revert (arc :: lt_todo) le_todo lt le
     end
   | u :: le ->
     let arc = repr g u in
     if arc == arcv then
       if strict then (to_revert, FastLT) else (to_revert, FastLE)
-    else process_lt c to_revert (arc :: lt_todo) le_todo arc0 lt le
+    else process_lt c to_revert (arc :: lt_todo) le_todo lt le
 
-  and process_le c to_revert lt_todo le_todo arc0 lt = match lt with
+  and process_le c to_revert lt_todo le_todo lt le = match lt with
   | [] ->
     let fold accu u =
       let node = repr g u in
       node :: accu
     in
-    let le_new = List.fold_left fold le_todo arc0.le in
-    let () = arc0.status <- SetLe in
-    cmp c (arc0 :: to_revert) lt_todo le_new
+    let le_new = List.fold_left fold le_todo le in
+    cmp c to_revert lt_todo le_new
   | u :: lt ->
     let arc = repr g u in
     if arc == arcv then
       if strict then (to_revert, FastLT) else (to_revert, FastLE)
-    else process_le c to_revert (arc :: lt_todo) le_todo arc0 lt
+    else process_le c to_revert (arc :: lt_todo) le_todo lt le
 
   in
 
-- 
cgit v1.2.3


From a9665989a93014355ab152920c0a0e58cf0a7dfe Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 1 Jul 2015 12:39:57 +0200
Subject: Display functions for primitive projections.

---
 kernel/names.ml  | 4 ++++
 kernel/names.mli | 4 ++++
 2 files changed, 8 insertions(+)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index 480b37e897..f217c932cc 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -819,6 +819,10 @@ struct
   let map f (c, b as x) =
     let c' = f c in
       if c' == c then x else (c', b)
+
+  let to_string p = Constant.to_string (constant p)
+  let print p = Constant.print (constant p)
+
 end
 
 type projection = Projection.t
diff --git a/kernel/names.mli b/kernel/names.mli
index 92ee58f260..7cc4443752 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -652,6 +652,10 @@ module Projection : sig
   val compare : t -> t -> int
     
   val map : (constant -> constant) -> t -> t
+
+  val to_string : t -> string
+  val print : t -> Pp.std_ppcmds
+
 end
 
 type projection = Projection.t
-- 
cgit v1.2.3


From 44f45f58dc0a169286c9fcfa7d2edbc8bc04673b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 2 Jul 2015 15:39:12 +0200
Subject: More robust pattern matching on structured constants in VM.

---
 kernel/csymtable.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index b29f06c652..49ab68beae 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -57,11 +57,14 @@ let set_global v =
 
 let rec eq_structured_constant c1 c2 = match c1, c2 with
 | Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2
+| Const_sorts _, _ -> false
 | Const_ind i1, Const_ind i2 -> Univ.eq_puniverses eq_ind i1 i2
+| Const_ind _, _ -> false
 | Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
+| Const_b0 _, _ -> false
 | Const_bn (t1, a1), Const_bn (t2, a2) ->
   Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2
-| _ -> false
+| Const_bn _, _ -> false
 
 let rec hash_structured_constant c =
   let open Hashset.Combine in
-- 
cgit v1.2.3