Module PcoqSource

Deprecated alias for Procq

include module type of struct include Procq end
include Gramlib.Grammar.S with type keyword_state := CLexer.keyword_state and type te := Tok.t and type 'a pattern := 'a Tok.p and type 'a with_gstate := 'a and type 'a with_kwstate := 'a and type 'a with_estate := 'a and type 'a mod_estate := 'a
Sourcetype ty_pattern = Procq.ty_pattern =
  1. | TPattern : 'a Tok.p -> ty_pattern

Type combinators to factor the module type between explicit state passing in Grammar and global state in Procq

Sourcemodule Parsable = Procq.Parsable
Sourcemodule Entry = Procq.Entry
Sourcemodule Symbol = Procq.Symbol
Sourcemodule Rule = Procq.Rule
Sourcemodule Rules = Procq.Rules
Sourcemodule Production = Procq.Production
Sourcetype 'a single_extend_statement = string option * Gramlib.Gramext.g_assoc option * 'a Production.t list
Sourcetype 'a extend_statement = 'a Procq.extend_statement =
  1. | Reuse of string option * 'a Production.t list
    (*

    Extend an existing level by its optional given name. If None, picks the topmost level.

    *)
  2. | Fresh of Gramlib.Gramext.position * 'a single_extend_statement list
    (*

    Create a level at the given position.

    *)
Sourceval generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('b, Gramlib.Grammar.norec, 'c) Symbol.t option
Sourceval level_of_nonterm : ('a, Gramlib.Grammar.norec, 'c) Symbol.t -> string option
Sourcemodule Lookahead = Procq.Lookahead
Sourceval terminal : string -> string Tok.p

When string is not an ident, returns a keyword.

The parser of Rocq is built from three kinds of rule declarations:

  • dynamic rules declared at the evaluation of Rocq files (using e.g. Notation, Infix, or Tactic Notation)
  • static rules explicitly defined in files g_*.mlg
  • static rules macro-generated by ARGUMENT EXTEND, TACTIC EXTEND and VERNAC EXTEND (see e.g. file extratactics.mlg)

Note that parsing a Rocq document is in essence stateful: the parser needs to recognize commands that start proofs and use a different parsing entry point for them.

We thus provide two different interfaces: the "raw" parsing interface, in the style of camlp5, which provides more flexibility, and a more specialize "parse_vernac" one, which will indeed adjust the state as needed.

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

Parse a string

Sourceval parse_string : 'a Entry.t -> ?loc:Loc.t -> string -> 'a
Sourceval eoi_entry : 'a Entry.t -> 'a Entry.t
Sourceval create_generic_entry2 : string -> ('a, Genarg.rlevel) Genarg.abstract_argument_type -> 'a Entry.t
Sourceval register_grammar : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw Entry.t -> unit
Sourceval genarg_grammar : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw Entry.t
Sourcemodule Prim = Procq.Prim
Sourcemodule Constr = Procq.Constr
Sourcemodule Module = Procq.Module
Type-safe grammar extension
Sourceval epsilon_value : ('a -> 'self) -> ('self, _, 'a) Symbol.t -> 'self option
Extending the parser without synchronization
Sourceval grammar_extend : 'a Entry.t -> 'a extend_statement -> unit

Extend the grammar of Rocq, without synchronizing it with the backtracking mechanism. This means that grammar extensions defined this way will survive an undo.

Extending the parser with summary-synchronized commands
module GramState = Procq.GramState

Auxiliary state of the grammar. Any added data must be marshallable.

Extension with parsing rules
Sourcetype 'a grammar_command = 'a Procq.grammar_command

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

Type of reinitialization data

Sourcetype extend_rule = Procq.extend_rule =
  1. | ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule
  2. | ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule
Sourcetype 'a grammar_extension = 'a Procq.grammar_extension = {
  1. gext_fun : 'a -> GramState.t -> extend_rule list * GramState.t;
  2. gext_eq : 'a -> 'a -> bool;
}

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.

Sourceval 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.

Sourceval extend_grammar_command : 'a grammar_command -> 'a -> unit

Extend the grammar of Rocq with the given data.

Extension with parsing entries
Sourcetype ('a, 'b) entry_command = ('a, 'b) Procq.entry_command

Type of synchronized entry creation. The 'a type should be marshallable.

Sourcetype ('a, 'b) entry_extension = ('a, 'b) Procq.entry_extension = {
  1. eext_fun : 'a -> GramState.t -> string list * GramState.t;
  2. eext_eq : 'a -> 'a -> bool;
}

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.

Sourceval 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.

Sourceval extend_entry_command : ('a, 'b) entry_command -> 'a -> 'b Entry.t list

Create new synchronized entries using the provided data.

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

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

Protection w.r.t. backtrack
Sourceval with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
Sourcetype frozen_t = Procq.frozen_t
Sourceval parser_summary_tag : frozen_t Summary.Dyn.tag

Registering grammars by name

Sourceval register_grammars_by_name : string -> Entry.any_t list -> unit
Sourceval find_grammars_by_name : string -> Entry.any_t list
Sourceval freeze : unit -> frozen_t

Parsing state handling

Sourceval unfreeze : frozen_t -> unit
Sourceval get_keyword_state : unit -> CLexer.keyword_state
Sourceval set_keyword_state : CLexer.keyword_state -> unit