summaryrefslogtreecommitdiff
path: root/parsing/egrammar.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /parsing/egrammar.mli
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'parsing/egrammar.mli')
-rw-r--r--parsing/egrammar.mli57
1 files changed, 29 insertions, 28 deletions
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index d2d912d1..1228b40c 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -6,62 +6,63 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: egrammar.mli 10122 2007-09-15 10:35:59Z letouzey $ i*)
+(*i $Id$ i*)
(*i*)
open Util
+open Names
open Topconstr
open Pcoq
open Extend
open Vernacexpr
open Ppextend
open Rawterm
+open Genarg
open Mod_subst
(*i*)
(** Mapping of grammar productions to camlp4 actions
- Used for Coq-level Notation and Tactic Notation,
+ Used for Coq-level Notation and Tactic Notation,
and for ML-level tactic and vernac extensions
*)
-type prod_item =
- | Term of Token.pattern
- | NonTerm of constr_production_entry *
- (Names.identifier * constr_production_entry) option
+(* For constr notations *)
-type notation_grammar =
- int * Gramext.g_assoc option * notation * prod_item list
+type grammar_constr_prod_item =
+ | GramConstrTerminal of Token.pattern
+ | GramConstrNonTerminal of constr_prod_entry_key * identifier option
+ | GramConstrListMark of int * bool
+ (* tells action rule to make a list of the n previous parsed items;
+ concat with last parsed list if true *)
+
+type notation_grammar =
+ int * Gramext.g_assoc option * notation * grammar_constr_prod_item list list
+
+(* For tactic and vernac notations *)
+
+type grammar_prod_item =
+ | GramTerminal of string
+ | GramNonTerminal of loc * argument_type *
+ Gram.te prod_entry_key * identifier option
+
+(* Adding notations *)
type all_grammar_command =
| Notation of (precedence * tolerability list) * notation_grammar
| TacticGrammar of
- (string * int * grammar_production list *
- (Names.dir_path * Tacexpr.glob_tactic_expr))
+ (string * int * grammar_prod_item list *
+ (dir_path * Tacexpr.glob_tactic_expr))
val extend_grammar : all_grammar_command -> unit
-(* Add grammar rules for tactics *)
-
-type grammar_tactic_production =
- | TacTerm of string
- | TacNonTerm of
- loc * (Compat.token Gramext.g_symbol * Genarg.argument_type) * string option
-
val extend_tactic_grammar :
- string -> grammar_tactic_production list list -> unit
+ string -> grammar_prod_item list list -> unit
val extend_vernac_command_grammar :
- string -> grammar_tactic_production list list -> unit
-(*
-val get_extend_tactic_grammars :
- unit -> (string * grammar_tactic_production list list) list
-*)
+ string -> grammar_prod_item list list -> unit
+
val get_extend_vernac_grammars :
- unit -> (string * grammar_tactic_production list list) list
-(*
-val reset_extend_grammars_v8 : unit -> unit
-*)
-val interp_entry_name : int -> string -> entry_type * Compat.token Gramext.g_symbol
+ unit -> (string * grammar_prod_item list list) list
val recover_notation_grammar :
notation -> (precedence * tolerability list) -> notation_grammar