From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- proofs/proof_global.mli | 154 ++++++++++++++++++++++++++++++++++-------------- 1 file changed, 110 insertions(+), 44 deletions(-) (limited to 'proofs/proof_global.mli') diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 08ae7519..2700e901 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit -val there_is_a_proof : unit -> bool val there_are_pending_proofs : unit -> bool val check_no_pending_proof : unit -> unit -val get_current_proof_name : unit -> Names.identifier -val get_all_proof_names : unit -> Names.identifier list +val get_current_proof_name : unit -> Names.Id.t +val get_all_proof_names : unit -> Names.Id.t list -val discard : Names.identifier Util.located -> unit +val discard : Names.Id.t Loc.located -> unit val discard_current : unit -> unit val discard_all : unit -> unit @@ -45,53 +44,102 @@ val set_proof_mode : string -> unit exception NoCurrentProof val give_me_the_proof : unit -> Proof.proof +(** @raise NoCurrentProof when outside proof mode. *) +val compact_the_proof : unit -> unit -(** [start_proof s str goals ~init_tac ~compute_guard hook] starts - a proof of name [s] and - conclusion [t]; [hook] is optionally a function to be applied at - proof end (e.g. to declare the built constructions as a coercion - or a setoid morphism). *) +(** When a proof is closed, it is reified into a [proof_object], where + [id] is the name of the proof, [entries] the list of the proof terms + (in a form suitable for definitions). Together with the [terminator] + 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 -val start_proof : Names.identifier -> - Decl_kinds.goal_kind -> - (Environ.env * Term.types) list -> - ?compute_guard:lemma_possible_guards -> - Tacexpr.declaration_hook -> - unit - -val close_proof : unit -> - Names.identifier * - (Entries.definition_entry list * - lemma_possible_guards * - Decl_kinds.goal_kind * - Tacexpr.declaration_hook) +type proof_universes = Evd.evar_universe_context +type proof_object = { + id : Names.Id.t; + entries : Entries.definition_entry list; + persistence : Decl_kinds.goal_kind; + universes: proof_universes; + (* constraints : Univ.constraints; *) + (** guards : lemma_possible_guards; *) +} + +type proof_ending = + | Admitted + | Proved of Vernacexpr.opacity_flag * + (Vernacexpr.lident * Decl_kinds.theorem_kind option) option * + proof_object +type proof_terminator = proof_ending -> unit +type closed_proof = proof_object * proof_terminator + +(** [start_proof id str goals terminator] starts a proof of name [id] + with goals [goals] (a list of pairs of environment and + conclusion); [str] describes what kind of theorem/definition this + is (spiwack: for potential printing, I believe is used only by + closing commands and the xml plugin); [terminator] is used at the + end of the proof to close the proof. *) +val start_proof : + Evd.evar_map -> Names.Id.t -> Decl_kinds.goal_kind -> (Environ.env * Term.types) list -> + proof_terminator -> unit + +(** Like [start_proof] except that there may be dependencies between + initial goals. *) +val start_dependent_proof : + Names.Id.t -> Decl_kinds.goal_kind -> Proofview.telescope -> + proof_terminator -> unit + +(* Takes a function to add to the exceptions data relative to the + state in which the proof was built *) +val close_proof : keep_body_ucst_sepatate:bool -> Future.fix_exn -> closed_proof + +(* Intermediate step necessary to delegate the future. + * Both access the current proof state. The formes is supposed to be + * chained with a computation that completed the proof *) + +type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context + +val return_proof : unit -> closed_proof_output +val close_future_proof : feedback_id:Stateid.t -> + closed_proof_output Future.computation -> closed_proof + +(** Gets the current terminator without checking that the proof has + been completed. Useful for the likes of [Admitted]. *) +val get_terminator : unit -> proof_terminator +val set_terminator : proof_terminator -> unit exception NoSuchProof -(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is - no current proof. *) -val run_tactic : unit Proofview.tactic -> unit +val get_open_goals : unit -> int -(** Sets the tactic to be used when a tactic line is closed with [...] *) -val set_endline_tactic : unit Proofview.tactic -> unit +(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is + no current proof. + The return boolean is set to [false] if an unsafe tactic has been used. *) +val with_current_proof : + (unit Proofview.tactic -> Proof.proof -> Proof.proof*'a) -> 'a +val simple_with_current_proof : + (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit -(** Sets the section variables assumed by the proof *) -val set_used_variables : Names.identifier list -> unit -val get_used_variables : unit -> Sign.section_context option +(** Sets the tactic to be used when a tactic line is closed with [...] *) +val set_endline_tactic : Tacexpr.raw_tactic_expr -> unit +val set_interp_tac : + (Tacexpr.raw_tactic_expr -> unit Proofview.tactic) + -> unit -(** Appends the endline tactic of the current proof to a tactic. *) -val with_end_tac : unit Proofview.tactic -> unit Proofview.tactic +(** Sets the section variables assumed by the proof, returns its closure + * (w.r.t. type dependencies *) +val set_used_variables : Names.Id.t list -> Context.section_context +val get_used_variables : unit -> Context.section_context option (**********************************************************) -(* *) -(* Utility functions *) -(* *) +(* *) +(* Proof modes *) +(* *) (**********************************************************) -(** [maximal_unfocus k p] unfocuses [p] until [p] has at least a - focused goal or that the last focus isn't of kind [k]. *) -val maximal_unfocus : 'a Proof.focus_kind -> Proof.proof -> unit + +val activate_proof_mode : string -> unit +val disactivate_proof_mode : string -> unit (**********************************************************) (* *) @@ -103,11 +151,13 @@ module Bullet : sig type t = Vernacexpr.bullet (** A [behavior] is the data of a put function which - is called when a bullet prefixes a tactic, together - with a name to identify it. *) + is called when a bullet prefixes a tactic, a suggest function + suggesting the right bullet to use on a given proof, together + with a name to identify the behavior. *) type behavior = { name : string; - put : Proof.proof -> t -> unit + put : Proof.proof -> t -> Proof.proof; + suggest: Proof.proof -> string option } (** A registered behavior can then be accessed in Coq @@ -123,9 +173,25 @@ module Bullet : sig (** Handles focusing/defocusing with bullets: *) - val put : Proof.proof -> t -> unit + val put : Proof.proof -> t -> Proof.proof + val suggest : Proof.proof -> string option end + +(**********************************************************) +(* *) +(* Default goal selector *) +(* *) +(**********************************************************) + +val get_default_goal_selector : unit -> Vernacexpr.goal_selector + module V82 : sig - val get_current_initial_conclusions : unit -> Names.identifier *(Term.types list * Decl_kinds.goal_kind * Tacexpr.declaration_hook) + val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list * + Decl_kinds.goal_kind) end + +type state +val freeze : marshallable:[`Yes | `No | `Shallow] -> state +val unfreeze : state -> unit +val proof_of_state : state -> Proof.proof -- cgit v1.2.3