--Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd.
--All rights reserved.
-- Copyright (C) 2007-2010, Gabriel Dos Reis.
-- All rights reserved.
--
--Redistribution and use in source and binary forms, with or without
--modification, are permitted provided that the following conditions are
--met:
--
--    - Redistributions of source code must retain the above copyright
--      notice, this list of conditions and the following disclaimer.
--
--    - Redistributions in binary form must reproduce the above copyright
--      notice, this list of conditions and the following disclaimer in
--      the documentation and/or other materials provided with the
--      distribution.
--
--    - Neither the name of The Numerical ALgorithms Group Ltd. nor the
--      names of its contributors may be used to endorse or promote products
--      derived from this software without specific prior written permission.
--
--THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
--IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
--TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
--PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
--OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
--EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
--PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
--PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
--LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
--NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
--SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

)abbrev category INS IntegerNumberSystem
++ Author: Stephen M. Watt
++ Date Created:
++   January 1988
++ Change History:
++ Basic Operations:
++   addmod, base, bit?, copy, dec, even?, hash, inc, invmod, length, mask,
++   positiveRemainder, symmetricRemainder, multiplicativeValuation, mulmod,
++   odd?, powmod, random, rational, rational?, rationalIfCan, shift, submod
++ Description:  An \spad{IntegerNumberSystem} is a model for the integers.
IntegerNumberSystem(): Category ==
  Join(UniqueFactorizationDomain, EuclideanDomain, OrderedIntegralDomain,
         DifferentialRing, ConvertibleTo Integer, RetractableTo Integer,
           LinearlyExplicitRingOver Integer, ConvertibleTo InputForm,
             ConvertibleTo Pattern Integer, PatternMatchable Integer,
               CombinatorialFunctionCategory, RealConstant,
                 CharacteristicZero, StepThrough) with
   odd?     : % -> Boolean
      ++ odd?(n) returns true if and only if n is odd.
   even?    : % -> Boolean
      ++ even?(n) returns true if and only if n is even.
   multiplicativeValuation
      ++ euclideanSize(a*b) returns \spad{euclideanSize(a)*euclideanSize(b)}.
   base     : () -> %
      ++ base() returns the base for the operations of \spad{IntegerNumberSystem}.
   length   : % -> %
      ++ length(a) length of \spad{a} in digits.
   shift    : (%, %) -> %
      ++ shift(a,i) shift \spad{a} by i digits.
   bit?     : (%, %) -> Boolean
      ++ bit?(n,i) returns true if and only if i-th bit of n is a 1.
   positiveRemainder     : (%, %) -> %
      ++ positiveRemainder(a,b) (where \spad{b > 1}) yields r
      ++ where \spad{0 <= r < b} and \spad{r == a rem b}.
   symmetricRemainder     : (%, %) -> %
      ++ symmetricRemainder(a,b) (where \spad{b > 1}) yields r
      ++ where \spad{ -b/2 <= r < b/2 }.
   rational?: % -> Boolean
      ++ rational?(n) tests if n is a rational number
      ++ (see \spadtype{Fraction Integer}).
   rational : % -> Fraction Integer
      ++ rational(n) creates a rational number (see \spadtype{Fraction Integer})..
   rationalIfCan: % -> Union(Fraction Integer, "failed")
      ++ rationalIfCan(n) creates a rational number, or returns "failed" if this is not possible.
   random   : () -> %
      ++ random() creates a random element.
   random   : % -> %
      ++ random(a) creates a random element from 0 to \spad{a-1}.
   copy     : % -> %
      ++ copy(n) gives a copy of n.
   inc      : % -> %
      ++ inc(x) returns \spad{x + 1}.
   dec      : % -> %
      ++ dec(x) returns \spad{x - 1}.
   mask     : % -> %
      ++ mask(n) returns \spad{2**n-1} (an n bit mask).
   addmod   : (%,%,%) -> %
      ++ addmod(a,b,p), \spad{0<=a,b<p>1}, means \spad{a+b mod p}.
   submod   : (%,%,%) -> %
      ++ submod(a,b,p), \spad{0<=a,b<p>1}, means \spad{a-b mod p}.
   mulmod   : (%,%,%) -> %
      ++ mulmod(a,b,p), \spad{0<=a,b<p>1}, means \spad{a*b mod p}.
   powmod   : (%,%,%) -> %
      ++ powmod(a,b,p), \spad{0<=a,b<p>1}, means \spad{a**b mod p}.
   invmod   : (%,%) -> %
      ++ invmod(a,b), \spad{0<=a<b>1}, \spad{(a,b)=1} means \spad{1/a mod b}.
   canonicalUnitNormal
