1module Compiler.NaturalMagnitude
2
3import Compiler.NaturalMagnitudeArithmetic
4import Compiler.IntegerLiteral
5import Std.Natural
6
7-- Checked admission for compile-time arbitrary natural magnitudes.
8-- Canonical payload: decimal digit values 0..9, least significant first;
9-- empty zero, no most-significant zero, at most 4096 significant digits.
10family NaturalMagnitudeFailure : Type 0
11constructor NaturalMagnitudeLiteralMalformed
12field unrestricted naturalMagnitudeLiteralFailure : (family IntegerLiteralFailure)
13constructor NaturalMagnitudeTooLarge
14constructor NaturalMagnitudeNonCanonical
15constructor NaturalMagnitudeNeedsType
16
17end-family
18
19family NaturalMagnitudeResult : Type 0
20constructor NaturalMagnitudeAccepted
21field unrestricted naturalMagnitudeDigitsLE : Bytes
22constructor NaturalMagnitudeRejected
23field unrestricted naturalMagnitudeFailure : (family NaturalMagnitudeFailure)
24
25end-family
26
27def magnitudeDigitLimit =
28 (Std.Natural/naturalMultiply (byte-to-nat (byte 64)) (byte-to-nat (byte 64)))
29
30def magnitudeDigitsValid =
31 (lambda unrestricted digits : Bytes .
32 (bytes-eliminate
33 (lambda unrestricted rest : Bytes . Nat)
34 (succ zero)
35 (lambda unrestricted head : Byte .
36 (lambda unrestricted tail : Bytes .
37 (lambda unrestricted continue : Nat .
38 (Std.Natural/naturalAnd
39 (nat-less-than (byte-to-nat head) (byte-to-nat (byte 10)))
40 continue))))
41 digits))
42
43def magnitudeBudgetAccept =
44 (lambda unrestricted digits : Bytes .
45 (app
46 (nat-eliminate
47 (lambda unrestricted flag : Nat .
48 (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
49 (lambda unrestricted force : Nat .
50 (constructor NaturalMagnitudeResult NaturalMagnitudeAccepted digits))
51 (lambda unrestricted predecessor : Nat .
52 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
53 (lambda unrestricted force : Nat .
54 (constructor
55 NaturalMagnitudeResult
56 NaturalMagnitudeRejected
57 (constructor NaturalMagnitudeFailure NaturalMagnitudeTooLarge)))))
58 (nat-less-than magnitudeDigitLimit (bytes-length digits)))
59 zero))
60
61def magnitudeDecodeCanonical =
62 (lambda unrestricted digits : Bytes .
63 (app
64 (nat-eliminate
65 (lambda unrestricted flag : Nat .
66 (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
67 (lambda unrestricted force : Nat .
68 (constructor
69 NaturalMagnitudeResult
70 NaturalMagnitudeRejected
71 (constructor NaturalMagnitudeFailure NaturalMagnitudeNonCanonical)))
72 (lambda unrestricted predecessor : Nat .
73 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
74 (lambda unrestricted force : Nat . (magnitudeBudgetAccept digits))))
75 (Std.Natural/naturalAnd
76 (magnitudeDigitsValid digits)
77 (bytes-equal digits (magnitudeNormalize digits))))
78 zero))
79
80def magnitudeAdmitNormalized =
81 (lambda unrestricted digits : Bytes . (magnitudeDecodeCanonical (magnitudeNormalize digits)))
82
83def magnitudeDecimalDigits =
84 (lambda unrestricted digits : Bytes .
85 (magnitudeAdmitNormalized
86 (app
87 (bytes-eliminate
88 (lambda unrestricted rest : Bytes . (pi unrestricted accumulator : Bytes . Bytes))
89 (lambda unrestricted accumulator : Bytes . accumulator)
90 (lambda unrestricted head : Byte .
91 (lambda unrestricted tail : Bytes .
92 (lambda unrestricted continue : (pi unrestricted accumulator : Bytes . Bytes) .
93 (lambda unrestricted accumulator : Bytes .
94 (continue
95 (bytes-cons
96 (nat-to-byte
97 (Std.Natural/naturalSaturatingSubtract
98 (byte-to-nat head)
99 (byte-to-nat (byte 48))))
100 accumulator))))))
101 digits)
102 b"")))
103
104def magnitudeRadixScale =
105 (lambda unrestricted radix : (family IntegerLiteralRadix) .
106 (lambda unrestricted digits : Bytes .
107 (eliminate
108 IntegerLiteralRadix
109 (lambda unrestricted current : (family IntegerLiteralRadix) . Bytes)
110 radix
111 (branch IntegerLiteralDecimal . (magnitudeMultiplyDigit digits (byte 10)))
112 (branch IntegerLiteralBinary . (magnitudeDouble digits))
113 (branch
114 IntegerLiteralHexadecimal
115 .
116 (magnitudeRepeatSmall
117 Bytes
118 (byte-to-nat (byte 4))
119 (lambda unrestricted value : Bytes . (magnitudeDouble value))
120 digits)))))
121
122def magnitudeRadixDigits =
123 (lambda unrestricted radix : (family IntegerLiteralRadix) .
124 (lambda unrestricted digits : Bytes .
125 (app
126 (bytes-eliminate
127 (lambda unrestricted rest : Bytes .
128 (pi unrestricted accumulator : Bytes . (family NaturalMagnitudeResult)))
129 (lambda unrestricted accumulator : Bytes .
130 (constructor NaturalMagnitudeResult NaturalMagnitudeAccepted accumulator))
131 (lambda unrestricted head : Byte .
132 (lambda unrestricted tail : Bytes .
133 (lambda unrestricted continue : (pi unrestricted accumulator : Bytes . (family NaturalMagnitudeResult)) .
134 (lambda unrestricted accumulator : Bytes .
135 (eliminate
136 IntegerLiteralDigitResult
137 (lambda unrestricted current : (family IntegerLiteralDigitResult) .
138 (family NaturalMagnitudeResult))
139 (Compiler.IntegerLiteral/integerLiteralDecodeDigit radix head)
140 (branch
141 IntegerLiteralDigitValue
142 digit
143 .
144 (eliminate
145 NaturalMagnitudeResult
146 (lambda unrestricted current : (family NaturalMagnitudeResult) .
147 (family NaturalMagnitudeResult))
148 (magnitudeBudgetAccept
149 (magnitudeAdd
150 (magnitudeFromNatural digit)
151 (magnitudeRadixScale radix accumulator)))
152 (branch NaturalMagnitudeAccepted next . (continue next))
153 (branch
154 NaturalMagnitudeRejected
155 failure
156 .
157 (constructor NaturalMagnitudeResult NaturalMagnitudeRejected failure))))
158 (branch
159 IntegerLiteralDigitFailed
160 failure
161 .
162 (constructor
163 NaturalMagnitudeResult
164 NaturalMagnitudeRejected
165 (constructor
166 NaturalMagnitudeFailure
167 NaturalMagnitudeLiteralMalformed
168 failure))))))))
169 digits)
170 b"")))
171
172def magnitudeConvertValidatedDigits =
173 (lambda unrestricted radix : (family IntegerLiteralRadix) .
174 (lambda unrestricted digits : Bytes .
175 (eliminate
176 IntegerLiteralRadix
177 (lambda unrestricted current : (family IntegerLiteralRadix) .
178 (family NaturalMagnitudeResult))
179 radix
180 (branch IntegerLiteralDecimal . (magnitudeDecimalDigits digits))
181 (branch IntegerLiteralBinary . (magnitudeRadixDigits radix digits))
182 (branch IntegerLiteralHexadecimal . (magnitudeRadixDigits radix digits)))))
183
184def magnitudeParseDigits =
185 (lambda unrestricted radix : (family IntegerLiteralRadix) .
186 (lambda unrestricted digits : Bytes .
187 (app
188 (nat-eliminate
189 (lambda unrestricted flag : Nat .
190 (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
191 (lambda unrestricted force : Nat .
192 (eliminate
193 IntegerLiteralSyntaxResult
194 (lambda unrestricted current : (family IntegerLiteralSyntaxResult) .
195 (family NaturalMagnitudeResult))
196 (Compiler.IntegerLiteral/integerLiteralValidateSeparators radix digits)
197 (branch
198 IntegerLiteralSyntaxAccepted
199 .
200 (magnitudeConvertValidatedDigits
201 radix
202 (Compiler.IntegerLiteral/integerLiteralStripSeparators digits)))
203 (branch
204 IntegerLiteralSyntaxFailed
205 failure
206 .
207 (constructor
208 NaturalMagnitudeResult
209 NaturalMagnitudeRejected
210 (constructor NaturalMagnitudeFailure NaturalMagnitudeLiteralMalformed failure)))))
211 (lambda unrestricted predecessor : Nat .
212 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
213 (lambda unrestricted force : Nat .
214 (constructor
215 NaturalMagnitudeResult
216 NaturalMagnitudeRejected
217 (constructor
218 NaturalMagnitudeFailure
219 NaturalMagnitudeLiteralMalformed
220 (constructor IntegerLiteralFailure IntegerLiteralMissingDigits))))))
221 (bytes-equal digits b""))
222 zero)))
223
224def magnitudeParseUnsigned =
225 (lambda unrestricted spelling : Bytes .
226 (app
227 (nat-eliminate
228 (lambda unrestricted flag : Nat .
229 (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
230 (lambda unrestricted force : Nat .
231 (app
232 (nat-eliminate
233 (lambda unrestricted flag : Nat .
234 (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
235 (lambda unrestricted force : Nat .
236 (magnitudeParseDigits
237 (constructor IntegerLiteralRadix IntegerLiteralDecimal)
238 spelling))
239 (lambda unrestricted predecessor : Nat .
240 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
241 (lambda unrestricted force : Nat .
242 (app
243 (nat-eliminate
244 (lambda unrestricted flag : Nat .
245 (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
246 (lambda unrestricted force : Nat .
247 (app
248 (nat-eliminate
249 (lambda unrestricted flag : Nat .
250 (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
251 (lambda unrestricted force : Nat .
252 (magnitudeParseDigits
253 (constructor IntegerLiteralRadix IntegerLiteralDecimal)
254 spelling))
255 (lambda unrestricted predecessor : Nat .
256 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
257 (lambda unrestricted force : Nat .
258 (magnitudeParseDigits
259 (constructor IntegerLiteralRadix IntegerLiteralBinary)
260 (bytes-tail (bytes-tail spelling))))))
261 (Std.Natural/naturalOr
262 (byte-equal (bytes-head (bytes-tail spelling)) (byte 98))
263 (byte-equal (bytes-head (bytes-tail spelling)) (byte 66))))
264 zero))
265 (lambda unrestricted predecessor : Nat .
266 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
267 (lambda unrestricted force : Nat .
268 (magnitudeParseDigits
269 (constructor IntegerLiteralRadix IntegerLiteralHexadecimal)
270 (bytes-tail (bytes-tail spelling))))))
271 (Std.Natural/naturalOr
272 (byte-equal (bytes-head (bytes-tail spelling)) (byte 120))
273 (byte-equal (bytes-head (bytes-tail spelling)) (byte 88))))
274 zero))))
275 (byte-equal (bytes-head spelling) (byte 48)))
276 zero))
277 (lambda unrestricted predecessor : Nat .
278 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
279 (lambda unrestricted force : Nat .
280 (constructor
281 NaturalMagnitudeResult
282 NaturalMagnitudeRejected
283 (constructor NaturalMagnitudeFailure NaturalMagnitudeNeedsType)))))
284 (byte-equal (bytes-head spelling) (byte 45)))
285 zero))
286
287def magnitudeCanonicalValid =
288 (lambda unrestricted digits : Bytes .
289 (eliminate
290 NaturalMagnitudeResult
291 (lambda unrestricted result : (family NaturalMagnitudeResult) . Nat)
292 (magnitudeDecodeCanonical digits)
293 (branch NaturalMagnitudeAccepted valid . (succ zero))
294 (branch NaturalMagnitudeRejected failure . zero)))
295
296def magnitudeFailureCode =
297 (lambda unrestricted error : (family NaturalMagnitudeFailure) .
298 (eliminate
299 NaturalMagnitudeFailure
300 (lambda unrestricted current : (family NaturalMagnitudeFailure) . Bytes)
301 error
302 (branch
303 NaturalMagnitudeLiteralMalformed
304 failure
305 .
306 (eliminate
307 IntegerLiteralFailure
308 (lambda unrestricted current : (family IntegerLiteralFailure) . Bytes)
309 failure
310 (branch
311 IntegerLiteralMissingDigits
312 .
313 b"ALPHA-LITERAL-MISSING-DIGITS")
314 (branch
315 IntegerLiteralBadDigit
316 .
317 b"ALPHA-LITERAL-BAD-DIGIT")
318 (branch
319 IntegerLiteralBadSeparator
320 .
321 b"ALPHA-LITERAL-BAD-SEPARATOR")
322 (branch
323 IntegerLiteralOutOfRange
324 .
325 b"ALPHA-LITERAL-OUT-OF-RANGE")))
326 (branch
327 NaturalMagnitudeTooLarge
328 .
329 b"ALPHA-PARSE-NAT-LITERAL-TOO-LARGE")
330 (branch
331 NaturalMagnitudeNonCanonical
332 .
333 b"ALPHA-NAT-MAGNITUDE-NONCANONICAL")
334 (branch
335 NaturalMagnitudeNeedsType
336 .
337 b"ALPHA-LITERAL-NEEDS-TYPE")))
338
339-- Validate both operands before invoking a checked binary operation.
340def magnitudeBinaryChecked =
341 (lambda unrestricted operation : (pi unrestricted left : Bytes . (pi unrestricted right : Bytes . (family NaturalMagnitudeResult))) .
342 (lambda unrestricted left : Bytes .
343 (lambda unrestricted right : Bytes .
344 (eliminate
345 NaturalMagnitudeResult
346 (lambda unrestricted current : (family NaturalMagnitudeResult) .
347 (family NaturalMagnitudeResult))
348 (magnitudeDecodeCanonical left)
349 (branch
350 NaturalMagnitudeAccepted
351 a
352 .
353 (eliminate
354 NaturalMagnitudeResult
355 (lambda unrestricted current : (family NaturalMagnitudeResult) .
356 (family NaturalMagnitudeResult))
357 (magnitudeDecodeCanonical right)
358 (branch NaturalMagnitudeAccepted b . (operation a b))
359 (branch
360 NaturalMagnitudeRejected
361 error
362 .
363 (constructor NaturalMagnitudeResult NaturalMagnitudeRejected error))))
364 (branch
365 NaturalMagnitudeRejected
366 error
367 .
368 (constructor NaturalMagnitudeResult NaturalMagnitudeRejected error))))))
369
370-- Nonzero n- and m-digit products have at least n+m-1 digits. Refuse
371-- guaranteed overflow before multiplication; the boundary still needs exact admission.
372def magnitudeMultiplyAdmitted =
373 (lambda unrestricted left : Bytes .
374 (lambda unrestricted right : Bytes .
375 (app
376 (nat-eliminate
377 (lambda unrestricted flag : Nat .
378 (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
379 (lambda unrestricted force : Nat .
380 (magnitudeAdmitNormalized (magnitudeMultiply left right)))
381 (lambda unrestricted predecessor : Nat .
382 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
383 (lambda unrestricted force : Nat .
384 (constructor
385 NaturalMagnitudeResult
386 NaturalMagnitudeRejected
387 (constructor NaturalMagnitudeFailure NaturalMagnitudeTooLarge)))))
388 (nat-less-than
389 (succ magnitudeDigitLimit)
390 (Std.Natural/naturalAdd (bytes-length left) (bytes-length right))))
391 zero)))
392
393def magnitudeAddChecked =
394 (magnitudeBinaryChecked
395 (lambda unrestricted left : Bytes .
396 (lambda unrestricted right : Bytes . (magnitudeAdmitNormalized (magnitudeAdd left right)))))
397
398def magnitudeSubtractChecked =
399 (magnitudeBinaryChecked
400 (lambda unrestricted left : Bytes .
401 (lambda unrestricted right : Bytes .
402 (magnitudeAdmitNormalized (magnitudeSubtract left right)))))
403
404def magnitudeDivideChecked =
405 (magnitudeBinaryChecked
406 (lambda unrestricted left : Bytes .
407 (lambda unrestricted right : Bytes . (magnitudeAdmitNormalized (magnitudeDivide left right)))))
408
409def magnitudeModuloChecked =
410 (magnitudeBinaryChecked
411 (lambda unrestricted left : Bytes .
412 (lambda unrestricted right : Bytes . (magnitudeAdmitNormalized (magnitudeModulo left right)))))
413
414def magnitudeMultiplyChecked =
415 (magnitudeBinaryChecked
416 (lambda unrestricted left : Bytes .
417 (lambda unrestricted right : Bytes . (magnitudeMultiplyAdmitted left right))))
418
419def magnitudeSuccessorChecked =
420 (lambda unrestricted digits : Bytes .
421 (eliminate
422 NaturalMagnitudeResult
423 (lambda unrestricted current : (family NaturalMagnitudeResult) .
424 (family NaturalMagnitudeResult))
425 (magnitudeDecodeCanonical digits)
426 (branch
427 NaturalMagnitudeAccepted
428 value
429 .
430 (magnitudeAdmitNormalized (magnitudeSuccessor value)))
431 (branch
432 NaturalMagnitudeRejected
433 error
434 .
435 (constructor NaturalMagnitudeResult NaturalMagnitudeRejected error))))
436
437def magnitudePredecessorChecked =
438 (lambda unrestricted digits : Bytes .
439 (eliminate
440 NaturalMagnitudeResult
441 (lambda unrestricted current : (family NaturalMagnitudeResult) .
442 (family NaturalMagnitudeResult))
443 (magnitudeDecodeCanonical digits)
444 (branch
445 NaturalMagnitudeAccepted
446 value
447 .
448 (magnitudeAdmitNormalized (magnitudePredecessor value)))
449 (branch
450 NaturalMagnitudeRejected
451 error
452 .
453 (constructor NaturalMagnitudeResult NaturalMagnitudeRejected error))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.