diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 61 |
1 files changed, 3 insertions, 58 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 154de1221..ae4f5cab6 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -16,63 +16,18 @@ open Libnames (** The parser of Coq *) +(** DO NOT USE EXTENSION FUNCTIONS IN THIS MODULE. + We only have it here to work with Camlp5. Handwritten grammar extensions + should use the safe [Pcoq.grammar_extend] function below. *) module Gram : sig include Grammar.S with type te = Tok.t -(* Where Grammar.S is - -module type S = - sig - type te = 'x; - type parsable = 'x; - value parsable : Stream.t char -> parsable; - value tokens : string -> list (string * int); - value glexer : Plexing.lexer te; - value set_algorithm : parse_algorithm -> unit; - module Entry : - sig - type e 'a = 'y; - value create : string -> e 'a; - value parse : e 'a -> parsable -> 'a; - value parse_token : e 'a -> Stream.t te -> 'a; - value name : e 'a -> string; - value of_parser : string -> (Stream.t te -> 'a) -> e 'a; - value print : Format.formatter -> e 'a -> unit; - external obj : e 'a -> Gramext.g_entry te = "%identity"; - end - ; - module Unsafe : - sig - value gram_reinit : Plexing.lexer te -> unit; - value clear_entry : Entry.e 'a -> unit; - end - ; - value extend : - Entry.e 'a -> option Gramext.position -> - list - (option string * option Gramext.g_assoc * - list (list (Gramext.g_symbol te) * Gramext.g_action)) -> - unit; - value delete_rule : Entry.e 'a -> list (Gramext.g_symbol te) -> unit; - end - -*) - type 'a entry = 'a Entry.e - type internal_entry = Tok.t Gramext.g_entry - type symbol = Tok.t Gramext.g_symbol - type action = Gramext.g_action - type production_rule = symbol list * action - type single_extend_statement = - string option * Gramext.g_assoc option * production_rule list - type extend_statement = - Gramext.position option * single_extend_statement list type coq_parsable val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable - val action : 'a -> action val entry_create : string -> 'a entry val entry_parse : 'a entry -> coq_parsable -> 'a val entry_print : Format.formatter -> 'a entry -> unit @@ -82,18 +37,8 @@ module type S = val gram_extend : 'a entry -> 'a Extend.extend_statement -> unit - (* Apparently not used *) - val srules' : production_rule list -> symbol - val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a - end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e -module Symbols : sig - - val stoken : Tok.t -> Gram.symbol - val snterm : Gram.internal_entry -> Gram.symbol -end - (** The parser of Coq is built from three kinds of rule declarations: - dynamic rules declared at the evaluation of Coq files (using |