diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 201 |
1 files changed, 108 insertions, 93 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index ada016094..3ec149256 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -15,13 +15,13 @@ open Genarg open Topconstr open Tacexpr open Libnames +open Compat (** The parser of Coq *) -module Gram : Grammar.S with type te = Tok.t +module Gram : GrammarSig -(** - The parser of Coq is built from three kinds of rule declarations: +(** The parser of Coq is built from three kinds of rule declarations: - dynamic rules declared at the evaluation of Coq files (using e.g. Notation, Infix, or Tactic Notation) @@ -96,24 +96,17 @@ module Gram : Grammar.S with type te = Tok.t *) -val gram_token_of_token : Tok.t -> Tok.t Gramext.g_symbol -val gram_token_of_string : string -> Tok.t Gramext.g_symbol +val gram_token_of_token : Tok.t -> Gram.symbol +val gram_token_of_string : string -> Gram.symbol (** The superclass of all grammar entries *) type grammar_object -type camlp4_rule = - Tok.t Gramext.g_symbol list * Gramext.g_action - -type camlp4_entry_rules = - (** first two parameters are name and assoc iff a level is created *) - string option * Gramext.g_assoc option * camlp4_rule list - (** Add one extension at some camlp4 position of some camlp4 entry *) val grammar_extend : - grammar_object Gram.Entry.e -> Gramext.position option -> - (** for reinitialization if ever needed: *) Gramext.g_assoc option -> - camlp4_entry_rules list -> unit + grammar_object Gram.entry -> + gram_assoc option (** for reinitialization if ever needed *) -> + Gram.extend_statment -> unit (** Remove the last n extensions *) val remove_grammars : int -> unit @@ -128,8 +121,8 @@ type typed_entry 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 object_of_typed_entry : typed_entry -> grammar_object Gram.entry +val weaken_entry : 'a Gram.entry -> grammar_object Gram.entry (** Temporary activate camlp4 verbosity *) @@ -137,9 +130,9 @@ 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 +val parse_string : 'a Gram.entry -> string -> 'a +val eoi_entry : 'a Gram.entry -> 'a Gram.entry +val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry (** Table of Coq statically defined grammar entries *) @@ -161,130 +154,152 @@ val get_entry_type : gram_universe -> string -> entry_type val create_entry : gram_universe -> string -> entry_type -> typed_entry val create_generic_entry : string -> ('a, rlevel) abstract_argument_type -> - 'a Gram.Entry.e + 'a Gram.entry 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 pattern_ident : identifier Gram.Entry.e - val pattern_identref : identifier located Gram.Entry.e - val base_ident : identifier Gram.Entry.e - val natural : int 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 by_notation : (loc * string * string option) Gram.Entry.e - val smart_global : reference or_by_notation Gram.Entry.e - val dirpath : dir_path Gram.Entry.e - val ne_string : string Gram.Entry.e - val ne_lstring : string located Gram.Entry.e - val var : identifier located Gram.Entry.e + val preident : string Gram.entry + val ident : identifier Gram.entry + val name : name located Gram.entry + val identref : identifier located Gram.entry + val pattern_ident : identifier Gram.entry + val pattern_identref : identifier located Gram.entry + val base_ident : identifier Gram.entry + val natural : int Gram.entry + val bigint : Bigint.bigint Gram.entry + val integer : int Gram.entry + val string : string Gram.entry + val qualid : qualid located Gram.entry + val fullyqualid : identifier list located Gram.entry + val reference : reference Gram.entry + val by_notation : (loc * string * string option) Gram.entry + val smart_global : reference or_by_notation Gram.entry + val dirpath : dir_path Gram.entry + val ne_string : string Gram.entry + val ne_lstring : string located Gram.entry + val var : identifier located Gram.entry 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 constr_pattern : constr_expr Gram.Entry.e - val lconstr_pattern : constr_expr Gram.Entry.e - val binder : (name located list * binder_kind * constr_expr) Gram.Entry.e - val binder_let : local_binder list Gram.Entry.e - val binders_let : local_binder list Gram.Entry.e - val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e - val typeclass_constraint : (name located * bool * constr_expr) Gram.Entry.e - val record_declaration : constr_expr Gram.Entry.e - val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e + val constr : constr_expr Gram.entry + val constr_eoi : constr_expr Gram.entry + val lconstr : constr_expr Gram.entry + val binder_constr : constr_expr Gram.entry + val operconstr : constr_expr Gram.entry + val ident : identifier Gram.entry + val global : reference Gram.entry + val sort : rawsort Gram.entry + val pattern : cases_pattern_expr Gram.entry + val constr_pattern : constr_expr Gram.entry + val lconstr_pattern : constr_expr Gram.entry + val binder : (name located list * binder_kind * constr_expr) Gram.entry + val binder_let : local_binder list Gram.entry + val binders_let : local_binder list Gram.entry + val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.entry + val typeclass_constraint : (name located * bool * constr_expr) Gram.entry + val record_declaration : constr_expr Gram.entry + val appl_arg : (constr_expr * explicitation located option) Gram.entry end module Module : sig - val module_expr : module_ast Gram.Entry.e - val module_type : module_ast Gram.Entry.e + val module_expr : module_ast Gram.entry + val module_type : module_ast Gram.entry end module Tactic : sig open Rawterm - val open_constr : 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 - val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) 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 located Gram.Entry.e - val tactic_arg : raw_tactic_arg Gram.Entry.e - val tactic_expr : raw_tactic_expr Gram.Entry.e - val binder_tactic : raw_tactic_expr Gram.Entry.e - val tactic : raw_tactic_expr Gram.Entry.e - val tactic_eoi : raw_tactic_expr Gram.Entry.e + val open_constr : open_constr_expr Gram.entry + val casted_open_constr : open_constr_expr Gram.entry + val constr_with_bindings : constr_expr with_bindings Gram.entry + val bindings : constr_expr bindings Gram.entry + val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry + val quantified_hypothesis : quantified_hypothesis Gram.entry + val int_or_var : int or_var Gram.entry + val red_expr : raw_red_expr Gram.entry + val simple_tactic : raw_atomic_tactic_expr Gram.entry + val simple_intropattern : Genarg.intro_pattern_expr located Gram.entry + val tactic_arg : raw_tactic_arg Gram.entry + val tactic_expr : raw_tactic_expr Gram.entry + val binder_tactic : raw_tactic_expr Gram.entry + val tactic : raw_tactic_expr Gram.entry + val tactic_eoi : raw_tactic_expr Gram.entry 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 + 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 : vernac_expr Gram.entry + val vernac_eoi : vernac_expr Gram.entry end (** The main entry: reads an optional vernac command *) -val main_entry : (loc * vernac_expr) option Gram.Entry.e +val main_entry : (loc * vernac_expr) option Gram.entry (** Mapping formal entries into concrete ones *) (** Binding constr entry keys to entries and symbols *) val interp_constr_entry_key : bool (** true for cases_pattern *) -> - constr_entry_key -> grammar_object Gram.Entry.e * int option + constr_entry_key -> grammar_object Gram.entry * int option -val symbol_of_constr_prod_entry_key : Gramext.g_assoc option -> +val symbol_of_constr_prod_entry_key : gram_assoc option -> constr_entry_key -> bool -> constr_prod_entry_key -> - Tok.t Gramext.g_symbol + Gram.symbol + +(** General entry keys *) + +(** This intermediate abstract representation of entries can + both be reified into mlexpr for the ML extensions and + dynamically interpreted as entries for the Coq level extensions +*) + +type prod_entry_key = + | Alist1 of prod_entry_key + | Alist1sep of prod_entry_key * string + | Alist0 of prod_entry_key + | Alist0sep of prod_entry_key * string + | Aopt of prod_entry_key + | Amodifiers of prod_entry_key + | Aself + | Anext + | Atactic of int + | Agram of Gram.internal_entry + | Aentry of string * string (** Binding general entry keys to symbols *) val symbol_of_prod_entry_key : - Gram.te prod_entry_key -> Gram.te Gramext.g_symbol + prod_entry_key -> Gram.symbol (** Interpret entry names of the form "ne_constr_list" as entry keys *) val interp_entry_name : bool (** true to fail on unknown entry *) -> - int option -> string -> string -> entry_type * Gram.te prod_entry_key + int option -> string -> string -> entry_type * prod_entry_key (** Registering/resetting the level of a constr entry *) val find_position : bool (** true if for creation in pattern entry; false if in constr entry *) -> - Gramext.g_assoc option -> int option -> - Gramext.position option * Gramext.g_assoc option * string option * - (** for reinitialization: *) Gramext.g_assoc option + gram_assoc option -> int option -> + gram_position option * gram_assoc option * string option * + (** for reinitialization: *) gram_assoc option val synchronize_level_positions : unit -> unit val register_empty_levels : bool -> int list -> - (Gramext.position option * Gramext.g_assoc option * - string option * Gramext.g_assoc option) list + (gram_position option * gram_assoc option * + string option * gram_assoc option) list val remove_levels : int -> unit + +val level_of_snterml : Gram.symbol -> int |