src/float/bin.bend

bend-lawful-stdlib@0.1.0.0 · 279 lines · 30 definitions

1import Base
2
3# bin.bend: natural numbers in binary, little-endian (lowest bit first).
4#
5#   import ./bin.bend as Bin
6#
7# Nat is unary in the checker, so exact arithmetic on large numbers
8# (a float's 24-bit mantissa, an aligned sum of two floats) overflows it.
9# These numbers compute in the checker in time linear or quadratic in
10# their bit length. Trailing zero bits are allowed; every function reads
11# BZ as zeros, so B0{BZ{}} and BZ{} are the same number.
12
13type Bin is Data:
14  BZ{}
15  B0{r: Bin}
16  B1{r: Bin}
17
18def one() -> Bin:
19  B1{BZ{}}
20
21def is_zero(a: Bin) -> Bool:
22  match a:
23    case BZ{}:
24      True{}
25    case B0{r}:
26      is_zero(r)
27    case B1{r}:
28      False{}
29
30def trim.cons0(t: Bin) -> Bin:
31  match t:
32    case BZ{}:
33      BZ{}
34    case t:
35      B0{t}
36
37# the same number without high zero bits, so equal numbers are equal terms
38def trim(a: Bin) -> Bin:
39  match a:
40    case BZ{}:
41      BZ{}
42    case B0{r}:
43      trim.cons0(trim(r))
44    case B1{r}:
45      B1{trim(r)}
46
47def odd(a: Bin) -> Bool:
48  match a:
49    case B1{r}:
50      True{}
51    case _:
52      False{}
53
54def inc(a: Bin) -> Bin:
55  match a:
56    case BZ{}:
57      B1{BZ{}}
58    case B0{r}:
59      B1{r}
60    case B1{r}:
61      B0{inc(r)}
62
63def cons(s: Bool, r: Bin) -> Bin:
64  match s:
65    case False{}:
66      B0{r}
67    case True{}:
68      B1{r}
69
70def adc.one(a: Bin, c: Bool) -> Bin:
71  match c:
72    case False{}:
73      a
74    case True{}:
75      inc(a)
76
77# a + b + carry, one bit at a time: bits 0+0 pass the carry through and
78# carry nothing, 0+1 flip it and carry it, 1+1 pass it and carry one
79def adc(a: Bin, b: Bin, +c: Bool) -> Bin:
80  match a b:
81    case BZ{} b:
82      adc.one(b, c)
83    case a BZ{}:
84      adc.one(a, c)
85    case B0{x} B0{y}:
86      cons(c, adc(x, y, False{}))
87    case B0{x} B1{y}:
88      cons(Bool.not(c), adc(x, y, c))
89    case B1{x} B0{y}:
90      cons(Bool.not(c), adc(x, y, c))
91    case B1{x} B1{y}:
92      cons(c, adc(x, y, True{}))
93
94def add(a: Bin, b: Bin) -> Bin:
95  adc(a, b, False{})
96
97def dec(a: Bin) -> Bin:
98  match a:
99    case BZ{}:
100      BZ{}
101    case B1{r}:
102      B0{r}
103    case B0{r}:
104      B1{dec(r)}
105
106def sbb.one(a: Bin, w: Bool) -> Bin:
107  match w:
108    case False{}:
109      a
110    case True{}:
111      dec(a)
112
113# a - b - borrow, for a >= b (callers order the operands with cmp first)
114def sbb(a: Bin, b: Bin, +w: Bool) -> Bin:
115  match a b:
116    case a BZ{}:
117      sbb.one(a, w)
118    case BZ{} b:
119      BZ{}
120    case B0{x} B0{y}:
121      cons(w, sbb(x, y, w))
122    case B0{x} B1{y}:
123      cons(Bool.not(w), sbb(x, y, True{}))
124    case B1{x} B0{y}:
125      cons(Bool.not(w), sbb(x, y, False{}))
126    case B1{x} B1{y}:
127      cons(w, sbb(x, y, w))
128
129def sub(a: Bin, b: Bin) -> Bin:
130  sbb(a, b, False{})
131
132def mul(a: Bin, +b: Bin) -> Bin:
133  match a:
134    case BZ{}:
135      BZ{}
136    case B0{r}:
137      B0{mul(r, b)}
138    case B1{r}:
139      add(b, B0{mul(r, b)})
140
141def cmp.fin(p: Bool, q: Bool, hi: Cmp) -> Cmp:
142  match hi:
143    case LT{}:
144      LT{}
145    case EQ{}:
146      Bool.cmp(p, q)
147    case GT{}:
148      GT{}
149
150def cmp(a: Bin, b: Bin) -> Cmp:
151  match a b:
152    case BZ{} BZ{}:
153      EQ{}
154    case BZ{} B0{y}:
155      cmp(BZ{}, y)
156    case BZ{} B1{y}:
157      LT{}
158    case B0{x} BZ{}:
159      cmp(x, BZ{})
160    case B1{x} BZ{}:
161      GT{}
162    case B0{x} B0{y}:
163      cmp.fin(False{}, False{}, cmp(x, y))
164    case B0{x} B1{y}:
165      cmp.fin(False{}, True{}, cmp(x, y))
166    case B1{x} B0{y}:
167      cmp.fin(True{}, False{}, cmp(x, y))
168    case B1{x} B1{y}:
169      cmp.fin(True{}, True{}, cmp(x, y))
170
171# a * 2^n
172def shl(a: Bin, n: Nat) -> Bin:
173  match n:
174    case 0n:
175      a
176    case 1n+k:
177      B0{shl(a, k)}
178
179def pow2(n: Nat) -> Bin:
180  shl(one(), n)
181
182def len.up(l: Nat) -> Nat:
183  match l:
184    case 0n:
185      0n
186    case 1n+k:
187      2n+k
188
189# number of significant bits
190def len(a: Bin) -> Nat:
191  match a:
192    case BZ{}:
193      0n
194    case B0{r}:
195      len.up(len(r))
196    case B1{r}:
197      1n+len(r)
198
199# a / 2^k, with the last bit shifted out (round) and whether any bit
200# below it was set (sticky); r and s are the bits already shifted out
201def shr(k: Nat, a: Bin, r: Bool, s: Bool) -> Bin & Bool & Bool:
202  match k:
203    case 0n:
204      (a, r, s)
205    case 1n+j:
206      match a:
207        case BZ{}:
208          shr(j, BZ{}, False{}, Bool.or(r, s))
209        case B0{x}:
210          shr(j, x, False{}, Bool.or(r, s))
211        case B1{x}:
212          shr(j, x, True{}, Bool.or(r, s))
213
214# the n low bits of a word, and back
215def of_word(n: Nat, w: Word(n)) -> Bin:
216  match n:
217    case 0n:
218      BZ{}
219    case 1n+p:
220      match w:
221        case WCon{b, t}:
222          cons(b, of_word(p, t))
223
224def to_word(n: Nat, a: Bin) -> Word(n):
225  match n:
226    case 0n:
227      WNil{}
228    case 1n+p:
229      match a:
230        case BZ{}:
231          WCon{False{}, to_word(p, BZ{})}
232        case B0{r}:
233          WCon{False{}, to_word(p, r)}
234        case B1{r}:
235          WCon{True{}, to_word(p, r)}
236
237def to_nat(a: Bin) -> Nat:
238  match a:
239    case BZ{}:
240      0n
241    case B0{r}:
242      Nat.double(to_nat(r))
243    case B1{r}:
244      1n+Nat.double(to_nat(r))
245
246def of_nat(n: Nat) -> Bin:
247  match n:
248    case 0n:
249      BZ{}
250    case 1n+k:
251      inc(of_nat(k))
252
253# the low k bits of a
254def low(k: Nat, a: Bin) -> Bin:
255  match k:
256    case 0n:
257      BZ{}
258    case 1n+j:
259      match a:
260        case BZ{}:
261          BZ{}
262        case B0{r}:
263          B0{low(j, r)}
264        case B1{r}:
265          B1{low(j, r)}
266
267def take.cons(-r: Nat, b: Bool, p: Bin & Word(r)) -> Bin & Word(r):
268  (x, w) = p
269  (cons(b, x), w)
270
271# the low k bits of a word as a Bin, and the word that remains
272def take(k: Nat, -r: Nat, w: Word(Nat.add(k, r))) -> Bin & Word(r):
273  match k:
274    case 0n:
275      (BZ{}, w)
276    case 1n+j:
277      match w:
278        case WCon{b, t}:
279          take.cons(r, b, take(j, r, t))