Fix crash and add test (#5447)

Fixes #4860

### Description
- Fix crash by adding missing error report

### How has this been tested?
- Added CLI test for crash

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs

@@ -1,6 +1,7 @@
 using System;
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.IO;
 using System.Linq;
 
 namespace Microsoft.Dafny;
@@ -35,4 +36,10 @@ public class NestedMatchCaseExpr : NestedMatchCase, IAttributeBearingDeclaration
  resolver.ConstrainSubtypeRelation(resultType, Body.Type, Body.tok, "type of case bodies do not agree (found {0}, previous types {1})", Body.Type, resultType);
  }
  }
+
+ public override string ToString() {
+ var writer = new StringWriter();
+ new Printer(writer, DafnyOptions.Default).PrintNestedMatchCase(false, false, this, false, false);
+ return writer.ToString();
+ }
 }

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

@@ -97,14 +97,13 @@ public abstract class ExtendedPattern : TokenNode {
  Contract.Assert(tupleTypeDecl.Ctors[0] == tupleTypeDecl.GroundingCtor);
  idpat.Ctor = tupleTypeDecl.GroundingCtor;
 
- //We expect the number of arguments in the type of the matchee and the provided pattern to match, except if the pattern is a bound variable
- if (udt.TypeArgs.Count != idpat.Arguments.Count) {
+ if (idpat.Id != tupleTypeDecl.GroundingCtor.Name) {
  if (idpat.Id.StartsWith(SystemModuleManager.TupleTypeCtorNamePrefix)) {
  resolver.reporter.Error(MessageSource.Resolver, this.Tok,
  $"the case pattern is a {idpat.Arguments.Count}-element tuple, while the match expression is a {udt.TypeArgs.Count}-element tuple");
  } else {
- resolver.reporter.Error(MessageSource.Resolver, this.Tok,
- $"case pattern {idpat.Id} has {idpat.Arguments.Count} arguments whereas the match expression has {udt.TypeArgs.Count}");
+ resolver.Reporter.Error(MessageSource.Resolver, idpat.Tok,
+ $"found constructor {idpat.Id} but expected a {tupleTypeDecl.Dims}-tuple");
  }
  }
 

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

@@ -13,7 +13,9 @@ public class IdPattern : ExtendedPattern, IHasUsages {
  public String Id;
  public PreType PreType;
  public Type Type; // This is the syntactic type, ExtendedPatterns disappear during resolution.
- public IVariable BoundVar { get; set; }
+
+ public IVariable BoundVar { get; set; } // Only set if there are no arguments
+
  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
  [FilledInDuringResolution]

Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs

@@ -1145,12 +1145,7 @@ void PrintCasePattern<VT>(CasePattern<VT> pat)
  int i = 0;
  foreach (var mc in e.Cases) {
  bool isLastCase = i == e.Cases.Count - 1;
- wr.Write(" case");
- PrintAttributes(mc.Attributes);
- wr.Write(" ");
- PrintExtendedPattern(mc.Pat);
- wr.Write(" => ");
- PrintExpression(mc.Body, isRightmost && isLastCase, !parensNeeded && isFollowedBySemicolon);
+ PrintNestedMatchCase(isRightmost, isFollowedBySemicolon, mc, isLastCase, parensNeeded);
  i++;
  }
  if (e.UsesOptionalBraces) { wr.Write(" }"); } else if (parensNeeded) { wr.Write(")"); }
@@ -1202,5 +1197,15 @@ void PrintCasePattern<VT>(CasePattern<VT> pat)
  Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
  }
  }
+
+ public void PrintNestedMatchCase(bool isRightmost, bool isFollowedBySemicolon, NestedMatchCaseExpr mc, bool isLastCase,
+ bool parensNeeded) {
+ wr.Write(" case");
+ PrintAttributes(mc.Attributes);
+ wr.Write(" ");
+ PrintExtendedPattern(mc.Pat);
+ wr.Write(" => ");
+ PrintExpression(mc.Body, isRightmost && isLastCase, !parensNeeded && isFollowedBySemicolon);
+ }
  }
 }

Source/DafnyLanguageServer/Workspace/IdeState.cs

@@ -206,6 +206,7 @@ public record IdeState(
  var ownedUris = new HashSet<Uri>();
  foreach (var file in determinedRootFiles.Roots) {
  var uriProject = await projectDatabase.GetProject(file.Uri);
+ logger.LogDebug($"HandleDeterminedRootFiles found project for {file.Uri} to be {uriProject.Uri}");
  var ownedUri = uriProject.Equals(determinedRootFiles.Project);
  if (ownedUri) {
  ownedUris.Add(file.Uri);

Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/constructorInsteadOfTuple.dfy

@@ -0,0 +1,29 @@
+// RUN: ! %resolve "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype Expr =
+ | Const(value: int)
+ | Var(name: string)
+ | Add(left: Expr, right: Expr)
+ | Mult(left: Expr, right: Expr)
+
+function Optimize(expr: Expr): Expr
+{
+ match expr
+ case Const(value) => Const(value)
+ case Var(name) => Var(name)
+ case Add(left, right) =>
+ match (Optimize(left), Optimize(right))
+ case (Const(lv), Const(rv)) => Const(lv + rv)
+ case (Const(0), rv) => rv
+ case (lv, Const(0)) => lv
+ case (lv, rv) => Add(lv, rv)
+ case Mult(left, right) =>
+ match (Optimize(left), Optimize(right))
+ case (Const(lv), Const(rv)) => Const(lv * rv)
+ case (Const(0), _) => Const(0)
+ case (_, Const(0)) => Const(0)
+ case (Const(1), rv) => rv
+ case (lv, Const(1)) => lv
+ case (lv, rv) => Mult(lv, rv)
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/constructorInsteadOfTuple.dfy.expect

@@ -0,0 +1,2 @@
+constructorInsteadOfTuple.dfy(21,21): Error: found constructor Mult but expected a 2-tuple
+1 resolution/type errors detected in constructorInsteadOfTuple.dfy

docs/dev/news/4860.fix

@@ -0,0 +1 @@
+- Fix crash that could occur when using a constructor in a match pattern where a tuple was expected