diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 245 |
1 files changed, 150 insertions, 95 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 0a4b349f..ed370a99 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -6,47 +6,131 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pcoq.mli 11784 2009-01-14 11:36:32Z herbelin $ i*) +(*i $Id$ i*) 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 *) - -val tactic_main_level : int +(* There are four predefined universes: "prim", "constr", "tactic", "vernac" *) -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 get_univ : string -> 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 uprim : gram_universe +val uconstr : gram_universe +val utactic : gram_universe +val uvernac : gram_universe -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 get_entry : gram_universe -> string -> typed_entry +val get_entry_type : gram_universe -> string -> entry_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 @@ -143,8 +182,11 @@ module Prim : 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 end @@ -159,7 +201,6 @@ module Constr : 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 * binder_kind * constr_expr) Gram.Entry.e @@ -171,10 +212,10 @@ module Constr : val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e end -module Module : +module Module : sig val module_expr : module_ast Gram.Entry.e - val module_type : module_type_ast Gram.Entry.e + val module_type : module_ast Gram.Entry.e end module Tactic : @@ -184,7 +225,7 @@ module Tactic : 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) may_eval 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 @@ -205,27 +246,43 @@ 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 + +(* The main entry: reads an optional vernac command *) +val main_entry : (loc * vernac_expr) option Gram.Entry.e - (*/ MMode *) +(**********************************************************************) +(* Mapping formal entries into concrete ones *) - val vernac_eoi : vernac_expr Gram.Entry.e - end +(* Binding constr entry keys to entries and symbols *) -(* Binding entry names to campl4 entries *) +val interp_constr_entry_key : bool (* true for cases_pattern *) -> + constr_entry_key -> grammar_object Gram.Entry.e * int option -val symbol_of_production : Gramext.g_assoc option -> constr_entry -> - bool -> constr_production_entry -> Compat.token Gramext.g_symbol +val symbol_of_constr_prod_entry_key : Gramext.g_assoc option -> + constr_entry_key -> bool -> constr_prod_entry_key -> + Compat.token Gramext.g_symbol -(* Registering/resetting the level of an entry *) +(* Binding general entry keys to symbols *) -val find_position : +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 : bool (* true to fail on unknown entry *) -> + 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 *) -> Gramext.g_assoc option -> int option -> - Gramext.position option * Gramext.g_assoc option * string option * + Gramext.position option * Gramext.g_assoc option * string option * (* for reinitialization: *) Gramext.g_assoc option val synchronize_level_positions : unit -> unit @@ -234,6 +291,4 @@ val register_empty_levels : bool -> int list -> (Gramext.position option * Gramext.g_assoc option * string option * Gramext.g_assoc option) list -val remove_levels : int -> unit - -val coerce_global_to_id : reference -> identifier +val remove_levels : int -> unit |