do not parse `|` as infix in patterns; parse `|}` as `|` `}`

* use mixfix `(p1 | … | pn)` notation for nested disjunctive patterns,
rather than infix `|`, making pattern syntax consistent with term
syntax.
* disable extending `pattern` grammar with notation incompatible with
the nested disjunctive pattern syntax `(p1 | … | pn)`, such as the `(p
| q)` divisibility notation used by `Numbers`.
* emit a (disabled by default) `disj-pattern-notation` warning when such
`Notation` is attempted.
* update documentation accordingly; document incompatibilities in
`changelog`.
* comment special treatment of `(num)` in grammar.
* update file extensions in `Pcoq` header comment.
* correct the keyword declarations to reflect the contents of the
grammar files; perhaps there should be an option to disable implicit
keyword extension in a `.mlg` file, so that these lists could actually
be checked.
* parse the `|}` manifest record terminator as `|` followed by `}`,
eliminating the `|}` token which conflicts with notations that use `|`
as a terminator (such as, absolute value, norm, or cardinal in
MathComp). Since `|` is now an `operconstr` _and_ `pattern` terminator,
`bar_cbrace` rule checks for contiguous symbols, this change entails no
visible behaviour change.

1 files changed, 11 insertions, 2 deletions

diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index 80dd997860..9653964262 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -15,7 +15,7 @@ open Libnames
 
 open Pcoq.Prim
 
-let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"]
+let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"; "%"; "|"]
 let _ = List.iter CLexer.add_keyword prim_kw
 
 
@@ -31,13 +31,19 @@ let my_int_of_string loc s =
   with Failure _ ->
     CErrors.user_err ~loc (Pp.str "This number is too large.")
 
+let check_nospace loc expected =
+  let (bp, ep) = Loc.unloc loc in
+  if ep = bp + String.length expected then () else
+  Gramlib.Ploc.raise loc (Stream.Error ("'" ^ expected ^ "' expected"))
+
 }
 
 GRAMMAR EXTEND Gram
   GLOBAL:
     bigint natural integer identref name ident var preident
     fullyqualid qualid reference dirpath ne_lstring
-    ne_string string lstring pattern_ident pattern_identref by_notation smart_global;
+    ne_string string lstring pattern_ident pattern_identref by_notation
+    smart_global bar_cbrace;
   preident:
     [ [ s = IDENT -> { s } ] ]
   ;
@@ -123,4 +129,7 @@ GRAMMAR EXTEND Gram
   bigint: (* Negative numbers are dealt with elsewhere *)
     [ [ i = NUMERAL -> { check_int loc i } ] ]
   ;
+  bar_cbrace:
+    [ [ "|"; "}" -> { check_nospace loc "|}" } ] ]
+  ;
 END