{-# language MultiParamTypeClasses, PatternGuards #-}

-- | operations from this module cannot overflow.
-- instead they increase the bit width.

module Satchmo.Binary.Op.Flexible

( add, times, dot_product
, add_with_carry, times1, shift
, module Satchmo.Binary.Data
, module Satchmo.Binary.Op.Common
)

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 Satchmo.Binary.Op.Times as T
import Satchmo.Counting.Unary

import qualified Data.Map as M

add :: (MonadSAT m) => Number -> Number -> m Number
add :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
add Number
a Number
b = do
    Boolean
false <- Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
Satchmo.Boolean.constant Bool
False
    ( Booleans
zs, Boolean
carry ) <- 
        Boolean -> Booleans -> Booleans -> m (Booleans, Boolean)
forall (m :: * -> *).
MonadSAT m =>
Boolean -> Booleans -> Booleans -> m (Booleans, Boolean)
add_with_carry Boolean
false (Number -> Booleans
bits Number
a) (Number -> Booleans
bits Number
b)
    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
$ Booleans -> Number
make (Booleans -> Number) -> Booleans -> Number
forall a b. (a -> b) -> a -> b
$ Booleans
zs Booleans -> Booleans -> Booleans
forall a. [a] -> [a] -> [a]
++ [Boolean
carry]

add_with_carry :: (MonadSAT m) => Boolean 
               -> Booleans -> Booleans
               -> m ( Booleans, Boolean )
add_with_carry :: forall (m :: * -> *).
MonadSAT m =>
Boolean -> Booleans -> Booleans -> m (Booleans, Boolean)
add_with_carry Boolean
cin [] [] = (Booleans, Boolean) -> m (Booleans, Boolean)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ( [], Boolean
cin )
add_with_carry Boolean
cin (Boolean
x:Booleans
xs) [] = do
    (Boolean
z, Boolean
c) <- Boolean -> Boolean -> m (Boolean, Boolean)
forall (m :: * -> *).
MonadSAT m =>
Boolean -> Boolean -> m (Boolean, Boolean)
half_adder Boolean
cin Boolean
x
    ( Booleans
zs, Boolean
cout ) <- Boolean -> Booleans -> Booleans -> m (Booleans, Boolean)
forall (m :: * -> *).
MonadSAT m =>
Boolean -> Booleans -> Booleans -> m (Booleans, Boolean)
add_with_carry Boolean
c Booleans
xs []
    (Booleans, Boolean) -> m (Booleans, Boolean)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ( Boolean
z Boolean -> Booleans -> Booleans
forall a. a -> [a] -> [a]
: Booleans
zs, Boolean
cout )
add_with_carry Boolean
cin [] (Boolean
y:Booleans
ys) = do
    Boolean -> Booleans -> Booleans -> m (Booleans, Boolean)
forall (m :: * -> *).
MonadSAT m =>
Boolean -> Booleans -> Booleans -> m (Booleans, Boolean)
add_with_carry Boolean
cin (Boolean
yBoolean -> Booleans -> Booleans
forall a. a -> [a] -> [a]
:Booleans
ys) []
add_with_carry Boolean
cin (Boolean
x:Booleans
xs ) (Boolean
y:Booleans
ys) = do
    (Boolean
z, Boolean
c) <- Boolean -> Boolean -> Boolean -> m (Boolean, Boolean)
forall (m :: * -> *).
MonadSAT m =>
Boolean -> Boolean -> Boolean -> m (Boolean, Boolean)
full_adder Boolean
cin Boolean
x Boolean
y
    ( Booleans
zs, Boolean
cout ) <- Boolean -> Booleans -> Booleans -> m (Booleans, Boolean)
forall (m :: * -> *).
MonadSAT m =>
Boolean -> Booleans -> Booleans -> m (Booleans, Boolean)
add_with_carry Boolean
c Booleans
xs Booleans
ys
    (Booleans, Boolean) -> m (Booleans, Boolean)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ( Boolean
z Boolean -> Booleans -> Booleans
forall a. a -> [a] -> [a]
: Booleans
zs, Boolean
cout )

times :: (MonadSAT m) => Number -> Number -> m Number
times :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
times = -- plain_times 
      Maybe Int -> Number -> Number -> m Number
forall (m :: * -> *).
MonadSAT m =>
Maybe Int -> Number -> Number -> m Number
T.times Maybe Int
forall a. Maybe a
Nothing

dot_product :: (MonadSAT m) 
             => [ Number ] -> [ Number ] -> m Number
dot_product :: forall (m :: * -> *).
MonadSAT m =>
[Number] -> [Number] -> m Number
dot_product = Maybe Int -> [Number] -> [Number] -> m Number
forall (m :: * -> *).
MonadSAT m =>
Maybe Int -> [Number] -> [Number] -> m Number
T.dot_product Maybe Int
forall a. Maybe a
Nothing

plain_times :: (MonadSAT m) => Number -> Number -> m Number
plain_times :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
plain_times Number
a Number
b | [] <- Number -> Booleans
bits Number
a = Number -> m Number
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Number
a
plain_times Number
a Number
b | [] <- Number -> Booleans
bits Number
b = Number -> m Number
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Number
b
plain_times Number
a Number
b | [Boolean
x] <- Number -> Booleans
bits Number
a = Boolean -> Number -> m Number
forall (m :: * -> *). MonadSAT m => Boolean -> Number -> m Number
times1 Boolean
x Number
b
plain_times Number
a Number
b | [Boolean
y] <- Number -> Booleans
bits Number
b = Boolean -> Number -> m Number
forall (m :: * -> *). MonadSAT m => Boolean -> Number -> m Number
times1 Boolean
y Number
a
plain_times Number
a Number
b | Boolean
x:Booleans
xs <- Number -> Booleans
bits Number
a = do
    Number
xys  <- Boolean -> Number -> m Number
forall (m :: * -> *). MonadSAT m => Boolean -> Number -> m Number
times1 Boolean
x Number
b
    Number
xsys <- Number -> Number -> m Number
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
plain_times (Booleans -> Number
make Booleans
xs) Number
b
    Number
zs <- Number -> m Number
forall (m :: * -> *). MonadSAT m => Number -> m Number
shift Number
xsys
    Number -> Number -> m Number
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
add Number
xys Number
zs

-- | multiply by 2
shift :: (MonadSAT m) => Number -> m Number
shift :: forall (m :: * -> *). MonadSAT m => Number -> m Number
shift Number
a = do
    Boolean
false <- Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
Satchmo.Boolean.constant Bool
False 
    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
$ Booleans -> Number
make (Booleans -> Number) -> Booleans -> Number
forall a b. (a -> b) -> a -> b
$ Boolean
false Boolean -> Booleans -> Booleans
forall a. a -> [a] -> [a]
: Number -> Booleans
bits Number
a

times1 :: (MonadSAT m) => Boolean -> Number -> m Number
times1 :: forall (m :: * -> *). MonadSAT m => Boolean -> Number -> m Number
times1 Boolean
x Number
b = do
    Booleans
zs <- (Boolean -> m Boolean) -> Booleans -> m Booleans
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ( \ Boolean
y -> Booleans -> m Boolean
forall (m :: * -> *). MonadSAT m => Booleans -> m Boolean
and [Boolean
x,Boolean
y] ) (Booleans -> m Booleans) -> Booleans -> m Booleans
forall a b. (a -> b) -> a -> b
$ Number -> Booleans
bits Number
b
    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
$ Booleans -> Number
make Booleans
zs