From de0ab0910df2e0166097368bd620c417a1d4d60d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= Date: Fri, 15 Jul 2022 23:00:27 -0700 Subject: [PATCH 01/12] =?UTF-8?q?feat:=20Add=20support=20for=20disjunctive?= =?UTF-8?q?=20(=E2=80=9Cor=E2=80=9D)=20patterns?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * `Source/Dafny/AST/DafnyAst.cs` (`DisjunctivePattern`): New subclass of `ExtendedPattern`. * `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. (`RemoveDisjunctivePatterns`): 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. Closes #2220. --- RELEASE_NOTES.md | 2 + Source/Dafny/AST/DafnyAst.cs | 9 +++ Source/Dafny/AST/Printer.cs | 8 +++ Source/Dafny/Cloner.cs | 19 ++--- Source/Dafny/Dafny.atg | 13 +++- Source/Dafny/Resolver.cs | 97 +++++++++++++++++++------- Test/dafny0/OrPatternErrors.dfy | 20 ++++++ Test/dafny0/OrPatternErrors.dfy.expect | 0 Test/dafny0/OrPatterns.dfy | 74 ++++++++++++++++++++ Test/dafny0/OrPatterns.dfy.expect | 5 ++ docs/DafnyRef/Expressions.md | 26 ++++--- 11 files changed, 230 insertions(+), 43 deletions(-) create mode 100644 Test/dafny0/OrPatternErrors.dfy create mode 100644 Test/dafny0/OrPatternErrors.dfy.expect create mode 100644 Test/dafny0/OrPatterns.dfy create mode 100644 Test/dafny0/OrPatterns.dfy.expect diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index dd9a9f16256..64b4fe5148a 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -1,6 +1,8 @@ # Upcoming - feat: *Less code navigation when verifying code*: In the IDE, failing postconditions and preconditions error messages now immediately display the sub-conditions that Dafny could not prove. Both on hover and in the Problems window. (https://github.com/dafny-lang/dafny/pull/2434) +- 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.2 diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index ab14f864861..58927e20246 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -12283,6 +12283,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 diff --git a/Source/Dafny/AST/Printer.cs b/Source/Dafny/AST/Printer.cs index f0beb3e4fd6..9739f382af7 100644 --- a/Source/Dafny/AST/Printer.cs +++ b/Source/Dafny/AST/Printer.cs @@ -2870,6 +2870,14 @@ void PrintExtendedPattern(ExtendedPattern pat) { wr.Write(")"); } break; + case DisjunctivePattern dp: + var psep = ""; + foreach (var arg in dp.Alternatives) { + wr.Write(psep); + PrintExtendedPattern(arg); + psep = " | "; + } + break; case LitPattern litPat: wr.Write(litPat.ToString()); break; 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 e2519d73720..51389c4ec5a 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -3250,7 +3250,7 @@ BindingGuard /*------------------------------------------------------------------------*/ -ExtendedPattern<.out ExtendedPattern pat.> +SingleExtendedPattern<.out ExtendedPattern pat.> = (. IToken id; List arguments; Expression lit; BoundVar bv; pat = null; @@ -3285,6 +3285,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 4da9942106d..778b5e060ae 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 { @@ -11947,6 +11938,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; @@ -11964,6 +11956,7 @@ public RBranchStmt(IToken tok, int branchid, List patterns, Lis } public RBranchStmt(int branchid, NestedMatchCaseStmt x, Attributes attrs = null) : base(x.Tok, branchid, new List()) { + 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); @@ -12190,7 +12183,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); } @@ -12501,6 +12494,48 @@ private SyntaxContainer CompileRBranch(MatchTempInfo mti, MatchingContext contex } } + private ExtendedPattern RemoveDisjunctivePatterns(ExtendedPattern pat, bool allowVariables) { + switch (pat) { + case LitPattern: + return pat; + case IdPattern p: + if (p.Arguments == null && !p.Id.StartsWith("_") && !allowVariables) { + reporter.Error(MessageSource.Resolver, pat.Tok, "Or-patterns may not bind variables"); + return new IdPattern(p.Tok, FreshTempVarName("_", null), null); + } + return new IdPattern(p.Tok, p.Id, p.Arguments?.ConvertAll(a => RemoveDisjunctivePatterns(a, allowVariables))); + case DisjunctivePattern p: + reporter.Error(MessageSource.Resolver, pat.Tok, "Or-patterns are not allowed inside other patterns"); + return new IdPattern(p.Tok, FreshTempVarName("_", null), null); + 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 => RemoveDisjunctivePatterns(a, allowVariables: false)) + : Enumerable.Repeat(RemoveDisjunctivePatterns(pat, allowVariables: true), 1); + } + + private IEnumerable FlattenNestedMatchCaseExpr(NestedMatchCaseExpr c) { + var cloner = new Cloner(); + foreach (var pat in FlattenDisjunctivePatterns(c.Pat)) { + yield return new NestedMatchCaseExpr(c.Tok, pat, cloner.CloneExpr(c.Body), cloner.CloneAttributes(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, c.Body.ConvertAll(cloner.CloneStmt), cloner.CloneAttributes(c.Attributes)); + } + } + private void CompileNestedMatchExpr(NestedMatchExpr e, ResolveOpts opts) { if (e.ResolvedExpression != null) { //post-resolve, skip @@ -12510,12 +12545,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; } @@ -12534,8 +12570,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(); } } @@ -12564,13 +12600,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; } @@ -12588,8 +12625,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(); } } @@ -12652,6 +12689,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 @@ -12662,7 +12700,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 @@ -12715,6 +12763,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/dafny0/OrPatternErrors.dfy b/Test/dafny0/OrPatternErrors.dfy new file mode 100644 index 00000000000..3e7ebcbd82f --- /dev/null +++ b/Test/dafny0/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/dafny0/OrPatternErrors.dfy.expect b/Test/dafny0/OrPatternErrors.dfy.expect new file mode 100644 index 00000000000..e69de29bb2d diff --git a/Test/dafny0/OrPatterns.dfy b/Test/dafny0/OrPatterns.dfy new file mode 100644 index 00000000000..acbda2df77e --- /dev/null +++ b/Test/dafny0/OrPatterns.dfy @@ -0,0 +1,74 @@ +// 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 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/dafny0/OrPatterns.dfy.expect b/Test/dafny0/OrPatterns.dfy.expect new file mode 100644 index 00000000000..d8ec0e6ecfc --- /dev/null +++ b/Test/dafny0/OrPatterns.dfy.expect @@ -0,0 +1,5 @@ + +Dafny program verifier finished with 7 verified, 0 errors +Running... + +OK diff --git a/docs/DafnyRef/Expressions.md b/docs/DafnyRef/Expressions.md index 3a1a88ca747..627947179be 100644 --- a/docs/DafnyRef/Expressions.md +++ b/docs/DafnyRef/Expressions.md @@ -918,17 +918,19 @@ TO BE WRITTEN - binding form ## 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 @@ -944,13 +946,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 @@ -958,6 +961,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 @@ -970,6 +975,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. @@ -980,7 +988,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 From 2ef4189543b4b2a4c0529fa0884e2856c110bcac Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= Date: Wed, 20 Jul 2022 17:34:06 -0700 Subject: [PATCH 02/12] Rename dp and psep --- Source/Dafny/AST/Printer.cs | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/Source/Dafny/AST/Printer.cs b/Source/Dafny/AST/Printer.cs index a6280f13022..bf32361d664 100644 --- a/Source/Dafny/AST/Printer.cs +++ b/Source/Dafny/AST/Printer.cs @@ -2870,12 +2870,12 @@ void PrintExtendedPattern(ExtendedPattern pat) { wr.Write(")"); } break; - case DisjunctivePattern dp: - var psep = ""; - foreach (var arg in dp.Alternatives) { - wr.Write(psep); + case DisjunctivePattern dPat: + var patSep = ""; + foreach (var arg in dPat.Alternatives) { + wr.Write(patSep); PrintExtendedPattern(arg); - psep = " | "; + patSep = " | "; } break; case LitPattern litPat: @@ -2884,7 +2884,6 @@ void PrintExtendedPattern(ExtendedPattern pat) { } } - private void PrintQuantifierDomain(List boundVars, Attributes attrs, Expression range) { Contract.Requires(boundVars != null); string sep = ""; From 53808c6e732dbf2ebfee49a8fff1ce3417b3a6ae Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= Date: Wed, 20 Jul 2022 17:34:48 -0700 Subject: [PATCH 03/12] Rename RemoveDisjunctivePatterns and clean up its implementation --- Source/Dafny/Resolver.cs | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index be45dd7b56d..5ea67020395 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -12494,18 +12494,18 @@ private SyntaxContainer CompileRBranch(MatchTempInfo mti, MatchingContext contex } } - private ExtendedPattern RemoveDisjunctivePatterns(ExtendedPattern pat, bool allowVariables) { + private ExtendedPattern RemoveIllegalSubpatterns(ExtendedPattern pat, bool inDisjunctivePattern) { switch (pat) { case LitPattern: return pat; case IdPattern p: - if (p.Arguments == null && !p.Id.StartsWith("_") && !allowVariables) { - reporter.Error(MessageSource.Resolver, pat.Tok, "Or-patterns may not bind variables"); + if (inDisjunctivePattern && p.Arguments == null && !p.Id.StartsWith("_")) { + reporter.Error(MessageSource.Resolver, pat.Tok, "Disjunctive patterns may not bind variables"); return new IdPattern(p.Tok, FreshTempVarName("_", null), null); } - return new IdPattern(p.Tok, p.Id, p.Arguments?.ConvertAll(a => RemoveDisjunctivePatterns(a, allowVariables))); + return new IdPattern(p.Tok, p.Id, p.Arguments?.ConvertAll(a => RemoveIllegalSubpatterns(a, inDisjunctivePattern))); case DisjunctivePattern p: - reporter.Error(MessageSource.Resolver, pat.Tok, "Or-patterns are not allowed inside other patterns"); + reporter.Error(MessageSource.Resolver, pat.Tok, "Disjunctive patterns are not allowed inside other patterns"); return new IdPattern(p.Tok, FreshTempVarName("_", null), null); default: Contract.Assert(false); @@ -12518,8 +12518,8 @@ private IEnumerable FlattenDisjunctivePatterns(ExtendedPattern // 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 => RemoveDisjunctivePatterns(a, allowVariables: false)) - : Enumerable.Repeat(RemoveDisjunctivePatterns(pat, allowVariables: true), 1); + ? p.Alternatives.ConvertAll(a => RemoveIllegalSubpatterns(a, inDisjunctivePattern: true)) + : Enumerable.Repeat(RemoveIllegalSubpatterns(pat, inDisjunctivePattern: false), 1); } private IEnumerable FlattenNestedMatchCaseExpr(NestedMatchCaseExpr c) { From afb871854c47f9bc80c0f8eec0e93ac682fea407 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= Date: Wed, 20 Jul 2022 17:39:22 -0700 Subject: [PATCH 04/12] ; --- Test/dafny0/OrPatternErrors.dfy.expect | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Test/dafny0/OrPatternErrors.dfy.expect b/Test/dafny0/OrPatternErrors.dfy.expect index e69de29bb2d..48e97b18829 100644 --- a/Test/dafny0/OrPatternErrors.dfy.expect +++ b/Test/dafny0/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 From d326179df4497b1687531242cffcfc9d065608ea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= Date: Thu, 21 Jul 2022 11:35:27 -0700 Subject: [PATCH 05/12] Refactor check for wildcard patterns --- Source/Dafny/AST/DafnyAst.cs | 3 +++ Source/Dafny/Resolver.cs | 6 +++--- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 65d1296a4b8..6c604bd4738 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -12439,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/Resolver.cs b/Source/Dafny/Resolver.cs index 4a431098699..9ab3457df5b 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -12078,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); } } @@ -12500,7 +12500,7 @@ private ExtendedPattern RemoveIllegalSubpatterns(ExtendedPattern pat, bool inDis case LitPattern: return pat; case IdPattern p: - if (inDisjunctivePattern && p.Arguments == null && !p.Id.StartsWith("_")) { + if (inDisjunctivePattern && p.IsWildcardPattern) { reporter.Error(MessageSource.Resolver, pat.Tok, "Disjunctive patterns may not bind variables"); return new IdPattern(p.Tok, FreshTempVarName("_", null), null); } @@ -12652,7 +12652,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 { From aa8d2b11f7e3b9d107bde378692d17b5508d64f0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= Date: Thu, 21 Jul 2022 14:09:13 -0700 Subject: [PATCH 06/12] Move release notes to Upcoming section --- RELEASE_NOTES.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 7383b241f35..8a639acc089 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -1,12 +1,13 @@ # 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 - feat: *Less code navigation when verifying code*: In the IDE, failing postconditions and preconditions error messages now immediately display the sub-conditions that Dafny could not prove. Both on hover and in the Problems window. (https://github.com/dafny-lang/dafny/pull/2434) -- 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) - feat: Whitespaces and comments are kept in relevant parts of the AST (https://github.com/dafny-lang/dafny/pull/1801) - fix: NuGet packages no longer depend on specific patch releases of the .NET frameworks. From d6f9242adf6668faf89c4023861d6bd4539777d0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= Date: Thu, 21 Jul 2022 14:43:48 -0700 Subject: [PATCH 07/12] Fix IsWildcardPattern test --- Source/Dafny/AST/DafnyAst.cs | 2 +- Source/Dafny/Resolver.cs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 6c604bd4738..7d2e847ad33 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -12440,7 +12440,7 @@ public class IdPattern : ExtendedPattern { public LiteralExpr ResolvedLit; // null if just an identifier public bool IsWildcardPattern => - Arguments == null && !Id.StartsWith("_"); + Arguments == null && Id.StartsWith("_"); public void MakeAConstructor() { this.Arguments = new List(); diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 9ab3457df5b..b89186b0dc7 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -12500,7 +12500,7 @@ private ExtendedPattern RemoveIllegalSubpatterns(ExtendedPattern pat, bool inDis case LitPattern: return pat; case IdPattern p: - if (inDisjunctivePattern && p.IsWildcardPattern) { + if (inDisjunctivePattern && 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); } From 1c89a9d7e06bdd54b47be9af2fea21d15b7fd877 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= Date: Thu, 21 Jul 2022 16:06:39 -0700 Subject: [PATCH 08/12] Preserve ResolvedLit and add a test for that case --- Source/Dafny/Resolver.cs | 9 +++++---- Test/dafny0/OrPatterns.dfy | 11 +++++++++++ 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index b89186b0dc7..f59b1fbd891 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -12500,14 +12500,15 @@ private ExtendedPattern RemoveIllegalSubpatterns(ExtendedPattern pat, bool inDis case LitPattern: return pat; case IdPattern p: - if (inDisjunctivePattern && p.Arguments == null && !p.IsWildcardPattern) { + 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); + return new IdPattern(p.Tok, FreshTempVarName("_", null), null, p.IsGhost); } - return new IdPattern(p.Tok, p.Id, p.Arguments?.ConvertAll(a => RemoveIllegalSubpatterns(a, inDisjunctivePattern))); + var args = p.Arguments?.ConvertAll(a => RemoveIllegalSubpatterns(a, inDisjunctivePattern)); + return new IdPattern(p.Tok, p.Id, 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); + return new IdPattern(p.Tok, FreshTempVarName("_", null), null, p.IsGhost); default: Contract.Assert(false); return null; diff --git a/Test/dafny0/OrPatterns.dfy b/Test/dafny0/OrPatterns.dfy index acbda2df77e..7062fc19295 100644 --- a/Test/dafny0/OrPatterns.dfy +++ b/Test/dafny0/OrPatterns.dfy @@ -21,6 +21,17 @@ datatype Enum = One | Two | Three { 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 { From a0c4848152811efdb005b4b2d191967daa806786 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= Date: Thu, 21 Jul 2022 17:41:07 -0700 Subject: [PATCH 09/12] Format --- Source/Dafny/Resolver.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index f59b1fbd891..d5f5513ca90 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -12505,7 +12505,7 @@ private ExtendedPattern RemoveIllegalSubpatterns(ExtendedPattern pat, bool inDis 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, args, p.IsGhost) {ResolvedLit = p.ResolvedLit}; + return new IdPattern(p.Tok, p.Id, 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); From b04bdf1a2d579612b737413139e5b3db325e629a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= Date: Thu, 21 Jul 2022 23:14:00 -0700 Subject: [PATCH 10/12] Preserve pattern type --- Source/Dafny/Resolver.cs | 2 +- Test/{dafny0 => patterns}/OrPatternErrors.dfy | 0 Test/{dafny0 => patterns}/OrPatternErrors.dfy.expect | 0 Test/{dafny0 => patterns}/OrPatterns.dfy | 0 Test/{dafny0 => patterns}/OrPatterns.dfy.expect | 0 5 files changed, 1 insertion(+), 1 deletion(-) rename Test/{dafny0 => patterns}/OrPatternErrors.dfy (100%) rename Test/{dafny0 => patterns}/OrPatternErrors.dfy.expect (100%) rename Test/{dafny0 => patterns}/OrPatterns.dfy (100%) rename Test/{dafny0 => patterns}/OrPatterns.dfy.expect (100%) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index d5f5513ca90..504631395e0 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -12505,7 +12505,7 @@ private ExtendedPattern RemoveIllegalSubpatterns(ExtendedPattern pat, bool inDis 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, args, p.IsGhost) { ResolvedLit = p.ResolvedLit }; + 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); diff --git a/Test/dafny0/OrPatternErrors.dfy b/Test/patterns/OrPatternErrors.dfy similarity index 100% rename from Test/dafny0/OrPatternErrors.dfy rename to Test/patterns/OrPatternErrors.dfy diff --git a/Test/dafny0/OrPatternErrors.dfy.expect b/Test/patterns/OrPatternErrors.dfy.expect similarity index 100% rename from Test/dafny0/OrPatternErrors.dfy.expect rename to Test/patterns/OrPatternErrors.dfy.expect diff --git a/Test/dafny0/OrPatterns.dfy b/Test/patterns/OrPatterns.dfy similarity index 100% rename from Test/dafny0/OrPatterns.dfy rename to Test/patterns/OrPatterns.dfy diff --git a/Test/dafny0/OrPatterns.dfy.expect b/Test/patterns/OrPatterns.dfy.expect similarity index 100% rename from Test/dafny0/OrPatterns.dfy.expect rename to Test/patterns/OrPatterns.dfy.expect From 5dbd839cccf5f8845fab1a7e3a399c4d33f4cf7f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= Date: Thu, 21 Jul 2022 23:49:19 -0700 Subject: [PATCH 11/12] Fix test output --- Test/patterns/OrPatterns.dfy.expect | 2 -- 1 file changed, 2 deletions(-) diff --git a/Test/patterns/OrPatterns.dfy.expect b/Test/patterns/OrPatterns.dfy.expect index d8ec0e6ecfc..55701992ee3 100644 --- a/Test/patterns/OrPatterns.dfy.expect +++ b/Test/patterns/OrPatterns.dfy.expect @@ -1,5 +1,3 @@ Dafny program verifier finished with 7 verified, 0 errors -Running... - OK From b39ac541f52eefc1225961dcb781134d4c617e53 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= Date: Fri, 22 Jul 2022 00:04:00 -0700 Subject: [PATCH 12/12] Don't clone the body of the matches (see dafny-lang/dafny#2334) --- Source/Dafny/Resolver.cs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 504631395e0..176c88b87dc 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -11958,7 +11958,7 @@ public RBranchStmt(IToken tok, int branchid, List patterns, Lis public RBranchStmt(int branchid, NestedMatchCaseStmt x, Attributes attrs = null) : base(x.Tok, branchid, new List()) { Contract.Requires(!(x.Pat is DisjunctivePattern)); // No nested or patterns - this.Body = new List(x.Body); // Resolving the body will insert new elements. + this.Body = new List(x.Body); // Resolving the body will insert new elements. this.Attributes = attrs; this.Patterns.Add(x.Pat); } @@ -12527,14 +12527,14 @@ private IEnumerable FlattenDisjunctivePatterns(ExtendedPattern private IEnumerable FlattenNestedMatchCaseExpr(NestedMatchCaseExpr c) { var cloner = new Cloner(); foreach (var pat in FlattenDisjunctivePatterns(c.Pat)) { - yield return new NestedMatchCaseExpr(c.Tok, pat, cloner.CloneExpr(c.Body), cloner.CloneAttributes(c.Attributes)); + 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, c.Body.ConvertAll(cloner.CloneStmt), cloner.CloneAttributes(c.Attributes)); + yield return new NestedMatchCaseStmt(c.Tok, pat, new List(c.Body), c.Attributes); } }