From 7dc04f0244aeb277b62070f87590cbc2cafd8396 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 24 Feb 2019 20:27:09 +0100
Subject: [proof] drop parameter from terminator type

This makes the type of terminator simpler, progressing towards its
total reification.
---
 plugins/derive/derive.ml |  6 ++--
 proofs/proof_global.ml   |  3 --
 proofs/proof_global.mli  |  2 --
 stm/stm.ml               | 13 ++++-----
 vernac/comFixpoint.mli   |  3 +-
 vernac/declareObl.ml     |  8 +++---
 vernac/declareObl.mli    |  3 +-
 vernac/lemmas.ml         | 71 +++++++++++++++++++++++-------------------------
 vernac/lemmas.mli        | 35 +++++++++++++-----------
 vernac/obligations.ml    |  5 ++--
 vernac/vernacentries.mli |  2 +-
 vernac/vernacstate.ml    |  8 +++---
 vernac/vernacstate.mli   |  2 +-
 13 files changed, 76 insertions(+), 85 deletions(-)

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index f8b5f455d1..0f0bec0129 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
@@ -99,7 +99,7 @@ let start_deriving f suchthat name : Lemmas.t =
       ignore (Declare.declare_constant name lemma_def)
   in
 
-  let terminator ?hook _ = Lemmas.Internal.make_terminator terminator in
+  let terminator = Lemmas.Internal.make_terminator terminator in
   let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in
   Lemmas.pf_map (Proof_global.map_proof begin fun p ->
     Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 96d90e9252..a871a3fc95 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -24,9 +24,6 @@ module NamedDecl = Context.Named.Declaration
 
 (*** Proof Global Environment ***)
 
-(* Extra info on proofs. *)
-type lemma_possible_guards = int list list
-
 type proof_object = {
   id : Names.Id.t;
   entries : Evd.side_effects Entries.definition_entry list;
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index f84ec27df7..9c2ada2457 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -31,8 +31,6 @@ val compact_the_proof : t -> t
     function which takes a [proof_object] together with a [proof_end]
     (i.e. an proof ending command) and registers the appropriate
     values. *)
-type lemma_possible_guards = int list list
-
 type proof_object = {
   id : Names.Id.t;
   entries : Evd.side_effects Entries.definition_entry list;
diff --git a/stm/stm.ml b/stm/stm.ml
index 4f435f1fa5..13996aca0f 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1532,15 +1532,12 @@ 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, _terminator, _hook =
+          let pobject, _info =
             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, None) st
+            ~proof:(pobject, Lemmas.default_info) st
             { verbose = false; indentation = 0; strlen = 0;
               expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in
         ignore(Future.join checked_proof);
@@ -1677,10 +1674,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, _hook =
+      let pterm, _info =
         PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
 
-      let proof = pterm , Lemmas.standard_proof_terminator [], None in
+      let proof = pterm, Lemmas.default_info 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 *)
@@ -1735,7 +1732,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/comFixpoint.mli b/vernac/comFixpoint.mli
index 1ded9f3d29..ea9ab33346 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -88,7 +88,8 @@ val declare_fixpoint :
   locality -> polymorphic ->
   recursive_preentry * UState.universe_decl * UState.t *
   (Constr.rel_context * Impargs.manual_implicits * int option) list ->
-  Proof_global.lemma_possible_guards -> decl_notation list -> unit
+  Lemmas.lemma_possible_guards -> decl_notation list ->
+  unit
 
 val declare_cofixpoint :
   locality -> polymorphic ->
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 564e83efd5..2afd056950 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -486,13 +486,13 @@ let dependencies obls n =
     obls;
   !res
 
-let obligation_terminator name num guard auto pf =
+let obligation_terminator name num auto pf =
   let open Proof_global in
   let open Lemmas in
-  let term = standard_proof_terminator guard in
+  let term = Lemmas.standard_proof_terminator in
   match pf with
   | Admitted _ -> Internal.apply_terminator term pf
-  | Proved (opq, id, { entries=[entry]; universes=uctx }, hook ) -> begin
+  | Proved (opq, id, { entries=[entry]; universes=uctx }, hook, compute_guard ) -> begin
     let env = Global.env () in
     let ty = entry.Entries.const_entry_type in
     let body, eff = Future.force entry.const_entry_body in
@@ -552,5 +552,5 @@ let obligation_terminator 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")
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index 3974954870..ab305da3af 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -62,9 +62,8 @@ module ProgMap : CMap.ExtS with type key = Id.t and module Set := Id.Set
 val declare_definition : program_info -> Names.GlobRef.t
 
 val obligation_terminator :
-     ProgMap.key
+     Id.t
   -> int
-  -> Proof_global.lemma_possible_guards
   -> (ProgMap.key option -> 'a option -> Int.Set.t -> 'b)
   -> Lemmas.proof_ending
   -> unit
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index d7e9e83649..0ca273a02d 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -48,6 +48,8 @@ let call_hook ?hook ?fix_exn uctx trans l c =
 (* Support for terminators and proofs with an associated constant
    [that can be saved] *)
 
+type lemma_possible_guards = int list list
+
 type proof_ending =
   | Admitted of
       Names.Id.t *
@@ -60,7 +62,8 @@ type proof_ending =
       Proof_global.opacity_flag *
       lident option *
       Proof_global.proof_object *
-      declaration_hook option
+      declaration_hook option *
+      lemma_possible_guards
 
 type proof_terminator = (proof_ending -> unit) CEphemeron.key
 
@@ -69,10 +72,11 @@ type t =
   { proof : Proof_global.t
   ; terminator : proof_terminator
   ; hook : declaration_hook option
+  ; compute_guard : lemma_possible_guards
   }
 
-let pf_map f { proof; terminator; hook } = { proof = f proof; terminator; hook }
-let pf_fold f ps = f ps.proof
+let pf_map f pf = { pf with proof = f pf.proof }
+let pf_fold f pf = f pf.proof
 
 let set_endline_tactic t = pf_map (Proof_global.set_endline_tactic t)
 
@@ -84,14 +88,14 @@ 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
+let get_info ps = ps.terminator, ps.hook, ps.compute_guard
 
 end
+(* Internal *)
 
-let by tac { proof; terminator; hook } =
-  let proof, res = Pfedit.by tac proof in
-  { proof; terminator; hook}, res
+let by tac pf =
+  let proof, res = Pfedit.by tac pf.proof in
+  { pf with proof }, res
 
 (* Support for mutually proved theorems *)
 
@@ -326,13 +330,13 @@ let admit ?hook ctx (id,k,e) pl () =
 
 (* Starting a goal *)
 
-let standard_proof_terminator compute_guard =
+let standard_proof_terminator =
   let open Proof_global in
   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 }, hook ) ->
