{-# 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 }