(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * 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) *) (************************************************************************)
(** Vernacular Extension data *)
(* A vernac classifier provides information about the exectuion of a command:
- vernac_when: encodes if the vernac may alter the parser [thus forcing immediate execution], or if indeed it is pure and parsing can continue without its execution.
- vernac_type: if it is starts, ends, continues a proof or alters the global state or is a control command like BackTo or is a query like Check.
The classification works on the assumption that we have 3 states: parsing, execution (global environment, etc...), and proof state. For example, commands that only alter the proof state are considered safe to delegate to a worker.
*)
type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque
type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop
type vernac_when =
| VtNow
| VtLater
type vernac_classification = (* Start of a proof *)
| VtStartProof of vernac_start (* Command altering the global state, bad for parallel
processing. *)
| VtSideff of vernac_sideff_type (* End of a proof *)
| VtQed of vernac_qed_type (* A proof step *)
| VtProofStep of {
proof_block_detection : proof_block_name option
} (* Queries are commands assumed to be "pure", that is to say, they
don't modify the interpretation state. *)
| VtQuery (* Commands that change the current proof mode *)
| VtProofMode of Pvernac.proof_mode (* To be removed *)
| VtMeta and vernac_start = opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list * vernac_when and opacity_guarantee =
| GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
| Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
and solving_tac = bool(** a terminator *)
and anon_abstracting_tac = bool(** abstracting anonymously its result *)
and proof_block_name = string(** open type of delimiters *)
type vernac_command = ?loc:Loc.t -> atts:Attributes.vernac_flags -> unit -> Vernactypes.typed_vernac
type plugin_args = Genarg.raw_generic_argument list
val type_vernac : Vernacexpr.extend_name -> plugin_args -> vernac_command
(** {5 VERNAC EXTEND} *)
type classifier =
Genarg.raw_generic_argument list ->
atts:Attributes.vernac_flags ->
vernac_classification
This is used by coqpp VERNAC EXTEND. It should not be used directly, use [declare_dynamic_vernac_extend] instead.
Commands added by plugins at Declare ML Module / Require time should provide [plugin].
Commands added without providing [plugin] cannot be removed from the grammar or modified. Not passing [plugin] is possible for non-plugin rocq-runtime commands and deprecated for all other callers.
*) val static_vernac_extend :
plugin:stringoption ->
command:string ->
?classifier:(atts:Attributes.vernac_flags -> string -> vernac_classification) ->
?entry:Vernacexpr.vernac_expr Procq.Entry.t ->
ty_ml list -> unit
(** Used to tell the system that all future vernac extends are from plugins. *) val static_linking_done : unit -> unit
(** Dynamically extend vernacular commands (for instance when importing some module).
Reusing a [command] string will replace previous uses. The result is undefined and probably produces anomalies if the previous grammar rule is still active and was different from the new one.
The polymorphic arguments are as in [TyML].
The declared grammar extension is disabled, one needs to call [Egramml.extend_vernac_command_grammar] in order to enable it. That call should use [undoable:true] to make it possible to disable the extension, e.g. by backtracking over the command which enabled it.
*) val declare_dynamic_vernac_extend
: command:Vernacexpr.extend_name
-> ?entry:Vernacexpr.vernac_expr Procq.Entry.t
-> depr:bool
-> 's (* classifier *)
-> ('r, 's) ty_sig (* grammar *)
-> 'r (* command interpretation *)
-> Vernacexpr.extend_name
(** {5 VERNAC ARGUMENT EXTEND} *)
type'a argument_rule =
| Arg_alias of'a Procq.Entry.t (** This is used because CAMLP5 parser can be dumb about rule factorization,
which sometimes requires two entries to be the same. *)
| Arg_rules of'a Procq.Production.t list (** There is a discrepancy here as we use directly extension rules and thus
entries instead of ty_user_symbol and thus arguments as roots. *)
type'a vernac_argument = {
arg_printer : Environ.env -> Evd.evar_map -> 'a -> Pp.t;
arg_parsing : 'a argument_rule;
}
val vernac_argument_extend : plugin:stringoption -> name:string -> 'a vernac_argument -> 'a Genarg.vernac_genarg_type * 'a Procq.Entry.t
(** Standard constant classifiers *) val classify_as_query : vernac_classification val classify_as_sideeff : vernac_classification val classify_as_proofstep : vernac_classification
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
