2022-09-29 23:33:23 +03:00
|
|
|
# Basics
|
2024-07-10 17:46:18 +03:00
|
|
|
|
2023-07-19 20:45:05 +03:00
|
|
|
## non-exhaustive patterns
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
unique type T = A | B | C
|
|
|
|
|
|
|
|
test : T -> ()
|
|
|
|
test = cases
|
2023-02-27 19:31:41 +03:00
|
|
|
A -> ()
|
2022-09-29 23:33:23 +03:00
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-01 23:28:16 +03:00
|
|
|
Pattern match doesn't cover all possible cases:
|
2022-09-29 23:33:23 +03:00
|
|
|
4 | test = cases
|
2023-02-27 19:31:41 +03:00
|
|
|
5 | A -> ()
|
2022-09-29 23:33:23 +03:00
|
|
|
|
|
|
|
|
|
|
|
Patterns not matched:
|
|
|
|
|
|
|
|
* B
|
|
|
|
* C
|
|
|
|
|
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-03-02 18:04:36 +03:00
|
|
|
unique type T = A | B
|
|
|
|
|
|
|
|
test : (T, Optional T) -> ()
|
|
|
|
test = cases
|
|
|
|
(A, Some _) -> ()
|
|
|
|
(A, None) -> ()
|
|
|
|
(B, Some A) -> ()
|
|
|
|
(B, None) -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-03-02 18:04:36 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-02 18:04:36 +03:00
|
|
|
Pattern match doesn't cover all possible cases:
|
|
|
|
4 | test = cases
|
|
|
|
5 | (A, Some _) -> ()
|
|
|
|
6 | (A, None) -> ()
|
|
|
|
7 | (B, Some A) -> ()
|
|
|
|
8 | (B, None) -> ()
|
|
|
|
|
|
|
|
|
|
|
|
Patterns not matched:
|
|
|
|
* (B, Some B)
|
|
|
|
|
|
|
|
```
|
|
|
|
## redundant patterns
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
unique type T = A | B | C
|
|
|
|
|
|
|
|
test : T -> ()
|
|
|
|
test = cases
|
2023-02-27 19:31:41 +03:00
|
|
|
A -> ()
|
|
|
|
B -> ()
|
|
|
|
C -> ()
|
|
|
|
_ -> ()
|
2022-09-29 23:33:23 +03:00
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-01 23:28:16 +03:00
|
|
|
This case would be ignored because it's already covered by the preceding case(s):
|
2023-02-27 19:31:41 +03:00
|
|
|
8 | _ -> ()
|
2022-09-29 23:33:23 +03:00
|
|
|
|
|
|
|
|
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-03-02 18:04:36 +03:00
|
|
|
unique type T = A | B
|
|
|
|
|
|
|
|
test : (T, Optional T) -> ()
|
|
|
|
test = cases
|
|
|
|
(A, Some _) -> ()
|
|
|
|
(A, None) -> ()
|
|
|
|
(B, Some _) -> ()
|
|
|
|
(B, None) -> ()
|
|
|
|
(A, Some A) -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-03-02 18:04:36 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-02 18:04:36 +03:00
|
|
|
This case would be ignored because it's already covered by the preceding case(s):
|
|
|
|
9 | (A, Some A) -> ()
|
|
|
|
|
|
|
|
|
|
|
|
```
|
|
|
|
# Uninhabited patterns
|
|
|
|
|
|
|
|
match is complete without covering uninhabited patterns
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
unique type V =
|
|
|
|
|
|
|
|
test : Optional (Optional V) -> ()
|
|
|
|
test = cases
|
|
|
|
None -> ()
|
|
|
|
Some None -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2022-09-29 23:33:23 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
2024-01-04 11:42:12 +03:00
|
|
|
type V
|
2022-09-29 23:33:23 +03:00
|
|
|
test : Optional (Optional V) -> ()
|
|
|
|
|
|
|
|
```
|
2023-03-02 18:04:36 +03:00
|
|
|
uninhabited patterns are reported as redundant
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
unique type V =
|
|
|
|
|
2023-03-08 20:24:21 +03:00
|
|
|
test0 : V -> ()
|
|
|
|
test0 = cases
|
|
|
|
_ -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-03-08 20:24:21 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-08 20:25:09 +03:00
|
|
|
This case would be ignored because it's already covered by the preceding case(s):
|
|
|
|
5 | _ -> ()
|
2023-03-08 20:24:21 +03:00
|
|
|
|
|
|
|
|
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-03-08 20:24:21 +03:00
|
|
|
unique type V =
|
|
|
|
|
2022-09-29 23:33:23 +03:00
|
|
|
test : Optional (Optional V) -> ()
|
|
|
|
test = cases
|
|
|
|
None -> ()
|
|
|
|
Some None -> ()
|
|
|
|
Some _ -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-01 23:28:16 +03:00
|
|
|
This case would be ignored because it's already covered by the preceding case(s):
|
2022-09-29 23:33:23 +03:00
|
|
|
7 | Some _ -> ()
|
|
|
|
|
|
|
|
|
|
|
|
```
|
2023-03-02 18:04:36 +03:00
|
|
|
# Guards
|
|
|
|
|
|
|
|
## Incomplete patterns due to guards should be reported
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
test : () -> ()
|
|
|
|
test = cases
|
|
|
|
() | false -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-01 23:28:16 +03:00
|
|
|
Pattern match doesn't cover all possible cases:
|
2022-09-29 23:33:23 +03:00
|
|
|
2 | test = cases
|
|
|
|
3 | () | false -> ()
|
|
|
|
|
|
|
|
|
|
|
|
Patterns not matched:
|
|
|
|
* ()
|
|
|
|
|
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-03-02 18:04:36 +03:00
|
|
|
test : Optional Nat -> Nat
|
|
|
|
test = cases
|
|
|
|
None -> 0
|
|
|
|
Some x
|
|
|
|
| isEven x -> x
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-03-02 18:04:36 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-02 18:04:36 +03:00
|
|
|
Pattern match doesn't cover all possible cases:
|
|
|
|
2 | test = cases
|
|
|
|
3 | None -> 0
|
|
|
|
4 | Some x
|
|
|
|
5 | | isEven x -> x
|
|
|
|
|
|
|
|
|
|
|
|
Patterns not matched:
|
|
|
|
* Some _
|
|
|
|
|
|
|
|
```
|
|
|
|
## Complete patterns with guards should be accepted
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2023-03-02 18:04:36 +03:00
|
|
|
test : Optional Nat -> Nat
|
|
|
|
test = cases
|
|
|
|
None -> 0
|
|
|
|
Some x
|
|
|
|
| isEven x -> x
|
|
|
|
| otherwise -> 0
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-03-02 18:04:36 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-02 18:04:36 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
|
|
|
test : Optional Nat -> Nat
|
|
|
|
|
|
|
|
```
|
|
|
|
# Pattern instantiation depth
|
|
|
|
|
|
|
|
Uncovered patterns are only instantiated as deeply as necessary to
|
|
|
|
distinguish them from existing patterns.
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
unique type T = A | B | C
|
|
|
|
|
|
|
|
test : Optional (Optional T) -> ()
|
|
|
|
test = cases
|
|
|
|
None -> ()
|
|
|
|
Some None -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-01 23:28:16 +03:00
|
|
|
Pattern match doesn't cover all possible cases:
|
2022-09-29 23:33:23 +03:00
|
|
|
4 | test = cases
|
|
|
|
5 | None -> ()
|
|
|
|
6 | Some None -> ()
|
|
|
|
|
|
|
|
|
|
|
|
Patterns not matched:
|
|
|
|
* Some (Some _)
|
|
|
|
|
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
unique type T = A | B | C
|
|
|
|
|
|
|
|
test : Optional (Optional T) -> ()
|
|
|
|
test = cases
|
|
|
|
None -> ()
|
|
|
|
Some None -> ()
|
|
|
|
Some (Some A) -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-01 23:28:16 +03:00
|
|
|
Pattern match doesn't cover all possible cases:
|
2022-09-29 23:33:23 +03:00
|
|
|
4 | test = cases
|
|
|
|
5 | None -> ()
|
|
|
|
6 | Some None -> ()
|
|
|
|
7 | Some (Some A) -> ()
|
|
|
|
|
|
|
|
|
|
|
|
Patterns not matched:
|
|
|
|
|
|
|
|
* Some (Some B)
|
|
|
|
* Some (Some C)
|
|
|
|
|
|
|
|
```
|
|
|
|
# Literals
|
2023-03-02 18:04:36 +03:00
|
|
|
|
|
|
|
## Non-exhaustive
|
|
|
|
|
|
|
|
Nat
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
test : Nat -> ()
|
|
|
|
test = cases
|
|
|
|
0 -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-01 23:28:16 +03:00
|
|
|
Pattern match doesn't cover all possible cases:
|
2022-09-29 23:33:23 +03:00
|
|
|
2 | test = cases
|
|
|
|
3 | 0 -> ()
|
|
|
|
|
|
|
|
|
|
|
|
Patterns not matched:
|
|
|
|
* _
|
|
|
|
|
|
|
|
```
|
2023-03-02 18:04:36 +03:00
|
|
|
Boolean
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2023-03-02 18:04:36 +03:00
|
|
|
test : Boolean -> ()
|
|
|
|
test = cases
|
|
|
|
true -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-03-02 18:04:36 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-02 18:04:36 +03:00
|
|
|
Pattern match doesn't cover all possible cases:
|
|
|
|
2 | test = cases
|
|
|
|
3 | true -> ()
|
|
|
|
|
|
|
|
|
|
|
|
Patterns not matched:
|
|
|
|
* false
|
|
|
|
|
|
|
|
```
|
|
|
|
## Exhaustive
|
|
|
|
|
|
|
|
Nat
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
test : Nat -> ()
|
|
|
|
test = cases
|
|
|
|
0 -> ()
|
|
|
|
_ -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2022-09-29 23:33:23 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
|
|
|
test : Nat -> ()
|
|
|
|
|
|
|
|
```
|
2023-03-02 18:04:36 +03:00
|
|
|
Boolean
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
test : Boolean -> ()
|
|
|
|
test = cases
|
|
|
|
true -> ()
|
2023-03-02 18:04:36 +03:00
|
|
|
false -> ()
|
2022-09-29 23:33:23 +03:00
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-02 18:04:36 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-03-02 18:04:36 +03:00
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
|
|
|
test : Boolean -> ()
|
2022-09-29 23:33:23 +03:00
|
|
|
|
|
|
|
```
|
2023-03-02 18:04:36 +03:00
|
|
|
# Redundant
|
|
|
|
|
|
|
|
Nat
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2023-03-02 18:04:36 +03:00
|
|
|
test : Nat -> ()
|
2022-09-29 23:33:23 +03:00
|
|
|
test = cases
|
2023-03-02 18:04:36 +03:00
|
|
|
0 -> ()
|
|
|
|
0 -> ()
|
|
|
|
_ -> ()
|
2022-09-29 23:33:23 +03:00
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-02 18:04:36 +03:00
|
|
|
This case would be ignored because it's already covered by the preceding case(s):
|
|
|
|
4 | 0 -> ()
|
2022-09-29 23:33:23 +03:00
|
|
|
|
|
|
|
|
|
|
|
```
|
2023-03-02 18:04:36 +03:00
|
|
|
Boolean
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
test : Boolean -> ()
|
|
|
|
test = cases
|
|
|
|
true -> ()
|
|
|
|
false -> ()
|
|
|
|
_ -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-01 23:28:16 +03:00
|
|
|
This case would be ignored because it's already covered by the preceding case(s):
|
2022-09-29 23:33:23 +03:00
|
|
|
5 | _ -> ()
|
|
|
|
|
|
|
|
|
|
|
|
```
|
|
|
|
# Sequences
|
2023-03-02 18:04:36 +03:00
|
|
|
|
|
|
|
## Exhaustive
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
test : [()] -> ()
|
|
|
|
test = cases
|
|
|
|
[] -> ()
|
|
|
|
x +: xs -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2022-09-29 23:33:23 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
|
|
|
test : [()] -> ()
|
|
|
|
|
|
|
|
```
|
2023-03-02 18:04:36 +03:00
|
|
|
## Non-exhaustive
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
test : [()] -> ()
|
|
|
|
test = cases
|
|
|
|
[] -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-01 23:28:16 +03:00
|
|
|
Pattern match doesn't cover all possible cases:
|
2022-09-29 23:33:23 +03:00
|
|
|
2 | test = cases
|
|
|
|
3 | [] -> ()
|
|
|
|
|
|
|
|
|
|
|
|
Patterns not matched:
|
2023-03-02 18:04:36 +03:00
|
|
|
* (() +: _)
|
2022-09-29 23:33:23 +03:00
|
|
|
|
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
test : [()] -> ()
|
|
|
|
test = cases
|
|
|
|
x +: xs -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-01 23:28:16 +03:00
|
|
|
Pattern match doesn't cover all possible cases:
|
2022-09-29 23:33:23 +03:00
|
|
|
2 | test = cases
|
|
|
|
3 | x +: xs -> ()
|
|
|
|
|
|
|
|
|
|
|
|
Patterns not matched:
|
|
|
|
* []
|
|
|
|
|
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
test : [()] -> ()
|
|
|
|
test = cases
|
|
|
|
xs :+ x -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-01 23:28:16 +03:00
|
|
|
Pattern match doesn't cover all possible cases:
|
2022-09-29 23:33:23 +03:00
|
|
|
2 | test = cases
|
|
|
|
3 | xs :+ x -> ()
|
|
|
|
|
|
|
|
|
|
|
|
Patterns not matched:
|
|
|
|
* []
|
|
|
|
|
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
test : [()] -> ()
|
|
|
|
test = cases
|
|
|
|
x0 +: (x1 +: xs) -> ()
|
|
|
|
[] -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-01 23:28:16 +03:00
|
|
|
Pattern match doesn't cover all possible cases:
|
2022-09-29 23:33:23 +03:00
|
|
|
2 | test = cases
|
|
|
|
3 | x0 +: (x1 +: xs) -> ()
|
|
|
|
4 | [] -> ()
|
|
|
|
|
|
|
|
|
|
|
|
Patterns not matched:
|
2023-03-02 18:04:36 +03:00
|
|
|
* (() +: [])
|
2022-09-29 23:33:23 +03:00
|
|
|
|
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
test : [()] -> ()
|
|
|
|
test = cases
|
|
|
|
[] -> ()
|
|
|
|
x0 +: [] -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-01 23:28:16 +03:00
|
|
|
Pattern match doesn't cover all possible cases:
|
2022-09-29 23:33:23 +03:00
|
|
|
2 | test = cases
|
|
|
|
3 | [] -> ()
|
|
|
|
4 | x0 +: [] -> ()
|
|
|
|
|
|
|
|
|
|
|
|
Patterns not matched:
|
2023-03-02 18:04:36 +03:00
|
|
|
* (() +: (() +: _))
|
|
|
|
|
|
|
|
```
|
|
|
|
## Uninhabited
|
|
|
|
|
|
|
|
`Cons` is not expected since `V` is uninhabited
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2023-03-02 18:04:36 +03:00
|
|
|
unique type V =
|
|
|
|
|
|
|
|
test : [V] -> ()
|
|
|
|
test = cases
|
|
|
|
[] -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-03-02 18:04:36 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-02 18:04:36 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
2024-01-04 11:42:12 +03:00
|
|
|
type V
|
2023-03-02 18:04:36 +03:00
|
|
|
test : [V] -> ()
|
2022-09-29 23:33:23 +03:00
|
|
|
|
|
|
|
```
|
2023-03-02 18:04:36 +03:00
|
|
|
## Length restrictions can equate cons and nil patterns
|
|
|
|
|
|
|
|
Here the first pattern matches lists of length two or greater, the
|
|
|
|
second pattern matches lists of length 0. The third case matches when the
|
|
|
|
final element is `false`, while the fourth pattern matches when the
|
|
|
|
first element is `true`. However, the only possible list length at
|
|
|
|
the third or fourth clause is 1, so the first and final element must
|
|
|
|
be equal. Thus, the pattern match is exhaustive.
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
test : [Boolean] -> ()
|
|
|
|
test = cases
|
|
|
|
[a, b] ++ xs -> ()
|
|
|
|
[] -> ()
|
|
|
|
xs :+ false -> ()
|
|
|
|
true +: xs -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2022-09-29 23:33:23 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
|
|
|
test : [Boolean] -> ()
|
|
|
|
|
|
|
|
```
|
2023-03-02 18:04:36 +03:00
|
|
|
This is the same idea as above but shows that fourth match is redundant.
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
test : [Boolean] -> ()
|
|
|
|
test = cases
|
|
|
|
[a, b] ++ xs -> ()
|
|
|
|
[] -> ()
|
|
|
|
xs :+ true -> ()
|
|
|
|
true +: xs -> ()
|
|
|
|
_ -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-01 23:28:16 +03:00
|
|
|
This case would be ignored because it's already covered by the preceding case(s):
|
2022-09-29 23:33:23 +03:00
|
|
|
6 | true +: xs -> ()
|
|
|
|
|
|
|
|
|
|
|
|
```
|
2023-03-02 18:04:36 +03:00
|
|
|
This is another similar example. The first pattern matches lists of
|
|
|
|
length 5 or greater. The second matches lists of length 4 or greater where the
|
|
|
|
first and third element are true. The third matches lists of length 4
|
2023-07-19 20:45:05 +03:00
|
|
|
or greater where the final 4 elements are `true, false, true, false`.
|
2023-03-02 18:04:36 +03:00
|
|
|
The list must be exactly of length 4 to arrive at the second or third
|
|
|
|
clause, so the third pattern is redundant.
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2022-09-29 23:33:23 +03:00
|
|
|
test : [Boolean] -> ()
|
|
|
|
test = cases
|
|
|
|
[a, b, c, d, f] ++ xs -> ()
|
|
|
|
[true, _, true, _] ++ _ -> ()
|
|
|
|
_ ++ [true, false, true, false] -> ()
|
|
|
|
_ -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2022-09-29 23:33:23 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-01 23:28:16 +03:00
|
|
|
This case would be ignored because it's already covered by the preceding case(s):
|
2022-09-29 23:33:23 +03:00
|
|
|
5 | _ ++ [true, false, true, false] -> ()
|
|
|
|
|
|
|
|
|
|
|
|
```
|
2023-03-08 18:53:46 +03:00
|
|
|
# bugfix: Sufficient data decl map
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-03-08 18:53:46 +03:00
|
|
|
unique type T = A
|
|
|
|
|
|
|
|
unit2t : Unit -> T
|
|
|
|
unit2t = cases
|
|
|
|
() -> A
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-03-08 18:53:46 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-08 18:53:46 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
2024-01-04 11:42:12 +03:00
|
|
|
type T
|
2023-03-08 18:53:46 +03:00
|
|
|
unit2t : 'T
|
|
|
|
|
|
|
|
```
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> add
|
2023-03-08 18:53:46 +03:00
|
|
|
|
|
|
|
⍟ I've added these definitions:
|
|
|
|
|
2024-01-04 11:42:12 +03:00
|
|
|
type T
|
2023-03-08 18:53:46 +03:00
|
|
|
unit2t : 'T
|
|
|
|
|
|
|
|
```
|
2023-07-19 20:45:05 +03:00
|
|
|
Pattern coverage checking needs the data decl map to contain all
|
|
|
|
transitive type dependencies of the scrutinee type. We do this
|
2023-03-08 18:53:46 +03:00
|
|
|
before typechecking begins in a roundabout way: fetching all
|
|
|
|
transitive type dependencies of references that appear in the expression.
|
|
|
|
|
|
|
|
This test ensures that we have fetched the `T` type although there is
|
|
|
|
no data decl reference to `T` in `witht`.
|
2024-07-10 17:46:18 +03:00
|
|
|
|
|
|
|
``` unison
|
2023-03-08 18:53:46 +03:00
|
|
|
witht : Unit
|
|
|
|
witht = match unit2t () with
|
|
|
|
x -> ()
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-03-08 18:53:46 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-08 18:44:03 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
|
|
|
witht : ()
|
|
|
|
|
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-03-08 18:44:03 +03:00
|
|
|
unique type V =
|
2023-03-08 18:53:46 +03:00
|
|
|
|
2023-03-08 18:44:03 +03:00
|
|
|
evil : Unit -> V
|
|
|
|
evil = bug ""
|
2023-03-08 18:53:46 +03:00
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-03-08 18:44:03 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-08 18:44:03 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
2024-01-04 11:42:12 +03:00
|
|
|
type V
|
2023-03-08 18:44:03 +03:00
|
|
|
evil : 'V
|
2023-03-08 18:53:46 +03:00
|
|
|
|
2023-03-08 18:44:03 +03:00
|
|
|
```
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> add
|
2023-03-08 18:53:46 +03:00
|
|
|
|
2023-03-08 18:44:03 +03:00
|
|
|
⍟ I've added these definitions:
|
|
|
|
|
2024-01-04 11:42:12 +03:00
|
|
|
type V
|
2023-03-08 18:44:03 +03:00
|
|
|
evil : 'V
|
2023-03-08 18:53:46 +03:00
|
|
|
|
2023-03-08 18:44:03 +03:00
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-03-08 18:44:03 +03:00
|
|
|
withV : Unit
|
|
|
|
withV = match evil () with
|
|
|
|
x -> ()
|
|
|
|
```
|
2023-03-08 18:53:46 +03:00
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-03-08 18:53:46 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-08 18:44:03 +03:00
|
|
|
This case would be ignored because it's already covered by the preceding case(s):
|
|
|
|
3 | x -> ()
|
|
|
|
|
2023-03-08 18:53:46 +03:00
|
|
|
|
2023-03-08 18:44:03 +03:00
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-03-13 21:11:39 +03:00
|
|
|
unique type SomeType = A
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-03-13 21:11:39 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-13 21:11:39 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
2024-01-04 11:42:12 +03:00
|
|
|
type SomeType
|
2023-03-13 21:11:39 +03:00
|
|
|
|
|
|
|
```
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> add
|
2023-03-13 21:11:39 +03:00
|
|
|
|
|
|
|
⍟ I've added these definitions:
|
|
|
|
|
2024-01-04 11:42:12 +03:00
|
|
|
type SomeType
|
2023-03-13 21:11:39 +03:00
|
|
|
|
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-03-13 21:11:39 +03:00
|
|
|
unique type R = R SomeType
|
|
|
|
|
|
|
|
get x = match x with
|
|
|
|
R y -> y
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-03-13 21:11:39 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-13 21:17:04 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
2024-01-04 11:42:12 +03:00
|
|
|
type R
|
2023-03-13 21:17:04 +03:00
|
|
|
get : R -> SomeType
|
2023-03-13 21:11:39 +03:00
|
|
|
|
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-03-13 21:17:04 +03:00
|
|
|
unique type R = { someType : SomeType }
|
|
|
|
```
|
2023-03-13 21:11:39 +03:00
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-03-13 21:11:39 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-03-13 21:17:04 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
2024-01-04 11:42:12 +03:00
|
|
|
type R
|
2023-03-13 21:17:04 +03:00
|
|
|
R.someType : R -> SomeType
|
|
|
|
R.someType.modify : (SomeType ->{g} SomeType) -> R ->{g} R
|
|
|
|
R.someType.set : SomeType -> R -> R
|
2023-03-13 21:11:39 +03:00
|
|
|
|
2023-03-13 21:17:04 +03:00
|
|
|
```
|
2023-04-13 22:17:39 +03:00
|
|
|
# Ability handlers
|
|
|
|
|
|
|
|
## Exhaustive ability handlers are accepted
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-04-13 22:17:39 +03:00
|
|
|
structural ability Abort where
|
|
|
|
abort : {Abort} a
|
|
|
|
|
|
|
|
|
|
|
|
result : '{e, Abort} a -> {e} a
|
|
|
|
result f = handle !f with cases
|
|
|
|
{ x } -> x
|
|
|
|
{ abort -> _ } -> bug "aborted"
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-13 22:17:39 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-04-13 22:17:39 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
|
|
|
structural ability Abort
|
|
|
|
result : '{e, Abort} a ->{e} a
|
|
|
|
|
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-04-13 22:17:39 +03:00
|
|
|
structural ability Abort where
|
|
|
|
abort : {Abort} a
|
|
|
|
|
|
|
|
unique type T = A | B
|
|
|
|
|
|
|
|
result : '{e, Abort} T -> {e} ()
|
|
|
|
result f = handle !f with cases
|
2024-08-26 20:37:19 +03:00
|
|
|
{ T.A } -> ()
|
2023-04-13 22:17:39 +03:00
|
|
|
{ B } -> ()
|
|
|
|
{ abort -> _ } -> bug "aborted"
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-13 22:17:39 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-04-13 22:17:39 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
|
|
|
structural ability Abort
|
|
|
|
result : '{e, Abort} T ->{e} ()
|
|
|
|
|
|
|
|
⍟ These names already exist. You can `update` them to your
|
|
|
|
new definition:
|
|
|
|
|
2024-01-04 11:42:12 +03:00
|
|
|
type T
|
2023-04-13 22:17:39 +03:00
|
|
|
|
2023-04-14 23:50:14 +03:00
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-04-14 23:50:14 +03:00
|
|
|
structural ability Abort where
|
|
|
|
abort : {Abort} a
|
|
|
|
|
|
|
|
result : '{e, Abort} V -> {e} V
|
2023-07-19 20:45:05 +03:00
|
|
|
result f =
|
2023-04-14 23:50:14 +03:00
|
|
|
impl : Request {Abort} V -> V
|
|
|
|
impl = cases
|
|
|
|
{ abort -> _ } -> bug "aborted"
|
|
|
|
handle !f with impl
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-14 23:50:14 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-04-14 23:50:14 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
|
|
|
structural ability Abort
|
|
|
|
result : '{e, Abort} V ->{e} V
|
|
|
|
|
2023-04-18 16:17:34 +03:00
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-04-18 16:17:34 +03:00
|
|
|
structural ability Abort where
|
|
|
|
abort : {Abort} a
|
2023-07-19 20:45:05 +03:00
|
|
|
|
2023-04-18 16:17:34 +03:00
|
|
|
structural ability Stream a where
|
|
|
|
emit : a -> {Stream a} Unit
|
2023-07-19 20:45:05 +03:00
|
|
|
|
2023-04-18 16:17:34 +03:00
|
|
|
handleMulti : '{Stream a, Abort} r -> (Optional r, [a])
|
|
|
|
handleMulti c =
|
|
|
|
impl xs = cases
|
|
|
|
{ r } -> (Some r, xs)
|
|
|
|
{ emit x -> resume } -> handle !resume with impl (xs :+ x)
|
|
|
|
{ abort -> _ } -> (None, xs)
|
|
|
|
handle !c with impl []
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-18 16:17:34 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-04-18 16:17:34 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
|
|
|
structural ability Abort
|
|
|
|
structural ability Stream a
|
|
|
|
handleMulti : '{Abort, Stream a} r -> (Optional r, [a])
|
|
|
|
|
2023-04-13 22:17:39 +03:00
|
|
|
```
|
|
|
|
## Non-exhaustive ability handlers are rejected
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-04-13 22:17:39 +03:00
|
|
|
structural ability Abort where
|
|
|
|
abort : {Abort} a
|
|
|
|
abortWithMessage : Text -> {Abort} a
|
|
|
|
|
|
|
|
|
|
|
|
result : '{e, Abort} a -> {e} a
|
|
|
|
result f = handle !f with cases
|
|
|
|
{ abort -> _ } -> bug "aborted"
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-13 22:17:39 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-04-13 22:17:39 +03:00
|
|
|
Pattern match doesn't cover all possible cases:
|
|
|
|
7 | result f = handle !f with cases
|
|
|
|
8 | { abort -> _ } -> bug "aborted"
|
|
|
|
|
|
|
|
|
|
|
|
Patterns not matched:
|
|
|
|
|
|
|
|
* { _ }
|
2023-07-21 09:12:22 +03:00
|
|
|
* { abortWithMessage _ -> _ }
|
2023-04-13 22:17:39 +03:00
|
|
|
|
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-04-13 22:17:39 +03:00
|
|
|
structural ability Abort where
|
|
|
|
abort : {Abort} a
|
|
|
|
|
|
|
|
unique type T = A | B
|
|
|
|
|
|
|
|
result : '{e, Abort} T -> {e} ()
|
|
|
|
result f = handle !f with cases
|
2024-08-26 20:37:19 +03:00
|
|
|
{ T.A } -> ()
|
2023-04-13 22:17:39 +03:00
|
|
|
{ abort -> _ } -> bug "aborted"
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-13 22:17:39 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-04-13 22:17:39 +03:00
|
|
|
Pattern match doesn't cover all possible cases:
|
|
|
|
7 | result f = handle !f with cases
|
2024-08-26 20:37:19 +03:00
|
|
|
8 | { T.A } -> ()
|
2023-04-13 22:17:39 +03:00
|
|
|
9 | { abort -> _ } -> bug "aborted"
|
|
|
|
|
|
|
|
|
|
|
|
Patterns not matched:
|
|
|
|
* { B }
|
|
|
|
|
2023-04-14 04:27:31 +03:00
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-04-14 04:27:31 +03:00
|
|
|
unique ability Give a where
|
|
|
|
give : a -> {Give a} Unit
|
|
|
|
|
|
|
|
unique type T = A | B
|
|
|
|
|
|
|
|
result : '{e, Give T} r -> {e} r
|
|
|
|
result f = handle !f with cases
|
|
|
|
{ x } -> x
|
2024-08-28 02:29:29 +03:00
|
|
|
{ give T.A -> resume } -> result resume
|
2023-04-14 04:27:31 +03:00
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-14 04:27:31 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-04-14 21:59:31 +03:00
|
|
|
Pattern match doesn't cover all possible cases:
|
|
|
|
7 | result f = handle !f with cases
|
|
|
|
8 | { x } -> x
|
2024-08-28 02:29:29 +03:00
|
|
|
9 | { give T.A -> resume } -> result resume
|
2023-04-14 04:27:31 +03:00
|
|
|
|
2023-04-14 21:59:31 +03:00
|
|
|
|
|
|
|
Patterns not matched:
|
2023-07-21 09:12:22 +03:00
|
|
|
* { give B -> _ }
|
2023-04-14 04:27:31 +03:00
|
|
|
|
2023-04-18 16:17:34 +03:00
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-04-18 16:17:34 +03:00
|
|
|
structural ability Abort where
|
|
|
|
abort : {Abort} a
|
2023-07-19 20:45:05 +03:00
|
|
|
|
2023-04-18 16:17:34 +03:00
|
|
|
structural ability Stream a where
|
|
|
|
emit : a -> {Stream a} Unit
|
2023-07-19 20:45:05 +03:00
|
|
|
|
2023-04-18 16:17:34 +03:00
|
|
|
handleMulti : '{Stream a, Abort} r -> (Optional r, [a])
|
|
|
|
handleMulti c =
|
|
|
|
impl : [a] -> Request {Stream a, Abort} r -> (Optional r, [a])
|
|
|
|
impl xs = cases
|
|
|
|
{ r } -> (Some r, xs)
|
|
|
|
{ emit x -> resume } -> handle !resume with impl (xs :+ x)
|
|
|
|
handle !c with impl []
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-18 16:17:34 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-04-18 16:17:34 +03:00
|
|
|
Pattern match doesn't cover all possible cases:
|
|
|
|
10 | impl xs = cases
|
|
|
|
11 | { r } -> (Some r, xs)
|
|
|
|
12 | { emit x -> resume } -> handle !resume with impl (xs :+ x)
|
|
|
|
|
|
|
|
|
|
|
|
Patterns not matched:
|
2023-07-21 09:12:22 +03:00
|
|
|
* { abort -> _ }
|
2023-04-18 16:17:34 +03:00
|
|
|
|
2023-04-14 04:27:31 +03:00
|
|
|
```
|
2023-04-14 21:59:31 +03:00
|
|
|
## Redundant handler cases are rejected
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-04-14 04:27:31 +03:00
|
|
|
unique ability Give a where
|
|
|
|
give : a -> {Give a} Unit
|
|
|
|
|
2023-04-14 21:59:31 +03:00
|
|
|
unique type T = A | B
|
2023-04-14 04:27:31 +03:00
|
|
|
|
2023-04-14 21:59:31 +03:00
|
|
|
result : '{e, Give T} r -> {e} r
|
2023-04-14 04:27:31 +03:00
|
|
|
result f = handle !f with cases
|
|
|
|
{ x } -> x
|
|
|
|
{ give _ -> resume } -> result resume
|
2024-08-29 21:12:25 +03:00
|
|
|
{ give T.A -> resume } -> result resume
|
2023-04-14 04:27:31 +03:00
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-14 04:27:31 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2024-08-29 21:12:25 +03:00
|
|
|
This case would be ignored because it's already covered by the preceding case(s):
|
|
|
|
10 | { give T.A -> resume } -> result resume
|
2024-08-29 21:07:17 +03:00
|
|
|
|
2023-04-14 04:27:31 +03:00
|
|
|
|
2023-04-13 22:17:39 +03:00
|
|
|
```
|
|
|
|
## Exhaustive ability reinterpretations are accepted
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-04-13 22:17:39 +03:00
|
|
|
structural ability Abort where
|
|
|
|
abort : {Abort} a
|
|
|
|
abortWithMessage : Text -> {Abort} a
|
|
|
|
|
|
|
|
|
|
|
|
result : '{e, Abort} a -> {e, Abort} a
|
|
|
|
result f = handle !f with cases
|
|
|
|
{ x } -> x
|
|
|
|
{ abort -> _ } -> abort
|
|
|
|
{ abortWithMessage msg -> _ } -> abortWithMessage ("aborting: " ++ msg)
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-13 22:17:39 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-04-13 22:17:39 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
|
|
|
structural ability Abort
|
|
|
|
result : '{e, Abort} a ->{e, Abort} a
|
|
|
|
|
2023-04-14 21:59:31 +03:00
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-04-14 21:59:31 +03:00
|
|
|
structural ability Abort a where
|
|
|
|
abort : {Abort a} r
|
|
|
|
abortWithMessage : a -> {Abort a} r
|
|
|
|
|
|
|
|
result : '{e, Abort V} a -> {e, Abort V} a
|
2023-07-19 20:45:05 +03:00
|
|
|
result f =
|
2023-04-14 21:59:31 +03:00
|
|
|
impl : Request {Abort V} r -> {Abort V} r
|
|
|
|
impl = cases
|
|
|
|
{ x } -> x
|
|
|
|
{ abort -> _ } -> abort
|
|
|
|
handle !f with impl
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-14 21:59:31 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-04-14 21:59:31 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
|
|
|
structural ability Abort a
|
|
|
|
result : '{e, Abort V} a ->{e, Abort V} a
|
|
|
|
|
2023-04-13 22:17:39 +03:00
|
|
|
```
|
|
|
|
## Non-exhaustive ability reinterpretations are rejected
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-04-13 22:17:39 +03:00
|
|
|
structural ability Abort where
|
|
|
|
abort : {Abort} a
|
|
|
|
abortWithMessage : Text -> {Abort} a
|
|
|
|
|
|
|
|
|
|
|
|
result : '{e, Abort} a -> {e, Abort} a
|
|
|
|
result f = handle !f with cases
|
|
|
|
{ x } -> x
|
|
|
|
{ abortWithMessage msg -> _ } -> abortWithMessage ("aborting: " ++ msg)
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-13 22:17:39 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-04-13 22:17:39 +03:00
|
|
|
Pattern match doesn't cover all possible cases:
|
|
|
|
7 | result f = handle !f with cases
|
|
|
|
8 | { x } -> x
|
|
|
|
9 | { abortWithMessage msg -> _ } -> abortWithMessage ("aborting: " ++ msg)
|
|
|
|
|
|
|
|
|
|
|
|
Patterns not matched:
|
2023-07-21 09:12:22 +03:00
|
|
|
* { abort -> _ }
|
2023-04-13 22:17:39 +03:00
|
|
|
|
|
|
|
```
|
2023-04-14 21:59:31 +03:00
|
|
|
## Hacky workaround for uninhabited abilities
|
|
|
|
|
|
|
|
Although all of the constructors of an ability might be uninhabited,
|
|
|
|
the typechecker requires at least one be specified so that it can
|
|
|
|
determine that the ability should be discharged. So, the default
|
|
|
|
pattern match coverage checking behavior of prohibiting covering any
|
|
|
|
of the cases is problematic. Instead, the pattern match coverage
|
|
|
|
checker will require that at least one constructor be given, even if
|
|
|
|
they are all uninhabited.
|
|
|
|
|
|
|
|
The messages here aren't the best, but I don't think uninhabited
|
|
|
|
abilities will come up and get handlers written for them often.
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-04-14 21:59:31 +03:00
|
|
|
unique ability Give a where
|
|
|
|
give : a -> {Give a} Unit
|
|
|
|
give2 : a -> {Give a} Unit
|
|
|
|
|
|
|
|
result : '{e, Give V} r -> {e} r
|
2023-07-19 20:45:05 +03:00
|
|
|
result f =
|
2023-04-14 21:59:31 +03:00
|
|
|
impl : Request {Give V} r -> {} r
|
|
|
|
impl = cases
|
|
|
|
{ x } -> x
|
|
|
|
handle !f with impl
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-14 21:59:31 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-04-14 21:59:31 +03:00
|
|
|
Pattern match doesn't cover all possible cases:
|
2023-07-19 20:45:05 +03:00
|
|
|
8 | impl = cases
|
|
|
|
9 | { x } -> x
|
2023-04-14 21:59:31 +03:00
|
|
|
|
|
|
|
|
|
|
|
Patterns not matched:
|
|
|
|
|
2023-07-21 09:12:22 +03:00
|
|
|
* { give _ -> _ }
|
|
|
|
* { give2 _ -> _ }
|
2023-04-14 21:59:31 +03:00
|
|
|
|
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-04-14 21:59:31 +03:00
|
|
|
unique ability Give a where
|
|
|
|
give : a -> {Give a} Unit
|
|
|
|
give2 : a -> {Give a} Unit
|
|
|
|
|
|
|
|
result : '{e, Give V} r -> {e} r
|
2023-07-19 20:45:05 +03:00
|
|
|
result f =
|
2023-04-14 21:59:31 +03:00
|
|
|
impl : Request {Give V} r -> {} r
|
|
|
|
impl = cases
|
|
|
|
{ x } -> x
|
|
|
|
{ give _ -> resume } -> bug "impossible"
|
|
|
|
handle !f with impl
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-14 21:59:31 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-04-14 21:59:31 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
2024-01-04 11:42:12 +03:00
|
|
|
ability Give a
|
2023-04-14 21:59:31 +03:00
|
|
|
result : '{e, Give V} r ->{e} r
|
|
|
|
|
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-04-14 21:59:31 +03:00
|
|
|
unique ability Give a where
|
|
|
|
give : a -> {Give a} Unit
|
|
|
|
give2 : a -> {Give a} Unit
|
|
|
|
|
|
|
|
result : '{e, Give V} r -> {e} r
|
2023-07-19 20:45:05 +03:00
|
|
|
result f =
|
2023-04-14 21:59:31 +03:00
|
|
|
impl : Request {Give V} r -> {} r
|
|
|
|
impl = cases
|
|
|
|
{ x } -> x
|
|
|
|
{ give2 _ -> resume } -> bug "impossible"
|
|
|
|
handle !f with impl
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-14 21:59:31 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-04-14 21:59:31 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
2024-01-04 11:42:12 +03:00
|
|
|
ability Give a
|
2023-04-14 21:59:31 +03:00
|
|
|
result : '{e, Give V} r ->{e} r
|
|
|
|
|
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-04-14 21:59:31 +03:00
|
|
|
unique ability Give a where
|
|
|
|
give : a -> {Give a} Unit
|
|
|
|
give2 : a -> {Give a} Unit
|
|
|
|
|
|
|
|
result : '{e, Give V} r -> {e} r
|
2023-07-19 20:45:05 +03:00
|
|
|
result f =
|
2023-04-14 21:59:31 +03:00
|
|
|
impl : Request {Give V} r -> {} r
|
|
|
|
impl = cases
|
|
|
|
{ x } -> x
|
|
|
|
{ give _ -> resume } -> bug "impossible"
|
|
|
|
{ give2 _ -> resume } -> bug "impossible"
|
|
|
|
handle !f with impl
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-14 21:59:31 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-04-14 21:59:31 +03:00
|
|
|
This case would be ignored because it's already covered by the preceding case(s):
|
2023-07-19 20:45:05 +03:00
|
|
|
11 | { give2 _ -> resume } -> bug "impossible"
|
2023-04-14 21:59:31 +03:00
|
|
|
|
|
|
|
|
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-04-14 21:59:31 +03:00
|
|
|
unique ability GiveA a where
|
|
|
|
giveA : a -> {GiveA a} Unit
|
|
|
|
giveA2 : a -> {GiveA a} Unit
|
|
|
|
|
|
|
|
unique ability GiveB a where
|
|
|
|
giveB : a -> {GiveB a} Unit
|
|
|
|
giveB2 : a -> {GiveB a} Unit
|
|
|
|
|
|
|
|
result : '{e, GiveA V, GiveB V} r -> {e} r
|
2023-07-19 20:45:05 +03:00
|
|
|
result f =
|
2023-04-14 21:59:31 +03:00
|
|
|
impl : Request {GiveA V, GiveB V} r -> {} r
|
|
|
|
impl = cases
|
|
|
|
{ x } -> x
|
|
|
|
{ giveA _ -> _ } -> bug "impossible"
|
|
|
|
{ giveA2 _ -> _ } -> bug "impossible"
|
|
|
|
{ giveB _ -> _ } -> bug "impossible"
|
|
|
|
{ giveB2 _ -> _ } -> bug "impossible"
|
|
|
|
handle !f with impl
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-14 21:59:31 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-04-14 21:59:31 +03:00
|
|
|
This case would be ignored because it's already covered by the preceding case(s):
|
2023-07-19 20:45:05 +03:00
|
|
|
15 | { giveA2 _ -> _ } -> bug "impossible"
|
2023-04-14 21:59:31 +03:00
|
|
|
|
|
|
|
|
|
|
|
```
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2023-04-14 21:59:31 +03:00
|
|
|
unique ability GiveA a where
|
|
|
|
giveA : a -> {GiveA a} Unit
|
|
|
|
giveA2 : a -> {GiveA a} Unit
|
|
|
|
|
|
|
|
unique ability GiveB a where
|
|
|
|
giveB : a -> {GiveB a} Unit
|
|
|
|
giveB2 : a -> {GiveB a} Unit
|
|
|
|
|
|
|
|
result : '{e, GiveA V, GiveB V} r -> {e} r
|
2023-07-19 20:45:05 +03:00
|
|
|
result f =
|
2023-04-14 21:59:31 +03:00
|
|
|
impl : Request {GiveA V, GiveB V} r -> {} r
|
|
|
|
impl = cases
|
|
|
|
{ x } -> x
|
|
|
|
{ giveA2 _ -> _ } -> bug "impossible"
|
|
|
|
{ giveB _ -> _ } -> bug "impossible"
|
|
|
|
handle !f with impl
|
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2023-04-14 21:59:31 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2023-04-14 21:59:31 +03:00
|
|
|
I found and typechecked these definitions in scratch.u. If you
|
|
|
|
do an `add` or `update`, here's how your codebase would
|
|
|
|
change:
|
|
|
|
|
|
|
|
⍟ These new definitions are ok to `add`:
|
|
|
|
|
2024-01-04 11:42:12 +03:00
|
|
|
ability GiveA a
|
|
|
|
ability GiveB a
|
2023-04-18 16:17:34 +03:00
|
|
|
result : '{e, GiveA V, GiveB V} r ->{e} r
|
2023-04-14 21:59:31 +03:00
|
|
|
|
|
|
|
```
|