{-# language MultiParamTypeClasses #-}
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
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