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 <- [(Number, Number)]
-> ((Number, Number) -> m [(Int, [Boolean])])
-> m [[(Int, [Boolean])]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( [Number] -> [Number] -> [(Number, Number)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Number]
xs [Number]
ys ) (((Number, Number) -> m [(Int, [Boolean])])
 -> m [[(Int, [Boolean])]])
-> ((Number, Number) -> m [(Int, [Boolean])])
-> m [[(Int, [Boolean])]]
forall a b. (a -> b) -> a -> b
$ \ (Number
x,Number
y) -> Overflow
-> Maybe Int -> [Boolean] -> [Boolean] -> m [(Int, [Boolean])]
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 ([Boolean] -> Number) -> m [Boolean] -> m Number
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Overflow -> Maybe Int -> [(Int, [Boolean])] -> m [Boolean]
forall {m :: * -> *} {a}.
(MonadSAT m, Num a, Enum a, Ord a) =>
Overflow -> Maybe a -> [(a, [Boolean])] -> m [Boolean]
export Overflow
Refuse Maybe Int
bound ( [[(Int, [Boolean])]] -> [(Int, [Boolean])]
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 ([Boolean] -> Number) -> m [Boolean] -> m Number
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Overflow -> Maybe Int -> [Boolean] -> [Boolean] -> m [Boolean]
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 <- Overflow -> Maybe a -> [Boolean] -> [Boolean] -> m [(a, [Boolean])]
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
    Overflow -> Maybe a -> [(a, [Boolean])] -> m [Boolean]
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 = [m (a, [Boolean])] -> m [(a, [Boolean])]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([m (a, [Boolean])] -> m [(a, [Boolean])])
-> [m (a, [Boolean])] -> m [(a, [Boolean])]
forall a b. (a -> b) -> a -> b
$ do
    ( a
i , Boolean
x ) <- [a] -> [Boolean] -> [(a, Boolean)]
forall a b. [a] -> [b] -> [(a, b)]
zip [ a
0 .. ] [Boolean]
a
    ( a
j , Boolean
y ) <- [a] -> [Boolean] -> [(a, Boolean)]
forall a b. [a] -> [b] -> [(a, b)]
zip [ a
0 .. ] [Boolean]
b        
    m (a, [Boolean]) -> [m (a, [Boolean])]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (m (a, [Boolean]) -> [m (a, [Boolean])])
-> m (a, [Boolean]) -> [m (a, [Boolean])]
forall a b. (a -> b) -> a -> b
$ do
        Boolean
z <- [Boolean] -> m Boolean
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
ia -> a -> a
forall a. Num a => a -> a -> a
+a
j a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
b )
             then do
                case Overflow
over of
                  Overflow
Ignore -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                  Overflow
Refuse -> [Boolean] -> m ()
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [ Boolean -> Boolean
not Boolean
z ]
                (a, [Boolean]) -> m (a, [Boolean])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ( a
ia -> a -> a
forall a. Num a => a -> a -> a
+a
j , [ ] )
             else do
                (a, [Boolean]) -> m (a, [Boolean])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ( a
ia -> a -> a
forall 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 <- Overflow -> Maybe a -> Map a [Boolean] -> m (Map a [Boolean])
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 (Map a [Boolean] -> m (Map a [Boolean]))
-> Map a [Boolean] -> m (Map a [Boolean])
forall a b. (a -> b) -> a -> b
$ ([Boolean] -> [Boolean] -> [Boolean])
-> [(a, [Boolean])] -> Map a [Boolean]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith [Boolean] -> [Boolean] -> [Boolean]
forall a. [a] -> [a] -> [a]
(++) [(a, [Boolean])]
kzs
    case Map a [Boolean] -> Maybe ((a, [Boolean]), Map a [Boolean])
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 -> [Boolean] -> m [Boolean]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        Just ((a
k,[Boolean]
_) , Map a [Boolean]
_) -> do 
              [Boolean] -> m [Boolean]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Boolean] -> m [Boolean]) -> [Boolean] -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ do 
                    a
