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]) ]