Resolve match before compile #2734

keyboardDrummer · 2022-09-13T17:41:20Z

Changes

A nested match is one where a single case may match on multiple destructors, organised in a tree. A nested match case may also match on a constant value. A simple match case may only match on a single constructor. The process of compiling/denesting/flattening nested matches, transforms nested matches into if statements and simple matches.

Previously the flattening was done during resolution, but this PR moves it further back in the pipeline so the resolved AST does not have the flattening applied to it. The flattening is still computed during resolution, but it is stored in a new field instead of being applied to the resolved AST. That way, the IDE can derive code navigation from the unflattened AST, but still emit warnings produced by the flattening. Using the flattened results is done in verification and compilation by traversing the new field.

I think more idiomatically would be not to have the newly added field flattened inside NestedMatchExpr/Stmt, and instead fully replace the NestedMatchExpr/Stmt node, since that would prevent having to add code in the backends. However, we don't have a good mechanism for replacing AST nodes yet. Also, doing that would require being able to set up a transformation that runs after resolution, so it doesn't affect the IDE's code navigation, but before verification and code generation, so both of those can benefit from it, and we don't have a good mechanism for that either. I also wonder whether that would require cloning the AST right after resolution so it's preserved for code navigation. However, I think such mechanisms could benefit code generators that produce warnings after doing other transformations, so it's not a ton of work just for nested matches.

Code related to the flattening of nested matches has been moved out of Resolver.cs and into a new file MatchFlattener.cs. Code related to resolving nested matches has been moved out of resolver and into the related AST nodes. Simple matches no longer have resolution code since they're instantiated already resolved. Resolution of nested matches is currently done in two phases, the 'Check' and 'Resolve' phase, that can be merged, but I'll leave that for a follow-up PR.

The was a small transformation that was done during match flattening, which transforms explicit type annotations on bound case variables, by replacing them with a let statement around the body of the case, where the bound let variable carries the explicit type annotation. This transformation has been moved to the resolution phase of nested matches. Possibly we don't need this transformation, but I leave removing or moving it for a follow-up PR.

Fix a bug related to matches and ghost constructors. In the following program, D0 is non-ghost, but previously the match was still considered to be ghost because XY has constructors other than D0 that are ghost.

  method P0(xy: XY) returns (r: int) {
-    // the following match statement is ghost, because it indirectly mentions a ghost constructor of type XY
+   // the following match statement is non-ghost, because it does not mention a ghost constructor of type XY
    match xy
-    case D0(_) => r := 0; // error: assignment to r in a ghost context
+   case D0(_) => r := 0;
     case any =>
  }

Testing

Some commented assertions in the test DefinitionTests.DatatypesAndMatches have been uncommented, to test the additionally supported behavior.
Update Test/dafny0/GhostDatatypeConstructors-Resolution.dfy to capture new behavior.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

RustanLeino · 2022-09-21T16:59:11Z

This is great! This will make many things better. For example, it will help my new type inference and will aid in producing good linter warnings about the user's given syntax.

…r/dafny into resolveMatchBeforeCompile

…ompile

…t, expr or stmt

atomb

Just a few cleanup changes and questions. Otherwise I think this looks good, and makes the treatment of nested matches easier to understand.

atomb · 2023-01-03T22:00:41Z

Source/DafnyCore/Resolver/ResolverBottomUpVisitor.cs

