File : s-libm-ada.ads
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT COMPILER COMPONENTS --
4 -- --
5 -- S Y S T E M . L I B M --
6 -- --
7 -- S p e c --
8 -- --
9 -- Copyright (C) 2014-2015, Free Software Foundation, Inc. --
10 -- --
11 -- GNAT is free software; you can redistribute it and/or modify it under --
12 -- terms of the GNU General Public License as published by the Free Soft- --
13 -- ware Foundation; either version 3, or (at your option) any later ver- --
14 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
15 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
16 -- or FITNESS FOR A PARTICULAR PURPOSE. --
17 -- --
18 -- --
19 -- --
20 -- --
21 -- --
22 -- You should have received a copy of the GNU General Public License and --
23 -- a copy of the GCC Runtime Library Exception along with this program; --
24 -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
25 -- <http://www.gnu.org/licenses/>. --
26 -- --
27 -- GNAT was originally developed by the GNAT team at New York University. --
28 -- Extensive contributions were provided by Ada Core Technologies Inc. --
29 -- --
30 ------------------------------------------------------------------------------
31
32 -- This is the Ada Cert Math specific version of s-libm.ads
33
34 with Ada.Numerics;
35
36 package System.Libm is
37 pragma Pure;
38
39 Ln_2 : constant := 0.69314_71805_59945_30941_72321_21458_17656_80755;
40 Ln_3 : constant := 1.09861_22886_68109_69139_52452_36922_52570_46474;
41 Half_Ln_2 : constant := Ln_2 / 2.0;
42 Inv_Ln_2 : constant := 1.0 / Ln_2;
43 Half_Pi : constant := Ada.Numerics.Pi / 2.0;
44 Third_Pi : constant := Ada.Numerics.Pi / 3.0;
45 Quarter_Pi : constant := Ada.Numerics.Pi / 4.0;
46 Sixth_Pi : constant := Ada.Numerics.Pi / 6.0;
47
48 Max_Red_Trig_Arg : constant := 0.26 * Ada.Numerics.Pi;
49 -- This constant representing the maximum absolute value of the reduced
50 -- argument of the approximation functions for Sin, Cos and Tan. A value
51 -- slightly larger than Pi / 4 is used. The reduction doesn't reduce to
52 -- an interval strictly within +-Pi / 4, as that would complicate the
53 -- reduction code.
54
55 One_Over_Pi : constant := 1.0 / Ada.Numerics.Pi;
56 Two_Over_Pi : constant := 2.0 / Ada.Numerics.Pi;
57
58 Sqrt_2 : constant := 1.41421_35623_73095_04880_16887_24209_69807_85696;
59 Sqrt_3 : constant := 1.73205_08075_68877_29352_74463_41505_87236_69428;
60
61 Root16_Half : constant := 0.95760_32806_98573_64693_63056_35147_91544;
62 -- Sixteenth root of 0.5
63
64 Sqrt_Half : constant := 0.70710_67811_86547_52440_08443_62104;
65
66 subtype Quadrant is Integer range 0 .. 3;
67
68 generic
69 type T is digits <>;
70 with function Sqrt (X : T) return T is <>;
71 with function Approx_Asin (X : T) return T is <>;
72 function Generic_Acos (X : T) return T;
73
74 generic
75 type T is digits <>;
76 with function Approx_Atan (X : T) return T is <>;
77 function Generic_Atan2 (Y, X : T) return T;
78
79 generic
80 type T is digits <>;
81 procedure Generic_Pow_Special_Cases
82 (Left : T;
83 Right : T;
84 Is_Special : out Boolean;
85 Result : out T);
86
87 generic
88 type T is private;
89 Mantissa : Positive;
90 with function "-" (X : T) return T is <>;
91 with function "+" (X, Y : T) return T is <>;
92 with function "-" (X, Y : T) return T is <>;
93 with function "*" (X, Y : T) return T is <>;
94 with function "/" (X, Y : T) return T is <>;
95 with function "<=" (X, Y : T) return Boolean is <>;
96 with function "abs" (X : T) return T is <>;
97 with function Exact (X : Long_Long_Float) return T is <>;
98 with function Maximum_Relative_Error (X : T) return Float is <>;
99 with function Sqrt (X : T) return T is <>;
100 package Generic_Approximations is
101 Epsilon : constant Float := 2.0**(1 - Mantissa);
102 -- The approximations in this package will work well for single
103 -- precision floating point types.
104
105 function Approx_Asin (X : T) return T
106 with Pre => abs X <= Exact (0.25),
107 Post => abs Approx_Asin'Result <= Exact (Half_Pi);
108 -- @llr Approx_Asin
109 -- The Approx_Asin function shallapproximate the mathematical function
110 -- arcsin (sqrt (x)) / sqrt (x) - 1.0 on -0.25 .. 0.25.
111 --
112 -- Ada accuracy requirements:
113 -- The approximation MRE shall be XXX T'Model_Epsilon.
114
115 function Approx_Atan (X : T) return T
116 with Pre => abs X <= Exact (Sqrt_3),
117 Post => abs (Approx_Atan'Result) <= Exact (Half_Pi) and then
118 Maximum_Relative_Error (Approx_Atan'Result) <= 2.0 * Epsilon;
119 -- @llr Approx_Atan
120 -- The Approx_Atan approximates the mathematical inverse tangent on
121 -- -Sqrt (3) .. Sqrt (3)
122 --
123 -- Accuracy requirements:
124 -- The approximation MRE is XXX T'Model_Epsilon
125
126 function Approx_Cos (X : T) return T
127 with Pre => abs (X) <= Exact (Max_Red_Trig_Arg),
128 Post => abs (Approx_Cos'Result) <= Exact (1.0)
129 and then Maximum_Relative_Error (Approx_Cos'Result)
130 <= 2.0 * Epsilon;
131 -- @llr Approx_Cos
132 -- The Approx_Cos approximates the mathematical cosine on
133 -- -0.26 * Pi .. 0.26 * Pi
134 --
135 -- Accuracy requirements:
136 -- The approximation MRE is XXX T'Model_Epsilon
137
138 function Approx_Exp (X : T) return T
139 with Pre => abs (X) <= Exact (Ln_2 / 2.0),
140 Post => Exact (0.0) <= Approx_Exp'Result and then
141 Maximum_Relative_Error (Approx_Exp'Result) <= 2.0 * Epsilon;
142 -- @llr Approx_Exp
143 -- The Approx_Exp function approximates the mathematical exponent on
144 -- -Ln (2.0) / 2.0 .. Ln (2.0) / 2.0
145 --
146 -- Accuracy requirements:
147 -- The approximation MRE is XXX T'Model_Epsilon
148
149 function Approx_Exp2 (X : T) return T
150 with Pre => abs (X) <= Exact (Ln_2 / 2.0),
151 Post => Exact (0.0) <= Approx_Exp2'Result and then
152 Maximum_Relative_Error (Approx_Exp2'Result) <= 2.0 * Epsilon;
153 -- @llr Approx_Exp2
154 -- The Approx_Exp2 function approximates the mathematical function
155 -- (x-> 2.0 ** x) on -Ln (2.0) / 2.0 .. Ln (2.0) / 2.0
156 --
157 -- Accuracy requirements:
158 -- The approximation MRE is XXX T'Model_Epsilon
159
160 function Approx_Log (X : T) return T
161 with
162 Pre => Exact (Sqrt_2 / 2.0) <= X and then
163 X <= Exact (Sqrt_2),
164 Post => Maximum_Relative_Error (Approx_Log'Result) <= 2.0 * Epsilon;
165 -- @llr Approx_Log
166 -- The Approx_Log function approximates the mathematical logarithm on
167 -- Sqrt (2.0) /2.0 .. Sqrt (2.0)
168 --
169 -- Accuracy requirements:
170 -- The approximation MRE is XXX T'Model_Epsilon
171
172 function Approx_Power_Log (X : T) return T;
173 -- @llr Approx_Power_Log
174 -- The Approx_Power_Log approximates the function
175 -- (x -> Log ((x-1) / (x+1), base => 2)) on the interval
176 -- TODO
177 --
178 -- Accuracy requirements:
179 -- The approximation MRE is XXX T'Model_Epsilon
180
181 function Approx_Sin (X : T) return T
182 with Pre => (abs X) <= Exact (Max_Red_Trig_Arg),
183 Post => abs Approx_Sin'Result <= Exact (1.0) and then
184 Maximum_Relative_Error (Approx_Sin'Result) <= 2.0 * Epsilon;
185 -- @llr Approx_Sin
186 -- The Approx_Sin function approximates the mathematical sine on
187 -- -0.26 * Pi .. 0.26 * Pi
188 --
189 -- Ada accuracy requirements:
190 -- The approximation MRE is XXX T'Model_Epsilon
191
192 function Approx_Sinh (X : T) return T
193 with Pre => True, -- The original X >= 0.0 and X <= 1.0, fails ???
194 Post => abs Approx_Sinh'Result <= Exact
195 ((Ada.Numerics.e - 1.0 / Ada.Numerics.e) / 2.0)
196 and then Maximum_Relative_Error (Approx_Sinh'Result)
197 <= 2.0 * Epsilon;
198 -- @llr Approx_Sinh
199 -- The Approx_Sinh function approximates the mathematical hyperbolic
200 -- sine on XXX
201 --
202 -- Accuracy requirements:
203 -- The approximation MRE is XXX T'Model_Epsilon
204
205 function Approx_Tan (X : T) return T
206 with Pre => abs X <= Exact (Max_Red_Trig_Arg),
207 Post =>
208 Maximum_Relative_Error (Approx_Tan'Result) <= 2.0 * Epsilon;
209 -- @llr Approx_Tan
210 -- The Approx_Tan function approximates the mathematical tangent on
211 -- -0.26 * Pi .. 0.26 * Pi
212 --
213 -- Accuracy requirements:
214 -- The approximation MRE is XXX T'Model_Epsilon
215
216 function Approx_Cot (X : T) return T
217 with Pre => abs X <= Exact (Max_Red_Trig_Arg),
218 Post =>
219 Maximum_Relative_Error (Approx_Cot'Result) <= 2.0 * Epsilon;
220 -- @llr Approx_Cot
221 -- The Approx_Cot function approximates the mathematical cotangent on
222 -- -0.26 * Pi .. 0.26 * Pi
223 --
224 -- Accuracy requirements:
225 -- The approximation MRE is XXX T'Model_Epsilon
226
227 function Approx_Tanh (X : T) return T
228 with Pre => Exact (0.0) <= X and then X <= Exact (Ln_3 / 2.0),
229 Post => abs (Approx_Tanh'Result) <= Exact (Half_Pi)
230 and then Maximum_Relative_Error (Approx_Tanh'Result)
231 <= 2.0 * Epsilon;
232 -- @llr Approx_Tanh
233 -- The Approx_Tanh function approximates the mathematical hyperbolic
234 -- tangent on 0.0 .. Ln (3.0) / 2.0
235 --
236 -- Accuracy requirements:
237 -- The approximation MRE is XXX T'Model_Epsilon
238
239 function Asin (X : T) return T
240 with Pre => abs X <= Exact (1.0),
241 Post => Maximum_Relative_Error (Asin'Result) <= 400.0 * Epsilon;
242 -- @llr Asin
243 -- The Asin function has a maximum relative error of 2 epsilon.
244 end Generic_Approximations;
245
246 end System.Libm;