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

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 #2334 for details.

Closes #2220.

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
 

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
 
@@ -12430,6 +12439,9 @@ public class IdPattern : ExtendedPattern {
     public List<ExtendedPattern> 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<ExtendedPattern>();
     }

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<BoundVar> boundVars, Attributes attrs, Expression range) {
       Contract.Requires(boundVars != null);
       string sep = "";

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> {
@@ -11948,6 +11939,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;
@@ -11965,7 +11957,8 @@ 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>()) {
-        this.Body = new List<Statement>(x.Body); // Resolving the body will insert new elements. 
+        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);
       }
@@ -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<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);
       }
@@ -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<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 => RemoveIllegalSubpatterns(a, inDisjunctivePattern: true))
+        : Enumerable.Repeat(RemoveIllegalSubpatterns(pat, inDisjunctivePattern: false), 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, c.Body, 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, new List<Statement>(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<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;
       }
@@ -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<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;
       }
@@ -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;

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

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