From ca4b15c2ba733bdff783762bbfc4b53f88014320 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 20 May 2019 11:30:36 +0200
Subject: Remove a useless call to the Future API for opaque proofs in the STM.

We know statically that the check function producing this forces its
argument, so there is no point in chaining futures lazily.
---
 stm/stm.ml | 29 +++++++++++++++--------------
 1 file changed, 15 insertions(+), 14 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index d469994f3f..9e9d23ba93 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1837,22 +1837,23 @@ end = struct (* {{{ *)
         let o = match c.Declarations.const_body with
           | Declarations.OpaqueDef o -> o
           | _ -> assert false in
-        let uc =
-          Option.get
-            (Opaqueproof.get_constraints (Global.opaque_tables ()) o) in
+        (* No need to delay the computation, the future has been forced by
+           the call to [check_task_aux] above. *)
+        let uc = Opaqueproof.force_constraints (Global.opaque_tables ()) o in
+        let uc = Univ.hcons_universe_context_set uc in
         (* We only manipulate monomorphic terms here. *)
         let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in
-        let pr =
-          Future.from_val (map (Option.get (Global.body_of_constant_body c))) in
-        let uc =
-          Future.chain uc Univ.hcons_universe_context_set in
-        let pr = Future.chain pr discharge in
-        let pr = Future.chain pr Constr.hcons in
-        Future.sink pr;
-        let extra = Future.join uc in
-        u.(bucket) <- uc;
-        p.(bucket) <- pr;
-        u, Univ.ContextSet.union cst extra, false
+        let pr = map (Option.get (Global.body_of_constant_body c)) in
+        let pr = discharge pr in
+        let pr = Constr.hcons pr in
+        let return c =
+          let fc = Future.from_val c in
+          let _ = Future.join fc in
+          fc
+        in
+        u.(bucket) <- return uc;
+        p.(bucket) <- return pr;
+        u, Univ.ContextSet.union cst uc, false
 
   let check_task name l i =
     match check_task_aux "" name l i with
-- 
cgit v1.2.3


From b245a6c46bc3ef70142e8a165f6cde54265b941e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 20 May 2019 11:51:31 +0200
Subject: Statically ensure the content of delayed proofs in vio file.

Before, we would store futures, but it was actually ensured by the
upper layers that they were either evaluated or stored by the STM
somewhere else. We simply replace this type with an option, thus
removing the Future.computation type from vo/vio files.

This also enhances debug printing, as the latter is unable to properly
print futures.
---
 stm/stm.ml | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 9e9d23ba93..30cf8a0622 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1846,13 +1846,8 @@ end = struct (* {{{ *)
         let pr = map (Option.get (Global.body_of_constant_body c)) in
         let pr = discharge pr in
         let pr = Constr.hcons pr in
-        let return c =
-          let fc = Future.from_val c in
-          let _ = Future.join fc in
-          fc
-        in
-        u.(bucket) <- return uc;
-        p.(bucket) <- return pr;
+        u.(bucket) <- Some uc;
+        p.(bucket) <- Some pr;
         u, Univ.ContextSet.union cst uc, false
 
   let check_task name l i =
-- 
cgit v1.2.3


From d3c931cd8c84d1b7d9d5763e20221d51700f0709 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 21 May 2019 19:22:30 +0200
Subject: Remove the indirect opaque accessor hooks from Opaqueproof.

We simply pass them as arguments, now that they are not called by the
kernel anymore.

The checker definitely needs to access the opaque proofs. In order not to
touch the API at all, I added a hook there, but it could also be provided
as an additional argument, at the cost of changing all the upwards callers.
---
 stm/stm.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 30cf8a0622..660dc27211 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1839,11 +1839,11 @@ end = struct (* {{{ *)
           | _ -> assert false in
         (* No need to delay the computation, the future has been forced by
            the call to [check_task_aux] above. *)
-        let uc = Opaqueproof.force_constraints (Global.opaque_tables ()) o in
+        let uc = Opaqueproof.force_constraints Library.indirect_accessor (Global.opaque_tables ()) o in
         let uc = Univ.hcons_universe_context_set uc in
         (* We only manipulate monomorphic terms here. *)
         let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in
-        let pr = map (Option.get (Global.body_of_constant_body c)) in
+        let pr = map (Option.get (Global.body_of_constant_body Library.indirect_accessor c)) in
         let pr = discharge pr in
         let pr = Constr.hcons pr in
         u.(bucket) <- Some uc;
-- 
cgit v1.2.3