module Satchmo.Binary.Op.Times

( times, dot_product
, Overflow (..), times'
)

where

import Prelude hiding ( and, or, not )

import Satchmo.Boolean
import qualified Satchmo.Code as C
import Satchmo.Binary.Data
import Satchmo.Binary.Op.Common

import qualified Data.Map as M
import Control.Monad ( forM )
import Control.Applicative

dot_product :: (MonadSAT m) 
             => ( Maybe Int) 
            -> [ Number ] -> [ Number ] -> m Number
dot_product :: forall (m :: * -> *).
MonadSAT m =>
Maybe Int -> [Number] -> [Number] -> m Number
dot_product Maybe Int
bound [Number]
xs [Number]
ys = do
    [[(Int, [Boolean])]]
cs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( forall a b. [a] -> [b] -> [(a, b)]
zip [Number]
xs [Number]
ys ) forall a b. (a -> b) -> a -> b
$ \ (Number
x,Number
y) -> forall {m :: * -> *} {a}.
(Num a, Enum a, MonadSAT m, Ord a) =>
Overflow -> Maybe a -> [Boolean] -> [Boolean] -> m [(a, [Boolean])]
product_components Overflow
Refuse Maybe Int
bound (Number -> [Boolean]
bits Number
x) (Number -> [Boolean]
bits Number
y)
    [Boolean] -> Number
make forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {m :: * -> *} {a}.
(MonadSAT m, Num a, Enum a, Ord a) =>
Overflow -> Maybe a -> [(a, [Boolean])] -> m [Boolean]
export Overflow
Refuse Maybe Int
bound ( forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Int, [Boolean])]]
cs )

data Overflow = Ignore | Refuse

times :: (MonadSAT m) 
             => Maybe Int
             -> Number -> Number -> m Number
times :: forall (m :: * -> *).
MonadSAT m =>
Maybe Int -> Number -> Number -> m Number
times Maybe Int
bound Number
a Number
b =
  [Boolean] -> Number
make forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {m :: * -> *} {a}.
(Num a, Enum a, MonadSAT m, Ord a) =>
Overflow -> Maybe a -> [Boolean] -> [Boolean] -> m [Boolean]
times' Overflow
Refuse Maybe Int
bound (Number -> [Boolean]
bits Number
a) (Number -> [Boolean]
bits Number
b)

times' :: Overflow -> Maybe a -> [Boolean] -> [Boolean] -> m [Boolean]
times' Overflow
over Maybe a
bound [Boolean]
a [Boolean]
b = do
    [(a, [Boolean])]
kzs <- forall {m :: * -> *} {a}.
(Num a, Enum a, MonadSAT m, Ord a) =>
Overflow -> Maybe a -> [Boolean] -> [Boolean] -> m [(a, [Boolean])]
product_components Overflow
over Maybe a
bound [Boolean]
a [Boolean]
b
    forall {m :: * -> *} {a}.
(MonadSAT m, Num a, Enum a, Ord a) =>
Overflow -> Maybe a -> [(a, [Boolean])] -> m [Boolean]
export Overflow
over Maybe a
bound [(a, [Boolean])]
kzs

product_components :: Overflow -> Maybe a -> [Boolean] -> [Boolean] -> m [(a, [Boolean])]
product_components Overflow
over Maybe a
bound [Boolean]
a [Boolean]
b = forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall a b. (a -> b) -> a -> b
$ do
    ( a
i , Boolean
x ) <- forall a b. [a] -> [b] -> [(a, b)]
zip [ a
0 .. ] [Boolean]
a
    ( a
j , Boolean
y ) <- forall a b. [a] -> [b] -> [(a, b)]
zip [ a
0 .. ] [Boolean]
b        
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
        Boolean
z <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean
x, Boolean
y ]
        if ( case Maybe a
bound of Maybe a
Nothing -> Bool
False ; Just a
b -> a
iforall a. Num a => a -> a -> a
+a
j forall a. Ord a => a -> a -> Bool
>= a
b )
             then do
                case Overflow
over of
                  Overflow
Ignore -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
                  Overflow
Refuse -> forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [ Boolean -> Boolean
not Boolean
z ]
                forall (m :: * -> *) a. Monad m => a -> m a
return ( a
iforall a. Num a => a -> a -> a
+a
j , [ ] )
             else do
                forall (m :: * -> *) a. Monad m => a -> m a
return ( a
iforall a. Num a => a -> a -> a
+a
j , [Boolean
z] ) 

export :: Overflow -> Maybe a -> [(a, [Boolean])] -> m [Boolean]
export Overflow
over Maybe a
bound [(a, [Boolean])]
kzs = do 
    Map a [Boolean]
m <- forall {m :: * -> *} {k}.
(Ord k, MonadSAT m, Num k) =>
Overflow -> Maybe k -> Map k [Boolean] -> m (Map k [Boolean])
reduce Overflow
over Maybe a
bound forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith forall a. [a] -> [a] -> [a]
(++) [(a, [Boolean])]
kzs
    case forall k a. Map k a -> Maybe ((k, a), Map k a)
M.maxViewWithKey Map a [Boolean]
m of
        Maybe ((a, [Boolean]), Map a [Boolean])
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return []
        Just ((a
k,[Boolean]
_) , Map a [Boolean]
_) -> do 
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do 
                    a
i <- [ a
0 .. a
k ] 
                    let { [ Boolean
b ] = Map a [Boolean]
m forall k a. Ord k => Map k a -> k -> a
M.! a
i }  
                    forall (m :: * -> *) a. Monad m => a -> m a
return Boolean
b

reduce :: Overflow -> Maybe k -> Map k [Boolean] -> m (Map k [Boolean])
reduce Overflow
over Maybe k
bound Map k [Boolean]
m = case forall k a. Map k a -> Maybe ((k, a), Map k a)
M.minViewWithKey Map k [Boolean]
m of
    Maybe ((k, [Boolean]), Map k [Boolean])
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall k a. Map k a
M.empty
    Just ((k
k, [Boolean]
bs), Map k [Boolean]
rest ) -> 
        if ( case Maybe k
bound of Maybe k
Nothing -> Bool
False ; Just k
b -> k
k forall a. Ord a => a -> a -> Bool
>= k
b )
        then do
            forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Boolean]
bs forall a b. (a -> b) -> a -> b
$ \ Boolean
b -> case Overflow
over of
              Overflow
Refuse -> forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [ Boolean -> Boolean
not Boolean
b ]
              Overflow
Ignore -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Overflow -> Maybe k -> Map k [Boolean] -> m (Map k [Boolean])
reduce Overflow
over Maybe k
bound Map k [Boolean]
rest
        else case [Boolean]
bs of
            [] -> Overflow -> Maybe k -> Map k [Boolean] -> m (Map k [Boolean])
reduce Overflow
over Maybe k
bound Map k [Boolean]
rest
            [Boolean
x] -> do
                Map k [Boolean]
m' <- Overflow -> Maybe k -> Map k [Boolean] -> m (Map k [Boolean])
reduce Overflow
over Maybe k
bound Map k [Boolean]
rest
                forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith (forall a. HasCallStack => [Char] -> a
error [Char]
"huh") Map k [Boolean]
m' 
                       forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(k
k,[Boolean
x])] 
            [Boolean
x,Boolean
y] -> do
                (Boolean
r,Boolean
c) <- forall (m :: * -> *).
MonadSAT m =>
Boolean -> Boolean -> m (Boolean, Boolean)
half_adder Boolean
x Boolean
y
                Overflow -> Maybe k -> Map k [Boolean] -> m (Map k [Boolean])
reduce Overflow
over Maybe k
bound forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith forall a. [a] -> [a] -> [a]
(++) Map k [Boolean]
rest
                       forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (k
k,[Boolean
r]), (k
kforall a. Num a => a -> a -> a
+k
1, [Boolean
c]) ] 
            (Boolean
x:Boolean
y:Boolean
z:[Boolean]
more) -> do
                (Boolean
r,Boolean
c) <- forall (m :: * -> *).
MonadSAT m =>
Boolean -> Boolean -> Boolean -> m (Boolean, Boolean)
full_adder Boolean
x Boolean
y Boolean
z
                Overflow -> Maybe k -> Map k [Boolean] -> m (Map k [Boolean])
reduce Overflow
over Maybe k
bound forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith forall a. [a] -> [a] -> [a]
(++) Map k [Boolean]
rest
                       forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (k
k, [Boolean]
more forall a. [a] -> [a] -> [a]
++ [Boolean
r]), (k
kforall a. Num a => a -> a -> a
+k
1, [Boolean
c]) ]