Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support or patterns in matches #2220

Closed
cpitclaudel opened this issue Jun 7, 2022 · 5 comments · Fixed by #2448
Closed

Support or patterns in matches #2220

cpitclaudel opened this issue Jun 7, 2022 · 5 comments · Fixed by #2448
Assignees
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking priority: not yet Will reconsider working on this when we're looking for work

Comments

@cpitclaudel
Copy link
Member

cpitclaudel commented Jun 7, 2022

Desired syntax:

datatype T = A(i: int) | B(j: int) | C(bool) | D

method Test(t: T) {
  match A
    case A(i) | B(i) => print i;
    case C(_) | D => print "";
}
@cpitclaudel cpitclaudel added kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking priority: not yet Will reconsider working on this when we're looking for work labels Jun 7, 2022
@MikaelMayer
Copy link
Member

How do you handle the second case, where it seems that you need a variable C(b) ? Would b be ignored then?

@cpitclaudel
Copy link
Member Author

It was a typo, good catch; thanks! I was hoping to use that case to demonstrate that you could use _ :/

@MikaelMayer
Copy link
Member

MikaelMayer commented Jun 10, 2022

What about:

datatype XT = X_AORB(i: int) | X_OTHER

method Test(t: T) {
  match AORB(t)
    case X_AORB(i) => print i;
    case X_OTHER => print "";
}

function method AORB(t: T): XT {
  if t.A? then X(t.i) else if t.B? then X(t.i) else X_OTHER
}

@cpitclaudel
Copy link
Member Author

There are a few problems with this alternative:

  • It's longer than the original code
  • It has a runtime cost.
  • It doesn't scale: you have to define a new datatype and a new function to project the original one for each new match that groups constructors differently.

When you have tens of constructors, it's not really viable to do it this way, I think (and even for this specific example, I find the or pattern a lot more readable)

@cpitclaudel cpitclaudel self-assigned this Jul 8, 2022
@cpitclaudel
Copy link
Member Author

cpitclaudel commented Jul 15, 2022

In the long term, we'd like to have support for fully general or-patterns, including or patterns nested inside constructors and or patterns including variables. Prior to doing this, we need to refactor the computation of pattern match decision trees, which currently is done during resolution.

For the first iteration of this feature, we'll support only top-level patterns with _, literals, and constructors — no variable bindings and no nested | patterns. Disallowing variables is the most important part, as it allows us to punt on tricky cases like the following:

datatype T = Nat(n: nat) | Int(i: int)

method M(t: T) {
  match t {
    case Nat(n) | Int(n) =>
      print n;
  }
}

method M'(t: T) {
  match t {
    case _ =>
      var n := if t.Nat? then t.n else t.i;
      print n;
  }
}

cpitclaudel added a commit that referenced this issue Jul 19, 2022
* `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.
cpitclaudel added a commit that referenced this issue Jul 22, 2022
feat: Add support for disjunctive (“or”) patterns

* `Source/Dafny/AST/DafnyAst.cs`
  (`DisjunctivePattern`): New subclass of `ExtendedPattern`.
  (`IsWildcardPattern`): New property.
* `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.
  (`RemoveIllegalSubpatterns`): 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.

Match bodies are not cloned because they are already resolved;
see #2334 for details.

Closes #2220.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking priority: not yet Will reconsider working on this when we're looking for work
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants