blob: 4118d2bb99c72d31b51f9bddfeb9f7fa3c7f3316 [file] [log] [blame]
------------------------------------------------------------------------------
-- --
-- GNAT RUN-TIME COMPONENTS --
-- --
-- ADA.NUMERICS.BIG_NUMBERS.BIG_REALS --
-- --
-- S p e c --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. In accordance with the copyright of that document, you can freely --
-- copy and modify this specification, provided that if you redistribute a --
-- modified version, any changes that you have made are clearly indicated. --
-- --
------------------------------------------------------------------------------
with Ada.Numerics.Big_Numbers.Big_Integers;
with Ada.Strings.Text_Buffers; use Ada.Strings.Text_Buffers;
package Ada.Numerics.Big_Numbers.Big_Reals
with Preelaborate
is
type Big_Real is private with
Real_Literal => From_Universal_Image,
Put_Image => Put_Image;
function Is_Valid (Arg : Big_Real) return Boolean
with
Convention => Intrinsic,
Global => null;
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 Global => null;
-- with Pre => (Big_Integers."/=" (Den, Big_Integers.To_Big_Integer (0))
-- or else Constraint_Error);
function Numerator
(Arg : Valid_Big_Real) return Big_Integers.Valid_Big_Integer
with Global => null;
function Denominator (Arg : Valid_Big_Real) return Big_Integers.Big_Positive
with
Post =>
(if Arg = To_Real (0)
then Big_Integers."=" (Denominator'Result,
Big_Integers.To_Big_Integer (1))
else Big_Integers."="
(Big_Integers.Greatest_Common_Divisor
(Numerator (Arg), Denominator'Result),
Big_Integers.To_Big_Integer (1))),
Global => null;
function To_Big_Real
(Arg : Big_Integers.Big_Integer)
return Valid_Big_Real is (Arg / Big_Integers.To_Big_Integer (1))
with Global => null;
function To_Real (Arg : Integer) return Valid_Big_Real is
(Big_Integers.To_Big_Integer (Arg) / Big_Integers.To_Big_Integer (1))
with Global => null;
function "=" (L, R : Valid_Big_Real) return Boolean with Global => null;
function "<" (L, R : Valid_Big_Real) return Boolean with Global => null;
function "<=" (L, R : Valid_Big_Real) return Boolean with Global => null;
function ">" (L, R : Valid_Big_Real) return Boolean with Global => null;
function ">=" (L, R : Valid_Big_Real) return Boolean with Global => null;
function In_Range (Arg, Low, High : Big_Real) return Boolean is
(Low <= Arg and then Arg <= High)
with Global => null;
generic
type Num is digits <>;
package Float_Conversions is
function To_Big_Real (Arg : Num) return Valid_Big_Real
with Global => null;
function From_Big_Real (Arg : 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),
Global => null;
end Float_Conversions;
generic
type Num is delta <>;
package Fixed_Conversions is
function To_Big_Real (Arg : Num) return Valid_Big_Real
with Global => null;
function From_Big_Real (Arg : 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),
Global => null;
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,
Global => null;
function From_String (Arg : String) return Valid_Big_Real
with Global => null;
function From_Universal_Image (Arg : String) return Valid_Big_Real
renames From_String;
function From_Universal_Image (Num, Den : String) return Valid_Big_Real is
(Big_Integers.From_Universal_Image (Num) /
Big_Integers.From_Universal_Image (Den))
with Global => null;
function To_Quotient_String (Arg : Big_Real) return String is
(Big_Integers.To_String (Numerator (Arg)) & " / "
& Big_Integers.To_String (Denominator (Arg)))
with Global => null;
function From_Quotient_String (Arg : String) return Valid_Big_Real
with Global => null;
procedure Put_Image (S : in out Root_Buffer_Type'Class; V : Big_Real);
function "+" (L : Valid_Big_Real) return Valid_Big_Real
with Global => null;
function "-" (L : Valid_Big_Real) return Valid_Big_Real
with Global => null;
function "abs" (L : Valid_Big_Real) return Valid_Big_Real
with Global => null;
function "+" (L, R : Valid_Big_Real) return Valid_Big_Real
with Global => null;
function "-" (L, R : Valid_Big_Real) return Valid_Big_Real
with Global => null;
function "*" (L, R : Valid_Big_Real) return Valid_Big_Real
with Global => null;
function "/" (L, R : Valid_Big_Real) return Valid_Big_Real
with Global => null;
function "**" (L : Valid_Big_Real; R : Integer) return Valid_Big_Real
with Global => null;
function Min (L, R : Valid_Big_Real) return Valid_Big_Real
with Global => null;
function Max (L, R : Valid_Big_Real) return Valid_Big_Real
with Global => null;
private
type Big_Real is record
Num, Den : Big_Integers.Big_Integer;
end record;
end Ada.Numerics.Big_Numbers.Big_Reals;