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.
144 lines
3.6 KiB
Markdown
144 lines
3.6 KiB
Markdown
``` unison
|
|
id x = x
|
|
|
|
structural ability Stream a where
|
|
emit : a -> ()
|
|
|
|
Stream.foldl : (x ->{g} a ->{g} x) -> x -> '{g, Stream a} r -> '{g} x
|
|
Stream.foldl f z str _ =
|
|
h acc = cases
|
|
{ emit x -> k } -> handle !k with h (f acc x)
|
|
{ _ } -> acc
|
|
handle !str with h z
|
|
|
|
Stream.range : Nat -> Nat -> '{Stream Nat} ()
|
|
Stream.range m n = do
|
|
f : Nat ->{Stream Nat} ()
|
|
f k = if k < n then emit k ; f (k+1) else ()
|
|
f m
|
|
|
|
unique type Fold' g a b x = Fold' (x -> {g} a -> {g} x) x (x -> {g} b)
|
|
|
|
unique type Fold g a b = Fold (∀ g2 r. (∀ x. Fold' g a b x -> {g2} r) -> {g2} r)
|
|
|
|
Fold.fromFold' : Fold' g a b x -> Fold g a b
|
|
Fold.fromFold' fold = Fold.Fold (f -> f fold)
|
|
|
|
Fold.mkFold : (t -> {g} a -> {g} t) -> t -> (t -> {g} b) -> Fold g a b
|
|
Fold.mkFold step init extract =
|
|
Fold.fromFold' (Fold'.Fold' step init extract)
|
|
|
|
folds.all : (a -> {g} Boolean) -> Fold g a Boolean
|
|
folds.all predicate =
|
|
Fold.mkFold (b -> a -> b && (predicate a)) true id
|
|
|
|
Fold.Stream.fold : Fold g a b -> '{g, Stream a} r -> '{g} b
|
|
Fold.Stream.fold =
|
|
run: Fold' g a b x -> '{g, Stream a} r -> '{g} b
|
|
run =
|
|
cases Fold'.Fold' step init extract ->
|
|
stream -> _ -> extract !(foldl step init stream)
|
|
cases
|
|
Fold f -> stream -> f (f' -> run f' stream)
|
|
|
|
> folds.all.tests.stream =
|
|
pred = n -> (Nat.gt n 2)
|
|
res : 'Boolean
|
|
res = Fold.Stream.fold (folds.all pred) (Stream.range 1 5)
|
|
!res Universal.== false
|
|
```
|
|
|
|
``` 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`:
|
|
|
|
type Fold g a b
|
|
type Fold' g a b x
|
|
structural ability Stream a
|
|
Fold.Stream.fold : Fold g a b
|
|
-> '{g, Stream a} r
|
|
-> '{g} b
|
|
Fold.fromFold' : Fold' g a b x -> Fold g a b
|
|
Fold.mkFold : (t ->{g} a ->{g} t)
|
|
-> t
|
|
-> (t ->{g} b)
|
|
-> Fold g a b
|
|
Stream.foldl : (x ->{g} a ->{g} x)
|
|
-> x
|
|
-> '{g, Stream a} r
|
|
-> '{g} x
|
|
Stream.range : Nat -> Nat -> '{Stream Nat} ()
|
|
folds.all : (a ->{g} Boolean) -> Fold g a Boolean
|
|
id : x -> x
|
|
|
|
Now evaluating any watch expressions (lines starting with
|
|
`>`)... Ctrl+C cancels.
|
|
|
|
44 | pred = n -> (Nat.gt n 2)
|
|
⧩
|
|
true
|
|
|
|
```
|
|
Tests some capabilities for catching runtime exceptions.
|
|
|
|
``` unison
|
|
catcher : '{IO} () ->{IO} Result
|
|
catcher act =
|
|
handle tryEval act with cases
|
|
{ raise _ -> _ } -> Ok "caught"
|
|
{ _ } -> Fail "nothing to catch"
|
|
|
|
tests _ =
|
|
[ catcher do
|
|
_ = 1/0
|
|
()
|
|
, catcher '(bug "testing")
|
|
, handle tryEval (do 1+1) with cases
|
|
{ raise _ -> _ } -> Fail "1+1 failed"
|
|
{ 2 } -> Ok "got the right answer"
|
|
{ _ } -> Fail "got the wrong answer"
|
|
]
|
|
```
|
|
|
|
``` 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`:
|
|
|
|
catcher : '{IO} () ->{IO} Result
|
|
tests : ∀ _. _ ->{IO} [Result]
|
|
|
|
```
|
|
``` ucm
|
|
scratch/main> add
|
|
|
|
⍟ I've added these definitions:
|
|
|
|
catcher : '{IO} () ->{IO} Result
|
|
tests : ∀ _. _ ->{IO} [Result]
|
|
|
|
scratch/main> io.test tests
|
|
|
|
New test results:
|
|
|
|
1. tests ◉ caught
|
|
◉ caught
|
|
◉ got the right answer
|
|
|
|
✅ 3 test(s) passing
|
|
|
|
Tip: Use view 1 to view the source of a test.
|
|
|
|
```
|