i <- [ a
0 .. a
k ] 
                    let { [ Boolean
b ] = Map a [Boolean]
m Map a [Boolean] -> a -> [Boolean]
forall k a. Ord k => Map k a -> k -> a
M.! a
i }  
                    Boolean -> [Boolean]
forall a. a -> [a]
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 Map k [Boolean] -> Maybe ((k, [Boolean]), Map k [Boolean])
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 -> Map k [Boolean] -> m (Map k [Boolean])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Map k [Boolean]
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 k -> k -> Bool
forall a. Ord a => a -> a -> Bool
>= k
b )
        then do
            [Boolean] -> (Boolean -> m ()) -> m [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Boolean]
bs ((Boolean -> m ()) -> m [()]) -> (Boolean -> m ()) -> m [()]
forall a b. (a -> b) -> a -> b
$ \ Boolean
b -> case Overflow
over of
              Overflow
Refuse -> [Boolean] -> m ()
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [ Boolean -> Boolean
not Boolean
b ]
              Overflow
Ignore -> () -> m ()
forall a. a -> m a
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
                Map k [Boolean] -> m (Map k [Boolean])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Map k [Boolean] -> m (Map k [Boolean]))
-> Map k [Boolean] -> m (Map k [Boolean])
forall a b. (a -> b) -> a -> b
$ ([Boolean] -> [Boolean] -> [Boolean])
-> Map k [Boolean] -> Map k [Boolean] -> Map k [Boolean]
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith ([Char] -> [Boolean] -> [Boolean] -> [Boolean]
forall a. HasCallStack => [Char] -> a
error [Char]
"huh") Map k [Boolean]
m' 
                       (Map k [Boolean] -> Map k [Boolean])
-> Map k [Boolean] -> Map k [Boolean]
forall a b. (a -> b) -> a -> b
$ [(k, [Boolean])] -> Map k [Boolean]
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) <- Boolean -> Boolean -> m (Boolean, Boolean)
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 (Map k [Boolean] -> m (Map k [Boolean]))
-> Map k [Boolean] -> m (Map k [Boolean])
forall a b. (a -> b) -> a -> b
$ ([Boolean] -> [Boolean] -> [Boolean])
-> Map k [Boolean] -> Map k [Boolean] -> Map k [Boolean]
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith [Boolean] -> [Boolean] -> [Boolean]
forall a. [a] -> [a] -> [a]
(++) Map k [Boolean]
rest
                       (Map k [Boolean] -> Map k [Boolean])
-> Map k [Boolean] -> Map k [Boolean]
forall a b. (a -> b) -> a -> b
$ [(k, [Boolean])] -> Map k [Boolean]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (k
k,[Boolean
r]), (k
kk -> k -> k
forall a. Num a => a -> a -> a
+k
1, [Boolean
c]) ] 
            (Boolean
x:Boolean
y:Boolean
z:[Boolean]
more) -> do
                (Boolean
r,Boolean
c) <- Boolean -> Boolean -> Boolean -> m (Boolean, Boolean)
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 (Map k [Boolean] -> m (Map k [Boolean]))
-> Map k [Boolean] -> m (Map k [Boolean])
forall a b. (a -> b) -> a -> b
$ ([Boolean] -> [Boolean] -> [Boolean])
-> Map k [Boolean] -> Map k [Boolean] -> Map k [Boolean]
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith [Boolean] -> [Boolean] -> [Boolean]
forall a. [a] -> [a] -> [a]
(++) Map k [Boolean]
rest
                       (Map k [Boolean] -> Map k [Boolean])
-> Map k [Boolean] -> Map k [Boolean]
forall a b. (a -> b) -> a -> b
$ [(k, [Boolean])] -> Map k [Boolean]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (k
k, [Boolean]
more [Boolean] -> [Boolean] -> [Boolean]
forall a. [a] -> [a] -> [a]
++ [Boolean
r]), (k
kk -> k -> k
forall a. Num a => a -> a -> a
+k
1, [Boolean
c]) ]