From a2ea73d84be2fe95eeda42f5f5ac458f0af9968f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 24 Feb 2019 01:57:59 +0100
Subject: [proofs] Store hooks in the proof object.

As of now, hooks were stored in the terminators as closures, we place
them instead in the proof object and are thus passed back at proof
closing time.

This helps towards the reification and unification of terminators.
---
 plugins/derive/derive.ml |  4 +--
 stm/stm.ml               | 11 ++++----
 vernac/lemmas.ml         | 70 ++++++++++++++++++++++++++++--------------------
 vernac/lemmas.mli        | 27 ++++++++++++-------
 vernac/obligations.ml    | 12 ++++-----
 vernac/vernacentries.mli |  2 +-
 vernac/vernacstate.ml    |  6 ++---
 vernac/vernacstate.mli   |  2 +-
 8 files changed, 77 insertions(+), 57 deletions(-)

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index aad3967f6d..f8b5f455d1 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -56,9 +56,9 @@ let start_deriving f suchthat name : Lemmas.t =
       let (opaque,f_def,lemma_def) =
         match com with
         | Lemmas.Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.")
-        | Lemmas.Proved (_,Some _,_) ->
+        | Lemmas.Proved (_,Some _,_, _) ->
             CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.")
-        | Lemmas.Proved (opaque, None, obj) ->
+        | Lemmas.Proved (opaque, None, obj,_) ->
             match Proof_global.(obj.entries) with
             | [_;f_def;lemma_def] ->
                 opaque <> Proof_global.Transparent , f_def , lemma_def
