From a8b3c907cb2d6da16bdeea10b943552dc9efc0ed Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 5 Jun 2019 17:48:46 +0200
Subject: [proof] Move proofs that have an associated constant to `Lemmas`

The main idea of this PR is to distinguish the types of "proof object"
`Proof_global.t` and the type of "proof object associated to a
constant, the new `Lemmas.t`.

This way, we can move the terminator setup to the higher layer in
`vernac`, which is the one that really knows about constants, paving
the way for further simplification and in particular for a unified
handling of constant saving by removal of the control inversion here.

Terminators are now internal to `Lemmas`, as it is the only part of
the code applying them.

As a consequence, proof nesting is now handled by `Lemmas`, and
`Proof_global.t` is just a single `Proof.t` plus some environmental
meta-data.

We are also enable considerable simplification in a future PR, as this
patch makes `Proof.t` and `Proof_global.t` essentially the same, so we
should expect to handle them under a unified interface.
---
 plugins/derive/derive.ml    | 24 +++++++++++-------------
 plugins/derive/derive.mli   |  6 +++++-
 plugins/derive/g_derive.mlg |  2 +-
 3 files changed, 17 insertions(+), 15 deletions(-)

(limited to 'plugins/derive')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 7c0f269481..fd5b3a7e48 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -22,7 +22,7 @@ let map_const_entry_body (f:constr->constr) (x:Safe_typing.private_constants Ent
     (which can contain references to [f]) in the context extended by
     [f:=?x]. When the proof ends, [f] is defined as the value of [?x]
     and [lemma] as the proof. *)
-let start_deriving f suchthat lemma =
+let start_deriving f suchthat name : Lemmas.t =
 
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -48,7 +48,6 @@ let start_deriving f suchthat lemma =
 
     (* The terminator handles the registering of constants when the proof is closed. *)
     let terminator com =
-      let open Proof_global in
       (* Extracts the relevant information from the proof. [Admitted]
          and [Save] result in user errors. [opaque] is [true] if the
          proof was concluded by [Qed], and [false] if [Defined]. [f_def]
@@ -56,10 +55,10 @@ let start_deriving f suchthat lemma =
          [suchthat], respectively. *)
       let (opaque,f_def,lemma_def) =
         match com with
-        | Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.")
-        | Proved (_,Some _,_) ->
+        | Lemmas.Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.")
+        | Lemmas.Proved (_,Some _,_) ->
             CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.")
-        | 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
@@ -97,12 +96,11 @@ let start_deriving f suchthat lemma =
         Entries.DefinitionEntry lemma_def ,
         Decl_kinds.(IsProof Proposition)
       in
-      ignore (Declare.declare_constant lemma lemma_def)
-      in
+      ignore (Declare.declare_constant name lemma_def)
+  in
 
-  let terminator = Proof_global.make_terminator terminator in
-  let pstate = Proof_global.start_dependent_proof lemma kind goals terminator in
-  Proof_global.modify_proof begin fun p ->
-    let p,_,() =  Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p in
-    p
-  end pstate
+  let terminator ?hook _ = Lemmas.make_terminator terminator in
+  let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in
+  Lemmas.simple_with_proof begin fun _ p ->
+    Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
+  end lemma
diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli
index 6bb923118e..ffbc726e22 100644
--- a/plugins/derive/derive.mli
+++ b/plugins/derive/derive.mli
@@ -12,4 +12,8 @@
     (which can contain references to [f]) in the context extended by
     [f:=?x]. When the proof ends, [f] is defined as the value of [?x]
     and [lemma] as the proof. *)
-val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.t
+val start_deriving
+  :  Names.Id.t
+  -> Constrexpr.constr_expr
+  -> Names.Id.t
+  -> Lemmas.t
diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg
index 526989fdf3..6c9cd66f96 100644
--- a/plugins/derive/g_derive.mlg
+++ b/plugins/derive/g_derive.mlg
@@ -24,5 +24,5 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac
 
 VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } STATE open_proof
 | [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] ->
-  { Derive.(start_deriving f suchthat lemma) }
+  { Derive.start_deriving f suchthat lemma }
 END
-- 
cgit v1.2.3