1 % (c) 2020-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(external_functions_reals,['STRING_TO_REAL'/3,
6 'RADD'/4,'RSUB'/4,'RMUL'/4,'RDIV'/5, 'RINV'/4,
7 'RPI'/1, 'RZERO'/1, 'RONE'/1, 'REULER'/1,
8 'REPSILON'/1, 'RMAXFLOAT'/1,
9 'RSIN'/3, 'RCOS'/3, 'RTAN'/3, 'RCOT'/3,
10 'RSINH'/3, 'RCOSH'/3, 'RTANH'/3, 'RCOTH'/3,
11 'RASIN'/3, 'RACOS'/3, 'RATAN'/3, 'RACOT'/3,
12 'RASINH'/3, 'RACOSH'/3, 'RATANH'/3, 'RACOTH'/3,
13 'RATAN2'/5, 'RHYPOT'/5,
14 'RADIANS'/4, 'DEGREE'/4,
15 'RUMINUS'/3,
16 'REXP'/3, 'RLOGe'/4, 'RSQRT'/4,
17 'RABS'/3, 'ROUND'/3, 'RSIGN'/3,
18 'RINTEGER'/3, 'RFRACTION'/3,
19 'RMAX'/5, 'RMIN'/5,
20 'RPOW'/5, 'RLOG'/5,
21 'RDECIMAL'/5, % scientific notation using integers
22 'RLT'/4, 'REQ'/4, 'RNEQ'/4, 'RLEQ'/4, 'RGT'/4, 'RGEQ'/4,
23 'RMAXIMUM'/4, 'RMINIMUM'/4,
24
25 'RNEXT'/2, 'RPREV'/2,
26
27 'SFADD16'/3,
28 'SFSUB16'/3,
29 'SFMUL16'/3,
30 'SFDIV16'/3,
31 'SFSQRT16'/2,
32 'SFMULADD16'/4,
33
34 'SFADD32'/3,
35 'SFSUB32'/3,
36 'SFMUL32'/3,
37 'SFDIV32'/3,
38 'SFSQRT32'/2,
39 'SFMULADD32'/4,
40
41 'SFADD64'/3,
42 'SFSUB64'/3,
43 'SFMUL64'/3,
44 'SFDIV64'/3,
45 'SFSQRT64'/2,
46 'SFMULADD64'/4,
47
48 'SFADD80'/3,
49 'SFSUB80'/3,
50 'SFMUL80'/3,
51 'SFDIV80'/3,
52 'SFSQRT80'/2,
53
54 'SFADD128'/3,
55 'SFSUB128'/3,
56 'SFMUL128'/3,
57 'SFDIV128'/3,
58 'SFSQRT128'/2,
59 'SFMULADD128'/4
60 ]).
61
62
63 % -------------------------------
64 :- use_module(probsrc(kernel_reals),[construct_real/2,
65 is_largest_positive_float/1, is_smallest_positive_float/1,
66 is_next_larger_float/2, is_next_smaller_float/2]).
67
68 %external_fun_type('STRING_TO_REAL',[],[string,real]).
69 % allows to call construct_real/2; also works for numbers without decimal point
70
71 :- block 'STRING_TO_REAL'(-,?,?).
72 'STRING_TO_REAL'(string(A),Result,_) :-
73 block_construct_real(A,Result).
74
75 :- block 'block_construct_real'(-,?).
76 block_construct_real(A,Result) :-
77 construct_real(A,Result).
78
79 % -------------------------------
80
81 :- use_module(probsrc(kernel_reals),[real_addition_wf/4, real_subtraction_wf/4,
82 real_multiplication_wf/4, real_division_wf/5, real_power_of_wf/5,
83 real_unary_minus_wf/3, real_absolute_value_wf/3, real_square_root_wf/4,
84 convert_int_to_real/2,
85 real_round_wf/3,
86 real_unop_wf/4, real_unop_wf/5, real_binop_wf/6,
87 real_comp_wf/5,
88 real_maximum_of_set/4, real_minimum_of_set/4]).
89
90 'RADD'(RX,RY,RR,WF) :-
91 real_addition_wf(RX,RY,RR,WF).
92
93 'RSUB'(RX,RY,RR,WF) :-
94 real_subtraction_wf(RX,RY,RR,WF).
95
96 'RMUL'(RX,RY,RR,WF) :-
97 real_multiplication_wf(RX,RY,RR,WF).
98
99 'RDIV'(RX,RY,RR,Span,WF) :-
100 real_division_wf(RX,RY,RR,Span,WF).
101
102 'RINV'(RY,RR,Span,WF) :-
103 'RONE'(RX),
104 real_division_wf(RX,RY,RR,Span,WF).
105
106 % ---- constants
107
108 'RPI'(term(floating(R))) :- R is pi.
109
110 'RZERO'(term(floating(R))) :- R = 0.0.
111
112 'RONE'(term(floating(R))) :- R = 1.0.
113
114 'REULER'(term(floating(R))) :- R is exp(1.0).
115
116 'REPSILON'(R) :- is_smallest_positive_float(R). % 5.0E-324
117
118 'RMAXFLOAT'(R) :- is_largest_positive_float(R). % 1.7976931348623157E+308
119
120 % ---- unary operators
121
122 % --- Trigonometric
123
124 :- block 'RSIN'(-,?,?).
125 'RSIN'(X,R,WF) :-
126 real_unop_wf('sin',X,R,WF).
127
128 :- block 'RCOS'(-,?,?).
129 'RCOS'(X,R,WF) :-
130 real_unop_wf('cos',X,R,WF).
131
132 :- block 'RTAN'(-,?,?).
133 'RTAN'(X,R,WF) :-
134 real_unop_wf('tan',X,R,WF).
135
136 :- block 'RCOT'(-,?,?).
137 'RCOT'(X,R,WF) :-
138 real_unop_wf('cot',X,R,WF).
139
140 :- block 'RSINH'(-,?,?).
141 'RSINH'(X,R,WF) :-
142 real_unop_wf('sinh',X,R,WF).
143
144 :- block 'RCOSH'(-,?,?).
145 'RCOSH'(X,R,WF) :-
146 real_unop_wf('cosh',X,R,WF).
147
148 :- block 'RTANH'(-,?,?).
149 'RTANH'(X,R,WF) :-
150 real_unop_wf('tanh',X,R,WF).
151
152 :- block 'RCOTH'(-,?,?).
153 'RCOTH'(X,R,WF) :-
154 real_unop_wf('coth',X,R,WF).
155
156 :- block 'RASIN'(-,?,?).
157 'RASIN'(X,R,WF) :-
158 real_unop_wf('asin',X,R,WF).
159
160 :- block 'RACOS'(-,?,?).
161 'RACOS'(X,R,WF) :-
162 real_unop_wf('acos',X,R,WF).
163
164 :- block 'RATAN'(-,?,?).
165 'RATAN'(X,R,WF) :-
166 real_unop_wf('atan',X,R,WF).
167
168 :- block 'RACOT'(-,?,?).
169 'RACOT'(X,R,WF) :-
170 real_unop_wf('acot',X,R,WF).
171
172 :- block 'RASINH'(-,?,?).
173 'RASINH'(X,R,WF) :-
174 real_unop_wf('asinh',X,R,WF).
175
176 :- block 'RACOSH'(-,?,?).
177 'RACOSH'(X,R,WF) :-
178 real_unop_wf('acosh',X,R,WF).
179
180 :- block 'RATANH'(-,?,?).
181 'RATANH'(X,R,WF) :-
182 real_unop_wf('atanh',X,R,WF).
183
184 :- block 'RACOTH'(-,?,?).
185 'RACOTH'(X,R,WF) :-
186 real_unop_wf('acoth',X,R,WF).
187
188 :- block 'RATAN2'(-,?,?,?,?), 'RATAN2'(?,-,?,?,?).
189 'RATAN2'(RX,RY,RR,Span,WF) :-
190 real_binop_wf(atan2,RX,RY,RR,Span,WF).
191 % is useful for computing angle in radians from deltax, deltay, avoiding division by 0
192 % e.g. converting Cartesian coordinates x,y to Polar can be done with:
193 % angle phi = RATAN2(y,x)
194 % r = RHYPOT(x,y)
195 % Note: conversion from Polar to Cartesian is x = r*RCOS(phi) and y=r*RSIN(phi)
196
197 :- block 'RHYPOT'(-,?,?,?,?), 'RHYPOT'(?,-,?,?,?).
198 'RHYPOT'(X,Y,Res,Span,WF) :-
199 'RMUL'(X,X,X2,WF),
200 'RMUL'(Y,Y,Y2,WF),
201 'RADD'(X2,Y2,X2Y2,WF),
202 'RSQRT'(X2Y2,Res,Span,WF).
203
204 :- block 'RADIANS'(-,?,?,?).
205 'RADIANS'(Degree,Res,Span,WF) :-
206 D180 = term(floating(180.0)),
207 'RDIV'(Degree,D180,Deg2,Span,WF),
208 'RPI'(PI),
209 'RMUL'(PI,Deg2,Res,WF).
210
211 :- block 'DEGREE'(-,?,?,?).
212 'DEGREE'(Radians,Res,Span,WF) :-
213 D180 = term(floating(180.0)),
214 'RPI'(PI),
215 'RDIV'(Radians,PI,Deg2,Span,WF),
216 'RMUL'(D180,Deg2,Res,WF).
217
218
219 % -----------------------
220
221
222 'RUMINUS'(RX,RR,WF) :- % unary minus
223 real_unary_minus_wf(RX,RR,WF).
224
225 :- block 'REXP'(-,?,?).
226 'REXP'(X,R,WF) :-
227 real_unop_wf('exp',X,R,WF).
228
229 :- block 'RLOGe'(-,?,?,?).
230 'RLOGe'(X,R,Span,WF) :-
231 real_unop_wf('log',X,R,Span,WF).
232
233 'RSQRT'(X,R,Span,WF) :-
234 real_square_root_wf(X,R,Span,WF).
235
236 'RABS'(X,R,WF) :-
237 real_absolute_value_wf(X,R,WF).
238
239 :- block 'ROUND'(-,?,?).
240 'ROUND'(X,R,WF) :-
241 real_round_wf(X,R,WF).
242
243 :- block 'RSIGN'(-,?,?).
244 'RSIGN'(X,R,WF) :-
245 real_unop_wf('sign',X,R,WF).
246
247 :- block 'RINTEGER'(-,?,?).
248 'RINTEGER'(X,R,WF) :-
249 real_unop_wf('float_integer_part',X,R,WF).
250
251 :- block 'RFRACTION'(-,?,?).
252 'RFRACTION'(X,R,WF) :-
253 real_unop_wf('float_fractional_part',X,R,WF).
254
255 % ---- other binary operators
256 'RMAX'(RX,RY,RR,Span,WF) :-
257 real_binop_wf(max,RX,RY,RR,Span,WF).
258
259 'RMIN'(RX,RY,RR,Span,WF) :-
260 real_binop_wf(min,RX,RY,RR,Span,WF).
261
262 'RPOW'(RX,RY,RR,Span,WF) :-
263 real_power_of_wf(RX,RY,RR,Span,WF).
264
265 % convert integers x,y to reak x*10^y
266 'RDECIMAL'(IntX,IntY,RR,Span,WF) :-
267 convert_int_to_real(int(10),R10),
268 convert_int_to_real(IntY,RY),
269 real_power_of_wf(R10,RY,RR10,Span,WF),
270 convert_int_to_real(IntX,RX),
271 'RMUL'(RX,RR10,RR,WF).
272
273 'RLOG'(RX,RY,RR,Span,WF) :-
274 real_binop_wf(log,RX,RY,RR,Span,WF).
275
276 % ---- other binary predicates
277
278 'RLT'(RX,RY,RR,WF) :-
279 real_comp_wf('<',RX,RY,RR,WF).
280
281 'REQ'(RX,RY,RR,WF) :-
282 real_comp_wf('=:=',RX,RY,RR,WF).
283
284 'RNEQ'(RX,RY,RR,WF) :-
285 real_comp_wf('=\\=',RX,RY,RR,WF). % =\=
286
287 'RLEQ'(RX,RY,RR,WF) :-
288 real_comp_wf('=<',RX,RY,RR,WF).
289
290 'RGT'(RY,RX,RR,WF) :-'RLT'(RX,RY,RR,WF).
291
292 'RGEQ'(RY,RX,RR,WF) :-'RLEQ'(RX,RY,RR,WF).
293
294 % set operators
295
296 'RMAXIMUM'(Set,Res,Span,WF) :-
297 real_maximum_of_set(Set,Res,Span,WF).
298 'RMINIMUM'(Set,Res,Span,WF) :-
299 real_minimum_of_set(Set,Res,Span,WF).
300
301 % ---- Float operators
302
303 'RNEXT'(Nr,NextNr) :-
304 is_next_larger_float(Nr,NextNr).
305 'RPREV'(Nr,NextNr) :-
306 is_next_smaller_float(Nr,NextNr).
307
308 % softfloat functions.
309
310 :- use_module(extension('softfloat/softfloat')).
311
312 'SFADD16'(term(floating(X)),term(floating(Y)),term(floating(R))) :-
313 init_softfloat,
314 add16(X,Y,R).
315
316 'SFSUB16'(term(floating(X)),term(floating(Y)),term(floating(R))) :-
317 init_softfloat,
318 sub16(X,Y,R).
319
320 'SFMUL16'(term(floating(X)),term(floating(Y)),term(floating(R))) :-
321 init_softfloat,
322 mul16(X,Y,R).
323
324 'SFDIV16'(term(floating(X)),term(floating(Y)),term(floating(R))) :-
325 init_softfloat,
326 div16(X,Y,R).
327
328 'SFSQRT16'(term(floating(X)),term(floating(R))) :-
329 init_softfloat,
330 sqrt16(X,R).
331
332 'SFMULADD16'(term(floating(X)),term(floating(Y)),term(floating(Z)),term(floating(R))) :-
333 init_softfloat,
334 muladd16(X,Y,Z,R).
335 %32bit
336
337 'SFADD32'(term(floating(X)),term(floating(Y)),term(floating(R))) :-
338 init_softfloat,
339 add32(X,Y,R).
340
341 'SFSUB32'(term(floating(X)),term(floating(Y)),term(floating(R))) :-
342 init_softfloat,
343 sub32(X,Y,R).
344
345 'SFMUL32'(term(floating(X)),term(floating(Y)),term(floating(R))) :-
346 init_softfloat,
347 mul32(X,Y,R).
348
349 'SFDIV32'(term(floating(X)),term(floating(Y)),term(floating(R))) :-
350 init_softfloat,
351 div32(X,Y,R).
352
353 'SFSQRT32'(term(floating(X)),term(floating(R))) :-
354 init_softfloat,
355 sqrt32(X,R).
356
357 'SFMULADD32'(term(floating(X)),term(floating(Y)),term(floating(Z)),term(floating(R))) :-
358 init_softfloat,
359 muladd32(X,Y,Z,R).
360
361 %32bit
362 %64bit
363
364 'SFADD64'(term(floating(X)),term(floating(Y)),term(floating(R))) :-
365 init_softfloat,
366 add64(X,Y,R).
367
368 'SFSUB64'(term(floating(X)),term(floating(Y)),term(floating(R))) :-
369 init_softfloat,
370 sub64(X,Y,R).
371
372 'SFMUL64'(term(floating(X)),term(floating(Y)),term(floating(R))) :-
373 init_softfloat,
374 mul64(X,Y,R).
375
376 'SFDIV64'(term(floating(X)),term(floating(Y)),term(floating(R))) :-
377 init_softfloat,
378 div64(X,Y,R).
379
380 'SFSQRT64'(term(floating(X)),term(floating(R))) :-
381 init_softfloat,
382 sqrt64(X,R).
383
384 'SFMULADD64'(term(floating(X)),term(floating(Y)),term(floating(Z)),term(floating(R))) :-
385 init_softfloat,
386 muladd64(X,Y,Z,R).
387 %64bit
388 %80bit
389 'SFADD80'((int(X1),int(X2)),(int(Y1),int(Y2)),(int(R1),int(R2))) :-
390 init_softfloat,
391 add80(X1,X2,Y1,Y2,R1,R2).
392
393 'SFSUB80'((int(X1),int(X2)),(int(Y1),int(Y2)),(int(R1),int(R2))) :-
394 init_softfloat,
395 sub80(X1,X2,Y1,Y2,R1,R2).
396
397 'SFMUL80'((int(X1),int(X2)),(int(Y1),int(Y2)),(int(R1),int(R2))) :-
398 init_softfloat,
399 mul80(X1,X2,Y1,Y2,R1,R2).
400
401 'SFDIV80'((int(X1),int(X2)),(int(Y1),int(Y2)),(int(R1),int(R2))) :-
402 init_softfloat,
403 div80(X1,X2,Y1,Y2,R1,R2).
404
405 'SFSQRT80'( (int(X1),int(X2)),(int(R1),int(R2)) ) :-
406 init_softfloat,
407 sqrt80(X1,X2,R1,R2).
408 %80bit
409 %128bit
410 'SFADD128'((int(X1),int(X2)),(int(Y1),int(Y2)),(int(R1),int(R2))) :-
411 init_softfloat,
412 add128(X1,X2,Y1,Y2,R1,R2).
413
414 'SFSUB128'((int(X1),int(X2)),(int(Y1),int(Y2)),(int(R1),int(R2))) :-
415 init_softfloat,
416 sub128(X1,X2,Y1,Y2,R1,R2).
417
418 'SFMUL128'((int(X1),int(X2)),(int(Y1),int(Y2)),(int(R1),int(R2))) :-
419 init_softfloat,
420 mul128(X1,X2,Y1,Y2,R1,R2).
421
422 'SFDIV128'((int(X1),int(X2)),(int(Y1),int(Y2)),(int(R1),int(R2))) :-
423 init_softfloat,
424 div128(X1,X2,Y1,Y2,R1,R2).
425
426 'SFSQRT128'((int(X1),int(X2)),(int(R1),int(R2))) :-
427 init_softfloat,
428 sqrt128(X1,X2,R1,R2).
429
430 'SFMULADD128'((int(X1),int(X2)),(int(Y1),int(Y2)),(int(Z1),int(Z2)),(int(R1),int(R2))) :-
431 init_softfloat,
432 muladd128(X1,X2,Y1,Y2,Z1,Z2,R1,R2).
433 %128bit