Ordered, nested matching of datatypes and constants

[osavaryb]

Added support for ordered, nested matching of datatypes and constants.

[robin-aws]

AWS CodeBuild CI Report

• CodeBuild project: Dafny
• Commit ID: a9ec0cd
• Result: SUCCEEDED
• Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

[osavaryb]

Return path, inductive lemmas

In Test/dafny3/Inc.dfy.expect, the "this return path" location has changed (from before the PR). All the places where this occurs (which I think is just in this file) in this file seem to be in inductive lemmas. Is there a bug to look into there?

Location of case, not variable declaration> L9 of Test/git-issues/git-issue-495.dfy L9 and L565 of Test/dafny0/ResolutionErrors.dfy seem like they may be the same problem. It seems that the bound variable gets the location of the enclosing constructor. Can this be changed?

I'll have a closer look at this over the weekend, the second issue (with git-issue-495 and ResolutionErrors) is due to how the selector's token (used when generating fresh variables in the PM compiler) is overwritten by the RBranch's token when let-bound in that branch. I should be able to get better error location by overwriting these token earlier. 

Missing-case error messages

In a program like:

function F(xs: List): int {
  match xs  // missing case in case statement: Nil
  case Cons(x, Cons(y, rest)) => 5
  case Nil => 8
}

I don't find the error message as helpful as I would wish. The missing Nil is not the one that is given in the function, but the Nil in Cons(_, Nil). Is there a way to make such error messages more specific?
This is a bit complicated since the missing case error is thrown by the verifier while doing a semantic exhaustiveness check...I may be able to generate the missingCases during NestedMatch desugaring instead of while resolving the Match.

There's also something else with this message. There are no "case statements" in Dafny--they are "match statements". Furthermore, the function above does not have a "match statement" but a "match expression".

This is unrelated to the PR, but I will update the error messages in Translator.cs

Verification message for missing case

In the program

datatype Dt = Real(real)
method U(d: Dt) {
  match d  // assertion violation
  case Real(15.0) =>
}

This program is erroneous, because it's missing cases for non-15.0 reals. However, the error message is just the mysterious "assertion violation". This should be improved.

 This example gets desugared to  match d {
    case Real(_mcc#0: real) =>
      {
        assert _mcc#0 == 15.0;
      }
I may be able to do better by attaching a custom error message to the assertion generated by the lack of default case in a constant match.

Checking redundant cases

The analysis incorrectly reports a "redundant branch" error for this program:

datatype PairOfNumbers = P(int, int)
method M(p: PairOfNumbers) {
  match p
  case P(10, 10) =>
  case P(10, 11) =>  // this branch is redundant
  case _ =>
}

Fixed (and added as test case in PatternMatching.dfy), thank you!

[RustanLeino]

I reviewed the latest commits. Thank you for the changes!

I'm thinking the only remaining issue is getting the tests to all pass (StateMonad.dfy is failing).