From 280be11cb4706e039cf4e9f68a5ae38b0aef9340 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 28 May 2017 00:35:57 +0200
Subject: [stm] Remove state-handling from Futures.

We make Vernacentries.interp functional wrt state, and thus remove
state-handling from `Future`. Now, a future needs a closure if it
wants to preserve state.

Consequently, `Vernacentries.interp` takes a state, and returns the
new one.

We don't explicitly thread the state in the STM yet, instead, we
recover the state that was used before and pass it explicitly to
`interp`.

I have tested the commit with the files in interactive, but we aware
that some new bugs may appear or old ones be made more apparent.
However, I am confident that this step will improve our understanding
of bugs.

In some cases, we perform a bit more summary wrapping/unwrapping. This
will go away in future commits; informal timings for a full make:

- master:
  real	2m11,027s
  user	8m30,904s
  sys	1m0,000s

- no_futures:
  real	2m8,474s
  user	8m34,380s
  sys	0m59,156s
---
 kernel/opaqueproof.ml | 16 ++++++++--------
 kernel/term_typing.ml |  6 +++---
 2 files changed, 11 insertions(+), 11 deletions(-)

(limited to 'kernel')

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 5e20c1b514..400f9feeea 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -78,12 +78,12 @@ let subst_opaque sub = function
 let iter_direct_opaque f = function
   | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
   | Direct (d,cu) ->
-      Direct (d,Future.chain ~pure:true cu (fun (c, u) -> f c; c, u))
+      Direct (d,Future.chain cu (fun (c, u) -> f c; c, u))
 
 let discharge_direct_opaque ~cook_constr ci = function
   | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
   | Direct (d,cu) ->
-      Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u))
+      Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u))
 
 let join_opaque { opaque_val = prfs; opaque_dir = odp } = function
   | Direct (_,cu) -> ignore(Future.join cu)
@@ -105,7 +105,7 @@ let force_proof { opaque_val = prfs; opaque_dir = odp } = function
   | Indirect (l,dp,i) ->
       let pt =
         if DirPath.equal dp odp
-        then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst
+        then Future.chain (snd (Int.Map.find i prfs)) fst
         else !get_opaque dp i in
       let c = Future.force pt in
       force_constr (List.fold_right subst_substituted l (from_val c))
@@ -120,20 +120,20 @@ let force_constraints { opaque_val = prfs; opaque_dir = odp } = function
         | Some u -> Future.force u
 
 let get_constraints { opaque_val = prfs; opaque_dir = odp } = function
-  | Direct (_,cu) -> Some(Future.chain ~pure:true cu snd)
+  | Direct (_,cu) -> Some(Future.chain cu snd)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
-      then Some(Future.chain ~pure:true (snd (Int.Map.find i prfs)) snd)
+      then Some(Future.chain (snd (Int.Map.find i prfs)) snd)
       else !get_univ dp i
 
 let get_proof { opaque_val = prfs; opaque_dir = odp } = function
-  | Direct (_,cu) -> Future.chain ~pure:true cu fst
+  | Direct (_,cu) -> Future.chain cu fst
   | Indirect (l,dp,i) ->
       let pt =
         if DirPath.equal dp odp
-        then Future.chain ~pure:true (snd (Int.Map.find i prfs)) fst
+        then Future.chain (snd (Int.Map.find i prfs)) fst
         else !get_opaque dp i in
-      Future.chain ~pure:true pt (fun c ->
+      Future.chain pt (fun c ->
         force_constr (List.fold_right subst_substituted l (from_val c)))
  
 module FMap = Future.UUIDMap
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 22e109b01c..f93b24b3ee 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -266,7 +266,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
-        Future.chain ~pure:true body (fun ((body,uctx),side_eff) ->
+        Future.chain body (fun ((body,uctx),side_eff) ->
           let j, uctx = match trust with
           | Pure ->
             let env = push_context_set uctx env in
@@ -535,7 +535,7 @@ let export_side_effects mb env ce =
       let { const_entry_body = body } = c in
       let _, eff = Future.force body in
       let ce = DefinitionEntry { c with
-        const_entry_body = Future.chain ~pure:true body
+        const_entry_body = Future.chain body
           (fun (b_ctx, _) -> b_ctx, ()) } in
       let not_exists (c,_,_,_) =
         try ignore(Environ.lookup_constant c env); false
@@ -628,7 +628,7 @@ let translate_local_def mb env id centry =
 let translate_mind env kn mie = Indtypes.check_inductive env kn mie
 
 let inline_entry_side_effects env ce = { ce with
-  const_entry_body = Future.chain ~pure:true
+  const_entry_body = Future.chain
     ce.const_entry_body (fun ((body, ctx), side_eff) ->
       let body, ctx',_ = inline_side_effects env body ctx side_eff in
       (body, ctx'), ());
-- 
cgit v1.2.3