Module Pcoq

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
type keyword_state
type te
type 'c pattern
type ty_pattern =
| TPattern : 'a pattern -> ty_pattern
type 'a with_gstate

Reader of grammar state

type 'a with_kwstate

Read keyword state

type 'a with_estate

Read entry state

type 'a mod_estate

Read/write entry state

module Parsable : sig ... end
module Entry : sig ... end
module rec Symbol : sig ... end
and Rule : sig ... end
and Rules : sig ... end
module Production : sig ... end
type 'a single_extend_statement = string option * Gramlib.Gramext.g_assoc option * 'a Production.t list
type 'a extend_statement =
| Reuse of string option * 'a Production.t list

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

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

Create a level at the given position.

val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, Gramlib.Grammar.norec, 'c) Symbol.t option
val level_of_nonterm : ('a, Gramlib.Grammar.norec, 'c) Symbol.t -> string option
module Lookahead : sig ... end
val terminal : string -> string Tok.p

When string is not an ident, returns a keyword.

val parse_string : 'a Entry.t -> ?⁠loc:Loc.t -> string -> 'a
val eoi_entry : 'a Entry.t -> 'a Entry.t
val create_generic_entry2 : string -> ('a, Genarg.rlevel) Genarg.abstract_argument_type -> 'a Entry.t
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
module Prim : sig ... end
module Constr : sig ... end
module Module : sig ... end
Type-safe grammar extension
val epsilon_value : ('a -> 'self) -> ('self, _, 'a) Symbol.t -> 'self option
Extending the parser without synchronization
val grammar_extend : 'a Entry.t -> '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.

Extending the parser with summary-synchronized commands
module GramState : Store.S

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

Extension with parsing rules
type 'a grammar_command

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

type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position

Type of reinitialization data

type extend_rule =
| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule
| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule
type 'a grammar_extension = {
gext_fun : 'a -> GramState.t -> extend_rule list * GramState.t;
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.

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.

Extension with parsing entries
type ('a, 'b) entry_command

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

type ('a, 'b) entry_extension = {
eext_fun : 'a -> GramState.t -> string list * GramState.t;
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.

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.

raises Not_found

if non-existent.

Protection w.r.t. backtrack
val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
type frozen_t
val parser_summary_tag : frozen_t Summary.Dyn.tag
val register_grammars_by_name : string -> Entry.any_t list -> unit
val find_grammars_by_name : string -> Entry.any_t list
val freeze : unit -> frozen_t

Parsing state handling

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