+
+namespace Microsoft.Dafny;
+
+class ResolverBottomUpVisitor : BottomUpVisitor {


It looks like this class still also exists inside Resolver.cs. Was that intentional?

atomb · 2023-01-03T22:04:37Z

Source/DafnyCore/AST/Expressions/NestedMatchStmt.cs

-  public override IEnumerable<Statement> SubStatements =>
-    ResolvedStatement == null ? Cases.SelectMany(c => c.Body) : base.SubStatements;
+  public override IEnumerable<Statement> SubStatements {
+    get {


Why make this use a get block instead of => like before?

atomb · 2023-01-03T22:14:25Z

Source/DafnyCore/Resolver/LinkedList.cs

+  }
+}
+
+public abstract record LinkedList<T> : IEnumerable<T> {


Why can't you use System.Collections.Generic.LinkedList?

That's a doubly linked list and this is a single one, which allows easily grabbing just the tail. I will rename this one to make it more clear.

atomb · 2023-01-03T22:20:51Z

Source/DafnyCore/Resolver/Resolver.cs

@@ -8558,6 +7362,14 @@ public CollectFriendlyCallsInSpec_Visitor(Resolver resolver, ISet<Expression> fr
    }
  }

+  abstract class ResolverTopDownVisitor<T> : TopDownVisitor<T> {


This class appears to be duplicated.

atomb · 2023-01-03T22:28:10Z

Source/DafnyCore/AST/Expressions/Expressions.cs

-/// it gets "replaced" by the statement in "ResolvedStatement".
-/// Adapted from ConcreteSyntaxStatement
-/// </summary>
-public abstract class ConcreteSyntaxStatement : Statement {


I'm happy to see this go away!

Yes but NestedMatchStmt.Flattened came in its place so I'm not sure if it's an improvement 😅 I considered changing ConcreteSyntaxStatement and ConcreteSyntaxExpression so they would have not only a resolvedX but also a compiledX field, instead of the current Flattened property. That would reduce the code added to Translator.cs and SinglePassCompiler.cs, and add opportunities for other post resolution compilation passes.

Good point. But one advantage to NestedMatchStmt.Flattened is that it's clear that it's used for one thing, whereas ConcreteSyntaxStatement sounds like it could cover many instances of concrete syntax, even if it didn't, in practice.

atomb · 2023-01-03T23:52:56Z

Source/DafnyCore/AST/Expressions/ExtendedPattern.cs

+  *  4 - An IdPattern at datatype type with no arguments representing a bound variable
+  */
+  public void CheckLinearExtendedPattern(Type type, ResolutionContext resolutionContext, Resolver resolver) {
+    if (type == null) {


Under what circumstances might this happen?

That doesn't seem possible to me. Note this is an existing check, this method was moved from Resolver.cs. In a follow-up PR, I will merge CheckLinearExtendedPattern and ExtendedPattern.Resolve and maybe this can go then.

atomb · 2023-01-04T00:15:06Z

Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs

+
+    // Get the datatype of the matchee
+    var currMatcheeType = currMatchee.Type
+    // resolver.PartiallyResolveTypeForMemberSelection(currMatchee.tok, currMatchee.Type)


Perhaps remove this commented-out code?

atomb · 2023-01-04T00:15:16Z

Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs

+      .NormalizeExpand();
+    // if (currMatcheeType is TypeProxy) {
+    //   resolver.PartiallySolveTypeConstraints(true);
+    // }


Remove this, as well?

atomb · 2023-01-04T00:15:37Z

Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs

+    if (dtd == null) {
+      ctors = null;
+    } else {
+      ctors = dtd.Ctors.ToDictionary(c => c.Name, c => c); //resolver.datatypeCtors[dtd];


Obsolete comment?

atomb · 2023-01-04T00:17:50Z

Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs

+    }
+  }
+
+  // TODO use a record.


Is there any reason not to do this right away?

…r/dafny into resolveMatchBeforeCompile

atomb

Looks great!

Fixes #3333 The actual fix was already accidentally made in #2734, this PR is just adding a test case and a release note, and removing some obsolete code. <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>

During PR dafny-lang#2734, a refactoring of the cloner mistakenly omitted a clone call for one sub-expression of TypeRHS, leading to issue dafny-lang#3343. This PR reinstates that clone. Fixes dafny-lang#3343.

During PR #2734, a refactoring of the cloner mistakenly omitted a clone call for one sub-expression of TypeRHS, leading to issue #3343. This PR reinstates that clone. Fixes #3343.

During PR dafny-lang#2734, a refactoring of the cloner mistakenly omitted a clone call for one sub-expression of TypeRHS, leading to issue dafny-lang#3343. This PR reinstates that clone. Fixes dafny-lang#3343.

keyboardDrummer self-assigned this Sep 15, 2022

keyboardDrummer added 28 commits October 4, 2022 14:27

Small fix

7527220

Run formatter

bbeb012

Refactor CompileNestedMatch

135fc5e

Refactor CompileNestedMatch take2

2e86af7

Further refactoring of CompileNestedMatch

ed423c9

Refactoring

1fdc9c9

Fix bugs related to nested match constructs

9edf54d

Move unnested match AST

ff6e47a

Override ToString for statements

4127e8e

Fix accidental Body reuse bug

7a41faf

Printing changes

58e711f

Allow cloning with resolved fields

63de739

PatternMatching.dfy passes

619b238

Ran formatter

7a11b6b

Merge branch 'resolveMatchBeforeCompile' of github.com:keyboardDrumme…

c9a59df

…r/dafny into resolveMatchBeforeCompile

Merge remote-tracking branch 'origin/master' into resolveMatchBeforeC…

6d89b73

…ompile

More cloning if resolved fields

3eaa042

Merge remote-tracking branch 'origin/master' into resolveMatchBeforeC…

373e422

…ompile

Tiny refac

ae8b336

Remove bad cast

4f32cec

Ran formatter

e91b271

Bring back pre-resolve processing of explicit bound variable types

83c9458

Ran formatter

a437955

Add missing type annotation

5991bc6

Update cloner for all inheritors of ConcreteSyntaxExpression

6977673

NameSegment creation improvement, refactoring, and test updates

f76bd59

Let IdPattern use a BoundVar or LocalVariable depending on the contex…

40b5dfd

…t, expr or stmt

Merge branch 'master' into resolveMatchBeforeCompile

3ee3856

Fix comp error

3059618

keyboardDrummer requested review from robin-aws and atomb and removed request for robin-aws January 3, 2023 17:26

atomb requested changes Jan 4, 2023

View reviewed changes

keyboardDrummer added 7 commits January 4, 2023 13:36

Code review

ba64de2

Apply TODO

0e850be

Merge branch 'master' into resolveMatchBeforeCompile

5ecb444

Merge branch 'resolveMatchBeforeCompile' of github.com:keyboardDrumme…

2ed841c

…r/dafny into resolveMatchBeforeCompile

Move SinglyLinkedList

2040d73

Resolve TODO that removes SyntaxContainer

74e7ecd

Remove TODO

4589aed

keyboardDrummer enabled auto-merge (squash) January 4, 2023 13:45

keyboardDrummer requested a review from atomb January 4, 2023 13:46

keyboardDrummer added 4 commits January 4, 2023 14:50

Remove .Reverse call

b319033

Fix

513fe70

Refactor

97d3fb3

Fix NRE

6644b8c

atomb approved these changes Jan 4, 2023

View reviewed changes

keyboardDrummer merged commit a8afc97 into dafny-lang:master Jan 4, 2023

keyboardDrummer deleted the resolveMatchBeforeCompile branch January 4, 2023 17:57

keyboardDrummer mentioned this pull request Jan 6, 2023

Add test case and release notes for 3333 fix #3334

Merged

robin-aws mentioned this pull request Jan 8, 2023

Regression from #2734: dangling reference in array size #3343

Closed

atomb mentioned this pull request Jan 10, 2023

Add a missing expression clone #3346

Merged

stefan-aws mentioned this pull request Feb 1, 2023

Release Dafny 3.11.0 #3432

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Resolve match before compile #2734

Resolve match before compile #2734

keyboardDrummer commented Sep 13, 2022 •

edited

RustanLeino commented Sep 21, 2022

atomb left a comment

atomb Jan 3, 2023

atomb Jan 3, 2023

atomb Jan 3, 2023

keyboardDrummer Jan 4, 2023

atomb Jan 3, 2023

atomb Jan 3, 2023

keyboardDrummer Jan 4, 2023 •

edited

atomb Jan 4, 2023

atomb Jan 3, 2023

keyboardDrummer Jan 4, 2023

atomb Jan 4, 2023

atomb Jan 4, 2023

atomb Jan 4, 2023

atomb Jan 4, 2023

atomb left a comment


		namespace Microsoft.Dafny;

		class ResolverBottomUpVisitor : BottomUpVisitor {

Resolve match before compile #2734

Resolve match before compile #2734

Conversation

keyboardDrummer commented Sep 13, 2022 • edited

Changes

Testing

RustanLeino commented Sep 21, 2022

atomb left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Jan 4, 2023 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

atomb left a comment

Choose a reason for hiding this comment

keyboardDrummer commented Sep 13, 2022 •

edited

keyboardDrummer Jan 4, 2023 •

edited