Common.hs

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 a b = Boolean.equals [msb a, msb b]
negativePositive a b = and [msb a, not $ msb b]

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

lt a b = ifThenElseM ( sameSign a b )
                     ( B.lt (toUnsigned a) (toUnsigned b) )
                     ( negativePositive a b )

le a b = ifThenElseM ( sameSign a b )
                     ( B.le (toUnsigned a) (toUnsigned b) )
                     ( negativePositive a b )

ge = flip le
gt = flip lt

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

negative = return . msb

nonNegative = return . not . msb