summaryrefslogtreecommitdiff
path: root/parsing/extend.ml
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/extend.ml
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'parsing/extend.ml')
-rw-r--r--parsing/extend.ml62
1 files changed, 34 insertions, 28 deletions
diff --git a/parsing/extend.ml b/parsing/extend.ml
index f4c98291..7643120f 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -6,52 +6,58 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-
-(*i $Id: extend.ml 7761 2005-12-30 10:52:19Z herbelin $ i*)
+(*i $Id$ i*)
open Util
-open Pp
-open Gramext
-open Names
-open Ppextend
-open Topconstr
-open Genarg
(**********************************************************************)
-(* constr entry keys *)
+(* 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 'a prod_entry_key =
+ | Alist1 of 'a prod_entry_key
+ | Alist1sep of 'a prod_entry_key * string
+ | Alist0 of 'a prod_entry_key
+ | Alist0sep of 'a prod_entry_key * string
+ | Aopt of 'a prod_entry_key
+ | Amodifiers of 'a prod_entry_key
+ | Aself
+ | Anext
+ | Atactic of int
+ | Agram of 'a Gramext.g_entry
+ | Aentry of string * string
+
+(**********************************************************************)
+(* Entry keys for constr notations *)
type side = Left | Right
type production_position =
- | BorderProd of side * Gramext.g_assoc option (* true=left; false=right *)
+ | BorderProd of side * Gramext.g_assoc option
| InternalProd
type production_level =
| NextLevel
| NumLevel of int
-type ('lev,'pos) constr_entry_key =
- | ETIdent | ETReference | ETBigint
+type ('lev,'pos) constr_entry_key_gen =
+ | ETName | ETReference | ETBigint
| ETConstr of ('lev * 'pos)
| ETPattern
| ETOther of string * string
| ETConstrList of ('lev * 'pos) * Token.pattern list
-type constr_production_entry =
- (production_level,production_position) constr_entry_key
-type constr_entry =
- (int,unit) constr_entry_key
-type simple_constr_production_entry =
- (production_level,unit) constr_entry_key
-
-(**********************************************************************)
-(* syntax modifiers *)
+(* Entries level (left-hand-side of grammar rules) *)
+type constr_entry_key =
+ (int,unit) constr_entry_key_gen
-type syntax_modifier =
- | SetItemLevel of string list * production_level
- | SetLevel of int
- | SetAssoc of Gramext.g_assoc
- | SetEntryType of string * simple_constr_production_entry
- | SetOnlyParsing
- | SetFormat of string located
+(* Entries used in productions (in right-hand-side of grammar rules) *)
+type constr_prod_entry_key =
+ (production_level,production_position) constr_entry_key_gen
+(* Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *)
+type simple_constr_prod_entry_key =
+ (production_level,unit) constr_entry_key_gen