{-# language MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-} module Satchmo.Integer.Difference where import Satchmo.Code import Satchmo.Numeric data Number a = Difference { forall a. Number a -> a top :: a, forall a. Number a -> a bot :: a } instance Decode m a Integer => Decode m ( Number a ) Integer where decode :: Number a -> m Integer decode Number a n = do Integer t <- forall (m :: * -> *) c a. Decode m c a => c -> m a decode forall a b. (a -> b) -> a -> b $ forall a. Number a -> a top Number a n Integer b <- forall (m :: * -> *) c a. Decode m c a => c -> m a decode forall a b. (a -> b) -> a -> b $ forall a. Number a -> a bot Number a n forall (m :: * -> *) a. Monad m => a -> m a return forall a b. (a -> b) -> a -> b $ Integer t forall a. Num a => a -> a -> a - Integer b instance Constant a => Constant ( Number a ) where constant :: forall (m :: * -> *). MonadSAT m => Integer -> m (Number a) constant Integer n = if Integer n forall a. Ord a => a -> a -> Bool >= Integer 0 then do a t <- forall a (m :: * -> *). (Constant a, MonadSAT m) => Integer -> m a constant Integer n a b <- forall a (m :: * -> *). (Constant a, MonadSAT m) => Integer -> m a constant Integer 0 forall (m :: * -> *) a. Monad m => a -> m a return forall a b. (a -> b) -> a -> b $ Difference { top :: a top = a t, bot :: a bot = a b } else do a t <- forall a (m :: * -> *). (Constant a, MonadSAT m) => Integer -> m a constant Integer 0 a b <- forall a (m :: * -> *). (Constant a, MonadSAT m) => Integer -> m a constant forall a b. (a -> b) -> a -> b $ forall a. Num a => a -> a negate Integer n forall (m :: * -> *) a. Monad m => a -> m a return forall a b. (a -> b) -> a -> b $ Difference { top :: a top = a t, bot :: a bot = a b } instance Create a => Create ( Number a ) where create :: forall (m :: * -> *). MonadSAT m => Int -> m (Number a) create Int bits = do a t <- forall a (m :: * -> *). (Create a, MonadSAT m) => Int -> m a create Int bits a b <- forall a (m :: * -> *). (Create a, MonadSAT m) => Int -> m a create Int bits forall (m :: * -> *) a. Monad m => a -> m a return forall a b. (a -> b) -> a -> b $ Difference { top :: a top = a t, bot :: a bot = a b } instance Numeric a => Numeric ( Number a ) where equal :: forall (m :: * -> *). MonadSAT m => Number a -> Number a -> m Boolean equal Number a a Number a b = do a t <- forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a plus ( forall a. Number a -> a top Number a a ) ( forall a. Number a -> a bot Number a b ) a b <- forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a plus ( forall a. Number a -> a bot Number a a ) ( forall a. Number a -> a top Number a b ) forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m Boolean equal a t a b greater_equal :: forall (m :: * -> *). MonadSAT m => Number a -> Number a -> m Boolean greater_equal Number a a Number a b = do a t <- forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a plus ( forall a. Number a -> a top Number a a ) ( forall a. Number a -> a bot Number a b ) a b <- forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a plus ( forall a. Number a -> a bot Number a a ) ( forall a. Number a -> a top Number a b ) forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m Boolean greater_equal a t a b plus :: forall (m :: * -> *). MonadSAT m => Number a -> Number a -> m (Number a) plus Number a a Number a b = do a t <- forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a plus ( forall a. Number a -> a top Number a a ) ( forall a. Number a -> a top Number a b ) a b <- forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a plus ( forall a. Number a -> a bot Number a a ) ( forall a. Number a -> a bot Number a b ) forall (m :: * -> *) a. Monad m => a -> m a return forall a b. (a -> b) -> a -> b $ Difference { top :: a top = a t, bot :: a bot = a b } minus :: forall (m :: * -> *). MonadSAT m => Number a -> Number a -> m (Number a) minus Number a a Number a b = do a t <- forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a plus ( forall a. Number a -> a top Number a a ) ( forall a. Number a -> a bot Number a b ) a b <- forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a plus ( forall a. Number a -> a bot Number a a ) ( forall a. Number a -> a top Number a b ) forall (m :: * -> *) a. Monad m => a -> m a return forall a b. (a -> b) -> a -> b $ Difference { top :: a top = a t, bot :: a bot = a b } times :: forall (m :: * -> *). MonadSAT m => Number a -> Number a -> m (Number a) times Number a a Number a b = do a tt <- forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a times ( forall a. Number a -> a top Number a a ) ( forall a. Number a -> a top Number a b ) a bb <- forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a times ( forall a. Number a -> a bot Number a a ) ( forall a. Number a -> a bot Number a b ) a t <- forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a plus a tt a bb a tb <- forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a times ( forall a. Number a -> a top Number a a ) ( forall a. Number a -> a bot Number a b ) a bt <- forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a times ( forall a. Number a -> a bot Number a a ) ( forall a. Number a -> a top Number a b ) a b <- forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a plus a tb a bt forall (m :: * -> *) a. Monad m => a -> m a return forall a b. (a -> b) -> a -> b $ Difference { top :: a top = a t, bot :: a bot = a b }