1	import 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	
13	type Bin is Data:
14	  BZ{}
15	  B0{r: Bin}
16	  B1{r: Bin}
17	
18	def one() -> Bin:
19	  B1{BZ{}}
20	
21	def 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	
30	def 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
38	def 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	
47	def odd(a: Bin) -> Bool:
48	  match a:
49	    case B1{r}:
50	      True{}
51	    case _:
52	      False{}
53	
54	def 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	
63	def cons(s: Bool, r: Bin) -> Bin:
64	  match s:
65	    case False{}:
66	      B0{r}
67	    case True{}:
68	      B1{r}
69	
70	def 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
79	def 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	
94	def add(a: Bin, b: Bin) -> Bin:
95	  adc(a, b, False{})
96	
97	def 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	
106	def 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)
114	def 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	
129	def sub(a: Bin, b: Bin) -> Bin:
130	  sbb(a, b, False{})
131	
132	def 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	
141	def 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	
150	def 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
172	def shl(a: Bin, n: Nat) -> Bin:
173	  match n:
174	    case 0n:
175	      a
176	    case 1n+k:
177	      B0{shl(a, k)}
178	
179	def pow2(n: Nat) -> Bin:
180	  shl(one(), n)
181	
182	def 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
190	def 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
201	def 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
215	def 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	
224	def 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	
237	def 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	
246	def 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
254	def 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	
267	def 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
272	def 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))