Module `Pcoq`

The parser of Coq

module Parsable : sig ... end

module Entry : sig ... end

Dynamic extension of rules

For constr notations, dynamic addition of new rules is done in several steps:

"x + y" (user gives a notation string of type Topconstr.notation) | (together with a constr entry level, e.g. 50, and indications of) | (subentries, e.g. x in constr next level and y constr same level) | | splitting into tokens by Metasyntax.split_notation_string V String "x"; String "+"; String "y" : symbol_token list | | interpreted as a mixed parsing/printing production | by Metasyntax.analyse_notation_tokens V NonTerminal "x"; Terminal "+"; NonTerminal "y" : symbol list | | translated to a parsing production by Metasyntax.make_production V GramConstrNonTerminal (ETConstr (NextLevel,(BorderProd Left,LeftA)), Some "x"); GramConstrTerminal ("","+"); GramConstrNonTerminal (ETConstr (NextLevel,(BorderProd Right,LeftA)), Some "y") : grammar_constr_prod_item list | | Egrammar.make_constr_prod_item V Gramext.g_symbol list which is sent to camlp5

For user level tactic notations, dynamic addition of new rules is also done in several steps:

"f" constr(x) (user gives a Tactic Notation command) | | parsing V TacTerm "f"; TacNonTerm ("constr", Some "x") : grammar_tactic_prod_item_expr list | | Metasyntax.interp_prod_item V GramTerminal "f"; GramNonTerminal (ConstrArgType, Aentry ("constr","constr"), Some "x") : grammar_prod_item list | | Egrammar.make_prod_item V Gramext.g_symbol list

For TACTIC/VERNAC/ARGUMENT EXTEND, addition of new rules is done as follows:

"f" constr(x) (developer gives an EXTEND rule) | | macro-generation in tacextend.mlg/vernacextend.mlg/argextend.mlg V GramTerminal "f"; GramNonTerminal (ConstrArgType, Aentry ("constr","constr"), Some "x") | | Egrammar.make_prod_item V Gramext.g_symbol list

val get_univ : string -> gram_universe
val create_universe : string -> gram_universe
val new_entry : gram_universe -> string -> 'a Entry.t
val uprim : gram_universe
val uconstr : gram_universe
val utactic : gram_universe
val register_grammar : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw Entry.t -> unit
val genarg_grammar : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw Entry.t
val create_generic_entry : gram_universe -> string -> ('a, Genarg.rlevel) Genarg.abstract_argument_type -> 'a Entry.t

module Prim : sig ... end

module Constr : sig ... end

module Module : sig ... end

val epsilon_value : ('a -> 'self) -> ('self, _, 'a) Extend.symbol -> 'self option

type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position: Type of reinitialization data

type 'a single_extend_statement = string option * Gramlib.Gramext.g_assoc option * 'a Extend.production_rule list
type 'a extend_statement = Gramlib.Gramext.position option * 'a single_extend_statement list

val grammar_extend : 'a Entry.t -> gram_reinit option -> 'a extend_statement -> unit: Extend the grammar of Coq, without synchronizing it with the backtracking mechanism. This means that grammar extensions defined this way will survive an undo.

module GramState : Store.S: Auxiliary state of the grammar. Any added data must be marshallable.

type 'a grammar_command: Type of synchronized parsing extensions. The 'a type should be marshallable.

type extend_rule = | ExtendRule : 'a Entry.t * gram_reinit option * 'a extend_statement -> extend_rule
type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t: Grammar extension entry point. Given some 'a and a current grammar state, such a function must produce the list of grammar extensions that will be applied in the same order and kept synchronized w.r.t. the summary, together with a new state. It should be pure.

val create_grammar_command : string -> 'a grammar_extension -> 'a grammar_command: Create a new grammar-modifying command with the given name. The extension function is called to generate the rules for a given data.

val extend_grammar_command : 'a grammar_command -> 'a -> unit: Extend the grammar of Coq with the given data.

type ('a, 'b) entry_command: Type of synchronized entry creation. The 'a type should be marshallable.

type ('a, 'b) entry_extension = 'a -> GramState.t -> string list * GramState.t: Entry extension entry point. Given some 'a and a current grammar state, such a function must produce the list of entry extensions that will be created and kept synchronized w.r.t. the summary, together with a new state. It should be pure.

val create_entry_command : string -> ('a, 'b) entry_extension -> ('a, 'b) entry_command: Create a new entry-creating command with the given name. The extension function is called to generate the new entries for a given data.

val extend_entry_command : ('a, 'b) entry_command -> 'a -> 'b Entry.t list: Create new synchronized entries using the provided data.

val find_custom_entry : ('a, 'b) entry_command -> string -> 'b Entry.t

Find an entry generated by the synchronized system in the current state.