From a47f0c044b95e2b634e32c7ed7a838045187812e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= Date: Fri, 22 Jul 2022 10:13:23 -0400 Subject: [PATCH] =?UTF-8?q?feat:=20Add=20support=20for=20disjunctive=20(?= =?UTF-8?q?=E2=80=9Cor=E2=80=9D)=20patterns=20(#2448)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit feat: Add support for disjunctive (“or”) patterns * `Source/Dafny/AST/DafnyAst.cs` (`DisjunctivePattern`): New subclass of `ExtendedPattern`. (`IsWildcardPattern`): New property. * `Source/Dafny/AST/Printer.cs` (`PrintExtendedPattern`): Add support for disjunctive patterns. * `Source/Dafny/Cloner.cs` (`CloneExtendedPattern`): Refactor, add support for disjunctive patterns. * `Source/Dafny/Dafny.atg` (`ExtendedPattern`): Rename to `SingleExtendedPattern`. (`ExtendedPattern`): New production for `|`-separated patterns. * `Source/Dafny/Resolver.cs` (`FreshTempVarName`): Refactor, remove obsolete comment. * `Source/Dafny/Resolver.cs` (`RBranch`, `RBranchStmt`): Reject disjunctive patterns. (`RemoveIllegalSubpatterns`): New function to detect, report, and remove nested disjunctive patterns and variables in disjunctive patterns. (`FlattenDisjunctivePatterns`): New function to convert a single `DisjunctivePattern` into one extended pattern per alternative. (`FlattenNestedMatchCaseExpr`): New wrapper around `FlattenDisjunctivePatterns` for `NestedMatchCaseExpr`. (`CompileNestedMatchExpr`): Use it. (`FlattenNestedMatchCaseStmt`): New wrappers around `FlattenDisjunctivePatterns` for `NestedMatchCaseStmt`. (`CompileNestedMatchStmt`): Use it. (`CheckLinearExtendedPattern`): Check the branches of each disjunctive pattern separately. Match bodies are not cloned because they are already resolved; see dafny-lang/dafny#2334 for details. Closes #2220. --- RELEASE_NOTES.md | 5 +- Source/Dafny/AST/DafnyAst.cs | 12 +++ Source/Dafny/AST/Printer.cs | 9 +- Source/Dafny/Cloner.cs | 19 +++-- Source/Dafny/Dafny.atg | 13 ++- Source/Dafny/Resolver.cs | 104 +++++++++++++++++------ Test/patterns/OrPatternErrors.dfy | 20 +++++ Test/patterns/OrPatternErrors.dfy.expect | 6 ++ Test/patterns/OrPatterns.dfy | 85 ++++++++++++++++++ Test/patterns/OrPatterns.dfy.expect | 3 + docs/DafnyRef/Expressions.md | 26 ++++-- 11 files changed, 254 insertions(+), 48 deletions(-) create mode 100644 Test/patterns/OrPatternErrors.dfy create mode 100644 Test/patterns/OrPatternErrors.dfy.expect create mode 100644 Test/patterns/OrPatterns.dfy create mode 100644 Test/patterns/OrPatterns.dfy.expect diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 0aa638f8068..8a639acc089 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -1,6 +1,9 @@ # Upcoming -- feat: New option `-diagnosticsFormat:json` to print Dafny error messages as JSON objects (one per line). (https://github.com/dafny-lang/dafny/pull/2363) +- feat: New option `-diagnosticsFormat:json` to print Dafny error messages as JSON objects (one per line). + (https://github.com/dafny-lang/dafny/pull/2363) +- feat: Dafny now supports disjunctive (“or”) patterns in match statements and expressions. Cases are separated by `|` characters. Disjunctive patterns may not appear within other patterns and may not bind variables. + (https://github.com/dafny-lang/dafny/pull/2448) # 3.7.3 diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 471eef47788..7d2e847ad33 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -12367,6 +12367,15 @@ public ExtendedPattern(IToken tok, bool isGhost = false) { this.IsGhost = isGhost; } } + + public class DisjunctivePattern : ExtendedPattern { + public readonly List Alternatives; + public DisjunctivePattern(IToken tok, List alternatives, bool isGhost = false) : base(tok, isGhost) { + Contract.Requires(alternatives != null && alternatives.Count > 0); + this.Alternatives = alternatives; + } + } + public class LitPattern : ExtendedPattern { public readonly Expression OrigLit; // the expression as parsed; typically a LiteralExpr, but could be a NegationExpression @@ -12430,6 +12439,9 @@ public class IdPattern : ExtendedPattern { public List Arguments; // null if just an identifier; possibly empty argument list if a constructor call public LiteralExpr ResolvedLit; // null if just an identifier + public bool IsWildcardPattern => + Arguments == null && Id.StartsWith("_"); + public void MakeAConstructor() { this.Arguments = new List(); } diff --git a/Source/Dafny/AST/Printer.cs b/Source/Dafny/AST/Printer.cs index 0887cd4f529..bf32361d664 100644 --- a/Source/Dafny/AST/Printer.cs +++ b/Source/Dafny/AST/Printer.cs @@ -2870,13 +2870,20 @@ void PrintExtendedPattern(ExtendedPattern pat) { wr.Write(")"); } break; + case DisjunctivePattern dPat: + var patSep = ""; + foreach (var arg in dPat.Alternatives) { + wr.Write(patSep); + PrintExtendedPattern(arg); + patSep = " | "; + } + break; case LitPattern litPat: wr.Write(litPat.ToString()); break; } } - private void PrintQuantifierDomain(List boundVars, Attributes attrs, Expression range) { Contract.Requires(boundVars != null); string sep = ""; diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index a02cf9b594b..8ed78d36293 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -688,15 +688,16 @@ public MatchCaseStmt CloneMatchCaseStmt(MatchCaseStmt c) { } public ExtendedPattern CloneExtendedPattern(ExtendedPattern pat) { - if (pat is LitPattern) { - var p = (LitPattern)pat; - return new LitPattern(p.Tok, CloneExpr(p.OrigLit)); - } else if (pat is IdPattern) { - var p = (IdPattern)pat; - return new IdPattern(p.Tok, p.Id, p.Arguments == null ? null : p.Arguments.ConvertAll(CloneExtendedPattern)); - } else { - Contract.Assert(false); - return null; + switch (pat) { + case LitPattern p: + return new LitPattern(p.Tok, CloneExpr(p.OrigLit)); + case IdPattern p: + return new IdPattern(p.Tok, p.Id, p.Arguments == null ? null : p.Arguments.ConvertAll(CloneExtendedPattern)); + case DisjunctivePattern p: + return new DisjunctivePattern(p.Tok, p.Alternatives.ConvertAll(CloneExtendedPattern), p.IsGhost); + default: + Contract.Assert(false); + return null; } } public NestedMatchCaseStmt CloneNestedMatchCaseStmt(NestedMatchCaseStmt c) { diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index b6eba5622fd..6d34701f6d1 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -3289,7 +3289,7 @@ BindingGuard /*------------------------------------------------------------------------*/ -ExtendedPattern<.out ExtendedPattern pat.> +SingleExtendedPattern<.out ExtendedPattern pat.> = (. IToken id; List arguments; Expression lit; BoundVar bv; pat = null; @@ -3324,6 +3324,17 @@ ExtendedPattern<.out ExtendedPattern pat.> .) . +/*------------------------------------------------------------------------*/ +ExtendedPattern<.out ExtendedPattern pat.> += (. List branches = null; + ExtendedPattern branch = null; .) + SingleExtendedPattern + { "|" (. branches ??= new() { branch }; .) + SingleExtendedPattern (. branches.Add(branch); .) + } + (. pat = branches == null ? branch : new DisjunctivePattern(branches[0].Tok, branches); .) + . + /*------------------------------------------------------------------------*/ MatchStmt = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 8598e487e99..176c88b87dc 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -44,20 +44,11 @@ private bool VisibleInScope(Declaration d) { return useCompileSignatures || d.IsVisibleInScope(moduleInfo.VisibilityScope); } - FreshIdGenerator defaultTempVarIdGenerator; + FreshIdGenerator defaultTempVarIdGenerator = new FreshIdGenerator(); string FreshTempVarName(string prefix, ICodeContext context) { - var decl = context as Declaration; - if (decl != null) { - return decl.IdGenerator.FreshId(prefix); - } - - // TODO(wuestholz): Is the following code ever needed? - if (defaultTempVarIdGenerator == null) { - defaultTempVarIdGenerator = new FreshIdGenerator(); - } - - return defaultTempVarIdGenerator.FreshId(prefix); + var gen = context is Declaration decl ? decl.IdGenerator : defaultTempVarIdGenerator; + return gen.FreshId(prefix); } interface IAmbiguousThing { @@ -11948,6 +11939,7 @@ private abstract class RBranch { public List Patterns; public RBranch(IToken tok, int branchid, List patterns) { + Contract.Requires(patterns.All(p => !(p is DisjunctivePattern))); this.Tok = tok; this.BranchID = branchid; this.Patterns = patterns; @@ -11965,7 +11957,8 @@ public RBranchStmt(IToken tok, int branchid, List patterns, Lis } public RBranchStmt(int branchid, NestedMatchCaseStmt x, Attributes attrs = null) : base(x.Tok, branchid, new List()) { - this.Body = new List(x.Body); // Resolving the body will insert new elements. + Contract.Requires(!(x.Pat is DisjunctivePattern)); // No nested or patterns + this.Body = new List(x.Body); // Resolving the body will insert new elements. this.Attributes = attrs; this.Patterns.Add(x.Pat); } @@ -12085,7 +12078,7 @@ private void LetBind(RBranch branch, IdPattern var, Expression genExpr) { // If cp is not a wildcard, replace branch.Body with let cp = expr in branch.Body // Otherwise do nothing private void LetBindNonWildCard(RBranch branch, IdPattern var, Expression expr) { - if (!var.Id.StartsWith("_")) { + if (!var.IsWildcardPattern) { LetBind(branch, var, expr); } } @@ -12191,7 +12184,7 @@ private void PrintRBranches(MatchingContext context, List matchees, * PairPB contains, for each branches, its head pattern and the rest of the branch. */ private SyntaxContainer CompileRBranchConstant(MatchTempInfo mti, MatchingContext context, Expression currMatchee, List matchees, List> pairPB) { - // Decreate the count for each branch (increases back for each occurence later on) + // Decrease the count for each branch (increases back for each occurence later on) foreach (var PB in pairPB) { mti.UpdateBranchID(PB.Item2.BranchID, -1); } @@ -12502,6 +12495,49 @@ private SyntaxContainer CompileRBranch(MatchTempInfo mti, MatchingContext contex } } + private ExtendedPattern RemoveIllegalSubpatterns(ExtendedPattern pat, bool inDisjunctivePattern) { + switch (pat) { + case LitPattern: + return pat; + case IdPattern p: + if (inDisjunctivePattern && p.ResolvedLit == null && p.Arguments == null && !p.IsWildcardPattern) { + reporter.Error(MessageSource.Resolver, pat.Tok, "Disjunctive patterns may not bind variables"); + return new IdPattern(p.Tok, FreshTempVarName("_", null), null, p.IsGhost); + } + var args = p.Arguments?.ConvertAll(a => RemoveIllegalSubpatterns(a, inDisjunctivePattern)); + return new IdPattern(p.Tok, p.Id, p.Type, args, p.IsGhost) { ResolvedLit = p.ResolvedLit }; + case DisjunctivePattern p: + reporter.Error(MessageSource.Resolver, pat.Tok, "Disjunctive patterns are not allowed inside other patterns"); + return new IdPattern(p.Tok, FreshTempVarName("_", null), null, p.IsGhost); + default: + Contract.Assert(false); + return null; + } + } + + private IEnumerable FlattenDisjunctivePatterns(ExtendedPattern pat) { + // TODO: Once we rewrite the pattern-matching compiler, we'll handle disjunctive patterns in it, too. + // For now, we handle top-level disjunctive patterns by duplicating the corresponding cases here, and disjunctive + // sub-patterns are unsupported. + return pat is DisjunctivePattern p + ? p.Alternatives.ConvertAll(a => RemoveIllegalSubpatterns(a, inDisjunctivePattern: true)) + : Enumerable.Repeat(RemoveIllegalSubpatterns(pat, inDisjunctivePattern: false), 1); + } + + private IEnumerable FlattenNestedMatchCaseExpr(NestedMatchCaseExpr c) { + var cloner = new Cloner(); + foreach (var pat in FlattenDisjunctivePatterns(c.Pat)) { + yield return new NestedMatchCaseExpr(c.Tok, pat, c.Body, c.Attributes); + } + } + + private IEnumerable FlattenNestedMatchCaseStmt(NestedMatchCaseStmt c) { + var cloner = new Cloner(); + foreach (var pat in FlattenDisjunctivePatterns(c.Pat)) { + yield return new NestedMatchCaseStmt(c.Tok, pat, new List(c.Body), c.Attributes); + } + } + private void CompileNestedMatchExpr(NestedMatchExpr e, ResolveOpts opts) { if (e.ResolvedExpression != null) { //post-resolve, skip @@ -12511,12 +12547,13 @@ private void CompileNestedMatchExpr(NestedMatchExpr e, ResolveOpts opts) { Console.WriteLine("DEBUG: CompileNestedMatchExpr for match at line {0}", e.tok.line); } - MatchTempInfo mti = new MatchTempInfo(e.tok, e.Cases.Count, opts.codeContext, DafnyOptions.O.MatchCompilerDebug); + var cases = e.Cases.SelectMany(FlattenNestedMatchCaseExpr).ToList(); + MatchTempInfo mti = new MatchTempInfo(e.tok, cases.Count, opts.codeContext, DafnyOptions.O.MatchCompilerDebug); // create Rbranches from MatchCaseExpr and set the branch tokens in mti List branches = new List(); - for (int id = 0; id < e.Cases.Count; id++) { - var branch = e.Cases.ElementAt(id); + for (int id = 0; id < cases.Count; id++) { + var branch = cases.ElementAt(id); branches.Add(new RBranchExpr(id, branch, branch.Attributes)); mti.BranchTok[id] = branch.Tok; } @@ -12535,8 +12572,8 @@ private void CompileNestedMatchExpr(NestedMatchExpr e, ResolveOpts opts) { if (mti.BranchIDCount[id] <= 0) { reporter.Warning(MessageSource.Resolver, mti.BranchTok[id], "this branch is redundant "); scope.PushMarker(); - CheckLinearNestedMatchCase(e.Source.Type, e.Cases.ElementAt(id), opts); - ResolveExpression(e.Cases.ElementAt(id).Body, opts); + CheckLinearNestedMatchCase(e.Source.Type, cases.ElementAt(id), opts); + ResolveExpression(cases.ElementAt(id).Body, opts); scope.PopMarker(); } } @@ -12565,13 +12602,14 @@ private void CompileNestedMatchStmt(NestedMatchStmt s, ResolveOpts opts) { Console.WriteLine("DEBUG: CompileNestedMatchStmt for match at line {0}", s.Tok.line); } + var cases = s.Cases.SelectMany(FlattenNestedMatchCaseStmt).ToList(); // initialize the MatchTempInfo to record position and duplication information about each branch - MatchTempInfo mti = new MatchTempInfo(s.Tok, s.EndTok, s.Cases.Count, codeContext, DafnyOptions.O.MatchCompilerDebug, s.Attributes); + MatchTempInfo mti = new MatchTempInfo(s.Tok, s.EndTok, cases.Count, codeContext, DafnyOptions.O.MatchCompilerDebug, s.Attributes); // create Rbranches from NestedMatchCaseStmt and set the branch tokens in mti List branches = new List(); - for (int id = 0; id < s.Cases.Count; id++) { - var branch = s.Cases.ElementAt(id); + for (int id = 0; id < cases.Count; id++) { + var branch = cases.ElementAt(id); branches.Add(new RBranchStmt(id, branch, branch.Attributes)); mti.BranchTok[id] = branch.Tok; } @@ -12589,8 +12627,8 @@ private void CompileNestedMatchStmt(NestedMatchStmt s, ResolveOpts opts) { if (mti.BranchIDCount[id] <= 0) { reporter.Warning(MessageSource.Resolver, mti.BranchTok[id], "this branch is redundant"); scope.PushMarker(); - CheckLinearNestedMatchCase(s.Source.Type, s.Cases.ElementAt(id), opts); - s.Cases.ElementAt(id).Body.ForEach(s => ResolveStatement(s, codeContext)); + CheckLinearNestedMatchCase(s.Source.Type, cases.ElementAt(id), opts); + cases.ElementAt(id).Body.ForEach(s => ResolveStatement(s, codeContext)); scope.PopMarker(); } } @@ -12615,7 +12653,7 @@ private void CheckLinearVarPattern(Type type, IdPattern pat, ResolveOpts opts) { if (scope.FindInCurrentScope(pat.Id) != null) { reporter.Error(MessageSource.Resolver, pat.Tok, "Duplicate parameter name: {0}", pat.Id); - } else if (pat.Id.StartsWith("_")) { + } else if (pat.IsWildcardPattern) { // Wildcard, ignore return; } else { @@ -12653,6 +12691,7 @@ private void CheckLinearVarPattern(Type type, IdPattern pat, ResolveOpts opts) { } // pat could be + // 0 - A DisjunctivePattern // 1 - An IdPattern (without argument) at base type // 2 - A LitPattern at base type // 3* - An IdPattern at tuple type representing a tuple @@ -12663,7 +12702,17 @@ private void CheckLinearExtendedPattern(Type type, ExtendedPattern pat, ResolveO return; } - if (!type.IsDatatype) { // Neither tuple nor datatype + if (pat is DisjunctivePattern dp) { + foreach (var alt in dp.Alternatives) { + // Pushing a scope silences the “duplicate parameter” error in + // `CheckLinearVarPattern`. This is acceptable because disjunctive + // patterns are not allowed to bind variables (the corresponding + // error is raised in `RemoveDisjunctivePatterns`). + scope.PushMarker(); + CheckLinearExtendedPattern(type, alt, opts); + scope.PopMarker(); + } + } else if (!type.IsDatatype) { // Neither tuple nor datatype if (pat is IdPattern id) { if (id.Arguments != null) { // pat is a tuple or constructor @@ -12716,6 +12765,7 @@ private void CheckLinearExtendedPattern(Type type, ExtendedPattern pat, ResolveO return; } else { // matching a datatype value if (!(pat is IdPattern)) { + Contract.Assert(pat is LitPattern); reporter.Error(MessageSource.Resolver, pat.Tok, "Constant pattern used in place of datatype"); } IdPattern idpat = (IdPattern)pat; diff --git a/Test/patterns/OrPatternErrors.dfy b/Test/patterns/OrPatternErrors.dfy new file mode 100644 index 00000000000..3e7ebcbd82f --- /dev/null +++ b/Test/patterns/OrPatternErrors.dfy @@ -0,0 +1,20 @@ +// RUN: %dafny_0 /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module SanityChecks { + datatype T = A(int) | B(nat) | C(bool) + + method Variables(t: T) { + match t + case A(n) // Error: Or-patterns may not bind variables + | B(n) => // Error: Or-patterns may not bind variables + case _ => + } + + method Nesting(t: T) { + match t + case A(1 | 2 | _) => // Error: Or-patterns are not allowed inside other patterns + case B(0 | _) // Error: Or-patterns are not allowed inside other patterns + | C(_ | _ | _) => // Error: Or-patterns are not allowed inside other patterns + } +} diff --git a/Test/patterns/OrPatternErrors.dfy.expect b/Test/patterns/OrPatternErrors.dfy.expect new file mode 100644 index 00000000000..48e97b18829 --- /dev/null +++ b/Test/patterns/OrPatternErrors.dfy.expect @@ -0,0 +1,6 @@ +OrPatternErrors.dfy(9,13): Error: Disjunctive patterns may not bind variables +OrPatternErrors.dfy(10,13): Error: Disjunctive patterns may not bind variables +OrPatternErrors.dfy(16,13): Error: Disjunctive patterns are not allowed inside other patterns +OrPatternErrors.dfy(17,13): Error: Disjunctive patterns are not allowed inside other patterns +OrPatternErrors.dfy(18,13): Error: Disjunctive patterns are not allowed inside other patterns +5 resolution/type errors detected in OrPatternErrors.dfy diff --git a/Test/patterns/OrPatterns.dfy b/Test/patterns/OrPatterns.dfy new file mode 100644 index 00000000000..7062fc19295 --- /dev/null +++ b/Test/patterns/OrPatterns.dfy @@ -0,0 +1,85 @@ +// RUN: %dafny /compile:3 /print:"%t.print" /rprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +datatype Enum = One | Two | Three { + predicate method Even() { + this.Two? + } + + predicate method Even'() { + match this + case One | Three => false + case Two => true + } + + predicate method Even''() { + match this + case Two => true + case One | Three => false + } + + lemma EvenOk() ensures Even() == Even'() == Even''() {} +} + +module Constants { + const ONE := 1 + const TWO := 2 + + method M(i: int) { + match i + case ONE | TWO => return; // `ONE` and `TWO` are not variables here + case _ => // Not redundant + } +} + +module Lists { + datatype List = Nil | Cons(car: T, cdr: List) { + function {:fuel 5} Length(): nat { + match this + case Nil => 0 + case Cons(_, t) => 1 + t.Length() + } + } + + predicate method ContainsOne(l: List) + requires l.Length() == 3 + { + l.car == 1 || l.cdr.car == 1 || l.cdr.cdr.car == 1 + } + + predicate method ContainsOne'(l: List) + requires l.Length() == 3 + { + match l + case Cons(1, Cons(_, Cons(_, Nil))) + | Cons(_, Cons(1, Cons(_, Nil))) + | Cons(_, Cons(_, Cons(1, Nil))) => + true + case Cons(_, Cons(_, Cons(_, Nil))) => + false + } + + lemma ContainsOneOK(l: List) + requires l.Length() == 3 + ensures ContainsOne(l) == ContainsOne'(l) + {} +} + +import opened Lists + +method Main() { + expect One.Even() == One.Even'() == One.Even''() == false; + expect Two.Even() == Two.Even'() == Two.Even''() == true; + expect Three.Even() == Three.Even'() == Three.Even''() == false; + + var a0 := Cons(0, Cons(0, Cons(0, Nil))); + expect ContainsOne(a0) == ContainsOne'(a0) == false; + var a1 := Cons(1, Cons(0, Cons(0, Nil))); + expect ContainsOne(a1) == ContainsOne'(a1) == true; + var a2 := Cons(0, Cons(1, Cons(0, Nil))); + expect ContainsOne(a2) == ContainsOne'(a2) == true; + var a3 := Cons(0, Cons(0, Cons(1, Nil))); + expect ContainsOne(a3) == ContainsOne'(a3) == true; + + print "OK\n"; +} diff --git a/Test/patterns/OrPatterns.dfy.expect b/Test/patterns/OrPatterns.dfy.expect new file mode 100644 index 00000000000..55701992ee3 --- /dev/null +++ b/Test/patterns/OrPatterns.dfy.expect @@ -0,0 +1,3 @@ + +Dafny program verifier finished with 7 verified, 0 errors +OK diff --git a/docs/DafnyRef/Expressions.md b/docs/DafnyRef/Expressions.md index d62d146ec6e..37396f127db 100644 --- a/docs/DafnyRef/Expressions.md +++ b/docs/DafnyRef/Expressions.md @@ -946,17 +946,19 @@ then the `if` and `y` are no longer ghost, and `y` could be used, for example, i ## 21.33. Case and Extended Patterns {#sec-case-pattern} ````grammar CasePattern = - ( Ident "(" [ CasePattern { "," CasePattern } ] ")" - | "(" [ CasePattern { "," CasePattern } ] ")" - | IdentTypeOptional + ( IdentTypeOptional + | [Ident] "(" [ CasePattern { "," CasePattern } ] ")" ) -ExtendedPattern = +SingleExtendedPattern = ( PossiblyNegatedLiteralExpression | IdentTypeOptional - | [ Ident ] "(" [ ExtendedPattern { "," ExtendedPattern } ] ")" + | [ Ident ] "(" [ SingleExtendedPattern { "," SingleExtendedPattern } ] ")" ) +ExtendedPattern = + ( SingleExtendedPattern { "|" SingleExtendedPattern } ) + PossiblyNegatedLiteralExpression = ( "-" ( Nat | Dec ) | LiteralExpression @@ -972,13 +974,14 @@ that is, in `match` and [expressions](#sec-match-expression). `CasePattern`s are used in `LetExpr`s and `VarDeclStatement`s. -The `ExtendedPattern` differs from `CasePattern` in allowing literals -and symbolic constants. +The `ExtendedPattern` differs from `CasePattern` in allowing literals, +symbolic constants, and disjunctive (“or”) patterns. When matching an inductive or coinductive value in a ``MatchStmt`` or ``MatchExpression``, the ``ExtendedPattern`` -must correspond to a +must correspond to one of the following: +* (0) a case disjunction (“or-pattern”) * (1) bound variable (a simple identifier), * (2) a constructor of the type of the value, * (3) a literal of the correct type, or @@ -986,6 +989,8 @@ must correspond to a If the extended pattern is +* a sequence of `|`-separated sub-patterns, then the pattern matches values + matched by any of the sub-patterns. * a parentheses-enclosed possibly-empty list of patterns, then the pattern matches a tuple. * an identifier followed @@ -998,6 +1003,9 @@ matches a constructor. a constant with the given name (if the name is declared but with a non-matching type, a type resolution error will occur), * otherwise, the identifier is a new bound variable +Disjunctive patterns may not bind variables, and may not be nested inside other +patterns. + Any ``ExtendedPattern``s inside the parentheses are then matched against the arguments that were given to the constructor when the value was constructed. @@ -1008,7 +1016,7 @@ When matching a value of base type, the ``ExtendedPattern`` should either be a ``LiteralExpression_`` of the same type as the value, or a single identifier matching all values of this type. -The `ExtendedPattern`s and `CasePattern`s may be nested. The set of bound variable +`ExtendedPattern`s and `CasePattern`s may be nested. The set of bound variable identifiers contained in a `CaseBinding_` or `CasePattern` must be distinct. They are bound to the corresponding values in the value being matched. (Thus, for example, one cannot repeat a bound variable to