feat: Add support for disjunctive (“or”) patterns

RELEASE_NOTES.md

@@ -1,6 +1,8 @@
 # 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.
 

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<ExtendedPattern> Alternatives;
+ public DisjunctivePattern(IToken tok, List<ExtendedPattern> 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
 

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;

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) {

Source/Dafny/Dafny.atg

@@ -3289,7 +3289,7 @@ BindingGuard<out Expression e, bool allowLambda>
 
 
 /*------------------------------------------------------------------------*/
-ExtendedPattern<.out ExtendedPattern pat.>
+SingleExtendedPattern<.out ExtendedPattern pat.>
 = (. IToken id; List<ExtendedPattern> arguments;
  Expression lit; BoundVar bv;
  pat = null;
@@ -3324,6 +3324,17 @@ ExtendedPattern<.out ExtendedPattern pat.>
  .)
  .
 
+/*------------------------------------------------------------------------*/
+ExtendedPattern<.out ExtendedPattern pat.>
+= (. List<ExtendedPattern> branches = null;
+ ExtendedPattern branch = null; .)
+ SingleExtendedPattern<out branch>
+ { "|" (. branches ??= new() { branch }; .)
+ SingleExtendedPattern<out branch> (. branches.Add(branch); .)
+ }
+ (. pat = branches == null ? branch : new DisjunctivePattern(branches[0].Tok, branches); .)
+ .
+
 /*------------------------------------------------------------------------*/
 MatchStmt<out Statement/*!*/ s>
 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);

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<Thing> {
@@ -11947,6 +11938,7 @@ private abstract class RBranch {
  public List<ExtendedPattern> Patterns;
 
  public RBranch(IToken tok, int branchid, List<ExtendedPattern> 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<ExtendedPattern> patterns, Lis
  }
 
  public RBranchStmt(int branchid, NestedMatchCaseStmt x, Attributes attrs = null) : base(x.Tok, branchid, new List<ExtendedPattern>()) {
+ Contract.Requires(!(x.Pat is DisjunctivePattern)); // No nested or patterns
  this.Body = new List<Statement>(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<Expression> 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<Expression> matchees, List<Tuple<ExtendedPattern, RBranch>> 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<ExtendedPattern> 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<NestedMatchCaseExpr> 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<NestedMatchCaseStmt> 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<RBranch> branches = new List<RBranch>();
- 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<RBranch> branches = new List<RBranch>();
- 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;

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
+ }
+}

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<T> = Nil | Cons(car: T, cdr: List<T>) {
+ function {:fuel 5} Length(): nat {
+ match this
+ case Nil => 0
+ case Cons(_, t) => 1 + t.Length()
+ }
+ }
+
+ predicate method ContainsOne(l: List<int>)
+ requires l.Length() == 3
+ {
+ l.car == 1 || l.cdr.car == 1 || l.cdr.cdr.car == 1
+ }
+
+ predicate method ContainsOne'(l: List<int>)
+ 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<int>)
+ 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";
+}

Test/dafny0/OrPatterns.dfy.expect

@@ -0,0 +1,5 @@
+
+Dafny program verifier finished with 7 verified, 0 errors
+Running...
+
+OK