{-# language MultiParamTypeClasses #-}

-- | Operations with fixed bit width.
-- Still they are non-overflowing:
-- if overflow occurs, the constraints are not satisfiable.
-- The bit width of the result of binary operations
-- is the max of the bit width of the inputs.

module Satchmo.BinaryTwosComplement.Op.Fixed
    ( add, subtract, times, increment, negate, linear
    , module Satchmo.BinaryTwosComplement.Data
    , module Satchmo.BinaryTwosComplement.Op.Common
    )
where

import Prelude hiding (not,negate, subtract)
import Control.Applicative ((<$>))
import Satchmo.MonadSAT (MonadSAT)
import Satchmo.BinaryTwosComplement.Op.Common
import Satchmo.BinaryTwosComplement.Data
import qualified Satchmo.Binary.Op.Common as C
import qualified Satchmo.Binary.Op.Flexible as F
import Satchmo.Binary.Op.Fixed (restrictedTimes)
import Satchmo.Boolean (Boolean,monadic,assertOr,equals2,implies,not)
import qualified Satchmo.Boolean as Boolean

-- | Sign extension
extendMsb :: Int -> Number -> Number
extendMsb :: Int -> Number -> Number
extendMsb Int
i Number
n = [Boolean] -> Number
fromBooleans forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
n forall a. [a] -> [a] -> [a]
++ (forall a. Int -> a -> [a]
replicate Int
i forall a b. (a -> b) -> a -> b
$ Number -> Boolean
msb Number
n)

add :: (MonadSAT m) => Number -> Number -> m Number
add :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
add Number
a Number
b = do
  let maxWidth :: Int
maxWidth  = forall a. Ord a => a -> a -> a
max (Number -> Int
width Number
a) (Number -> Int
width Number
b)
      widthDiff :: Int
widthDiff = forall a. Num a => a -> a
abs forall a b. (a -> b) -> a -> b
$ (Number -> Int
width Number
a) forall a. Num a => a -> a -> a
- (Number -> Int
width Number
b)
      extend :: Number -> Number
extend Number
x = if Number -> Int
width Number
x forall a. Eq a => a -> a -> Bool
== Int
maxWidth then Int -> Number -> Number
extendMsb Int
1 Number
x
                 else Int -> Number -> Number
extendMsb (Int
widthDiff forall a. Num a => a -> a -> a
+ Int
1) Number
x
      a' :: Number
a' = Number -> Number
extend Number
a
      b' :: Number
b' = Number -> Number
extend Number
b

  Number
flexibleResult <- Number -> Number
fromUnsigned forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
F.add (Number -> Number
toUnsigned Number
a') (Number -> Number
toUnsigned Number
b')
  let ([Boolean]
low, [Boolean]
high) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
maxWidth forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
flexibleResult

  Boolean
e <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
Boolean.equals [forall a. [a] -> a
last [Boolean]
low, forall a. [a] -> a
head [Boolean]
high]
  forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr [ Boolean
e ]
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
fromBooleans [Boolean]
low

times :: MonadSAT m => Number -> Number -> m Number
times :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
times Number
a Number
b = do
  let a' :: Number
a' = Int -> Number -> Number
extendMsb (Number -> Int
width Number
b) Number
a
      b' :: Number
b' = Int -> Number -> Number
extendMsb (Number -> Int
width Number
a) Number
b
      unsignedResultWidth :: Int
unsignedResultWidth = (Number -> Int
width Number
a) forall a. Num a => a -> a -> a
+ (Number -> Int
width Number
b)
      resultWidth :: Int
resultWidth = forall a. Ord a => a -> a -> a
max (Number -> Int
width Number
a) (Number -> Int
width Number
b)

  Number
unsignedResult <- Number -> Number
fromUnsigned forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 
                    forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
restrictedTimes (Number -> Number
toUnsigned Number
a') (Number -> Number
toUnsigned Number
b')
  let ([Boolean]
low, [Boolean]
high) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
resultWidth forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
unsignedResult
  Boolean
allHighOne  <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
Boolean.and forall a b. (a -> b) -> a -> b
$ [Boolean]
high
  Boolean
allHighZero <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
Boolean.and forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Boolean -> Boolean
not [Boolean]
high
  forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr [Boolean
allHighOne, Boolean
allHighZero]

  Boolean
e <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
Boolean.equals [ forall a. [a] -> a
last [Boolean]
low, forall a. [a] -> a
head [Boolean]
high ]
  forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr [Boolean
e]
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
fromBooleans [Boolean]
low

increment :: MonadSAT m => Number -> m Number
increment :: forall (m :: * -> *). MonadSAT m => Number -> m Number
increment Number
n =
    let inc :: [Boolean] -> Boolean -> m ([Boolean], Boolean)
inc [] Boolean
z = forall (m :: * -> *) a. Monad m => a -> m a
return ( [], Boolean
z )
        inc (Boolean
y:[Boolean]
ys) Boolean
z = do
          ( Boolean
r, Boolean
c ) <- forall (m :: * -> *).
MonadSAT m =>
Boolean -> Boolean -> m (Boolean, Boolean)
C.half_adder Boolean
y Boolean
z
          ( [Boolean]
rAll, Boolean
cAll ) <- [Boolean] -> Boolean -> m ([Boolean], Boolean)
inc [Boolean]
ys Boolean
c
          forall (m :: * -> *) a. Monad m => a -> m a
return ( Boolean
r forall a. a -> [a] -> [a]
: [Boolean]
rAll, Boolean
cAll )
    in do
      Boolean
add1 <- forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
Boolean.constant Bool
True
      ([Boolean]
n', Boolean
_) <- forall {m :: * -> *}.
MonadSAT m =>
[Boolean] -> Boolean -> m ([Boolean], Boolean)
inc (Number -> [Boolean]
bits Number
n) Boolean
add1
      Boolean
e <- (Boolean -> Boolean
not forall a b. (a -> b) -> a -> b
$ Number -> Boolean
msb Number
n) forall (m :: * -> *). MonadSAT m => Boolean -> Boolean -> m Boolean
`implies` (Boolean -> Boolean
not forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
last [Boolean]
n')
      forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr [ Boolean
e ]
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
fromBooleans [Boolean]
n'

subtract :: MonadSAT m => Number -> Number -> m Number
subtract :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
subtract Number
a Number
b = do
    Number
b' <- forall (m :: * -> *). MonadSAT m => Number -> m Number
negate Number
b
    forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
add Number
a Number
b'

negate :: MonadSAT m => Number -> m Number
negate :: forall (m :: * -> *). MonadSAT m => Number -> m Number
negate Number
n =
    let invN :: Number
invN = [Boolean] -> Number
fromBooleans forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Boolean -> Boolean
not forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
n
    in do
      Number
n' <- forall (m :: * -> *). MonadSAT m => Number -> m Number
increment Number
invN
      Boolean
e <- (Number -> Boolean
msb Number
n) forall (m :: * -> *). MonadSAT m => Boolean -> Boolean -> m Boolean
`implies` (Boolean -> Boolean
not forall a b. (a -> b) -> a -> b
$ Number -> Boolean
msb Number
n')
      forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr [ Boolean
e ]
      forall (m :: * -> *) a. Monad m => a -> m a
return Number
n'
      
linear :: MonadSAT m => Number -> Number -> Number -> m Number
linear :: forall (m :: * -> *).
MonadSAT m =>
Number -> Number -> Number -> m Number
linear Number
m Number
x Number
n = Number
m forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
`times` Number
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
add Number
n