diff --git a/stm/stm.ml b/stm/stm.ml
index d77e37c910..a0247e0d8f 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1532,14 +1532,15 @@ end = struct (* {{{ *)
           (* Unfortunately close_future_proof and friends are not pure so we need
              to set the state manually here *)
           State.unfreeze st;
-          let pobject, _ =
+          let pobject, _terminator, _hook =
             PG_compat.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in
+
           let terminator = (* The one sent by master is an InvalidKey *)
             Lemmas.(standard_proof_terminator []) in
 
           let st = Vernacstate.freeze_interp_state ~marshallable:false in
           stm_vernac_interp stop
-            ~proof:(pobject, terminator) st
+            ~proof:(pobject, terminator, None) st
             { verbose = false; indentation = 0; strlen = 0;
               expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in
         ignore(Future.join checked_proof);
@@ -1676,10 +1677,10 @@ end = struct (* {{{ *)
       let opaque = Proof_global.Opaque in
 
       (* The original terminator, a hook, has not been saved in the .vio*)
-      let pterm, _invalid_terminator =
+      let pterm, _invalid_terminator, _hook =
         PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
 
-      let proof = pterm , Lemmas.standard_proof_terminator [] in
+      let proof = pterm , Lemmas.standard_proof_terminator [], None in
 
       (* We jump at the beginning since the kernel handles side effects by also
        * looking at the ones that happen to be present in the current env *)
@@ -1734,7 +1735,7 @@ end = struct (* {{{ *)
     | `ERROR -> exit 1
     | `ERROR_ADMITTED -> cst, false
     | `OK_ADMITTED -> cst, false
-    | `OK (po,_) ->
+    | `OK (po,_,_) ->
         let con =
           Nametab.locate_constant
             (Libnames.qualid_of_ident po.Proof_global.id) in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 7aba64fb93..695da1fcee 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -34,12 +34,12 @@ module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit
-type declaration_hook = hook_type
+type declaration_hook = hook_type CEphemeron.key
 
-let mk_hook hook = hook
+let mk_hook hook = CEphemeron.create hook
 
 let call_hook ?hook ?fix_exn uctx trans l c =
-  try Option.iter (fun hook -> hook uctx trans l c) hook
+  try Option.iter (fun hook -> CEphemeron.get hook uctx trans l c) hook
   with e when CErrors.noncritical e ->
     let e = CErrors.push e in
     let e = Option.cata (fun fix -> fix e) e fix_exn in
@@ -49,10 +49,18 @@ let call_hook ?hook ?fix_exn uctx trans l c =
    [that can be saved] *)
 
 type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
-  | Proved of Proof_global.opacity_flag *
-              lident option *
-              Proof_global.proof_object
+  | Admitted of
+      Names.Id.t *
+      Decl_kinds.goal_kind *
+      Entries.parameter_entry *
+      UState.t *
+      declaration_hook option
+
+  | Proved of
+      Proof_global.opacity_flag *
+      lident option *
+      Proof_global.proof_object *
+      declaration_hook option
 
 type proof_terminator = (proof_ending -> unit) CEphemeron.key
 
@@ -60,9 +68,10 @@ type proof_terminator = (proof_ending -> unit) CEphemeron.key
 type t =
   { proof : Proof_global.t
   ; terminator : proof_terminator
+  ; hook : declaration_hook option
   }
 
-let pf_map f { proof; terminator} = { proof = f proof; terminator }
+let pf_map f { proof; terminator; hook } = { proof = f proof; terminator; hook }
 let pf_fold f ps = f ps.proof
 
 let set_endline_tactic t = pf_map (Proof_global.set_endline_tactic t)
@@ -76,12 +85,13 @@ let apply_terminator f = CEphemeron.get f
 (** Gets the current terminator without checking that the proof has
     been completed. Useful for the likes of [Admitted]. *)
 let get_terminator ps = ps.terminator
+let get_hook ps = ps.hook
 
 end
 
-let by tac { proof; terminator } =
+let by tac { proof; terminator; hook } =
   let proof, res = Pfedit.by tac proof in
-  { proof; terminator}, res
+  { proof; terminator; hook}, res
 
 (* Support for mutually proved theorems *)
 
@@ -316,13 +326,13 @@ let admit ?hook ctx (id,k,e) pl () =
 
 (* Starting a goal *)
 
-let standard_proof_terminator ?(hook : declaration_hook option) compute_guard =
+let standard_proof_terminator compute_guard =
   let open Proof_global in
-  CEphemeron.create begin function
-  | Admitted (id,k,pe,ctx) ->
+  Internal.make_terminator begin function
+  | Admitted (id,k,pe,ctx,hook) ->
     let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in
     Feedback.feedback Feedback.AddedAxiom
-  | Proved (opaque,idopt, { id; entries=[const]; persistence; universes } ) ->
+  | Proved (opaque,idopt, { id; entries=[const]; persistence; universes }, hook ) ->
     let is_opaque, export_seff = match opaque with
       | Transparent -> false, true
       | Opaque      -> true, false
@@ -333,7 +343,7 @@ let standard_proof_terminator ?(hook : declaration_hook option) compute_guard =
       | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
     let () = save ~export_seff id const universes compute_guard persistence hook universes in
     ()
-  | Proved (opaque,idopt, _ ) ->
+  | Proved (opaque,idopt, _, hook) ->
     CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term")
   end
 
@@ -381,8 +391,8 @@ end
 
 let start_lemma id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c =
   let terminator = match terminator with
-  | None -> standard_proof_terminator ?hook compute_guard
-  | Some terminator -> terminator ?hook compute_guard
+  | None -> standard_proof_terminator compute_guard
+  | Some terminator -> terminator compute_guard
   in
   let sign =
     match sign with
@@ -391,15 +401,15 @@ let start_lemma id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c
   in
   let goals = [ Global.env_of_context sign , c ] in
   let proof = Proof_global.start_proof sigma id ?pl kind goals in
-  { proof ; terminator }
+  { proof ; terminator; hook }
 
 let start_dependent_lemma id ?pl kind ?terminator ?sign ?(compute_guard=[]) ?hook telescope =
   let terminator = match terminator with
-  | None -> standard_proof_terminator ?hook compute_guard
-  | Some terminator -> terminator ?hook compute_guard
+  | None -> standard_proof_terminator compute_guard
+  | Some terminator -> terminator compute_guard
   in
   let proof = Proof_global.start_dependent_proof id ?pl kind telescope in
-  { proof ; terminator }
+  { proof ; terminator; hook }
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
@@ -447,6 +457,7 @@ let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl =
         List.iter (fun (ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
           call_hook ?hook ctx [] strength ref) thms_data in
+      let hook = mk_hook hook in
       let lemma = start_lemma id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
       let lemma = pf_map (Proof_global.map_proof (fun p ->
           match init_tac with
@@ -505,7 +516,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
   let pe =
     let open Proof_global in
     match proof with
-    | Some ({ id; entries; persistence = k; universes }, _) ->
+    | Some ({ id; entries; persistence = k; universes }, _, hook) ->
       if List.length entries <> 1 then
         user_err Pp.(str "Admitted does not support multiple statements");
       let { const_entry_secctx; const_entry_type } = List.hd entries in
@@ -514,7 +525,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
       let typ = Option.get const_entry_type in
       let ctx = UState.univ_entry ~poly:(pi2 k) universes in
       let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
-      Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
+      Admitted(id, k, (sec_vars, (typ, ctx), None), universes, hook)
     | None ->
       let pftree = Proof_global.get_proof lemma.proof in
       let gk = Proof_global.get_persistence lemma.proof in
@@ -542,7 +553,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
           | _ -> None in
       let decl = Proof_global.get_universe_decl lemma.proof in
       let ctx = UState.check_univ_decl ~poly universes decl in
-      Admitted(name,gk,(sec_vars, (typ, ctx), None), universes)
+      Admitted(name,gk,(sec_vars, (typ, ctx), None), universes, lemma.hook)
   in
   CEphemeron.get lemma.terminator pe
 
@@ -550,13 +561,14 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt =
   (* Invariant (uh) *)
   if Option.is_empty lemma && Option.is_empty proof then
     user_err (str "No focused proof (No proof-editing in progress).");
-  let (proof_obj,terminator) =
+  let proof_obj,terminator, hook =
     match proof with
     | None ->
       (* XXX: The close_proof and proof state API should be refactored
          so it is possible to insert proofs properly into the state *)
-      let { proof; terminator } = Option.get lemma in
-      Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, terminator
-    | Some proof -> proof
+      let { proof; terminator; hook } = Option.get lemma in
+      Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, terminator, hook
+    | Some (proof, terminator, hook) ->
+      proof, terminator, hook
   in
-  CEphemeron.get terminator (Proved (opaque,idopt,proof_obj))
+  CEphemeron.get terminator (Proved (opaque,idopt,proof_obj,hook))
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 25c5b24e91..03cd45b8bf 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -65,8 +65,7 @@ module Stack : sig
 end
 
 val standard_proof_terminator
-  :  ?hook:declaration_hook
-  -> Proof_global.lemma_possible_guards
+  :  Proof_global.lemma_possible_guards
   -> proof_terminator
 
 val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
@@ -82,7 +81,7 @@ val start_lemma
   -> ?pl:UState.universe_decl
   -> goal_kind
   -> Evd.evar_map
-  -> ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> proof_terminator)
+  -> ?terminator:(Proof_global.lemma_possible_guards -> proof_terminator)
   -> ?sign:Environ.named_context_val
   -> ?compute_guard:Proof_global.lemma_possible_guards
   -> ?hook:declaration_hook
@@ -93,7 +92,7 @@ val start_dependent_lemma
   :  Id.t
   -> ?pl:UState.universe_decl
   -> goal_kind
-  -> ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> proof_terminator)
+  -> ?terminator:(Proof_global.lemma_possible_guards -> proof_terminator)
   -> ?sign:Environ.named_context_val
   -> ?compute_guard:Proof_global.lemma_possible_guards
   -> ?hook:declaration_hook
@@ -126,12 +125,12 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val
 (** {6 Saving proofs } *)
 
 val save_lemma_admitted
-  :  ?proof:(Proof_global.proof_object * proof_terminator)
+  :  ?proof:(Proof_global.proof_object * proof_terminator * declaration_hook option)
   -> lemma:t
   -> unit
 
 val save_lemma_proved
-  :  ?proof:(Proof_global.proof_object * proof_terminator)
+  :  ?proof:(Proof_global.proof_object * proof_terminator * declaration_hook option)
   -> ?lemma:t
   -> opaque:Proof_global.opacity_flag
   -> idopt:Names.lident option
@@ -139,16 +138,24 @@ val save_lemma_proved
 
 (* API to build a terminator, should go away *)
 type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
-  | Proved of Proof_global.opacity_flag *
-              Names.lident option *
-              Proof_global.proof_object
+  | Admitted of
+      Names.Id.t *
+      Decl_kinds.goal_kind *
+      Entries.parameter_entry *
+      UState.t *
+      declaration_hook option
+  | Proved of
+      Proof_global.opacity_flag *
+      lident option *
+      Proof_global.proof_object *
+      declaration_hook option
 
 (** This stuff is internal and will be removed in the future.  *)
 module Internal : sig
 
   (** Only needed due to the Proof_global compatibility layer. *)
   val get_terminator : t -> proof_terminator
+  val get_hook : t -> declaration_hook option
 
   (** Only needed by obligations, should be reified soon *)
   val make_terminator : (proof_ending -> unit) -> proof_terminator
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 6ef2f80067..4a564e705e 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -839,13 +839,13 @@ let solve_by_tac ?loc name evi t poly ctx =
     warn_solve_errored ?loc err;
     None
 
-let obligation_terminator ?hook name num guard auto pf =
+let obligation_terminator name num guard auto pf =
   let open Proof_global in
   let open Lemmas in
-  let term = standard_proof_terminator ?hook guard in
+  let term = standard_proof_terminator guard in
   match pf with
   | Admitted _ -> Internal.apply_terminator term pf
-  | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin
+  | Proved (opq, id, { entries=[entry]; universes=uctx }, hook ) -> begin
     let env = Global.env () in
     let ty = entry.Entries.const_entry_type in
     let body, eff = Future.force entry.const_entry_body in
@@ -905,7 +905,7 @@ let obligation_terminator ?hook name num guard auto pf =
       let e = CErrors.push e in
       pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
   end
-  | Proved (_, _, _ ) ->
+  | Proved (_, _, _,_ ) ->
     CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term")
 
 let obligation_hook prg obl num auto ctx' _ _ gr =
@@ -964,9 +964,9 @@ let rec solve_obligation prg num tac =
   let evd = Evd.from_ctx prg.prg_ctx in
   let evd = Evd.update_sigma_env evd (Global.env ()) in
   let auto n tac oblset = auto_solve_obligations n ~oblset tac in
-  let terminator ?hook guard =
+  let terminator guard =
     Lemmas.Internal.make_terminator
-      (obligation_terminator prg.prg_name num guard ?hook auto) in
+      (obligation_terminator prg.prg_name num guard auto) in
   let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in
   let lemma = Lemmas.start_lemma ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in
   let lemma = fst @@ Lemmas.by !default_tactic lemma in
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index f1c8b29313..8d1d9abc0b 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -22,7 +22,7 @@ val vernac_require :
 (** The main interpretation function of vernacular expressions *)
 val interp :
   ?verbosely:bool ->
-  ?proof:(Proof_global.proof_object * Lemmas.proof_terminator) ->
+  ?proof:(Proof_global.proof_object * Lemmas.proof_terminator * Lemmas.declaration_hook option) ->
   st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t
 
 (** Prepare a "match" template for a given inductive type.
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index c51d3c30f4..0cdf748ce9 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -131,18 +131,18 @@ module Proof_global = struct
       s_lemmas := Some stack;
       res
 
-  type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator
+  type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator * Lemmas.declaration_hook option
 
 
   let return_proof ?allow_partial () = cc (return_proof ?allow_partial)
 
   let close_future_proof ~opaque ~feedback_id pf =
     cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~feedback_id st pf) pt,
-                        Internal.get_terminator pt)
+                        Internal.get_terminator pt, Internal.get_hook pt)
 
   let close_proof ~opaque ~keep_body_ucst_separate f =
     cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate f)) pt,
-                        Internal.get_terminator pt)
+                        Internal.get_terminator pt, Internal.get_hook pt)
 
   let discard_all () = s_lemmas := None
   let update_global_env () = dd (update_global_env)
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 9f4e366e1c..15b8aaefb6 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -51,7 +51,7 @@ module Proof_global : sig
 
   val return_proof : ?allow_partial:bool -> unit -> Proof_global.closed_proof_output
 
-  type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator
+  type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator * Lemmas.declaration_hook option
 
   val close_future_proof :
     opaque:Proof_global.opacity_flag ->
-- 
cgit v1.2.3