act.bend

cswap-bend-cli@0.1.0.0 · 60 lines · 11 definitions

1import Base
2import cswap-bend-cli@0.1.0.0/fs.bend as Fs
3
4# `do Act<A>:` blocks: an IO step that can fail with Fs's `(code, message)`.
5# `x : T <- step` stops the block at the first Fail. A binder cannot be used
6# twice: rebind it with `+y : T = x` first.
7
8def of(-A: Type) -> Type:
9  IO(Fs.Res(A))
10
11def pure(-A: Type, x: A) -> of(A):
12  IO.pure(Fs.Res(A), Done{x})
13
14def fail(-A: Type, code: U32, msg: String) -> of(A):
15  IO.pure(Fs.Res(A), Fail{(code, msg)})
16
17def step(-A: Type, -B: Type, r: Fs.Res(A), f: A -> of(B)) -> of(B):
18  match r:
19    case Fail{e}:
20      IO.pure(Fs.Res(B), Fail{e})
21    case Done{a}:
22      f(a)
23
24def bind(-A: Type, -B: Type, m: of(A), f: A -> of(B)) -> of(B):
25  IO.bind(Fs.Res(A), Fs.Res(B), m, r => step(A, B, r, f))
26
27# Lift a plain IO value.
28def lift(-A: Type, m: IO(A)) -> of(A):
29  IO.bind(A, Fs.Res(A), m, x => IO.pure(Fs.Res(A), Done{x}))
30
31# Run `act` whatever `m` answered with, after it: for cleanup.
32def finally(-A: Type, act: of(A), cleanup: of(Unit)) -> of(A):
33  IO.bind(Fs.Res(A), Fs.Res(A), act, r => IO.bind(Fs.Res(Unit), Fs.Res(A), cleanup, c => IO.pure(Fs.Res(A), r)))
34
35# a when `c`, else b.
36def cond(-A: Type, c: Bool, a: of(A), b: of(A)) -> of(A):
37  match c:
38    case True{}:
39      a
40    case False{}:
41      b
42
43# Fail with (code, msg) unless `ok`.
44def guard(ok: Bool, code: U32, msg: String) -> of(Unit):
45  match ok:
46    case True{}:
47      pure(Unit, Unit{})
48    case False{}:
49      fail(Unit, code, msg)
50
51def on_fail2(-A: Type, r: Fs.Res(A), cleanup: of(Unit)) -> of(A):
52  match r:
53    case Done{x}:
54      IO.pure(Fs.Res(A), Done{x})
55    case Fail{e}:
56      IO.bind(Fs.Res(Unit), Fs.Res(A), cleanup, c => IO.pure(Fs.Res(A), Fail{e}))
57
58# Run `cleanup` only when `act` failed, and still answer the failure.
59def on_fail(-A: Type, act: of(A), cleanup: of(Unit)) -> of(A):
60  IO.bind(Fs.Res(A), Fs.Res(A), act, r => on_fail2(A, r, cleanup))