diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 82 |
1 files changed, 38 insertions, 44 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 2146ad964..ad4d9e501 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -14,13 +14,12 @@ open Genarg open Constrexpr open Tacexpr open Libnames -open Compat open Misctypes open Genredexpr (** The parser of Coq *) -module Gram : GrammarSig +module Gram : Compat.GrammarSig (** The parser of Coq is built from three kinds of rule declarations: @@ -106,28 +105,40 @@ type grammar_object (** Type of reinitialization data *) type gram_reinit = gram_assoc * gram_position +(** 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 ('self, 'a) entry_key = ('self, 'a) Extend.symbol = +| Atoken : Tok.t -> ('self, string) entry_key +| Alist1 : ('self, 'a) entry_key -> ('self, 'a list) entry_key +| Alist1sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key +| Alist0 : ('self, 'a) entry_key -> ('self, 'a list) entry_key +| Alist0sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key +| Aopt : ('self, 'a) entry_key -> ('self, 'a option) entry_key +| Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key +| Aself : ('self, 'self) entry_key +| Anext : ('self, 'self) entry_key +| Aentry : 'a Entry.t -> ('self, 'a) entry_key +| Aentryl : 'a Entry.t * int -> ('self, 'a) entry_key + (** Add one extension at some camlp4 position of some camlp4 entry *) -val grammar_extend : +val unsafe_grammar_extend : grammar_object Gram.entry -> gram_reinit option (** for reinitialization if ever needed *) -> Gram.extend_statment -> unit +val grammar_extend : + 'a Gram.entry -> + gram_reinit option (** for reinitialization if ever needed *) -> + 'a Extend.extend_statment -> unit + (** Remove the last n extensions *) val remove_grammars : int -> unit - - - -(** The type of typed grammar objects *) -type typed_entry - -(** The possible types for extensible grammars *) -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 -val weaken_entry : 'a Gram.entry -> grammar_object Gram.entry - (** Temporary activate camlp4 verbosity *) val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit @@ -138,11 +149,7 @@ 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 *) - -type gram_universe - -(** There are four predefined universes: "prim", "constr", "tactic", "vernac" *) +type gram_universe = Entry.universe val get_univ : string -> gram_universe @@ -151,7 +158,6 @@ val uconstr : gram_universe val utactic : gram_universe val uvernac : gram_universe -val create_entry : gram_universe -> string -> entry_type -> typed_entry val create_generic_entry : string -> ('a, rlevel) abstract_argument_type -> 'a Gram.entry @@ -167,6 +173,7 @@ module Prim : val pattern_identref : Id.t located Gram.entry val base_ident : Id.t Gram.entry val natural : int Gram.entry + val index : int Gram.entry val bigint : Bigint.bigint Gram.entry val integer : int Gram.entry val string : string Gram.entry @@ -258,38 +265,25 @@ val symbol_of_constr_prod_entry_key : gram_assoc option -> constr_entry_key -> bool -> constr_prod_entry_key -> 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 string - | Aentry of string * string +val name_of_entry : 'a Gram.entry -> 'a Entry.t (** Binding general entry keys to symbols *) val symbol_of_prod_entry_key : - prod_entry_key -> Gram.symbol + ('self, 'a) entry_key -> Gram.symbol + +type 's entry_name = EntryName : + 'a raw_abstract_argument_type * ('s, 'a) entry_key -> 's entry_name (** Interpret entry names of the form "ne_constr_list" as entry keys *) +type _ target = TgAny : 's target | TgTactic : int -> raw_tactic_expr target + val interp_entry_name : bool (** true to fail on unknown entry *) -> - int option -> string -> string -> entry_type * prod_entry_key + 's target -> string -> string -> 's entry_name (** Recover the list of all known tactic notation entries. *) -val list_entry_names : unit -> (string * entry_type) list +val list_entry_names : unit -> (string * argument_type) list (** Registering/resetting the level of a constr entry *) |