rework the verifier to prepare for loop cutting
[ajla.git] / newlib / private / fixed_point.ajla
blobbbf60384c7f0592f1f173e8d98a9ebe71cb7131d
1 {*
2  * Copyright (C) 2024 Mikulas Patocka
3  *
4  * This file is part of Ajla.
5  *
6  * Ajla is free software: you can redistribute it and/or modify it under the
7  * terms of the GNU General Public License as published by the Free Software
8  * Foundation, either version 3 of the License, or (at your option) any later
9  * version.
10  *
11  * Ajla is distributed in the hope that it will be useful, but WITHOUT ANY
12  * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR
13  * A PARTICULAR PURPOSE. See the GNU General Public License for more details.
14  *
15  * You should have received a copy of the GNU General Public License along with
16  * Ajla. If not, see <https://www.gnu.org/licenses/>.
17  *}
19 private unit private.fixed_point;
21 type fp_type := int128;
23 fn fixed_point_zero~inline(base digits : int) : fp_type;
24 fn fixed_point_one~inline(base digits : int) : fp_type;
25 fn fixed_point_neg~inline(base digits : int, i1 : fp_type) : fp_type;
26 fn fixed_point_recip~inline(base digits : int, i1 : fp_type) : fp_type;
27 fn fixed_point_add~inline(base digits : int, i1 i2 : fp_type) : fp_type;
28 fn fixed_point_subtract~inline(base digits : int, i1 i2 : fp_type) : fp_type;
29 fn fixed_point_multiply~inline(base digits : int, i1 i2 : fp_type) : fp_type;
30 fn fixed_point_divide~inline(base digits : int, i1 i2 : fp_type) : fp_type;
31 fn fixed_point_modulo~inline(const base digits : int, i1 i2 : fixed_point(base, digits)) : fixed_point(base, digits);
32 fn fixed_point_power~inline(const base digits : int, i1 i2 : fixed_point(base, digits)) : fixed_point(base, digits);
33 fn fixed_point_ldexp~inline(const base digits : int, i1 i2 : fixed_point(base, digits)) : fixed_point(base, digits);
34 fn fixed_point_atan2~inline(const base digits : int, i1 i2 : fixed_point(base, digits)) : fixed_point(base, digits);
35 fn fixed_point_pi~inline(const base digits : int) : fixed_point(base, digits);
36 fn fixed_point_sqrt~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
37 fn fixed_point_cbrt~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
38 fn fixed_point_sin~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
39 fn fixed_point_cos~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
40 fn fixed_point_tan~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
41 fn fixed_point_asin~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
42 fn fixed_point_acos~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
43 fn fixed_point_atan~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
44 fn fixed_point_sinh~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
45 fn fixed_point_cosh~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
46 fn fixed_point_tanh~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
47 fn fixed_point_asinh~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
48 fn fixed_point_acosh~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
49 fn fixed_point_atanh~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
50 fn fixed_point_exp2~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
51 fn fixed_point_exp~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
52 fn fixed_point_exp10~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
53 fn fixed_point_log2~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
54 fn fixed_point_log~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
55 fn fixed_point_log10~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
56 fn fixed_point_round~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
57 fn fixed_point_ceil~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
58 fn fixed_point_floor~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
59 fn fixed_point_trunc~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
60 fn fixed_point_fract~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
61 fn fixed_point_mantissa~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
62 fn fixed_point_exponent~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
63 fn fixed_point_next_number~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
64 fn fixed_point_prev_number~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits);
65 fn fixed_point_is_negative~inline(base digits : int, i1 : fp_type) : bool;
66 fn fixed_point_is_infinity~inline(base digits : int, i1 : fp_type) : bool;
67 fn fixed_point_equal~inline(base digits : int, i1 i2 : fp_type) : bool;
68 fn fixed_point_not_equal~inline(base digits : int, i1 i2 : fp_type) : bool;
69 fn fixed_point_less~inline(base digits : int, i1 i2 : fp_type) : bool;
70 fn fixed_point_less_equal~inline(base digits : int, i1 i2 : fp_type) : bool;
71 fn fixed_point_to_int~inline(base digits : int, i1 : fp_type) : int;
72 fn fixed_point_from_int~inline(base digits : int, i1 : int) : fp_type;
73 fn fixed_point_to_rational~inline(base digits : int, i1 : fp_type) : rational;
74 fn fixed_point_from_rational~inline(base digits : int, i1 : rational) : fp_type;
75 fn fixed_point_to_bytes(const base digits : int, i1 : fixed_point(base, digits)) : bytes;
76 fn fixed_point_to_bytes_base_precision(const base digits : int, i1 : fixed_point(base, digits), b : int, d : int) : bytes;
77 fn fixed_point_from_bytes(const base digits : int, a1 : bytes) : fixed_point(base, digits);
78 fn fixed_point_from_bytes_base(const base digits : int, a1 : bytes, b : int) : fixed_point(base, digits);
80 implementation
82 uses exception;
83 uses private.show;
84 uses private.math;
86 fn fixed_point_validate(base digits : int) : unit_type
88         if base < 2 or digits < 0 then
89                 abort exception_make(unit_type, ec_sync, error_invalid_operation, 0, true);
90         return unit_value;
93 fn fixed_point_zero~inline(base digits : int) : fp_type
95         xeval fixed_point_validate(base, digits);
96         return 0;
99 fn fixed_point_one~inline(base digits : int) : fp_type
101         xeval fixed_point_validate(base, digits);
102         return ipower(base, digits);
105 fn fixed_point_neg~inline(base digits : int, i1 : fp_type) : fp_type
107         return -i1;
110 fn fixed_point_add~inline(base digits : int, i1 i2 : fp_type) : fp_type
112         return i1 + i2;
115 fn fixed_point_subtract~inline(base digits : int, i1 i2 : fp_type) : fp_type
117         return i1 - i2;
120 fn fixed_point_multiply~inline(base digits : int, i1 i2 : fp_type) : fp_type
122         return i1 * i2 div ipower(base, digits);
125 fn fixed_point_recip~inline(base digits : int, i1 : fp_type) : fp_type
127         if i1 = 0 then
128                 return exception_make(fp_type, ec_sync, error_infinity, 0, true);
129         return ipower(base, digits * 2) div i1;
132 fn fixed_point_divide~inline(base digits : int, i1 i2 : fp_type) : fp_type
134         if i2 = 0 then [
135                 if i1 = 0 then
136                         return exception_make(fp_type, ec_sync, error_nan, 0, true);
137                 else
138                         return exception_make(fp_type, ec_sync, error_infinity, 0, true);
139         ]
140         return i1 * ipower(base, digits) div i2;
143 fn fixed_point_modulo~inline(const base digits : int, i1 i2 : fixed_point(base, digits)) : fixed_point(base, digits)
145         if i2 = 0 then
146                 return exception_make(fp_type, ec_sync, error_nan, 0, true);
147         return math_modulo(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1, i2);
150 fn fixed_point_power~inline(const base digits : int, i1 i2 : fixed_point(base, digits)) : fixed_point(base, digits)
152         return math_power(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1, i2);
155 fn fixed_point_ldexp~inline(const base digits : int, i1 i2 : fixed_point(base, digits)) : fixed_point(base, digits)
157         return math_ldexp(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1, i2);
160 fn fixed_point_atan2~inline(const base digits : int, i1 i2 : fixed_point(base, digits)) : fixed_point(base, digits)
162         return math_atan2(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1, i2);
165 fn fixed_point_pi~inline(const base digits : int) : fixed_point(base, digits)
167         xeval fixed_point_validate(base, digits);
168         return math_pi(fixed_point(base, digits), instance_real_number_fixed_point(base, digits));
171 fn fixed_point_sqrt~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
173         return math_sqrt(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
176 fn fixed_point_cbrt~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
178         return math_cbrt(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
181 fn fixed_point_sin~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
183         return math_sin(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
186 fn fixed_point_cos~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
188         return math_cos(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
191 fn fixed_point_tan~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
193         return math_tan(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
196 fn fixed_point_asin~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
198         return math_asin(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
201 fn fixed_point_acos~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
203         return math_acos(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
206 fn fixed_point_atan~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
208         return math_atan(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
211 fn fixed_point_sinh~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
213         return math_sinh(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
216 fn fixed_point_cosh~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
218         return math_cosh(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
221 fn fixed_point_tanh~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
223         return math_tanh(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
226 fn fixed_point_asinh~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
228         return math_asinh(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
231 fn fixed_point_acosh~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
233         return math_acosh(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
236 fn fixed_point_atanh~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
238         return math_atanh(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
241 fn fixed_point_exp2~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
243         return math_exp2(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
246 fn fixed_point_exp~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
248         return math_exp(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
251 fn fixed_point_exp10~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
253         return math_exp10(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
256 fn fixed_point_log2~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
258         return math_log2(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
261 fn fixed_point_log~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
263         return math_log(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
266 fn fixed_point_log10~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
268         return math_log10(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
271 fn fixed_point_round~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
273         return math_round(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
276 fn fixed_point_ceil~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
278         return math_ceil(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
281 fn fixed_point_floor~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
283         return math_floor(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
286 fn fixed_point_trunc~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
288         return math_trunc(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
291 fn fixed_point_fract~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
293         return math_fract(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
296 fn fixed_point_mantissa~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
298         return math_mantissa(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
301 fn fixed_point_exponent~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
303         return math_exponent(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1);
306 fn fixed_point_next_number~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
308         return i1 + 1;
311 fn fixed_point_prev_number~inline(const base digits : int, i1 : fixed_point(base, digits)) : fixed_point(base, digits)
313         return i1 - 1;
316 fn fixed_point_is_negative~inline(base digits : int, i1 : fp_type) : bool
318         return i1 < 0;
321 fn fixed_point_is_infinity~inline(base digits : int, i1 : fp_type) : bool
323         return false;
326 fn fixed_point_equal~inline(base digits : int, i1 i2 : fp_type) : bool
328         return i1 = i2;
331 fn fixed_point_not_equal~inline(base digits : int, i1 i2 : fp_type) : bool
333         return i1 <> i2;
336 fn fixed_point_less~inline(base digits : int, i1 i2 : fp_type) : bool
338         return i1 < i2;
341 fn fixed_point_less_equal~inline(base digits : int, i1 i2 : fp_type) : bool
343         return i1 <= i2;
346 fn fixed_point_to_int~inline(base digits : int, i1 : fp_type) : int
348         return i1 div ipower(base, digits);
351 fn fixed_point_from_int~inline(base digits : int, i1 : int) : fp_type
353         xeval fixed_point_validate(base, digits);
354         return i1 * ipower(base, digits);
357 fn fixed_point_to_rational~inline(base digits : int, i1 : fp_type) : rational
359         var r1 : rational := i1;
360         var r2 : rational := ipower(base, digits);
361         return r1 / r2;
364 fn fixed_point_from_rational~inline(base digits : int, i1 : rational) : fp_type
366         xeval fixed_point_validate(base, digits);
367         var r2 : rational := ipower(base, digits);
368         var r := i1 * r2;
369         if r.den = 0 then [
370                 if r.num = 0 then
371                         return exception_make(fp_type, ec_sync, error_nan, 0, true);
372                 else
373                         return exception_make(fp_type, ec_sync, error_infinity, 0, true);
374         ]
375         if r.num >= 0 then
376                 return (r.num + r.den div 2) div r.den;
377         else
378                 return (r.num - r.den div 2) div r.den;
381 fn fixed_point_to_bytes(const base digits : int, i1 : fixed_point(base, digits)) : bytes
383         return real_to_bytes_base_precision(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1, base, digits);
386 fn fixed_point_to_bytes_base_precision(const base digits : int, i1 : fixed_point(base, digits), b : int, d : int) : bytes
388         return real_to_bytes_base_precision(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), i1, b, d);
391 fn fixed_point_from_bytes(const base digits : int, a1 : bytes) : fixed_point(base, digits)
393         xeval fixed_point_validate(base, digits);
394         return bytes_to_real_base(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), a1, base);
397 fn fixed_point_from_bytes_base(const base digits : int, a1 : bytes, b : int) : fixed_point(base, digits)
399         xeval fixed_point_validate(base, digits);
400         return bytes_to_real_base(fixed_point(base, digits), instance_real_number_fixed_point(base, digits), a1, b);