+  | Proved (opaque,idopt, { id; entries=[const]; persistence; universes }, hook, compute_guard ) ->
     let is_opaque, export_seff = match opaque with
       | Transparent -> false, true
       | Opaque      -> true, false
@@ -343,7 +347,7 @@ let standard_proof_terminator 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, _, hook) ->
+  | Proved (opaque,idopt, _, hook,_) ->
     CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term")
   end
 
@@ -382,34 +386,22 @@ module Stack = struct
     let (pn, pns) = map Proof.(function pf -> (data (prj pf.proof)).name) pf in
     pn :: pns
 
-  let copy_terminators ~src ~tgt =
+  let copy_info ~src ~tgt =
     let (ps, psl), (ts,tsl) = src, tgt in
     assert(List.length psl = List.length tsl);
-    {ts with terminator = ps.terminator}, List.map2 (fun op p -> { p with terminator = op.terminator }) psl tsl
+    { ps with proof = ts.proof },
+    List.map2 (fun op p -> { op with proof = p.proof }) psl tsl
 
 end
 
-let start_lemma id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c =
-  let terminator = match terminator with
-  | None -> standard_proof_terminator compute_guard
-  | Some terminator -> terminator compute_guard
-  in
-  let sign =
-    match sign with
-    | Some sign -> sign
-    | None -> initialize_named_context_for_proof ()
-  in
+let start_lemma id ?pl kind sigma ?(terminator=standard_proof_terminator) ?(sign=initialize_named_context_for_proof()) ?(compute_guard=[]) ?hook c =
   let goals = [ Global.env_of_context sign , c ] in
   let proof = Proof_global.start_proof sigma id ?pl kind goals in
-  { proof ; terminator; hook }
+  { proof ; terminator; hook; compute_guard }
 
-let start_dependent_lemma id ?pl kind ?terminator ?sign ?(compute_guard=[]) ?hook telescope =
-  let terminator = match terminator with
-  | None -> standard_proof_terminator compute_guard
-  | Some terminator -> terminator compute_guard
-  in
+let start_dependent_lemma id ?pl kind ?(terminator=standard_proof_terminator) ?sign ?(compute_guard=[]) ?hook telescope =
   let proof = Proof_global.start_dependent_proof id ?pl kind telescope in
-  { proof ; terminator; hook }
+  { proof; terminator; hook; compute_guard }
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
@@ -516,7 +508,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
   let pe =
     let open Proof_global in
     match proof with
-    | Some ({ id; entries; persistence = k; universes }, _, hook) ->
+    | 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
@@ -557,18 +549,23 @@ let save_lemma_admitted ?proof ~(lemma : t) =
   in
   CEphemeron.get lemma.terminator pe
 
+type proof_info = proof_terminator * declaration_hook option * lemma_possible_guards
+
+let default_info = standard_proof_terminator, None, []
+
 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, hook =
+  let proof_obj, proof_info =
     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; 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
+      let { proof; terminator; hook; compute_guard } = Option.get lemma in
+      Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, (terminator, hook, compute_guard)
+    | Some (proof, info) ->
+      proof, info
   in