--   commutative("*")    -- follows from the above

 add
   characteristic == 0
   differentiate x          == 0
   even? x                  == not odd? x
   copy x                   == x
   bit?(x, i)               == odd? shift(x, -i)
   mask n                   == dec shift(1, n)
   rational? x              == true
   euclideanSize(x)         ==
        x=0 => error "euclideanSize called on zero"
        negative? x => (-convert(x)@Integer)::NonNegativeInteger
        convert(x)@Integer::NonNegativeInteger
   convert(x:%):Float       == (convert(x)@Integer)::Float
   convert(x:%):DoubleFloat  == (convert(x)@Integer)::DoubleFloat
   convert(x:%):InputForm   == convert(convert(x)@Integer)
   retract(x:%):Integer     == convert(x)@Integer
   convert(x:%):Pattern(Integer)== convert(x)@Integer ::Pattern(Integer)
   factor x          == factor(x)$IntegerFactorizationPackage(%)
   squareFree x      == squareFree(x)$IntegerFactorizationPackage(%)
   prime? x          == prime?(x)$IntegerPrimesPackage(%)
   factorial x       == factorial(x)$IntegerCombinatoricFunctions(%)
   binomial(n, m)    == binomial(n, m)$IntegerCombinatoricFunctions(%)
   permutation(n, m) == permutation(n,m)$IntegerCombinatoricFunctions(%)
   retractIfCan(x:%):Union(Integer, "failed") == convert(x)@Integer

   init() == 0

   -- iterates in order 0,1,-1,2,-2,3,-3,...
   nextItem n ==
     zero? n => just 1
     positive? n => just(-n)
     just(1-n)

   patternMatch(x, p, l) ==
     patternMatch(x, p, l)$PatternMatchIntegerNumberSystem(%)

   rational(x:%):Fraction(Integer) ==
     (convert(x)@Integer)::Fraction(Integer)

   rationalIfCan(x:%):Union(Fraction Integer, "failed") ==
     (convert(x)@Integer)::Fraction(Integer)

   symmetricRemainder(x, n) ==
      r := x rem n
      r = 0 => r
      if negative? n then n:=-n
      positive? r =>
         2 * r > n => r - n
         r
      2*r + n <= 0 => r + n
      r

   invmod(a, b) ==
      if negative? a then a := positiveRemainder(a, b)
      c := a; c1:% := 1
      d := b; d1:% := 0
      while not zero? d repeat
         q := c quo d
         r := c-q*d
         r1 := c1-q*d1
         c := d; c1 := d1
         d := r; d1 := r1
      not one? c => error "inverse does not exist"
      negative? c1 => c1 + b
      c1

   powmod(x, n, p) ==
      if negative? x then x := positiveRemainder(x, p)
      zero? x => 0
      zero? n => 1
      y:% := 1
      z := x
      repeat
         if odd? n then y := mulmod(y, z, p)
         zero?(n := shift(n, -1)) => return y
         z := mulmod(z, z, p)

)abbrev domain SINT SingleInteger

++ Author:  Michael Monagan
++ Date Created:
++    January 1988
++ Change History:
++ Basic Operations: max, min,
++    not, and, or, xor, Not, And, Or
++ Related Constructors:
++ Keywords: single integer
++ Description: SingleInteger is intended to support machine integer
++ arithmetic.

-- MAXINT, BASE (machine integer constants)
-- MODULUS, MULTIPLIER (random number generator constants)


