A.5.7 Big Reals
Static Semantics
with Ada.Numerics.Big_Numbers.Big_Integers;
use all type Big_Integers.Big_Integer;
with Ada.Strings.Text_Buffers;
package Ada.Numerics.Big_Numbers.Big_Reals
with Preelaborate, Nonblocking, Global =>
null is
type Big_Real
is private
with Real_Literal => From_String,
Put_Image => Put_Image;
function Is_Valid (Arg : Big_Real)
return Boolean
with Convention => Intrinsic;
subtype Valid_Big_Real
is Big_Real
with Dynamic_Predicate => Is_Valid (Valid_Big_Real),
Predicate_Failure =>
raise Program_Error;
function "/" (Num, Den : Big_Integers.Valid_Big_Integer)
return Valid_Big_Real
with Pre => Den /= 0
or else raise Constraint_Error;
function Numerator
(Arg : Valid_Big_Real)
return Big_Integers.Valid_Big_Integer
with Post => (
if Arg = 0.0
then Numerator'Result = 0);
Reason: The postcondition of Numerator
cannot be complete as it cannot mention Denominator. Since the postcondition
of Denominator uses Numerator, we would get an infinite mutual recursion
if both postconditions are enabled. The postcondition of Denominator
serves as the postcondition for Numerator as well unless Arg = 0.0.
function Denominator (Arg : Valid_Big_Real)
return Big_Integers.Big_Positive
with Post =>
(
if Arg = 0.0
then Denominator'Result = 1
else Big_Integers.Greatest_Common_Divisor
(Numerator (Arg), Denominator'Result) = 1);
function To_Big_Real (Arg : Big_Integers.Valid_Big_Integer)
return Valid_Big_Real
is (Arg / 1);
function To_Real (Arg : Integer)
return Valid_Big_Real
is
(Big_Integers.To_Big_Integer (Arg) / 1);
function "=" (L, R : Valid_Big_Real) return Boolean;
function "<" (L, R : Valid_Big_Real) return Boolean;
function "<=" (L, R : Valid_Big_Real) return Boolean;
function ">" (L, R : Valid_Big_Real) return Boolean;
function ">=" (L, R : Valid_Big_Real) return Boolean;
function In_Range (Arg, Low, High : Valid_Big_Real)
return Boolean
is
(Low <= Arg
and Arg <= High);
generic
type Num
is digits <>;
package Float_Conversions
is
function To_Big_Real (Arg : Num)
return Valid_Big_Real;
function From_Big_Real (Arg : Valid_Big_Real)
return Num
with Pre => In_Range (Arg,
Low => To_Big_Real (Num'First),
High => To_Big_Real (Num'Last))
or else (
raise Constraint_Error);
end Float_Conversions;
generic
type Num
is delta <>;
package Fixed_Conversions
is
function To_Big_Real (Arg : Num)
return Valid_Big_Real;
function From_Big_Real (Arg : Valid_Big_Real)
return Num
with Pre => In_Range (Arg,
Low => To_Big_Real (Num'First),
High => To_Big_Real (Num'Last))
or else (
raise Constraint_Error);
end Fixed_Conversions;
function To_String (Arg : Valid_Big_Real;
Fore : Field := 2;
Aft : Field := 3;
Exp : Field := 0)
return String
with Post => To_String'Result'First = 1;
function From_String (Arg : String)
return Valid_Big_Real;
function To_Quotient_String (Arg : Valid_Big_Real)
return String
is
(To_String (Numerator (Arg)) & " / " & To_String (Denominator (Arg)));
function From_Quotient_String (Arg : String)
return Valid_Big_Real;
procedure Put_Image
(Buffer :
in out Ada.Strings.Text_Buffers.Root_Buffer_Type'Class;
Arg :
in Valid_Big_Real);
function "+" (L : Valid_Big_Real)
return Valid_Big_Real;
function "-" (L : Valid_Big_Real)
return Valid_Big_Real;
function "abs" (L : Valid_Big_Real)
return Valid_Big_Real;
function "+" (L, R : Valid_Big_Real)
return Valid_Big_Real;
function "-" (L, R : Valid_Big_Real)
return Valid_Big_Real;
function "*" (L, R : Valid_Big_Real)
return Valid_Big_Real;
function "/" (L, R : Valid_Big_Real)
return Valid_Big_Real;
function "**" (L : Valid_Big_Real; R : Integer)
return Valid_Big_Real;
function Min (L, R : Valid_Big_Real)
return Valid_Big_Real;
function Max (L, R : Valid_Big_Real)
return Valid_Big_Real;
private
... -- not specified by the language
end Ada.Numerics.Big_Numbers.Big_Reals;
{
AI12-0208-1}
{
AI12-0366-1}
To_String and From_String behave analogously to the Put and Get procedures
defined in Text_IO.Float_IO (in particular, with respect to the interpretation
of the Fore, Aft, and Exp parameters), except that Constraint_Error (not
Data_Error) is propagated in error cases. From_Quotient_String implements
the inverse function of To_Quotient_String; Constraint_Error is propagated
in error cases. Put_Image calls To_String, and writes the resulting value
to the buffer using Text_Buffers.Put.
{
AI12-0208-1}
For an instance of Float_Conversions or Fixed_Conversions, To_Big_Real
is exact (that is, the result represents exactly the same mathematical
value as the argument) and From_Big_Real is subject to the same precision
rules as a type conversion of a value of type T to the target type Num,
where T is a hypothetical floating point type whose model numbers include
all of the model numbers of Num as well as the exact mathematical value
of the argument.
{
AI12-0208-1}
The other functions have their usual mathematical meanings.
Dynamic Semantics
{
AI12-0208-1}
{
AI12-0366-1}
For purposes of determining whether predicate checks are performed as
part of default initialization, the type Big_Real is considered to have
a subcomponent that has a
default_expression.
Ramification:
{
AI12-0208-1}
This means that the elaboration of
Default_Initialized_Object : Valid_Big_Real;
is required to propagate Program_Error.
Implementation Requirements
{
AI12-0208-1}
{
AI12-0366-1}
No storage associated with a Big_Real object shall be lost upon assignment
or scope exit.
Implementation Note: {
AI12-0208-1}
The “No storage ... shall be lost” requirement does not preclude
implementation techniques such as caching or unique number tables.
Extensions to Ada 2012
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe