-- "=" --
---------
- function "=" (L, R : Big_Integer) return Boolean is
+ function "=" (L, R : Valid_Big_Integer) return Boolean is
begin
return Big_EQ (Get_Bignum (L), Get_Bignum (R));
end "=";
-- "<" --
---------
- function "<" (L, R : Big_Integer) return Boolean is
+ function "<" (L, R : Valid_Big_Integer) return Boolean is
begin
return Big_LT (Get_Bignum (L), Get_Bignum (R));
end "<";
-- "<=" --
----------
- function "<=" (L, R : Big_Integer) return Boolean is
+ function "<=" (L, R : Valid_Big_Integer) return Boolean is
begin
return Big_LE (Get_Bignum (L), Get_Bignum (R));
end "<=";
-- ">" --
---------
- function ">" (L, R : Big_Integer) return Boolean is
+ function ">" (L, R : Valid_Big_Integer) return Boolean is
begin
return Big_GT (Get_Bignum (L), Get_Bignum (R));
end ">";
-- ">=" --
----------
- function ">=" (L, R : Big_Integer) return Boolean is
+ function ">=" (L, R : Valid_Big_Integer) return Boolean is
begin
return Big_GE (Get_Bignum (L), Get_Bignum (R));
end ">=";
-- To_Big_Integer --
--------------------
- function To_Big_Integer (Arg : Integer) return Big_Integer is
+ function To_Big_Integer (Arg : Integer) return Valid_Big_Integer is
Result : Big_Integer;
begin
Set_Bignum (Result, To_Bignum (Long_Long_Integer (Arg)));
-- To_Big_Integer --
--------------------
- function To_Big_Integer (Arg : Int) return Big_Integer is
+ function To_Big_Integer (Arg : Int) return Valid_Big_Integer is
Result : Big_Integer;
begin
Set_Bignum (Result, To_Bignum (Long_Long_Integer (Arg)));
-- To_Big_Integer --
--------------------
- function To_Big_Integer (Arg : Int) return Big_Integer is
+ function To_Big_Integer (Arg : Int) return Valid_Big_Integer is
Result : Big_Integer;
begin
Set_Bignum (Result, To_Bignum (Unsigned_64 (Arg)));
Hex_Chars : constant array (0 .. 15) of Character := "0123456789ABCDEF";
function To_String
- (Arg : Big_Integer; Width : Field := 0; Base : Number_Base := 10)
+ (Arg : Valid_Big_Integer; Width : Field := 0; Base : Number_Base := 10)
return String
is
Big_Base : constant Big_Integer := To_Big_Integer (Integer (Base));
-- "+" --
---------
- function "+" (L : Big_Integer) return Big_Integer is
+ function "+" (L : Valid_Big_Integer) return Valid_Big_Integer is
Result : Big_Integer;
begin
Set_Bignum (Result, new Bignum_Data'(Get_Bignum (L).all));
-- "-" --
---------
- function "-" (L : Big_Integer) return Big_Integer is
+ function "-" (L : Valid_Big_Integer) return Valid_Big_Integer is
Result : Big_Integer;
begin
Set_Bignum (Result, Big_Neg (Get_Bignum (L)));
-- "abs" --
-----------
- function "abs" (L : Big_Integer) return Big_Integer is
+ function "abs" (L : Valid_Big_Integer) return Valid_Big_Integer is
Result : Big_Integer;
begin
Set_Bignum (Result, Big_Abs (Get_Bignum (L)));
-- "+" --
---------
- function "+" (L, R : Big_Integer) return Big_Integer is
+ function "+" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
Result : Big_Integer;
begin
Set_Bignum (Result, Big_Add (Get_Bignum (L), Get_Bignum (R)));
-- "-" --
---------
- function "-" (L, R : Big_Integer) return Big_Integer is
+ function "-" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
Result : Big_Integer;
begin
Set_Bignum (Result, Big_Sub (Get_Bignum (L), Get_Bignum (R)));
-- "*" --
---------
- function "*" (L, R : Big_Integer) return Big_Integer is
+ function "*" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
Result : Big_Integer;
begin
Set_Bignum (Result, Big_Mul (Get_Bignum (L), Get_Bignum (R)));
-- "/" --
---------
- function "/" (L, R : Big_Integer) return Big_Integer is
+ function "/" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
Result : Big_Integer;
begin
Set_Bignum (Result, Big_Div (Get_Bignum (L), Get_Bignum (R)));
-- "mod" --
-----------
- function "mod" (L, R : Big_Integer) return Big_Integer is
+ function "mod" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
Result : Big_Integer;
begin
Set_Bignum (Result, Big_Mod (Get_Bignum (L), Get_Bignum (R)));
-- "rem" --
-----------
- function "rem" (L, R : Big_Integer) return Big_Integer is
+ function "rem" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
Result : Big_Integer;
begin
Set_Bignum (Result, Big_Rem (Get_Bignum (L), Get_Bignum (R)));
-- "**" --
----------
- function "**" (L : Big_Integer; R : Natural) return Big_Integer is
+ function "**"
+ (L : Valid_Big_Integer; R : Natural) return Valid_Big_Integer is
begin
- -- Explicitly check for validity before allocating Exp so that
- -- the call to Get_Bignum below cannot raise an exception before
- -- we get a chance to free Exp.
-
- if not Is_Valid (L) then
- raise Constraint_Error with "invalid big integer";
- end if;
-
declare
Exp : Bignum := To_Bignum (Long_Long_Integer (R));
Result : Big_Integer;
-- Min --
---------
- function Min (L, R : Big_Integer) return Big_Integer is
+ function Min (L, R : Valid_Big_Integer) return Valid_Big_Integer is
(if L < R then L else R);
---------
-- Max --
---------
- function Max (L, R : Big_Integer) return Big_Integer is
+ function Max (L, R : Valid_Big_Integer) return Valid_Big_Integer is
(if L > R then L else R);
-----------------------------
-- Greatest_Common_Divisor --
-----------------------------
- function Greatest_Common_Divisor (L, R : Big_Integer) return Big_Positive is
+ function Greatest_Common_Divisor
+ (L, R : Valid_Big_Integer) return Big_Positive
+ is
function GCD (A, B : Big_Integer) return Big_Integer;
-- Recursive internal version
package Ada.Numerics.Big_Numbers.Big_Integers
with Preelaborate
is
- type Big_Integer is private with
- Integer_Literal => From_String,
- Put_Image => Put_Image;
+ type Big_Integer is private
+ with Integer_Literal => From_String,
+ Put_Image => Put_Image;
function Is_Valid (Arg : Big_Integer) return Boolean
with Convention => Intrinsic;
- function "=" (L, R : Big_Integer) return Boolean;
+ subtype Valid_Big_Integer is Big_Integer
+ with Dynamic_Predicate => Is_Valid (Valid_Big_Integer),
+ Predicate_Failure => raise Program_Error;
- function "<" (L, R : Big_Integer) return Boolean;
+ function "=" (L, R : Valid_Big_Integer) return Boolean;
- function "<=" (L, R : Big_Integer) return Boolean;
+ function "<" (L, R : Valid_Big_Integer) return Boolean;
- function ">" (L, R : Big_Integer) return Boolean;
+ function "<=" (L, R : Valid_Big_Integer) return Boolean;
- function ">=" (L, R : Big_Integer) return Boolean;
+ function ">" (L, R : Valid_Big_Integer) return Boolean;
- function To_Big_Integer (Arg : Integer) return Big_Integer;
+ function ">=" (L, R : Valid_Big_Integer) return Boolean;
+
+ function To_Big_Integer (Arg : Integer) return Valid_Big_Integer;
subtype Big_Positive is Big_Integer
with Dynamic_Predicate =>
type Int is range <>;
package Signed_Conversions is
- function To_Big_Integer (Arg : Int) return Big_Integer;
+ function To_Big_Integer (Arg : Int) return Valid_Big_Integer;
function From_Big_Integer (Arg : Big_Integer) return Int
with Pre => In_Range (Arg,
type Int is mod <>;
package Unsigned_Conversions is
- function To_Big_Integer (Arg : Int) return Big_Integer;
+ function To_Big_Integer (Arg : Int) return Valid_Big_Integer;
function From_Big_Integer (Arg : Big_Integer) return Int
with Pre => In_Range (Arg,
end Unsigned_Conversions;
- function To_String (Arg : Big_Integer;
+ function To_String (Arg : Valid_Big_Integer;
Width : Field := 0;
Base : Number_Base := 10) return String
with Post => To_String'Result'First = 1;
procedure Put_Image (S : in out Sink'Class; V : Big_Integer);
- function "+" (L : Big_Integer) return Big_Integer;
+ function "+" (L : Valid_Big_Integer) return Valid_Big_Integer;
- function "-" (L : Big_Integer) return Big_Integer;
+ function "-" (L : Valid_Big_Integer) return Valid_Big_Integer;
- function "abs" (L : Big_Integer) return Big_Integer;
+ function "abs" (L : Valid_Big_Integer) return Valid_Big_Integer;
- function "+" (L, R : Big_Integer) return Big_Integer;
+ function "+" (L, R : Valid_Big_Integer) return Valid_Big_Integer;
- function "-" (L, R : Big_Integer) return Big_Integer;
+ function "-" (L, R : Valid_Big_Integer) return Valid_Big_Integer;
- function "*" (L, R : Big_Integer) return Big_Integer;
+ function "*" (L, R : Valid_Big_Integer) return Valid_Big_Integer;
- function "/" (L, R : Big_Integer) return Big_Integer;
+ function "/" (L, R : Valid_Big_Integer) return Valid_Big_Integer;
- function "mod" (L, R : Big_Integer) return Big_Integer;
+ function "mod" (L, R : Valid_Big_Integer) return Valid_Big_Integer;
- function "rem" (L, R : Big_Integer) return Big_Integer;
+ function "rem" (L, R : Valid_Big_Integer) return Valid_Big_Integer;
- function "**" (L : Big_Integer; R : Natural) return Big_Integer;
+ function "**" (L : Valid_Big_Integer; R : Natural) return Valid_Big_Integer;
- function Min (L, R : Big_Integer) return Big_Integer;
+ function Min (L, R : Valid_Big_Integer) return Valid_Big_Integer;
- function Max (L, R : Big_Integer) return Big_Integer;
+ function Max (L, R : Valid_Big_Integer) return Valid_Big_Integer;
function Greatest_Common_Divisor
- (L, R : Big_Integer) return Big_Positive
+ (L, R : Valid_Big_Integer) return Big_Positive
with Pre => (L /= To_Big_Integer (0) and R /= To_Big_Integer (0))
or else (raise Constraint_Error);
-- "=" --
---------
- function "=" (L, R : Big_Integer) return Boolean is
+ function "=" (L, R : Valid_Big_Integer) return Boolean is
begin
return mpz_cmp (Get_Mpz (L), Get_Mpz (R)) = 0;
end "=";
-- "<" --
---------
- function "<" (L, R : Big_Integer) return Boolean is
+ function "<" (L, R : Valid_Big_Integer) return Boolean is
begin
return mpz_cmp (Get_Mpz (L), Get_Mpz (R)) < 0;
end "<";
-- "<=" --
----------
- function "<=" (L, R : Big_Integer) return Boolean is
+ function "<=" (L, R : Valid_Big_Integer) return Boolean is
begin
return mpz_cmp (Get_Mpz (L), Get_Mpz (R)) <= 0;
end "<=";
-- ">" --
---------
- function ">" (L, R : Big_Integer) return Boolean is
+ function ">" (L, R : Valid_Big_Integer) return Boolean is
begin
return mpz_cmp (Get_Mpz (L), Get_Mpz (R)) > 0;
end ">";
-- ">=" --
----------
- function ">=" (L, R : Big_Integer) return Boolean is
+ function ">=" (L, R : Valid_Big_Integer) return Boolean is
begin
return mpz_cmp (Get_Mpz (L), Get_Mpz (R)) >= 0;
end ">=";
-- To_Big_Integer --
--------------------
- function To_Big_Integer (Arg : Integer) return Big_Integer is
+ function To_Big_Integer (Arg : Integer) return Valid_Big_Integer is
Result : Big_Integer;
begin
Allocate (Result);
-- To_Integer --
----------------
- function To_Integer (Arg : Big_Integer) return Integer is
+ function To_Integer (Arg : Valid_Big_Integer) return Integer is
begin
return Integer (mpz_get_si (Get_Mpz (Arg)));
end To_Integer;
-- To_Big_Integer --
--------------------
- function To_Big_Integer (Arg : Int) return Big_Integer is
+ function To_Big_Integer (Arg : Int) return Valid_Big_Integer is
Result : Big_Integer;
begin
Allocate (Result);
-- From_Big_Integer --
----------------------
- function From_Big_Integer (Arg : Big_Integer) return Int is
+ function From_Big_Integer (Arg : Valid_Big_Integer) return Int is
begin
return Int (mpz_get_si (Get_Mpz (Arg)));
end From_Big_Integer;
-- To_Big_Integer --
--------------------
- function To_Big_Integer (Arg : Int) return Big_Integer is
+ function To_Big_Integer (Arg : Int) return Valid_Big_Integer is
Result : Big_Integer;
begin
Allocate (Result);
-- From_Big_Integer --
----------------------
- function From_Big_Integer (Arg : Big_Integer) return Int is
+ function From_Big_Integer (Arg : Valid_Big_Integer) return Int is
begin
return Int (mpz_get_ui (Get_Mpz (Arg)));
end From_Big_Integer;
---------------
function To_String
- (Arg : Big_Integer; Width : Field := 0; Base : Number_Base := 10)
+ (Arg : Valid_Big_Integer; Width : Field := 0; Base : Number_Base := 10)
return String
is
function mpz_get_str
-- From_String --
-----------------
- function From_String (Arg : String) return Big_Integer is
+ function From_String (Arg : String) return Valid_Big_Integer is
function mpz_set_str
(this : access mpz_t;
str : System.Address;
-- "+" --
---------
- function "+" (L : Big_Integer) return Big_Integer is
+ function "+" (L : Valid_Big_Integer) return Valid_Big_Integer is
Result : Big_Integer;
begin
Set_Mpz (Result, new mpz_t);
-- "-" --
---------
- function "-" (L : Big_Integer) return Big_Integer is
+ function "-" (L : Valid_Big_Integer) return Valid_Big_Integer is
Result : Big_Integer;
begin
Allocate (Result);
-- "abs" --
-----------
- function "abs" (L : Big_Integer) return Big_Integer is
+ function "abs" (L : Valid_Big_Integer) return Valid_Big_Integer is
procedure mpz_abs (ROP : access mpz_t; OP : access constant mpz_t);
pragma Import (C, mpz_abs, "__gmpz_abs");
-- "+" --
---------
- function "+" (L, R : Big_Integer) return Big_Integer is
+ function "+" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
procedure mpz_add
(ROP : access mpz_t; OP1, OP2 : access constant mpz_t);
pragma Import (C, mpz_add, "__gmpz_add");
-- "-" --
---------
- function "-" (L, R : Big_Integer) return Big_Integer is
+ function "-" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
Result : Big_Integer;
begin
Allocate (Result);
-- "*" --
---------
- function "*" (L, R : Big_Integer) return Big_Integer is
+ function "*" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
procedure mpz_mul
(ROP : access mpz_t; OP1, OP2 : access constant mpz_t);
pragma Import (C, mpz_mul, "__gmpz_mul");
-- "/" --
---------
- function "/" (L, R : Big_Integer) return Big_Integer is
+ function "/" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
procedure mpz_tdiv_q (Q : access mpz_t; N, D : access constant mpz_t);
pragma Import (C, mpz_tdiv_q, "__gmpz_tdiv_q");
begin
-- "mod" --
-----------
- function "mod" (L, R : Big_Integer) return Big_Integer is
+ function "mod" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
procedure mpz_mod (R : access mpz_t; N, D : access constant mpz_t);
pragma Import (C, mpz_mod, "__gmpz_mod");
-- result is always non-negative
-- "rem" --
-----------
- function "rem" (L, R : Big_Integer) return Big_Integer is
+ function "rem" (L, R : Valid_Big_Integer) return Valid_Big_Integer is
procedure mpz_tdiv_r (R : access mpz_t; N, D : access constant mpz_t);
pragma Import (C, mpz_tdiv_r, "__gmpz_tdiv_r");
-- R will have the same sign as N.
-- "**" --
----------
- function "**" (L : Big_Integer; R : Natural) return Big_Integer is
+ function "**"
+ (L : Valid_Big_Integer; R : Natural) return Valid_Big_Integer
+ is
procedure mpz_pow_ui (ROP : access mpz_t;
BASE : access constant mpz_t;
EXP : unsigned_long);
-- Min --
---------
- function Min (L, R : Big_Integer) return Big_Integer is
+ function Min (L, R : Valid_Big_Integer) return Valid_Big_Integer is
(if L < R then L else R);
---------
-- Max --
---------
- function Max (L, R : Big_Integer) return Big_Integer is
+ function Max (L, R : Valid_Big_Integer) return Valid_Big_Integer is
(if L > R then L else R);
-----------------------------
-- Greatest_Common_Divisor --
-----------------------------
- function Greatest_Common_Divisor (L, R : Big_Integer) return Big_Positive is
+ function Greatest_Common_Divisor
+ (L, R : Valid_Big_Integer) return Big_Positive
+ is
procedure mpz_gcd
(ROP : access mpz_t; Op1, Op2 : access constant mpz_t);
pragma Import (C, mpz_gcd, "__gmpz_gcd");
-- "/" --
---------
- function "/" (Num, Den : Big_Integer) return Big_Real is
+ function "/" (Num, Den : Valid_Big_Integer) return Valid_Big_Real is
Result : Big_Real;
begin
if Den = To_Big_Integer (0) then
-- Numerator --
---------------
- function Numerator (Arg : Big_Real) return Big_Integer is
- (if Is_Valid (Arg.Num) then Arg.Num
- else raise Constraint_Error with "invalid big real");
+ function Numerator (Arg : Valid_Big_Real) return Valid_Big_Integer is
+ (Arg.Num);
-----------------
-- Denominator --
-----------------
- function Denominator (Arg : Big_Real) return Big_Positive is
- (if Is_Valid (Arg.Den) then Arg.Den
- else raise Constraint_Error with "invalid big real");
+ function Denominator (Arg : Valid_Big_Real) return Big_Positive is
+ (Arg.Den);
---------
-- "=" --
---------
- function "=" (L, R : Big_Real) return Boolean is
+ function "=" (L, R : Valid_Big_Real) return Boolean is
(abs L.Num = abs R.Num and then L.Den = R.Den);
---------
-- "<" --
---------
- function "<" (L, R : Big_Real) return Boolean is
+ function "<" (L, R : Valid_Big_Real) return Boolean is
(abs L.Num * R.Den < abs R.Num * L.Den);
----------
-- "<=" --
----------
- function "<=" (L, R : Big_Real) return Boolean is (not (R < L));
+ function "<=" (L, R : Valid_Big_Real) return Boolean is (not (R < L));
---------
-- ">" --
---------
- function ">" (L, R : Big_Real) return Boolean is (R < L);
+ function ">" (L, R : Valid_Big_Real) return Boolean is (R < L);
----------
-- ">=" --
----------
- function ">=" (L, R : Big_Real) return Boolean is (not (L < R));
+ function ">=" (L, R : Valid_Big_Real) return Boolean is (not (L < R));
-----------------------
-- Float_Conversions --
-- To_Big_Real --
-----------------
- function To_Big_Real (Arg : Num) return Big_Real is
+ function To_Big_Real (Arg : Num) return Valid_Big_Real is
begin
return From_String (Arg'Image);
end To_Big_Real;
-- To_Big_Real --
-----------------
- function To_Big_Real (Arg : Num) return Big_Real is
+ function To_Big_Real (Arg : Num) return Valid_Big_Real is
begin
return From_String (Arg'Image);
end To_Big_Real;
---------------
function To_String
- (Arg : Big_Real; Fore : Field := 2; Aft : Field := 3; Exp : Field := 0)
- return String
+ (Arg : Valid_Big_Real;
+ Fore : Field := 2;
+ Aft : Field := 3;
+ Exp : Field := 0) return String
is
Zero : constant Big_Integer := To_Big_Integer (0);
Ten : constant Big_Integer := To_Big_Integer (10);
-- From_Quotient_String --
--------------------------
- function From_Quotient_String (Arg : String) return Big_Real is
+ function From_Quotient_String (Arg : String) return Valid_Big_Real is
Index : Natural := 0;
begin
for J in Arg'First + 1 .. Arg'Last - 1 loop
-- "+" --
---------
- function "+" (L : Big_Real) return Big_Real is
+ function "+" (L : Valid_Big_Real) return Valid_Big_Real is
Result : Big_Real;
begin
- if not Is_Valid (L) then
- raise Constraint_Error with "invalid big real";
- end if;
-
Result.Num := L.Num;
Result.Den := L.Den;
return Result;
-- "-" --
---------
- function "-" (L : Big_Real) return Big_Real is
- (if Is_Valid (L) then (Num => -L.Num, Den => L.Den)
- else raise Constraint_Error with "invalid big real");
+ function "-" (L : Valid_Big_Real) return Valid_Big_Real is
+ (Num => -L.Num, Den => L.Den);
-----------
-- "abs" --
-----------
- function "abs" (L : Big_Real) return Big_Real is
- (if Is_Valid (L) then (Num => abs L.Num, Den => L.Den)
- else raise Constraint_Error with "invalid big real");
+ function "abs" (L : Valid_Big_Real) return Valid_Big_Real is
+ (Num => abs L.Num, Den => L.Den);
---------
-- "+" --
---------
- function "+" (L, R : Big_Real) return Big_Real is
+ function "+" (L, R : Valid_Big_Real) return Valid_Big_Real is
Result : Big_Real;
begin
- if not Is_Valid (L) or not Is_Valid (R) then
- raise Constraint_Error with "invalid big real";
- end if;
-
Result.Num := L.Num * R.Den + R.Num * L.Den;
Result.Den := L.Den * R.Den;
Normalize (Result);
-- "-" --
---------
- function "-" (L, R : Big_Real) return Big_Real is
+ function "-" (L, R : Valid_Big_Real) return Valid_Big_Real is
Result : Big_Real;
begin
- if not Is_Valid (L) or not Is_Valid (R) then
- raise Constraint_Error with "invalid big real";
- end if;
-
Result.Num := L.Num * R.Den - R.Num * L.Den;
Result.Den := L.Den * R.Den;
Normalize (Result);
-- "*" --
---------
- function "*" (L, R : Big_Real) return Big_Real is
+ function "*" (L, R : Valid_Big_Real) return Valid_Big_Real is
Result : Big_Real;
begin
- if not Is_Valid (L) or not Is_Valid (R) then
- raise Constraint_Error with "invalid big real";
- end if;
-
Result.Num := L.Num * R.Num;
Result.Den := L.Den * R.Den;
Normalize (Result);
-- "/" --
---------
- function "/" (L, R : Big_Real) return Big_Real is
+ function "/" (L, R : Valid_Big_Real) return Valid_Big_Real is
Result : Big_Real;
begin
- if not Is_Valid (L) or not Is_Valid (R) then
- raise Constraint_Error with "invalid big real";
- end if;
-
Result.Num := L.Num * R.Den;
Result.Den := L.Den * R.Num;
Normalize (Result);
-- "**" --
----------
- function "**" (L : Big_Real; R : Integer) return Big_Real is
+ function "**" (L : Valid_Big_Real; R : Integer) return Valid_Big_Real is
Result : Big_Real;
begin
- if not Is_Valid (L) then
- raise Constraint_Error with "invalid big real";
- end if;
-
if R = 0 then
Result.Num := To_Big_Integer (1);
Result.Den := To_Big_Integer (1);
-- Min --
---------
- function Min (L, R : Big_Real) return Big_Real is (if L < R then L else R);
+ function Min (L, R : Valid_Big_Real) return Valid_Big_Real is
+ (if L < R then L else R);
---------
-- Max --
---------
- function Max (L, R : Big_Real) return Big_Real is (if L > R then L else R);
+ function Max (L, R : Valid_Big_Real) return Valid_Big_Real is
+ (if L > R then L else R);
---------------
-- Normalize --
function Is_Valid (Arg : Big_Real) return Boolean
with Convention => Intrinsic;
- function "/" (Num, Den : Big_Integers.Big_Integer) return Big_Real;
--- with Pre => (if Big_Integers."=" (Den, Big_Integers.To_Big_Integer (0))
--- then raise Constraint_Error);
+ subtype Valid_Big_Real is Big_Real
+ with Dynamic_Predicate => Is_Valid (Valid_Big_Real),
+ Predicate_Failure => raise Program_Error;
- function Numerator (Arg : Big_Real) return Big_Integers.Big_Integer;
+ function "/"
+ (Num, Den : Big_Integers.Valid_Big_Integer) return Valid_Big_Real;
+-- with Pre => (Big_Integers."/=" (Den, Big_Integers.To_Big_Integer (0))
+-- or else Constraint_Error);
- function Denominator (Arg : Big_Real) return Big_Integers.Big_Positive
+ function Numerator
+ (Arg : Valid_Big_Real) return Big_Integers.Valid_Big_Integer;
+
+ function Denominator (Arg : Valid_Big_Real) return Big_Integers.Big_Positive
with Post =>
- (Arg = To_Real (0)) or else
- (Big_Integers."="
- (Big_Integers.Greatest_Common_Divisor
- (Numerator (Arg), Denominator'Result),
- Big_Integers.To_Big_Integer (1)));
+ (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)));
function To_Big_Real
(Arg : Big_Integers.Big_Integer)
- return Big_Real is (Arg / Big_Integers.To_Big_Integer (1));
+ return Valid_Big_Real is (Arg / Big_Integers.To_Big_Integer (1));
- function To_Real (Arg : Integer) return Big_Real is
+ function To_Real (Arg : Integer) return Valid_Big_Real is
(Big_Integers.To_Big_Integer (Arg) / Big_Integers.To_Big_Integer (1));
- function "=" (L, R : Big_Real) return Boolean;
+ function "=" (L, R : Valid_Big_Real) return Boolean;
- function "<" (L, R : Big_Real) return Boolean;
+ function "<" (L, R : Valid_Big_Real) return Boolean;
- function "<=" (L, R : Big_Real) return Boolean;
+ function "<=" (L, R : Valid_Big_Real) return Boolean;
- function ">" (L, R : Big_Real) return Boolean;
+ function ">" (L, R : Valid_Big_Real) return Boolean;
- function ">=" (L, R : Big_Real) return Boolean;
+ function ">=" (L, R : Valid_Big_Real) return Boolean;
function In_Range (Arg, Low, High : Big_Real) return Boolean is
(Low <= Arg and then Arg <= High);
type Num is digits <>;
package Float_Conversions is
- function To_Big_Real (Arg : Num) return Big_Real;
+ function To_Big_Real (Arg : Num) return Valid_Big_Real;
function From_Big_Real (Arg : Big_Real) return Num
with Pre => In_Range (Arg,
type Num is delta <>;
package Fixed_Conversions is
- function To_Big_Real (Arg : Num) return Big_Real;
+ function To_Big_Real (Arg : Num) return Valid_Big_Real;
function From_Big_Real (Arg : Big_Real) return Num
with Pre => In_Range (Arg,
end Fixed_Conversions;
- function To_String (Arg : Big_Real;
+ function To_String (Arg : Valid_Big_Real;
Fore : Field := 2;
Aft : Field := 3;
Exp : Field := 0) return String
(Big_Integers.To_String (Numerator (Arg)) & " / "
& Big_Integers.To_String (Denominator (Arg)));
- function From_Quotient_String (Arg : String) return Big_Real;
+ function From_Quotient_String (Arg : String) return Valid_Big_Real;
procedure Put_Image (S : in out Sink'Class; V : Big_Real);
- function "+" (L : Big_Real) return Big_Real;
+ function "+" (L : Valid_Big_Real) return Valid_Big_Real;
- function "-" (L : Big_Real) return Big_Real;
+ function "-" (L : Valid_Big_Real) return Valid_Big_Real;
- function "abs" (L : Big_Real) return Big_Real;
+ function "abs" (L : Valid_Big_Real) return Valid_Big_Real;
- function "+" (L, R : Big_Real) return Big_Real;
+ function "+" (L, R : Valid_Big_Real) return Valid_Big_Real;
- function "-" (L, R : Big_Real) return Big_Real;
+ function "-" (L, R : Valid_Big_Real) return Valid_Big_Real;
- function "*" (L, R : Big_Real) return Big_Real;
+ function "*" (L, R : Valid_Big_Real) return Valid_Big_Real;
- function "/" (L, R : Big_Real) return Big_Real;
+ function "/" (L, R : Valid_Big_Real) return Valid_Big_Real;
- function "**" (L : Big_Real; R : Integer) return Big_Real;
+ function "**" (L : Valid_Big_Real; R : Integer) return Valid_Big_Real;
- function Min (L, R : Big_Real) return Big_Real;
+ function Min (L, R : Valid_Big_Real) return Valid_Big_Real;
- function Max (L, R : Big_Real) return Big_Real;
+ function Max (L, R : Valid_Big_Real) return Valid_Big_Real;
private