SingleInteger(): Join(IntegerNumberSystem,OrderedFinite,BooleanLogic) with
   canonical
      ++ \spad{canonical} means that mathematical equality is implied by data structure equality.
   canonicalsClosed
      ++ \spad{canonicalClosed} means two positives multiply to give positive.
   noetherian
      ++ \spad{noetherian} all ideals are finitely generated (in fact principal).

   -- bit operations
   xor: (%, %) -> %
      ++ xor(n,m)  returns the bit-by-bit logical {\em xor} of
      ++ the single integers n and m.
 == SubDomain(Integer, %ismall?(#1)$Foreign(Builtin)) add

   import %icst0: %                 from Foreign Builtin
   import %icst1: %                 from Foreign Builtin
   import %icstmin: %               from Foreign Builtin
   import %icstmax: %               from Foreign Builtin
   import %iadd: (%,%) -> %         from Foreign Builtin
   import %iaddmod: (%,%,%) -> %    from Foreign Builtin
   import %isub: (%,%) -> %         from Foreign Builtin
   import %isubmod: (%,%,%) -> %    from Foreign Builtin
   import %imul: (%,%) -> %         from Foreign Builtin
   import %imulmod: (%,%,%) -> %    from Foreign Builtin
   import %irem: (%,%) -> %         from Foreign Builtin
   import %iquo: (%,%) -> %         from Foreign Builtin
   import %ilshift: (%,%) -> %      from Foreign Builtin
   import %ineg: % -> %             from Foreign Builtin
   import %iinc: % -> %             from Foreign Builtin
   import %idec: % -> %             from Foreign Builtin
   import %iabs: % -> %             from Foreign Builtin
   import %irandom: % -> %          from Foreign Builtin
   import %imax: (%,%) -> %         from Foreign Builtin
   import %imin: (%,%) -> %         from Foreign Builtin
   import %igcd: (%,%) -> %         from Foreign Builtin
   import %hash: % -> SingleInteger from Foreign Builtin
   import %ilength: % -> %          from Foreign Builtin
   import %iodd?: % -> Boolean      from Foreign Builtin
   import %ieven?: % -> Boolean      from Foreign Builtin
   import %ieq: (%,%) -> Boolean    from Foreign Builtin
   import %ilt: (%,%) -> Boolean    from Foreign Builtin
   import %ile: (%,%) -> Boolean    from Foreign Builtin
   import %igt: (%,%) -> Boolean    from Foreign Builtin
   import %ige: (%,%) -> Boolean    from Foreign Builtin
   import %bitnot: % -> %           from Foreign Builtin
   import %bitand: (%,%) -> %       from Foreign Builtin
   import %bitior: (%,%) -> %       from Foreign Builtin
   import %bitxor: (%,%) -> %       from Foreign Builtin

   reducedSystem(m: Matrix %) == m pretend Matrix(Integer)
   coerce(x):OutputForm == rep(x)::OutputForm
   convert(x:%):Integer == rep x
   i:Integer * y:%      == %imul(i::%,y)
   0         == %icst0
   1         == %icst1
   base()    == per 2
   max()     == %icstmax
   min()     == %icstmin
   x = y     == %ieq(x,y)
   ~ x       == %bitnot x
   not(x)    == %bitnot x
   x /\ y    == %bitand(x,y)
   x \/ y    == %bitior(x,y)
   x and y   == %bitand(x,y)
   x or y    == %bitior(x,y)
   xor(x,y)  == %bitxor(x,y)
   x < y     == %ilt(x,y)
   x > y     == %igt(x,y)
   x <= y    == %ile(x,y)
   x >= y    == %ige(x,y)
   inc x     == %iinc x
   dec x     == %idec x
   - x       == %ineg x
   x + y     == %iadd(x,y)
   x:% - y:% == %isub(x,y)
   x:% * y:% == %imul(x,y)
   x:% ** n:NonNegativeInteger == 
      (%ipow(x, n)$Foreign(Builtin) pretend Integer)::%
   x quo y   == %iquo(x,y)
   x rem y   == %irem(x,y)
   divide(x, y)   == %idivide(x,y)$Foreign(Builtin)
   gcd(x,y)  == %igcd(x,y)
   abs(x)    == %iabs x
   odd?(x)   == %iodd? x
   even?(x)   == %ieven? x
   zero?(x)  == %ieq(x,%icst0)
   one?(x)   == %ieq(x,%icst1)
   max(x,y)  == %imax(x,y)
   min(x,y)  == %imin(x,y)
   hash(x)   == %hash x
   length(x) == %ilength x
   shift(x,n)    == %ilshift(x,n)
   mulmod(a,b,p) == %imulmod(a,b,p)
   addmod(a,b,p) == %iaddmod(a,b,p)
   submod(a,b,p) == %isubmod(a,b,p)
   negative?(x)  == %ilt(x,%icst0)
   size() ==
     (%icstmax - %icstmin + %icst1)  pretend NonNegativeInteger
   index i == per(i + rep %icstmin - rep %icst1)
   lookup x ==
     (rep x - rep %icstmin + rep %icst1) pretend PositiveInteger


   reducedSystem(m: Matrix %, v: Vector %) ==
        [m pretend Matrix(Integer), v pretend Vector(Integer)]

   positiveRemainder(x,n) ==
      r := %irem(x,n)
      negative? r =>
        negative? n => x - n 
        r + n
      r

   coerce(x:Integer):% == per x
   random() == random %icstmax
   random(n) == %irandom n

   UCA ==> Record(unit:%,canonical:%,associate:%)
   unitNormal x ==
      negative? x => [-%icst1,-x,-%icst1]$UCA
      [%icst1,x,%icst1]$UCA
   positive? x == %icst0 < x

