-------------------------------------------------------------------------------
-- (C) Altran Praxis Limited
-------------------------------------------------------------------------------
--
-- The SPARK toolset is free software; you can redistribute it and/or modify it
-- under terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 3, or (at your option) any later
-- version. The SPARK toolset is distributed in the hope that it will be
-- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
-- Public License for more details. You should have received a copy of the GNU
-- General Public License distributed with the SPARK toolset; see file
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
-- the license.
--
--=============================================================================

package body Maths is

   type Division_Result_Type is record
      Quotient, Remnant : Part;
   end record;

   --------------------------------------------------------------------------
   --                        Local Procedures
   --------------------------------------------------------------------------

   --------------------------------------------------------------------------
   -- Low-level conversions and utilities
   --------------------------------------------------------------------------

   --------------------------------------------------------------------------
   -- Converts extended Character to digit
   -- only works for '0'..'9' and 'A'..'F'.  ParseString will ensure that
   -- no other values will be passed to it.
   function CharToDigit (Ch : Character) return Digit
   -- # pre ((Ch >= '0') and (Ch <= '9')) or ((Ch >= 'A') and (Ch <= 'F'));
   is
      Valu : Digit;
   begin
      if Ch in '0' .. '9' then
         Valu := (Character'Pos (Ch) - Character'Pos ('0'));
      else
         Valu := ((Character'Pos (Ch) - Character'Pos ('A')) + 10);
      end if;
      return Valu;
   end CharToDigit;

   --------------------------------------------------------------------------
   -- Converts digit (Integer subtype 0..15) to extended Character
   function DigitToChar (Dig : Digit) return Character is
      Ch : Character;
   begin
      if Dig <= 9 then
         Ch := Character'Val (Dig + Character'Pos ('0'));
      else
         Ch := Character'Val ((Dig + Character'Pos ('A')) - 10);
      end if;
      return Ch;
   end DigitToChar;

   --------------------------------------------------------------------------
   -- Returns Larger of 2 Naturals
   function Max (X, Y : Natural) return Natural is
      Larger : Natural;
   begin
      if X > Y then
         Larger := X;
      else
         Larger := Y;
      end if;
      return Larger;
   end Max;

   --------------------------------------------------------------------------
   -- final check of value overflow or underflow before returning Value
   -- to caller from one of the exported procedures below.  Any existing
   -- error is preserved ie. overflow will only be reported if an earlier
   -- error is not detected.
   function OverflowCheck (ExistingError : ErrorCode;
                           Num           : Value) return ErrorCode is
      Result : ErrorCode;
   begin
      if ExistingError = NoError and then (Num.Numerator.Overflowed or Num.Denominator.Overflowed) then
         Result := OverFlow;
      else
         Result := ExistingError;
      end if;
      return Result;
   end OverflowCheck;

   --------------------------------------------------------------------------
   -- Low-level manipulation of part-Value arrays
   function StripLeadingZeros (P : Part) return Part is
      PLocal : Part;
   begin
      PLocal := P;
      while (PLocal.Length > 1) and then (PLocal.Numerals (PLocal.Length) = 0) loop
         PLocal.Length := PLocal.Length - 1;
      end loop;
      return PLocal;
   end StripLeadingZeros;

   --------------------------------------------------------------------------
   -- Multiplies Value part by 10
   function ShiftUpPart (P : Part) return Part is
      PLocal : Part;
   begin
      PLocal := P;
      if PLocal.Length = MaxLength then ----------can't shift it without overflow
         PLocal.Overflowed := True;
      else                              ----------room to shift
         for i in reverse PosRange range 1 .. PLocal.Length loop
            PLocal.Numerals (i + 1) := PLocal.Numerals (i);
         end loop;

         PLocal.Numerals (1) := 0;
         PLocal.Length       := P.Length + 1;
         PLocal              := StripLeadingZeros (PLocal); --in case we have just turned 0 into 00
      end if;
      return PLocal;
   end ShiftUpPart;

   --------------------------------------------------------------------------
   -- Divides Value Part by 10
   function ShiftDownPart (P : Part) return Part is
      PLocal : Part;
   begin
      PLocal := P;
      if PLocal.Length = 1 then
         PLocal.Numerals (1) := 0;
      else
         for i in PosRange range 2 .. PLocal.Length loop
            PLocal.Numerals (i - 1) := PLocal.Numerals (i);
         end loop;

         PLocal.Numerals (PLocal.Length) := 0;
         PLocal.Length                   := PLocal.Length - 1;
      end if;
      return PLocal;
   end ShiftDownPart;

   --------------------------------------------------------------------------
   -- Basic arithmetic on Part Values
   --------------------------------------------------------------------------
   -- Symbolically adds two Part Values together
   function AddPart (FirstPart, SecondPart : Part) return Part is
      Length                   : PosRange;
      Carry, IntermediateValue : Natural;
      Result                   : Part;
   begin
      Carry := 0;

      Result            := ZeroPart;
      Result.Overflowed := FirstPart.Overflowed or SecondPart.Overflowed;        -- propagate error

      Length := Max (FirstPart.Length, SecondPart.Length);
      for i in PosRange range 1 .. Length loop
         IntermediateValue := (Natural (FirstPart.Numerals (i)) + Natural (SecondPart.Numerals (i))) + Carry;

         if IntermediateValue >= 10 then
            IntermediateValue := IntermediateValue - 10;
            Carry             := 1;
         else
            Carry := 0;
         end if;
         Result.Numerals (i) := Digit (IntermediateValue);
      end loop;

      if Carry /= 0 then
         if Length = MaxLength then              -- can't carry without overflow
            Result.Overflowed := True;
         else                                    -- ok to extend Value
            Length                   := Length + 1;
            Result.Numerals (Length) := 1;
         end if;
      end if;
      Result.Length := Length;
      return Result;
   end AddPart;

   --------------------------------------------------------------------------
   -- Symbolically subtracts Part Values
   -- WARNING second parameter must be <= first before the call
   function SubtractPart (Larger, Smaller : Part) return Part is
      Length            : PosRange;
      Borrow            : Natural;
      IntermediateValue : Integer;
      Result            : Part;
   begin
      Borrow            := 0;
      Result            := ZeroPart;
      Result.Overflowed := Larger.Overflowed or Smaller.Overflowed;           -- propagate error

      Length        := Max (Larger.Length, Smaller.Length);
      Result.Length := Length;

      for i in PosRange range 1 .. Length loop
         IntermediateValue := (Natural (Larger.Numerals (i)) - Natural (Smaller.Numerals (i))) - Borrow;

         if IntermediateValue < 0 then
            IntermediateValue := IntermediateValue + 10;
            Borrow            := 1;
         else
            Borrow := 0;
         end if;
         Result.Numerals (i) := Digit (IntermediateValue);
      end loop;

      return StripLeadingZeros (Result);
   end SubtractPart;

   --------------------------------------------------------------------------
   -- NB.  These Parts are considered unsigned
   function GreaterPart (FirstPart, SecondPart : Part) return Boolean is
      IsGreater : Boolean;
      i         : LengthRange;
   begin
      if FirstPart.Length = SecondPart.Length then
         IsGreater := False;
         i         := FirstPart.Length;
         loop
            if FirstPart.Numerals (i) /= SecondPart.Numerals (i) then
               IsGreater := FirstPart.Numerals (i) > SecondPart.Numerals (i);
               exit;
            end if;

            exit when i = 1;
            i := i - 1;
         end loop;

      else
         IsGreater := FirstPart.Length > SecondPart.Length;
      end if;
      return IsGreater;
   end GreaterPart;

   --------------------------------------------------------------------------
   -- NB.  These Parts are considered unsigned
   function LesserPart (FirstPart, SecondPart : Part) return Boolean is
      IsLesser : Boolean;
      i        : LengthRange;
   begin
      if FirstPart.Length = SecondPart.Length then
         IsLesser := False;
         i        := FirstPart.Length;

         loop
            if FirstPart.Numerals (i) /= SecondPart.Numerals (i) then
               IsLesser := FirstPart.Numerals (i) < SecondPart.Numerals (i);
               exit;
            end if;

            exit when i = 1;
            i := i - 1;
         end loop;

      else
         IsLesser := FirstPart.Length < SecondPart.Length;
      end if;
      return IsLesser;
   end LesserPart;

   --------------------------------------------------------------------------
   -- Multiplies a Part Value by a single digit (range 0..15).
   -- Used in conversion of based literal to a Value and as Part of the
   -- Value multiply routines
   function SingleDigitMult (P : Part;
                             D : Digit) return Part is
      Carry, IntermediateValue : Natural;
      Result                   : Part;
   begin
      Carry             := 0;
      Result            := ZeroPart;
      Result.Overflowed := P.Overflowed;           --propagate error
      Result.Length     := P.Length;

      for i in PosRange range 1 .. P.Length loop
         IntermediateValue := Natural (P.Numerals (i)) * Natural (D) + Carry;

         Result.Numerals (i) := Digit (IntermediateValue mod 10);
         Carry               := IntermediateValue / 10;
      end loop;

      while Carry /= 0 loop
         if Result.Length = MaxLength then       -- can't carry without overflow
            Result.Overflowed := True;
            exit;
         end if;

         Result.Length                   := Result.Length + 1;
         Result.Numerals (Result.Length) := Digit (Carry mod 10);

         Carry := Carry / 10;
      end loop;

      return Result;
   end SingleDigitMult;

   --------------------------------------------------------------------------
   -- Symbolically multiples 2 Part Values together
   function MultPart (FirstPart, SecondPart : Part) return Part is
      FirstPartLocal, Result : Part;
   begin
      Result            := ZeroPart;
      Result.Overflowed := FirstPart.Overflowed or SecondPart.Overflowed;      -- propagate error
      FirstPartLocal    := FirstPart;

      for i in PosRange range 1 .. SecondPart.Length loop
         Result         := AddPart (Result, SingleDigitMult (FirstPartLocal, SecondPart.Numerals (i)));
         FirstPartLocal := ShiftUpPart (FirstPartLocal);
      end loop;
      return Result;
   end MultPart;

   --------------------------------------------------------------------------
   --Digit by digit long div of one Value Part by another
   --Do not call with bot=0

   function DivPart (Top, Bot : Part) return Division_Result_Type is
      subtype GoesIndexRange is Integer range 0 .. 9;
      type GoesArray is array (GoesIndexRange) of Part;
      GoesDigit               : GoesIndexRange;
      Goes                    : GoesArray;
      ResultLocal, CurrentTry : Part;
      Column                  : Natural;

      ---------------------------

      -- builds array of 1*divisor..9*divisor
      procedure BuildGoesTable
      --# global in     Bot;
      --#           out Goes;
      --# derives Goes from Bot;
      is
      begin
         Goes     := GoesArray'(GoesIndexRange => ZeroPart);
         Goes (1) := Bot;

         for i in GoesIndexRange range 2 .. 9 loop
            Goes (i) := AddPart (Goes (i - 1), Bot);
         end loop;
      end BuildGoesTable;

      ---------------------------

      function FindGoes (Into : Part) return GoesIndexRange
      --# global in Goes;
      is
         Result : GoesIndexRange;
      begin
         Result := 0;
         for i in reverse Integer range 1 .. 9 loop
            if (LesserPart (Goes (i), Into)) or (Goes (i) = Into) then
               Result := i;
               exit;
            end if;
         end loop;
         return Result;
      end FindGoes;

      ---------------------------

      procedure StoreDigit (Dig  : in     GoesIndexRange;
                            Dest : in out Part)
      --# derives Dest from *,
      --#                   Dig;
      --NB. This method of stroring digit automatically excludes leading zeros
      --    since Length only increases once a non-zero is present.
      is
      begin
         Dest              := ShiftUpPart (Dest);
         Dest.Numerals (1) := Digit (Dig);
      end StoreDigit;

      ---------------------------

   begin -- DivPart
      BuildGoesTable;

      ResultLocal := ZeroPart;
      CurrentTry  := ZeroPart;
      Column      := Top.Length;           -- start at MSD
      loop
         exit when Column = 0;

         StoreDigit (Integer (Top.Numerals (Column)), CurrentTry);
         Column    := Column - 1;
         GoesDigit := FindGoes (CurrentTry);
         StoreDigit (GoesDigit, ResultLocal);
         if GoesDigit /= 0 then
            CurrentTry := SubtractPart (CurrentTry, Goes (GoesDigit));
         end if;
      end loop;

      return Division_Result_Type'(Quotient => ResultLocal,
                                   Remnant  => CurrentTry);
   end DivPart;

   --------------------------------------------------------------------------
   -- Conversions too and from Part Values
   --------------------------------------------------------------------------

   --Converts an Ada Natural type to a Part Value;
   function NaturalToPart (Int : Natural) return Part is
      IntLocal : Natural;
      Result   : Part;
   begin
      Result        := ZeroPart;
      IntLocal      := Int;
      Result.Length := 0;
      while IntLocal > 0 loop
         Result.Length                   := Result.Length + 1;
         Result.Numerals (Result.Length) := Digit (IntLocal mod 10);
         IntLocal                        := IntLocal / 10;
      end loop;
      return Result;
   end NaturalToPart;

   --------------------------------------------------------------------------

   -- Convert String to Natural - NB. not done symbolically
   -- Assumes decimal
   function String_To_Natural (Str : E_Strings.T) return Natural is
      Position_Multiplier, Total : Natural;
   begin
      Position_Multiplier := 1;
      Total               := 0;

      for I in reverse E_Strings.Positions range 1 .. E_Strings.Get_Length (E_Str => Str) loop
         Total := Total + Position_Multiplier * Natural (CharToDigit (E_Strings.Get_Element (E_Str => Str,
                                                                                             Pos   => I)));

         Position_Multiplier := Position_Multiplier * 10;
      end loop;
      return Total;
   end String_To_Natural;

   --------------------------------------------------------------------------
   -- Produces Value Part from string interpreting it as being to base
   function String_To_Part (Base : Natural;
                            Str  : E_Strings.T) return Part is
      Position_Multiplier, Base_Part, Result : Part;
   begin
      Result              := ZeroPart;
      Position_Multiplier := OnePart;
      Base_Part           := NaturalToPart (Base);

      for I in reverse E_Strings.Positions range 1 .. E_Strings.Get_Length (E_Str => Str) loop
         Result              :=
           AddPart
           (Result,
            SingleDigitMult (Position_Multiplier, CharToDigit (E_Strings.Get_Element (E_Str => Str,
                                                                                      Pos   => I))));
         Position_Multiplier := MultPart (Position_Multiplier, Base_Part);
      end loop;
      return Result;
   end String_To_Part;

   --------------------------------------------------------------------------
   -- Produces Value Part from decimal string more quickly than String_To_Part
   function Dec_String_To_Part (Str : E_Strings.T) return Part is
      Result : Part;
      Hi     : Natural;
   begin
      Result := ZeroPart;
      Hi     := E_Strings.Get_Length (E_Str => Str);
      if Hi <= MaxLength then
         for I in Natural range 1 .. Hi loop
            Result.Numerals (I) := CharToDigit (E_Strings.Get_Element (E_Str => Str,
                                                                       Pos   => (Hi - I) + 1));
         end loop;
         Result.Length := E_Strings.Get_Length (E_Str => Str);
      else
         Result.Overflowed := True;
      end if;
      return Result;
   end Dec_String_To_Part;

   --------------------------------------------------------------------------
   -- Normalization routines for rational pairs
   --------------------------------------------------------------------------

   -- removes zeros symmetrically from Numerator and Denominator
   procedure NormalizeByTen (Num : in out Value)
   --# derives Num from *;
   is
   begin
      -- strip mutual trailing zeros
      while (Num.Numerator.Numerals (1) = 0) and (Num.Denominator.Numerals (1) = 0) loop
         Num.Numerator   := ShiftDownPart (Num.Numerator);
         Num.Denominator := ShiftDownPart (Num.Denominator);
      end loop;
   end NormalizeByTen;

   --------------------------------------------------------------------------
   -- Routine to find GCD of 2 Parts
   function GCD (FirstPart, SecondPart : Part) return Part is
      FirstPartLocal, SecondPartLocal : Part;
      DivisionResult                  : Division_Result_Type;
   begin
      FirstPartLocal  := FirstPart;
      SecondPartLocal := SecondPart;
      loop
         exit when SecondPartLocal = ZeroPart;

         DivisionResult  := DivPart (FirstPartLocal, SecondPartLocal);
         FirstPartLocal  := SecondPartLocal;
         SecondPartLocal := DivisionResult.Remnant;
      end loop;
      return FirstPartLocal;
   end GCD;

   --------------------------------------------------------------------------

   procedure Normalize (Num : in out Value)
   --# derives Num from *;
   is
      Divisor : Part;
   begin
      NormalizeByTen (Num); --does not reduce no of GCD iterations but shortens each one
      if not (Num.Numerator.Overflowed or Num.Denominator.Overflowed) then
         Divisor         := GCD (Num.Numerator, Num.Denominator);
         Num.Numerator   := DivPart (Num.Numerator, Divisor).Quotient;
         Num.Denominator := DivPart (Num.Denominator, Divisor).Quotient;
      end if;
   end Normalize;

   --------------------------------------------------------------------------
   -- Higher level arithmetic routines
   --------------------------------------------------------------------------

   -- Correctly handles ordering and sign of subtraction of +ve Numerator Parts
   -- of Value but leaves Denominator and Value types alone so can be
   -- use by both Integer and Real routines.  Callers should ensure that field
   -- Sort of Result is set correctly.
   procedure NumeratorSubtract (FirstNum, SecondNum : in     Value;
                                Result              : in out Value)
   --# derives Result from *,
   --#                     FirstNum,
   --#                     SecondNum;
   is
   begin
      if GreaterPart (FirstNum.Numerator, SecondNum.Numerator) then
         Result.Numerator := SubtractPart (FirstNum.Numerator, SecondNum.Numerator);
      elsif GreaterPart (SecondNum.Numerator, FirstNum.Numerator) then
         Result.Numerator  := SubtractPart (SecondNum.Numerator, FirstNum.Numerator);
         Result.IsPositive := False;
      else
         Result.Numerator := ZeroPart;
      end if;
   end NumeratorSubtract;

   --------------------------------------------------------------------------
   -- Correctly handles adding (including ordering and signs) of numerator Parts
   -- of Values but leaves Denominator and Value types alone so can be
   -- use by both Integer and Real routines.  Callers should ensure that field
   -- Sort of Result is set correctly.
   procedure NumeratorAdd (FirstNum, SecondNum : in     Value;
                           Result              : in out Value)
   --# derives Result from *,
   --#                     FirstNum,
   --#                     SecondNum;
   is
   begin
      if FirstNum.IsPositive and SecondNum.IsPositive then
         Result.Numerator := AddPart (FirstNum.Numerator, SecondNum.Numerator);

      elsif not (FirstNum.IsPositive or SecondNum.IsPositive) then
         Result.Numerator  := AddPart (FirstNum.Numerator, SecondNum.Numerator);
         Result.IsPositive := False;

      elsif FirstNum.IsPositive and not SecondNum.IsPositive then
         NumeratorSubtract (FirstNum  => FirstNum,
                            SecondNum => SecondNum,
                            Result    => Result);

      elsif not FirstNum.IsPositive and SecondNum.IsPositive then
         NumeratorSubtract (FirstNum  => SecondNum,
                            SecondNum => FirstNum,
                            Result    => Result);
      end if;
   end NumeratorAdd;

   --------------------------------------------------------------------------
   -- Modifies 2 Values such that their Denominators are the same
   procedure CommonDenominator (FirstNum, SecondNum           : in     Value;
                                ModifiedFirst, ModifiedSecond :    out Value)
   --# derives ModifiedFirst,
   --#         ModifiedSecond from FirstNum,
   --#                             SecondNum;
   is
      CommonDenom : Part;
   begin
      ModifiedFirst  := FirstNum;
      ModifiedSecond := SecondNum;
      if not (FirstNum.Denominator = SecondNum.Denominator) then
         CommonDenom                := MultPart (FirstNum.Denominator, SecondNum.Denominator);
         ModifiedFirst.Numerator    := MultPart (FirstNum.Numerator, SecondNum.Denominator);
         ModifiedSecond.Numerator   := MultPart (SecondNum.Numerator, FirstNum.Denominator);
         ModifiedFirst.Denominator  := CommonDenom;
         ModifiedSecond.Denominator := CommonDenom;
      end if;
   end CommonDenominator;

   --------------------------------------------------------------------------

   procedure RealAdd (FirstNum, SecondNum : in     Value;
                      Result              :    out Value;
                      Ok                  :    out ErrorCode)
   --# derives Ok,
   --#         Result from FirstNum,
   --#                     SecondNum;
   is
      FirstNumLocal, SecondNumLocal, Res : Value;
   begin
      Res := ZeroReal;
      CommonDenominator (FirstNum, SecondNum, FirstNumLocal, SecondNumLocal);
      NumeratorAdd (FirstNumLocal, SecondNumLocal, Res);
      Res.Denominator := FirstNumLocal.Denominator;
      Normalize (Res);
      Result := Res;
      Ok     := OverflowCheck (NoError, Res);
   end RealAdd;

   --------------------------------------------------------------------------

   procedure IntegerMultiply (FirstNum, SecondNum : in     Value;
                              Result              :    out Value;
                              Ok                  :    out ErrorCode)
   --# derives Ok,
   --#         Result from FirstNum,
   --#                     SecondNum;
   is
      Res : Value;
   begin
      Res            := ZeroInteger;
      Res.Numerator  := StripLeadingZeros (MultPart (FirstNum.Numerator, SecondNum.Numerator));
      Res.IsPositive := (FirstNum.IsPositive = SecondNum.IsPositive);
      Ok             := OverflowCheck (NoError, Res);
      Result         := Res;
   end IntegerMultiply;

   --------------------------------------------------------------------------

   procedure RealMultiply (FirstNum, SecondNum : in     Value;
                           Result              :    out Value;
                           Ok                  :    out ErrorCode)
   --# derives Ok,
   --#         Result from FirstNum,
   --#                     SecondNum;
   is
      Res : Value;
   begin
      Res             := ZeroReal;
      Res.Numerator   := MultPart (FirstNum.Numerator, SecondNum.Numerator);
      Res.Denominator := MultPart (FirstNum.Denominator, SecondNum.Denominator);
      Res.IsPositive  := (FirstNum.IsPositive = SecondNum.IsPositive);
      Normalize (Res);
      Result := Res;
      Ok     := OverflowCheck (NoError, Res);
   end RealMultiply;

   --------------------------------------------------------------------------

   procedure RealDivide (FirstNum, SecondNum : in     Value;
                         Result              :    out Value;
                         Ok                  :    out ErrorCode)
   --# derives Ok,
   --#         Result from FirstNum,
   --#                     SecondNum;
   is

      ----------------------------------------

      function Invert (N : Value) return Value is
      begin
         return Value'(Numerator   => N.Denominator,
                       Denominator => N.Numerator,
                       IsPositive  => N.IsPositive,
                       Sort        => N.Sort);
      end Invert;

      ----------------------------------------

   begin -- RealDivide
      RealMultiply (FirstNum, Invert (SecondNum), Result, Ok);
   end RealDivide;

   --------------------------------------------------------------------------

   procedure GreaterLocal (FirstNum, SecondNum : in     Value;
                           Result              :    out Boolean;
                           Ok                  :    out ErrorCode)
   --# derives Ok,
   --#         Result from FirstNum,
   --#                     SecondNum;
   is
      FirstLocal, SecondLocal : Value;
      LocalOk                 : ErrorCode;
   begin
      LocalOk := NoError;
      if FirstNum.Sort /= SecondNum.Sort then
         Result  := False;
         LocalOk := TypeMismatch;
      else --legal types
         if FirstNum.Sort = RealValue then           --put on common Denominator
            CommonDenominator (FirstNum, SecondNum, FirstLocal, SecondLocal);
         else --this covers Integer, enumeration and Boolean
            FirstLocal  := FirstNum;
            SecondLocal := SecondNum;
         end if;
         if FirstLocal.IsPositive then
            if SecondLocal.IsPositive then                  -- both positive
               Result := GreaterPart (FirstLocal.Numerator, SecondLocal.Numerator);
            else  -- first positive and second Value is negative
               Result := True;
            end if;
         else  --first Value is negative
            if SecondLocal.IsPositive then     -- first negative, second positive
               Result := False;
            else  --both Values are negative
               Result := LesserPart (FirstLocal.Numerator, SecondLocal.Numerator);
            end if;
         end if;
         LocalOk := OverflowCheck (LocalOk, FirstLocal);
         LocalOk := OverflowCheck (LocalOk, SecondLocal);
      end if;
      Ok := LocalOk;
   end GreaterLocal;

   --------------------------------------------------------------------------
   -- Non-exported procedure used by Remainder and Modulus Only
   --------------------------------------------------------------------------

   procedure ModRemLegalityCheck (FirstNum, SecondNum : in     Value;
                                  Err                 :    out ErrorCode)
   --# derives Err from FirstNum,
   --#                  SecondNum;
   is
   begin
      if (FirstNum.Sort = IntegerValue) and (SecondNum.Sort = IntegerValue) then
         if SecondNum.Numerator = ZeroPart then
            Err := DivideByZero;
         else  --this is the legal case we can do something with
            Err := NoError;
         end if;
      elsif (FirstNum.Sort = RealValue) and (SecondNum.Sort = RealValue) then
         Err := IllegalOperation;
      else
         Err := TypeMismatch;
      end if;
   end ModRemLegalityCheck;

   -------------------------------------------------------------------------

   procedure ParseString
     (S                                               : in     E_Strings.T;
      Decimal_Point_Found, Exponent_Found, Base_Found :    out Boolean;
      Base                                            :    out Natural;
      Core_String, Exp_String                         :    out E_Strings.T;
      Exp_Sign                                        :    out Character;
      Places_After_Point                              :    out E_Strings.Lengths;
      Legal_Syntax                                    :    out Boolean)
   --# derives Base,
   --#         Base_Found,
   --#         Core_String,
   --#         Decimal_Point_Found,
   --#         Exponent_Found,
   --#         Exp_Sign,
   --#         Exp_String,
   --#         Legal_Syntax,
   --#         Places_After_Point  from S;

   -- NOTES
   --   BaseString will be set to "10" if Base_Found = False
   --   Exp_String is "0" if ExpFound = False
   --   Exp_Sign is plus if ExpFound = False
   --   PlacesAferPoint is 0 if Decimal_Point_Found = False
   --   Legal_Syntax only implies that String looks like an Ada literal
      is separate;

   -------------------------------------------------------------------------
   -- PartToBits - converts a Part into a Bits array, with LSB in element 0
   -- All insignificant MSBs are set to False
   -------------------------------------------------------------------------
   function PartToBits (A : in Part) return Bits is
      R     : Bits;
      Power : Part;
      Q     : Division_Result_Type;
   begin
      R     := ZeroBits;
      Power := OnePart;

      for J in BinaryLengthRange loop
         Q     := DivPart (DivPart (A, Power).Quotient, TwoPart);
         R (J) := Q.Remnant /= ZeroPart;
         Power := SingleDigitMult (Power, 2);
         exit when Power.Overflowed;
      end loop;
      return R;
   end PartToBits;

   -------------------------------------------------------------------------
   -- BitsToPart - converts a Bits array into a Part, assuming LSB in
   -- element 0.
   -------------------------------------------------------------------------
   function BitsToPart (B : in Bits) return Part is
      P     : Part;
      Power : Part;
   begin
      P     := ZeroPart;
      Power := OnePart;

      for J in BinaryLengthRange loop
         if B (J) then
            P := AddPart (P, Power);
         end if;
         Power := SingleDigitMult (Power, 2);
         exit when Power.Overflowed;
      end loop;

      return P;
   end BitsToPart;

   -------------------------------------------------------------------------
   --------------------------------------------------------------------------
   --                        Exported Procedures
   --------------------------------------------------------------------------
   --------------------------------------------------------------------------

   procedure LiteralToValue (Str : in     LexTokenManager.Lex_String;
                             Num :    out Value;
                             OK  :    out ErrorCode) is separate;

   ----------------------------------------------------------------------------

   function IntegerToValue (I : Integer) return Value is
      IsPositive : Boolean;
      Numerator  : Part;
      ValSoFar   : Integer;
      NextDigit  : Digit;
      Length     : LengthRange;
   begin --IntegerToValue
      Numerator  := ZeroPart;
      IsPositive := I >= 0;
      ValSoFar   := abs (I);

      if ValSoFar /= 0 then
         Length := 1;
         loop
            NextDigit                   := Digit (ValSoFar mod 10);
            ValSoFar                    := ValSoFar / 10;
            Numerator.Numerals (Length) := NextDigit;
            exit when ValSoFar = 0;

            Length := Length + 1;
         end loop;
         Numerator.Length := Length;
      end if;

      return Value'(Numerator   => Numerator,
                    Denominator => OnePart,
                    IsPositive  => IsPositive,
                    Sort        => IntegerValue);
   end IntegerToValue;

   ---------------------------------------------------------------------------

   procedure StorageRep (Num : in     Value;
                         Rep :    out LexTokenManager.Lex_String)
   --670
   is
      Str      : E_Strings.T := E_Strings.Empty_String;
      StoreRep : LexTokenManager.Lex_String;

      procedure BuildString (IsPos   : in Boolean;
                             PartVal : in Part)
      --# global in out Str;
      --# derives Str from *,
      --#                  IsPos,
      --#                  PartVal;
      is
      begin
         if not IsPos then
            E_Strings.Append_Char (E_Str => Str,
                                   Ch    => '-');
         end if;
         for I in LengthRange range 1 .. PartVal.Length loop
            E_Strings.Append_Char (E_Str => Str,
                                   Ch    => DigitToChar (PartVal.Numerals (I)));
         end loop;
      end BuildString;

      -----------------

      procedure AppendDenominator (PartVal : in Part)
      --# global in out Str;
      --# derives Str from *,
      --#                  PartVal;
      is
      begin
         E_Strings.Append_Char (E_Str => Str,
                                Ch    => '/');
         for I in LengthRange range 1 .. PartVal.Length loop
            E_Strings.Append_Char (E_Str => Str,
                                   Ch    => DigitToChar (PartVal.Numerals (I)));
         end loop;
      end AppendDenominator;

   begin
      case Num.Sort is
         when UnknownValue =>
            StoreRep := LexTokenManager.Null_String;
         when TruthValue =>
            if Num.IsPositive then
               StoreRep := LexTokenManager.True_Token;
            else
               StoreRep := LexTokenManager.False_Token;
            end if;
         when IntegerValue =>
            BuildString (Num.IsPositive, Num.Numerator);
            LexTokenManager.Insert_Examiner_String (Str     => Str,
                                                    Lex_Str => StoreRep);
         when RealValue =>
            BuildString (Num.IsPositive, Num.Numerator);
            AppendDenominator (Num.Denominator);
            LexTokenManager.Insert_Examiner_String (Str     => Str,
                                                    Lex_Str => StoreRep);
      end case;
      Rep := StoreRep;
   end StorageRep;

   ----------------------------------------------------------------------------

   function ValueRep (StoreRep : LexTokenManager.Lex_String) return Value is
      Str           : E_Strings.T;
      ValIsPositive : Boolean;
      PartVal       : Part;
      Ptr           : E_Strings.Positions;
      SlashFound    : Boolean;
      Val           : Value;

      ----------------

      procedure GetSign
      --# global in     Str;
      --#           out Ptr;
      --#           out ValIsPositive;
      --# derives Ptr,
      --#         ValIsPositive from Str;
      is
      begin
         if E_Strings.Get_Element (E_Str => Str,
                                   Pos   => 1) = '-' then
            ValIsPositive := False;
            Ptr           := 2;
         else
            ValIsPositive := True;
            Ptr           := 1;
         end if;
      end GetSign;

      ---------------

      procedure GetPart (PartVal : out Part)
      --# global in     Str;
      --#        in out Ptr;
      --#           out SlashFound;
      --# derives PartVal,
      --#         Ptr,
      --#         SlashFound from Ptr,
      --#                         Str;
      is
         Len : LengthRange;
      begin
         SlashFound := False;
         PartVal    := ZeroPart;
         Len        := 0;
         loop
            if E_Strings.Get_Element (E_Str => Str,
                                      Pos   => Ptr) = '/' then
               Ptr        := Ptr + 1; --skip over '/'
               SlashFound := True;
               exit;
            end if;

            --here we are neither at the end of the string nor have we reached a /
            Len                    := Len + 1;
            PartVal.Numerals (Len) := CharToDigit (E_Strings.Get_Element (E_Str => Str,
                                                                          Pos   => Ptr));

            exit when Ptr = E_Strings.Get_Length (E_Str => Str);

            Ptr := Ptr + 1;
         end loop;
         PartVal.Length := Len;
      end GetPart;

   begin -- ValueRep
      if LexTokenManager.Lex_String_Case_Insensitive_Compare (Lex_Str1 => StoreRep,
                                                              Lex_Str2 => LexTokenManager.Null_String) =
        LexTokenManager.Str_Eq then
         Val := NoValue;
      elsif LexTokenManager.Lex_String_Case_Insensitive_Compare (Lex_Str1 => StoreRep,
                                                                 Lex_Str2 => LexTokenManager.True_Token) =
        LexTokenManager.Str_Eq then
         Val := TrueValue;
      elsif LexTokenManager.Lex_String_Case_Insensitive_Compare (Lex_Str1 => StoreRep,
                                                                 Lex_Str2 => LexTokenManager.False_Token) =
        LexTokenManager.Str_Eq then
         Val := FalseValue;
      else --some Sort of Number
         Val := ZeroInteger;  --set up all fields with suitable default Values
         Str := LexTokenManager.Lex_String_To_String (Lex_Str => StoreRep);
         GetSign;
         Val.IsPositive := ValIsPositive;
         GetPart (PartVal);
         Val.Numerator := PartVal;
         if SlashFound then
            Val.Sort := RealValue;
            --# accept F, 10, SlashFound, "SlashFound not used here" &
            --#        F, 10, Ptr, "Ptr not used here";
            GetPart (PartVal);
            --# end accept;
            Val.Denominator := PartVal;
         end if;
      end if;
      return Val;
   end ValueRep;

   ----------------------------------------------------------------------------

   function HasNoValue (Num : Value) return Boolean is
   begin
      return Num.Sort = UnknownValue;
   end HasNoValue;

   ----------------------------------------------------------------------------

   function ValueToString (Num : Value) return E_Strings.T is separate;

   --------------------------------------------------------------------------

   procedure ValueToInteger (Num : in     Value;
                             Int :    out Integer;
                             Ok  :    out ErrorCode) is
      Column, IntLocal, PosMult : Natural;
   begin
      if Num.Sort = IntegerValue then
         if GreaterPart (Num.Numerator, NaturalToPart (Integer'Last)) then
            Int := 0;
            Ok  := OverFlow;
         else
            IntLocal := 0;
            PosMult  := 1;
            Column   := 1;
            loop
               IntLocal := IntLocal + PosMult * Natural (Num.Numerator.Numerals (Column));
               exit when Column = Num.Numerator.Length;

               Column  := Column + 1;
               PosMult := PosMult * 10;
            end loop;
            Ok := NoError;
            if Num.IsPositive then
               Int := IntLocal;
            else
               Int := -IntLocal;
            end if;
         end if;
      else ------------------------its not an Integer
         Int := 0;
         Ok  := TypeMismatch;
      end if;
   end ValueToInteger;

   --------------------------------------------------------------------------

   procedure Add (FirstNum, SecondNum : in     Value;
                  Result              :    out Value;
                  Ok                  :    out ErrorCode) is
      Res : Value;
   begin
      if HasNoValue (FirstNum) or else HasNoValue (SecondNum) then
         Result := NoValue;
         Ok     := NoError;

      elsif (FirstNum.Sort = IntegerValue) and then (SecondNum.Sort = IntegerValue) then
         Res := ZeroInteger;
         NumeratorAdd (FirstNum, SecondNum, Res);
         Result := Res;
         Ok     := OverflowCheck (NoError, Res);

      elsif (FirstNum.Sort = RealValue) and then (SecondNum.Sort = RealValue) then
         RealAdd (FirstNum, SecondNum, Result, Ok);

      else
         Result := NoValue;
         Ok     := TypeMismatch;
      end if;
   end Add;

   --------------------------------------------------------------------------

   procedure Negate (Num : in out Value) is
   begin
      if Num.Sort /= UnknownValue and then Num.Numerator /= ZeroPart then
         Num.IsPositive := not Num.IsPositive;
      end if;
   end Negate;

   --------------------------------------------------------------------------

   procedure Absolute (Num : in out Value) is
   begin
      Num.IsPositive := True;
   end Absolute;

   --------------------------------------------------------------------------

   procedure ConvertToInteger (Num : in out Value) is
   begin
      Num.Sort := IntegerValue;
   end ConvertToInteger;

   ----------------------------------------------------------------------------

   procedure ConvertToReal (Num : in out Value) is
   begin
      Num.Sort := RealValue;
   end ConvertToReal;

   ----------------------------------------------------------------------------

   procedure Subtract (FirstNum, SecondNum : in     Value;
                       Result              :    out Value;
                       Ok                  :    out ErrorCode) is
      deductor : Value;
   begin
      if HasNoValue (FirstNum) or else HasNoValue (SecondNum) then
         Result := NoValue;
         Ok     := NoError;
      else
         deductor := SecondNum;
         Negate (deductor);
         Add (FirstNum, deductor, Result, Ok);
      end if;
   end Subtract;

   --------------------------------------------------------------------------

   procedure Multiply (FirstNum, SecondNum : in     Value;
                       Result              :    out Value;
                       Ok                  :    out ErrorCode) is
   begin
      if HasNoValue (FirstNum) or else HasNoValue (SecondNum) then
         Result := NoValue;
         Ok     := NoError;

      elsif (FirstNum.Sort = IntegerValue) and then (SecondNum.Sort = IntegerValue) then
         IntegerMultiply (FirstNum, SecondNum, Result, Ok);

      else
         RealMultiply (FirstNum, SecondNum, Result, Ok);
      end if;
   end Multiply;

   --------------------------------------------------------------------------

   procedure Divide (FirstNum, SecondNum : in     Value;
                     Result              :    out Value;
                     Ok                  :    out ErrorCode) is
   begin
      if HasNoValue (FirstNum) or else HasNoValue (SecondNum) then
         Result := NoValue;
         Ok     := NoError;

      elsif (FirstNum.Sort = IntegerValue) and then (SecondNum.Sort = IntegerValue) then
         if SecondNum = ZeroInteger then
            Result := NoValue;
            Ok     := DivideByZero;
         else
            Result            := ZeroInteger;
            Result.Numerator  := DivPart (FirstNum.Numerator, SecondNum.Numerator).Quotient;
            Result.IsPositive := (FirstNum.IsPositive = SecondNum.IsPositive);
            Ok                := NoError;
         end if;

      elsif (FirstNum.Sort = RealValue) then
         if SecondNum = ZeroReal then
            Result := NoValue;
            Ok     := DivideByZero;
         else
            RealDivide (FirstNum, SecondNum, Result, Ok);
         end if;
      else
         Result := NoValue;
         Ok     := TypeMismatch;
      end if;
   end Divide;

   --------------------------------------------------------------------------

   procedure Remainder (FirstNum, SecondNum : in     Value;
                        Result              :    out Value;
                        Ok                  :    out ErrorCode) is
      OkLocal     : ErrorCode;
      ResultLocal : Value;
   begin
      if HasNoValue (FirstNum) or else HasNoValue (SecondNum) then
         Result := NoValue;
         Ok     := NoError;
      else
         ModRemLegalityCheck (FirstNum, SecondNum, OkLocal);
         if OkLocal = NoError then
            ResultLocal           := ZeroInteger;
            ResultLocal.Numerator := DivPart (FirstNum.Numerator, SecondNum.Numerator).Remnant;
            if not (ResultLocal = ZeroInteger) then
               ResultLocal.IsPositive := FirstNum.IsPositive;
            end if;
            Result := ResultLocal;

         else --some Sort of error
            Result := NoValue;
         end if;
         Ok := OkLocal;
      end if;
   end Remainder;

   --------------------------------------------------------------------------

   procedure Modulus (FirstNum, SecondNum : in     Value;
                      Result              :    out Value;
                      Ok                  :    out ErrorCode) is
      OkLocal        : ErrorCode;
      ResultLocal    : Value;
      DivisionResult : Division_Result_Type;
   begin
      if HasNoValue (FirstNum) or else HasNoValue (SecondNum) then
         Result := NoValue;
         Ok     := NoError;

      elsif FirstNum.IsPositive = SecondNum.IsPositive then
         Remainder (FirstNum, SecondNum, Result, Ok);

      else       -- special handling for MOD with mixed signs
         ModRemLegalityCheck (FirstNum, SecondNum, OkLocal);

         if OkLocal = NoError then
            ResultLocal    := ZeroInteger;
            DivisionResult := DivPart (FirstNum.Numerator, SecondNum.Numerator);

            if DivisionResult.Remnant = ZeroPart then  -- modulus is zero
               Result := ZeroInteger;

            else                                  -- modulus is non zero
               ResultLocal.Numerator :=
                 SubtractPart (MultPart (SecondNum.Numerator, AddPart (DivisionResult.Quotient, OnePart)), FirstNum.Numerator);

               ResultLocal.IsPositive := SecondNum.IsPositive;
               Result                 := ResultLocal;
            end if;  -- of either the zero remainder or actual remainder case
            Ok := OkLocal;
         else -----------------------------some Sort of error
            Result := NoValue;
            Ok     := OkLocal;
         end if;
      end if;
   end Modulus;

   --------------------------------------------------------------------------

   function IsAPositivePowerOf2 (Num : in Value) return Boolean is
      NormNum       : Value;
      DR            : Division_Result_Type;
      D             : Part;
      IsAPowerOfTwo : Boolean;
   begin
      IsAPowerOfTwo := True;

      if Num.Sort = IntegerValue and then Num.IsPositive then

         NormNum := Num;
         Normalize (NormNum);

         D := NormNum.Numerator;

         if D /= ZeroPart then

            -- A positive power of 2 has a single "1" digit in binary,
            -- so if we shift right (i.e. divide by 2) repeatedly, we should
            -- never get a remainder until the current value is 1.
            while D /= ZeroPart loop
               DR := DivPart (D, TwoPart);

               if D /= OnePart and DR.Remnant /= ZeroPart then
                  -- We have a non-zero remainder, and D is not 1, so
                  -- the original number could not have been a power of 2.
                  IsAPowerOfTwo := False;
                  exit;
               end if;

               D := DR.Quotient;
            end loop;
         else
            IsAPowerOfTwo := False;
         end if;
      else
         IsAPowerOfTwo := False;
      end if;

      return IsAPowerOfTwo;
   end IsAPositivePowerOf2;

   --------------------------------------------------------------------------

   function BoolToValue (B : Boolean) return Value is
      Result : Value;
   begin
      if B then
         Result := TrueValue;
      else
         Result := FalseValue;
      end if;
      return Result;
   end BoolToValue;

   ----------------------------------------------------------------------------

   procedure Greater (FirstNum, SecondNum : in     Value;
                      Result              :    out Value;
                      Ok                  :    out ErrorCode) is
      BoolResult : Boolean;
      OkLocal    : ErrorCode;
   begin
      if HasNoValue (FirstNum) or else HasNoValue (SecondNum) then
         Result  := NoValue;
         OkLocal := NoError;
      else
         GreaterLocal (FirstNum, SecondNum, BoolResult, OkLocal);
         if OkLocal = NoError then
            Result := BoolToValue (BoolResult);
         else
            Result := NoValue;
         end if;
      end if;
      Ok := OkLocal;
   end Greater;

   --------------------------------------------------------------------------

   procedure Lesser (FirstNum, SecondNum : in     Value;
                     Result              :    out Value;
                     Ok                  :    out ErrorCode) is
      BoolResult : Boolean;
      OkLocal    : ErrorCode;
   begin
      if HasNoValue (FirstNum) or else HasNoValue (SecondNum) then
         Result  := NoValue;
         OkLocal := NoError;
      else
         GreaterLocal (SecondNum, FirstNum, BoolResult, OkLocal);
         if OkLocal = NoError then
            Result := BoolToValue (BoolResult);
         else
            Result := NoValue;
         end if;
      end if;
      Ok := OkLocal;
   end Lesser;

   ----------------------------------------------------------------------------

   procedure FloorCeilInternal
     (Val     : in     Value;
      DoFloor :        Boolean;
      Result  :    out Value;
      OK      :    out ErrorCode)
   --# derives OK,
   --#         Result from DoFloor,
   --#                     Val;
   is
      Num          : Value;
      Denom        : Value;
      Temp_Swap    : Part;
      Mod_Val      : Value;
      New_Num      : Value;
      Error        : ErrorCode;
      Ceil_Temp    : Value;
      Final_Result : Value;
   begin
      -- floor (Num / Denom) = (Num - Num mod Denom) / Denom
      -- if_zero (val, result) = if val = 0 then (result) else (0);
      -- ceiling (Num / Denom) = (Nun - Num mod Denom + if_zero (Num mod Denom, Denom)) /
      --                                                                             Denom

      if Val.Sort = IntegerValue then
         Result := Val;
         OK     := NoError;
      elsif Val.Sort = RealValue then
         Num             := Val;
         Num.Denominator := OnePart;
         Num.Sort        := IntegerValue;
         Normalize (Num);

         Denom             := Val;
         Temp_Swap         := Denom.Denominator;
         Denom.Denominator := OnePart;
         Denom.Numerator   := Temp_Swap;
         Denom.Sort        := IntegerValue;
         Denom.IsPositive  := True;
         Normalize (Denom);

         Modulus (Num, Denom, Mod_Val, Error);

         if not DoFloor then -- doing a ceiling operation, so check if addition req'd
            Greater (Mod_Val, ZeroInteger, Ceil_Temp, Error);
            if Ceil_Temp = TrueValue then
               Add (Num, Denom, Ceil_Temp, Error);
               Num := Ceil_Temp;
            end if;
         end if;

         if Error = NoError then
            Subtract (Num, Mod_Val, New_Num, Error);
            if Error = NoError then
               Normalize (New_Num);
               Divide (New_Num, Denom, Final_Result, Error);
               if Error /= NoError then
                  Result := NoValue;
                  OK     := Error;
               else
                  Final_Result.Sort := RealValue;
                  Normalize (Final_Result);
                  Result := Final_Result;
                  OK     := NoError;
               end if;
            else
               Result := NoValue;
               OK     := Error;
            end if;
         else
            Result := NoValue;
            OK     := NoError;
         end if;

      elsif HasNoValue (Val) then
         OK     := NoError;
         Result := NoValue;
      else
         OK     := IllegalValue;
         Result := NoValue;
      end if;

   end FloorCeilInternal;

   ----------------------------------------------------------------------------

   procedure Floor (Val    : in     Value;
                    Result :    out Value;
                    OK     :    out ErrorCode) is
   begin
      FloorCeilInternal (Val, True, Result, OK);
   end Floor;

   ----------------------------------------------------------------------------

   procedure Ceiling (Val    : in     Value;
                      Result :    out Value;
                      OK     :    out ErrorCode) is
   begin
      FloorCeilInternal (Val, False, Result, OK);
   end Ceiling;

   --------------------------------------------------------------------------

   procedure LesserOrEqual (FirstNum, SecondNum : in     Value;
                            Result              :    out Value;
                            Ok                  :    out ErrorCode) is
      Res : Value;
   begin
      if HasNoValue (FirstNum) or else HasNoValue (SecondNum) then
         Result := NoValue;
         Ok     := NoError;
      else
         Lesser (FirstNum, SecondNum, Res, Ok);
         if Res.Sort = TruthValue then
            Result := BoolToValue ((Res = TrueValue) or (FirstNum = SecondNum));
         else
            Result := NoValue;
         end if;
      end if;
   end LesserOrEqual;

   --------------------------------------------------------------------------

   procedure GreaterOrEqual (FirstNum, SecondNum : in     Value;
                             Result              :    out Value;
                             Ok                  :    out ErrorCode) is
      Res     : Boolean;
      OkLocal : ErrorCode;
   begin
      if HasNoValue (FirstNum) or else HasNoValue (SecondNum) then
         Result  := NoValue;
         OkLocal := NoError;
      else
         GreaterLocal (FirstNum, SecondNum, Res, OkLocal);
         if OkLocal = NoError then
            Result := BoolToValue (Res or (FirstNum = SecondNum));
         else
            Result := NoValue;
         end if;
      end if;
      Ok := OkLocal;
   end GreaterOrEqual;

   --------------------------------------------------------------------------

   procedure RaiseByPower (FirstNum, SecondNum : in     Value;
                           Result              :    out Value;
                           Ok                  :    out ErrorCode) is
      Swap : Part;
      N    : Part;
      Q    : Division_Result_Type;
      Y    : Value;
      Z    : Value;
      Temp : Value;
      Err  : ErrorCode;
   begin
      if HasNoValue (FirstNum) or else HasNoValue (SecondNum) then
         Result := NoValue;
         Ok     := NoError;

      elsif (SecondNum.Sort = RealValue) then
         Result := NoValue;
         Ok     := IllegalOperation;

         --608--new elsif to catch INT ** NEGATIVE
      elsif ((FirstNum.Sort = IntegerValue) and (not SecondNum.IsPositive)) then
         Result := NoValue;
         Ok     := ConstraintError;

         --822--new elsif to catch 0.0 ** negative
      elsif ((FirstNum = ZeroReal) and then (not SecondNum.IsPositive)) then
         Result := NoValue;
         Ok     := ConstraintError;

      elsif SecondNum = ZeroInteger then         -- we must return 1
         if FirstNum.Sort = IntegerValue then
            Result := ZeroInteger;
         else
            Result := ZeroReal;
         end if;
         Result.Numerator := OnePart;
         Ok               := NoError;
      else -- we have legal and meaningful operation

         -- Bit-wise algorithm.  See Knuth Volume 2, section 4.6.3.
         N   := SecondNum.Numerator;
         Y   := OneInteger;
         Z   := FirstNum;
         Err := NoError;

         loop
            Q := DivPart (N, TwoPart);
            if Q.Remnant = OnePart then
               -- N is odd, so
               -- Y := Y * Z;
               Multiply (Y, Z, Temp, Err);
               Y := Temp;
            end if;
            -- N := Floor(N/2);
            N := Q.Quotient;

            exit when N = ZeroPart;

            -- Z := Z * Z;
            Multiply (Z, Z, Temp, Err);
            Z := Temp;
         end loop;

         -- If exponent was negative then form the
         -- reciprocal of Y
         if not SecondNum.IsPositive then   --reciprocate
            Swap          := Y.Numerator;
            Y.Numerator   := Y.Denominator;
            Y.Denominator := Swap;
            Normalize (Y);
         end if;
         Result := Y;
         Ok     := Err;
      end if;
   end RaiseByPower;

   ----------------------------------------------------------------------------
   -- Support of non-Numeric types
   ----------------------------------------------------------------------------

   procedure ValueToBool (TheVal : in     Value;
                          Result :    out Boolean;
                          Ok     :    out ErrorCode) is
   begin
      if TheVal.Sort = TruthValue then
         Ok     := NoError;
         Result := TheVal.IsPositive;
      else
         Result := False;
         Ok     := TypeMismatch;
      end if;
   end ValueToBool;

   ----------------------------------------------------------------------------

   function AndOp (LeftVal, RightVal : Value) return Value is
      Result : Value;
   begin
      if LeftVal.Sort = TruthValue and RightVal.Sort = TruthValue then
         -- Boolean "and"
         Result            := FalseValue;
         Result.IsPositive := LeftVal.IsPositive and RightVal.IsPositive;

      elsif LeftVal.Sort = IntegerValue and RightVal.Sort = IntegerValue then
         -- Must be a modular (bitwise) "and" operator
         Result :=
           Value'
           (Numerator   => BitsToPart (PartToBits (LeftVal.Numerator) and PartToBits (RightVal.Numerator)),
            Denominator => OnePart,
            IsPositive  => True,
            Sort        => IntegerValue);

      else
         Result := NoValue;
      end if;

      return Result;

   end AndOp;

   ----------------------------------------------------------------------------

   function OrOp (LeftVal, RightVal : Value) return Value is
      Result : Value;
   begin
      if LeftVal.Sort = TruthValue and RightVal.Sort = TruthValue then
         -- Boolean "or"
         Result            := FalseValue;
         Result.IsPositive := LeftVal.IsPositive or RightVal.IsPositive;

      elsif LeftVal.Sort = IntegerValue and RightVal.Sort = IntegerValue then
         -- Must be a modular (bitwise) "or" operator
         Result :=
           Value'
           (Numerator   => BitsToPart (PartToBits (LeftVal.Numerator) or PartToBits (RightVal.Numerator)),
            Denominator => OnePart,
            IsPositive  => True,
            Sort        => IntegerValue);

      else
         Result := NoValue;
      end if;

      return Result;

   end OrOp;

   ----------------------------------------------------------------------------
   function XorOp (LeftVal, RightVal : Value) return Value is
      Result : Value;
   begin
      if LeftVal.Sort = TruthValue and RightVal.Sort = TruthValue then
         -- Boolean "xor"
         Result            := FalseValue;
         Result.IsPositive := LeftVal.IsPositive xor RightVal.IsPositive;

      elsif LeftVal.Sort = IntegerValue and RightVal.Sort = IntegerValue then
         -- Must be a modular (bitwise) "xor" operator
         Result :=
           Value'
           (Numerator   => BitsToPart (PartToBits (LeftVal.Numerator) xor PartToBits (RightVal.Numerator)),
            Denominator => OnePart,
            IsPositive  => True,
            Sort        => IntegerValue);
      else
         Result := NoValue;
      end if;

      return Result;
   end XorOp;

   ----------------------------------------------------------------------------

   procedure NotOp (TheVal : in out Value) is
   begin
      if not HasNoValue (TheVal) then
         TheVal.IsPositive := not TheVal.IsPositive;
      end if;
   end NotOp;

   ----------------------------------------------------------------------------

   -- nb this implementation ONLY WORKS iff TheModulus is a positive power of 2!
   procedure ModularNotOp (TheVal     : in out Value;
                           TheModulus : in     Value) is
      TypeLast, NumeratorPart : Part;
   begin
      -- for type T is 2**N, then the LRM 4.5.6(5) says that
      -- not X == (T'Last - X) == ((T'Modulus - 1) - X), so...

      TypeLast      := SubtractPart (TheModulus.Numerator, OnePart);
      NumeratorPart := SubtractPart (TypeLast, TheVal.Numerator);
      TheVal        := Value'(Numerator   => NumeratorPart,
                              Denominator => OnePart,
                              IsPositive  => True,
                              Sort        => IntegerValue);
   end ModularNotOp;

   ----------------------------------------------------------------------------

   procedure InsideRange (Val, LowerBound, UpperBound : in     Value;
                          Result                      :    out Value;
                          Ok                          :    out ErrorCode) is
      Result1, Result2 : Value;
      Tmp_Ok1, Tmp_Ok2 : ErrorCode;
   begin
      --# accept F, 10, Tmp_Ok1, "Tmp_Ok1 not used here" &
      --#        F, 33, Tmp_Ok1, "Tmp_Ok1 not used here" &
      --#        F, 10, Tmp_Ok2, "Tmp_Ok2 not used here" &
      --#        F, 33, Tmp_Ok2, "Tmp_Ok2 not used here";
      if Val.Sort = LowerBound.Sort and then LowerBound.Sort = UpperBound.Sort then
         GreaterOrEqual (Val, LowerBound, Result1, Tmp_Ok1);
         LesserOrEqual (Val, UpperBound, Result2, Tmp_Ok2);
         if Result1.Sort = UnknownValue or else Result2.Sort = UnknownValue then
            Result := NoValue;
         else
            Result := AndOp (Result1, Result2);
         end if;
         Ok := NoError;
      else
         Result := NoValue;
         Ok     := TypeMismatch;
      end if;
   end InsideRange;

   ----------------------------------------------------------------------------

   procedure OutsideRange (Val, LowerBound, UpperBound : in     Value;
                           Result                      :    out Value;
                           Ok                          :    out ErrorCode) is
      Result1, Result2 : Value;
      Tmp_Ok1, Tmp_Ok2 : ErrorCode;
   begin
      --# accept F, 10, Tmp_Ok1, "Tmp_Ok1 not used here" &
      --#        F, 33, Tmp_Ok1, "Tmp_Ok1 not used here" &
      --#        F, 10, Tmp_Ok2, "Tmp_Ok2 not used here" &
      --#        F, 33, Tmp_Ok2, "Tmp_Ok2 not used here";
      if Val.Sort = LowerBound.Sort and then LowerBound.Sort = UpperBound.Sort then
         Greater (Val, -- CFR 430 Flow error here: internal anomaly to be fixed
                  UpperBound, Result1, Tmp_Ok1);
         Lesser (Val, LowerBound, Result2, Tmp_Ok2);
         if Result1.Sort = UnknownValue or else Result2.Sort = UnknownValue then
            Result := NoValue;
         else
            Result := OrOp (Result1, Result2);
         end if;
         Ok := NoError;
      else
         Result := NoValue;
         Ok     := TypeMismatch;
      end if;
   end OutsideRange;

   ----------------------------------------------------------------------------
   --attribute ops
   ----------------------------------------------------------------------------

   procedure PredOp (TheVal : in out Value;
                     Ok     :    out ErrorCode) is
      DedVal : Value;
   begin
      if HasNoValue (TheVal) then
         Ok := NoError;
      elsif TheVal.Sort = RealValue then
         Ok     := TypeMismatch;
         TheVal := NoValue;
      else
         Subtract (TheVal, OneInteger,
                   -- to get
                   DedVal, Ok);
         TheVal := DedVal;
      end if;
   end PredOp;

   ----------------------------------------------------------------------------

   procedure SuccOp (TheVal : in out Value;
                     Ok     :    out ErrorCode) is
      AddVal : Value;
   begin
      if HasNoValue (TheVal) then
         Ok := NoError;
      elsif TheVal.Sort = RealValue then
         Ok     := TypeMismatch;
         TheVal := NoValue;
      else
         Add (TheVal, OneInteger,
              -- to get
              AddVal, Ok);
         TheVal := AddVal;
      end if;
   end SuccOp;

   ----------------------------------------------------------------------------

   function MakeEnum (Pos : Natural) return Value is
      Result : Value;
   begin
      Result           := ZeroInteger;
      Result.Numerator := NaturalToPart (Pos);
      return Result;
   end MakeEnum;

   ----------------------------------------------------------------------------

   function IsIntegerValue (Val : Value) return Boolean is
   begin
      return Val.Sort = IntegerValue;
   end IsIntegerValue;

   ------------------------------------

   function IsRealValue (Val : Value) return Boolean is
   begin
      return Val.Sort = RealValue;
   end IsRealValue;

   ----------------------------------------------------------------------------

   function Ada95RealToInteger (TheReal : Value) return Value is
      Temp        : Value;
      Result      : Value;
      TheRem      : Value;
      RoundResult : Value;
      Unused      : ErrorCode;
      DivRes      : Division_Result_Type;
   begin
      --# accept F, 10, Unused, "Unused unused here" &
      --#        F, 33, Unused, "Unused unused here";
      if HasNoValue (TheReal) then
         Result := NoValue;
      else
         --get Quotient and remainder
         DivRes := DivPart (TheReal.Numerator, TheReal.Denominator);

         --create Integer truncated Part from Quotient
         Result := Value'(Numerator   => DivRes.Quotient,
                          Denominator => OnePart,
                          IsPositive  => True,
                          Sort        => IntegerValue);

         --create fractional remainder Part
         TheRem := Value'(Numerator   => DivRes.Remnant,
                          Denominator => TheReal.Denominator,
                          IsPositive  => True,
                          Sort        => RealValue);

         --see if remainder >= 0.5
         GreaterOrEqual (TheRem, ExactHalf,
                         --to get
                         RoundResult, Unused);

         if RoundResult = TrueValue then
            Temp := Result;  --needed because of aliasing in next call
            Add (Temp, OneInteger,
                 --to get
                 Result, Unused);
         end if;

         if Result /= ZeroInteger then
            Result.IsPositive := TheReal.IsPositive; --restore sign
         end if;
      end if;

      return Result;

   end Ada95RealToInteger;

   ----------------------------------------------------------------------------
   --                        Initialisation
   --------------------------------------------------------------------------

   --none

end Maths;