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

cpitclaudel · 2022-07-19T17:10:30Z

Source/Dafny/AST/DafnyAst.cs (DisjunctivePattern):
New subclass of ExtendedPattern.
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.
(RemoveDisjunctivePatterns): 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.

* `Source/Dafny/AST/DafnyAst.cs` (`DisjunctivePattern`): New subclass of `ExtendedPattern`. * `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. (`RemoveDisjunctivePatterns`): 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. Closes #2220.

keyboardDrummer · 2022-07-20T22:33:53Z

Source/Dafny/AST/Printer.cs

@@ -2870,6 +2870,14 @@ public class Printer {
 wr.Write(")");
 }
 break;
+ case DisjunctivePattern dp:
+ var psep = "";


Seems like we have a difference in style preference. I always write names out in full, so here it would be pattern or disjunctivePattern and patternSeparator. Maybe we can agree on that we should optimise for reading? Would that change your preference?

In general I find the shorter names more readable:

(-b + sqr(b*b - 4*a*c)) / (2 * a) vs (-linearFactor +- squareRoot(linearFactor * linearFactor - 4 * quadraticFactor * constantFactor)) / (2 * quadraticFactor)

In the snippet you highlighted (where there's a single variable) I don't have strong preferences; I just followed the style of the code right above.

For externally visible parameters (like function arguments or class fields) I prefer long names.

I think your example is more fair if you also include the legend for the small variable names, and add line breaks:

var a = quadraticFactor; var b = linearFactor; var c = constantFactor; return (-b + sqr(b*b - 4*a*c)) / (2 * a)

vs

return (-linearFactor + squareRoot(linearFactor * linearFactor - 4 * quadraticFactor * constantFactor)) / (2 * quadraticFactor)

keyboardDrummer · 2022-07-20T22:47:08Z

Source/Dafny/Resolver.cs

+ private IEnumerable<NestedMatchCaseStmt> FlattenNestedMatchCaseStmt(NestedMatchCaseStmt c) {
+ var cloner = new Cloner();
+ foreach (var pat in FlattenDisjunctivePatterns(c.Pat)) {
+ yield return new NestedMatchCaseStmt(c.Tok, pat, c.Body.ConvertAll(cloner.CloneStmt), cloner.CloneAttributes(c.Attributes));


Why do you need to clone here instead of use the old body and attributes? Will you be using the old cases?

Yes, the old body and attributes are used in the linearity checker.

But still, what happens if you don't clone them?

Most likely Dafny will crash. My answer above wasn't complete: notice how I don't clone pat, because this one isn't being shared. But I do need to clone c.Body, because that's the same body being copied into each newly created NestedMatchCaseStmt. Basically this code goes from:

case A | B | C => body

to

case A => Clone(body) case B => Clone(body) case C => Clone(body)

If we don't clone the body we'll have multiple places in the AST sharing the same reference to the body (and typechecking it multiple times, among other things)

Makes sense, thanks!

It made sense, but I was wrong :/ The crash I had observed was not due to not cloning, and in fact not cloning is wrong here, because of #2334 (the key point being that the branches are already partly resolved, and hence cloning them isn't safe). Thanks for flagging this.

keyboardDrummer · 2022-07-20T22:48:31Z

Source/Dafny/Resolver.cs

@@ -12510,12 +12545,13 @@ private class RBranchExpr : RBranch {
 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();


What is the right time for flattening the disjunctive patterns? Can't that be done before resolution as a separate rewriter?

Possibly, but I'm not sure it's what we want: I wrote it this way to give other code access to the disjunctive patterns. I think of this flattening as an implementation detail of the pattern compiler.

I wrote it this way to give other code access to the disjunctive patterns.

Didn't we want to use many small lowering transformations when possible, to make each individual transformation simpler? I think it would be a big benefit if we can avoid adding code to Resolver.cs.

Also, in what scenario do you envision someone needs access to disjunctive patterns? And if they need it, why couldn't they sit before the lowering transformation?

Didn't we want to use many small lowering transformations when possible, to make each individual transformation simpler?

Indeed, and we have that here, right? There's just a handful of calls in the resolver to new code that pre-processes the pattern.

I think it would be a big benefit if we can avoid adding code to Resolver.cs.

I can move it to a new file, but all of the other pattern matching compilation code is there, so… ?

Originally, the pattern matching compiler was implemented all in the parser. It was moved to the resolver, and in fact it should really be moved to the compiler. In fact, in the long run, disjunctive patterns should be supported at any level of nesting, so the nice separation we have right now won't survive. But for now it's good to have the separated implementation.

Indeed, and we have that here, right? There's just a handful of calls in the resolver to new code that pre-processes the pattern.
I can move it to a new file, but all of the other pattern matching compilation code is there, so… ?

I meant moving the code to a separate file and not calling it from Resolver.cs, except for possibly adding a DisjunctCaseRewriter to the rewriters list. Would that be possible?

In fact, in the long run, disjunctive patterns should be supported at any level of nesting, so the nice separation we have right now won't survive. But for now it's good to have the separated implementation.

I don't know the pattern matching transformations well enough to comment.

I meant moving the code to a separate file and not calling it from Resolver.cs, except for possibly adding a DisjunctCaseRewriter to the rewriters list. Would that be possible?

Possibly? I think it might work, because this pass doesn't use type information. The problem is that pattern matching compilation happens in the middle of resolution, and it uses some type info.

Also, do we have the architecture in place for writing such a pass? I need something that traverses all statements and expressions in a program. Do we have a visitor that does that?

Editing to add this following our conversation: it would be nice to add such a visitor, but one issue with rewriting this systematically would be that clients would lose access to the unresolved AST containing the full match structure.

keyboardDrummer · 2022-07-20T22:50:39Z

Source/Dafny/Resolver.cs

@@ -12501,6 +12494,48 @@ private class RBranchExpr : RBranch {
 }
 }

+ private ExtendedPattern RemoveDisjunctivePatterns(ExtendedPattern pat, bool allowVariables) {


The name only captures half of the behavior, so maybe replace Disjunctive with Illegal. And maybe replace Remove with Handle since you are both replacing patterns and emitting an error.

keyboardDrummer · 2022-07-20T22:54:41Z

Cool!

keyboardDrummer · 2022-07-20T22:56:33Z

Source/Dafny/Resolver.cs

+ case LitPattern:
+ return pat;
+ case IdPattern p:
+ if (p.Arguments == null && !p.Id.StartsWith("_") && !allowVariables) {


What is the check !p.Id.StartsWith("_") for?

Wildcards (_ patterns) are implemented as _-prefixed variables, and we don't want to complain about those.

From the documentation:

WildIdent = NoUSIdent | "_" Identifier, disallowing leading underscores, except the “wildcard” identifier _. When _ appears it is replaced by a unique generated identifier distinct from user identifiers. This wildcard has several uses in the language, but it is not used as part of expressions.

Shouldn't it be p.Id == "_" then?
If the point of a wildcard is to effectively not capture the variable, then why would we permit an identifier after the underscore?

Also, shouldn't there be a function Identifier.IsWildcard(p.id) to make this more explicit?

Also, is wildcard a good name? Hole seems more fitting.

Shouldn't it be p.Id == "_" then? If the point of a wildcard is to effectively not capture the variable, then why would we permit an identifier after the underscore?

No: internally, "_" is treated as a variable and gets renamed into a unique variable name starting with an underscore, so by the time we get here the holes are named something like _v64.

A future refactoring should probably just add a WildcardPattern (or HolePattern, indeed; I think it's a better fit)

Also, shouldn't there be a function Identifier.IsWildcard(p.id) to make this more explicit?

OK, I will do that. Even better, I can make it a property of the identifier pattern.

cpitclaudel · 2022-07-21T23:17:28Z

It turns out that I do need resolution information, and hence this transformation can't be implemented as a pre-resolve pass. The is the relevant case, for which I've added a test just now:

module Constants {
  const ONE := 1
  const TWO := 2

  method M(i: int) {
    match i
      case ONE | TWO => return; // `ONE` and `TWO` are not variables here
      case _ => // Not redundant
  }
}

…-patterns

cpitclaudel force-pushed the cpitclaudel_deep-or-patterns branch from d4ddfcb to de0ab09 Compare July 19, 2022 17:11

Merge branch 'master' into cpitclaudel_deep-or-patterns

17a5a68

keyboardDrummer reviewed Jul 20, 2022

View reviewed changes

cpitclaudel added 3 commits July 20, 2022 17:41

Rename dp and psep

2ef4189

Rename RemoveDisjunctivePatterns and clean up its implementation

53808c6

;

afb8718

cpitclaudel requested a review from keyboardDrummer July 21, 2022 00:44

cpitclaudel and others added 4 commits July 20, 2022 20:54

Merge branch 'master' into cpitclaudel_deep-or-patterns

ff2869c

Merge branch 'master' into cpitclaudel_deep-or-patterns

8973659

Refactor check for wildcard patterns

d326179

Merge branch 'master' into cpitclaudel_deep-or-patterns

46b34e3

keyboardDrummer previously approved these changes Jul 21, 2022

View reviewed changes

cpitclaudel enabled auto-merge (squash) July 21, 2022 21:06

Move release notes to Upcoming section

aa8d2b1

cpitclaudel dismissed keyboardDrummer’s stale review via aa8d2b1 July 21, 2022 21:09

Fix IsWildcardPattern test

d6f9242

Preserve ResolvedLit and add a test for that case

1c89a9d

cpitclaudel force-pushed the cpitclaudel_deep-or-patterns branch from 78d0e34 to 1c89a9d Compare July 22, 2022 00:29

cpitclaudel and others added 6 commits July 21, 2022 17:38

Merge remote-tracking branch 'origin/master' into cpitclaudel_deep-or…

cd7d728

…-patterns

Format

a0c4848

Preserve pattern type

b04bdf1

Merge branch 'master' into cpitclaudel_deep-or-patterns

48161bd

Fix test output

5dbd839

Don't clone the body of the matches (see #2334)

b39ac54

cpitclaudel disabled auto-merge July 22, 2022 07:04

cpitclaudel enabled auto-merge (squash) July 22, 2022 07:07

cpitclaudel requested a review from keyboardDrummer July 22, 2022 07:43

keyboardDrummer approved these changes Jul 22, 2022

View reviewed changes

Merge branch 'master' into cpitclaudel_deep-or-patterns

85bdb90

cpitclaudel merged commit a47f0c0 into master Jul 22, 2022

cpitclaudel deleted the cpitclaudel_deep-or-patterns branch July 22, 2022 14:13

stefan-aws mentioned this pull request Mar 27, 2023

Feature request: 'Or' patterns #1205

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

cpitclaudel commented Jul 19, 2022

keyboardDrummer Jul 20, 2022

cpitclaudel Jul 20, 2022

keyboardDrummer Jul 21, 2022 •

edited

Loading

keyboardDrummer Jul 20, 2022

cpitclaudel Jul 20, 2022 •

edited

Loading

keyboardDrummer Jul 21, 2022

cpitclaudel Jul 21, 2022

keyboardDrummer Jul 21, 2022

cpitclaudel Jul 22, 2022

keyboardDrummer Jul 20, 2022

cpitclaudel Jul 20, 2022 •

edited

Loading

keyboardDrummer Jul 21, 2022 •

edited

Loading

cpitclaudel Jul 21, 2022

keyboardDrummer Jul 21, 2022

cpitclaudel Jul 21, 2022

cpitclaudel Jul 22, 2022

keyboardDrummer Jul 20, 2022 •

edited

Loading

cpitclaudel Jul 20, 2022

keyboardDrummer commented Jul 20, 2022

keyboardDrummer Jul 20, 2022

cpitclaudel Jul 20, 2022

keyboardDrummer Jul 21, 2022 •

edited

Loading

cpitclaudel Jul 21, 2022

cpitclaudel Jul 21, 2022

cpitclaudel commented Jul 21, 2022

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

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

Conversation

cpitclaudel commented Jul 19, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Jul 21, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cpitclaudel Jul 20, 2022 • edited Loading

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

cpitclaudel Jul 20, 2022 • edited Loading

Choose a reason for hiding this comment

keyboardDrummer Jul 21, 2022 • edited Loading

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 Jul 20, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer commented Jul 20, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Jul 21, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cpitclaudel commented Jul 21, 2022

keyboardDrummer Jul 21, 2022 •

edited

Loading

cpitclaudel Jul 20, 2022 •

edited

Loading

cpitclaudel Jul 20, 2022 •

edited

Loading

keyboardDrummer Jul 21, 2022 •

edited

Loading

keyboardDrummer Jul 20, 2022 •

edited

Loading

keyboardDrummer Jul 21, 2022 •

edited

Loading