diff options
| author | Hugo Herbelin | 2017-08-12 09:15:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 10:03:06 +0100 |
| commit | edd0d22429354a5f2c703a8c7bd1f775e2f97d9e (patch) | |
| tree | 865fd16d40f5641cac233f951f951a9a4502159f /intf/notation_term.ml | |
| parent | 398358618bb3eabfe822b79c669703c1c33b67e6 (diff) | |
Adding support for parsing subterms of a notation as "pattern".
This allows in particular to define notations with 'pat style binders.
E.g.:
A non-trivial change in this commit is storing binders and patterns
separately from terms.
This is not strictly necessary but has some advantages.
However, it is relatively common to have binders also used as terms,
or binders parsed as terms. Thus, it is already relatively common to
embed binders into terms (see e.g. notation for ETA in output test
Notations3.v) or to coerce terms to idents (see e.g. the notation for
{x|P} where x is parsed as a constr).
So, it is as simple to always store idents (and eventually patterns)
as terms.
Diffstat (limited to 'intf/notation_term.ml')
| -rw-r--r-- | intf/notation_term.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/intf/notation_term.ml b/intf/notation_term.ml index 52fd0f368f..83cc454f43 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -61,13 +61,13 @@ 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_var_instance_type = - | NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList + | NtnTypeConstr | NtnTypeBinder of bool | NtnTypeConstrList | NtnTypeBinderList (** Type of variables when interpreting a constr_expr as a notation_constr: in a recursive pattern x..y, both x and y carry the individual type of each element of the list x..y *) type notation_var_internalization_type = - | NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent + | NtnInternTypeAny | NtnInternTypeOnlyBinder (** This characterizes to what a notation is interpreted to *) type interpretation = @@ -95,7 +95,7 @@ type precedence = int type parenRelation = L | E | Any | Prec of precedence type tolerability = precedence * parenRelation -type level = precedence * tolerability list * notation_var_internalization_type list +type level = precedence * tolerability list * Extend.constr_entry_key list (** Grammar rules for a notation *) |