From fd3bde66bc32ba70435aaad3f83d0b58c846af55 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 7 Dec 2018 23:15:26 +0100
Subject: [tactics] Remove dependency of abstract on global proof state.

In order to do so we place the polymorphic status and name in the
read-only part of the monad.

Note the added comments, as well as the fact that almost no part of
tactics depends on `proofs` nor `interp`, thus they should be placed
just after pretyping.

Gaëtan Gilbert noted that ideally, abstract should not depend on the
polymorphic status, should we be able to defer closing of the
constant, however this will require significant effort.

Also, we may deprecate nameless abstract, thus rending both of the
changes this PR need unnecessary.
---
 engine/proofview.ml        | 12 ++++++++----
 engine/proofview.mli       | 17 +++++++++++++----
 engine/proofview_monad.ml  |  9 ++++++---
 engine/proofview_monad.mli |  2 +-
 4 files changed, 28 insertions(+), 12 deletions(-)

(limited to 'engine')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index d4ad53ff5f..a725444e81 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -223,9 +223,9 @@ module Proof = Logical
 type +'a tactic = 'a Proof.t
 
 (** Applies a tactic to the current proofview. *)
-let apply env t sp =
+let apply ~name ~poly env t sp =
   let open Logic_monad in
-  let ans = Proof.repr (Proof.run t false (sp,env)) in
+  let ans = Proof.repr (Proof.run t P.{trace=false; name; poly} (sp,env)) in
   let ans = Logic_monad.NonLogical.run ans in
   match ans with
   | Nil (e, info) -> iraise (TacticFailure e, info)
@@ -993,7 +993,10 @@ let tclTIME s t =
         tclOR (tclUNIT x) (fun e -> aux (n+1) (k e))
   in aux 0 t
 
-
+let tclProofInfo =
+  let open Proof in
+  Logical.current >>= fun P.{name; poly} ->
+  tclUNIT (name, poly)
 
 (** {7 Unsafe primitives} *)
 
@@ -1275,7 +1278,8 @@ module V82 = struct
   let of_tactic t gls =
     try
       let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in
-      let (_,final,_,_) = apply (goal_env gls.Evd.sigma gls.Evd.it) t init in
+      let name, poly = Names.Id.of_string "legacy_pe", false in
+      let (_,final,_,_) = apply ~name ~poly (goal_env gls.Evd.sigma gls.Evd.it) t init in
       { Evd.sigma = final.solution ; it = CList.map drop_state final.comb }
     with Logic_monad.TacticFailure e as src ->
       let (_, info) = CErrors.push src in
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 286703c0dc..680a93f0cc 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -156,10 +156,15 @@ type +'a tactic
     tactic has given up. In case of multiple success the first one is
     selected. If there is no success, fails with
     {!Logic_monad.TacticFailure}*)
-val apply : Environ.env -> 'a tactic -> proofview -> 'a
-                                                   * proofview
-                                                   * (bool*Evar.t list*Evar.t list)
-                                                   * Proofview_monad.Info.tree
+val apply
+  :  name:Names.Id.t
+  -> poly:bool
+  -> Environ.env
+  -> 'a tactic
+  -> proofview
+  -> 'a * proofview
+       * (bool*Evar.t list*Evar.t list)
+       * Proofview_monad.Info.tree
 
 (** {7 Monadic primitives} *)
 
@@ -407,6 +412,10 @@ val tclTIMEOUT : int -> 'a tactic -> 'a tactic
     identifying annotation if present *)
 val tclTIME : string option -> 'a tactic -> 'a tactic
 
+(** Internal, don't use. *)
+val tclProofInfo : (Names.Id.t * bool) tactic
+[@@ocaml.deprecated "internal, don't use"]
+
 (** {7 Unsafe primitives} *)
 
 (** The primitives in the [Unsafe] module should be avoided as much as
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 69341d97df..80eb9d0124 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -177,7 +177,7 @@ module P = struct
   type s = proofview * Environ.env
 
   (** Recording info trace (true) or not. *)
-  type e = bool
+  type e = { trace: bool; name : Names.Id.t; poly : bool }
 
   (** Status (safe/unsafe) * shelved goals * given up *)
   type w = bool * goal list
@@ -254,13 +254,16 @@ end
 
 (** Lens and utilies pertaining to the info trace *)
 module InfoL = struct
-  let recording = Logical.current
+  let recording = Logical.(map (fun {P.trace} -> trace) current)
   let if_recording t =
     let open Logical in
     recording >>= fun r ->
     if r then t else return ()
 
-  let record_trace t = Logical.local true t
+  let record_trace t =
+    Logical.(
+      current >>= fun s ->
+      local {s with P.trace = true} t)
 
   let raw_update = Logical.update
   let update f = if_recording (raw_update f)
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index a08cab3bf6..3437b6ce77 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -98,7 +98,7 @@ module P : sig
   val wprod : w -> w -> w
 
   (** Recording info trace (true) or not. *)
-  type e = bool
+  type e = { trace: bool; name : Names.Id.t; poly : bool }
 
   type u = Info.state
 
-- 
cgit v1.2.3