aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/02-specification-language/10167-orpat-mixfix.rst12
-rw-r--r--doc/sphinx/addendum/extended-pattern-matching.rst7
-rw-r--r--doc/sphinx/language/gallina-specification-language.rst3
-rw-r--r--doc/sphinx/user-extensions/syntax-extensions.rst11
-rw-r--r--interp/constrintern.ml16
-rw-r--r--parsing/g_constr.mlg45
-rw-r--r--parsing/g_prim.mlg13
-rw-r--r--parsing/pcoq.ml2
-rw-r--r--parsing/pcoq.mli5
-rw-r--r--printing/ppconstr.ml5
-rw-r--r--test-suite/success/Case18.v5
-rw-r--r--vernac/egramcoq.ml18
-rw-r--r--vernac/g_vernac.mlg2
13 files changed, 99 insertions, 45 deletions
diff --git a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst
new file mode 100644
index 0000000000..e3c3923348
--- /dev/null
+++ b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst
@@ -0,0 +1,12 @@
+- Require parentheses around nested disjunctive patterns, so that pattern and
+ term syntax are consistent; match branch patterns no longer require
+ parentheses for notation at level 100 or more. Incompatibilities:
+
+ + in :g:`match p with (_, (0|1)) => ...` parentheses may no longer be
+ omitted around :n:`0|1`.
+ + notation :g:`(p | q)` now potentially clashes with core pattern syntax,
+ and should be avoided. ``-w disj-pattern-notation`` flags such :cmd:`Notation`.
+
+ see :ref:`extendedpatternmatching` for details
+ (`#10167 <https://github.com/coq/coq/pull/10167>`_,
+ by Georges Gonthier).
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index e882ce6e88..b568160356 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -21,10 +21,10 @@ type is considered to be a variable. A variable name cannot occur more
than once in a given pattern. It is recommended to start variable
names by a lowercase letter.
-If a pattern has the form ``(c x)`` where ``c`` is a constructor symbol and x
+If a pattern has the form ``c x`` where ``c`` is a constructor symbol and x
is a linear vector of (distinct) variables, it is called *simple*: it
is the kind of pattern recognized by the basic version of match. On
-the opposite, if it is a variable ``x`` or has the form ``(c p)`` with ``p`` not
+the opposite, if it is a variable ``x`` or has the form ``c p`` with ``p`` not
only made of variables, the pattern is called *nested*.
A variable pattern matches any value, and the identifier is bound to
@@ -216,7 +216,8 @@ Here is an example:
end.
-Here is another example using disjunctive subpatterns.
+Nested disjunctive patterns are allowed, inside parentheses, with the
+notation :n:`({+| @pattern})`, as in:
.. coqtop:: in
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 8acbcbec8f..ebaa6fde66 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -185,8 +185,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`.
: `qualid`
: _
: `num`
- : ( `or_pattern` , … , `or_pattern` )
- or_pattern : `pattern` | … | `pattern`
+ : ( `pattern` | … | `pattern` )
Types
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 3710c0af9d..aee5f66bb6 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -924,6 +924,17 @@ notations are given below. The optional :production:`scope` is described in
given to some notation, say ``"{ y } & { z }"`` in fact applies to the
underlying ``"{ x }"``\-free rule which is ``"y & z"``).
+.. note:: Notations such as ``"( p | q )"`` (or starting with ``"( x | "``,
+ more generally) are deprecated as they conflict with the syntax for
+ nested disjunctive patterns (see :ref:`extendedpatternmatching`),
+ and are not honored in pattern expressions.
+
+ .. warn:: Use of @string Notation is deprecated as it is inconsistent with pattern syntax.
+
+ This warning is disabled by default to avoid spurious diagnostics
+ due to legacy notation in the Coq standard library.
+ It can be turned on with the ``-w disj-pattern-notation`` flag.
+
Persistence of notations
++++++++++++++++++++++++
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 31f3736bae..1dd68f2abf 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1642,15 +1642,13 @@ let drop_notations_pattern looked_for genv =
| CPatCast (_,_) ->
(* We raise an error if the pattern contains a cast, due to
current restrictions on casts in patterns. Cast in patterns
- are supported only in local binders and only at top
- level. In fact, they are currently eliminated by the
- parser. The only reason why they are in the
- [cases_pattern_expr] type is that the parser needs to factor
- the "(c : t)" notation with user defined notations (such as
- the pair). In the long term, we will try to support such
- casts everywhere, and use them to print the domains of
- lambdas in the encoding of match in constr. This check is
- here and not in the parser because it would require
+ are supported only in local binders and only at top level.
+ The only reason they are in the [cases_pattern_expr] type
+ is that the parser needs to factor the "c : t" notation
+ with user defined notations. In the long term, we will try to
+ support such casts everywhere, and perhaps use them to print
+ the domains of lambdas in the encoding of match in constr.
+ This check is here and not in the parser because it would require
duplicating the levels of the [pattern] rule. *)
CErrors.user_err ?loc ~hdr:"drop_notations_pattern"
(Pp.strbrk "Casts are not supported in this pattern.")
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 6df97609f5..bd88570224 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -31,8 +31,10 @@ let ldots_var = Id.of_string ".."
let constr_kw =
[ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for";
"end"; "as"; "let"; "if"; "then"; "else"; "return";
- "SProp"; "Prop"; "Set"; "Type"; ".("; "_"; "..";
- "`{"; "`("; "{|"; "|}" ]
+ "SProp"; "Prop"; "Set"; "Type";
+ ":="; "=>"; "->"; ".."; "<:"; "<<:"; ":>";
+ ".("; "()"; "`{"; "`("; "@{"; "{|";
+ "_"; "@"; "+"; "!"; "?"; ";"; ","; ":" ]
let _ = List.iter CLexer.add_keyword constr_kw
@@ -225,11 +227,13 @@ GRAMMAR EXTEND Gram
[ c=atomic_constr -> { c }
| c=match_constr -> { c }
| "("; c = operconstr LEVEL "200"; ")" ->
- { (match c.CAst.v with
+ { (* Preserve parentheses around numerals so that constrintern does not
+ collapse -(3) into the numeral -3. *)
+ (match c.CAst.v with
| CPrim (Numeral (SPlus,n)) ->
CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"( _ )"),([c],[],[],[]))
| _ -> c) }
- | "{|"; c = record_declaration; "|}" -> { c }
+ | "{|"; c = record_declaration; bar_cbrace -> { c }
| "{"; c = binder_constr ; "}" ->
{ CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) }
| "`{"; c = operconstr LEVEL "200"; "}" ->
@@ -277,16 +281,16 @@ GRAMMAR EXTEND Gram
":="; c1 = operconstr LEVEL "200"; "in";
c2 = operconstr LEVEL "200" ->
{ CAst.make ~loc @@ CLetTuple (lb,po,c1,c2) }
- | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
+ | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200";
"in"; c2 = operconstr LEVEL "200" ->
{ CAst.make ~loc @@
CCases (LetPatternStyle, None, [c1, None, None], [CAst.make ~loc ([[p]], c2)]) }
- | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
+ | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200";
rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
{ CAst.make ~loc @@
CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [CAst.make ~loc ([[p]], c2)]) }
- | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200";
+ | "let"; "'"; p = pattern LEVEL "200"; "in"; t = pattern LEVEL "200";
":="; c1 = operconstr LEVEL "200"; rt = case_type;
"in"; c2 = operconstr LEVEL "200" ->
{ CAst.make ~loc @@
@@ -359,7 +363,7 @@ GRAMMAR EXTEND Gram
case_item:
[ [ c=operconstr LEVEL "100";
ona = OPT ["as"; id=name -> { id } ];
- ty = OPT ["in"; t=pattern -> { t } ] ->
+ ty = OPT ["in"; t = pattern LEVEL "200" -> { t } ] ->
{ (c,ona,ty) } ] ]
;
case_type:
@@ -377,14 +381,14 @@ GRAMMAR EXTEND Gram
[ [ OPT"|"; br=LIST0 eqn SEP "|" -> { br } ] ]
;
mult_pattern:
- [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> { pl } ] ]
+ [ [ pl = LIST1 pattern LEVEL "200" SEP "," -> { pl } ] ]
;
eqn:
[ [ pll = LIST1 mult_pattern SEP "|";
"=>"; rhs = lconstr -> { (CAst.make ~loc (pll,rhs)) } ] ]
;
record_pattern:
- [ [ id = global; ":="; pat = pattern -> { (id, pat) } ] ]
+ [ [ id = global; ":="; pat = pattern LEVEL "200" -> { (id, pat) } ] ]
;
record_patterns:
[ [ p = record_pattern; ";"; ps = record_patterns -> { p :: ps }
@@ -396,7 +400,10 @@ GRAMMAR EXTEND Gram
pattern:
[ "200" RIGHTA [ ]
| "100" RIGHTA
- [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> { CAst.make ~loc @@ CPatOr (p::pl) } ]
+ [ p = pattern; ":"; ty = binder_constr ->
+ {CAst.make ~loc @@ CPatCast (p, ty) }
+ | p = pattern; ":"; ty = operconstr LEVEL "100" ->
+ {CAst.make ~loc @@ CPatCast (p, ty) } ]
| "99" RIGHTA [ ]
| "90" RIGHTA [ ]
| "10" LEFTA
@@ -409,21 +416,17 @@ GRAMMAR EXTEND Gram
[ c = pattern; "%"; key=IDENT -> { CAst.make ~loc @@ CPatDelimiters (key,c) } ]
| "0"
[ r = Prim.reference -> { CAst.make ~loc @@ CPatAtom (Some r) }
- | "{|"; pat = record_patterns; "|}" -> { CAst.make ~loc @@ CPatRecord pat }
+ | "{|"; pat = record_patterns; bar_cbrace -> { CAst.make ~loc @@ CPatRecord pat }
| "_" -> { CAst.make ~loc @@ CPatAtom None }
| "("; p = pattern LEVEL "200"; ")" ->
- { (match p.CAst.v with
+ { (* Preserve parentheses around numerals so that constrintern does not
+ collapse -(3) into the numeral -3. *)
+ (match p.CAst.v with
| CPatPrim (Numeral (SPlus,n)) ->
CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
| _ -> p) }
- | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" ->
- { let p =
- match p with
- | { CAst.v = CPatPrim (Numeral (SPlus,n)) } ->
- CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
- | _ -> p
- in
- CAst.make ~loc @@ CPatCast (p, ty) }
+ | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" ->
+ { CAst.make ~loc @@ CPatOr (p::pl) }
| n = NUMERAL-> { CAst.make ~loc @@ CPatPrim (Numeral (SPlus,n)) }
| s = string -> { CAst.make ~loc @@ CPatPrim (String s) } ] ]
;
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
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index a78ad4f842..b474c8e9a9 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -411,6 +411,8 @@ module Prim =
let ne_string = Entry.create "Prim.ne_string"
let ne_lstring = Entry.create "Prim.ne_lstring"
+ let bar_cbrace = Entry.create "'|}'"
+
end
module Constr =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 3a57c14a3b..5f982346ab 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -38,9 +38,9 @@ end
- dynamic rules declared at the evaluation of Coq files (using
e.g. Notation, Infix, or Tactic Notation)
- - static rules explicitly defined in files g_*.ml4
+ - static rules explicitly defined in files g_*.mlg
- static rules macro-generated by ARGUMENT EXTEND, TACTIC EXTEND and
- VERNAC EXTEND (see e.g. file extratactics.ml4)
+ VERNAC EXTEND (see e.g. file extratactics.mlg)
Note that parsing a Coq document is in essence stateful: the parser
needs to recognize commands that start proofs and use a different
@@ -170,6 +170,7 @@ module Prim :
val ne_string : string Entry.t
val ne_lstring : lstring Entry.t
val var : lident Entry.t
+ val bar_cbrace : unit Entry.t
end
module Constr :
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 9d3ed40f6c..e2a63a4540 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -249,7 +249,7 @@ let tag_var = tag Tag.variable
str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}"))
let las = lapp
- let lpator = 100
+ let lpator = 0
let lpatrec = 0
let rec pr_patt sep inh p =
@@ -283,7 +283,8 @@ let tag_var = tag Tag.variable
pr_reference r, latom
| CPatOr pl ->
- hov 0 (prlist_with_sep pr_spcbar (pr_patt mt (lpator,L)) pl), lpator
+ let pp = pr_patt mt (lpator,Any) in
+ surround (hov 0 (prlist_with_sep pr_spcbar pp pl)), lpator
| CPatNotation ((_,"( _ )"),([p],[]),[]) ->
pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
diff --git a/test-suite/success/Case18.v b/test-suite/success/Case18.v
index be9ca8d41b..6bea435090 100644
--- a/test-suite/success/Case18.v
+++ b/test-suite/success/Case18.v
@@ -1,7 +1,10 @@
(* Check or-patterns *)
+(* Non-interference with Numbers divisibility. *)
+Reserved Notation "( p | q )" (at level 0).
+
Definition g x :=
- match x with ((((1 as x),_) | (_,x)), (_,(2 as y))|(y,_)) => (x,y) end.
+ match x with ((((1 as x),_) | (_,x)), ((_,(2 as y)) | (y,_))) => (x,y) end.
Check (refl_equal _ : g ((1,2),(3,4)) = (1,3)).
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 568e5b9997..9bc225475d 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -546,6 +546,15 @@ let extend_constr state forpat ng =
let constr_levels = GramState.field ()
+let is_disjunctive_pattern_rule ng =
+ String.is_sub "( _ | " (snd ng.notgram_notation) 0
+
+let warn_disj_pattern_notation =
+ let open Pp in
+ let pp ng = str "Use of " ++ Notation.pr_notation ng.notgram_notation ++
+ str " Notation is deprecated as it is inconsistent with pattern syntax." in
+ CWarnings.create ~name:"disj-pattern-notation" ~category:"notation" ~default:CWarnings.Disabled pp
+
let extend_constr_notation ng state =
let levels = match GramState.get state constr_levels with
| None -> String.Map.add "constr" default_constr_levels String.Map.empty
@@ -553,8 +562,13 @@ let extend_constr_notation ng state =
in
(* Add the notation in constr *)
let (r, levels) = extend_constr levels ForConstr ng in
- (* Add the notation in cases_pattern *)
- let (r', levels) = extend_constr levels ForPattern ng in
+ (* Add the notation in cases_pattern, unless it would disrupt *)
+ (* parsing nested disjunctive patterns. *)
+ let (r', levels) =
+ if is_disjunctive_pattern_rule ng then begin
+ warn_disj_pattern_notation ng;
+ ([], levels)
+ end else extend_constr levels ForPattern ng in
let state = GramState.set state constr_levels levels in
(r @ r', state)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index b2db64f74c..7c8c2b10ab 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -303,7 +303,7 @@ GRAMMAR EXTEND Gram
[ [ "@{" ; l = LIST0 identref; ext = [ "+" -> { true } | -> { false } ];
cs = [ "|"; l' = LIST0 univ_constraint SEP ",";
ext = [ "+" -> { true } | -> { false } ]; "}" -> { (l',ext) }
- | ext = [ "}" -> { true } | "|}" -> { false } ] -> { ([], ext) } ]
+ | ext = [ "}" -> { true } | bar_cbrace -> { false } ] -> { ([], ext) } ]
->
{ let open UState in
{ univdecl_instance = l;
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:55:06 +0000