-  CEphemeron.get terminator (Proved (opaque,idopt,proof_obj,hook))
+  let terminator, hook, compute_guard = proof_info in
+  CEphemeron.get terminator (Proved (opaque,idopt,proof_obj,hook,compute_guard))
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 03cd45b8bf..3efaac672a 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -41,6 +41,7 @@ val call_hook
 (* Proofs that define a constant + terminators *)
 type t
 type proof_terminator
+type lemma_possible_guards = int list list
 
 module Stack : sig
 
@@ -58,15 +59,13 @@ module Stack : sig
 
   val get_all_proof_names : t -> Names.Id.t list
 
-  val copy_terminators : src:t -> tgt:t -> t
-  (** Gets the current terminator without checking that the proof has
-      been completed. Useful for the likes of [Admitted]. *)
+  val copy_info : src:t -> tgt:t -> t
+  (** Gets the current info without checking that the proof has been
+     completed. Useful for the likes of [Admitted]. *)
 
 end
 
-val standard_proof_terminator
-  :  Proof_global.lemma_possible_guards
-  -> proof_terminator
+val standard_proof_terminator : proof_terminator
 
 val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
 val pf_map : (Proof_global.t -> Proof_global.t) -> t -> t
@@ -81,9 +80,9 @@ val start_lemma
   -> ?pl:UState.universe_decl
   -> goal_kind
   -> Evd.evar_map
-  -> ?terminator:(Proof_global.lemma_possible_guards -> proof_terminator)
+  -> ?terminator:proof_terminator
   -> ?sign:Environ.named_context_val
-  -> ?compute_guard:Proof_global.lemma_possible_guards
+  -> ?compute_guard:lemma_possible_guards
   -> ?hook:declaration_hook
   -> EConstr.types
   -> t
@@ -92,9 +91,9 @@ val start_dependent_lemma
   :  Id.t
   -> ?pl:UState.universe_decl
   -> goal_kind
-  -> ?terminator:(Proof_global.lemma_possible_guards -> proof_terminator)
+  -> ?terminator:proof_terminator
   -> ?sign:Environ.named_context_val
-  -> ?compute_guard:Proof_global.lemma_possible_guards
+  -> ?compute_guard:lemma_possible_guards
   -> ?hook:declaration_hook
   -> Proofview.telescope
   -> t
@@ -108,7 +107,7 @@ val start_lemma_com
 val start_lemma_with_initialization
   :  ?hook:declaration_hook
   -> goal_kind -> Evd.evar_map -> UState.universe_decl
-  -> (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option
+  -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option
   -> (Id.t (* name of thm *) *
      (EConstr.types (* type of thm *) *
       (Name.t list (* names to pre-introduce *) * Impargs.manual_implicits))) list
@@ -124,13 +123,17 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val
 
 (** {6 Saving proofs } *)
 
+type proof_info
+
+val default_info : proof_info
+
 val save_lemma_admitted
-  :  ?proof:(Proof_global.proof_object * proof_terminator * declaration_hook option)
+  :  ?proof:(Proof_global.proof_object * proof_info)
   -> lemma:t
   -> unit
 
 val save_lemma_proved
-  :  ?proof:(Proof_global.proof_object * proof_terminator * declaration_hook option)
+  :  ?proof:(Proof_global.proof_object * proof_info)
   -> ?lemma:t
   -> opaque:Proof_global.opacity_flag
   -> idopt:Names.lident option
@@ -148,14 +151,14 @@ type proof_ending =
       Proof_global.opacity_flag *
       lident option *
       Proof_global.proof_object *
-      declaration_hook option
+      declaration_hook option *
+      lemma_possible_guards
 
 (** 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
+  val get_info : t -> proof_info
 
   (** 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 98dec7930c..b6f2c47f98 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -491,9 +491,8 @@ 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 guard =
-    Lemmas.Internal.make_terminator
-      (obligation_terminator prg.prg_name num guard auto) in
+  let terminator = Lemmas.Internal.make_terminator
+      (obligation_terminator prg.prg_name num 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 8d1d9abc0b..2895d0e4df 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 * Lemmas.declaration_hook option) ->
+  ?proof:(Proof_global.proof_object * Lemmas.proof_info) ->
   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 0cdf748ce9..c387c5c5f1 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 * Lemmas.declaration_hook option
+  type closed_proof = Proof_global.proof_object * Lemmas.proof_info
 
 
   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_hook pt)
+                        Internal.get_info 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_hook pt)
+                        Internal.get_info pt)
 
   let discard_all () = s_lemmas := None
   let update_global_env () = dd (update_global_env)
@@ -158,6 +158,6 @@ module Proof_global = struct
     | None, None -> None
     | Some _ , None -> None
     | None, Some x -> Some x
-    | Some src, Some tgt -> Some (Stack.copy_terminators ~src ~tgt)
+    | Some src, Some tgt -> Some (Stack.copy_info ~src ~tgt)
 
 end
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 15b8aaefb6..b78b252579 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 * Lemmas.declaration_hook option
+  type closed_proof = Proof_global.proof_object * Lemmas.proof_info
 
   val close_future_proof :
     opaque:Proof_global.opacity_flag ->
-- 
cgit v1.2.3