2021-09-02 03:34:19 +03:00
|
|
|
Regression test for https://github.com/unisonweb/unison/pull/2377
|
|
|
|
|
2024-07-10 17:46:18 +03:00
|
|
|
``` unison
|
2021-09-02 03:34:19 +03:00
|
|
|
structural ability Ab where
|
|
|
|
a: Nat -> ()
|
|
|
|
|
|
|
|
dopey = cases
|
|
|
|
?0 -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
grumpy = cases
|
|
|
|
d -> ()
|
|
|
|
|
|
|
|
happy = cases
|
|
|
|
true -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
false -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
sneezy = cases
|
|
|
|
+1 -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
bashful = cases
|
|
|
|
Some a -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
mouthy = cases
|
|
|
|
[] -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
pokey = cases
|
|
|
|
h +: t -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
sleepy = cases
|
|
|
|
i :+ l -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
demure = cases
|
|
|
|
[0] -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
angry = cases
|
|
|
|
a ++ [] -> ()
|
|
|
|
|
|
|
|
tremulous = cases
|
|
|
|
(0,1) -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
throaty = cases
|
|
|
|
{ Ab.a a -> k } -> ()
|
2023-04-14 03:58:52 +03:00
|
|
|
{ _ } -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
agitated = cases
|
|
|
|
a | a == 2 -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
doc = cases
|
|
|
|
y@4 -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
```
|
|
|
|
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2021-09-02 03:34:19 +03:00
|
|
|
|
2023-12-22 14:55:24 +03:00
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
|
2021-09-02 03:34:19 +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 Ab
|
|
|
|
agitated : Nat -> ()
|
|
|
|
angry : [t] -> ()
|
|
|
|
bashful : Optional a -> ()
|
|
|
|
demure : [Nat] -> ()
|
|
|
|
doc : Nat -> ()
|
|
|
|
dopey : Char -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
grumpy : ff284oqf651 -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
happy : Boolean -> ()
|
|
|
|
mouthy : [t] -> ()
|
|
|
|
pokey : [t] -> ()
|
|
|
|
sleepy : [t] -> ()
|
|
|
|
sneezy : Int -> ()
|
2021-10-28 23:51:58 +03:00
|
|
|
throaty : Request {g, Ab} x -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
tremulous : (Nat, Nat) -> ()
|
|
|
|
|
|
|
|
```
|
2024-07-10 19:17:15 +03:00
|
|
|
``` ucm
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> add
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
⍟ I've added these definitions:
|
|
|
|
|
|
|
|
structural ability Ab
|
|
|
|
agitated : Nat -> ()
|
|
|
|
angry : [t] -> ()
|
|
|
|
bashful : Optional a -> ()
|
|
|
|
demure : [Nat] -> ()
|
|
|
|
doc : Nat -> ()
|
|
|
|
dopey : Char -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
grumpy : ff284oqf651 -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
happy : Boolean -> ()
|
|
|
|
mouthy : [t] -> ()
|
|
|
|
pokey : [t] -> ()
|
|
|
|
sleepy : [t] -> ()
|
|
|
|
sneezy : Int -> ()
|
2021-10-28 23:51:58 +03:00
|
|
|
throaty : Request {g, Ab} x -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
tremulous : (Nat, Nat) -> ()
|
|
|
|
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> view dopey
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
dopey : Char -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
dopey = cases
|
|
|
|
?0 -> ()
|
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> view grumpy
|
2021-09-02 03:34:19 +03:00
|
|
|
|
2023-01-17 17:55:38 +03:00
|
|
|
grumpy : ff284oqf651 -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
grumpy = cases d -> ()
|
|
|
|
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> view happy
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
happy : Boolean -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
happy = cases
|
|
|
|
true -> ()
|
|
|
|
false -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> view sneezy
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
sneezy : Int -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
sneezy = cases
|
|
|
|
+1 -> ()
|
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> view bashful
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
bashful : Optional a -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
bashful = cases
|
|
|
|
Some a -> ()
|
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> view mouthy
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
mouthy : [t] -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
mouthy = cases
|
|
|
|
[] -> ()
|
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> view pokey
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
pokey : [t] -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
pokey = cases
|
|
|
|
h +: t -> ()
|
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> view sleepy
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
sleepy : [t] -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
sleepy = cases
|
|
|
|
i :+ l -> ()
|
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> view demure
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
demure : [Nat] -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
demure = cases
|
|
|
|
[0] -> ()
|
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> view angry
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
angry : [t] -> ()
|
|
|
|
angry = cases a ++ [] -> ()
|
|
|
|
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> view tremulous
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
tremulous : (Nat, Nat) -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
tremulous = cases
|
|
|
|
(0, 1) -> ()
|
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> view throaty
|
2021-09-02 03:34:19 +03:00
|
|
|
|
2021-10-28 23:51:58 +03:00
|
|
|
throaty : Request {g, Ab} x -> ()
|
2023-04-14 03:58:52 +03:00
|
|
|
throaty = cases
|
2023-07-21 09:12:22 +03:00
|
|
|
{ Ab.a a -> k } -> ()
|
|
|
|
{ _ } -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> view agitated
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
agitated : Nat -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
agitated = cases
|
|
|
|
a | a == 2 -> ()
|
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
2024-06-12 01:22:09 +03:00
|
|
|
scratch/main> view doc
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
doc : Nat -> ()
|
2023-01-17 17:55:38 +03:00
|
|
|
doc = cases
|
|
|
|
y@4 -> ()
|
|
|
|
_ -> ()
|
2021-09-02 03:34:19 +03:00
|
|
|
|
|
|
|
```
|