diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 28 |
1 files changed, 26 insertions, 2 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 029c437136..e12ccaa636 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -233,6 +233,8 @@ val grammar_extend : 'a Entry.t -> gram_reinit option -> module GramState : Store.S (** Auxiliary state of the grammar. Any added data must be marshallable. *) +(** {6 Extension with parsing rules} *) + type 'a grammar_command (** Type of synchronized parsing extensions. The ['a] type should be marshallable. *) @@ -253,8 +255,30 @@ val create_grammar_command : string -> 'a grammar_extension -> 'a grammar_comman val extend_grammar_command : 'a grammar_command -> 'a -> unit (** Extend the grammar of Coq with the given data. *) -val recover_grammar_command : 'a grammar_command -> 'a list -(** Recover the current stack of grammar extensions. *) +(** {6 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 = '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. + @raise Not_found if non-existent. *) + +(** {6 Protection w.r.t. backtrack} *) val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b |