1		% (c) 2009-2022 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(softfloat, [
6		init_softfloat/0,
7		%itosf16/3, % Not defined anywhere
8
9		add16/3,
10		mul16/3,
11		sub16/3,
12		div16/3,
13		sqrt16/2,
14		muladd16/4,
15
16		add32/3,
17		mul32/3,
18		sub32/3,
19		div32/3,
20		sqrt32/2,
21		muladd32/4,
22
23		add64/3,
24		mul64/3,
25		sub64/3,
26		div64/3,
27		sqrt64/2,
28		muladd64/4,
29
30		add128/6,
31		mul128/6,
32		sub128/6,
33		div128/6,
34		sqrt128/4,
35		muladd128/8,
36
37		add80/6,
38		mul80/6,
39		sub80/6,
40		div80/6,
41		sqrt80/4
42		]).
43
44
45		:- use_module(probsrc(module_information),[module_info/2]).
46		:- module_info(group,cbc).
47		:- module_info(description,'This module provides software floating point operations via the berkley softfloat library.').
48
49		foreign_resource(softfloat,
50		[init,
51
52		add16,
53		mul16,
54		sub16,
55		div16,
56		sqrt16,
57		muladd16,
58
59		add32,
60		mul32,
61		sub32,
62		div32,
63		sqrt32,
64		muladd32,
65
66		add64,
67		mul64,
68		sub64,
69		div64,
70		sqrt64,
71		muladd64,
72
73		add128,
74		mul128,
75		sub128,
76		div128,
77		sqrt128,
78		muladd128,
79
80		add80,
81		mul80,
82		sub80,
83		div80,
84		sqrt80]).
85
86		foreign(init, c, init).
87
88		foreign(add16, c, add16(+float,+float,-float)).
89		foreign(mul16, c, mul16(+float,+float,-float)).
90		foreign(sub16, c, sub16(+float,+float,-float)).
91		foreign(div16, c, div16(+float,+float,-float)).
92		foreign(sqrt16, c, sqrt16(+float,-float)).
93		foreign(muladd16, c, muladd16(+float,+float,+float,-float)).
94
95		foreign(add32, c, add32(+float,+float,-float)).
96		foreign(mul32, c, mul32(+float,+float,-float)).
97		foreign(sub32, c, sub32(+float,+float,-float)).
98		foreign(div32, c, div32(+float,+float,-float)).
99		foreign(sqrt32, c, sqrt32(+float,-float)).
100		foreign(muladd32, c, muladd32(+float,+float,+float,-float)).
101
102		foreign(add64, c, add64(+float,+float,-float)).
103		foreign(mul64, c, mul64(+float,+float,-float)).
104		foreign(sub64, c, sub64(+float,+float,-float)).
105		foreign(div64, c, div64(+float,+float,-float)).
106		foreign(sqrt64, c, sqrt64(+float,-float)).
107		foreign(muladd64, c, muladd64(+float,+float,+float,-float)).
108
109		foreign(add80, c, add80(+integer,+integer, +integer,+integer, -integer,-integer)).
110		foreign(mul80, c, mul80(+integer,+integer, +integer,+integer, -integer,-integer)).
111		foreign(sub80, c, sub80(+integer,+integer, +integer,+integer, -integer,-integer)).
112		foreign(div80, c, div80(+integer,+integer, +integer,+integer, -integer,-integer)).
113		foreign(sqrt80, c, sqrt80(+integer,+integer, -integer,-integer)).
114
115		foreign(add128, c, add128(+integer,+integer, +integer,+integer, -integer,-integer)).
116		foreign(mul128, c, mul128(+integer,+integer, +integer,+integer, -integer,-integer)).
117		foreign(sub128, c, sub128(+integer,+integer, +integer,+integer, -integer,-integer)).
118		foreign(div128, c, div128(+integer,+integer, +integer,+integer, -integer,-integer)).
119		foreign(sqrt128, c, sqrt128(+integer,+integer, -integer,-integer)).
120		foreign(muladd128, c, muladd128(+integer,+integer, +integer,+integer, +integer,+integer, -integer,-integer)).
121
122		:- dynamic is_initialised/0.
123
124		init_softfloat :- is_initialised,!.
125		init_softfloat :-
126		safe_load_foreign_resource(softfloat),
127		init,
128		assertz(is_initialised).
129
130		safe_load_foreign_resource(R) :-
131		E=error(existence_error(_,_),_),
132		% print(loading_foreign_resource(R)),nl,
133		catch(
134		load_foreign_resource(library(R)),
135		E,
136		(format(user_error,'~n! Could not load ~w library!~n! Check that it is available in the lib folder of ProB.~n~n',[R]),throw(E))).