{-# 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 ([Boolean] -> Number) -> [Boolean] -> Number
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
n [Boolean] -> [Boolean] -> [Boolean]
forall a. [a] -> [a] -> [a]
++ (Int -> Boolean -> [Boolean]
forall a. Int -> a -> [a]
replicate Int
i (Boolean -> [Boolean]) -> Boolean -> [Boolean]
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  = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Number -> Int
width Number
a) (Number -> Int
width Number
b)
      widthDiff :: Int
widthDiff = Int -> Int
forall a. Num a => a -> a
abs (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ (Number -> Int
width Number
a) Int -> Int -> Int
forall a. Num a => a -> a -> a
- (Number -> Int
width Number
b)
      extend :: Number -> Number
extend Number
x = if Number -> Int
width Number
x Int -> Int -> Bool
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 Int -> Int -> Int
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 (Number -> Number) -> m Number -> m Number
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Number -> Number -> m Number
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) = Int -> [Boolean] -> ([Boolean], [Boolean])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
maxWidth ([Boolean] -> ([Boolean], [Boolean]))
-> [Boolean] -> ([Boolean], [Boolean])
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
flexibleResult

  Boolean
e <- [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
Boolean.equals [[Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
last [Boolean]
low, [Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
head [Boolean]
high]
  [Boolean] -> m ()
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr [ Boolean
e ]
  Number -> m Number
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number -> m Number) -> Number -> m Number
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) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Number -> Int
width Number
b)
      resultWidth :: Int
resultWidth = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Number -> Int
width Number
a) (Number -> Int
width Number
b)

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

  Boolean
e <- [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
Boolean.equals [ [Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
last [Boolean]
low, [Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
head [Boolean]
high ]
  [Boolean] -> m ()
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr [Boolean
e]
  Number -> m Number
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number -> m Number) -> Number -> m Number
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 = ([Boolean], Boolean) -> m ([Boolean], Boolean)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ( [], Boolean
z )
        inc (Boolean
y:[Boolean]
ys) Boolean
z = do
          ( Boolean
r, Boolean
c ) <- Boolean -> Boolean -> m (Boolean, Boolean)
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
          ([Boolean], Boolean) -> m ([Boolean], Boolean)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ( Boolean
r Boolean -> [Boolean] -> [Boolean]
forall a. a -> [a] -> [a]
: [Boolean]
rAll, Boolean
cAll )
    in do
      Boolean
add1 <- Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
Boolean.constant Bool
True
      ([Boolean]
n', Boolean
_) <- [Boolean] -> Boolean -> m ([Boolean], Boolean)
forall {m :: * -> *}.
MonadSAT m =>
[Boolean] -> Boolean -> m ([Boolean], Boolean)
inc (Number -> [Boolean]
bits Number
n) Boolean
add1
      Boolean
e <- (Boolean -> Boolean
not (Boolean -> Boolean) -> Boolean -> Boolean
forall a b. (a -> b) -> a -> b
$ Number -> Boolean
msb Number
n) Boolean -> Boolean -> m Boolean
forall (m :: * -> *). MonadSAT m => Boolean -> Boolean -> m Boolean
`implies` (Boolean -> Boolean
not (Boolean -> Boolean) -> Boolean -> Boolean
forall a b. (a -> b) -> a -> b
$ [Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
last [Boolean]
n')
      [Boolean] -> m ()
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr [ Boolean
e ]
      Number -> m Number
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number -> m Number) -> Number -> m Number
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' <- Number -> m Number
forall (m :: * -> *). MonadSAT m => Number -> m Number
negate Number
b
    Number -> Number -> m Number
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 ([Boolean] -> Number) -> [Boolean] -> Number
forall a b. (a -> b) -> a -> b
$ (Boolean -> Boolean) -> [Boolean] -> [Boolean]
forall a b. (a -> b) -> [a] -> [b]
map Boolean -> Boolean
not ([Boolean] -> [Boolean]) -> [Boolean] -> [Boolean]
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
n
    in do
      Number
n' <- Number -> m Number
forall (m :: * -> *). MonadSAT m => Number -> m Number
increment Number
invN
      Boolean
e <- (Number -> Boolean
msb Number
n) Boolean -> Boolean -> m Boolean
forall (m :: * -> *). MonadSAT m => Boolean -> Boolean -> m Boolean
`implies` (Boolean -> Boolean
not (Boolean -> Boolean) -> Boolean -> Boolean
forall a b. (a -> b) -> a -> b
$ Number -> Boolean
msb Number
n')
      [Boolean] -> m ()
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr [ Boolean
e ]
      Number -> m Number
forall a. a -> m a
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 Number -> Number -> m Number
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
`times` Number
x m Number -> (Number -> m Number) -> m Number
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Number -> Number -> m Number
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
add Number
n