From dcfd5c2c2cefcd8ae6a5b2e90fcbd98da4f1b120 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 25 Nov 2017 20:50:03 +0100
Subject: 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}.
---
 intf/notation_term.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'intf/notation_term.ml')

diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index 0f4bfef600..86f5adbd78 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
-- 
cgit v1.2.3