diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-11 19:24:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:04 +0100 |
| commit | 351e9acd3aa11a751129f5956fe991fc4d0bf0b8 (patch) | |
| tree | 55ce7af3e89df21649517cec521dc32225db18a5 /intf | |
| parent | ead835b3e8c366800b8c95a28a89062abb62d807 (diff) | |
Introducing an intermediary type "constr_prod_entry_key" for grammar productions.
This type describes the grammar non-terminal. It typically contains
ETConstrList (now renamed ETProdConstrList) but not ETBinder. It is
the type for metasyntax.ml and egramcoq.ml to communicate together.
The type constr_prod_entry_key with ETConstr, ETBinder, is now used
only in metasyntax.ml. This allows to get rid of some "assert false"
in uselessly matching over ETConstrList in metasyntax.ml and of some
"assert false" in uselessly matching over ETBinder in egramcoq.ml.
Also exporting less of extend.mli in API.
Diffstat (limited to 'intf')
| -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 = |