diff options
author | 2009-04-27 13:43:41 +0000 | |
---|---|---|
committer | 2009-04-27 13:43:41 +0000 | |
commit | f90fde30288f67b167b68bfd32363eaa20644c5f (patch) | |
tree | 00faf9b0c6aa8749d3ec67b8fdc4f14044535b1c /parsing/pcoq.mli | |
parent | 3f40ddb52ed52ea1e1939feaecf952269335500f (diff) |
- Cleaning (unification of ML names, removal of obsolete code,
reorganization of code) and documentation (in pcoq.mli) of the code
for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic
Notation, Notation); merged the two copies of interp_entry_name to
avoid they diverge.
- Added support in Tactic Notation for ne_..._list_sep in general and
for (ne_)ident_list(_sep) in particular.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12108 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pcoq.mli')
-rw-r--r-- | parsing/pcoq.mli | 227 |
1 files changed, 140 insertions, 87 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 97a47dcc4..02db8d55d 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -12,41 +12,125 @@ open Util open Names open Rawterm open Extend +open Vernacexpr open Genarg open Topconstr open Tacexpr -open Vernacexpr open Libnames -(* The lexer and parser of Coq. *) - -val lexer : Compat.lexer +(**********************************************************************) +(* The parser of Coq *) module Gram : Grammar.S with type te = Compat.token +(**********************************************************************) +(* 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) + - static rules explicitly defined in files g_*.ml4 + - static rules macro-generated by ARGUMENT EXTEND, TACTIC EXTEND and + VERNAC EXTEND (see e.g. file extratactics.ml4) +*) + +(* Dynamic extension of rules + + For constr notations, dynamic addition of new rules is done in + several steps: + + - "x + y" (user gives a notation string of type Topconstr.notation) + | (together with a constr entry level, e.g. 50, and indications of) + | (subentries, e.g. x in constr next level and y constr same level) + | + | spliting into tokens by Metasyntax.split_notation_string + V + [String "x"; String "+"; String "y"] : symbol_token list + | + | interpreted as a mixed parsing/printing production + | by Metasyntax.analyse_notation_tokens + V + [NonTerminal "x"; Terminal "+"; NonTerminal "y"] : symbol list + | + | translated to a parsing production by Metasyntax.make_production + V + [GramConstrNonTerminal (ETConstr (NextLevel,(BorderProd Left,LeftA)), + Some "x"); + GramConstrTerminal ("","+"); + GramConstrNonTerminal (ETConstr (NextLevel,(BorderProd Right,LeftA)), + Some "y")] + : grammar_constr_prod_item list + | + | Egrammar.make_constr_prod_item + V + Gramext.g_symbol list which is sent to camlp4 + + For user level tactic notations, dynamic addition of new rules is + also done in several steps: + + - "f" constr(x) (user gives a Tactic Notation command) + | + | parsing + V + [TacTerm "f"; TacNonTerm ("constr", Some "x")] + : grammar_tactic_prod_item_expr list + | + | Metasyntax.interp_prod_item + V + [GramTerminal "f"; + GramNonTerminal (ConstrArgType, Aentry ("constr","constr"), Some "x")] + : grammar_prod_item list + | + | Egrammar.make_prod_item + V + Gramext.g_symbol list + + For TACTIC/VERNAC/ARGUMENT EXTEND, addition of new rules is done as follows: + + - "f" constr(x) (developer gives an EXTEND rule) + | + | macro-generation in tacextend.ml4/vernacextend.ml4/argextend.ml4 + V + [GramTerminal "f"; + GramNonTerminal (ConstrArgType, Aentry ("constr","constr"), Some "x")] + | + | Egrammar.make_prod_item + V + Gramext.g_symbol list + +*) + (* The superclass of all grammar entries *) type grammar_object +type camlp4_rule = + Compat.token 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 + +(* 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.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 - -val grammar_extend : - grammar_object Gram.Entry.e -> Gramext.position option -> - (* for reinitialization if ever: *) Gramext.g_assoc option -> - (string option * Gramext.g_assoc option * - (Compat.token Gramext.g_symbol list * Gramext.g_action) list) list - -> unit - -val remove_grammars : int -> unit +(* Temporary activate camlp4 verbosity *) val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit @@ -56,73 +140,28 @@ 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 *) +(**********************************************************************) +(* Table of Coq statically defined 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, rlevel) 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 - -(* Tactics as arguments *) +(* There are four predefined universes: "prim", "constr", "tactic", "vernac" *) -val tactic_main_level : int +val get_univ : string -> gram_universe -val rawwit_tactic : int -> (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic : int -> (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic : int -> (glob_tactic_expr,tlevel) abstract_argument_type +val uprim : gram_universe +val uconstr : gram_universe +val utactic : gram_universe +val uvernac : gram_universe -val rawwit_tactic0 : (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic0 : (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic0 : (glob_tactic_expr,tlevel) abstract_argument_type +(* +val get_entry : gram_universe -> string -> typed_entry +val get_entry_type : gram_universe -> string -> entry_type +*) -val rawwit_tactic1 : (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic1 : (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic1 : (glob_tactic_expr,tlevel) abstract_argument_type - -val rawwit_tactic2 : (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic2 : (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic2 : (glob_tactic_expr,tlevel) abstract_argument_type - -val rawwit_tactic3 : (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic3 : (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic3 : (glob_tactic_expr,tlevel) abstract_argument_type - -val rawwit_tactic4 : (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic4 : (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic4 : (glob_tactic_expr,tlevel) abstract_argument_type - -val rawwit_tactic5 : (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic5 : (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic5 : (glob_tactic_expr,tlevel) abstract_argument_type - -val is_tactic_genarg : argument_type -> bool - -val tactic_genarg_level : string -> int option - -(* The main entry: reads an optional vernac command *) - -val main_entry : (loc * vernac_expr) option Gram.Entry.e - -(* Initial state of the grammar *) +val create_entry : gram_universe -> string -> entry_type -> typed_entry +val create_generic_entry : string -> ('a, rlevel) abstract_argument_type -> + 'a Gram.Entry.e module Prim : sig @@ -204,22 +243,38 @@ module Vernac_ : val command : vernac_expr Gram.Entry.e val syntax : vernac_expr Gram.Entry.e val vernac : vernac_expr Gram.Entry.e - - (* MMode *) - + val vernac_eoi : vernac_expr Gram.Entry.e val proof_instr : Decl_expr.raw_proof_instr Gram.Entry.e + end - (*/ MMode *) +(* The main entry: reads an optional vernac command *) +val main_entry : (loc * vernac_expr) option Gram.Entry.e - val vernac_eoi : vernac_expr Gram.Entry.e - end +(**********************************************************************) +(* Mapping formal entries into concrete ones *) -(* Binding entry names to campl4 entries *) +(* Binding constr entry keys to entries and symbols *) -val symbol_of_production : Gramext.g_assoc option -> constr_entry -> - bool -> constr_production_entry -> Compat.token Gramext.g_symbol +val interp_constr_entry_key : bool (* true for cases_pattern *) -> + constr_entry_key -> grammar_object Gram.Entry.e * int option -(* Registering/resetting the level of an entry *) +val symbol_of_constr_prod_entry_key : Gramext.g_assoc option -> + constr_entry_key -> bool -> constr_prod_entry_key -> + Compat.token Gramext.g_symbol + +(* Binding general entry keys to symbols *) + +val symbol_of_prod_entry_key : + Gram.te prod_entry_key -> Gram.te Gramext.g_symbol + +(**********************************************************************) +(* Interpret entry names of the form "ne_constr_list" as entry keys *) + +val interp_entry_name : int option -> string -> string -> + entry_type * Gram.te 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 *) -> @@ -234,5 +289,3 @@ val register_empty_levels : bool -> int list -> string option * Gramext.g_assoc option) list val remove_levels : int -> unit - -val coerce_global_to_id : reference -> identifier |