Module Pcoq
The parser of Coq
module Parsable : sig ... end
module Entry : sig ... end
val parse_string : 'a Entry.t -> ?loc:Loc.t -> string -> 'a
val eoi_entry : 'a Entry.t -> 'a Entry.t
val map_entry : ('a -> 'b) -> 'a Entry.t -> 'b Entry.t
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
Extending the parser without synchronization
type gram_reinit
= Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
Type of reinitialization data
val grammar_extend : 'a Entry.t -> gram_reinit option -> 'a Extend.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
Extension with parsing rules
type extend_rule
=
|
ExtendRule : 'a Entry.t * gram_reinit option * 'a Extend.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.
Extension with parsing entries
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.
- raises Not_found
if non-existent.
Protection w.r.t. backtrack
val parser_summary_tag : frozen_t Summary.Dyn.tag
val register_grammars_by_name : string -> any_entry list -> unit
val find_grammars_by_name : string -> any_entry list
val freeze : marshallable:bool -> frozen_t
Parsing state handling
val unfreeze : frozen_t -> unit