Fix: Compiled disjunctive nested pattern matching no longer crashing

Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs

@@ -22,10 +22,12 @@ public class IdPattern : ExtendedPattern, IHasReferences {
   public DatatypeCtor Ctor;
 
   public bool IsWildcardPattern =>
-    Arguments == null && Id.StartsWith("_");
+    Arguments == null && Id.StartsWith(WildcardString);
 
   public bool IsWildcardExact =>
-    Arguments == null && Id == "_";
+    Arguments == null && Id == WildcardString;
+
+  public const string WildcardString = "_";
 
   public void MakeAConstructor() {
     this.Arguments = new List<ExtendedPattern>();

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs

@@ -594,6 +594,10 @@ private ConcreteSyntaxTree EmitNestedMatchCaseConditions(string sourceName,
         writer = thenWriter;
       } else if (pattern is IdPattern idPattern) {
         if (idPattern.BoundVar != null) {
+          if (idPattern.BoundVar.Tok.val.StartsWith(IdPattern.WildcardString)) {
+            return writer;
+          }
+
           var boundVar = idPattern.BoundVar;
           var valueWriter = DeclareLocalVar(IdName(boundVar), boundVar.Type, idPattern.Tok, writer);
           valueWriter.Write(sourceName);
@@ -651,9 +655,11 @@ private ConcreteSyntaxTree EmitNestedMatchStmtCaseConstructor(string sourceName,
           var childPattern = idPattern.Arguments[index];
           if (childPattern is IdPattern { BoundVar: not null } childIdPattern) {
             var boundVar = childIdPattern.BoundVar;
-            newSourceName = IdName(boundVar);
-            var valueWriter = DeclareLocalVar(newSourceName, boundVar.Type, idPattern.Tok, result);
-            valueWriter.Append(destructor);
+            if (!childIdPattern.BoundVar.Name.StartsWith(IdPattern.WildcardString)) {
+              newSourceName = IdName(boundVar);
+              var valueWriter = DeclareLocalVar(newSourceName, boundVar.Type, idPattern.Tok, result);
+              valueWriter.Append(destructor);
+            }
           } else {
             newSourceName = ProtectedFreshId(arg.CompileName);
             var valueWriter = DeclareLocalVar(newSourceName, type, idPattern.Tok, result);

Source/DafnyCore/GeneratedFromDafny/DAST_Format.cs

@@ -17,12 +17,12 @@ public static BigInteger SeqToHeight<__T>(Dafny.ISequence<__T> s, Func<__T, BigI
       if ((new BigInteger((s).Count)).Sign == 0) {
         return BigInteger.Zero;
       } else {
-        BigInteger _763_i = Dafny.Helpers.Id<Func<__T, BigInteger>>(f)((s).Select(BigInteger.Zero));
-        BigInteger _764_j = DAST.Format.__default.SeqToHeight<__T>((s).Drop(BigInteger.One), f);
-        if ((_763_i) < (_764_j)) {
-          return _764_j;
+        BigInteger _759_i = Dafny.Helpers.Id<Func<__T, BigInteger>>(f)((s).Select(BigInteger.Zero));
+        BigInteger _760_j = DAST.Format.__default.SeqToHeight<__T>((s).Drop(BigInteger.One), f);
+        if ((_759_i) < (_760_j)) {
+          return _760_j;
         } else {
-          return _763_i;
+          return _759_i;
         }
       }
     }

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5572.dfy

@@ -0,0 +1,14 @@
+// RUN: %testDafnyForEachCompiler "%s"
+
+datatype D = A(int) | C(int) {
+  function Test(): D {
+    match this{
+      case A(_) | C(_) =>
+        this
+    }
+  }
+}
+method Main() {
+  var x := C(0).Test();
+  print "ok";
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5572.dfy.expect

@@ -0,0 +1 @@
+ok

docs/dev/news/5572.fix

@@ -0,0 +1 @@
+Compiled disjunctive nested pattern matching no longer crashing