base.tri (20558B)
1 !import native_math as N 2 !export * 3 -- 1. t t a b -> a 4 -- 2. t (t a) b c -> a c (b c) 5 -- 3a. t (t a b) c t -> a 6 -- 3b. t (t a b) c (t u) -> b u 7 -- 3c. t (t a b) c (t u v) -> c u v 8 9 false = t 10 _ = t 11 true = t t 12 id a = a 13 const a b = a 14 pair = t 15 if cond then else = t (t else (t t then)) t cond 16 17 y = ((mut wait fun : wait mut (x : fun (wait mut x))) 18 (x : x x) 19 (a0 a1 a2 : t (t a0) (t t a2) a1)) 20 21 compose f g x = f (g x) 22 23 triage leaf stem fork = t (t leaf stem) fork 24 test = triage "Leaf" (_ : "Stem") (_ _ : "Fork") 25 26 matchBool = (onTrue onFalse : triage 27 onFalse 28 (_ : onTrue) 29 (_ _ : onTrue) 30 ) 31 32 lAnd = (triage 33 (_ : false) 34 (_ x : x) 35 (_ _ x : x)) 36 37 lOr = (triage 38 (x : x) 39 (_ _ : true) 40 (_ _ _ : true)) 41 42 matchPair a = triage _ _ a 43 44 fst p = matchPair takeFirst p 45 where takeFirst a b = a 46 snd p = matchPair takeSecond p 47 where takeSecond a b = b 48 49 resultIsOk result = 50 matchResult (errR rest : false) (val rest : true) result 51 52 resultIsErr result = 53 matchResult (errR rest : true) (val rest : false) result 54 55 not? = matchBool false true 56 and? = matchBool id (_ : false) 57 58 -- Normalize truthiness without inspecting the right argument after success. 59 or? left right = matchBool true (matchBool true false right) left 60 61 xor? = (x z : 62 matchBool 63 (matchBool false true z) 64 (matchBool true false z) 65 x) 66 67 equal? = y (self : triage 68 (triage 69 true 70 (_ : false) 71 (_ _ : false)) 72 (ax : 73 triage 74 false 75 (self ax) 76 (_ _ : false)) 77 (ax ay : 78 triage 79 false 80 (_ : false) 81 (bx by : lAnd (self ax bx) (self ay by)))) 82 83 -- Unchecked successor for internal canonical-natural loops. 84 succ = N.successor 85 86 ok value rest = pair true (pair value rest) 87 err msg rest = pair false (pair msg rest) 88 89 matchResult errCase okCase result = 90 matchPair 91 (tag payload : 92 matchPair 93 (value rest : 94 matchBool 95 (okCase value rest) 96 (errCase value rest) 97 tag) 98 payload) 99 result 100 101 -- --------------------------------------------------------------------------- 102 -- Maybe / Option type 103 -- --------------------------------------------------------------------------- 104 105 nothing = t 106 just x = t x 107 108 matchMaybe nothingCase justCase maybe = 109 triage 110 nothingCase 111 justCase 112 (_ _ : nothingCase) 113 maybe 114 115 maybe default f m = matchMaybe default f m 116 maybeMap f m = matchMaybe nothing (x : just (f x)) m 117 maybeBind m f = matchMaybe nothing f m 118 maybeOr default m = matchMaybe default id m 119 maybe? = matchMaybe false (_ : true) 120 121 -- --------------------------------------------------------------------------- 122 -- Lazy eliminators 123 -- 124 -- Explicit branch thunks: the selected continuation receives Leaf. 125 -- Keep these where probes establish demand or construction benefits. Ordinary 126 -- eliminators are not intrinsically strict in both branches; inspect demand 127 -- rather than inferring it from syntax, especially when reifying function trees. 128 -- --------------------------------------------------------------------------- 129 130 lazyBool = (thenK elseK cond : 131 ((chosen : chosen t) 132 (matchBool 133 thenK 134 elseK 135 cond))) 136 137 -- `triage` selects a thunk directly: a cons is a Fork, so the cons case sits 138 -- in the fork slot, exactly as in `matchList` below. 139 lazyList = (nilK consK xs : 140 ((chosen : chosen t) 141 (triage 142 nilK 143 _ 144 (h r : (_ : consK h r)) 145 xs))) 146 147 lazyMaybe = (noneK someK m : 148 ((chosen : chosen t) 149 (matchMaybe 150 noneK 151 (x : (_ : someK x)) 152 m))) 153 154 lazyResult = (errK okK result : 155 ((chosen : chosen t) 156 (matchResult 157 (code rest : (_ : errK code rest)) 158 (value rest : (_ : okK value rest)) 159 result))) 160 161 -- --------------------------------------------------------------------------- 162 -- Basic arithmetic 163 -- --------------------------------------------------------------------------- 164 165 ifLazy = (cond thenK elseK : 166 matchBool 167 (thenK t) 168 (elseK t) 169 cond) 170 171 andLazy? = (a bK : 172 ifLazy 173 a 174 bK 175 (_ : false)) 176 177 -- Raw predicates/workers have a canonical-natural precondition; the public 178 -- annotated facade checks input/output contracts. Share one binary engine. 179 pred_ = N.predecessor 180 pred @nat? =@nat? pred_ 181 isZero_? = N.zero 182 isZero? @nat? =@bool? isZero_? 183 add @nat? @nat? =@nat? N.add 184 sub @nat? @nat? =@nat? N.subtract 185 lte_? = N.lte 186 lte? @nat? @nat? =@bool? lte_? 187 gte_? = N.gte 188 gte? @nat? @nat? =@bool? gte_? 189 lt_? = N.lt 190 lt? @nat? @nat? =@bool? lt_? 191 gt_? = N.gt 192 gt? @nat? @nat? =@bool? gt_? 193 mul @nat? @nat? =@nat? N.multiply 194 195 -- Division by zero is a boundary error, not a plausible numeric answer. 196 -- divMod shares the division pass when callers need both outputs. 197 divMod @nat? @nonZero? =@(pairOf nat? nat?) N.divMod 198 div @nat? @nonZero? =@nat? N.quotient 199 mod @nat? @nonZero? =@nat? N.remainder 200 pow @nat? @nat? =@nat? N.power 201 even? = N.even 202 odd? = N.odd 203 min @nat? @nat? =@nat? N.minimum 204 max @nat? @nat? =@nat? N.maximum 205 206 -- --------------------------------------------------------------------------- 207 -- Result combinators 208 -- --------------------------------------------------------------------------- 209 210 mapResult = (f result : 211 matchResult 212 (code rest : err code rest) 213 (value rest : ok (f value) rest) 214 result) 215 216 bindResult = (result f : 217 matchResult 218 (code rest : err code rest) 219 (value rest : f value rest) 220 result) 221 222 resultOr = (default result : 223 matchResult 224 (_ _ : default) 225 (value _ : value) 226 result) 227 228 resultMapErr = (f result : 229 matchResult 230 (code rest : err (f code) rest) 231 (value rest : ok value rest) 232 result) 233 234 -- --------------------------------------------------------------------------- 235 -- List 236 -- --------------------------------------------------------------------------- 237 238 matchList = a b : triage a _ b 239 240 emptyList? = matchList true (_ _ : false) 241 head xs@(nonEmptyListOf anyC) =@anyC matchList t (h _ : h) xs 242 tail xs@(nonEmptyListOf anyC) =@(listOf anyC) matchList t (_ r : r) xs 243 244 append xs ys = (let rec 245 walk xs = (matchList 246 ys 247 (h r : pair h (walk r)) 248 xs) 249 in walk xs) 250 251 lExist? x xs = (let rec 252 walk xs = (matchList 253 false 254 (h r : or? (equal? x h) (walk r)) 255 xs) 256 in walk xs) 257 258 -- Keep these eliminators: patterned traversal has higher measured runtime and 259 -- allocation costs here. Local workers capture callbacks rather than threading 260 -- them through every recursive call. 261 map f xs = (let rec 262 walk remaining = (matchList 263 t 264 (h r : pair (f h) (walk r)) 265 remaining) 266 in walk xs) 267 268 filter f xs = (let rec 269 walk remaining = (matchList 270 t 271 (h r : matchBool (pair h (walk r)) (walk r) (f h)) 272 remaining) 273 in walk xs) 274 275 foldl f initial xs = (let rec 276 walk remaining acc = (matchList 277 acc 278 (h r : walk r (f acc h)) 279 remaining) 280 in walk xs initial) 281 282 -- Like foldl, the callback receives accumulator first, element second. 283 foldr f initial xs = (let rec 284 walk remaining = (matchList 285 initial 286 (h r : f (walk r) h) 287 remaining) 288 in walk xs) 289 290 length xs@(listOf anyC) =@nat? (let rec 291 walk xs = (matchList 292 0 293 (_ r : succ (walk r)) 294 xs) 295 in walk xs) 296 297 reverse xs = (let rec 298 walk remaining acc = (matchList 299 acc 300 (h r : walk r (pair h acc)) 301 remaining) 302 in walk xs t) 303 304 snoc x xs = (let rec 305 walk xs = (matchList 306 (pair x t) 307 (h r : pair h (walk r)) 308 xs) 309 in walk xs) 310 311 count x xs = (let rec 312 walk xs = (matchList 313 0 314 (h r : 315 matchBool 316 (succ (walk r)) 317 (walk r) 318 (equal? x h)) 319 xs) 320 in walk xs) 321 322 last xs@(nonEmptyListOf anyC) =@anyC (let rec 323 walk xs = (matchList 324 t 325 (h r : 326 matchBool 327 h 328 (walk r) 329 (emptyList? r)) 330 xs) 331 in walk xs) 332 333 all? pred xs = (let rec 334 walk xs = (matchList 335 true 336 (h r : and? (pred h) (walk r)) 337 xs) 338 in walk xs) 339 340 any? pred xs = (let rec 341 walk xs = (matchList 342 false 343 (h r : or? (pred h) (walk r)) 344 xs) 345 in walk xs) 346 347 intersect = xs ys : filter (x : lExist? x ys) xs 348 349 nth n xs = (let rec 350 walk xs i = (matchList 351 t 352 (h r : 353 matchBool 354 h 355 (walk r (succ i)) 356 (equal? i n)) 357 xs) 358 in walk xs 0) 359 360 headMaybe = matchList nothing (h _ : just h) 361 362 lastMaybe xs = (let rec 363 walk xs = (matchList 364 nothing 365 (h r : 366 matchBool 367 (just h) 368 (walk r) 369 (emptyList? r)) 370 xs) 371 in walk xs) 372 373 nthMaybe n xs = (let rec 374 walk xs i = (matchList 375 nothing 376 (h r : 377 matchBool 378 (just h) 379 (walk r (succ i)) 380 (equal? i n)) 381 xs) 382 in walk xs 0) 383 384 -- Stop before inspecting another cell once the requested prefix is complete. 385 take n xs = (let rec 386 walk remaining i = (matchBool 387 t 388 (matchList t (h r : pair h (walk r (succ i))) remaining) 389 (equal? i n)) 390 in walk xs 0) 391 392 drop n xs = (let rec 393 walk xs i = (matchBool 394 xs 395 (matchList 396 t 397 (_ r : walk r (succ i)) 398 xs) 399 (equal? i n)) 400 in walk xs 0) 401 402 splitAt = n xs : pair (take n xs) (drop n xs) 403 404 concatMap f xs = (let rec 405 walk xs = (matchList 406 t 407 (h r : append (f h) (walk r)) 408 xs) 409 in walk xs) 410 411 find pred xs = (let rec 412 walk xs = (matchList 413 nothing 414 (h r : 415 matchBool 416 (just h) 417 (walk r) 418 (pred h)) 419 xs) 420 in walk xs) 421 422 partition pred xs = (let rec 423 walk xs trues falses = (matchList 424 (pair (reverse trues) (reverse falses)) 425 (h r : 426 matchBool 427 (walk r (pair h trues) falses) 428 (walk r trues (pair h falses)) 429 (pred h)) 430 xs) 431 in walk xs t t) 432 433 strLength = length 434 strAppend = append 435 strEq? = equal? 436 strEmpty? = emptyList? 437 438 startsWith? prefix input = (let rec 439 walk prefix input = (matchList 440 true 441 (ph pr : 442 matchList 443 false 444 (sh sr : 445 matchBool 446 (walk pr sr) 447 false 448 (equal? ph sh)) 449 input) 450 prefix) 451 in walk prefix input) 452 453 endsWith? = prefix str : startsWith? (reverse prefix) (reverse str) 454 455 contains? needle haystack = (let rec 456 walk haystack = (matchBool 457 true 458 (matchList 459 false 460 (_ r : walk r) 461 haystack) 462 (startsWith? needle haystack)) 463 in walk haystack) 464 465 sum @(listOf nat?) =@nat? foldl (acc x : add x acc) 0 466 product @(listOf nat?) =@nat? foldl (acc x : mul x acc) 1 467 468 -- --------------------------------------------------------------------------- 469 -- Generic separators 470 -- 471 -- `lines`, `unlines`, `words` and `unwords` at the bottom of this section are 472 -- the byte-valued special cases of these primitives. 473 -- 474 -- Joining takes any separator; splitting takes one byte. Separators are removed 475 -- rather than kept, and empty fields are preserved. 476 -- --------------------------------------------------------------------------- 477 478 takeWhile f xs = (let rec 479 walk remaining = (lazyList 480 (_ : t) 481 (h r : case f h of 482 t = t 483 _ = pair h (walk r)) 484 remaining) 485 in walk xs) 486 487 dropWhile f xs = (let rec 488 walk remaining = (lazyList 489 (_ : t) 490 (h r : case f h of 491 t = pair h r 492 _ = walk r) 493 remaining) 494 in walk xs) 495 496 -- Byte-level whitespace only: space and horizontal tab (HTTP OWS). 497 spaceByte? = b : equal? b 32 498 tabByte? = b : equal? b 9 499 trimByte? = b : or? (spaceByte? b) (tabByte? b) 500 501 trim = xs : dropWhile trimByte? (reverse (dropWhile trimByte? (reverse xs))) 502 503 intercalate sep xs = (let rec 504 walk remaining = (lazyList 505 (_ : t) 506 (h r : case emptyList? r of 507 t = append h (append sep (walk r)) 508 _ = h) 509 remaining) 510 in walk xs) 511 512 -- Separator after every field, including the last one. Line-oriented formats 513 -- want this: `joinSuffix "\n" xs` terminates the final line while 514 -- `intercalate "\n" xs` does not. 515 joinSuffix sep xs = (let rec 516 walk remaining = (lazyList 517 (_ : t) 518 (h r : append (append h sep) (walk r)) 519 remaining) 520 in walk xs) 521 522 -- Split on a single byte. 523 -- Empty fields are preserved: `splitOnByte 58 "a::b"` is ["a" "" "b"]. 524 -- Keep the two small thunks here: case dispatch and extra local branch 525 -- bindings both add measurable per-byte costs in the splitter. 526 splitOnByte byte str = (let rec 527 walk remaining reversedFields reversedField = (lazyList 528 (_ : map reverse (reverse (pair reversedField reversedFields))) 529 (h r : lazyBool 530 (_ : walk r (pair reversedField reversedFields) t) 531 (_ : walk r reversedFields (pair h reversedField)) 532 (equal? h byte)) 533 remaining) 534 in walk str t t) 535 536 -- Every one of these keeps its arguments bound: partially applying a 537 -- multi-argument function at the top level leaves a fixed point exposed. 538 lines = str : splitOnByte 10 str 539 unlines = xs : joinSuffix "\n" xs 540 541 -- Runs of separators collapse: empty fields are dropped. 542 words = str : filter (w : not? (emptyList? w)) (splitOnByte 32 str) 543 unwords = xs : intercalate " " xs 544 545 zipWith f xs ys = (let rec 546 walk xs ys = (matchList 547 t 548 (xh xt : 549 matchList 550 t 551 (yh yt : pair (f xh yh) (walk xt yt)) 552 ys) 553 xs) 554 in walk xs ys) 555 556 -- --------------------------------------------------------------------------- 557 -- Core contract type 558 -- 559 -- A contract is an ordinary tricu function: Tree -> Tree -> Result Tree Tree. 560 -- The second argument is the conventional "rest" slot. On success a contract 561 -- returns the checked value wrapped in the standard ok shape; on failure it 562 -- returns a diagnostic wrapped in the standard err shape. 563 -- 564 -- Kernel policies are ordinary compiled functions, not dynamic runner settings. 565 -- withContract uses the compiled kernel binding; callers needing a different 566 -- policy can apply it explicitly to checkContract's Result. 567 -- --------------------------------------------------------------------------- 568 569 contractOk = (value : (rest : ok value rest)) 570 contractErr = (msg : (rest : err msg rest)) 571 572 -- Default contract kernel. Return the contract Result unchanged. 573 defaultKernel = (contract value result : 574 matchResult 575 (msg rest : err msg rest) 576 (v rest : ok v rest) 577 result) 578 579 -- Default policy selected when this module is compiled. 580 kernel = defaultKernel 581 582 -- Skip-everything kernel. Resume with the original value on failure. 583 skipKernel = (contract value result : 584 matchResult 585 (msg rest : ok value rest) 586 (v rest : ok v rest) 587 result) 588 589 -- Apply a contract and pass the raw Result to the kernel. 590 withContract = (contract value : 591 kernel contract value (contract value t)) 592 593 -- Apply a contract and return the checked value or the diagnostic message. 594 check contract value = 595 matchResult 596 (msg _ : msg) 597 (v _ : v) 598 (withContract contract value) 599 600 -- Apply a contract and return the raw Result (kernel is bypassed). 601 checkContract = (contract value : contract value t) 602 603 -- --------------------------------------------------------------------------- 604 -- Basic contracts 605 -- --------------------------------------------------------------------------- 606 607 -- Any value passes. 608 anyC = (value : contractOk value) 609 610 -- Always fails with the supplied message. 611 neverC = (msg : (value : contractErr msg)) 612 613 -- Build a contract from a predicate that inspects only the value. 614 guardC msg predicate value rest = case predicate value of 615 t = contractErr msg rest 616 _ = contractOk value rest 617 618 -- Canonical compact naturals: exact Boolean bits, with no redundant high zero. 619 -- Zero is Leaf; a nonzero numeral ends in Fork (Stem Leaf) Leaf. 620 -- This boundary agrees with arithmetic/zero tests and native_math inputs. 621 isNat? n = (triage 622 true 623 (_ : false) 624 (bit rest : case bit of 625 t = (case rest of 626 t = false 627 _ = isNat? rest) 628 (t t) = isNat? rest 629 _ = false) 630 n) 631 632 -- Natural number contract. 633 nat? = guardC "not a natural number" isNat? 634 635 -- Non-zero natural number contract. 636 nonZero? = guardC "non-zero" (n : and? (isNat? n) (not? (isZero_? n))) 637 638 -- Boolean contract. 639 bool? = guardC "not a boolean" (b : or? (equal? b true) (equal? b false)) 640 641 -- --------------------------------------------------------------------------- 642 -- Contract combinators 643 -- --------------------------------------------------------------------------- 644 645 andC = (c1 c2 value rest : 646 matchResult 647 (msg _ : contractErr msg rest) 648 (v _ : c2 v rest) 649 (c1 value rest)) 650 651 orC = (c1 c2 value rest : 652 matchResult 653 (msg _ : c2 value rest) 654 (v _ : contractOk v rest) 655 (c1 value rest)) 656 657 notC = (c value rest : 658 matchResult 659 (msg _ : contractOk value rest) 660 (_ _ : contractErr "notC: predicate succeeded" rest) 661 (c value rest)) 662 663 mapC = (f c value rest : 664 matchResult 665 (msg _ : contractErr msg rest) 666 (v _ : contractOk (f v) rest) 667 (c value rest)) 668 669 bindC = (c f value rest : 670 matchResult 671 (msg _ : contractErr msg rest) 672 (v _ : f v value rest) 673 (c value rest)) 674 675 -- --------------------------------------------------------------------------- 676 -- Collection contracts 677 -- --------------------------------------------------------------------------- 678 679 -- Preserve accepted/transformed elements, including higher-order proxies. 680 -- Reject improper tails explicitly; input shape failures use the Result protocol. 681 listOf c value rest = (let rec 682 walk remaining reversed = (triage 683 (contractOk (reverse reversed) rest) 684 (_ : contractErr "not a list" rest) 685 (item tail : matchResult 686 (message _ : contractErr message rest) 687 (checked _ : walk tail (pair checked reversed)) 688 (c item rest)) 689 remaining) 690 in walk value t) 691 692 nonEmptyListOf c value rest = case value of 693 [] = contractErr "empty list" rest 694 [_ | _] = listOf c value rest 695 _ = contractErr "not a list" rest 696 697 pairOf c1 c2 value rest = case value of 698 (left, right) = (matchResult 699 (message _ : contractErr message rest) 700 (checkedLeft _ : matchResult 701 (message _ : contractErr message rest) 702 (checkedRight _ : contractOk (pair checkedLeft checkedRight) rest) 703 (c2 right rest)) 704 (c1 left rest)) 705 _ = contractErr "not a pair" rest 706 707 -- --------------------------------------------------------------------------- 708 -- Higher-order function contracts 709 -- 710 -- These return a Result-wrapped proxy. The proxy itself is a contract: it 711 -- checks arguments on the way in and results on the way out. 712 -- --------------------------------------------------------------------------- 713 714 fnContract argC resC f rest = (contractOk proxy rest 715 where 716 proxy argument callRest = (matchResult rejected accepted (withContract argC argument) 717 where 718 rejected message _ = contractErr message callRest 719 accepted checked _ = (matchResult rejected 720 (value _ : contractOk value callRest) 721 (withContract resC (f checked))))) 722 723 -- A curried two-argument proxy is a checked function returning a checked function. 724 fn2 arg1C arg2C resC f rest = fnContract arg1C (fnContract arg2C resC) f rest 725 726 -- --------------------------------------------------------------------------- 727 -- Interaction-tree effect layer 728 -- 729 -- These constructors and combinators layer catchable, composable failures on 730 -- top of the core Result contracts. They reuse the same tags as tricu IO: 731 -- 0 = pureE 732 -- 1 = bindE 733 -- 2 = exceptE 734 -- --------------------------------------------------------------------------- 735 736 pureE = (value : pair 0 value) 737 bindE = (action k : pair 1 (pair action k)) 738 exceptE = (tag value k : pair 2 (pair tag (pair value k))) 739 740 pureM = pureE 741 bindM = bindE 742 743 -- Lift a contract failure into an interaction tree. 744 checkM = (contract value : 745 matchResult 746 (msg _ : exceptE "contract" msg (_ : pureE t)) 747 (checked _ : pureE checked) 748 (contract value t)) 749 750 -- Lift a pure function into the interaction tree. 751 liftM = (f : (x : pureE (f x))) 752 753 -- Interpret a pure interaction tree into a Result. 754 runM tree = (matchPair interpret tree 755 where 756 interpret op payload = case op of 757 0 = contractOk payload t 758 1 = (matchPair 759 (action k : matchResult 760 (msg _ : contractErr msg t) 761 (value _ : runM (k value)) 762 (runM action)) 763 payload) 764 _ = (matchPair 765 (_ detail : matchPair (value _ : contractErr value t) detail) 766 payload)) 767 768 -- Handle matching exceptE nodes by applying the handler to the value and the 769 -- resumption continuation. Non-matching exceptions are left in place. 770 handleM tag handler tree = (let rec 771 handle current = (matchPair interpret current 772 where 773 choose exceptionTag value k = case equal? exceptionTag tag of 774 t = current 775 _ = handle (handler value k) 776 handleException exceptionTag detail = matchPair (choose exceptionTag) detail 777 interpret op payload = case op of 778 0 = current 779 1 = (matchPair 780 (action k : bindE (handle action) (value : handle (k value))) 781 payload) 782 _ = matchPair handleException payload) 783 in handle tree)