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 = [Boolean] -> m Boolean
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 = [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [Number -> Boolean
msb Number
a, Boolean -> Boolean
not (Boolean -> Boolean) -> Boolean -> Boolean
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 = Number -> Number -> m Boolean
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 = Number -> Number -> m Boolean
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
equals

lt :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
lt Number
a Number
b = m Boolean -> m Boolean -> m Boolean -> m Boolean
forall (m :: * -> *).
MonadSAT m =>
m Boolean -> m Boolean -> m Boolean -> m Boolean
ifThenElseM ( Number -> Number -> m Boolean
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
sameSign Number
a Number
b )
                     ( Number -> Number -> m Boolean
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
B.lt (Number -> Number
toUnsigned Number
a) (Number -> Number
toUnsigned Number
b) )
                     ( Number -> Number -> m Boolean
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 = m Boolean -> m Boolean -> m Boolean -> m Boolean
forall (m :: * -> *).
MonadSAT m =>
m Boolean -> m Boolean -> m Boolean -> m Boolean
ifThenElseM ( Number -> Number -> m Boolean
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
sameSign Number
a Number
b )
                     ( Number -> Number -> m Boolean
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
B.le (Number -> Number
toUnsigned Number
a) (Number -> Number
toUnsigned Number
b) )
                     ( Number -> Number -> m Boolean
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
negativePositive Number
a Number
b )

ge :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
ge = (Number -> Number -> m Boolean) -> Number -> Number -> m Boolean
forall a b c. (a -> b -> c) -> b -> a -> c
flip Number -> Number -> m Boolean
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
le
gt :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
gt = (Number -> Number -> m Boolean) -> Number -> Number -> m Boolean
forall a b c. (a -> b -> c) -> b -> a -> c
flip Number -> Number -> m Boolean
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 <- [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or ([Boolean] -> m Boolean) -> [Boolean] -> m Boolean
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a
  [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [Boolean -> Boolean
not (Boolean -> Boolean) -> Boolean -> Boolean
forall a b. (a -> b) -> a -> b
$ Number -> Boolean
msb Number
a, Boolean
one]

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

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