diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 49 |
1 files changed, 17 insertions, 32 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 9f186224b..9a45bc973 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -10,12 +10,9 @@ open Names open Extend -open Vernacexpr open Genarg open Constrexpr open Libnames -open Misctypes -open Genredexpr (** The parser of Coq *) @@ -67,10 +64,10 @@ module type S = type symbol = Tok.t Gramext.g_symbol type action = Gramext.g_action type production_rule = symbol list * action - type single_extend_statment = + type single_extend_statement = string option * Gramext.g_assoc option * production_rule list - type extend_statment = - Gramext.position option * single_extend_statment list + type extend_statement = + Gramext.position option * single_extend_statement list type coq_parsable @@ -89,6 +86,12 @@ module type S = 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 @@ -177,11 +180,14 @@ val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry type gram_universe val get_univ : string -> gram_universe +val create_universe : string -> gram_universe + +val new_entry : gram_universe -> string -> 'a Gram.entry val uprim : gram_universe val uconstr : gram_universe val utactic : gram_universe -val uvernac : gram_universe + val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry @@ -227,8 +233,8 @@ module Constr : val operconstr : constr_expr Gram.entry val ident : Id.t Gram.entry val global : reference Gram.entry - val universe_level : glob_level Gram.entry - val sort : glob_sort Gram.entry + val universe_level : Glob_term.glob_level Gram.entry + val sort : Glob_term.glob_sort Gram.entry val sort_family : Sorts.family Gram.entry val pattern : cases_pattern_expr Gram.entry val constr_pattern : constr_expr Gram.entry @@ -249,27 +255,6 @@ module Module : val module_type : module_ast Gram.entry end -module Vernac_ : - sig - val gallina : vernac_expr Gram.entry - val gallina_ext : vernac_expr Gram.entry - val command : vernac_expr Gram.entry - val syntax : vernac_expr Gram.entry - val vernac_control : vernac_control Gram.entry - val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry - val noedit_mode : vernac_expr Gram.entry - val command_entry : vernac_expr Gram.entry - val red_expr : raw_red_expr Gram.entry - val hint_info : Vernacexpr.hint_info_expr Gram.entry - end - -(** The main entry: reads an optional vernac command *) -val main_entry : (Loc.t * vernac_control) option Gram.entry - -(** Handling of the proof mode entry *) -val get_command_entry : unit -> vernac_expr Gram.entry -val set_command_entry : vernac_expr Gram.entry -> unit - val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option (** {5 Extending the parser without synchronization} *) @@ -278,7 +263,7 @@ type gram_reinit = gram_assoc * gram_position (** Type of reinitialization data *) val grammar_extend : 'a Gram.entry -> gram_reinit option -> - 'a Extend.extend_statment -> unit + '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. *) @@ -293,7 +278,7 @@ type 'a grammar_command marshallable. *) type extend_rule = -| ExtendRule : 'a Gram.entry * gram_reinit option * 'a extend_statment -> extend_rule +| ExtendRule : 'a Gram.entry * gram_reinit option * 'a 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, |