diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 58 |
1 files changed, 22 insertions, 36 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 15a2c2cc..fe6fd083 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -6,18 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pcoq.mli,v 1.63.2.3 2005/06/21 15:31:12 herbelin Exp $ i*) +(*i $Id: pcoq.mli 7826 2006-01-09 22:00:34Z herbelin $ i*) open Util open Names open Rawterm -open Ast +open Extend open Genarg open Topconstr open Tacexpr open Vernacexpr open Libnames -open Extend (* The lexer and parser of Coq. *) @@ -25,21 +24,23 @@ val lexer : Token.lexer module Gram : Grammar.S with type te = Token.t +(* The superclass of all grammar entries *) type grammar_object + +(* The type of typed grammar objects *) type typed_entry -val type_of_typed_entry : typed_entry -> Extend.entry_type +type entry_type = argument_type + +val type_of_typed_entry : typed_entry -> entry_type val object_of_typed_entry : typed_entry -> grammar_object Gram.Entry.e val weaken_entry : 'a Gram.Entry.e -> grammar_object Gram.Entry.e val get_constr_entry : bool -> constr_entry -> grammar_object Gram.Entry.e * int option * bool -val symbol_of_production : Gramext.g_assoc option -> constr_entry -> - bool -> constr_production_entry -> Token.t Gramext.g_symbol - val grammar_extend : - 'a Gram.Entry.e -> Gramext.position option -> + grammar_object Gram.Entry.e -> Gramext.position option -> (string option * Gramext.g_assoc option * (Token.t Gramext.g_symbol list * Gramext.g_action) list) list -> unit @@ -80,22 +81,6 @@ val create_generic_entry : string -> ('a, constr_expr,raw_tactic_expr) abstract_ val get_generic_entry : string -> grammar_object Gram.Entry.e val get_generic_entry_type : string * gram_universe -> string -> Genarg.argument_type -type parser_type = - | ConstrParser - | CasesPatternParser - -val entry_type_of_parser : parser_type -> entry_type option -val parser_type_from_name : string -> parser_type - -(* Quotations in ast parser *) -val define_ast_quotation : bool -> string -> (Coqast.t Gram.Entry.e) -> unit -val set_globalizer : (constr_expr -> Coqast.t) -> unit - -(* The default parser for actions in grammar rules *) - -val default_action_parser : dynamic_grammar Gram.Entry.e -val set_default_action_parser : parser_type -> unit - (* The main entry: reads an optional vernac command *) val main_entry : (loc * vernac_expr) option Gram.Entry.e @@ -113,20 +98,15 @@ module Prim : val identref : identifier located Gram.Entry.e val base_ident : identifier Gram.Entry.e val natural : int Gram.Entry.e - val bigint : Bignat.bigint Gram.Entry.e + val bigint : Bigint.bigint Gram.Entry.e val integer : int Gram.Entry.e val string : string Gram.Entry.e val qualid : qualid located Gram.Entry.e + val fullyqualid : identifier list located Gram.Entry.e val reference : reference Gram.Entry.e val dirpath : dir_path Gram.Entry.e val ne_string : string Gram.Entry.e - val hyp : identifier Gram.Entry.e - (* v7 only entries *) - val astpat: typed_ast Gram.Entry.e - val ast : Coqast.t Gram.Entry.e - val astlist : Coqast.t list Gram.Entry.e - val ast_eoi : Coqast.t Gram.Entry.e - val var : identifier Gram.Entry.e + val var : identifier located Gram.Entry.e end module Constr : @@ -157,17 +137,18 @@ module Tactic : sig open Rawterm val open_constr : open_constr_expr Gram.Entry.e - val castedopenconstr : open_constr_expr Gram.Entry.e + val casted_open_constr : open_constr_expr Gram.Entry.e val constr_with_bindings : constr_expr with_bindings Gram.Entry.e val bindings : constr_expr bindings Gram.Entry.e -(*v7*) val constrarg : (constr_expr,reference) may_eval Gram.Entry.e -(*v8*) val constr_may_eval : (constr_expr,reference) may_eval Gram.Entry.e + val constr_may_eval : (constr_expr,reference) may_eval Gram.Entry.e val quantified_hypothesis : quantified_hypothesis Gram.Entry.e val int_or_var : int or_var Gram.Entry.e val red_expr : raw_red_expr Gram.Entry.e val simple_tactic : raw_atomic_tactic_expr Gram.Entry.e val simple_intropattern : Genarg.intro_pattern_expr Gram.Entry.e val tactic_arg : raw_tactic_arg Gram.Entry.e + val tactic_expr : raw_tactic_expr Gram.Entry.e + val tactic_main_level : int val tactic : raw_tactic_expr Gram.Entry.e val tactic_eoi : raw_tactic_expr Gram.Entry.e end @@ -183,7 +164,10 @@ module Vernac_ : val vernac_eoi : vernac_expr Gram.Entry.e end -val reset_all_grammars : unit -> unit +(* Binding entry names to campl4 entries *) + +val symbol_of_production : Gramext.g_assoc option -> constr_entry -> + bool -> constr_production_entry -> Token.t Gramext.g_symbol (* Registering/resetting the level of an entry *) @@ -192,3 +176,5 @@ val find_position : Gramext.position option * Gramext.g_assoc option * string option val remove_levels : int -> unit + +val coerce_global_to_id : reference -> identifier |