diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-25 20:50:03 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:07 +0100 |
| commit | dcfd5c2c2cefcd8ae6a5b2e90fcbd98da4f1b120 (patch) | |
| tree | 48bc1c2a7aef0498290e55917323dcc484e2e878 /intf | |
| 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')
| -rw-r--r-- | intf/extend.ml | 8 | ||||
| -rw-r--r-- | intf/notation_term.ml | 9 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 1 |
3 files changed, 16 insertions, 2 deletions
diff --git a/intf/extend.ml b/intf/extend.ml index 813ed6dc6..78f0aa117 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) *) diff --git a/intf/notation_term.ml b/intf/notation_term.ml index 0f4bfef60..86f5adbd7 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -61,7 +61,14 @@ type subscopes = tmp_scope_name option * scope_name list (** Type of the meta-variables of an notation_constr: in a recursive pattern x..y, x carries the sequence of objects bound to the list x..y *) -type notation_binder_source = NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern +type notation_binder_source = + (* This accepts only pattern *) + (* NtnParsedAsPattern true means only strict pattern (no single variable) at printing *) + | NtnParsedAsPattern of bool + (* This accepts only ident *) + | NtnParsedAsIdent + (* This accepts ident, or pattern, or both *) + | NtnBinderParsedAsConstr of Extend.constr_as_binder_kind type notation_var_instance_type = | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 8e0fe54c5..0b5009e26 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -214,6 +214,7 @@ type proof_expr = type syntax_modifier = | SetItemLevel of string list * Extend.production_level + | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level | SetLevel of int | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key |