diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 192 |
1 files changed, 192 insertions, 0 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli new file mode 100644 index 00000000..5c6c8354 --- /dev/null +++ b/parsing/pcoq.mli @@ -0,0 +1,192 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: pcoq.mli,v 1.63.2.1 2004/07/16 19:30:40 herbelin Exp $ i*) + +open Util +open Names +open Rawterm +open Ast +open Genarg +open Topconstr +open Tacexpr +open Vernacexpr +open Libnames +open Extend + +(* The lexer and parser of Coq. *) + +val lexer : Token.lexer + +module Gram : Grammar.S with type te = Token.t + +type grammar_object +type typed_entry + +val type_of_typed_entry : typed_entry -> Extend.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 -> + (string option * Gramext.g_assoc option * + (Token.t Gramext.g_symbol list * Gramext.g_action) list) list + -> unit + +val remove_grammars : int -> unit + +val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit + +(* Parse a string *) + +val parse_string : 'a Gram.Entry.e -> string -> 'a +val eoi_entry : 'a Gram.Entry.e -> 'a Gram.Entry.e +val map_entry : ('a -> 'b) -> 'a Gram.Entry.e -> 'b Gram.Entry.e + +(* Entry types *) + +(* Table of Coq's grammar entries *) + +type gram_universe + +val create_univ_if_new : string -> string * gram_universe +val get_univ : string -> string * gram_universe +val get_entry : string * gram_universe -> string -> typed_entry + +val entry_type : string * gram_universe -> string -> entry_type option + +val get_entry_type : string * string -> entry_type +val create_entry_if_new : + string * gram_universe -> string -> entry_type -> unit +val create_entry : + string * gram_universe -> string -> entry_type -> typed_entry +val force_entry_type : + string * gram_universe -> string -> entry_type -> typed_entry + +val create_constr_entry : + string * gram_universe -> string -> constr_expr Gram.Entry.e +val create_generic_entry : string -> ('a, constr_expr,raw_tactic_expr) abstract_argument_type -> 'a Gram.Entry.e +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 + +(* Initial state of the grammar *) + +module Prim : + sig + open Util + open Names + open Libnames + val preident : string Gram.Entry.e + val ident : identifier Gram.Entry.e + val name : name located Gram.Entry.e + 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 integer : int Gram.Entry.e + val string : string Gram.Entry.e + val qualid : qualid 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 + end + +module Constr : + sig + val constr : constr_expr Gram.Entry.e + val constr_eoi : constr_expr Gram.Entry.e + val lconstr : constr_expr Gram.Entry.e + val binder_constr : constr_expr Gram.Entry.e + val operconstr : constr_expr Gram.Entry.e + val ident : identifier Gram.Entry.e + val global : reference Gram.Entry.e + val sort : rawsort Gram.Entry.e + val pattern : cases_pattern_expr Gram.Entry.e + val annot : constr_expr Gram.Entry.e + val constr_pattern : constr_expr Gram.Entry.e + val lconstr_pattern : constr_expr Gram.Entry.e + val binder : (name located list * constr_expr) Gram.Entry.e + val binder_let : local_binder Gram.Entry.e + end + +module Module : + sig + val module_expr : module_ast Gram.Entry.e + val module_type : module_type_ast Gram.Entry.e + end + +module Tactic : + sig + open Rawterm + val castedopenconstr : constr_expr Gram.Entry.e + val constr_with_bindings : constr_expr with_bindings Gram.Entry.e + val bindings : constr_expr bindings Gram.Entry.e + val constrarg : (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 : raw_tactic_expr Gram.Entry.e + val tactic_eoi : raw_tactic_expr Gram.Entry.e + end + +module Vernac_ : + sig + open Decl_kinds + val gallina : vernac_expr Gram.Entry.e + val gallina_ext : vernac_expr Gram.Entry.e + val command : vernac_expr Gram.Entry.e + val syntax : vernac_expr Gram.Entry.e + val vernac : vernac_expr Gram.Entry.e + val vernac_eoi : vernac_expr Gram.Entry.e + end + +val reset_all_grammars : unit -> unit + +(* Registering/resetting the level of an entry *) + +val find_position : + bool -> bool -> Gramext.g_assoc option -> int option -> + Gramext.position option * Gramext.g_assoc option * string option + +val remove_levels : int -> unit |