diff options
Diffstat (limited to 'engine/proofview.mli')
| -rw-r--r-- | engine/proofview.mli | 82 |
1 files changed, 51 insertions, 31 deletions
diff --git a/engine/proofview.mli b/engine/proofview.mli index b02fde3a80..e7be665527 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This files defines the basic mechanism of proofs: the [proofview] @@ -72,7 +74,15 @@ val return : proofview -> Evd.evar_map val partial_proof : entry -> proofview -> constr list val initial_goals : entry -> (constr * types) list +(** goal <-> goal_with_state *) +val with_empty_state : + Proofview_monad.goal -> Proofview_monad.goal_with_state +val drop_state : + Proofview_monad.goal_with_state -> Proofview_monad.goal +val goal_with_state : + Proofview_monad.goal -> Proofview_monad.StateStore.t -> + Proofview_monad.goal_with_state (** {6 Focusing commands} *) @@ -416,14 +426,26 @@ module Unsafe : sig (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently being proved, appending them to the list of focused goals. If a goal is already solved, it is not added. *) - val tclNEWGOALS : Evar.t list -> unit tactic + val tclNEWGOALS : Proofview_monad.goal_with_state list -> unit tactic (** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a goal is already solved, it is not set. *) - val tclSETGOALS : Evar.t list -> unit tactic + val tclSETGOALS : Proofview_monad.goal_with_state list -> unit tactic (** [tclGETGOALS] returns the list of goals under focus. *) - val tclGETGOALS : Evar.t list tactic + val tclGETGOALS : Proofview_monad.goal_with_state list tactic + + (** [tclSETSHELF gls] sets goals [gls] as the current shelf. *) + val tclSETSHELF : Evar.t list -> unit tactic + + (** [tclGETSHELF] returns the list of goals on the shelf. *) + val tclGETSHELF : Evar.t list tactic + + (** [tclPUTSHELF] appends goals to the shelf. *) + val tclPUTSHELF : Evar.t list -> unit tactic + + (** [tclPUTGIVENUP] add an given up goal. *) + val tclPUTGIVENUP : Evar.t list -> unit tactic (** Sets the evar universe context. *) val tclEVARUNIVCONTEXT : UState.t -> unit tactic @@ -461,56 +483,51 @@ end module Goal : sig - (** Type of goals. - - The first parameter type is a phantom argument indicating whether the data - contained in the goal has been normalized w.r.t. the current sigma. If it - is the case, it is flagged [ `NF ]. You may still access the un-normalized - data using {!assume} if you known you do not rely on the assumption of - being normalized, at your own risk. - - *) - type 'a t + (** Type of goals. *) + type t (** Assume that you do not need the goal to be normalized. *) - val assume : 'a t -> [ `NF ] t + val assume : t -> t + [@@ocaml.deprecated "Normalization is enforced by EConstr, [assume] is not needed anymore"] (** Normalises the argument goal. *) - val normalize : 'a t -> [ `NF ] t tactic + val normalize : t -> t tactic (** [concl], [hyps], [env] and [sigma] given a goal [gl] return respectively the conclusion of [gl], the hypotheses of [gl], the environment of [gl] (i.e. the global environment and the hypotheses) and the current evar map. *) - val concl : 'a t -> constr - val hyps : 'a t -> named_context - val env : 'a t -> Environ.env - val sigma : 'a t -> Evd.evar_map - val extra : 'a t -> Evd.Store.t + val concl : t -> constr + val hyps : t -> named_context + val env : t -> Environ.env + val sigma : t -> Evd.evar_map + val extra : t -> Evd.Store.t + val state : t -> Proofview_monad.StateStore.t (** [nf_enter t] applies the goal-dependent tactic [t] in each goal independently, in the manner of {!tclINDEPENDENT} except that the current goal is also given as an argument to [t]. The goal is normalised with respect to evars. *) - val nf_enter : ([ `NF ] t -> unit tactic) -> unit tactic + val nf_enter : (t -> unit tactic) -> unit tactic (** Like {!nf_enter}, but does not normalize the goal beforehand. *) - val enter : ([ `LZ ] t -> unit tactic) -> unit tactic + val enter : (t -> unit tactic) -> unit tactic (** Like {!enter}, but assumes exactly one goal under focus, raising *) (** a fatal error otherwise. *) - val enter_one : ?__LOC__:string -> ([ `LZ ] t -> 'a tactic) -> 'a tactic + val enter_one : ?__LOC__:string -> (t -> 'a tactic) -> 'a tactic (** Recover the list of current goals under focus, without evar-normalization. FIXME: encapsulate the level in an existential type. *) - val goals : [ `LZ ] t tactic list tactic + val goals : t tactic list tactic (** [unsolved g] is [true] if [g] is still unsolved in the current proof state. *) - val unsolved : 'a t -> bool tactic + val unsolved : t -> bool tactic (** Compatibility: avoid if possible *) - val goal : [ `NF ] t -> Evar.t + val goal : t -> Evar.t + val print : t -> Goal.goal Evd.sigma end @@ -547,7 +564,10 @@ val tclLIFT : 'a NonLogical.t -> 'a tactic (*** Compatibility layer with <= 8.2 tactics ***) module V82 : sig type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma - val tactic : tac -> unit tactic + + (* [nf_evars=true] applies the evar (assignment) map to the goals + * (conclusion and context) before calling the tactic *) + val tactic : ?nf_evars:bool -> tac -> unit tactic (* normalises the evars in the goals, and stores the result in solution. *) |