{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Data.Delta
-- Copyright   :  (c) Masahiro Sakai 2011-2013
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Augmenting number types with infinitesimal parameter δ.
--
-- Reference:
--
-- * Bruno Dutertre and Leonardo de Moura,
--   \"/A Fast Linear-Arithmetic Solver for DPLL(T)/\",
--   Computer Aided Verification In Computer Aided Verification, Vol. 4144
--   (2006), pp. 81-94.
--   <https://doi.org/10.1007/11817963_11>
--   <http://yices.csl.sri.com/cav06.pdf>
--
-----------------------------------------------------------------------------

module ToySolver.Data.Delta
  (
  -- * The Delta type
    Delta (..)

  -- * Construction
  , fromReal
  , delta

  -- * Query
  , realPart
  , deltaPart

  -- * Relationship with integers
  , floor'
  , ceiling'
  , isInteger'
  ) where

import Data.VectorSpace
import ToySolver.Internal.Util (isInteger)

-- | @Delta r k@ represents r + kδ for symbolic infinitesimal parameter δ.
data Delta r = Delta !r !r deriving (Eq (Delta r)
Eq (Delta r)
-> (Delta r -> Delta r -> Ordering)
-> (Delta r -> Delta r -> Bool)
-> (Delta r -> Delta r -> Bool)
-> (Delta r -> Delta r -> Bool)
-> (Delta r -> Delta r -> Bool)
-> (Delta r -> Delta r -> Delta r)
-> (Delta r -> Delta r -> Delta r)
-> Ord (Delta r)
Delta r -> Delta r -> Bool
Delta r -> Delta r -> Ordering
Delta r -> Delta r -> Delta r
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall r. Ord r => Eq (Delta r)
forall r. Ord r => Delta r -> Delta r -> Bool
forall r. Ord r => Delta r -> Delta r -> Ordering
forall r. Ord r => Delta r -> Delta r -> Delta r
min :: Delta r -> Delta r -> Delta r
$cmin :: forall r. Ord r => Delta r -> Delta r -> Delta r
max :: Delta r -> Delta r -> Delta r
$cmax :: forall r. Ord r => Delta r -> Delta r -> Delta r
>= :: Delta r -> Delta r -> Bool
$c>= :: forall r. Ord r => Delta r -> Delta r -> Bool
> :: Delta r -> Delta r -> Bool
$c> :: forall r. Ord r => Delta r -> Delta r -> Bool
<= :: Delta r -> Delta r -> Bool
$c<= :: forall r. Ord r => Delta r -> Delta r -> Bool
< :: Delta r -> Delta r -> Bool
$c< :: forall r. Ord r => Delta r -> Delta r -> Bool
compare :: Delta r -> Delta r -> Ordering
$ccompare :: forall r. Ord r => Delta r -> Delta r -> Ordering
$cp1Ord :: forall r. Ord r => Eq (Delta r)
Ord, Delta r -> Delta r -> Bool
(Delta r -> Delta r -> Bool)
-> (Delta r -> Delta r -> Bool) -> Eq (Delta r)
forall r. Eq r => Delta r -> Delta r -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Delta r -> Delta r -> Bool
$c/= :: forall r. Eq r => Delta r -> Delta r -> Bool
== :: Delta r -> Delta r -> Bool
$c== :: forall r. Eq r => Delta r -> Delta r -> Bool
Eq, Int -> Delta r -> ShowS
[Delta r] -> ShowS
Delta r -> String
(Int -> Delta r -> ShowS)
-> (Delta r -> String) -> ([Delta r] -> ShowS) -> Show (Delta r)
forall r. Show r => Int -> Delta r -> ShowS
forall r. Show r => [Delta r] -> ShowS
forall r. Show r => Delta r -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Delta r] -> ShowS
$cshowList :: forall r. Show r => [Delta r] -> ShowS
show :: Delta r -> String
$cshow :: forall r. Show r => Delta r -> String
showsPrec :: Int -> Delta r -> ShowS
$cshowsPrec :: forall r. Show r => Int -> Delta r -> ShowS
Show)

-- | symbolic infinitesimal parameter δ.
delta :: Num r => Delta r
delta :: Delta r
delta = r -> r -> Delta r
forall r. r -> r -> Delta r
Delta r
0 r
1

-- | Conversion from a base @r@ value to @Delta r@.
fromReal :: Num r => r -> Delta r
fromReal :: r -> Delta r
fromReal r
x = r -> r -> Delta r
forall r. r -> r -> Delta r
Delta r
x r
0

-- | Extracts the real part..
realPart :: Delta r -> r
realPart :: Delta r -> r
realPart (Delta r
r r
_) = r
r

-- | Extracts the δ part..
deltaPart :: Delta r -> r
deltaPart :: Delta r -> r
deltaPart (Delta r
_ r
k) = r
k

instance Num r => AdditiveGroup (Delta r) where
  Delta r
r1 r
k1 ^+^ :: Delta r -> Delta r -> Delta r
^+^ Delta r
r2 r
k2 = r -> r -> Delta r
forall r. r -> r -> Delta r
Delta (r
r1r -> r -> r
forall a. Num a => a -> a -> a
+r
r2) (r
k1r -> r -> r
forall a. Num a => a -> a -> a
+r
k2)
  zeroV :: Delta r
zeroV = r -> r -> Delta r
forall r. r -> r -> Delta r
Delta r
0 r
0
  negateV :: Delta r -> Delta r
negateV (Delta r
r r
k) = r -> r -> Delta r
forall r. r -> r -> Delta r
Delta (- r
r) (- r
k)

instance Num r => VectorSpace (Delta r) where
  type Scalar (Delta r) = r
  Scalar (Delta r)
c *^ :: Scalar (Delta r) -> Delta r -> Delta r
*^ Delta r
r r
k = r -> r -> Delta r
forall r. r -> r -> Delta r
Delta (r
Scalar (Delta r)
cr -> r -> r
forall a. Num a => a -> a -> a
*r
r) (r
Scalar (Delta r)
cr -> r -> r
forall a. Num a => a -> a -> a
*r
k)

-- | This instance assumes the symbolic infinitesimal parameter δ is a nilpotent with δ² = 0.
instance (Num r, Ord r) => Num (Delta r) where
  + :: Delta r -> Delta r -> Delta r
(+) = Delta r -> Delta r -> Delta r
forall v. AdditiveGroup v => v -> v -> v
(^+^)
  negate :: Delta r -> Delta r
negate = Delta r -> Delta r
forall v. AdditiveGroup v => v -> v
negateV
  Delta r
r1 r
k1 * :: Delta r -> Delta r -> Delta r
* Delta r
r2 r
k2 = r -> r -> Delta r
forall r. r -> r -> Delta r
Delta (r
r1r -> r -> r
forall a. Num a => a -> a -> a
*r
r2) (r
r1r -> r -> r
forall a. Num a => a -> a -> a
*r
k2r -> r -> r
forall a. Num a => a -> a -> a
+r
r2r -> r -> r
forall a. Num a => a -> a -> a
*r
k1)
  abs :: Delta r -> Delta r
abs Delta r
x =
    case Delta r
x Delta r -> Delta r -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Delta r
0 of
      Ordering
LT -> Delta r -> Delta r
forall v. AdditiveGroup v => v -> v
negateV Delta r
x
      Ordering
EQ -> Delta r
x
      Ordering
GT -> Delta r
x
  signum :: Delta r -> Delta r
signum Delta r
x =
    case Delta r
x Delta r -> Delta r -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Delta r
0 of
      Ordering
LT -> -Delta r
1
      Ordering
EQ -> Delta r
0
      Ordering
GT -> Delta r
1
  fromInteger :: Integer -> Delta r
fromInteger Integer
x = r -> r -> Delta r
forall r. r -> r -> Delta r
Delta (Integer -> r
forall a. Num a => Integer -> a
fromInteger Integer
x) r
0

-- | This is unsafe instance in the sense that only a proper real can be a divisor.
instance (Fractional r, Ord r) => Fractional (Delta r) where
  Delta r
r1 r
k1 / :: Delta r -> Delta r -> Delta r
/ Delta r
r2 r
0  = r -> r -> Delta r
forall r. r -> r -> Delta r
Delta (r
r1 r -> r -> r
forall a. Fractional a => a -> a -> a
/ r
r2) (r
k1 r -> r -> r
forall a. Fractional a => a -> a -> a
/ r
r2)
  Delta r
r1 r
k1 / Delta r
r2 r
k2 =
    String -> Delta r
forall a. HasCallStack => String -> a
error String
"Fractional{ToySolver.Data.Delta.Delta}.(/): divisor must be a proper real"
  fromRational :: Rational -> Delta r
fromRational Rational
x = r -> r -> Delta r
forall r. r -> r -> Delta r
Delta (Rational -> r
forall a. Fractional a => Rational -> a
fromRational Rational
x) r
0

instance (Real r, Eq r) => Real (Delta r) where
  toRational :: Delta r -> Rational
toRational (Delta r
r r
0) = r -> Rational
forall a. Real a => a -> Rational
toRational r
r
  toRational (Delta r
r r
k) =
    String -> Rational
forall a. HasCallStack => String -> a
error String
"Real{ToySolver.Data.Delta.Delta}.toRational: not a real number"

instance (RealFrac r, Eq r) => RealFrac (Delta r) where
  properFraction :: Delta r -> (b, Delta r)
properFraction Delta r
x =
    case Delta r
x Delta r -> Delta r -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Delta r
0 of
      Ordering
LT -> let n :: b
n = Delta r -> b
forall r a. (RealFrac r, Integral a) => Delta r -> a
ceiling' Delta r
x in (b
n, Delta r
x Delta r -> Delta r -> Delta r
forall a. Num a => a -> a -> a
- b -> Delta r
forall a b. (Integral a, Num b) => a -> b
fromIntegral b
n)
      Ordering
EQ -> (b
0, Delta r
0)
      Ordering
GT -> let n :: b
n = Delta r -> b
forall r a. (RealFrac r, Integral a) => Delta r -> a
floor' Delta r
x in (b
n, Delta r
x Delta r -> Delta r -> Delta r
forall a. Num a => a -> a -> a
- b -> Delta r
forall a b. (Integral a, Num b) => a -> b
fromIntegral b
n)
  ceiling :: Delta r -> b
ceiling = Delta r -> b
forall r a. (RealFrac r, Integral a) => Delta r -> a
ceiling'
  floor :: Delta r -> b
floor   = Delta r -> b
forall r a. (RealFrac r, Integral a) => Delta r -> a
floor'

-- | 'Delta' version of 'floor'.
-- @'floor'' x@ returns the greatest integer not greater than @x@
floor' :: (RealFrac r, Integral a) => Delta r -> a
floor' :: Delta r -> a
floor' (Delta r
r r
k) = Integer -> a
forall a. Num a => Integer -> a
fromInteger (Integer -> a) -> Integer -> a
forall a b. (a -> b) -> a -> b
$ if r
r2r -> r -> Bool
forall a. Eq a => a -> a -> Bool
==r
r Bool -> Bool -> Bool
&& r
k r -> r -> Bool
forall a. Ord a => a -> a -> Bool
< r
0 then Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1 else Integer
i
  where
    i :: Integer
i = r -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
floor r
r
    r2 :: r
r2 = Integer -> r
forall a. Num a => Integer -> a
fromInteger Integer
i

-- | 'Delta' version of 'ceiling'.
-- @'ceiling'' x@ returns the least integer not less than @x@
ceiling' :: (RealFrac r, Integral a) => Delta r -> a
ceiling' :: Delta r -> a
ceiling' (Delta r
r r
k) = Integer -> a
forall a. Num a => Integer -> a
fromInteger (Integer -> a) -> Integer -> a
forall a b. (a -> b) -> a -> b
$ if r
r2r -> r -> Bool
forall a. Eq a => a -> a -> Bool
==r
r Bool -> Bool -> Bool
&& r
k r -> r -> Bool
forall a. Ord a => a -> a -> Bool
> r
0 then Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1 else Integer
i
  where
    i :: Integer
i = r -> Integer
forall a b. (RealFrac a, Integral b) => a -> b
ceiling r
r
    r2 :: r
r2 = Integer -> r
forall a. Num a => Integer -> a
fromInteger Integer
i

-- | Is this a integer?
isInteger' :: RealFrac r => Delta r -> Bool
isInteger' :: Delta r -> Bool
isInteger' (Delta r
r r
k) = r -> Bool
forall a. RealFrac a => a -> Bool
isInteger r
r Bool -> Bool -> Bool
&& r
k r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== r
0