[declare] Make `proof_entry` a private type.

Proof entries are low-level objects and should not be manipulated by
users directly, in particular as we want to unify all the code
around declaration of constants.

This patch doesn't bring by itself a lot of improvement, other than
setting the base where to extend the interface, however it already
points out some points of interest, and in particular the manipulation
of opacity done by `Derive` which can be quite problematic, and of
course the handling of delayed proofs.

So while this is a first step, IMHO it doesn't harm a lot having it in
place, but a lot more work will be needed, in particular regarding the
handling of delayed proofs.

To make `proof_entry` a fully abstract type, the remaining work is
focused on `abstract` and obligations, both of which do quite a few
hackery that will have to be migrated to the `Declare` API.

8 files changed, 143 insertions, 96 deletions

diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 03ab0a1c13..4ddd29f973 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -8,14 +8,11 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-module CVars = Vars
-
 open Util
 open Termops
 open EConstr
 open Evarutil
 
-module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 (* tactical to save as name a subproof such that the generalisation of
@@ -37,54 +34,6 @@ let interpretable_as_section_decl env evd d1 d2 =
     e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2
   | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (NamedDecl.get_type d2)
 
-let rec decompose len c t accu =
-  let open Constr in
-  let open Context.Rel.Declaration in
-  if len = 0 then (c, t, accu)
-  else match kind c, kind t with
-  | Lambda (na, u, c), Prod (_, _, t) ->
-    decompose (pred len) c t (LocalAssum (na, u) :: accu)
-  | LetIn (na, b, u, c), LetIn (_, _, _, t) ->
-    decompose (pred len) c t (LocalDef (na, b, u) :: accu)
-  | _ -> assert false
-
-let rec shrink ctx sign c t accu =
-  let open Constr in
-  let open CVars in
-  match ctx, sign with
-  | [], [] -> (c, t, accu)
-  | p :: ctx, decl :: sign ->
-      if noccurn 1 c && noccurn 1 t then
-        let c = subst1 mkProp c in
-        let t = subst1 mkProp t in
-        shrink ctx sign c t accu
-      else
-        let c = Term.mkLambda_or_LetIn p c in
-        let t = Term.mkProd_or_LetIn p t in
-        let accu = if RelDecl.is_local_assum p
-                   then mkVar (NamedDecl.get_id decl) :: accu
-                   else accu
-    in
-    shrink ctx sign c t accu
-| _ -> assert false
-
-let shrink_entry sign const =
-  let open Declare in
-  let typ = match const.proof_entry_type with
-  | None -> assert false
-  | Some t -> t
-  in
-  (* The body has been forced by the call to [build_constant_by_tactic] *)
-  let () = assert (Future.is_over const.proof_entry_body) in
-  let ((body, uctx), eff) = Future.force const.proof_entry_body in
-  let (body, typ, ctx) = decompose (List.length sign) body typ [] in
-  let (body, typ, args) = shrink ctx sign body typ [] in
-  let const = { const with
-    proof_entry_body = Future.from_val ((body, uctx), eff);
-    proof_entry_type = Some typ;
-  } in
-  (const, args)
-
 let name_op_to_name ~name_op ~name suffix =
   match name_op with
   | Some s -> s
@@ -101,9 +50,10 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
      redundancy on constant declaration. This opens up an interesting
      question, how does abstract behave when discharge is local for example?
   *)
-  let suffix = if opaque
-    then "_subproof"
-    else "_subterm" in
+  let suffix, kind = if opaque
+    then "_subproof", Decls.(IsProof Lemma)
+    else "_subterm", Decls.(IsDefinition Definition)
+  in
   let name = name_op_to_name ~name_op ~name suffix in
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
@@ -140,7 +90,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in
   let ectx = Evd.evar_universe_context evd in
   let (const, safe, ectx) =
