-
Notifications
You must be signed in to change notification settings - Fork 58
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
Side conditions in pattern matching #2804
Comments
lukaszcz
added
enhancement
New feature or request
syntax
pending-review
pattern-matching
labels
Jun 4, 2024
This came up when we were writing the logic function for the simple counter application: |
janmasrovira
added a commit
that referenced
this issue
Jul 3, 2024
…2852) - Syntax for #2804. -⚠️ Depends on #2869. This pr introduces: 1. front-end support (parsing, printing, typechecking) for boolean side conditions for branches of case expressions. 2. Now `if` is a reserved keyword. 3. Multiway `if` is allowed to have only the `else` branch. I've also refactored the parser to be simpler. Example: ``` multiCaseBr : Nat := case 1 of | zero | if 0 < 0 := 3 | else := 4 | suc (suc n) | if 0 < 0 := 3 | else := n | suc n if 0 < 0 := 3; ``` The side if branches must satisfy the following. 1. There must be at least one `if` branch. 4. The `else` branch is optional. If present, it must be the last. Future work: 1. Translate side if conditions to Core and extend the exhaustiveness algorithm. 5. Add side if conditions to function clauses.
lukaszcz
added a commit
that referenced
this issue
Sep 9, 2024
* Closes #2804 * Requires #3003 * Front-end syntax for side conditions was implemented in #2852. This PR implements compilation of side conditions. * Adds side-conditions to `Match` nodes in Core. Updates Core parsing, printing and the evaluator. * Only side-conditions without an `else` branch are allowed in Core. If there is an `else` branch, the side conditions are translated in `fromInternal` into nested ifs. Because with `else` the conditions are exhaustive, there are no implications for pattern exhaustiveness checking. * Adjusts the "wildcard row" case in the pattern matching compilation algorithm to take into account the side conditions.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Allow side conditions in pattern matches:
For example, allow to write
instead of
Syntax proposal:
The text was updated successfully, but these errors were encountered: