Delta.hs

{-# 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 (Ord, Eq, Show)

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

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

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

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

instance Num r => AdditiveGroup (Delta r) where
  Delta r1 k1 ^+^ Delta r2 k2 = Delta (r1+r2) (k1+k2)
  zeroV = Delta 0 0
  negateV (Delta r k) = Delta (- r) (- k)

instance Num r => VectorSpace (Delta r) where
  type Scalar (Delta r) = r
  c *^ Delta r k = Delta (c*r) (c*k)

-- | This instance assumes the symbolic infinitesimal parameter δ is a nilpotent with δ² = 0.
instance (Num r, Ord r) => Num (Delta r) where
  (+) = (^+^)
  negate = negateV
  Delta r1 k1 * Delta r2 k2 = Delta (r1*r2) (r1*k2+r2*k1)
  abs x =
    case x `compare` 0 of
      LT -> negateV x
      EQ -> x
      GT -> x
  signum x =
    case x `compare` 0 of
      LT -> -1
      EQ -> 0
      GT -> 1
  fromInteger x = Delta (fromInteger x) 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 r1 k1 / Delta r2 0  = Delta (r1 / r2) (k1 / r2)
  Delta r1 k1 / Delta r2 k2 =
    error "Fractional{ToySolver.Data.Delta.Delta}.(/): divisor must be a proper real"
  fromRational x = Delta (fromRational x) 0

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

instance (RealFrac r, Eq r) => RealFrac (Delta r) where
  properFraction x =
    case x `compare` 0 of
      LT -> let n = ceiling' x in (n, x - fromIntegral n)
      EQ -> (0, 0)
      GT -> let n = floor' x in (n, x - fromIntegral n)
  ceiling = ceiling'
  floor   = 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 k) = fromInteger $ if r2==r && k < 0 then i-1 else i
  where
    i = floor r
    r2 = fromInteger 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 k) = fromInteger $ if r2==r && k > 0 then i+1 else i
  where
    i = ceiling r
    r2 = fromInteger i

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