svDivide: Always use Euclidean division for unbounded integers (#802)

* Factor out {div,mod}Eucl into top-level definitions

Towards #799.

* svDivide: Always use Euclidean division for unbounded integers

Fixes #799.

Author: RyanGlScott

Data/SBV/Core/Operations.hs

@@ -75,7 +75,7 @@ import Data.SBV.Core.SizedFloats
 
 import Data.Ratio
 
-import Data.SBV.Utils.Numeric (RoundingMode(..), {-fp2fp,-} fpIsEqualObjectH, fpIsNormalizedH, fpMaxH, fpMinH, fpRemH, fpRoundToIntegralH, floatToWord, doubleToWord, wordToFloat, wordToDouble)
+import Data.SBV.Utils.Numeric (RoundingMode(..), divEucl, modEucl, {-fp2fp,-} fpIsEqualObjectH, fpIsNormalizedH, fpMaxH, fpMinH, fpRemH, fpRoundToIntegralH, floatToWord, doubleToWord, wordToFloat, wordToDouble)
 
 import LibBF
 
@@ -238,11 +238,15 @@ svSignum a
         z = SVal k $ Left $ mkConstCV k (0 :: Integer)
         i = SVal k $ Left $ mkConstCV k (1 :: Integer)
 
--- | Division.
+-- | Division. For integers, this behaves like 'svQuot', except that this
+-- ensures @'svQuot' a 0 = a@.
 svDivide :: SVal -> SVal -> SVal
-svDivide = liftSym2 (mkSymOp Quot) [rationalCheck] (/) idiv (/) (/) (/) (/)
-   where idiv x 0 = x
-         idiv x y = x `quot` y
+svDivide x y = liftSym2 (mkSymOp Quot) [rationalCheck] (/) idiv (/) (/) (/) (/) x y
+   where isInteger = kindOf x == KUnbounded
+
+         idiv a 0 = a
+         idiv a b | isInteger = a `divEucl` b
+                  | True      = a `quot` b
 
 -- | Divides predicate
 svDivides :: Integer -> SVal -> SVal
@@ -333,7 +337,7 @@ svQuot x y
   where
     isInteger = kindOf x == KUnbounded
 
-    quot' a b | isInteger = div a (abs b) * signum b
+    quot' a b | isInteger = divEucl a b
               | True      = quot a b
 
 -- | Remainder: Overloaded operation whose meaning depends on the kind at which
@@ -360,7 +364,7 @@ svRem x y
   where
     isInteger = kindOf x == KUnbounded
 
-    rem' a b | isInteger = mod a (abs b)
+    rem' a b | isInteger = modEucl a b
              | True      = rem a b
 
 -- | Combination of 'svQuot' and 'svRem'

Data/SBV/Utils/Numeric.hs

@@ -17,6 +17,7 @@
 module Data.SBV.Utils.Numeric (
            fpMaxH, fpMinH, fp2fp, fpRemH, fpRoundToIntegralH, fpIsEqualObjectH, fpCompareObjectH, fpIsNormalizedH
          , roundAway
+         , divEucl, modEucl
          , floatToWord, wordToFloat, doubleToWord, wordToDouble
          , RoundingMode(..), smtRoundingMode
          ) where
@@ -142,6 +143,17 @@ roundAway x = case properFraction x of
                            else
                              n + 1
 
+-- | Euclidean division. @'divEucl' a b@ returns the integer @q@ satisfying the
+-- equations @a = (b * q) + r@ and @0 <= r < abs b@, where @'modEucl' a b = r@.
+divEucl :: Integral a => a -> a -> a
+divEucl a b = div a (abs b) * signum b
+
+-- | Euclidean modular division. @'modEucl' a b@ returns the integer @r@
+-- satisfying the equations @a = (b * q) + r@ and @0 <= r < abs b@, where
+-- @'divEucl' a b = q@.
+modEucl :: Integral a => a -> a -> a
+modEucl a b = mod a (abs b)
+
 -------------------------------------------------------------------------
 -- Reinterpreting float/double as word32/64 and back. Here, we use the
 -- definitions from the reinterpret-cast package: