1------------------------------------------------------------------------------
2--                                                                          --
3--                         GNAT RUN-TIME COMPONENTS                         --
4--                                                                          --
5--                   ADA.NUMERICS.BIG_NUMBERS.BIG_REALS                     --
6--                                                                          --
7--                                 S p e c                                  --
8--                                                                          --
9-- This specification is derived from the Ada Reference Manual for use with --
10-- GNAT.  In accordance with the copyright of that document, you can freely --
11-- copy and modify this specification,  provided that if you redistribute a --
12-- modified version,  any changes that you have made are clearly indicated. --
13--                                                                          --
14------------------------------------------------------------------------------
15
16with Ada.Numerics.Big_Numbers.Big_Integers;
17
18with Ada.Strings.Text_Output; use Ada.Strings.Text_Output;
19
20package Ada.Numerics.Big_Numbers.Big_Reals
21  with Preelaborate
22is
23   type Big_Real is private with
24     Real_Literal => From_String,
25     Put_Image    => Put_Image;
26
27   function Is_Valid (Arg : Big_Real) return Boolean
28   with
29     Convention => Intrinsic,
30     Global     => null;
31
32   subtype Valid_Big_Real is Big_Real
33     with Dynamic_Predicate => Is_Valid (Valid_Big_Real),
34          Predicate_Failure => raise Program_Error;
35
36   function "/"
37     (Num, Den : Big_Integers.Valid_Big_Integer) return Valid_Big_Real
38     with Global => null;
39--   with Pre => (Big_Integers."/=" (Den, Big_Integers.To_Big_Integer (0))
40--                or else Constraint_Error);
41
42   function Numerator
43     (Arg : Valid_Big_Real) return Big_Integers.Valid_Big_Integer
44     with Global => null;
45
46   function Denominator (Arg : Valid_Big_Real) return Big_Integers.Big_Positive
47   with
48     Post   =>
49       (if Arg = To_Real (0)
50        then Big_Integers."=" (Denominator'Result,
51                               Big_Integers.To_Big_Integer (1))
52        else Big_Integers."="
53               (Big_Integers.Greatest_Common_Divisor
54                 (Numerator (Arg), Denominator'Result),
55                Big_Integers.To_Big_Integer (1))),
56     Global => null;
57
58   function To_Big_Real
59     (Arg : Big_Integers.Big_Integer)
60     return Valid_Big_Real is (Arg / Big_Integers.To_Big_Integer (1))
61     with Global => null;
62
63   function To_Real (Arg : Integer) return Valid_Big_Real is
64     (Big_Integers.To_Big_Integer (Arg) / Big_Integers.To_Big_Integer (1))
65     with Global => null;
66
67   function "=" (L, R : Valid_Big_Real) return Boolean with Global => null;
68
69   function "<" (L, R : Valid_Big_Real) return Boolean with Global => null;
70
71   function "<=" (L, R : Valid_Big_Real) return Boolean with Global => null;
72
73   function ">" (L, R : Valid_Big_Real) return Boolean with Global => null;
74
75   function ">=" (L, R : Valid_Big_Real) return Boolean with Global => null;
76
77   function In_Range (Arg, Low, High : Big_Real) return Boolean is
78     (Low <= Arg and then Arg <= High)
79     with Global => null;
80
81   generic
82      type Num is digits <>;
83   package Float_Conversions is
84
85      function To_Big_Real (Arg : Num) return Valid_Big_Real
86        with Global => null;
87
88      function From_Big_Real (Arg : Big_Real) return Num
89      with
90        Pre    => In_Range (Arg,
91                            Low  => To_Big_Real (Num'First),
92                            High => To_Big_Real (Num'Last))
93                   or else (raise Constraint_Error),
94        Global => null;
95
96   end Float_Conversions;
97
98   generic
99      type Num is delta <>;
100   package Fixed_Conversions is
101
102      function To_Big_Real (Arg : Num) return Valid_Big_Real
103        with Global => null;
104
105      function From_Big_Real (Arg : Big_Real) return Num
106      with
107        Pre    => In_Range (Arg,
108                            Low  => To_Big_Real (Num'First),
109                            High => To_Big_Real (Num'Last))
110                   or else (raise Constraint_Error),
111        Global => null;
112
113   end Fixed_Conversions;
114
115   function To_String (Arg  : Valid_Big_Real;
116                       Fore : Field := 2;
117                       Aft  : Field := 3;
118                       Exp  : Field := 0) return String
119   with
120     Post   => To_String'Result'First = 1,
121     Global => null;
122
123   function From_String (Arg : String) return Valid_Big_Real
124     with Global => null;
125   function From_String (Numerator, Denominator : String) return Valid_Big_Real
126     with Global => null;
127
128   function To_Quotient_String (Arg : Big_Real) return String is
129     (Big_Integers.To_String (Numerator (Arg)) & " / "
130      & Big_Integers.To_String (Denominator (Arg)))
131     with Global => null;
132
133   function From_Quotient_String (Arg : String) return Valid_Big_Real
134     with Global => null;
135
136   procedure Put_Image (S : in out Sink'Class; V : Big_Real);
137
138   function "+" (L : Valid_Big_Real) return Valid_Big_Real
139     with Global => null;
140
141   function "-" (L : Valid_Big_Real) return Valid_Big_Real
142     with Global => null;
143
144   function "abs" (L : Valid_Big_Real) return Valid_Big_Real
145     with Global => null;
146
147   function "+" (L, R : Valid_Big_Real) return Valid_Big_Real
148     with Global => null;
149
150   function "-" (L, R : Valid_Big_Real) return Valid_Big_Real
151     with Global => null;
152
153   function "*" (L, R : Valid_Big_Real) return Valid_Big_Real
154     with Global => null;
155
156   function "/" (L, R : Valid_Big_Real) return Valid_Big_Real
157     with Global => null;
158
159   function "**" (L : Valid_Big_Real; R : Integer) return Valid_Big_Real
160     with Global => null;
161
162   function Min (L, R : Valid_Big_Real) return Valid_Big_Real
163     with Global => null;
164
165   function Max (L, R : Valid_Big_Real) return Valid_Big_Real
166     with Global => null;
167
168private
169
170   type Big_Real is record
171      Num, Den : Big_Integers.Big_Integer;
172   end record;
173
174end Ada.Numerics.Big_Numbers.Big_Reals;
175