[declare] Merge `DeclareObl` into `Declare`

This is needed as a first step to refactor and unify the obligation
save path and state; in particular `Equations` is a heavy user of
Hooks to modify obligations state, thus in order to make the hook
aware of this we need to place the obligation state before the hook.

As a good side-effect, `inline_private_constants` and `Hook.call` are
not exported from `Declare` anymore.

1 files changed, 158 insertions, 14 deletions

diff --git a/vernac/declare.mli b/vernac/declare.mli
index 340c035d1d..2c4a801f9a 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -160,7 +160,7 @@ val definition_entry
   -> constr
   -> Evd.side_effects proof_entry
 
-type import_status = ImportDefaultBehavior | ImportNeedQualified
+type import_status = Locality.import_status = ImportDefaultBehavior | ImportNeedQualified
 
 (** [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
@@ -177,17 +177,6 @@ val declare_constant
   -> Evd.side_effects constant_entry
   -> Constant.t
 
-(** [inline_private_constants ~sideff ~uctx env ce] will inline the
-   constants in [ce]'s body and return the body plus the updated
-   [UState.t].
-
-   XXX: Scheduled for removal from public API, don't rely on it *)
-val inline_private_constants
-  :  uctx:UState.t
-  -> Environ.env
-  -> Evd.side_effects proof_entry
-  -> Constr.t * UState.t
-
 (** Declaration messages *)
 
 (** XXX: Scheduled for removal from public API, do not use *)
@@ -233,6 +222,7 @@ val close_future_proof : feedback_id:Stateid.t -> Proof.t -> closed_proof_output
     Returns [false] if an unsafe tactic has been used. *)
 val by : unit Proofview.tactic -> Proof.t -> Proof.t * bool
 
+(** Semantics of this function is a bit dubious, use with care *)
 val build_by_tactic
   :  ?side_eff:bool
   -> Environ.env
@@ -260,7 +250,7 @@ val get_current_goal_context : Proof.t -> Evd.evar_map * Environ.env
   environment and empty evar_map. *)
 val get_current_context : Proof.t -> Evd.evar_map * Environ.env
 
-(** Temporarily re-exported for 3rd party code; don't use  *)
+(** XXX: Temporarily re-exported for 3rd party code; don't use  *)
 val build_constant_by_tactic :
   name:Names.Id.t ->
   ?opaque:opacity_flag ->
@@ -274,7 +264,7 @@ val build_constant_by_tactic :
 val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
 [@@ocaml.deprecated "Use DeclareUctx.declare_universe_context"]
 
-type locality = Discharge | Global of import_status
+type locality = Locality.locality = Discharge | Global of import_status
 
 (** Declaration hooks *)
 module Hook : sig
@@ -397,3 +387,157 @@ val prepare_parameter
 
 (* Compat: will remove *)
 exception AlreadyDeclared of (string option * Names.Id.t)
+
+module Obls : sig
+
+type 'a obligation_body = DefinedObl of 'a | TermObl of constr
+
+module Obligation : sig
+  type t = private
+    { obl_name : Id.t
+    ; obl_type : types
+    ; obl_location : Evar_kinds.t Loc.located
+    ; obl_body : pconstant obligation_body option
+    ; obl_status : bool * Evar_kinds.obligation_definition_status
+    ; obl_deps : Int.Set.t
+    ; obl_tac : unit Proofview.tactic option }
+
+  val set_type : typ:Constr.types -> t -> t
+  val set_body : body:pconstant obligation_body -> t -> t
+end
+
+type obligations = {obls : Obligation.t array; remaining : int}
+type fixpoint_kind = IsFixpoint of lident option list | IsCoFixpoint
+
+(* Information about a single [Program {Definition,Lemma,..}] declaration *)
+module ProgramDecl : sig
+  type t = private
+    { prg_name : Id.t
+    ; prg_body : constr
+    ; prg_type : constr
+    ; prg_ctx : UState.t
+    ; prg_univdecl : UState.universe_decl
+    ; prg_obligations : obligations
+    ; prg_deps : Id.t list
+    ; prg_fixkind : fixpoint_kind option
+    ; prg_implicits : Impargs.manual_implicits
+    ; prg_notations : Vernacexpr.decl_notation list
+    ; prg_poly : bool
+    ; prg_scope : locality
+    ; prg_kind : Decls.definition_object_kind
+    ; prg_reduce : constr -> constr
+    ; prg_hook : Hook.t option
+    ; prg_opaque : bool }
+
+  val make :
+       ?opaque:bool
+    -> ?hook:Hook.t
+    -> Names.Id.t
+    -> udecl:UState.universe_decl
+    -> uctx:UState.t
+    -> impargs:Impargs.manual_implicits
+    -> poly:bool
+    -> scope:locality
+    -> kind:Decls.definition_object_kind
+    -> Constr.constr option
+    -> Constr.types
+    -> Names.Id.t list
+    -> fixpoint_kind option
+    -> Vernacexpr.decl_notation list
+    -> ( Names.Id.t
+       * Constr.types
+       * Evar_kinds.t Loc.located
+       * (bool * Evar_kinds.obligation_definition_status)
+       * Int.Set.t
+       * unit Proofview.tactic option )
+       array
+    -> (Constr.constr -> Constr.constr)
+    -> t
+
+  val set_uctx : uctx:UState.t -> t -> t
+end
+
+(** [declare_obligation] Save an obligation *)
+val declare_obligation :
+     ProgramDecl.t
+  -> Obligation.t
+  -> Constr.types
+  -> Constr.types option
+  -> Entries.universes_entry
+  -> bool * Obligation.t
+
+module State : sig
+
+  val num_pending : unit -> int
+  val first_pending : unit -> ProgramDecl.t option
+
+  (** Returns [Error duplicate_list] if not a single program is open *)
+  val get_unique_open_prog :
+    Id.t option -> (ProgramDecl.t, Id.t list) result
+
+  (** Add a new obligation *)
+  val add : Id.t -> ProgramDecl.t -> unit
+
+  val fold : f:(Id.t -> ProgramDecl.t -> 'a -> 'a) -> init:'a -> 'a
+
+  val all : unit -> ProgramDecl.t list
+
+  val find : Id.t -> ProgramDecl.t option
+
+  (* Internal *)
+  type t
+  val prg_tag : t Summary.Dyn.tag
+end
+
+val declare_definition : ProgramDecl.t -> Names.GlobRef.t
+
+(** Resolution status of a program *)
+type progress =
+  | Remain of int  (** n obligations remaining *)
+  | Dependent  (** Dependent on other definitions *)
+  | Defined of GlobRef.t  (** Defined as id *)
+
+type obligation_resolver =
+     Id.t option
+  -> Int.Set.t
+  -> unit Proofview.tactic option
+  -> progress
+
+type obligation_qed_info = {name : Id.t; num : int; auto : obligation_resolver}
+
+(** [obligation_terminator] part 2 of saving an obligation, proof mode *)
+val obligation_terminator :
+    Evd.side_effects proof_entry list
+  -> UState.t
+  -> obligation_qed_info
+  -> unit
+
+(** [obligation_admitted_terminator] part 2 of saving an obligation, non-interactive mode *)
+val obligation_admitted_terminator :
+  obligation_qed_info -> UState.t -> GlobRef.t -> unit
+
+(** [update_obls prg obls n progress] What does this do? *)
+val update_obls :
+  ProgramDecl.t -> Obligation.t array -> int -> progress
+
+(** Check obligations are properly solved before closing the
+   [what_for] section / module *)
+val check_solved_obligations : what_for:Pp.t -> unit
+
+(** { 2 Util }  *)
+
+val obl_substitution :
+     bool
+  -> Obligation.t array
+  -> Int.Set.t
+  -> (Id.t * (Constr.types * Constr.types)) list
+
+val dependencies : Obligation.t array -> int -> Int.Set.t
+val err_not_transp : unit -> unit
+
+(* This is a hack to make it possible for Obligations to craft a Qed
+ * behind the scenes.  The fix_exn the Stm attaches to the Future proof
+ * is not available here, so we provide a side channel to get it *)
+val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) ref
+
+end