diff options
Diffstat (limited to 'intf/extend.ml')
| -rw-r--r-- | intf/extend.ml | 29 |
1 files changed, 19 insertions, 10 deletions
diff --git a/intf/extend.ml b/intf/extend.ml index e4d014a09..79bbbd376 100644 --- a/intf/extend.ml +++ b/intf/extend.ml @@ -29,32 +29,41 @@ type production_level = | NextLevel | NumLevel of int -type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.t list +(** User-level types used to tell how to parse or interpret of the non-terminal *) type ('lev,'pos) constr_entry_key_gen = - | ETName | ETReference | ETBigint - | ETBinder of bool + | ETName + | ETReference + | ETBigint + | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) | ETConstr of ('lev * 'pos) | ETPattern | ETOther of string * string - | ETConstrList of ('lev * 'pos) * Tok.t list - | ETBinderList of binder_entry_kind (** Entries level (left-hand-side of grammar rules) *) type constr_entry_key = (int,unit) constr_entry_key_gen -(** 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 +(** Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals *) + +type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.t list + +type constr_prod_entry_key = + | ETProdName (* Parsed as a name (ident or _) *) + | ETProdReference (* Parsed as a global reference *) + | ETProdBigint (* Parsed as an (unbounded) integer *) + | ETProdConstr of (production_level * production_position) (* Parsed as constr or pattern *) + | ETProdPattern (* Parsed as pattern (as subpart of a constr) *) + | ETProdOther of string * string (* Intended for embedding custom entries in constr or pattern *) + | ETProdConstrList of (production_level * production_position) * Tok.t list (* Parsed as non-empty list of constr *) + | ETProdBinderList of binder_entry_kind (* Parsed as non-empty list of local binders *) + (** {5 AST for user-provided entries} *) type 'a user_symbol = |