module Satchmo.BinaryTwosComplement.Op.Common
    (equals, eq, lt, le, ge, gt, positive, negative, nonNegative)
where

import Prelude hiding (and,or,not)
import Satchmo.MonadSAT (MonadSAT)
import Satchmo.BinaryTwosComplement.Data (Number,toUnsigned,msb,bits)
import Satchmo.Boolean (Boolean,and,or,not,ifThenElseM)
import qualified Satchmo.Boolean as Boolean
import qualified Satchmo.Binary.Op.Common as B

sameSign, negativePositive :: MonadSAT m => Number -> Number -> m Boolean
sameSign :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
sameSign Number
a Number
b = forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
Boolean.equals [Number -> Boolean
msb Number
a, Number -> Boolean
msb Number
b]
negativePositive :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
negativePositive Number
a Number
b = forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [Number -> Boolean
msb Number
a, Boolean -> Boolean
not forall a b. (a -> b) -> a -> b
$ Number -> Boolean
msb Number
b]

equals,eq,lt,le,ge,gt :: MonadSAT m => Number -> Number -> m Boolean
equals :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
equals Number
a Number
b = forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
B.equals (Number -> Number
toUnsigned Number
a) (Number -> Number
toUnsigned Number
b)
eq :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
eq = forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
equals

lt :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
lt Number
a Number
b = forall (m :: * -> *).
MonadSAT m =>
m Boolean -> m Boolean -> m Boolean -> m Boolean
ifThenElseM ( forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
sameSign Number
a Number
b )
                     ( forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
B.lt (Number -> Number
toUnsigned Number
a) (Number -> Number
toUnsigned Number
b) )
                     ( forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
negativePositive Number
a Number
b )

le :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
le Number
a Number
b = forall (m :: * -> *).
MonadSAT m =>
m Boolean -> m Boolean -> m Boolean -> m Boolean
ifThenElseM ( forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
sameSign Number
a Number
b )
                     ( forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
B.le (Number -> Number
toUnsigned Number
a) (Number -> Number
toUnsigned Number
b) )
                     ( forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
negativePositive Number
a Number
b )

ge :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
ge = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
le
gt :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
gt = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
lt

positive,negative,nonNegative :: MonadSAT m => Number -> m Boolean
positive :: forall (m :: * -> *). MonadSAT m => Number -> m Boolean
positive Number
a = do
  Boolean
one <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a
  forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [Boolean -> Boolean
not forall a b. (a -> b) -> a -> b
$ Number -> Boolean
msb Number
a, Boolean
one]

negative :: forall (m :: * -> *). MonadSAT m => Number -> m Boolean
negative = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Number -> Boolean
msb

nonNegative :: forall (m :: * -> *). MonadSAT m => Number -> m Boolean
nonNegative = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Boolean -> Boolean
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Number -> Boolean
msb