diff options
| author | Hugo Herbelin | 2017-11-25 20:50:03 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 10:03:07 +0100 |
| commit | dcfd5c2c2cefcd8ae6a5b2e90fcbd98da4f1b120 (patch) | |
| tree | 48bc1c2a7aef0498290e55917323dcc484e2e878 /intf/extend.ml | |
| parent | 8f93f9a2df6e17386f46f79b2a7eda4104d0a94e (diff) | |
Notations: Adding modifiers to tell which kind of binder a constr can parse.
Concretely, we provide "constr as ident", "constr as strict pattern"
and "constr as pattern".
This tells to parse a binder as a constr, restricting to only ident or
to only a strict pattern, or to a pattern which can also be an ident.
The "strict pattern" modifier allows to restrict the use of patterns
in printing rules. This allows e.g. to select the appropriate rule for
printing between {x|P} and {'pat|P}.
Diffstat (limited to 'intf/extend.ml')
| -rw-r--r-- | intf/extend.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/intf/extend.ml b/intf/extend.ml index 813ed6dc6c..78f0aa1178 100644 --- a/intf/extend.ml +++ b/intf/extend.ml @@ -29,6 +29,11 @@ type production_level = | NextLevel | NumLevel of int +type constr_as_binder_kind = + | AsIdent + | AsIdentOrPattern + | AsStrictPattern + (** User-level types used to tell how to parse or interpret of the non-terminal *) type 'a constr_entry_key_gen = @@ -37,7 +42,8 @@ type 'a constr_entry_key_gen = | ETBigint | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) | ETConstr of 'a - | ETPattern of int option + | ETConstrAsBinder of constr_as_binder_kind * 'a + | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *) | ETOther of string * string (** Entries level (left-hand side of grammar rules) *) |