1 # Types 2 # ===== 3 4 # Data 5 # ---- 6 7 type Empty is Data: 8 9 type Unit is Data: 10 Unit{} 11 12 type Bool is Data: 13 False{} 14 True{} 15 16 type Cmp is Data: 17 LT{} 18 EQ{} 19 GT{} 20 21 type Either is Kind(a <&> b): 22 Inl{value: A} 23 Inr{value: B} 24 25 type Sigma Kind(b)> is Kind(a <&> b): 26 Tuple{fst: A, snd: B(fst)} 27 28 type Nat is Data: 29 Zero{} 30 Succ{pred: Nat} 31 32 type Maybe is Kind(a): 33 None{} 34 Some{value: A} 35 36 type Result 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). 43 type Poll is Kind(a <&> b): 44 Ready{value: A} 45 Wait{rest: R} 46 47 type List is Kind(a): 48 Nil{} 49 Con{head: A, tail: List} 50 51 type Word.Nil is Data: 52 WNil{} 53 54 type Word.Con<-p: Nat> is Data: 55 WCon{head: Bool, tail: Word(p)} 56 57 def Word(n: Nat) -> Data: 58 match n: 59 case 0n: 60 Word.Nil 61 case 1n+p: 62 Word.Con

63 64 type U32 is Data: 65 U32{data: Word(32n)} 66 67 type F32 is Data: 68 F32{data: Word(32n)} 69 70 type Char is Data: 71 Chr{code: U32} 72 73 type String is Data: 74 SNil{} 75 SCon{head: Char, tail: String} 76 77 type Array<-T: Type> is Type: 78 ALeaf{value: T} 79 ANode{xs: Array, ys: Array} 80 81 type 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. 89 type 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 98 type Map is Kind(a): 99 MTip{} 100 MLeaf{key: String, val: V} 101 MNode{pos: Nat, lo: Map, hi: Map} 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. 108 law File: 109 Type 110 111 law Socket: 112 Type 113 114 law Listener: 115 Type 116 117 law Window: 118 Type 119 120 law Audio: 121 Type 122 123 # A channel is Data: the computations it links each hold a copy. 124 law Chan: 125 for -A: Type 126 Data 127 128 type IO.OP<-R: Type> is Type: 129 Emit{value: R} 130 Halt{code: U32, message: String} 131 Exit{code: U32} 132 133 type App<-S: Type> is Type: 134 App{view: S -> Pair(S, Image), tick: List -> S -> IO(Maybe)} 135 136 # Defs 137 # ==== 138 139 # Pair 140 # ---- 141 142 def Pair(-A: Type, -B: Type) -> Type: 143 Sigma<&1, &1, A, _ => B> 144 145 def Exists(-A: Type, -B: @-x: A -> Type) -> Type: 146 Sigma<&1, &1, A, B> 147 148 def Or(-A: Type, -B: Type) -> Type: 149 Either<&1, &1, A, B> 150 151 def Pair.fst(-A: Type, -B: Type, p: A & B) -> A: 152 (a, b) = p 153 a 154 155 def Pair.snd(-A: Type, -B: Type, p: A & B) -> B: 156 (a, b) = p 157 b 158 159 # Effects 160 # ------- 161 162 def IO(-A: Type) -> Type: 163 @-R: Type -> 164 @k: (A -> IO.OP) -> 165 IO.OP 166 167 def IO.pure(-A: Type, x: A) -> IO(A): 168 R => k => k(x) 169 170 def 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 173 def IO.print(text: String) -> IO(Unit): 174 import "./effs/print.c" 175 import "./effs/print.js" 176 177 def IO.write(text: String) -> IO(Unit): 178 import "./effs/write.c" 179 import "./effs/write.js" 180 181 def IO.print_err(text: String) -> IO(Unit): 182 import "./effs/print_err.c" 183 import "./effs/print_err.js" 184 185 def 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. 191 def IO.args() -> IO(List): 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. 200 def IO.args_bytes() -> IO(List>): 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. 206 def Process.run(program: String, args: List, 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 212 def IO.die(-A: Type, code: U32, msg: String) -> IO(A): 213 R => k => Halt{code, msg} 214 215 def IO.exit(code: U32) -> IO(Unit): 216 R => k => Exit{code} 217 218 def 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 225 def 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 228 def IO.random_u32() -> IO(Result<&1, &1, U32 & String, U32>): 229 import "./effs/random_u32.c" 230 import "./effs/random_u32.js" 231 232 def IO.spawn(-A: Type, act: IO(A)) -> IO(Unit): 233 import "./effs/spawn.c" 234 import "./effs/spawn.js" 235 236 def IO.sleep(ms: U32) -> IO(Unit): 237 import "./effs/sleep.c" 238 import "./effs/sleep.js" 239 240 def IO.now() -> IO(Nat): 241 import "./effs/now.c" 242 import "./effs/now.js" 243 244 def IO.thread_count() -> IO(U32): 245 import "./effs/thread_count.c" 246 import "./effs/thread_count.js" 247 248 def 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. 253 def 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. 258 def Chan.recv(-A: Type, chan: Chan(A)) -> IO(Maybe<&1, A>): 259 import "./effs/chan.c" 260 import "./effs/chan.js" 261 262 def 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 267 def 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 272 def Chan.close(-A: Type, chan: Chan(A)) -> IO(Unit): 273 import "./effs/chan.c" 274 import "./effs/chan.js" 275 276 def 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 282 def 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 285 def 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 292 def 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. 297 def 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 304 def 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. 312 def 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 317 def 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 322 def 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 327 def 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 332 def 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 337 def 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 342 def 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 347 def File.close(file: File) -> IO(Unit): 348 import "./effs/file_close.c" 349 import "./effs/file_close.js" 350 351 def 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 355 def 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 360 def 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 365 def 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. 373 def 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 378 def 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. 386 def 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 391 def 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. 399 def 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 404 def 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 410 def 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 415 def 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 421 def 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. 426 def 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 431 def 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. 439 def 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 444 def 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{}. 452 def 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 457 def 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. 464 def 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 469 def 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 475 def Socket.close(socket: Socket) -> IO(Unit): 476 import "./effs/socket_close.c" 477 import "./effs/socket_close.js" 478 479 def Listener.close(listener: Listener) -> IO(Unit): 480 import "./effs/listener_close.c" 481 import "./effs/listener_close.js" 482 483 def 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 488 def Window.frame(window: Window, image: Image) -> 489 IO(Window & Image & List): 490 import "./effs/window.c" 491 import "./effs/window_frame.js" 492 493 def 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. 499 def Window.grab(window: Window, on: Bool) -> IO(Window): 500 import "./effs/window.c" 501 import "./effs/window_grab.js" 502 503 def Window.close(window: Window) -> IO(Unit): 504 import "./effs/window.c" 505 import "./effs/window_close.js" 506 507 def Audio.open(rate: U32) -> IO(Result<&1, &1, U32 & String, Audio>): 508 import "./effs/audio.c" 509 import "./effs/audio_open.js" 510 511 def Audio.write(audio: Audio, samples: List<&2, F32>) -> IO(Audio & U32): 512 import "./effs/audio.c" 513 import "./effs/audio_write.js" 514 515 def Audio.close(audio: Audio) -> IO(Unit): 516 import "./effs/audio.c" 517 import "./effs/audio_close.js" 518 519 # Equal 520 # ----- 521 522 law 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 531 def Equal.cong(A, B, f, a, b, e): 532 %e : {f(a) == f(_) : B} 533 {==} 534 535 law 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 542 def Equal.sym(A, a, b, e): 543 %e : {_ == a : A} 544 {==} 545 546 law 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 555 def Equal.trans(A, a, b, c, ab, bc): 556 %bc : {a == _ : A} 557 ab 558 559 # Empty 560 # ----- 561 562 def Empty.absurd(-A: Type, e: Empty) -> A: 563 match e: 564 565 # Bool 566 # ---- 567 568 def Bool.not(b: Bool) -> Bool: 569 match b: 570 case False{}: 571 True{} 572 case True{}: 573 False{} 574 575 def Bool.and(a: Bool, b: Bool) -> Bool: 576 match a: 577 case False{}: 578 False{} 579 case True{}: 580 b 581 582 def Bool.or(a: Bool, b: Bool) -> Bool: 583 match a: 584 case False{}: 585 b 586 case True{}: 587 True{} 588 589 def Bool.xor(a: Bool, b: Bool) -> Bool: 590 match a: 591 case False{}: 592 b 593 case True{}: 594 Bool.not(b) 595 596 def 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 607 def 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 614 def 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 621 def Bool.to_u32(b: Bool) -> U32: 622 match b: 623 case False{}: 624 0 625 case True{}: 626 1 627 628 # Cmp 629 # --- 630 631 def Cmp.is_lt(c: Cmp) -> Bool: 632 match c: 633 case LT{}: 634 True{} 635 case o: 636 False{} 637 638 def Cmp.is_eq(c: Cmp) -> Bool: 639 match c: 640 case EQ{}: 641 True{} 642 case o: 643 False{} 644 645 def Cmp.is_gt(c: Cmp) -> Bool: 646 match c: 647 case GT{}: 648 True{} 649 case o: 650 False{} 651 652 def Cmp.is_le(c: Cmp) -> Bool: 653 match c: 654 case GT{}: 655 False{} 656 case o: 657 True{} 658 659 def Cmp.is_ge(c: Cmp) -> Bool: 660 match c: 661 case LT{}: 662 False{} 663 case o: 664 True{} 665 666 # Nat 667 # --- 668 669 def Nat.double(n: Nat) -> Nat: 670 match n: 671 case 0n: 672 0n 673 case 1n+p: 674 2n+Nat.double(p) 675 676 def 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 683 def 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 692 def 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 699 def 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 710 def 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 717 def 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 728 def Nat.is_lt(a: Nat, b: Nat) -> Bool: 729 Cmp.is_lt(Nat.cmp(a, b)) 730 731 def Nat.is_eq(a: Nat, b: Nat) -> Bool: 732 Cmp.is_eq(Nat.cmp(a, b)) 733 734 def Nat.is_ne(a: Nat, b: Nat) -> Bool: 735 Bool.not(Cmp.is_eq(Nat.cmp(a, b))) 736 737 def Nat.is_le(a: Nat, b: Nat) -> Bool: 738 Cmp.is_le(Nat.cmp(a, b)) 739 740 def Nat.is_gt(a: Nat, b: Nat) -> Bool: 741 Cmp.is_gt(Nat.cmp(a, b)) 742 743 def Nat.is_ge(a: Nat, b: Nat) -> Bool: 744 Cmp.is_ge(Nat.cmp(a, b)) 745 746 def 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 755 def 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 764 law Nat.ge_refl: 765 for a: Nat 766 {Nat.is_ge(a, a) == True{} : Bool} 767 768 def Nat.ge_refl(a): 769 match a: 770 case 0n: 771 {==} 772 case 1n+p: 773 Nat.ge_refl(p) 774 775 law Nat.max_ge_l: 776 for +a: Nat 777 for +b: Nat 778 {Nat.is_ge(Nat.max(a, b), a) == True{} : Bool} 779 780 def 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 791 law Nat.max_ge_r: 792 for +a: Nat 793 for +b: Nat 794 {Nat.is_ge(Nat.max(a, b), b) == True{} : Bool} 795 796 def 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 805 def Nat.div(a: Nat, b: Nat) -> Nat: 806 Pair.fst(Nat, Nat, Nat.divmod(a, b)) 807 808 def Nat.mod(a: Nat, b: Nat) -> Nat: 809 Pair.snd(Nat, Nat, Nat.divmod(a, b)) 810 811 def 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 821 def Maybe.pure(a, -A: Kind(a), x: A) -> Maybe: 822 Some{x} 823 824 def Maybe.bind( 825 a, -A: Kind(a), -B: Kind(a), m: Maybe, f: A -> Maybe 826 ) -> Maybe: 827 match m: 828 case None{}: 829 None{} 830 case Some{x}: 831 f(x) 832 833 def Maybe.default(a, -A: Kind(a), m: Maybe, d: A) -> A: 834 match m: 835 case None{}: 836 d 837 case Some{x}: 838 x 839 840 def Maybe.is_some(a, -A: Kind(a), m: Maybe) -> Bool: 841 match m: 842 case None{}: 843 False{} 844 case Some{x}: 845 True{} 846 847 def Maybe.is_none(a, -A: Kind(a), m: Maybe) -> Bool: 848 Bool.not(Maybe.is_some(a, A, m)) 849 850 def Maybe.map( 851 a, -A: Kind(a), -B: Kind(a), f: A -> B, m: Maybe 852 ) -> Maybe: 853 match m: 854 case None{}: 855 None{} 856 case Some{x}: 857 Some{f(x)} 858 859 def Maybe.or(a, -A: Kind(a), m: Maybe, n: Maybe) -> Maybe: 860 match m: 861 case None{}: 862 n 863 case Some{x}: 864 Some{x} 865 866 # Result 867 # ------ 868 869 def Result.pure(a, b, -E: Kind(a), -A: Kind(b), x: A) -> Result: 870 Done{x} 871 872 def Result.bind( 873 a, b, -E: Kind(a), -A: Kind(b), -B: Kind(b), r: Result, 874 f: A -> Result 875 ) -> Result: 876 match r: 877 case Fail{e}: 878 Fail{e} 879 case Done{x}: 880 f(x) 881 882 def Result.default( 883 a, b, -E: Kind(a), -A: Kind(b), r: Result, d: A 884 ) -> A: 885 match r: 886 case Fail{e}: 887 d 888 case Done{x}: 889 x 890 891 def Result.is_done( 892 a, b, -E: Kind(a), -A: Kind(b), r: Result 893 ) -> Bool: 894 match r: 895 case Fail{e}: 896 False{} 897 case Done{x}: 898 True{} 899 900 def Result.is_fail( 901 a, b, -E: Kind(a), -A: Kind(b), r: Result 902 ) -> Bool: 903 Bool.not(Result.is_done(a, b, E, A, r)) 904 905 def Result.map( 906 a, b, -E: Kind(a), -A: Kind(b), -B: Kind(b), f: A -> B, 907 r: Result 908 ) -> Result: 909 match r: 910 case Fail{e}: 911 Fail{e} 912 case Done{x}: 913 Done{f(x)} 914 915 # List 916 # ---- 917 918 def List.map(~A: Type, ~B: Type, ~f: A -> B, xs: List) -> List: 919 match xs: 920 case Nil{}: 921 Nil{} 922 case h <> t: 923 f(h) <> List.map(~A, ~B, ~f, t) 924 925 def List.length(a, -A: Kind(a), xs: List) -> Nat: 926 match xs: 927 case Nil{}: 928 0n 929 case h <> t: 930 1n+List.length(a, A, t) 931 932 def List.append(a, -A: Kind(a), xs: List, ys: List) -> List: 933 match xs: 934 case Nil{}: 935 ys 936 case h <> t: 937 h <> List.append(a, A, t, ys) 938 939 def List.concat(a, -A: Kind(a), xss: List>) -> List: 940 match xss: 941 case Nil{}: 942 Nil{} 943 case h <> t: 944 List.append(a, A, h, List.concat(a, A, t)) 945 946 def List.reverse.go(a, -A: Kind(a), xs: List, acc: List) -> 947 List: 948 match xs: 949 case Nil{}: 950 acc 951 case h <> t: 952 List.reverse.go(a, A, t, h <> acc) 953 954 def List.reverse(a, -A: Kind(a), xs: List) -> List: 955 List.reverse.go(a, A, xs, Nil{}) 956 957 def List.is_empty(a, -A: Kind(a), xs: List) -> Bool: 958 match xs: 959 case Nil{}: 960 True{} 961 case h <> t: 962 False{} 963 964 def List.head(a, -A: Kind(a), xs: List) -> Maybe: 965 match xs: 966 case Nil{}: 967 None{} 968 case h <> t: 969 Some{h} 970 971 def List.tail(a, -A: Kind(a), xs: List) -> List: 972 match xs: 973 case Nil{}: 974 Nil{} 975 case h <> t: 976 t 977 978 def List.last.go(a, -A: Kind(a), xs: List, last: A) -> A: 979 match xs: 980 case Nil{}: 981 last 982 case h <> t: 983 List.last.go(a, A, t, h) 984 985 def List.last(a, -A: Kind(a), xs: List) -> Maybe: 986 match xs: 987 case Nil{}: 988 None{} 989 case h <> t: 990 Some{List.last.go(a, A, t, h)} 991 992 def List.get(a, -A: Kind(a), xs: List, n: Nat) -> Maybe: 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 1001 def List.set(a, -A: Kind(a), xs: List, n: Nat, x: A) -> List: 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 1010 def List.take(a, -A: Kind(a), xs: List, n: Nat) -> List: 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 1019 def List.drop(a, -A: Kind(a), xs: List, n: Nat) -> List: 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 1028 def List.zip( 1029 a, -A: Kind(a), b, -B: Kind(b), xs: List, ys: List 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 1039 def 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 1046 def List.range(n: Nat) -> List<&2, Nat>: 1047 List.range.go(n, Nil{}) 1048 1049 def 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 1056 def 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 1063 def 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 1070 def List.foldl( 1071 ~a: Quant, ~A: Kind(a), ~B: Type, ~f: B -> A -> B, xs: List, 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 1079 def List.foldr( 1080 ~a: Quant, ~A: Kind(a), ~B: Type, ~f: A -> B -> B, xs: List, 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. 1089 def List.any.if(rest: Unit -> Bool, hit: Bool) -> Bool: 1090 match hit: 1091 case False{}: 1092 rest(Unit{}) 1093 case True{}: 1094 True{} 1095 1096 def List.any(~a: Quant, ~A: Kind(a), ~f: A -> Bool, xs: List) -> 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 1103 def List.all.if(rest: Unit -> Bool, hit: Bool) -> Bool: 1104 match hit: 1105 case False{}: 1106 False{} 1107 case True{}: 1108 rest(Unit{}) 1109 1110 def List.all(~a: Quant, ~A: Kind(a), ~f: A -> Bool, xs: List) -> 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 1117 def 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 1124 def 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 1131 def 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 1140 def 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. 1151 def 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 1172 def 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 1179 def 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 1191 def 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 1207 def 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 1216 def List.for_each( 1217 ~a: Quant, ~A: Kind(a), ~f: A -> IO(Unit), xs: List 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 1228 def 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 1235 def 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 1244 def 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 1253 def 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 1262 def 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 1271 def 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 1280 def 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 1289 def 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 1293 def 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 1302 def 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 1311 def 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 1320 def 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 1329 def 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 1338 def 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 1349 law 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 1357 def 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 1362 def 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 1373 def Word.add(n: Nat, a: Word(n), b: Word(n)) -> Word(n): 1374 Word.adc(n, a, b, False{}, False{}) 1375 1376 def Word.sub(n: Nat, a: Word(n), b: Word(n)) -> Word(n): 1377 Word.adc(n, a, b, True{}, True{}) 1378 1379 law 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

} 1387 1388 law 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 1395 def 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 1400 def 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 1425 law 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 1431 def Word.add_comm(n, a, b): 1432 Word.add_comm.go(n, a, b, False{}) 1433 1434 def 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 1445 def 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 1457 def 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 1463 def U32.inc(a: U32) -> U32: 1464 match a: 1465 case U32{x}: 1466 U32{Word.inc(32n, x)} 1467 1468 def 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 1473 law U32.add_comm: 1474 for a: U32 1475 for b: U32 1476 {U32.add(a, b) == U32.add(b, a) : U32} 1477 1478 def 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 1484 def 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 1489 def 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 1494 def U32.not(a: U32) -> U32: 1495 match a: 1496 case U32{x}: 1497 U32{Word.not(32n, x)} 1498 1499 def 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 1504 def 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 1509 def 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 1514 def U32.shl(a: U32) -> U32: 1515 match a: 1516 case U32{x}: 1517 U32{Word.shl(32n, x)} 1518 1519 def U32.shr(a: U32) -> U32: 1520 match a: 1521 case U32{x}: 1522 U32{Word.shr(32n, x)} 1523 1524 def 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 1531 def 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 1538 def U32.cmp(a: U32, b: U32) -> Cmp: 1539 match a b: 1540 case U32{x} U32{y}: 1541 Word.cmp(32n, x, y) 1542 1543 def U32.is_eq(a: U32, b: U32) -> Bool: 1544 Cmp.is_eq(U32.cmp(a, b)) 1545 1546 def U32.is_ne(a: U32, b: U32) -> Bool: 1547 Bool.not(Cmp.is_eq(U32.cmp(a, b))) 1548 1549 def U32.is_lt(a: U32, b: U32) -> Bool: 1550 Cmp.is_lt(U32.cmp(a, b)) 1551 1552 def U32.is_le(a: U32, b: U32) -> Bool: 1553 Cmp.is_le(U32.cmp(a, b)) 1554 1555 def U32.is_gt(a: U32, b: U32) -> Bool: 1556 Cmp.is_gt(U32.cmp(a, b)) 1557 1558 def U32.is_ge(a: U32, b: U32) -> Bool: 1559 Cmp.is_ge(U32.cmp(a, b)) 1560 1561 def U32.is_zero(a: U32) -> Bool: 1562 U32.is_eq(a, 0) 1563 1564 def U32.to_nat(a: U32) -> Nat: 1565 match a: 1566 case U32{w}: 1567 Word.to_nat(32n, w) 1568 1569 def 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 1576 def 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 1585 def U32.log2(n: U32) -> Nat: 1586 U32.log2.go(5n, n, 0n) 1587 1588 def 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 1596 def 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 1602 def 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 1608 def 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 1615 def U32.div.fin(qr: Word(32n) & U32) -> U32: 1616 (q, r) = qr 1617 U32{q} 1618 1619 def 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 1626 def 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 1631 def U32.mod.fin(qr: Word(32n) & U32) -> U32: 1632 (q, r) = qr 1633 r 1634 1635 def 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 1642 def 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 1647 def 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 1652 def 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 1657 def U32.clamp(x: U32, lo: U32, hi: U32) -> U32: 1658 U32.min(U32.max(x, lo), hi) 1659 1660 def 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 1667 def U32.is_even(a: U32) -> Bool: 1668 U32.is_zero(U32.and(a, 1)) 1669 1670 # F32 1671 # --- 1672 1673 law U32.to_f32: 1674 for a: U32 1675 F32 1676 1677 law F32.to_u32: 1678 for a: F32 1679 U32 1680 1681 law F32.add: 1682 for a: F32 1683 for b: F32 1684 F32 1685 1686 law F32.sub: 1687 for a: F32 1688 for b: F32 1689 F32 1690 1691 law F32.mul: 1692 for a: F32 1693 for b: F32 1694 F32 1695 1696 law F32.div: 1697 for a: F32 1698 for b: F32 1699 F32 1700 1701 law F32.mod: 1702 for a: F32 1703 for b: F32 1704 F32 1705 1706 law F32.pow: 1707 for a: F32 1708 for b: F32 1709 F32 1710 1711 law F32.atan2: 1712 for a: F32 1713 for b: F32 1714 F32 1715 1716 law F32.neg: 1717 for a: F32 1718 F32 1719 1720 law F32.abs: 1721 for a: F32 1722 F32 1723 1724 law F32.sqrt: 1725 for a: F32 1726 F32 1727 1728 law F32.exp: 1729 for a: F32 1730 F32 1731 1732 law F32.log: 1733 for a: F32 1734 F32 1735 1736 law F32.log2: 1737 for a: F32 1738 F32 1739 1740 law F32.log10: 1741 for a: F32 1742 F32 1743 1744 law F32.sin: 1745 for a: F32 1746 F32 1747 1748 law F32.cos: 1749 for a: F32 1750 F32 1751 1752 law F32.tan: 1753 for a: F32 1754 F32 1755 1756 law F32.asin: 1757 for a: F32 1758 F32 1759 1760 law F32.acos: 1761 for a: F32 1762 F32 1763 1764 law F32.atan: 1765 for a: F32 1766 F32 1767 1768 law F32.sinh: 1769 for a: F32 1770 F32 1771 1772 law F32.cosh: 1773 for a: F32 1774 F32 1775 1776 law F32.tanh: 1777 for a: F32 1778 F32 1779 1780 law F32.floor: 1781 for a: F32 1782 F32 1783 1784 law F32.ceil: 1785 for a: F32 1786 F32 1787 1788 law F32.trunc: 1789 for a: F32 1790 F32 1791 1792 law F32.is_eq: 1793 for a: F32 1794 for b: F32 1795 Bool 1796 1797 law F32.is_ne: 1798 for a: F32 1799 for b: F32 1800 Bool 1801 1802 law F32.is_lt: 1803 for a: F32 1804 for b: F32 1805 Bool 1806 1807 law F32.is_le: 1808 for a: F32 1809 for b: F32 1810 Bool 1811 1812 law F32.is_gt: 1813 for a: F32 1814 for b: F32 1815 Bool 1816 1817 law F32.is_ge: 1818 for a: F32 1819 for b: F32 1820 Bool 1821 1822 law F32.show: 1823 for a: F32 1824 String 1825 1826 law F32.bits: 1827 for a: F32 1828 U32 1829 1830 law F32.read: 1831 for s: String 1832 Maybe<&2, F32> 1833 1834 def 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 1839 def 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 1844 def 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. 1851 def 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 1856 def 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 1863 def 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 1870 def 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. 1877 def 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. 1892 def 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 1899 def 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 1906 def F32.pi() -> F32: 1907 3.14159265 1908 1909 def 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. 1914 def 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 1923 def 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 1933 def 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 1938 def Char.to_u32(c: Char) -> U32: 1939 match c: 1940 case Chr{x}: 1941 x 1942 1943 def Char.from_u32(x: U32) -> Char: 1944 Chr{x} 1945 1946 def 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 1951 def 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 1956 def 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 1961 def 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 1966 def Char.is_alpha(+c: Char) -> Bool: 1967 Bool.or(Char.is_upper(c), Char.is_lower(c)) 1968 1969 def 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 1974 def 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 1979 def 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 1987 def 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 1994 def 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 1999 law String.cmp: 2000 for a: String Lines 1-2000 of 3210. More: https://jend.leeeet.dev/read.txt?path=Base/base.bend&start_line=2001