{-# language MultiParamTypeClasses #-}
module Satchmo.Binary.Op.Fixed
( restricted
, add, times, dot_product, dot_product'
, module Satchmo.Binary.Data
, module Satchmo.Binary.Op.Common
, restrictedTimes
)
where
import Prelude hiding ( and, or, not, min, max )
import qualified Prelude
import Control.Monad (foldM)
import qualified Satchmo.Code as C
import Satchmo.Boolean
import Satchmo.Binary.Data
import Satchmo.Binary.Op.Common
import qualified Satchmo.Binary.Op.Times as T
import qualified Satchmo.Binary.Op.Flexible as Flexible
import Satchmo.Counting
import Control.Monad ( forM, when )
import Data.Map ( Map )
import qualified Data.Map as M
restricted :: (MonadSAT m) => Int -> Number -> m Number
restricted :: forall (m :: * -> *). MonadSAT m => Int -> Number -> m Number
restricted Int
w Number
a = do
let ( [Boolean]
low, [Boolean]
high ) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
w forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall a b. (a -> b) -> a -> b
$ do Boolean
x <- [Boolean]
high ; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr [ Boolean -> Boolean
not Boolean
x ]
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
low
add :: (MonadSAT m) => Number -> Number -> m Number
add :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
add Number
a Number
b = do
Boolean
false <- forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
Satchmo.Boolean.constant Bool
False
let w :: Int
w = forall a. Ord a => a -> a -> a
Prelude.max ( Number -> Int
width Number
a ) ( Number -> Int
width Number
b )
[Boolean]
zs <- forall (m :: * -> *).
MonadSAT m =>
Int -> Boolean -> [Boolean] -> [Boolean] -> m [Boolean]
add_with_carry Int
w Boolean
false ( Number -> [Boolean]
bits Number
a ) ( Number -> [Boolean]
bits Number
b )
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
zs
add_with_carry :: (MonadSAT m) => Int -> Boolean -> Booleans -> Booleans -> m Booleans
add_with_carry :: forall (m :: * -> *).
MonadSAT m =>
Int -> Boolean -> [Boolean] -> [Boolean] -> m [Boolean]
add_with_carry Int
w Boolean
c [Boolean]
xxs [Boolean]
yys = case ( [Boolean]
xxs, [Boolean]
yys ) of
([Boolean], [Boolean])
_ | Int
w forall a. Ord a => a -> a -> Bool
<= Int
0 -> do
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ forall a b. (a -> b) -> a -> b
$ do Boolean
p <- Boolean
c forall a. a -> [a] -> [a]
: [Boolean]
xxs forall a. [a] -> [a] -> [a]
++ [Boolean]
yys ; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr [ Boolean -> Boolean
not Boolean
p ]
forall (m :: * -> *) a. Monad m => a -> m a
return []
( [] , [] ) -> forall (m :: * -> *) a. Monad m => a -> m a
return [ Boolean
c ]
( [], Boolean
y : [Boolean]
ys) -> do
(Boolean
r,Boolean
d) <- forall (m :: * -> *).
MonadSAT m =>
Boolean -> Boolean -> m (Boolean, Boolean)
half_adder Boolean
c Boolean
y
[Boolean]
rest <- forall (m :: * -> *).
MonadSAT m =>
Int -> Boolean -> [Boolean] -> [Boolean] -> m [Boolean]
add_with_carry (Int
wforall a. Num a => a -> a -> a
-Int
1) Boolean
d [] [Boolean]
ys
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Boolean
r forall a. a -> [a] -> [a]
: [Boolean]
rest
( Boolean
x : [Boolean]
xs, [] ) -> forall (m :: * -> *).
MonadSAT m =>
Int -> Boolean -> [Boolean] -> [Boolean] -> m [Boolean]
add_with_carry Int
w Boolean
c [Boolean]
yys [Boolean]
xxs
(Boolean
x : [Boolean]
xs, Boolean
y:[Boolean]
ys) -> do
(Boolean
r,Boolean
d) <- forall (m :: * -> *).
MonadSAT m =>
Boolean -> Boolean -> Boolean -> m (Boolean, Boolean)
full_adder Boolean
c Boolean
x Boolean
y
[Boolean]
rest <- forall (m :: * -> *).
MonadSAT m =>
Int -> Boolean -> [Boolean] -> [Boolean] -> m [Boolean]
add_with_carry (Int
wforall a. Num a => a -> a -> a
-Int
1) Boolean
d [Boolean]
xs [Boolean]
ys
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Boolean
r forall a. a -> [a] -> [a]
: [Boolean]
rest
times :: (MonadSAT m) => Number -> Number -> m Number
times :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
times Number
a Number
b = do
let w :: Int
w = forall a. Ord a => a -> a -> a
Prelude.max ( Number -> Int
width Number
a ) ( Number -> Int
width Number
b )
forall (m :: * -> *).
MonadSAT m =>
Maybe Int -> Number -> Number -> m Number
T.times (forall a. a -> Maybe a
Just Int
w) Number
a Number
b
dot_product :: (MonadSAT m)
=> Int -> [ Number ] -> [ Number ] -> m Number
dot_product :: forall (m :: * -> *).
MonadSAT m =>
Int -> [Number] -> [Number] -> m Number
dot_product Int
w [Number]
xs [Number]
ys = do
forall (m :: * -> *).
MonadSAT m =>
Maybe Int -> [Number] -> [Number] -> m Number
T.dot_product (forall a. a -> Maybe a
Just Int
w) [Number]
xs [Number]
ys
dot_product' :: [Number] -> [Number] -> m Number
dot_product' [Number]
xs [Number]
ys = do
let l :: Number -> Int
l = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. Number -> [Boolean]
bits
w :: Int
w = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
Prelude.maximum forall a b. (a -> b) -> a -> b
$ Int
0 forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map Number -> Int
l ( [Number]
xs forall a. [a] -> [a] -> [a]
++ [Number]
ys )
forall (m :: * -> *).
MonadSAT m =>
Int -> [Number] -> [Number] -> m Number
dot_product Int
w [Number]
xs [Number]
ys
restrictedAdd :: (MonadSAT m) => Number -> Number -> m Number
restrictedAdd :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
restrictedAdd Number
a Number
b = do
Boolean
zero <- forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
Satchmo.Boolean.constant Bool
False
([Boolean]
result, Boolean
_) <- forall (m :: * -> *).
MonadSAT m =>
Boolean -> [Boolean] -> [Boolean] -> m ([Boolean], Boolean)
Flexible.add_with_carry Boolean
zero (Number -> [Boolean]
bits Number
a) (Number -> [Boolean]
bits Number
b)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
result
restrictedShift :: (MonadSAT m) => Number -> m Number
restrictedShift :: forall (m :: * -> *). MonadSAT m => Number -> m Number
restrictedShift Number
a = do
Boolean
zero <- forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
Satchmo.Boolean.constant Bool
False
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make forall a b. (a -> b) -> a -> b
$ Boolean
zero forall a. a -> [a] -> [a]
: (forall a. Int -> [a] -> [a]
take (Number -> Int
width Number
a forall a. Num a => a -> a -> a
- Int
1) forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a)
restrictedTimes :: (MonadSAT m) => Number -> Number -> m Number
restrictedTimes :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
restrictedTimes Number
as Number
bs = do
(Number, Number)
result <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\(Number
as',Number
sum) Boolean
b -> do
Number
summand <- forall (m :: * -> *). MonadSAT m => Boolean -> Number -> m Number
Flexible.times1 Boolean
b Number
as'
Number
sum' <- Number
sum forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
`restrictedAdd` Number
summand
Number
nextAs' <- forall (m :: * -> *). MonadSAT m => Number -> m Number
restrictedShift Number
as'
forall (m :: * -> *) a. Monad m => a -> m a
return (Number
nextAs', Number
sum')
) (Number
as, [Boolean] -> Number
make []) forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
bs
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd (Number, Number)
result