diff options
Diffstat (limited to 'engine/proofview.mli')
| -rw-r--r-- | engine/proofview.mli | 145 |
1 files changed, 70 insertions, 75 deletions
diff --git a/engine/proofview.mli b/engine/proofview.mli index 90be2f90..e7be6655 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-2016 *) +(* * 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] @@ -13,7 +15,7 @@ state and returning a value of type ['a]. *) open Util -open Term +open EConstr (** Main state of tactics *) type proofview @@ -25,7 +27,7 @@ type proofview new nearly identical function everytime. Hence the generic name. *) (* In this version: returns the list of focused goals together with the [evar_map] context. *) -val proofview : proofview -> Goal.goal list * Evd.evar_map +val proofview : proofview -> Evar.t list * Evd.evar_map (** {6 Starting and querying a proof view} *) @@ -43,7 +45,7 @@ val compact : entry -> proofview -> entry * proofview empty [evar_map] (indeed a proof can be triggered by an incomplete pretyping), [init] takes an additional argument to represent the initial [evar_map]. *) -val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview +val init : Evd.evar_map -> (Environ.env * types) list -> entry * proofview (** A [telescope] is a list of environment and conclusion like in {!init}, except that each element may depend on the previous @@ -52,7 +54,7 @@ val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview [evar_map] is threaded in state passing style. *) type telescope = | TNil of Evd.evar_map - | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope) + | TCons of Environ.env * Evd.evar_map * types * (Evd.evar_map -> constr -> telescope) (** Like {!init}, but goals are allowed to be dependent on one another. Dependencies between goals is represented with the type @@ -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} *) @@ -88,7 +98,7 @@ type focus_context new nearly identical function everytime. Hence the generic name. *) (* In this version: the goals in the context, as a "zipper" (the first list is in reversed order). *) -val focus_context : focus_context -> Goal.goal list * Goal.goal list +val focus_context : focus_context -> Evar.t list * Evar.t list (** [focus i j] focuses a proofview on the goals from index [i] to index [j] (inclusive, goals are indexed from [1]). I.e. goals @@ -148,7 +158,7 @@ type +'a tactic {!Logic_monad.TacticFailure}*) val apply : Environ.env -> 'a tactic -> proofview -> 'a * proofview - * (bool*Goal.goal list*Goal.goal list) + * (bool*Evar.t list*Evar.t list) * Proofview_monad.Info.tree (** {7 Monadic primitives} *) @@ -235,7 +245,7 @@ val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic This hook is used to add a suggestion about bullets when applicable. *) exception NoSuchGoals of int -val set_nosuchgoals_hook: (int -> Pp.std_ppcmds) -> unit +val set_nosuchgoals_hook: (int -> Pp.t) -> unit val tclFOCUS : int -> int -> 'a tactic -> 'a tactic @@ -292,6 +302,7 @@ val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tact independent of backtracking in another. It is equivalent to [tclEXTEND [] tac []]. *) val tclINDEPENDENT : unit tactic -> unit tactic +val tclINDEPENDENTL: 'a tactic -> 'a list tactic (** {7 Goal manipulation} *) @@ -303,12 +314,12 @@ val shelve : unit tactic (** Shelves the given list of goals, which might include some that are under focus and some that aren't. All the goals are placed on the shelf for later use (or being solved by side-effects). *) -val shelve_goals : Goal.goal list -> unit tactic +val shelve_goals : Evar.t list -> unit tactic (** [unifiable sigma g l] checks whether [g] appears in another subgoal of [l]. The list [l] may contain [g], but it does not affect the result. Used by [shelve_unifiable]. *) -val unifiable : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool +val unifiable : Evd.evar_map -> Evar.t -> Evar.t list -> bool (** Shelves the unifiable goals under focus, i.e. the goals which appear in other goals under focus (the unfocused goals are not @@ -321,15 +332,15 @@ val guard_no_unifiable : Names.Name.t list option tactic (** [unshelve l p] adds all the goals in [l] at the end of the focused goals of p *) -val unshelve : Goal.goal list -> proofview -> proofview +val unshelve : Evar.t list -> proofview -> proofview (** [depends_on g1 g2 sigma] checks if g1 occurs in the type/ctx of g2 *) -val depends_on : Evd.evar_map -> Goal.goal -> Goal.goal -> bool +val depends_on : Evd.evar_map -> Evar.t -> Evar.t -> bool (** [with_shelf tac] executes [tac] and returns its result together with the set of goals shelved by [tac]. The current shelf is unchanged and the returned list contains only unsolved goals. *) -val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic +val with_shelf : 'a tactic -> (Evar.t list * 'a) tactic (** If [n] is positive, [cycle n] puts the [n] first goal last. If [n] is negative, then it puts the [n] last goals first.*) @@ -415,17 +426,29 @@ 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 : Goal.goal 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 : Goal.goal list -> unit tactic + val tclSETGOALS : Proofview_monad.goal_with_state list -> unit tactic (** [tclGETGOALS] returns the list of goals under focus. *) - val tclGETGOALS : Goal.goal 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 : Evd.evar_universe_context -> unit tactic + val tclEVARUNIVCONTEXT : UState.t -> unit tactic (** Clears the future goals store in the proof view. *) val reset_future_goals : proofview -> proofview @@ -460,79 +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. - - The second parameter is a stage indicating where the goal belongs. See - module {!Sigma}. - *) - type ('a, 'r) t + (** Type of goals. *) + type t (** Assume that you do not need the goal to be normalized. *) - val assume : ('a, 'r) t -> ([ `NF ], 'r) t + val assume : t -> t + [@@ocaml.deprecated "Normalization is enforced by EConstr, [assume] is not needed anymore"] (** Normalises the argument goal. *) - val normalize : ('a, 'r) t -> ([ `NF ], 'r) 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 : ([ `NF ], 'r) t -> Term.constr - val hyps : ([ `NF ], 'r) t -> Context.Named.t - val env : ('a, 'r) t -> Environ.env - val sigma : ('a, 'r) t -> 'r Sigma.t - val extra : ('a, 'r) t -> Evd.Store.t - - (** Returns the goal's conclusion even if the goal is not - normalised. *) - val raw_concl : ('a, 'r) t -> Term.constr - - type ('a, 'b) enter = - { enter : 'r. ('a, 'r) t -> 'b } + 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 ], unit tactic) enter -> unit tactic + val nf_enter : (t -> unit tactic) -> unit tactic (** Like {!nf_enter}, but does not normalize the goal beforehand. *) - val enter : ([ `LZ ], unit tactic) enter -> unit tactic + val enter : (t -> unit tactic) -> unit tactic (** Like {!enter}, but assumes exactly one goal under focus, raising *) - (** an error otherwise. *) - val enter_one : ([ `LZ ], 'a tactic) enter -> 'a tactic - - type ('a, 'b) s_enter = - { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma } - - (** A variant of {!enter} allows to work with a monotonic state. The evarmap - returned by the argument is put back into the current state before firing - the returned tactic. *) - val s_enter : ([ `LZ ], unit tactic) s_enter -> unit tactic - - (** Like {!s_enter}, but normalizes the goal beforehand. *) - val nf_s_enter : ([ `NF ], unit tactic) s_enter -> unit tactic + (** a fatal error otherwise. *) + 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 ], 'r) 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, 'r) t -> bool tactic + val unsolved : t -> bool tactic (** Compatibility: avoid if possible *) - val goal : ([ `NF ], 'r) t -> Evar.t - - (** Every goal is valid at a later stage. FIXME: take a later evarmap *) - val lift : ('a, 'r) t -> ('r, 's) Sigma.le -> ('a, 's) t + val goal : t -> Evar.t + val print : t -> Goal.goal Evd.sigma end @@ -548,7 +543,7 @@ module Trace : sig val log : Proofview_monad.lazy_msg -> unit tactic val name_tactic : Proofview_monad.lazy_msg -> 'a tactic -> 'a tactic - val pr_info : ?lvl:int -> Proofview_monad.Info.tree -> Pp.std_ppcmds + val pr_info : ?lvl:int -> Proofview_monad.Info.tree -> Pp.t end @@ -569,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. *) @@ -585,11 +583,12 @@ module V82 : sig (* Returns the open goals of the proofview together with the evar_map to interpret them. *) val goals : proofview -> Evar.t list Evd.sigma + [@@ocaml.deprecated "Use [Proofview.proofview]"] val top_goals : entry -> proofview -> Evar.t list Evd.sigma - + (* returns the existential variable used to start the proof *) - val top_evars : entry -> Evd.evar list + val top_evars : entry -> Evar.t list (* Caution: this function loses quite a bit of information. It should be avoided as much as possible. It should work as @@ -619,8 +618,4 @@ module Notations : sig (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *) val (<+>) : 'a tactic -> 'a tactic -> 'a tactic - type ('a, 'b) enter = ('a, 'b) Goal.enter = - { enter : 'r. ('a, 'r) Goal.t -> 'b } - type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter = - { s_enter : 'r. ('a, 'r) Goal.t -> ('b, 'r) Sigma.sigma } end |