base.bend

Base · 3,210 lines · 486 definitions

1# Types
2# =====
3
4# Data
5# ----
6
7type Empty is Data:
8
9type Unit is Data:
10  Unit{}
11
12type Bool is Data:
13  False{}
14  True{}
15
16type Cmp is Data:
17  LT{}
18  EQ{}
19  GT{}
20
21type Either<a, b, -A: Kind(a), -B: Kind(b)> is Kind(a <&> b):
22  Inl{value: A}
23  Inr{value: B}
24
25type Sigma<a, b, -A: Kind(a), -B: @-x: A -> Kind(b)> is Kind(a <&> b):
26  Tuple{fst: A, snd: B(fst)}
27
28type Nat is Data:
29  Zero{}
30  Succ{pred: Nat}
31
32type Maybe<a, -A: Kind(a)> is Kind(a):
33  None{}
34  Some{value: A}
35
36type Result<a, b, -E: Kind(a), -A: Kind(b)> is Kind(a <&> b):
37  Fail{error: E}
38  Done{value: A}
39
40# What a try_ operation answers: Ready{x}, x what its blocking twin answers,
41# or Wait{rest} once ms milliseconds pass first (0: at once), rest what did
42# not happen (the value or the bytes not sent).
43type Poll<a, b, -A: Kind(a), -R: Kind(b)> is Kind(a <&> b):
44  Ready{value: A}
45  Wait{rest: R}
46
47type List<a, -A: Kind(a)> is Kind(a):
48  Nil{}
49  Con{head: A, tail: List<a, A>}
50
51type Word.Nil is Data:
52  WNil{}
53
54type Word.Con<-p: Nat> is Data:
55  WCon{head: Bool, tail: Word(p)}
56
57def Word(n: Nat) -> Data:
58  match n:
59    case 0n:
60      Word.Nil
61    case 1n+p:
62      Word.Con<p>
63
64type U32 is Data:
65  U32{data: Word(32n)}
66
67type F32 is Data:
68  F32{data: Word(32n)}
69
70type Char is Data:
71  Chr{code: U32}
72
73type String is Data:
74  SNil{}
75  SCon{head: Char, tail: String}
76
77type Array<-T: Type> is Type:
78  ALeaf{value: T}
79  ANode{xs: Array<T>, ys: Array<T>}
80
81type Image is Data:
82  Pix{color: U32}
83  Qua{tl: Image, tr: Image, bl: Image, br: Image}
84
85# Key is a key, pressed or let go. Text is what the keys typed, after
86# Shift, Caps Lock, the layout and any input method: never a control
87# character, so Enter or Backspace come only as Keys. A long input method
88# commit can come as several Texts.
89type Event is Data:
90  Key{code: U32, down: Bool}
91  Text{text: String}
92  Mouse{x: U32, y: U32, button: U32, down: Bool}
93  Move{x: U32, y: U32}
94  Look{dx: F32, dy: F32}
95  Scroll{x: U32, y: U32, dx: F32, dy: F32}
96  Close{}
97
98type Map<a, -V: Kind(a)> is Kind(a):
99  MTip{}
100  MLeaf{key: String, val: V}
101  MNode{pos: Nat, lo: Map<a, V>, hi: Map<a, V>}
102
103# Effects
104# -------
105
106# A handle is opaque, a law with no constructor and no field, so no
107# program forges one, and linear (Type), so none copies or reuses one.
108law File:
109  Type
110
111law Socket:
112  Type
113
114law Listener:
115  Type
116
117law Window:
118  Type
119
120law Audio:
121  Type
122
123# A channel is Data: the computations it links each hold a copy.
124law Chan:
125  for -A: Type
126  Data
127
128type IO.OP<-R: Type> is Type:
129  Emit{value: R}
130  Halt{code: U32, message: String}
131  Exit{code: U32}
132
133type App<-S: Type> is Type:
134  App{view: S -> Pair(S, Image), tick: List<Event> -> S -> IO(Maybe<S>)}
135
136# Defs
137# ====
138
139# Pair
140# ----
141
142def Pair(-A: Type, -B: Type) -> Type:
143  Sigma<&1, &1, A, _ => B>
144
145def Exists(-A: Type, -B: @-x: A -> Type) -> Type:
146  Sigma<&1, &1, A, B>
147
148def Or(-A: Type, -B: Type) -> Type:
149  Either<&1, &1, A, B>
150
151def Pair.fst(-A: Type, -B: Type, p: A & B) -> A:
152  (a, b) = p
153  a
154
155def Pair.snd(-A: Type, -B: Type, p: A & B) -> B:
156  (a, b) = p
157  b
158
159# Effects
160# -------
161
162def IO(-A: Type) -> Type:
163  @-R: Type ->
164  @k: (A -> IO.OP<R>) ->
165  IO.OP<R>
166
167def IO.pure(-A: Type, x: A) -> IO(A):
168  R => k => k(x)
169
170def IO.bind(-A: Type, -B: Type, m: IO(A), f: A -> IO(B)) -> IO(B):
171  R => k => m(R, x => f(x, R, k))
172
173def IO.print(text: String) -> IO(Unit):
174  import "./effs/print.c"
175  import "./effs/print.js"
176
177def IO.write(text: String) -> IO(Unit):
178  import "./effs/write.c"
179  import "./effs/write.js"
180
181def IO.print_err(text: String) -> IO(Unit):
182  import "./effs/print_err.c"
183  import "./effs/print_err.js"
184
185def IO.get_env(name: String) -> IO(Result<&1, &1, U32 & String, String>):
186  import "./effs/get_env.c"
187  import "./effs/get_env.js"
188
189# The command line, less the runtime's own options: the program as invoked
190# (the binary, the JS file or the .bend file), then its arguments.
191def IO.args() -> IO(List<String>):
192  import "./effs/args.c"
193  import "./effs/args.js"
194
195# IO.args as the OS hands it over: each entry's bytes (0..255), one List
196# cell each, with no UTF-8 decoding, so an argument that isn't UTF-8 (a
197# Latin-1 file name) keeps every byte, and File.open_bytes opens it. The
198# JS lanes get the arguments already decoded by the host: there, a byte
199# that isn't UTF-8 arrives as U+FFFD's UTF-8, EF BF BD.
200def IO.args_bytes() -> IO(List<List<&2, U32>>):
201  import "./effs/args.c"
202  import "./effs/args.js"
203
204# Runs an argv subprocess on C, Bun and Node, without a shell.
205# max_output bounds combined stdout/stderr bytes; timeout_ms includes pipe draining.
206def Process.run(program: String, args: List<String>, input: String,
207  max_output: U32, timeout_ms: U32) ->
208  IO(Result<&1, &1, U32 & String, U32 & (String & String)>):
209  import "./effs/process_run.c"
210  import "./effs/process_run.js"
211
212def IO.die(-A: Type, code: U32, msg: String) -> IO(A):
213  R => k => Halt{code, msg}
214
215def IO.exit(code: U32) -> IO(Unit):
216  R => k => Exit{code}
217
218def IO.pass(-A: Type, r: Result<&1, &1, U32 & String, A>) -> IO(A):
219  match r:
220    case Done{value}:
221      IO.pure(A, value)
222    case Fail{(code, message)}:
223      IO.die(A, code, message)
224
225def IO.try(-A: Type, act: IO(Result<&1, &1, U32 & String, A>)) -> IO(A):
226  IO.bind(Result<&1, &1, U32 & String, A>, A, act, IO.pass(A))
227
228def IO.random_u32() -> IO(Result<&1, &1, U32 & String, U32>):
229  import "./effs/random_u32.c"
230  import "./effs/random_u32.js"
231
232def IO.spawn(-A: Type, act: IO(A)) -> IO(Unit):
233  import "./effs/spawn.c"
234  import "./effs/spawn.js"
235
236def IO.sleep(ms: U32) -> IO(Unit):
237  import "./effs/sleep.c"
238  import "./effs/sleep.js"
239
240def IO.now() -> IO(Nat):
241  import "./effs/now.c"
242  import "./effs/now.js"
243
244def IO.thread_count() -> IO(U32):
245  import "./effs/thread_count.c"
246  import "./effs/thread_count.js"
247
248def Chan.new(-A: Type, room: U32) -> IO(Chan(A)):
249  import "./effs/chan.c"
250  import "./effs/chan.js"
251
252# Done{} once the channel takes the value, Fail{value} if it is closed.
253def Chan.send(-A: Type, chan: Chan(A), value: A) -> IO(Result<&1, &1, A, Unit>):
254  import "./effs/chan.c"
255  import "./effs/chan.js"
256
257# Some{value}, or None{} once the channel is closed and drained.
258def Chan.recv(-A: Type, chan: Chan(A)) -> IO(Maybe<&1, A>):
259  import "./effs/chan.c"
260  import "./effs/chan.js"
261
262def Chan.try_send(-A: Type, chan: Chan(A), value: A, ms: U32) ->
263  IO(Poll<&1, &1, Result<&1, &1, A, Unit>, A>):
264  import "./effs/chan.c"
265  import "./effs/chan.js"
266
267def Chan.try_recv(-A: Type, chan: Chan(A), ms: U32) ->
268  IO(Poll<&1, &1, Maybe<&1, A>, Unit>):
269  import "./effs/chan.c"
270  import "./effs/chan.js"
271
272def Chan.close(-A: Type, chan: Chan(A)) -> IO(Unit):
273  import "./effs/chan.c"
274  import "./effs/chan.js"
275
276def IO.fork.go(-A: Type, act: IO(A), chan: Chan(A)) -> IO(Chan(A)):
277  +c = chan
278  sent = IO.bind(A, Result<&1, &1, A, Unit>, act, x => Chan.send(A, c, x))
279  IO.bind(Unit, Chan(A), IO.spawn(Result<&1, &1, A, Unit>, sent),
280    u => IO.pure(Chan(A), c))
281
282def IO.fork(-A: Type, act: IO(A)) -> IO(Chan(A)):
283  IO.bind(Chan(A), Chan(A), Chan.new(A, 1), IO.fork.go(A, act))
284
285def IO.join.go(-A: Type, chan: Chan(A), got: Maybe<&1, A>) -> IO(A):
286  match got:
287    case None{}:
288      IO.die(A, 1, "IO.join: the channel was closed")
289    case Some{value}:
290      IO.bind(Unit, A, Chan.close(A, chan), u => IO.pure(A, value))
291
292def IO.join(-A: Type, +chan: Chan(A)) -> IO(A):
293  IO.bind(Maybe<&1, A>, A, Chan.recv(A, chan), IO.join.go(A, chan))
294
295# Some{x} if act answers x within ms milliseconds, else None{}. The loser
296# is not cancelled: it runs to its end before the program exits.
297def IO.within(-A: Type, ms: U32, act: IO(A)) -> IO(Maybe<&1, A>):
298  won = IO.bind(A, Maybe<&1, A>, act, x => IO.pure(Maybe<&1, A>, Some{x}))
299  late = IO.bind(Unit, Maybe<&1, A>, IO.sleep(ms), u => IO.pure(Maybe<&1, A>, None{}))
300  both = IO.bind(Chan(Maybe<&1, A>), Chan(Maybe<&1, A>), IO.fork(Maybe<&1, A>, won),
301    IO.fork.go(Maybe<&1, A>, late))
302  IO.bind(Chan(Maybe<&1, A>), Maybe<&1, A>, both, c => IO.join(Maybe<&1, A>, c))
303
304def File.open(path: String, mode: String) ->
305  IO(Result<&1, &1, U32 & String, File>):
306  import "./effs/file_open.c"
307  import "./effs/file_open.js"
308
309# The path as its bytes (0..255), with no UTF-8 encoding, so a name that
310# isn't UTF-8, as IO.args_bytes gives it, opens. A value past 255 fails
311# with EINVAL, and a 0 with EILSEQ, as a NUL in File.open's path does.
312def File.open_bytes(path: List<&2, U32>, mode: String) ->
313  IO(Result<&1, &1, U32 & String, File>):
314  import "./effs/file_open.c"
315  import "./effs/file_open.js"
316
317def File.read(file: File, max: U32) ->
318  IO(File & Result<&1, &1, U32 & String, String>):
319  import "./effs/file_read.c"
320  import "./effs/file_read.js"
321
322def File.read_bytes(file: File, max: U32) ->
323  IO(File & Result<&1, &1, U32 & String, List<&2, U32>>):
324  import "./effs/file_read.c"
325  import "./effs/file_read.js"
326
327def File.read_at(file: File, offset: U32, max: U32) ->
328  IO(File & Result<&1, &1, U32 & String, List<&2, U32>>):
329  import "./effs/file_read.c"
330  import "./effs/file_read.js"
331
332def File.size(file: File) ->
333  IO(File & Result<&1, &1, U32 & String, U32>):
334  import "./effs/file_size.c"
335  import "./effs/file_size.js"
336
337def File.write(file: File, data: String) ->
338  IO(File & Result<&1, &1, U32 & String, Unit>):
339  import "./effs/file_write.c"
340  import "./effs/file_write.js"
341
342def File.write_bytes(file: File, data: List<&2, U32>) ->
343  IO(File & Result<&1, &1, U32 & String, Unit>):
344  import "./effs/file_write.c"
345  import "./effs/file_write.js"
346
347def File.close(file: File) -> IO(Unit):
348  import "./effs/file_close.c"
349  import "./effs/file_close.js"
350
351def TCP.listen(host: String, port: U32) -> IO(Result<&1, &1, U32 & String, Listener>):
352  import "./effs/tcp_listen.c"
353  import "./effs/tcp_listen.js"
354
355def TCP.accept(listener: Listener) ->
356  IO(Listener & Result<&1, &1, U32 & String, Socket>):
357  import "./effs/tcp_accept.c"
358  import "./effs/tcp_accept.js"
359
360def TCP.try_accept(listener: Listener, ms: U32) ->
361  IO(Listener & Poll<&1, &1, Result<&1, &1, U32 & String, Socket>, Unit>):
362  import "./effs/tcp_accept.c"
363  import "./effs/tcp_accept.js"
364
365def TCP.connect(host: String, port: U32) ->
366  IO(Result<&1, &1, U32 & String, Socket>):
367  import "./effs/tcp_connect.c"
368  import "./effs/tcp_connect.js"
369
370# A failed or timed-out send returns the exact unsent bytes: the kernel
371# may stop inside UTF-8. Resume with TCP.send_bytes. Sent means taken by
372# the kernel, not yet read by the peer.
373def TCP.send(sock: Socket, data: String) ->
374  IO(Socket & Result<&1, &1, (U32 & String) & List<&2, U32>, Unit>):
375  import "./effs/tcp_send.c"
376  import "./effs/tcp_send.js"
377
378def TCP.try_send(sock: Socket, data: String, ms: U32) ->
379  IO(Socket & Poll<&1, &1, Result<&1, &1, (U32 & String) & List<&2, U32>, Unit>,
380    List<&2, U32>>):
381  import "./effs/tcp_send.c"
382  import "./effs/tcp_send.js"
383
384# Some{data}, or None{} once the peer has sent everything (it may still
385# read). A max of 0 fails with EINVAL, as in every receive below.
386def TCP.recv(sock: Socket, max: U32) ->
387  IO(Socket & Result<&1, &1, U32 & String, Maybe<&1, String>>):
388  import "./effs/tcp_recv.c"
389  import "./effs/tcp_recv.js"
390
391def TCP.try_recv(sock: Socket, max: U32, ms: U32) ->
392  IO(Socket & Poll<&1, &1, Result<&1, &1, U32 & String, Maybe<&1, String>>, Unit>):
393  import "./effs/tcp_recv.c"
394  import "./effs/tcp_recv.js"
395
396# The bytes as they are (0..255), one List cell each: no UTF-8 decoding, so
397# binary data and a character split between two reads survive. A value past
398# 255 fails with EINVAL before any byte is sent.
399def TCP.send_bytes(sock: Socket, data: List<&2, U32>) ->
400  IO(Socket & Result<&1, &1, (U32 & String) & List<&2, U32>, Unit>):
401  import "./effs/tcp_send.c"
402  import "./effs/tcp_send.js"
403
404def TCP.try_send_bytes(sock: Socket, data: List<&2, U32>, ms: U32) ->
405  IO(Socket & Poll<&1, &1, Result<&1, &1, (U32 & String) & List<&2, U32>, Unit>,
406    List<&2, U32>>):
407  import "./effs/tcp_send.c"
408  import "./effs/tcp_send.js"
409
410def TCP.recv_bytes(sock: Socket, max: U32) ->
411  IO(Socket & Result<&1, &1, U32 & String, Maybe<&1, List<&2, U32>>>):
412  import "./effs/tcp_recv.c"
413  import "./effs/tcp_recv.js"
414
415def TCP.try_recv_bytes(sock: Socket, max: U32, ms: U32) ->
416  IO(Socket & Poll<&1, &1, Result<&1, &1, U32 & String, Maybe<&1, List<&2, U32>>>,
417    Unit>):
418  import "./effs/tcp_recv.c"
419  import "./effs/tcp_recv.js"
420
421def UDP.bind(host: String, port: U32) -> IO(Result<&1, &1, U32 & String, Socket>):
422  import "./effs/udp_bind.c"
423  import "./effs/udp_bind.js"
424
425# A datagram goes whole or not at all: a failed send hands it back.
426def UDP.send_to(sock: Socket, host: String, port: U32, data: String) ->
427  IO(Socket & Result<&1, &1, (U32 & String) & String, Unit>):
428  import "./effs/udp_send_to.c"
429  import "./effs/udp_send_to.js"
430
431def UDP.try_send_to(sock: Socket, host: String, port: U32, data: String, ms: U32) ->
432  IO(Socket & Poll<&1, &1, Result<&1, &1, (U32 & String) & String, Unit>, String>):
433  import "./effs/udp_send_to.c"
434  import "./effs/udp_send_to.js"
435
436# The datagram's bytes as they are (0..255), one List cell each: no UTF-8
437# encoding, so a binary protocol's datagram goes out as written. A value
438# past 255 fails with EINVAL before anything is sent.
439def UDP.send_bytes_to(sock: Socket, host: String, port: U32, data: List<&2, U32>) ->
440  IO(Socket & Result<&1, &1, (U32 & String) & List<&2, U32>, Unit>):
441  import "./effs/udp_send_to.c"
442  import "./effs/udp_send_to.js"
443
444def UDP.try_send_bytes_to(sock: Socket, host: String, port: U32, data: List<&2, U32>,
445  ms: U32) ->
446  IO(Socket & Poll<&1, &1, Result<&1, &1, (U32 & String) & List<&2, U32>, Unit>,
447    List<&2, U32>>):
448  import "./effs/udp_send_to.c"
449  import "./effs/udp_send_to.js"
450
451# A datagram may be empty: UDP has no end, so no None{}.
452def UDP.recv_from(sock: Socket, max: U32) ->
453  IO(Socket & Result<&1, &1, U32 & String, String & U32 & String>):
454  import "./effs/udp_recv_from.c"
455  import "./effs/udp_recv_from.js"
456
457def UDP.try_recv_from(sock: Socket, max: U32, ms: U32) ->
458  IO(Socket & Poll<&1, &1, Result<&1, &1, U32 & String, String & U32 & String>, Unit>):
459  import "./effs/udp_recv_from.c"
460  import "./effs/udp_recv_from.js"
461
462# The datagram's bytes as they are: no UTF-8 decoding, so every byte of a
463# binary datagram survives.
464def UDP.recv_bytes_from(sock: Socket, max: U32) ->
465  IO(Socket & Result<&1, &1, U32 & String, String & U32 & List<&2, U32>>):
466  import "./effs/udp_recv_from.c"
467  import "./effs/udp_recv_from.js"
468
469def UDP.try_recv_bytes_from(sock: Socket, max: U32, ms: U32) ->
470  IO(Socket & Poll<&1, &1, Result<&1, &1, U32 & String,
471    String & U32 & List<&2, U32>>, Unit>):
472  import "./effs/udp_recv_from.c"
473  import "./effs/udp_recv_from.js"
474
475def Socket.close(socket: Socket) -> IO(Unit):
476  import "./effs/socket_close.c"
477  import "./effs/socket_close.js"
478
479def Listener.close(listener: Listener) -> IO(Unit):
480  import "./effs/listener_close.c"
481  import "./effs/listener_close.js"
482
483def Window.open(title: String, width: U32, height: U32) ->
484  IO(Result<&1, &1, U32 & String, Window>):
485  import "./effs/window.c"
486  import "./effs/window_open.js"
487
488def Window.frame(window: Window, image: Image) ->
489  IO(Window & Image & List<Event>):
490  import "./effs/window.c"
491  import "./effs/window_frame.js"
492
493def Window.set_title(window: Window, title: String) -> IO(Window):
494  import "./effs/window.c"
495  import "./effs/window_set_title.js"
496
497# While grabbed, the cursor is hidden and held, and the mouse's motion
498# comes as Look deltas instead of Move; losing focus releases it.
499def Window.grab(window: Window, on: Bool) -> IO(Window):
500  import "./effs/window.c"
501  import "./effs/window_grab.js"
502
503def Window.close(window: Window) -> IO(Unit):
504  import "./effs/window.c"
505  import "./effs/window_close.js"
506
507def Audio.open(rate: U32) -> IO(Result<&1, &1, U32 & String, Audio>):
508  import "./effs/audio.c"
509  import "./effs/audio_open.js"
510
511def Audio.write(audio: Audio, samples: List<&2, F32>) -> IO(Audio & U32):
512  import "./effs/audio.c"
513  import "./effs/audio_write.js"
514
515def Audio.close(audio: Audio) -> IO(Unit):
516  import "./effs/audio.c"
517  import "./effs/audio_close.js"
518
519# Equal
520# -----
521
522law Equal.cong:
523  for -A: Type
524  for -B: Type
525  for -f: A -> B
526  for -a: A
527  for -b: A
528  for  e: {a == b : A}
529  {f(a) == f(b) : B}
530
531def Equal.cong(A, B, f, a, b, e):
532  %e : {f(a) == f(_) : B}
533  {==}
534
535law Equal.sym:
536  for -A: Type
537  for -a: A
538  for -b: A
539  for  e: {a == b : A}
540  {b == a : A}
541
542def Equal.sym(A, a, b, e):
543  %e : {_ == a : A}
544  {==}
545
546law Equal.trans:
547  for -A : Type
548  for -a : A
549  for -b : A
550  for -c : A
551  for ab : {a == b : A}
552  for bc : {b == c : A}
553  {a == c : A}
554
555def Equal.trans(A, a, b, c, ab, bc):
556  %bc : {a == _ : A}
557  ab
558
559# Empty
560# -----
561
562def Empty.absurd(-A: Type, e: Empty) -> A:
563  match e:
564
565# Bool
566# ----
567
568def Bool.not(b: Bool) -> Bool:
569  match b:
570    case False{}:
571      True{}
572    case True{}:
573      False{}
574
575def Bool.and(a: Bool, b: Bool) -> Bool:
576  match a:
577    case False{}:
578      False{}
579    case True{}:
580      b
581
582def Bool.or(a: Bool, b: Bool) -> Bool:
583  match a:
584    case False{}:
585      b
586    case True{}:
587      True{}
588
589def Bool.xor(a: Bool, b: Bool) -> Bool:
590  match a:
591    case False{}:
592      b
593    case True{}:
594      Bool.not(b)
595
596def Bool.cmp(a: Bool, b: Bool) -> Cmp:
597  match a b:
598    case False{} False{}:
599      EQ{}
600    case False{} True{}:
601      LT{}
602    case True{} False{}:
603      GT{}
604    case True{} True{}:
605      EQ{}
606
607def Bool.full_add(a: Bool, +b: Bool, +c: Bool) -> Bool & Bool:
608  match a:
609    case False{}:
610      (Bool.xor(b, c), Bool.and(b, c))
611    case True{}:
612      (Bool.not(Bool.xor(b, c)), Bool.or(b, c))
613
614def Bool.pick(-A: Type, c: Bool, a: A, b: A) -> A:
615  match c:
616    case False{}:
617      b
618    case True{}:
619      a
620
621def Bool.to_u32(b: Bool) -> U32:
622  match b:
623    case False{}:
624      0
625    case True{}:
626      1
627
628# Cmp
629# ---
630
631def Cmp.is_lt(c: Cmp) -> Bool:
632  match c:
633    case LT{}:
634      True{}
635    case o:
636      False{}
637
638def Cmp.is_eq(c: Cmp) -> Bool:
639  match c:
640    case EQ{}:
641      True{}
642    case o:
643      False{}
644
645def Cmp.is_gt(c: Cmp) -> Bool:
646  match c:
647    case GT{}:
648      True{}
649    case o:
650      False{}
651
652def Cmp.is_le(c: Cmp) -> Bool:
653  match c:
654    case GT{}:
655      False{}
656    case o:
657      True{}
658
659def Cmp.is_ge(c: Cmp) -> Bool:
660  match c:
661    case LT{}:
662      False{}
663    case o:
664      True{}
665
666# Nat
667# ---
668
669def Nat.double(n: Nat) -> Nat:
670  match n:
671    case 0n:
672      0n
673    case 1n+p:
674      2n+Nat.double(p)
675
676def Nat.add(a: Nat, b: Nat) -> Nat:
677  match a:
678    case 0n:
679      b
680    case 1n+p:
681      1n+Nat.add(p, b)
682
683def Nat.sub(a: Nat, b: Nat) -> Nat:
684  match a b:
685    case 0n _:
686      0n
687    case 1n+ap 0n:
688      1n+ap
689    case 1n+ap 1n+bp:
690      Nat.sub(ap, bp)
691
692def Nat.mul(a: Nat, +b: Nat) -> Nat:
693  match a:
694    case 0n:
695      0n
696    case 1n+p:
697      Nat.add(b, Nat.mul(p, b))
698
699def Nat.divmod.go(n: Nat, m: Nat, d: Nat, r: Nat) -> Nat & Nat:
700  match n:
701    case 0n:
702      (d, r)
703    case 1n+np:
704      match m:
705        case 0n:
706          Nat.divmod.go(np, r, 1n+d, 0n)
707        case 1n+mp:
708          Nat.divmod.go(np, mp, d, 1n+r)
709
710def Nat.divmod(a: Nat, b: Nat) -> Nat & Nat:
711  match b:
712    case 0n:
713      (0n, a)
714    case 1n+bp:
715      Nat.divmod.go(a, bp, 0n, 0n)
716
717def Nat.cmp(a: Nat, b: Nat) -> Cmp:
718  match a b:
719    case 0n 0n:
720      EQ{}
721    case 0n 1n+bp:
722      LT{}
723    case 1n+ap 0n:
724      GT{}
725    case 1n+ap 1n+bp:
726      Nat.cmp(ap, bp)
727
728def Nat.is_lt(a: Nat, b: Nat) -> Bool:
729  Cmp.is_lt(Nat.cmp(a, b))
730
731def Nat.is_eq(a: Nat, b: Nat) -> Bool:
732  Cmp.is_eq(Nat.cmp(a, b))
733
734def Nat.is_ne(a: Nat, b: Nat) -> Bool:
735  Bool.not(Cmp.is_eq(Nat.cmp(a, b)))
736
737def Nat.is_le(a: Nat, b: Nat) -> Bool:
738  Cmp.is_le(Nat.cmp(a, b))
739
740def Nat.is_gt(a: Nat, b: Nat) -> Bool:
741  Cmp.is_gt(Nat.cmp(a, b))
742
743def Nat.is_ge(a: Nat, b: Nat) -> Bool:
744  Cmp.is_ge(Nat.cmp(a, b))
745
746def Nat.min(+a: Nat, +b: Nat) -> Nat:
747  match a b:
748    case 0n _:
749      0n
750    case 1n+ap 0n:
751      0n
752    case 1n+ap 1n+bp:
753      1n+Nat.min(ap, bp)
754
755def Nat.max(+a: Nat, +b: Nat) -> Nat:
756  match a b:
757    case 0n _:
758      b
759    case 1n+ap 0n:
760      1n+ap
761    case 1n+ap 1n+bp:
762      1n+Nat.max(ap, bp)
763
764law Nat.ge_refl:
765  for a: Nat
766  {Nat.is_ge(a, a) == True{} : Bool}
767
768def Nat.ge_refl(a):
769  match a:
770    case 0n:
771      {==}
772    case 1n+p:
773      Nat.ge_refl(p)
774
775law Nat.max_ge_l:
776  for +a: Nat
777  for +b: Nat
778  {Nat.is_ge(Nat.max(a, b), a) == True{} : Bool}
779
780def Nat.max_ge_l(a, b):
781  match a b:
782    case 0n 0n:
783      {==}
784    case 0n 1n+bp:
785      {==}
786    case 1n+ap 0n:
787      Nat.ge_refl(a)
788    case 1n+ap 1n+bp:
789      Nat.max_ge_l(ap, bp)
790
791law Nat.max_ge_r:
792  for +a: Nat
793  for +b: Nat
794  {Nat.is_ge(Nat.max(a, b), b) == True{} : Bool}
795
796def Nat.max_ge_r(a, b):
797  match a b:
798    case 0n _:
799      Nat.ge_refl(b)
800    case 1n+ap 0n:
801      {==}
802    case 1n+ap 1n+bp:
803      Nat.max_ge_r(ap, bp)
804
805def Nat.div(a: Nat, b: Nat) -> Nat:
806  Pair.fst(Nat, Nat, Nat.divmod(a, b))
807
808def Nat.mod(a: Nat, b: Nat) -> Nat:
809  Pair.snd(Nat, Nat, Nat.divmod(a, b))
810
811def Nat.pow(+a: Nat, b: Nat) -> Nat:
812  match b:
813    case 0n:
814      1n
815    case 1n+p:
816      Nat.mul(a, Nat.pow(a, p))
817
818# Maybe
819# -----
820
821def Maybe.pure(a, -A: Kind(a), x: A) -> Maybe<a, A>:
822  Some{x}
823
824def Maybe.bind(
825  a, -A: Kind(a), -B: Kind(a), m: Maybe<a, A>, f: A -> Maybe<a, B>
826) -> Maybe<a, B>:
827  match m:
828    case None{}:
829      None{}
830    case Some{x}:
831      f(x)
832
833def Maybe.default(a, -A: Kind(a), m: Maybe<a, A>, d: A) -> A:
834  match m:
835    case None{}:
836      d
837    case Some{x}:
838      x
839
840def Maybe.is_some(a, -A: Kind(a), m: Maybe<a, A>) -> Bool:
841  match m:
842    case None{}:
843      False{}
844    case Some{x}:
845      True{}
846
847def Maybe.is_none(a, -A: Kind(a), m: Maybe<a, A>) -> Bool:
848  Bool.not(Maybe.is_some(a, A, m))
849
850def Maybe.map(
851  a, -A: Kind(a), -B: Kind(a), f: A -> B, m: Maybe<a, A>
852) -> Maybe<a, B>:
853  match m:
854    case None{}:
855      None{}
856    case Some{x}:
857      Some{f(x)}
858
859def Maybe.or(a, -A: Kind(a), m: Maybe<a, A>, n: Maybe<a, A>) -> Maybe<a, A>:
860  match m:
861    case None{}:
862      n
863    case Some{x}:
864      Some{x}
865
866# Result
867# ------
868
869def Result.pure(a, b, -E: Kind(a), -A: Kind(b), x: A) -> Result<a, b, E, A>:
870  Done{x}
871
872def Result.bind(
873  a, b, -E: Kind(a), -A: Kind(b), -B: Kind(b), r: Result<a, b, E, A>,
874  f: A -> Result<a, b, E, B>
875) -> Result<a, b, E, B>:
876  match r:
877    case Fail{e}:
878      Fail{e}
879    case Done{x}:
880      f(x)
881
882def Result.default(
883  a, b, -E: Kind(a), -A: Kind(b), r: Result<a, b, E, A>, d: A
884) -> A:
885  match r:
886    case Fail{e}:
887      d
888    case Done{x}:
889      x
890
891def Result.is_done(
892  a, b, -E: Kind(a), -A: Kind(b), r: Result<a, b, E, A>
893) -> Bool:
894  match r:
895    case Fail{e}:
896      False{}
897    case Done{x}:
898      True{}
899
900def Result.is_fail(
901  a, b, -E: Kind(a), -A: Kind(b), r: Result<a, b, E, A>
902) -> Bool:
903  Bool.not(Result.is_done(a, b, E, A, r))
904
905def Result.map(
906  a, b, -E: Kind(a), -A: Kind(b), -B: Kind(b), f: A -> B,
907  r: Result<a, b, E, A>
908) -> Result<a, b, E, B>:
909  match r:
910    case Fail{e}:
911      Fail{e}
912    case Done{x}:
913      Done{f(x)}
914
915# List
916# ----
917
918def List.map(~A: Type, ~B: Type, ~f: A -> B, xs: List<A>) -> List<B>:
919  match xs:
920    case Nil{}:
921      Nil{}
922    case h <> t:
923      f(h) <> List.map(~A, ~B, ~f, t)
924
925def List.length(a, -A: Kind(a), xs: List<a, A>) -> Nat:
926  match xs:
927    case Nil{}:
928      0n
929    case h <> t:
930      1n+List.length(a, A, t)
931
932def List.append(a, -A: Kind(a), xs: List<a, A>, ys: List<a, A>) -> List<a, A>:
933  match xs:
934    case Nil{}:
935      ys
936    case h <> t:
937      h <> List.append(a, A, t, ys)
938
939def List.concat(a, -A: Kind(a), xss: List<a, List<a, A>>) -> List<a, A>:
940  match xss:
941    case Nil{}:
942      Nil{}
943    case h <> t:
944      List.append(a, A, h, List.concat(a, A, t))
945
946def List.reverse.go(a, -A: Kind(a), xs: List<a, A>, acc: List<a, A>) ->
947  List<a, A>:
948  match xs:
949    case Nil{}:
950      acc
951    case h <> t:
952      List.reverse.go(a, A, t, h <> acc)
953
954def List.reverse(a, -A: Kind(a), xs: List<a, A>) -> List<a, A>:
955  List.reverse.go(a, A, xs, Nil{})
956
957def List.is_empty(a, -A: Kind(a), xs: List<a, A>) -> Bool:
958  match xs:
959    case Nil{}:
960      True{}
961    case h <> t:
962      False{}
963
964def List.head(a, -A: Kind(a), xs: List<a, A>) -> Maybe<a, A>:
965  match xs:
966    case Nil{}:
967      None{}
968    case h <> t:
969      Some{h}
970
971def List.tail(a, -A: Kind(a), xs: List<a, A>) -> List<a, A>:
972  match xs:
973    case Nil{}:
974      Nil{}
975    case h <> t:
976      t
977
978def List.last.go(a, -A: Kind(a), xs: List<a, A>, last: A) -> A:
979  match xs:
980    case Nil{}:
981      last
982    case h <> t:
983      List.last.go(a, A, t, h)
984
985def List.last(a, -A: Kind(a), xs: List<a, A>) -> Maybe<a, A>:
986  match xs:
987    case Nil{}:
988      None{}
989    case h <> t:
990      Some{List.last.go(a, A, t, h)}
991
992def List.get(a, -A: Kind(a), xs: List<a, A>, n: Nat) -> Maybe<a, A>:
993  match xs n:
994    case Nil{} _:
995      None{}
996    case h <> t 0n:
997      Some{h}
998    case h <> t 1n+p:
999      List.get(a, A, t, p)
1000
1001def List.set(a, -A: Kind(a), xs: List<a, A>, n: Nat, x: A) -> List<a, A>:
1002  match xs n:
1003    case Nil{} _:
1004      Nil{}
1005    case h <> t 0n:
1006      x <> t
1007    case h <> t 1n+p:
1008      h <> List.set(a, A, t, p, x)
1009
1010def List.take(a, -A: Kind(a), xs: List<a, A>, n: Nat) -> List<a, A>:
1011  match xs n:
1012    case Nil{} _:
1013      Nil{}
1014    case h <> t 0n:
1015      Nil{}
1016    case h <> t 1n+p:
1017      h <> List.take(a, A, t, p)
1018
1019def List.drop(a, -A: Kind(a), xs: List<a, A>, n: Nat) -> List<a, A>:
1020  match xs n:
1021    case Nil{} _:
1022      Nil{}
1023    case h <> t 0n:
1024      h <> t
1025    case h <> t 1n+p:
1026      List.drop(a, A, t, p)
1027
1028def List.zip(
1029  a, -A: Kind(a), b, -B: Kind(b), xs: List<a, A>, ys: List<b, B>
1030) -> List<&1, A & B>:
1031  match xs ys:
1032    case Nil{} _:
1033      Nil{}
1034    case h <> t Nil{}:
1035      Nil{}
1036    case x <> xt y <> yt:
1037      (x, y) <> List.zip(a, A, b, B, xt, yt)
1038
1039def List.range.go(+n: Nat, acc: List<&2, Nat>) -> List<&2, Nat>:
1040  match n:
1041    case 0n:
1042      acc
1043    case 1n+p:
1044      List.range.go(p, p <> acc)
1045
1046def List.range(n: Nat) -> List<&2, Nat>:
1047  List.range.go(n, Nil{})
1048
1049def List.replicate(-A: Data, n: Nat, +x: A) -> List<&2, A>:
1050  match n:
1051    case 0n:
1052      Nil{}
1053    case 1n+p:
1054      x <> List.replicate(A, p, x)
1055
1056def List.filter.put(-A: Data, h: A, r: List<&2, A>, keep: Bool) -> List<&2, A>:
1057  match keep:
1058    case False{}:
1059      r
1060    case True{}:
1061      h <> r
1062
1063def List.filter(~A: Data, ~f: A -> Bool, xs: List<&2, A>) -> List<&2, A>:
1064  match xs:
1065    case Nil{}:
1066      Nil{}
1067    case +h <> t:
1068      List.filter.put(A, h, List.filter(~A, ~f, t), f(h))
1069
1070def List.foldl(
1071  ~a: Quant, ~A: Kind(a), ~B: Type, ~f: B -> A -> B, xs: List<a, A>, acc: B
1072) -> B:
1073  match xs:
1074    case Nil{}:
1075      acc
1076    case h <> t:
1077      List.foldl(~a, ~A, ~B, ~f, t, f(acc, h))
1078
1079def List.foldr(
1080  ~a: Quant, ~A: Kind(a), ~B: Type, ~f: A -> B -> B, xs: List<a, A>, z: B
1081) -> B:
1082  match xs:
1083    case Nil{}:
1084      z
1085    case h <> t:
1086      f(h, List.foldr(~a, ~A, ~B, ~f, t, z))
1087
1088# Searches stop at the first decisive predicate; later elements are not tested.
1089def List.any.if(rest: Unit -> Bool, hit: Bool) -> Bool:
1090  match hit:
1091    case False{}:
1092      rest(Unit{})
1093    case True{}:
1094      True{}
1095
1096def List.any(~a: Quant, ~A: Kind(a), ~f: A -> Bool, xs: List<a, A>) -> Bool:
1097  match xs:
1098    case Nil{}:
1099      False{}
1100    case h <> t:
1101      List.any.if(u => List.any(~a, ~A, ~f, t), f(h))
1102
1103def List.all.if(rest: Unit -> Bool, hit: Bool) -> Bool:
1104  match hit:
1105    case False{}:
1106      False{}
1107    case True{}:
1108      rest(Unit{})
1109
1110def List.all(~a: Quant, ~A: Kind(a), ~f: A -> Bool, xs: List<a, A>) -> Bool:
1111  match xs:
1112    case Nil{}:
1113      True{}
1114    case h <> t:
1115      List.all.if(u => List.all(~a, ~A, ~f, t), f(h))
1116
1117def List.find.if(-A: Data, h: A, rest: Unit -> Maybe<&2, A>, hit: Bool) -> Maybe<&2, A>:
1118  match hit:
1119    case False{}:
1120      rest(Unit{})
1121    case True{}:
1122      Some{h}
1123
1124def List.find(~A: Data, ~f: A -> Bool, xs: List<&2, A>) -> Maybe<&2, A>:
1125  match xs:
1126    case Nil{}:
1127      None{}
1128    case +h <> t:
1129      List.find.if(A, h, u => List.find(~A, ~f, t), f(h))
1130
1131def List.contains(
1132  ~A: Data, ~eq: A -> A -> Bool, xs: List<&2, A>, +x: A
1133) -> Bool:
1134  match xs:
1135    case Nil{}:
1136      False{}
1137    case h <> t:
1138      List.any.if(u => List.contains(~A, ~eq, t, x), eq(h, x))
1139
1140def List.merge.step(
1141  -A: Data, acc: List<&2, A>, x: A, xt: List<&2, A>, y: A, yt: List<&2, A>,
1142  le: Bool
1143) -> List<&2, A> & List<&2, A> & List<&2, A>:
1144  match le:
1145    case False{}:
1146      (y <> acc, x <> xt, yt)
1147    case True{}:
1148      (x <> acc, xt, y <> yt)
1149
1150# The fuel bounds the steps: a sort passes its length, enough for any merge.
1151def List.merge.go(
1152  ~A: Data, ~le: A -> A -> Bool, fuel: Nat,
1153  st: List<&2, A> & List<&2, A> & List<&2, A>
1154) -> List<&2, A>:
1155  match fuel:
1156    case 0n:
1157      (acc, xs, ys) = st
1158      List.reverse.go(&2, A, acc, List.append(&2, A, xs, ys))
1159    case 1n+f:
1160      (acc, xs, ys) = st
1161      match xs ys:
1162        case Nil{} Nil{}:
1163          List.reverse.go(&2, A, acc, Nil{})
1164        case Nil{} y <> yt:
1165          List.reverse.go(&2, A, acc, y <> yt)
1166        case x <> xt Nil{}:
1167          List.reverse.go(&2, A, acc, x <> xt)
1168        case +x <> xt +y <> yt:
1169          List.merge.go(~A, ~le, f,
1170            List.merge.step(A, acc, x, xt, y, yt, le(x, y)))
1171
1172def List.sort.runs(-A: Data, xs: List<&2, A>) -> List<&2, List<&2, A>>:
1173  match xs:
1174    case Nil{}:
1175      Nil{}
1176    case h <> t:
1177      [h] <> List.sort.runs(A, t)
1178
1179def List.sort.pass(
1180  ~A: Data, ~le: A -> A -> Bool, +n: Nat, runs: List<&2, List<&2, A>>
1181) -> List<&2, List<&2, A>>:
1182  match runs:
1183    case Nil{}:
1184      Nil{}
1185    case r <> Nil{}:
1186      [r]
1187    case r1 <> r2 <> rest:
1188      List.merge.go(~A, ~le, n, (Nil{}, r1, r2))
1189        <> List.sort.pass(~A, ~le, n, rest)
1190
1191def List.sort.go(
1192  ~A: Data, ~le: A -> A -> Bool, fuel: Nat, +n: Nat, runs: List<&2, List<&2, A>>
1193) -> List<&2, A>:
1194  match fuel:
1195    case 0n:
1196      List.concat(&2, A, runs)
1197    case 1n+f:
1198      match runs:
1199        case Nil{}:
1200          Nil{}
1201        case r <> Nil{}:
1202          r
1203        case r1 <> r2 <> rest:
1204          List.sort.go(~A, ~le, f, n,
1205            List.sort.pass(~A, ~le, n, r1 <> r2 <> rest))
1206
1207def List.sort(~A: Data, ~le: A -> A -> Bool, xs: List<&2, A>) -> List<&2, A>:
1208  match xs:
1209    case Nil{}:
1210      Nil{}
1211    case h <> t:
1212      +ys = {h <> t : List<&2, A>}
1213      +n = List.length(&2, A, ys)
1214      List.sort.go(~A, ~le, n, n, List.sort.runs(A, ys))
1215
1216def List.for_each(
1217  ~a: Quant, ~A: Kind(a), ~f: A -> IO(Unit), xs: List<a, A>
1218) -> IO(Unit):
1219  match xs:
1220    case Nil{}:
1221      IO.pure(Unit, Unit{})
1222    case h <> t:
1223      IO.bind(Unit, Unit, f(h), u => List.for_each(~a, ~A, ~f, t))
1224
1225# Word
1226# ----
1227
1228def Word.zero(n: Nat) -> Word(n):
1229  match n:
1230    case 0n:
1231      WNil{}
1232    case 1n+p:
1233      WCon{False{}, Word.zero(p)}
1234
1235def Word.not(n: Nat, w: Word(n)) -> Word(n):
1236  match n:
1237    case 0n:
1238      WNil{}
1239    case 1n+p:
1240      match w:
1241        case WCon{b, t}:
1242          WCon{Bool.not(b), Word.not(p, t)}
1243
1244def Word.and(n: Nat, a: Word(n), b: Word(n)) -> Word(n):
1245  match n:
1246    case 0n:
1247      WNil{}
1248    case 1n+p:
1249      match a b:
1250        case WCon{ab, at} WCon{bb, bt}:
1251          WCon{Bool.and(ab, bb), Word.and(p, at, bt)}
1252
1253def Word.or(n: Nat, a: Word(n), b: Word(n)) -> Word(n):
1254  match n:
1255    case 0n:
1256      WNil{}
1257    case 1n+p:
1258      match a b:
1259        case WCon{ab, at} WCon{bb, bt}:
1260          WCon{Bool.or(ab, bb), Word.or(p, at, bt)}
1261
1262def Word.xor(n: Nat, a: Word(n), b: Word(n)) -> Word(n):
1263  match n:
1264    case 0n:
1265      WNil{}
1266    case 1n+p:
1267      match a b:
1268        case WCon{ab, at} WCon{bb, bt}:
1269          WCon{Bool.xor(ab, bb), Word.xor(p, at, bt)}
1270
1271def Word.shl.put(n: Nat, c: Bool, w: Word(n)) -> Word(n):
1272  match n:
1273    case 0n:
1274      WNil{}
1275    case 1n+p:
1276      match w:
1277        case WCon{b, t}:
1278          WCon{c, Word.shl.put(p, b, t)}
1279
1280def Word.shl(n: Nat, w: Word(n)) -> Word(n):
1281  match n:
1282    case 0n:
1283      WNil{}
1284    case 1n+p:
1285      match w:
1286        case WCon{b, t}:
1287          WCon{False{}, Word.shl.put(p, b, t)}
1288
1289def Word.shl.out.con(-p: Nat, c: Bool, r: Bool & Word(p)) -> Bool & Word(1n+p):
1290  (hi, t2) = r
1291  (hi, WCon{c, t2})
1292
1293def Word.shl.out(n: Nat, c: Bool, w: Word(n)) -> Bool & Word(n):
1294  match n:
1295    case 0n:
1296      (c, WNil{})
1297    case 1n+p:
1298      match w:
1299        case WCon{b, t}:
1300          Word.shl.out.con(p, c, Word.shl.out(p, b, t))
1301
1302def Word.shr.pad(n: Nat, w: Word(n)) -> Word(1n+n):
1303  match n:
1304    case 0n:
1305      WCon{False{}, w}
1306    case 1n+p:
1307      match w:
1308        case WCon{b, t}:
1309          WCon{b, Word.shr.pad(p, t)}
1310
1311def Word.shr(n: Nat, w: Word(n)) -> Word(n):
1312  match n:
1313    case 0n:
1314      WNil{}
1315    case 1n+p:
1316      match w:
1317        case WCon{b, t}:
1318          Word.shr.pad(p, t)
1319
1320def Word.cmp.fin(ab: Bool, bb: Bool, t: Cmp) -> Cmp:
1321  match t:
1322    case LT{}:
1323      LT{}
1324    case EQ{}:
1325      Bool.cmp(ab, bb)
1326    case GT{}:
1327      GT{}
1328
1329def Word.cmp(n: Nat, a: Word(n), b: Word(n)) -> Cmp:
1330  match n:
1331    case 0n:
1332      EQ{}
1333    case 1n+p:
1334      match a b:
1335        case WCon{ab, at} WCon{bb, bt}:
1336          Word.cmp.fin(ab, bb, Word.cmp(p, at, bt))
1337
1338def Word.inc(n: Nat, w: Word(n)) -> Word(n):
1339  match n:
1340    case 0n:
1341      WNil{}
1342    case 1n+p:
1343      match w:
1344        case WCon{False{}, t}:
1345          WCon{True{}, t}
1346        case WCon{True{}, t}:
1347          WCon{False{}, Word.inc(p, t)}
1348
1349law Word.adc:
1350  for n: Nat
1351  for a: Word(n)
1352  for b: Word(n)
1353  for f: Bool
1354  for c: Bool
1355  Word(n)
1356
1357def Word.adc.con(p: Nat, at: Word(p), bt: Word(p), f: Bool, sk: Bool & Bool) ->
1358  Word(1n+p):
1359  (s, k) = sk
1360  WCon{s, Word.adc(p, at, bt, f, k)}
1361
1362def Word.adc(n, a, b, f, c):
1363  match n:
1364    case 0n:
1365      WNil{}
1366    case 1n+p:
1367      match a b f:
1368        case WCon{ab, at} WCon{bb, bt} False{}:
1369          Word.adc.con(p, at, bt, False{}, Bool.full_add(ab, bb, c))
1370        case WCon{ab, at} WCon{bb, bt} True{}:
1371          Word.adc.con(p, at, bt, True{}, Bool.full_add(ab, Bool.not(bb), c))
1372
1373def Word.add(n: Nat, a: Word(n), b: Word(n)) -> Word(n):
1374  Word.adc(n, a, b, False{}, False{})
1375
1376def Word.sub(n: Nat, a: Word(n), b: Word(n)) -> Word(n):
1377  Word.adc(n, a, b, True{}, True{})
1378
1379law Word.add_comm.arm:
1380  for p  : Nat
1381  for at : Word(p)
1382  for bt : Word(p)
1383  for k  : Bool
1384  for -h : Bool
1385  {WCon{h, Word.adc(p, at, bt, False{}, k)}
1386    == WCon{h, Word.adc(p, bt, at, False{}, k)} : Word.Con<p>}
1387
1388law Word.add_comm.go:
1389  for n: Nat
1390  for a: Word(n)
1391  for b: Word(n)
1392  for c: Bool
1393  {Word.adc(n, a, b, False{}, c) == Word.adc(n, b, a, False{}, c) : Word(n)}
1394
1395def Word.add_comm.arm(p, at, bt, k, h):
1396  Equal.cong(Word(p), Word(1n+p), w => WCon{h, w},
1397    Word.adc(p, at, bt, False{}, k), Word.adc(p, bt, at, False{}, k),
1398    Word.add_comm.go(p, at, bt, k))
1399
1400def Word.add_comm.go(n, a, b, c):
1401  match n:
1402    case 0n:
1403      match a b:
1404        case WNil{} WNil{}:
1405          {==}
1406    case 1n+p:
1407      match a b c:
1408        case WCon{False{}, at} WCon{False{}, bt} False{}:
1409          Word.add_comm.arm(p, at, bt, False{}, False{})
1410        case WCon{False{}, at} WCon{False{}, bt} True{}:
1411          Word.add_comm.arm(p, at, bt, False{}, True{})
1412        case WCon{False{}, at} WCon{True{}, bt} False{}:
1413          Word.add_comm.arm(p, at, bt, False{}, True{})
1414        case WCon{False{}, at} WCon{True{}, bt} True{}:
1415          Word.add_comm.arm(p, at, bt, True{}, False{})
1416        case WCon{True{}, at} WCon{False{}, bt} False{}:
1417          Word.add_comm.arm(p, at, bt, False{}, True{})
1418        case WCon{True{}, at} WCon{False{}, bt} True{}:
1419          Word.add_comm.arm(p, at, bt, True{}, False{})
1420        case WCon{True{}, at} WCon{True{}, bt} False{}:
1421          Word.add_comm.arm(p, at, bt, True{}, False{})
1422        case WCon{True{}, at} WCon{True{}, bt} True{}:
1423          Word.add_comm.arm(p, at, bt, True{}, True{})
1424
1425law Word.add_comm:
1426  for n: Nat
1427  for a: Word(n)
1428  for b: Word(n)
1429  {Word.add(n, a, b) == Word.add(n, b, a) : Word(n)}
1430
1431def Word.add_comm(n, a, b):
1432  Word.add_comm.go(n, a, b, False{})
1433
1434def Word.to_nat(n: Nat, w: Word(n)) -> Nat:
1435  match n:
1436    case 0n:
1437      0n
1438    case 1n+p:
1439      match w:
1440        case WCon{False{}, t}:
1441          Nat.double(Word.to_nat(p, t))
1442        case WCon{True{}, t}:
1443          1n+Nat.double(Word.to_nat(p, t))
1444
1445def Word.mul.go(+n: Nat, m: Nat, a: Word(m), +b: Word(n), acc: Word(n)) ->
1446  Word(n):
1447  match m:
1448    case 0n:
1449      acc
1450    case 1n+mp:
1451      match a:
1452        case WCon{False{}, at}:
1453          Word.mul.go(n, mp, at, Word.shl(n, b), acc)
1454        case WCon{True{}, at}:
1455          Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))
1456
1457def Word.mul(+n: Nat, a: Word(n), b: Word(n)) -> Word(n):
1458  Word.mul.go(n, n, a, b, Word.zero(n))
1459
1460# U32
1461# ---
1462
1463def U32.inc(a: U32) -> U32:
1464  match a:
1465    case U32{x}:
1466      U32{Word.inc(32n, x)}
1467
1468def U32.add(a: U32, b: U32) -> U32:
1469  match a b:
1470    case U32{x} U32{y}:
1471      U32{Word.add(32n, x, y)}
1472
1473law U32.add_comm:
1474  for a: U32
1475  for b: U32
1476  {U32.add(a, b) == U32.add(b, a) : U32}
1477
1478def U32.add_comm(a, b):
1479  match a b:
1480    case U32{x} U32{y}:
1481      Equal.cong(Word(32n), U32, w => U32{w}, Word.add(32n, x, y),
1482        Word.add(32n, y, x), Word.add_comm(32n, x, y))
1483
1484def U32.sub(a: U32, b: U32) -> U32:
1485  match a b:
1486    case U32{x} U32{y}:
1487      U32{Word.sub(32n, x, y)}
1488
1489def U32.mul(a: U32, b: U32) -> U32:
1490  match a b:
1491    case U32{x} U32{y}:
1492      U32{Word.mul(32n, x, y)}
1493
1494def U32.not(a: U32) -> U32:
1495  match a:
1496    case U32{x}:
1497      U32{Word.not(32n, x)}
1498
1499def U32.and(a: U32, b: U32) -> U32:
1500  match a b:
1501    case U32{x} U32{y}:
1502      U32{Word.and(32n, x, y)}
1503
1504def U32.or(a: U32, b: U32) -> U32:
1505  match a b:
1506    case U32{x} U32{y}:
1507      U32{Word.or(32n, x, y)}
1508
1509def U32.xor(a: U32, b: U32) -> U32:
1510  match a b:
1511    case U32{x} U32{y}:
1512      U32{Word.xor(32n, x, y)}
1513
1514def U32.shl(a: U32) -> U32:
1515  match a:
1516    case U32{x}:
1517      U32{Word.shl(32n, x)}
1518
1519def U32.shr(a: U32) -> U32:
1520  match a:
1521    case U32{x}:
1522      U32{Word.shr(32n, x)}
1523
1524def U32.shln(a: U32, n: Nat) -> U32:
1525  match n:
1526    case 0n:
1527      a
1528    case 1n+p:
1529      U32.shl(U32.shln(a, p))
1530
1531def U32.shrn(a: U32, n: Nat) -> U32:
1532  match n:
1533    case 0n:
1534      a
1535    case 1n+p:
1536      U32.shr(U32.shrn(a, p))
1537
1538def U32.cmp(a: U32, b: U32) -> Cmp:
1539  match a b:
1540    case U32{x} U32{y}:
1541      Word.cmp(32n, x, y)
1542
1543def U32.is_eq(a: U32, b: U32) -> Bool:
1544  Cmp.is_eq(U32.cmp(a, b))
1545
1546def U32.is_ne(a: U32, b: U32) -> Bool:
1547  Bool.not(Cmp.is_eq(U32.cmp(a, b)))
1548
1549def U32.is_lt(a: U32, b: U32) -> Bool:
1550  Cmp.is_lt(U32.cmp(a, b))
1551
1552def U32.is_le(a: U32, b: U32) -> Bool:
1553  Cmp.is_le(U32.cmp(a, b))
1554
1555def U32.is_gt(a: U32, b: U32) -> Bool:
1556  Cmp.is_gt(U32.cmp(a, b))
1557
1558def U32.is_ge(a: U32, b: U32) -> Bool:
1559  Cmp.is_ge(U32.cmp(a, b))
1560
1561def U32.is_zero(a: U32) -> Bool:
1562  U32.is_eq(a, 0)
1563
1564def U32.to_nat(a: U32) -> Nat:
1565  match a:
1566    case U32{w}:
1567      Word.to_nat(32n, w)
1568
1569def U32.from_nat(n: Nat) -> U32:
1570  match n:
1571    case 0n:
1572      0
1573    case 1n+p:
1574      U32.inc(U32.from_nat(p))
1575
1576def U32.log2.go(+k: Nat, +n: U32, b: Nat) -> Nat:
1577  match k:
1578    case 0n:
1579      b
1580    case 1n+p:
1581      +s = U32.to_nat(U32.shln(1, p))
1582      +t = Nat.mul(s, U32.to_nat(Bool.to_u32(U32.is_ne(U32.shrn(n, s), 0))))
1583      U32.log2.go(p, U32.shrn(n, t), Nat.add(b, t))
1584
1585def U32.log2(n: U32) -> Nat:
1586  U32.log2.go(5n, n, 0n)
1587
1588def U32.divmod.go.fin(-p: Nat, q: Word(p), s: U32, b: U32, g: Bool) ->
1589  Word(1n+p) & U32:
1590  match g:
1591    case True{}:
1592      (WCon{True{}, q}, U32.sub(s, b))
1593    case False{}:
1594      (WCon{False{}, q}, s)
1595
1596def U32.divmod.go.shl(-p: Nat, q: Word(p), +b: U32, ts: Bool & Word(32n)) ->
1597  Word(1n+p) & U32:
1598  (t, s) = ts
1599  +s2 = {U32{s} : U32}
1600  U32.divmod.go.fin(p, q, s2, b, Bool.or(t, U32.is_ge(s2, b)))
1601
1602def U32.divmod.go.rec(-p: Nat, a0: Bool, +b: U32, qr: Word(p) & U32) ->
1603  Word(1n+p) & U32:
1604  (q, r) = qr
1605  U32{rw} = r
1606  U32.divmod.go.shl(p, q, b, Word.shl.out(32n, a0, rw))
1607
1608def U32.divmod.go(m: Nat, a: Word(m), +b: U32) -> Word(m) & U32:
1609  match m a:
1610    case 0n WNil{}:
1611      (WNil{}, 0)
1612    case 1n+p WCon{a0, hi}:
1613      U32.divmod.go.rec(p, a0, b, U32.divmod.go(p, hi, b))
1614
1615def U32.div.fin(qr: Word(32n) & U32) -> U32:
1616  (q, r) = qr
1617  U32{q}
1618
1619def U32.div.if(aw: Word(32n), b: U32, z: Bool) -> U32:
1620  match z:
1621    case True{}:
1622      0
1623    case False{}:
1624      U32.div.fin(U32.divmod.go(32n, aw, b))
1625
1626def U32.div(a: U32, b: U32) -> U32:
1627  U32{aw} = a
1628  U32{+bw} = b
1629  U32.div.if(aw, U32{bw}, U32.is_zero(U32{bw}))
1630
1631def U32.mod.fin(qr: Word(32n) & U32) -> U32:
1632  (q, r) = qr
1633  r
1634
1635def U32.mod.if(aw: Word(32n), b: U32, z: Bool) -> U32:
1636  match z:
1637    case True{}:
1638      U32{aw}
1639    case False{}:
1640      U32.mod.fin(U32.divmod.go(32n, aw, b))
1641
1642def U32.mod(a: U32, b: U32) -> U32:
1643  U32{aw} = a
1644  U32{+bw} = b
1645  U32.mod.if(aw, U32{bw}, U32.is_zero(U32{bw}))
1646
1647def U32.min(a: U32, b: U32) -> U32:
1648  match a b:
1649    case U32{+x} U32{+y}:
1650      Bool.pick(U32, U32.is_lt(U32{x}, U32{y}), U32{x}, U32{y})
1651
1652def U32.max(a: U32, b: U32) -> U32:
1653  match a b:
1654    case U32{+x} U32{+y}:
1655      Bool.pick(U32, U32.is_lt(U32{x}, U32{y}), U32{y}, U32{x})
1656
1657def U32.clamp(x: U32, lo: U32, hi: U32) -> U32:
1658  U32.min(U32.max(x, lo), hi)
1659
1660def U32.pow(+a: U32, n: Nat) -> U32:
1661  match n:
1662    case 0n:
1663      1
1664    case 1n+p:
1665      U32.mul(a, U32.pow(a, p))
1666
1667def U32.is_even(a: U32) -> Bool:
1668  U32.is_zero(U32.and(a, 1))
1669
1670# F32
1671# ---
1672
1673law U32.to_f32:
1674  for a: U32
1675  F32
1676
1677law F32.to_u32:
1678  for a: F32
1679  U32
1680
1681law F32.add:
1682  for a: F32
1683  for b: F32
1684  F32
1685
1686law F32.sub:
1687  for a: F32
1688  for b: F32
1689  F32
1690
1691law F32.mul:
1692  for a: F32
1693  for b: F32
1694  F32
1695
1696law F32.div:
1697  for a: F32
1698  for b: F32
1699  F32
1700
1701law F32.mod:
1702  for a: F32
1703  for b: F32
1704  F32
1705
1706law F32.pow:
1707  for a: F32
1708  for b: F32
1709  F32
1710
1711law F32.atan2:
1712  for a: F32
1713  for b: F32
1714  F32
1715
1716law F32.neg:
1717  for a: F32
1718  F32
1719
1720law F32.abs:
1721  for a: F32
1722  F32
1723
1724law F32.sqrt:
1725  for a: F32
1726  F32
1727
1728law F32.exp:
1729  for a: F32
1730  F32
1731
1732law F32.log:
1733  for a: F32
1734  F32
1735
1736law F32.log2:
1737  for a: F32
1738  F32
1739
1740law F32.log10:
1741  for a: F32
1742  F32
1743
1744law F32.sin:
1745  for a: F32
1746  F32
1747
1748law F32.cos:
1749  for a: F32
1750  F32
1751
1752law F32.tan:
1753  for a: F32
1754  F32
1755
1756law F32.asin:
1757  for a: F32
1758  F32
1759
1760law F32.acos:
1761  for a: F32
1762  F32
1763
1764law F32.atan:
1765  for a: F32
1766  F32
1767
1768law F32.sinh:
1769  for a: F32
1770  F32
1771
1772law F32.cosh:
1773  for a: F32
1774  F32
1775
1776law F32.tanh:
1777  for a: F32
1778  F32
1779
1780law F32.floor:
1781  for a: F32
1782  F32
1783
1784law F32.ceil:
1785  for a: F32
1786  F32
1787
1788law F32.trunc:
1789  for a: F32
1790  F32
1791
1792law F32.is_eq:
1793  for a: F32
1794  for b: F32
1795  Bool
1796
1797law F32.is_ne:
1798  for a: F32
1799  for b: F32
1800  Bool
1801
1802law F32.is_lt:
1803  for a: F32
1804  for b: F32
1805  Bool
1806
1807law F32.is_le:
1808  for a: F32
1809  for b: F32
1810  Bool
1811
1812law F32.is_gt:
1813  for a: F32
1814  for b: F32
1815  Bool
1816
1817law F32.is_ge:
1818  for a: F32
1819  for b: F32
1820  Bool
1821
1822law F32.show:
1823  for a: F32
1824  String
1825
1826law F32.bits:
1827  for a: F32
1828  U32
1829
1830law F32.read:
1831  for s: String
1832  Maybe<&2, F32>
1833
1834def F32.min(a: F32, b: F32) -> F32:
1835  match a b:
1836    case F32{+x} F32{+y}:
1837      Bool.pick(F32, F32.is_lt(F32{x}, F32{y}), F32{x}, F32{y})
1838
1839def F32.max(a: F32, b: F32) -> F32:
1840  match a b:
1841    case F32{+x} F32{+y}:
1842      Bool.pick(F32, F32.is_lt(F32{x}, F32{y}), F32{y}, F32{x})
1843
1844def F32.clamp(x: F32, lo: F32, hi: F32) -> F32:
1845  F32.min(F32.max(x, lo), hi)
1846
1847# At t = 0 and t = 1 return that endpoint as is, keeping signed zero and never
1848# multiplying the other one (an infinite endpoint would give NaN). Between them
1849# the weighted sum avoids overflowing b - a for finite endpoints of opposite
1850# signs.
1851def F32.lerp(a: F32, b: F32, t: F32) -> F32:
1852  match t:
1853    case F32{+z}:
1854      F32.lerp.zero(a, b, F32{z}, F32.is_eq(F32{z}, 0.0))
1855
1856def F32.lerp.zero(a: F32, b: F32, +t: F32, zero: Bool) -> F32:
1857  match zero:
1858    case True{}:
1859      a
1860    case False{}:
1861      F32.lerp.one(a, b, t, F32.is_eq(t, 1.0))
1862
1863def F32.lerp.one(a: F32, b: F32, +t: F32, one: Bool) -> F32:
1864  match one:
1865    case True{}:
1866      b
1867    case False{}:
1868      F32.add(F32.mul(a, F32.sub(1.0, t)), F32.mul(b, t))
1869
1870def F32.square(a: F32) -> F32:
1871  match a:
1872    case F32{+x}:
1873      F32.mul(F32{x}, F32{x})
1874
1875# Outside [2^-60, 2^60] the squares would overflow or underflow, so scale
1876# both sides by a power of two first; inside, the scale is 1 and exact.
1877def F32.hypot(a: F32, b: F32) -> F32:
1878  +x = F32.abs(a)
1879  +y = F32.abs(b)
1880  +m = F32.max(x, y)
1881  +hi = F32.is_gt(m, 1.152921504606847e18)
1882  +lo = F32.is_lt(m, 8.673617379884035e-19)
1883  +s = Bool.pick(F32, hi, 8.470329472543003e-22,
1884    Bool.pick(F32, lo, 1.2676506002282294e30, 1.0))
1885  +u = Bool.pick(F32, hi, 1.1805916207174113e21,
1886    Bool.pick(F32, lo, 7.888609052210118e-31, 1.0))
1887  +p = F32.mul(x, s)
1888  +q = F32.mul(y, s)
1889  F32.mul(F32.sqrt(F32.add(F32.mul(p, p), F32.mul(q, q))), u)
1890
1891# A rounded zero keeps the input sign, including at the negative half.
1892def F32.round.zero(a: F32, r: F32, zero: Bool) -> F32:
1893  match zero:
1894    case True{}:
1895      F32.mul(a, 0.0)
1896    case False{}:
1897      r
1898
1899def F32.round(a: F32) -> F32:
1900  match a:
1901    case F32{+x}:
1902      +f = F32.floor(F32{x})
1903      +r = F32.add(f, Bool.pick(F32, F32.is_ge(F32.sub(F32{x}, f), 0.5), 1.0, 0.0))
1904      F32.round.zero(F32{x}, r, F32.is_eq(r, 0.0))
1905
1906def F32.pi() -> F32:
1907  3.14159265
1908
1909def F32.from_nat(n: Nat) -> F32:
1910  U32.to_f32(U32.from_nat(n))
1911
1912# Preserve the direct cast below 2^32; wider Nats need both word halves.
1913# Past 2^48-1 no Nat fits, so the direct cast gives 0.
1914def F32.to_nat.wide(+a: F32, wide: Bool) -> Nat:
1915  match wide:
1916    case False{}:
1917      U32.to_nat(F32.to_u32(a))
1918    case True{}:
1919      +hi = U32.to_nat(F32.to_u32(F32.div(a, 4294967296.0)))
1920      +lo = U32.to_nat(F32.to_u32(F32.mod(a, 4294967296.0)))
1921      Nat.add(Nat.mul(hi, Nat.mul(65536n, 65536n)), lo)
1922
1923def F32.to_nat(a: F32) -> Nat:
1924  match a:
1925    case F32{+x}:
1926      +wide = Bool.and(F32.is_ge(F32{x}, 4294967296.0),
1927        F32.is_lt(F32{x}, 281474976710656.0))
1928      F32.to_nat.wide(F32{x}, wide)
1929
1930# Char
1931# ----
1932
1933def Char.cmp(a: Char, b: Char) -> (Char & Char) & Cmp:
1934  match a b:
1935    case Chr{+x} Chr{+y}:
1936      ((Chr{x}, Chr{y}), U32.cmp(x, y))
1937
1938def Char.to_u32(c: Char) -> U32:
1939  match c:
1940    case Chr{x}:
1941      x
1942
1943def Char.from_u32(x: U32) -> Char:
1944  Chr{x}
1945
1946def Char.is_eq(a: Char, b: Char) -> Bool:
1947  match a b:
1948    case Chr{x} Chr{y}:
1949      U32.is_eq(x, y)
1950
1951def Char.is_digit(c: Char) -> Bool:
1952  match c:
1953    case Chr{+x}:
1954      Bool.and(U32.is_ge(x, 48), U32.is_le(x, 57))
1955
1956def Char.is_upper(c: Char) -> Bool:
1957  match c:
1958    case Chr{+x}:
1959      Bool.and(U32.is_ge(x, 65), U32.is_le(x, 90))
1960
1961def Char.is_lower(c: Char) -> Bool:
1962  match c:
1963    case Chr{+x}:
1964      Bool.and(U32.is_ge(x, 97), U32.is_le(x, 122))
1965
1966def Char.is_alpha(+c: Char) -> Bool:
1967  Bool.or(Char.is_upper(c), Char.is_lower(c))
1968
1969def Char.is_space(c: Char) -> Bool:
1970  match c:
1971    case Chr{+x}:
1972      Bool.or(U32.is_eq(x, 32), Bool.and(U32.is_ge(x, 9), U32.is_le(x, 13)))
1973
1974def Char.to_upper(c: Char) -> Char:
1975  match c:
1976    case Chr{+x}:
1977      Chr{U32.sub(x, U32.mul(Bool.to_u32(Char.is_lower(Chr{x})), 32))}
1978
1979def Char.to_lower(c: Char) -> Char:
1980  match c:
1981    case Chr{+x}:
1982      Chr{U32.add(x, U32.mul(Bool.to_u32(Char.is_upper(Chr{x})), 32))}
1983
1984# String
1985# ------
1986
1987def String.append(a: String, b: String) -> String:
1988  match a:
1989    case SNil{}:
1990      b
1991    case SCon{h, t}:
1992      SCon{h, String.append(t, b)}
1993
1994def String.cmp.rec(h1b: Char, h2b: Char, rr: (String & String) & Cmp) ->
1995  (String & String) & Cmp:
1996  ((t1b, t2b), r) = rr
1997  ((SCon{h1b, t1b}, SCon{h2b, t2b}), r)
1998
1999law String.cmp:
2000  for a: String
2001  for b: String
2002  (String & String) & Cmp
2003
2004def String.cmp.fin(t1: String, t2: String, hc: (Char & Char) & Cmp) ->
2005  (String & String) & Cmp:
2006  ((h1b, h2b), c) = hc
2007  match c:
2008    case LT{}:
2009      ((SCon{h1b, t1}, SCon{h2b, t2}), LT{})
2010    case EQ{}:
2011      String.cmp.rec(h1b, h2b, String.cmp(t1, t2))
2012    case GT{}:
2013      ((SCon{h1b, t1}, SCon{h2b, t2}), GT{})
2014
2015def String.cmp(a, b):
2016  match a b:
2017    case SNil{} SNil{}:
2018      ((SNil{}, SNil{}), EQ{})
2019    case SNil{} SCon{h, t}:
2020      ((SNil{}, SCon{h, t}), LT{})
2021    case SCon{h, t} SNil{}:
2022      ((SCon{h, t}, SNil{}), GT{})
2023    case SCon{h1, t1} SCon{h2, t2}:
2024      String.cmp.fin(t1, t2, Char.cmp(h1, h2))
2025
2026def String.eq(a: String, b: String) -> Bool:
2027  Cmp.is_eq(String.order(a, b))
2028
2029def String.length(s: String) -> Nat:
2030  match s:
2031    case SNil{}:
2032      0n
2033    case SCon{h, t}:
2034      1n+String.length(t)
2035
2036def String.is_empty(s: String) -> Bool:
2037  match s:
2038    case SNil{}:
2039      True{}
2040    case SCon{h, t}:
2041      False{}
2042
2043def String.reverse.go(s: String, acc: String) -> String:
2044  match s:
2045    case SNil{}:
2046      acc
2047    case SCon{h, t}:
2048      String.reverse.go(t, SCon{h, acc})
2049
2050def String.reverse(s: String) -> String:
2051  String.reverse.go(s, SNil{})
2052
2053# c is the order of the chars so far: the walk is one tail call per char
2054# and builds nothing (String.cmp rebuilds both strings for its callers).
2055def String.order.go(a: String, b: String, c: Cmp) -> Cmp:
2056  match a b c:
2057    case SNil{} SCon{h, t} EQ{}:
2058      LT{}
2059    case SCon{h, t} SNil{} EQ{}:
2060      GT{}
2061    case SCon{Chr{x}, t1} SCon{Chr{y}, t2} EQ{}:
2062      String.order.go(t1, t2, U32.cmp(x, y))
2063    case _ _ o:
2064      o
2065
2066def String.order(a: String, b: String) -> Cmp:
2067  String.order.go(a, b, EQ{})
2068
2069def String.is_lt(a: String, b: String) -> Bool:
2070  Cmp.is_lt(String.order(a, b))
2071
2072def String.is_le(a: String, b: String) -> Bool:
2073  Cmp.is_le(String.order(a, b))
2074
2075def String.is_gt(a: String, b: String) -> Bool:
2076  Cmp.is_gt(String.order(a, b))
2077
2078def String.is_ge(a: String, b: String) -> Bool:
2079  Cmp.is_ge(String.order(a, b))
2080
2081law String.starts_with:
2082  for s: String
2083  for p: String
2084  Bool
2085
2086law String.starts_with.go:
2087  for p: String
2088  for s: String
2089  Bool
2090
2091def String.starts_with.go.if(pt: String, t: String, same: Bool) -> Bool:
2092  match same:
2093    case False{}:
2094      False{}
2095    case True{}:
2096      String.starts_with.go(pt, t)
2097
2098# Match the prefix first so an exhausted prefix never inspects the tail.
2099def String.starts_with.go(p, s):
2100  match p s:
2101    case SNil{} _:
2102      True{}
2103    case SCon{y, yt} SNil{}:
2104      False{}
2105    case SCon{y, yt} SCon{x, xt}:
2106      String.starts_with.go.if(yt, xt, Char.is_eq(x, y))
2107
2108def String.starts_with(s, p):
2109  String.starts_with.go(p, s)
2110
2111def String.ends_with(s: String, p: String) -> Bool:
2112  String.starts_with(String.reverse(s), String.reverse(p))
2113
2114law String.contains:
2115  for +s: String
2116  for +p: String
2117  Bool
2118
2119def String.contains.if(t: String, p: String, here: Bool) -> Bool:
2120  match here:
2121    case False{}:
2122      String.contains(t, p)
2123    case True{}:
2124      True{}
2125
2126def String.contains(s, p):
2127  match s:
2128    case SNil{}:
2129      String.is_empty(p)
2130    case SCon{h, t}:
2131      String.contains.if(t, p, String.starts_with(SCon{h, t}, p))
2132
2133def String.take(s: String, n: Nat) -> String:
2134  match s n:
2135    case SNil{} _:
2136      SNil{}
2137    case SCon{h, t} 0n:
2138      SNil{}
2139    case SCon{h, t} 1n+p:
2140      SCon{h, String.take(t, p)}
2141
2142def String.drop(s: String, n: Nat) -> String:
2143  match s n:
2144    case SNil{} _:
2145      SNil{}
2146    case SCon{h, t} 0n:
2147      SCon{h, t}
2148    case SCon{h, t} 1n+p:
2149      String.drop(t, p)
2150
2151def String.get(s: String, n: Nat) -> Maybe<&2, Char>:
2152  match s n:
2153    case SNil{} _:
2154      None{}
2155    case SCon{h, t} 0n:
2156      Some{h}
2157    case SCon{h, t} 1n+p:
2158      String.get(t, p)
2159
2160def String.to_list(s: String) -> List<&2, Char>:
2161  match s:
2162    case SNil{}:
2163      Nil{}
2164    case SCon{h, t}:
2165      h <> String.to_list(t)
2166
2167def String.from_list(cs: List<&2, Char>) -> String:
2168  match cs:
2169    case Nil{}:
2170      SNil{}
2171    case h <> t:
2172      SCon{h, String.from_list(t)}
2173
2174def String.concat(xs: List<&2, String>) -> String:
2175  match xs:
2176    case Nil{}:
2177      SNil{}
2178    case h <> t:
2179      String.append(h, String.concat(t))
2180
2181def String.join.go(xs: List<&2, String>, h: String, +sep: String) -> String:
2182  match xs:
2183    case Nil{}:
2184      h
2185    case h2 <> t:
2186      String.append(h, String.append(sep, String.join.go(t, h2, sep)))
2187
2188def String.join(xs: List<&2, String>, +sep: String) -> String:
2189  match xs:
2190    case Nil{}:
2191      SNil{}
2192    case h <> t:
2193      String.join.go(t, h, sep)
2194
2195def String.split.push(c: Char, ps: List<&2, String>) -> List<&2, String>:
2196  match ps:
2197    case Nil{}:
2198      [SCon{c, SNil{}}]
2199    case h <> t:
2200      SCon{c, h} <> t
2201
2202def String.split.fin(c: Char, r: List<&2, String>, cut: Bool) ->
2203  List<&2, String>:
2204  match cut:
2205    case False{}:
2206      String.split.push(c, r)
2207    case True{}:
2208      SNil{} <> r
2209
2210def String.split(s: String, +sep: Char) -> List<&2, String>:
2211  match s:
2212    case SNil{}:
2213      [SNil{}]
2214    case SCon{+h, t}:
2215      String.split.fin(h, String.split(t, sep), Char.is_eq(h, sep))
2216
2217def String.lines(s: String) -> List<&2, String>:
2218  String.split(s, '\n')
2219
2220def String.repeat(+s: String, n: Nat) -> String:
2221  match n:
2222    case 0n:
2223      SNil{}
2224    case 1n+p:
2225      String.append(s, String.repeat(s, p))
2226
2227def String.to_upper(s: String) -> String:
2228  match s:
2229    case SNil{}:
2230      SNil{}
2231    case SCon{h, t}:
2232      SCon{Char.to_upper(h), String.to_upper(t)}
2233
2234def String.to_lower(s: String) -> String:
2235  match s:
2236    case SNil{}:
2237      SNil{}
2238    case SCon{h, t}:
2239      SCon{Char.to_lower(h), String.to_lower(t)}
2240
2241law String.trim_start:
2242  for s: String
2243  String
2244
2245def String.trim_start.if(t: String, h: Char, space: Bool) -> String:
2246  match space:
2247    case False{}:
2248      SCon{h, t}
2249    case True{}:
2250      String.trim_start(t)
2251
2252def String.trim_start(s):
2253  match s:
2254    case SNil{}:
2255      SNil{}
2256    case SCon{+h, t}:
2257      String.trim_start.if(t, h, Char.is_space(h))
2258
2259def String.trim_end(s: String) -> String:
2260  String.reverse(String.trim_start(String.reverse(s)))
2261
2262def String.trim(s: String) -> String:
2263  String.trim_end(String.trim_start(s))
2264
2265# Text
2266# ----
2267
2268def Nat.show.put(qr: Nat & Nat) -> Char & Nat:
2269  (q, r) = qr
2270  (Chr{U32.from_nat(Nat.add(48n, r))}, q)
2271
2272law Nat.show.go:
2273  for f   : Nat
2274  for n   : Nat
2275  for acc : String
2276  String
2277
2278def Nat.show.fin(g: Nat, acc: String, dq: Char & Nat) -> String:
2279  (d, q) = dq
2280  match q:
2281    case 0n:
2282      SCon{d, acc}
2283    case 1n+p:
2284      Nat.show.go(g, 1n+p, SCon{d, acc})
2285
2286def Nat.show.go(f, n, acc):
2287  match f:
2288    case 0n:
2289      acc
2290    case 1n+g:
2291      Nat.show.fin(g, acc, Nat.show.put(Nat.divmod(n, 10n)))
2292
2293def Nat.show(n: Nat) -> String:
2294  +m = n
2295  Nat.show.fin(m, SNil{}, Nat.show.put(Nat.divmod(m, 10n)))
2296
2297law Nat.read.go:
2298  for s   : String
2299  for +acc : Nat
2300  Maybe<&2, Nat>
2301
2302def Nat.read.if(t: String, acc: Nat, d: U32, ok: Bool) -> Maybe<&2, Nat>:
2303  match ok:
2304    case True{}:
2305      Nat.read.go(t, Nat.add(Nat.mul(acc, 10n), U32.to_nat(d)))
2306    case False{}:
2307      None{}
2308
2309def Nat.read.go(s, acc):
2310  match s:
2311    case SNil{}:
2312      Some{acc}
2313    case SCon{Chr{x}, t}:
2314      +d = U32.sub(x, 48)
2315      Nat.read.if(t, acc, d, U32.is_lt(d, 10))
2316
2317# 2^48-1 is the text 281474976710655. Past leading zeros, fewer than
2318# fifteen characters fit, more do not, and fifteen compare as text;
2319# Nat.read.go still refuses a non-digit. The gate is a def, not a
2320# Bool.pick: an argument is built before the call, and reading a string
2321# that does not fit would build a Nat past the bound. A law that reads
2322# "7" never builds the unary nat (each digit once divided it).
2323def Nat.read.trim(s: String) -> String:
2324  match s:
2325    case SCon{'0', t}:
2326      Nat.read.trim(t)
2327    case t:
2328      t
2329
2330def Nat.read.fits(+s: String) -> Bool:
2331  +n = String.length(s)
2332  Bool.or(Nat.is_lt(n, 15n),
2333    Bool.and(Nat.is_eq(n, 15n), String.is_le(s, "281474976710655")))
2334
2335def Nat.read.gate(+s: String, ok: Bool) -> Maybe<&2, Nat>:
2336  match ok:
2337    case True{}:
2338      Nat.read.go(s, 0n)
2339    case False{}:
2340      None{}
2341
2342def Nat.read(s: String) -> Maybe<&2, Nat>:
2343  match s:
2344    case SNil{}:
2345      None{}
2346    case SCon{h, t}:
2347      +u = Nat.read.trim(SCon{h, t})
2348      Nat.read.gate(u, Nat.read.fits(u))
2349
2350law U32.show.go:
2351  for f   : Nat
2352  for +n  : U32
2353  for acc : String
2354  String
2355
2356def U32.show.fin(g: Nat, acc: String, +n: U32, z: Bool) -> String:
2357  match z:
2358    case True{}:
2359      acc
2360    case False{}:
2361      U32.show.go(g, U32.div(n, 10),
2362        SCon{Chr{U32.add(48, U32.mod(n, 10))}, acc})
2363
2364def U32.show.go(f, n, acc):
2365  match f:
2366    case 0n:
2367      acc
2368    case 1n+g:
2369      U32.show.fin(g, acc, n, U32.is_zero(n))
2370
2371def U32.show.if(a: U32, z: Bool) -> String:
2372  match z:
2373    case True{}:
2374      SCon{Chr{48}, SNil{}}
2375    case False{}:
2376      U32.show.go(10n, a, SNil{})
2377
2378def U32.show(a: U32) -> String:
2379  +b = a
2380  U32.show.if(b, U32.is_zero(b))
2381
2382law U32.read.go:
2383  for s   : String
2384  for +acc : U32
2385  Maybe<&2, U32>
2386
2387def U32.read.if(t: String, n: U32, ok: Bool) -> Maybe<&2, U32>:
2388  match ok:
2389    case True{}:
2390      U32.read.go(t, n)
2391    case False{}:
2392      None{}
2393
2394def U32.read.go(s, acc):
2395  match s:
2396    case SNil{}:
2397      Some{acc}
2398    case SCon{Chr{x}, t}:
2399      +n = U32.add(U32.mul(acc, 10), U32.sub(x, 48))
2400      U32.read.if(t, n, U32.is_eq(U32.div(n, 10), acc))
2401
2402def U32.read(s: String) -> Maybe<&2, U32>:
2403  match s:
2404    case SNil{}:
2405      None{}
2406    case SCon{h, t}:
2407      U32.read.go(SCon{h, t}, 0)
2408
2409def Bool.show(b: Bool) -> String:
2410  match b:
2411    case False{}:
2412      "False"
2413    case True{}:
2414      "True"
2415
2416def Char.show(c: Char) -> String:
2417  SCon{c, SNil{}}
2418
2419def Maybe.show(~a: Quant, ~A: Kind(a), ~f: A -> String, m: Maybe<a, A>) ->
2420  String:
2421  match m:
2422    case None{}:
2423      "None"
2424    case Some{x}:
2425      "Some(" ++ f(x) ++ ")"
2426
2427def List.show.go(~a: Quant, ~A: Kind(a), ~f: A -> String, xs: List<a, A>) ->
2428  String:
2429  match xs:
2430    case Nil{}:
2431      "]"
2432    case h <> t:
2433      ", " ++ f(h) ++ List.show.go(~a, ~A, ~f, t)
2434
2435def List.show(~a: Quant, ~A: Kind(a), ~f: A -> String, xs: List<a, A>) ->
2436  String:
2437  match xs:
2438    case Nil{}:
2439      "[]"
2440    case h <> t:
2441      "[" ++ f(h) ++ List.show.go(~a, ~A, ~f, t)
2442
2443# Array
2444# -----
2445
2446def Array.size.node(-T: Type, ys: Array<T>, r: Array<T> & U32) ->
2447  Array<T> & U32:
2448  (xs2, n) = r
2449  (ANode{xs2, ys}, U32.shl(n))
2450
2451def Array.size(-T: Type, a: Array<T>) -> Array<T> & U32:
2452  match a:
2453    case ALeaf{x}:
2454      (ALeaf{x}, 1)
2455    case ANode{xs, ys}:
2456      Array.size.node(T, ys, Array.size(T, xs))
2457
2458def Array.swap.lo(-T: Type, ys: Array<T>, r: Array<T> & T) -> Array<T> & T:
2459  (nxs, old) = r
2460  (ANode{nxs, ys}, old)
2461
2462def Array.swap.hi(-T: Type, xs: Array<T>, r: Array<T> & T) -> Array<T> & T:
2463  (nys, old) = r
2464  (ANode{xs, nys}, old)
2465
2466# the recursion descends into a subtree, and z says which: the caller
2467# computes it from the index and the subtree's half size
2468def Array.swap.go(-T: Type, a: Array<T>, n: U32, +i: U32, v: T, z: Bool) -> Array<T> & T:
2469  match a z:
2470    case ALeaf{x} _:
2471      (ALeaf{v}, x)
2472    case ANode{xs, ys} True{}:
2473      +h = U32.shr(n)
2474      Array.swap.lo(T, ys, Array.swap.go(T, xs, h, i, v, U32.is_lt(i, U32.shr(h))))
2475    case ANode{xs, ys} False{}:
2476      +h = U32.shr(n)
2477      +j = U32.sub(i, h)
2478      Array.swap.hi(T, xs, Array.swap.go(T, ys, h, j, v, U32.is_lt(j, U32.shr(h))))
2479
2480def Array.swap.at(-T: Type, i: U32, v: T, an: Array<T> & U32) -> Array<T> & T:
2481  (a, +n) = an
2482  +j = U32.and(i, U32.sub(n, 1))
2483  Array.swap.go(T, a, n, j, v, U32.is_lt(j, U32.shr(n)))
2484
2485def Array.swap(-T: Type, a: Array<T>, +i: U32, v: T) -> Array<T> & T:
2486  Array.swap.at(T, i, v, Array.size(T, a))
2487
2488def Array.clone.node(
2489  -T: Data, cx: Array<T> & Array<T>, cy: Array<T> & Array<T>
2490) -> Array<T> & Array<T>:
2491  (xa, xb) = cx
2492  (ya, yb) = cy
2493  (ANode{xa, ya}, ANode{xb, yb})
2494
2495def Array.clone(-T: Data, a: Array<T>) -> Array<T> & Array<T>:
2496  match a:
2497    case ALeaf{+x}:
2498      (ALeaf{x}, ALeaf{x})
2499    case ANode{xs, ys}:
2500      Array.clone.node(T, Array.clone(T, xs), Array.clone(T, ys))
2501
2502# A fork is two handles to one array in O(1). Both read and write the
2503# same cells, so racing writes go through the atomics; a match on a
2504# handle copies its part, as a clone does. An atomic takes an Array<U32>
2505# (fadd an Array<F32>) and returns the array with the old value.
2506
2507@unsafe
2508def Array.fork(-T: Type, +a: Array<T>) -> Array<T> & Array<T>:
2509  (a, a)
2510
2511@unsafe
2512def Array.join(-T: Type, a: Array<T>, b: Array<T>) -> Array<T>:
2513  a
2514
2515law Array.atomic.add:
2516  for  a: Array<U32>
2517  for +i: U32
2518  for +v: U32
2519  Array<U32> & U32
2520
2521law Array.atomic.min:
2522  for  a: Array<U32>
2523  for +i: U32
2524  for +v: U32
2525  Array<U32> & U32
2526
2527law Array.atomic.max:
2528  for  a: Array<U32>
2529  for +i: U32
2530  for +v: U32
2531  Array<U32> & U32
2532
2533law Array.atomic.and:
2534  for  a: Array<U32>
2535  for +i: U32
2536  for +v: U32
2537  Array<U32> & U32
2538
2539law Array.atomic.or:
2540  for  a: Array<U32>
2541  for +i: U32
2542  for +v: U32
2543  Array<U32> & U32
2544
2545law Array.atomic.xor:
2546  for  a: Array<U32>
2547  for +i: U32
2548  for +v: U32
2549  Array<U32> & U32
2550
2551law Array.atomic.exch:
2552  for  a: Array<U32>
2553  for +i: U32
2554  for +v: U32
2555  Array<U32> & U32
2556
2557law Array.atomic.cas:
2558  for  a: Array<U32>
2559  for +i: U32
2560  for +x: U32
2561  for +v: U32
2562  Array<U32> & U32
2563
2564law Array.atomic.fadd:
2565  for  a: Array<F32>
2566  for +i: U32
2567  for +v: F32
2568  Array<F32> & F32
2569
2570def Array.new(-T: Data, +d: Nat, +v: T) -> Array<T>:
2571  match d:
2572    case 0n:
2573      ALeaf{v}
2574    case 1n+p:
2575      ANode{[v : T^p], [v : T^p]}
2576
2577def Array.set.fin(-T: Type, r: Array<T> & T) -> Array<T>:
2578  (na, old) = r
2579  na
2580
2581def Array.set(-T: Type, a: Array<T>, i: U32, v: T) -> Array<T>:
2582  Array.set.fin(T, Array.swap(T, a, i, v))
2583
2584def Array.get.go(-T: Data, a: Array<T>, n: U32, +i: U32, z: Bool) -> Array<T> & T:
2585  match a z:
2586    case ALeaf{+x} _:
2587      (ALeaf{x}, x)
2588    case ANode{xs, ys} True{}:
2589      +h = U32.shr(n)
2590      Array.swap.lo(T, ys, Array.get.go(T, xs, h, i, U32.is_lt(i, U32.shr(h))))
2591    case ANode{xs, ys} False{}:
2592      +h = U32.shr(n)
2593      +j = U32.sub(i, h)
2594      Array.swap.hi(T, xs, Array.get.go(T, ys, h, j, U32.is_lt(j, U32.shr(h))))
2595
2596def Array.get.at(-T: Data, i: U32, an: Array<T> & U32) -> Array<T> & T:
2597  (a, +n) = an
2598  +j = U32.and(i, U32.sub(n, 1))
2599  Array.get.go(T, a, n, j, U32.is_lt(j, U32.shr(n)))
2600
2601def Array.get(-T: Data, a: Array<T>, +i: U32) -> Array<T> & T:
2602  Array.get.at(T, i, Array.size(T, a))
2603
2604def Array.to_list.go(~T: Type, a: Array<T>, acc: List<T>) -> List<T>:
2605  match a:
2606    case ALeaf{x}:
2607      x <> acc
2608    case ANode{xs, ys}:
2609      Array.to_list.go(~T, xs, Array.to_list.go(~T, ys, acc))
2610
2611def Array.to_list(~T: Type, a: Array<T>) -> List<T>:
2612  Array.to_list.go(~T, a, Nil{})
2613
2614def Array.map.go(
2615  ~T: Data, ~U: Data, ~f: T -> U, +n: Nat, +i: U32, b: Array<U>,
2616  r: Array<T> & T
2617) -> Array<U>:
2618  match n:
2619    case 0n:
2620      b
2621    case 1n+p:
2622      (a, x) = r
2623      +j = U32.inc(i)
2624      Array.map.go(~T, ~U, ~f, p, j, Array.set(U, b, i, f(x)),
2625        Array.get(T, a, j))
2626
2627def Array.map.at(
2628  ~T: Data, ~U: Data, ~f: T -> U, v: U, an: Array<T> & U32
2629) -> Array<U>:
2630  (a, +n) = an
2631  Array.map.go(~T, ~U, ~f, U32.to_nat(U32.sub(n, 1)), 1,
2632    Array.new(U, U32.log2(n), v), Array.get(T, a, 1))
2633
2634def Array.map.seed(~T: Data, ~U: Data, ~f: T -> U, r: Array<T> & T) -> Array<U>:
2635  (a, x) = r
2636  Array.map.at(~T, ~U, ~f, f(x), Array.size(T, a))
2637
2638def Array.map(~T: Data, ~U: Data, ~f: T -> U, a: Array<T>) -> Array<U>:
2639  Array.map.seed(~T, ~U, ~f, Array.get(T, a, 0))
2640
2641# Map
2642# ---
2643
2644def Map.bit.u(x: U32, k: Nat) -> Bool:
2645  U32.is_ne(U32.and(U32.shrn(x, k), 1), 0)
2646
2647def Map.bit.chr(c: Char, off: Nat) -> Char & Bool:
2648  match c off:
2649    case Chr{x} 0n:
2650      (Chr{x}, True{})
2651    case Chr{+x} 1n+b:
2652      (Chr{x}, Map.bit.u(x, Nat.sub(31n, b)))
2653
2654def Map.bit.go.chr(t: String, r: Char & Bool) -> String & Bool:
2655  (c2, b) = r
2656  (SCon{c2, t}, b)
2657
2658def Map.bit.go.rec(c: Char, r: String & Bool) -> String & Bool:
2659  (t2, b) = r
2660  (SCon{c, t2}, b)
2661
2662def Map.bit.go(key: String, ci: Nat, off: Nat) -> String & Bool:
2663  match key:
2664    case SNil{}:
2665      (SNil{}, False{})
2666    case SCon{c, t}:
2667      match ci:
2668        case 0n:
2669          Map.bit.go.chr(t, Map.bit.chr(c, off))
2670        case 1n+j:
2671          Map.bit.go.rec(c, Map.bit.go(t, j, off))
2672
2673def Map.bit.at(key: String, co: Nat & Nat) -> String & Bool:
2674  (ci, off) = co
2675  Map.bit.go(key, ci, off)
2676
2677def Map.bit(key: String, pos: Nat) -> String & Bool:
2678  Map.bit.at(key, Nat.divmod(pos, 33n))
2679
2680law Map.msb.u:
2681  for n: Nat
2682  for +x: U32
2683  Nat
2684
2685def Map.msb.u.if(p: Nat, x2: U32, z: Bool) -> Nat:
2686  match z:
2687    case True{}:
2688      0n
2689    case False{}:
2690      Nat.add(1n, Map.msb.u(p, U32.shr(x2)))
2691
2692def Map.msb.u(n, x):
2693  match n:
2694    case 0n:
2695      0n
2696    case 1n+p:
2697      Map.msb.u.if(p, x, U32.is_zero(x))
2698
2699def Map.diff.chr(x: U32) -> Nat:
2700  Nat.sub(33n, Map.msb.u(32n, x))
2701
2702def Map.diff.step(x: Char, y: Char) -> Nat & Bool:
2703  match x y:
2704    case Chr{+cx} Chr{+cy}:
2705      (Map.diff.chr(U32.xor(cx, cy)), U32.is_eq(cx, cy))
2706
2707law Map.diff:
2708  for a: String
2709  for b: String
2710  Nat
2711
2712def Map.diff.fin(xt: String, yt: String, rc: Nat & Bool) -> Nat:
2713  (r, c) = rc
2714  match c:
2715    case True{}:
2716      Nat.add(33n, Map.diff(xt, yt))
2717    case False{}:
2718      r
2719
2720def Map.diff(a, b):
2721  match a b:
2722    case SNil{} _:
2723      0n
2724    case SCon{h, t} SNil{}:
2725      0n
2726    case SCon{x, xt} SCon{y, yt}:
2727      Map.diff.fin(xt, yt, Map.diff.step(x, y))
2728
2729def Map.new(a, -V: Kind(a)) -> Map<a, V>:
2730  MTip{}
2731
2732# Map.put.go, Map.ins.go, Map.seek.go, Map.has.go, Map.get.go and
2733# Map.pop.go take the node they are in, whole, and the key's bit at it:
2734# the child they descend into is that node's field, a node rebuilt
2735def Map.put.go(-a: Quant, -V: Kind(a), node: Map<a, V>, x: V, kb: String & Bool) -> Map<a, V>:
2736  match node kb:
2737    case MNode{p, MTip{}, hi} Tuple{key, False{}}:
2738      MNode{p, MLeaf{key, x}, hi}
2739    case MNode{p, MLeaf{k, v}, hi} Tuple{key, False{}}:
2740      MNode{p, MLeaf{k, x}, hi}
2741    case MNode{p, MNode{+q, c, d}, hi} Tuple{key, False{}}:
2742      MNode{p, Map.put.go(a, V, MNode{q, c, d}, x, Map.bit(key, q)), hi}
2743    case MNode{p, lo, MTip{}} Tuple{key, True{}}:
2744      MNode{p, lo, MLeaf{key, x}}
2745    case MNode{p, lo, MLeaf{k, v}} Tuple{key, True{}}:
2746      MNode{p, lo, MLeaf{k, x}}
2747    case MNode{p, lo, MNode{+q, c, d}} Tuple{key, True{}}:
2748      MNode{p, lo, Map.put.go(a, V, MNode{q, c, d}, x, Map.bit(key, q))}
2749    case m _:
2750      m
2751
2752def Map.put(-a: Quant, -V: Kind(a), m: Map<a, V>, key: String, x: V) -> Map<a, V>:
2753  match m:
2754    case MTip{}:
2755      MLeaf{key, x}
2756    case MLeaf{k, v}:
2757      MLeaf{k, x}
2758    case MNode{+pos, lo, hi}:
2759      Map.put.go(a, V, MNode{pos, lo, hi}, x, Map.bit(key, pos))
2760
2761def Map.ins.splice.bit(
2762  a, -V: Kind(a), x: V, rest: Map<a, V>, pb: Nat, kb: String & Bool
2763) -> Map<a, V>:
2764  (key2, b) = kb
2765  match b:
2766    case False{}:
2767      MNode{pb, MLeaf{key2, x}, rest}
2768    case True{}:
2769      MNode{pb, rest, MLeaf{key2, x}}
2770
2771def Map.ins.splice(
2772  a, -V: Kind(a), +p: Nat, key: String, x: V, rest: Map<a, V>
2773) -> Map<a, V>:
2774  Map.ins.splice.bit(a, V, x, rest, p, Map.bit(key, p))
2775
2776# t says whether the key splits deeper than node: else it goes above
2777def Map.ins.go(
2778  -a: Quant, -V: Kind(a), node: Map<a, V>, x: V, +p: Nat, kb: String & Bool,
2779  t: Bool
2780) -> Map<a, V>:
2781  match node kb t:
2782    case MNode{q, lo, hi} Tuple{key, b} False{}:
2783      Map.ins.splice(a, V, p, key, x, MNode{q, lo, hi})
2784    case MNode{q, MTip{}, hi} Tuple{key, False{}} True{}:
2785      MNode{q, MLeaf{key, x}, hi}
2786    case MNode{q, MLeaf{k, v}, hi} Tuple{key, False{}} True{}:
2787      MNode{q, Map.ins.splice(a, V, p, key, x, MLeaf{k, v}), hi}
2788    case MNode{q, MNode{+r, c, d}, hi} Tuple{key, False{}} True{}:
2789      MNode{q, Map.ins.go(a, V, MNode{r, c, d}, x, p, Map.bit(key, r), Nat.is_lt(r, p)), hi}
2790    case MNode{q, lo, MTip{}} Tuple{key, True{}} True{}:
2791      MNode{q, lo, MLeaf{key, x}}
2792    case MNode{q, lo, MLeaf{k, v}} Tuple{key, True{}} True{}:
2793      MNode{q, lo, Map.ins.splice(a, V, p, key, x, MLeaf{k, v})}
2794    case MNode{q, lo, MNode{+r, c, d}} Tuple{key, True{}} True{}:
2795      MNode{q, lo, Map.ins.go(a, V, MNode{r, c, d}, x, p, Map.bit(key, r), Nat.is_lt(r, p))}
2796    case m _ _:
2797      m
2798
2799def Map.ins(
2800  -a: Quant, -V: Kind(a), m: Map<a, V>, key: String, x: V, +p: Nat
2801) -> Map<a, V>:
2802  match m:
2803    case MTip{}:
2804      MLeaf{key, x}
2805    case MLeaf{k, v}:
2806      Map.ins.splice(a, V, p, key, x, MLeaf{k, v})
2807    case MNode{+pos, lo, hi}:
2808      Map.ins.go(a, V, MNode{pos, lo, hi}, x, p, Map.bit(key, pos), Nat.is_lt(pos, p))
2809
2810def Map.lo(
2811  a, -V: Kind(a), -R: Type, p2: Nat, hi: Map<a, V>, r0: Map<a, V> & R
2812) -> Map<a, V> & R:
2813  (lo2, r) = r0
2814  (MNode{p2, lo2, hi}, r)
2815
2816def Map.hi(
2817  a, -V: Kind(a), -R: Type, p2: Nat, lo: Map<a, V>, r0: Map<a, V> & R
2818) -> Map<a, V> & R:
2819  (hi2, r) = r0
2820  (MNode{p2, lo, hi2}, r)
2821
2822def Map.seek.go(-a: Quant, -V: Kind(a), node: Map<a, V>, kb: String & Bool) ->
2823  Map<a, V> & String & Maybe<&2, String>:
2824  match node kb:
2825    case MNode{p, MTip{}, hi} Tuple{key, False{}}:
2826      (MNode{p, MTip{}, hi}, key, None{})
2827    case MNode{p, MLeaf{+k, v}, hi} Tuple{key, False{}}:
2828      (MNode{p, MLeaf{k, v}, hi}, key, Some{k})
2829    case MNode{p, MNode{+q, c, d}, hi} Tuple{key, False{}}:
2830      Map.lo(a, V, String & Maybe<&2, String>, p, hi, Map.seek.go(a, V, MNode{q, c, d}, Map.bit(key, q)))
2831    case MNode{p, lo, MTip{}} Tuple{key, True{}}:
2832      (MNode{p, lo, MTip{}}, key, None{})
2833    case MNode{p, lo, MLeaf{+k, v}} Tuple{key, True{}}:
2834      (MNode{p, lo, MLeaf{k, v}}, key, Some{k})
2835    case MNode{p, lo, MNode{+q, c, d}} Tuple{key, True{}}:
2836      Map.hi(a, V, String & Maybe<&2, String>, p, lo, Map.seek.go(a, V, MNode{q, c, d}, Map.bit(key, q)))
2837    case m Tuple{key, b}:
2838      (m, key, None{})
2839
2840def Map.seek(-a: Quant, -V: Kind(a), m: Map<a, V>, key: String) ->
2841  Map<a, V> & String & Maybe<&2, String>:
2842  match m:
2843    case MTip{}:
2844      (MTip{}, key, None{})
2845    case MLeaf{+k, v}:
2846      (MLeaf{k, v}, key, Some{k})
2847    case MNode{+pos, lo, hi}:
2848      Map.seek.go(a, V, MNode{pos, lo, hi}, Map.bit(key, pos))
2849
2850def Map.set.fin.go(
2851  a, -V: Kind(a), m: Map<a, V>, key: String, x: V, r: (String & String) & Cmp
2852) -> Map<a, V>:
2853  ((keyb2, k2), c) = r
2854  match c:
2855    case EQ{}:
2856      Map.put(a, V, m, key, x)
2857    case o:
2858      Map.ins(a, V, m, key, x, Map.diff(keyb2, k2))
2859
2860def Map.set.fin(
2861  a, -V: Kind(a), m: Map<a, V>, key: String, x: V, keyb: String, k: String
2862) -> Map<a, V>:
2863  Map.set.fin.go(a, V, m, key, x, String.cmp(keyb, k))
2864
2865def Map.set.go(
2866  a, -V: Kind(a), x: V, r: Map<a, V> & String & Maybe<&2, String>
2867) -> Map<a, V>:
2868  (m2, key2, found) = r
2869  match found:
2870    case None{}:
2871      MLeaf{key2, x}
2872    case Some{k}:
2873      +ka = {key2 : String}
2874      Map.set.fin(a, V, m2, ka, x, ka, k)
2875
2876def Map.set(a, -V: Kind(a), m: Map<a, V>, key: String, x: V) -> Map<a, V>:
2877  Map.set.go(a, V, x, Map.seek(a, V, m, key))
2878
2879def Map.has.leaf(a, -V: Kind(a), v: V, r: (String & String) & Cmp) ->
2880  Map<a, V> & Bool:
2881  ((key2, k2), c) = r
2882  (MLeaf{k2, v}, Cmp.is_eq(c))
2883
2884def Map.has.go(-a: Quant, -V: Kind(a), node: Map<a, V>, kb: String & Bool) ->
2885  Map<a, V> & Bool:
2886  match node kb:
2887    case MNode{p, MTip{}, hi} Tuple{key, False{}}:
2888      (MNode{p, MTip{}, hi}, False{})
2889    case MNode{p, MLeaf{k, v}, hi} Tuple{key, False{}}:
2890      Map.lo(a, V, Bool, p, hi, Map.has.leaf(a, V, v, String.cmp(key, k)))
2891    case MNode{p, MNode{+q, c, d}, hi} Tuple{key, False{}}:
2892      Map.lo(a, V, Bool, p, hi, Map.has.go(a, V, MNode{q, c, d}, Map.bit(key, q)))
2893    case MNode{p, lo, MTip{}} Tuple{key, True{}}:
2894      (MNode{p, lo, MTip{}}, False{})
2895    case MNode{p, lo, MLeaf{k, v}} Tuple{key, True{}}:
2896      Map.hi(a, V, Bool, p, lo, Map.has.leaf(a, V, v, String.cmp(key, k)))
2897    case MNode{p, lo, MNode{+q, c, d}} Tuple{key, True{}}:
2898      Map.hi(a, V, Bool, p, lo, Map.has.go(a, V, MNode{q, c, d}, Map.bit(key, q)))
2899    case m _:
2900      (m, False{})
2901
2902def Map.has(-a: Quant, -V: Kind(a), m: Map<a, V>, key: String) -> Map<a, V> & Bool:
2903  match m:
2904    case MTip{}:
2905      (MTip{}, False{})
2906    case MLeaf{k, v}:
2907      Map.has.leaf(a, V, v, String.cmp(key, k))
2908    case MNode{+pos, lo, hi}:
2909      Map.has.go(a, V, MNode{pos, lo, hi}, Map.bit(key, pos))
2910
2911def Map.get.leaf(-V: Data, d: V, +v: V, r: (String & String) & Cmp) ->
2912  Map<&2, V> & V:
2913  ((key2, k2), c) = r
2914  match c:
2915    case EQ{}:
2916      (MLeaf{k2, v}, v)
2917    case o:
2918      (MLeaf{k2, v}, d)
2919
2920def Map.get.go(-V: Data, node: Map<&2, V>, d: V, kb: String & Bool) -> Map<&2, V> & V:
2921  match node kb:
2922    case MNode{p, MTip{}, hi} Tuple{key2, False{}}:
2923      (MNode{p, MTip{}, hi}, d)
2924    case MNode{p, MLeaf{k, v}, hi} Tuple{key2, False{}}:
2925      Map.lo(&2, V, V, p, hi, Map.get.leaf(V, d, v, String.cmp(key2, k)))
2926    case MNode{p, MNode{+q, a, b}, hi} Tuple{key2, False{}}:
2927      Map.lo(&2, V, V, p, hi, Map.get.go(V, MNode{q, a, b}, d, Map.bit(key2, q)))
2928    case MNode{p, lo, MTip{}} Tuple{key2, True{}}:
2929      (MNode{p, lo, MTip{}}, d)
2930    case MNode{p, lo, MLeaf{k, v}} Tuple{key2, True{}}:
2931      Map.hi(&2, V, V, p, lo, Map.get.leaf(V, d, v, String.cmp(key2, k)))
2932    case MNode{p, lo, MNode{+q, a, b}} Tuple{key2, True{}}:
2933      Map.hi(&2, V, V, p, lo, Map.get.go(V, MNode{q, a, b}, d, Map.bit(key2, q)))
2934    case m _:
2935      (m, d)
2936
2937def Map.get(-V: Data, d: V, m: Map<&2, V>, key: String) -> Map<&2, V> & V:
2938  match m:
2939    case MTip{}:
2940      (MTip{}, d)
2941    case MLeaf{k, v}:
2942      Map.get.leaf(V, d, v, String.cmp(key, k))
2943    case MNode{+pos, lo, hi}:
2944      Map.get.go(V, MNode{pos, lo, hi}, d, Map.bit(key, pos))
2945
2946def Map.pop.lo(
2947  a, -V: Kind(a), pos: Nat, hi: Map<a, V>, r0: Map<a, V> & Maybe<a, V>
2948) -> Map<a, V> & Maybe<a, V>:
2949  (lo, r) = r0
2950  match lo:
2951    case MTip{}:
2952      (hi, r)
2953    case lo2:
2954      (MNode{pos, lo2, hi}, r)
2955
2956def Map.pop.hi(
2957  a, -V: Kind(a), pos: Nat, lo: Map<a, V>, r0: Map<a, V> & Maybe<a, V>
2958) -> Map<a, V> & Maybe<a, V>:
2959  (hi, r) = r0
2960  match hi:
2961    case MTip{}:
2962      (lo, r)
2963    case hi2:
2964      (MNode{pos, lo, hi2}, r)
2965
2966def Map.pop.leaf(a, -V: Kind(a), v: V, r: (String & String) & Cmp) ->
2967  Map<a, V> & Maybe<a, V>:
2968  ((key2, k2), c) = r
2969  match c:
2970    case EQ{}:
2971      (MTip{}, Some{v})
2972    case o:
2973      (MLeaf{k2, v}, None{})
2974
2975def Map.pop.go(-a: Quant, -V: Kind(a), node: Map<a, V>, kb: String & Bool) ->
2976  Map<a, V> & Maybe<a, V>:
2977  match node kb:
2978    case MNode{p, MTip{}, hi} Tuple{key, False{}}:
2979      (hi, None{})
2980    case MNode{p, MLeaf{k, v}, hi} Tuple{key, False{}}:
2981      Map.pop.lo(a, V, p, hi, Map.pop.leaf(a, V, v, String.cmp(key, k)))
2982    case MNode{p, MNode{+q, c, d}, hi} Tuple{key, False{}}:
2983      Map.pop.lo(a, V, p, hi, Map.pop.go(a, V, MNode{q, c, d}, Map.bit(key, q)))
2984    case MNode{p, lo, MTip{}} Tuple{key, True{}}:
2985      (lo, None{})
2986    case MNode{p, lo, MLeaf{k, v}} Tuple{key, True{}}:
2987      Map.pop.hi(a, V, p, lo, Map.pop.leaf(a, V, v, String.cmp(key, k)))
2988    case MNode{p, lo, MNode{+q, c, d}} Tuple{key, True{}}:
2989      Map.pop.hi(a, V, p, lo, Map.pop.go(a, V, MNode{q, c, d}, Map.bit(key, q)))
2990    case m _:
2991      (m, None{})
2992
2993def Map.pop(-a: Quant, -V: Kind(a), m: Map<a, V>, key: String) -> Map<a, V> & Maybe<a, V>:
2994  match m:
2995    case MTip{}:
2996      (MTip{}, None{})
2997    case MLeaf{k, v}:
2998      Map.pop.leaf(a, V, v, String.cmp(key, k))
2999    case MNode{+pos, lo, hi}:
3000      Map.pop.go(a, V, MNode{pos, lo, hi}, Map.bit(key, pos))
3001
3002def Map.del.fin(a, -V: Kind(a), r: Map<a, V> & Maybe<a, V>) -> Map<a, V>:
3003  (m2, x) = r
3004  m2
3005
3006def Map.del(a, -V: Kind(a), m: Map<a, V>, key: String) -> Map<a, V>:
3007  Map.del.fin(a, V, Map.pop(a, V, m, key))
3008
3009def Map.to_list.go(
3010  a, -V: Kind(a), m: Map<a, V>, acc: List<a, Sigma<&2, a, String, _ => V>>
3011) -> List<a, Sigma<&2, a, String, _ => V>>:
3012  match m:
3013    case MTip{}:
3014      acc
3015    case MLeaf{k, v}:
3016      (k, v) <> acc
3017    case MNode{pos, lo, hi}:
3018      Map.to_list.go(a, V, lo, Map.to_list.go(a, V, hi, acc))
3019
3020def Map.to_list(a, -V: Kind(a), m: Map<a, V>) ->
3021  List<a, Sigma<&2, a, String, _ => V>>:
3022  Map.to_list.go(a, V, m, Nil{})
3023
3024def Map.keys.go(a, -V: Kind(a), m: Map<a, V>, acc: List<&2, String>) ->
3025  List<&2, String>:
3026  match m:
3027    case MTip{}:
3028      acc
3029    case MLeaf{k, v}:
3030      k <> acc
3031    case MNode{pos, lo, hi}:
3032      Map.keys.go(a, V, lo, Map.keys.go(a, V, hi, acc))
3033
3034def Map.keys(a, -V: Kind(a), m: Map<a, V>) -> List<&2, String>:
3035  Map.keys.go(a, V, m, Nil{})
3036
3037def Map.from_list.go(
3038  a, -V: Kind(a), kvs: List<a, Sigma<&2, a, String, _ => V>>, m: Map<a, V>
3039) -> Map<a, V>:
3040  match kvs:
3041    case Nil{}:
3042      m
3043    case (k, v) <> t:
3044      Map.from_list.go(a, V, t, Map.set(a, V, m, k, v))
3045
3046def Map.from_list(a, -V: Kind(a), kvs: List<a, Sigma<&2, a, String, _ => V>>) ->
3047  Map<a, V>:
3048  Map.from_list.go(a, V, kvs, MTip{})
3049
3050def Map.union(a, -V: Kind(a), m: Map<a, V>, n: Map<a, V>) -> Map<a, V>:
3051  Map.from_list.go(a, V, Map.to_list(a, V, n), m)
3052
3053def Map.size(a, -V: Kind(a), m: Map<a, V>) -> Nat:
3054  match m:
3055    case MTip{}:
3056      0n
3057    case MLeaf{k, v}:
3058      1n
3059    case MNode{pos, lo, hi}:
3060      Nat.add(Map.size(a, V, lo), Map.size(a, V, hi))
3061
3062def Map.values.go(a, -V: Kind(a), m: Map<a, V>, acc: List<a, V>) -> List<a, V>:
3063  match m:
3064    case MTip{}:
3065      acc
3066    case MLeaf{k, v}:
3067      v <> acc
3068    case MNode{pos, lo, hi}:
3069      Map.values.go(a, V, lo, Map.values.go(a, V, hi, acc))
3070
3071def Map.values(a, -V: Kind(a), m: Map<a, V>) -> List<a, V>:
3072  Map.values.go(a, V, m, Nil{})
3073
3074# Set
3075# ---
3076
3077def Set() -> Data:
3078  Map<&2, Unit>
3079
3080def Set.new() -> Set():
3081  Map.new(&2, Unit)
3082
3083def Set.add(s: Set(), key: String) -> Set():
3084  Map.set(&2, Unit, s, key, Unit{})
3085
3086def Set.has(s: Set(), key: String) -> Set() & Bool:
3087  Map.has(&2, Unit, s, key)
3088
3089def Set.del(s: Set(), key: String) -> Set():
3090  Map.del(&2, Unit, s, key)
3091
3092def Set.size(s: Set()) -> Nat:
3093  Map.size(&2, Unit, s)
3094
3095def Set.to_list(s: Set()) -> List<&2, String>:
3096  Map.keys(&2, Unit, s)
3097
3098def Set.from_list.go(keys: List<&2, String>, s: Set()) -> Set():
3099  match keys:
3100    case Nil{}:
3101      s
3102    case h <> t:
3103      Set.from_list.go(t, Set.add(s, h))
3104
3105def Set.from_list(keys: List<&2, String>) -> Set():
3106  Set.from_list.go(keys, Set.new())
3107
3108# Image
3109# -----
3110
3111def Image.sink(img: Image) -> Unit:
3112  Unit{}
3113
3114def Image.drop.join(a: Unit, b: Unit, c: Unit, d: Unit) -> Unit:
3115  match a b c d:
3116    case Unit{} Unit{} Unit{} Unit{}:
3117      Unit{}
3118
3119# Forks k levels, then a dead parameter sinks the rest in one loop.
3120def Image.free(+k: Nat, img: Image) -> Unit:
3121  match k:
3122    case 0n:
3123      Image.sink(img)
3124    case 1n+e:
3125      match img:
3126        case Pix{c}:
3127          Unit{}
3128        case Qua{tl, tr, bl, br}:
3129          a b c d = Image.free(e, tl) Image.free(e, tr) Image.free(e, bl)
3130            Image.free(e, br)
3131          Image.drop.join(a, b, c, d)
3132
3133def Image.drop(img: Image) -> Unit:
3134  Image.free(7n, img)
3135
3136# App
3137# ---
3138
3139def App.next(
3140  -S: Type, window: Window, rest: Window -> S -> IO(Unit), next: Maybe<S>
3141) -> IO(Unit):
3142  match next:
3143    case None{}:
3144      Window.close(window)
3145    case Some{state}:
3146      rest(window, state)
3147
3148def App.turn(
3149  -S: Type, shown: Window & Image & List<Event>,
3150  tick: List<Event> -> S -> IO(Maybe<S>), state: S,
3151  rest: Window -> S -> IO(Unit)
3152) -> IO(Unit):
3153  (window, image, events) = shown
3154  do IO<Unit>:
3155    Unit <- IO.pure(Unit, Image.drop!(image))
3156    IO.bind(Maybe<S>, Unit, tick(events, state), App.next(S, window, rest))
3157
3158def App.draw(
3159  -S: Type, window: Window, drawn: S & Image,
3160  tick: List<Event> -> S -> IO(Maybe<S>), rest: Window -> S -> IO(Unit)
3161) -> IO(Unit):
3162  (state, image) = drawn
3163  do IO<Unit>:
3164    shown : Window & Image & List<Event> <- Window.frame(window, image)
3165    App.turn(S, shown, tick, state, rest)
3166
3167def App.step(
3168  -S: Type, app: App<S>, window: Window, state: S,
3169  rest: Window -> S -> IO(Unit)
3170) -> IO(Unit):
3171  App{view, tick} = app
3172  App.draw(S, window, view(state), tick, rest)
3173
3174def App.loop(~S: Type, ~app: App<S>, fuel: Nat, window: Window, state: S) ->
3175  IO(Unit):
3176  match fuel:
3177    case 0n:
3178      Window.close(window)
3179    case 1n+f:
3180      App.step(S, app, window, state, w => s => App.loop(~S, ~app, f, w, s))
3181
3182def App.run(
3183  ~S: Type, ~app: App<S>, title: String, width: U32, height: U32, state: S
3184) -> IO(Unit):
3185  do IO<Unit>:
3186    window : Window <- IO.try(Window, Window.open(title, width, height))
3187    App.loop(~S, ~app, 4294967295n, window, state)
3188
3189def App.more(-S: Type, rest: S -> IO(Maybe<S>), next: Maybe<S>) ->
3190  IO(Maybe<S>):
3191  match next:
3192    case None{}:
3193      IO.pure(Maybe<S>, None{})
3194    case Some{state}:
3195      rest(state)
3196
3197def App.fold(
3198  -S: Type, app: App<S>, events: List<Event>, state: S,
3199  rest: S -> IO(Maybe<S>)
3200) -> IO(Maybe<S>):
3201  App{view, tick} = app
3202  IO.bind(Maybe<S>, Maybe<S>, tick(events, state), App.more(S, rest))
3203
3204def App.play(~S: Type, ~app: App<S>, frames: List<List<Event>>, state: S) ->
3205  IO(Maybe<S>):
3206  match frames:
3207    case Nil{}:
3208      IO.pure(Maybe<S>, Some{state})
3209    case events <> rest:
3210      App.fold(S, app, events, state, s => App.play(~S, ~app, rest, s))