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

Side conditions in pattern matching #2804

Closed
lukaszcz opened this issue Jun 4, 2024 · 1 comment · Fixed by #2984
Closed

Side conditions in pattern matching #2804

lukaszcz opened this issue Jun 4, 2024 · 1 comment · Fixed by #2984
Assignees
Labels
Milestone

Comments

@lukaszcz
Copy link
Collaborator

lukaszcz commented Jun 4, 2024

Allow side conditions in pattern matches:

| pat1 pat2 pat3 if condition := body

For example, allow to write

case lst of
| [x] if F x := B1
| [x] := B2
| _ := B3

instead of

case lst of
| [x] := 
  if
    | F x := B1
    | else := B2
| _ := B3

Syntax proposal:

case lst of
| [x] 
     | if F x := A
     | if G x := B
     | else := C (else branch is optional)
| _ := D;
@paulcadman
Copy link
Collaborator

This came up when we were writing the logic function for the simple counter application:

https://github.com/anoma/juvix-anoma-stdlib/blob/dcbc80536eadc5bc9a8b45cba259a987339dd768/examples/RawCounterTransaction.juvix#L26

@paulcadman paulcadman added this to the 0.6.3 milestone Jun 17, 2024
@paulcadman paulcadman modified the milestones: 0.6.3, 0.6.4 Jul 2, 2024
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.
@paulcadman paulcadman modified the milestones: 0.6.4, 0.6.5 Jul 19, 2024
@paulcadman paulcadman modified the milestones: 0.6.5, 0.6.6 Aug 15, 2024
@lukaszcz lukaszcz modified the milestones: 0.6.6, 0.6.7 Sep 4, 2024
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
Labels
Projects
None yet
3 participants