-    try Pfedit.build_constant_by_tactic ~poly ~name ectx secsign concl solve_tac
+    try Pfedit.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly ectx secsign concl solve_tac
     with Logic_monad.TacticFailure e as src ->
     (* if the tactic [tac] fails, it reports a [TacticFailure e],
        which is an error irrelevant to the proof system (in fact it
@@ -151,16 +101,20 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   in
   let body, effs = Future.force const.Declare.proof_entry_body in
   (* We drop the side-effects from the entry, they already exist in the ambient environment *)
-  let const = { const with Declare.proof_entry_body = Future.from_val (body, ()) } in
-  let const, args = shrink_entry sign const in
+  let const = Declare.Internal.map_entry_body const ~f:(fun _ -> body, ()) in
+  (* EJGA: Hack related to the above call to
+     `build_constant_by_tactic` with `~opaque:Transparent`. Even if
+     the abstracted term is destined to be opaque, if we trigger the
+     `if poly && opaque && private_poly_univs ()` in `Proof_global`
+     kernel will boom. This deserves more investigation. *)
+  let const = Declare.Internal.set_opacity ~opaque const in
+  let const, args = Declare.Internal.shrink_entry sign const in
   let args = List.map EConstr.of_constr args in
-  let cd = { const with Declare.proof_entry_opaque = opaque } in
-  let kind = if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition) in
   let cst () =
     (* do not compute the implicit arguments, it may be costly *)
     let () = Impargs.make_implicit_args false in
     (* ppedrot: seems legit to have abstracted subproofs as local*)
-    Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind cd
+    Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind const
   in
   let cst, eff = Impargs.with_implicit_protection cst () in
   let inst = match const.Declare.proof_entry_universes with
diff --git a/tactics/abstract.mli b/tactics/abstract.mli
index 96ddbea7b2..779e46cd49 100644
--- a/tactics/abstract.mli
+++ b/tactics/abstract.mli
@@ -20,11 +20,3 @@ val cache_term_by_tactic_then
   -> unit Proofview.tactic
 
 val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
-
-(* Internal but used in a few places; should likely be made intro a
-   proper library function, or incorporated into the generic constant
-   save path *)
-val shrink_entry
-  :  ('a, 'b) Context.Named.Declaration.pt list
-  -> 'c Declare.proof_entry
-  -> 'c Declare.proof_entry * Constr.t list
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 57eeddb847..eb17cf67d1 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -174,6 +174,7 @@ let record_aux env s_ty s_bo =
   Aux_file.record_in_aux "context_used" v
 
 let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
+
 let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body =
   { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
@@ -184,6 +185,26 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     proof_entry_feedback = None;
     proof_entry_inline_code = inline}
 
+let pure_definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
+    ?(univs=default_univ_entry) body =
+  { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), ());
+    proof_entry_secctx = None;
+    proof_entry_type = types;
+    proof_entry_universes = univs;
+    proof_entry_opaque = opaque;
+    proof_entry_feedback = None;
+    proof_entry_inline_code = inline}
+
+let delayed_definition_entry ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?(univs=default_univ_entry) ?types body =
+  { proof_entry_body = body
+  ; proof_entry_secctx = section_vars
+  ; proof_entry_type = types
+  ; proof_entry_universes = univs
+  ; proof_entry_opaque = opaque
+  ; proof_entry_feedback = feedback_id
+  ; proof_entry_inline_code = inline
+  }
+
 let cast_proof_entry e =
   let (body, ctx), () = Future.force e.proof_entry_body in
   let univs =
@@ -413,3 +434,62 @@ let assumption_message id =
   the type of the object than to the name of the object (see
   discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
   Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared")
+
+module Internal = struct
+
+  let map_entry_body ~f entry =
+    { entry with proof_entry_body = Future.chain entry.proof_entry_body f }
+
+  let map_entry_type ~f entry =
+    { entry with proof_entry_type = f entry.proof_entry_type }
+
+  let set_opacity ~opaque entry =
+    { entry with proof_entry_opaque = opaque }
+
+  let rec decompose len c t accu =
+    let open Constr in
+    let open Context.Rel.Declaration in
+    if len = 0 then (c, t, accu)
+    else match kind c, kind t with
+      | Lambda (na, u, c), Prod (_, _, t) ->
+        decompose (pred len) c t (LocalAssum (na, u) :: accu)
+      | LetIn (na, b, u, c), LetIn (_, _, _, t) ->
+        decompose (pred len) c t (LocalDef (na, b, u) :: accu)
+      | _ -> assert false
+
+  let rec shrink ctx sign c t accu =
+    let open Constr in
+    let open Vars in
+    match ctx, sign with
+    | [], [] -> (c, t, accu)
+    | p :: ctx, decl :: sign ->
+      if noccurn 1 c && noccurn 1 t then
+        let c = subst1 mkProp c in
+        let t = subst1 mkProp t in
+        shrink ctx sign c t accu
+      else
+        let c = Term.mkLambda_or_LetIn p c in
+        let t = Term.mkProd_or_LetIn p t in
+        let accu = if Context.Rel.Declaration.is_local_assum p
+          then mkVar (NamedDecl.get_id decl) :: accu
+          else accu
+        in
+        shrink ctx sign c t accu
+    | _ -> assert false
+
+  let shrink_entry sign const =
+    let typ = match const.proof_entry_type with
+      | None -> assert false
+      | Some t -> t
+    in
+    (* The body has been forced by the call to [build_constant_by_tactic] *)
+    let () = assert (Future.is_over const.proof_entry_body) in
+    let ((body, uctx), eff) = Future.force const.proof_entry_body in
+    let (body, typ, ctx) = decompose (List.length sign) body typ [] in
+    let (body, typ, args) = shrink ctx sign body typ [] in
+    { const with
+      proof_entry_body = Future.from_val ((body, uctx), eff)
+    ; proof_entry_type = Some typ
+    }, args
+
+end
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 1a037ef937..0cdf317fe4 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -20,7 +20,7 @@ open Entries
    [Nametab] and [Impargs]. *)
 
 (** Proof entries *)
-type 'a proof_entry = {
+type 'a proof_entry = private {
   proof_entry_body   : 'a Entries.const_entry_body;
   (* List of section variables *)
   proof_entry_secctx : Id.Set.t option;
@@ -55,10 +55,35 @@ val declare_variable
    i.e. Definition/Theorem/Axiom/Parameter/... *)
 
 (* Default definition entries, transparent with no secctx or proj information *)
-val definition_entry : ?fix_exn:Future.fix_exn ->
-  ?opaque:bool -> ?inline:bool -> ?types:types ->
-  ?univs:Entries.universes_entry ->
-  ?eff:Evd.side_effects -> constr -> Evd.side_effects proof_entry
+val definition_entry
+  : ?fix_exn:Future.fix_exn
+  -> ?opaque:bool
+  -> ?inline:bool
+  -> ?types:types
+  -> ?univs:Entries.universes_entry
+  -> ?eff:Evd.side_effects
+  -> constr
+  -> Evd.side_effects proof_entry
+
+val pure_definition_entry
+  : ?fix_exn:Future.fix_exn
+  -> ?opaque:bool
+  -> ?inline:bool
+  -> ?types:types
+  -> ?univs:Entries.universes_entry
+  -> constr
+  -> unit proof_entry
+
+(* Delayed definition entries *)
+val delayed_definition_entry
+  :  ?opaque:bool
+  -> ?inline:bool
+  -> ?feedback_id:Stateid.t
+  -> ?section_vars:Id.Set.t
+  -> ?univs:Entries.universes_entry
+  -> ?types:types
+  -> 'a Entries.const_entry_body
+  -> 'a proof_entry
 
 type import_status = ImportDefaultBehavior | ImportNeedQualified
 
@@ -101,3 +126,15 @@ val check_exists : Id.t -> unit
 
 (* Used outside this module only in indschemes *)
 exception AlreadyDeclared of (string option * Id.t)
+
+(* For legacy support, do not use *)
+module Internal : sig
+
+  val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry
+  val map_entry_type : f:(Constr.t option -> Constr.t option) -> 'a proof_entry -> 'a proof_entry
+  (* Overriding opacity is indeed really hacky *)
+  val set_opacity : opaque:bool -> 'a proof_entry -> 'a proof_entry
+
+  val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list
+
+end
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 3f824a94bf..ac98b5f116 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -124,16 +124,7 @@ let define internal role id c poly univs =
   let ctx = UState.minimize univs in
   let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
   let univs = UState.univ_entry ~poly ctx in
-  let entry = {
-    Declare.proof_entry_body =
-      Future.from_val ((c,Univ.ContextSet.empty), ());
-    proof_entry_secctx = None;
-    proof_entry_type = None;
-    proof_entry_universes = univs;
-    proof_entry_opaque = false;
-    proof_entry_inline_code = false;
-    proof_entry_feedback = None;
-  } in
+  let entry = Declare.pure_definition_entry ~univs c in
   let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id entry in
   let () = match internal with
     | InternalTacticRequest -> ()
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index 413c6540a3..3e057190ac 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -114,14 +114,14 @@ let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None t
 
 let next = let n = ref 0 in fun () -> incr n; !n
 
-let build_constant_by_tactic ~name ctx sign ~poly typ tac =
+let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ctx sign ~poly typ tac =
   let evd = Evd.from_ctx ctx in
   let goals = [ (Global.env_of_context sign , typ) ] in
   let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in
   try
     let pf, status = by tac pf in
     let open Proof_global in
-    let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in
+    let { entries; universes } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in
     match entries with
     | [entry] ->
       entry, status, universes
diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli
index 30514191fa..a780b2d96e 100644
--- a/tactics/pfedit.mli
+++ b/tactics/pfedit.mli
@@ -59,6 +59,7 @@ val use_unification_heuristics : unit -> bool
 
 val build_constant_by_tactic
   :  name:Id.t
+  -> ?opaque:Proof_global.opacity_flag
   -> UState.t
   -> named_context_val
   -> poly:bool
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index b723922642..b1fd34e43c 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -238,18 +238,10 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
     let t = EConstr.Unsafe.to_constr t in
     let univstyp, body = make_body t p in
     let univs, typ = Future.force univstyp in
-    let open Declare in
-    {
-      proof_entry_body = body;
-      proof_entry_secctx = section_vars;
-      proof_entry_feedback = feedback_id;
-      proof_entry_type  = Some typ;
-      proof_entry_inline_code = false;
-      proof_entry_opaque = opaque;
-      proof_entry_universes = univs; }
+    Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs ~types:typ body
   in
-  let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in
-  { name; entries = entries; poly; universes; udecl }
+  let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in
+  { name; entries; poly; universes; udecl }
 
 let return_proof ?(allow_partial=false) ps =
  let { proof } = ps in