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