e9d0b87564d13695bef695c552e9707710d9147877f9d9dc5282c7335664cc57.tri (5494B)
1 !export compare 2 !export equal 3 !export lt 4 !export lte 5 !export gt 6 !export gte 7 !export inRange 8 !export minimum 9 !export maximum 10 !export zero 11 !export odd 12 !export even 13 !export successor 14 !export predecessor 15 !export add 16 !export subtract 17 !export multiply 18 !export divMod 19 !export quotient 20 !export remainder 21 !export power 22 !export decimal 23 !export ascii 24 !export digit 25 !export letter 26 !export lowerHex 27 !export printable 28 -- Canonical natural numbers only. No validation or contracts on this path. 29 -- Self-contained binary algorithms. Stable direct recursion is the authoring path. 30 -- Subtraction saturates. divMod a 0 = (0,a); public base division rejects zero. 31 32 triage leaf stem fork = t (t leaf stem) fork 33 choose yes no value = triage no (_ : yes) (_ _ : yes) value 34 lazy yes no value = choose yes no value t 35 not value = choose t (t t) value 36 both a b = choose b t a 37 either a b = choose (t t) b a 38 xor a b = choose (not b) b a 39 -- Ordering: Leaf = equal, Stem Leaf = less, Fork Leaf Leaf = greater. 40 bitOrder a b = choose (choose t (t t t) b) (choose (t t) t b) a 41 compare a b = (triage 42 (triage t (_ : t) (_ _ : t t) b) 43 (_ : t) 44 (abit ar : triage (t t t) (_ : t) 45 (bbit br : triage (bitOrder abit bbit) (_ : t t) (_ _ : t t t) 46 (compare ar br)) b) 47 a) 48 isEqual order = triage (t t) (_ : t) (_ _ : t) order 49 isLess order = triage t (_ : t t) (_ _ : t) order 50 isGreater order = triage t (_ : t) (_ _ : t t) order 51 -- Equality may stop at the first differing low bit; ordering cannot. 52 equal a b = (triage 53 (zero b) 54 (_ : t) 55 (abit ar : triage t (_ : t) 56 (bbit br : lazy (_ : t) (_ : equal ar br) (xor abit bbit)) b) 57 a) 58 lt a b = isLess (compare a b) 59 lte a b = not (isGreater (compare a b)) 60 gt a b = isGreater (compare a b) 61 gte a b = not (isLess (compare a b)) 62 inRange value low high = both (gte value low) (lte value high) 63 minimum a b = choose b a (gt a b) 64 maximum a b = choose a b (gt a b) 65 zero value = triage (t t) (_ : t) (_ _ : t) value 66 odd value = triage t (_ : t) (bit rest : bit) value 67 even value = not (odd value) 68 69 -- Discard a redundant high zero bit when rebuilding after subtraction. 70 node bit rest = choose (t bit rest) (choose t (t bit rest) (zero rest)) bit 71 double value = node t value 72 successor value = (triage (t (t t) t) (_ : t) 73 (bit rest : triage (t (t t) rest) (_ : t t (successor rest)) (_ _ : t) bit) value) 74 predecessor value = (triage t (_ : t) 75 (bit rest : lazy (_ : node t rest) (_ : t (t t) (predecessor rest)) bit) value) 76 77 carry a b c = either (both a b) (both c (xor a b)) 78 addCarry a b c = (triage 79 (lazy (_ : successor b) (_ : b) c) 80 (_ : t) 81 (abit ar : triage 82 (lazy (_ : successor a) (_ : a) c) 83 (_ : t) 84 (bbit br : t (xor (xor abit bbit) c) (addCarry ar br (carry abit bbit c))) b) 85 a) 86 add a b = addCarry a b t 87 88 borrow a b c = either (both (not a) b) (both c (not (xor a b))) 89 subtractBorrow a b c = (triage t (_ : t) 90 (abit ar : triage 91 (lazy (_ : predecessor a) (_ : a) c) 92 (_ : t) 93 (bbit br : node (xor (xor abit bbit) c) (subtractBorrow ar br (borrow abit bbit c))) b) 94 a) 95 subtract a b = lazy (_ : t) (_ : subtractBorrow a b t) (lt a b) 96 97 multiply a b = (let rec 98 walk remaining = (triage t (_ : t) 99 (bit rest : lazy 100 (_ : add a (double (walk rest))) 101 (_ : double (walk rest)) bit) 102 remaining) 103 in walk b) 104 105 -- Binary long division: consume high bits first. If r < divisor, then 106 -- 2*r + bit < 2*divisor, so each step needs at most one subtraction. 107 -- Return a pair, sharing quotient/remainder work rather than dividing twice. 108 divMod dividend divisor = (lazy 109 (_ : t t dividend) 110 (_ : let rec 111 walk remaining = (triage 112 (t t t) 113 (_ : t t t) 114 (bit rest : step bit (walk rest)) 115 remaining) 116 in walk dividend) 117 (zero divisor) 118 where 119 step bit partial = (triage t (_ : t) 120 (quot rem : let shifted = node bit rem in lazy 121 (_ : t (double quot) shifted) 122 (_ : t (t (t t) quot) (subtract shifted divisor)) 123 (lt shifted divisor)) 124 partial)) 125 126 quotient a b = triage t (_ : t) (q r : q) (divMod a b) 127 remainder a b = triage t (_ : t) (q r : r) (divMod a b) 128 129 -- Exponentiation by squaring; 0^0 = 1. Do not square an unused final factor. 130 -- Work is bit-directed, but output size can still be enormous. 131 power base exponent = (let rec 132 walk factor remaining acc = (triage 133 acc 134 (_ : acc) 135 (bit rest : let next = lazy (_ : multiply acc factor) (_ : acc) bit in lazy 136 (_ : next) 137 (_ : walk (multiply factor factor) rest next) 138 (zero rest)) 139 remaining) 140 in walk base exponent 1) 141 142 -- Decimal accumulation: value * 10 + digit (digit must be 0..9). 143 decimal value digit = add (add (double (double (double value))) (double value)) digit 144 145 ascii value = lte value 127 146 -- 48..57: high part is 3; low nibble is 0..9. Bit zero is irrelevant. 147 digit (t _ (t b1 (t b2 (t b3 high)))) = 148 both (equal high 3) (not (both b3 (either b2 b1))) 149 digit _ = t 150 -- A..Z/a..z: ignore the case bit; low five bits must be 1..26. 151 letter (t b0 (t b1 (t b2 (t b3 (t b4 (t _ high)))))) = 152 (both (equal high 1) 153 (both (either b0 (either b1 (either b2 (either b3 b4)))) 154 (not (both (both b4 b3) (either b2 (both b1 b0)))))) 155 letter _ = t 156 -- a..f: high part is 12; low three bits are neither zero nor seven. 157 asciiLowerHexLetter (t b0 (t b1 (t b2 high))) = 158 (both (equal high 12) 159 (both (either b0 (either b1 b2)) (not (both b0 (both b1 b2))))) 160 asciiLowerHexLetter _ = t 161 lowerHex value = either (digit value) (asciiLowerHexLetter value) 162 printable value = inRange value 32 126