mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-11 02:25:39 +03:00
0031542faf
This is for consistency with the `cmark` style. Now the blocks we still pretty-print ourselves will match the bulk of them that `cmark` produces.
61 lines
1.4 KiB
Markdown
61 lines
1.4 KiB
Markdown
Tests for an ability failure that was caused by order dependence of
|
|
checking wanted vs. provided abilities. It was necessary to re-check
|
|
rows until a fixed point is reached.
|
|
|
|
``` unison
|
|
unique ability C c where
|
|
new : c a
|
|
receive : c a -> a
|
|
send : a -> c a -> ()
|
|
|
|
unique ability A t g where
|
|
fork : '{A t g, g, Exception} a -> t a
|
|
await : t a -> a
|
|
|
|
unique ability Ex where raise : () -> x
|
|
|
|
Ex.catch : '{Ex, g} a ->{g} Either () a
|
|
Ex.catch _ = todo "Exception.catch"
|
|
|
|
C.pure.run : (forall c . '{C c, g} r) ->{Ex, g} r
|
|
C.pure.run _ = todo "C.pure.run"
|
|
|
|
A.pure.run : (forall t . '{A t g, g} a) ->{Ex,g} a
|
|
A.pure.run _ = todo "A.pure.run"
|
|
|
|
ex : '{C c, A t {C c}} Nat
|
|
ex _ =
|
|
c = C.new
|
|
x = A.fork 'let
|
|
a = receive c
|
|
a + 10
|
|
y = A.fork 'let
|
|
send 0 c
|
|
()
|
|
A.await x
|
|
|
|
x : '{} (Either () Nat)
|
|
x _ = Ex.catch '(C.pure.run '(A.pure.run ex))
|
|
```
|
|
|
|
``` ucm
|
|
|
|
Loading changes detected in scratch.u.
|
|
|
|
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`:
|
|
|
|
ability A t g
|
|
ability C c
|
|
ability Ex
|
|
A.pure.run : (∀ t. '{g, A t g} a) ->{g, Ex} a
|
|
C.pure.run : (∀ c. '{g, C c} r) ->{g, Ex} r
|
|
Ex.catch : '{g, Ex} a ->{g} Either () a
|
|
ex : '{C c, A t {C c}} Nat
|
|
x : 'Either () Nat
|
|
|
|
```
|