{-# 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 <- a -> m Integer
forall (m :: * -> *) c a. Decode m c a => c -> m a
decode (a -> m Integer) -> a -> m Integer
forall a b. (a -> b) -> a -> b
$ Number a -> a
forall a. Number a -> a
top Number a
n
        Integer
b <- a -> m Integer
forall (m :: * -> *) c a. Decode m c a => c -> m a
decode (a -> m Integer) -> a -> m Integer
forall a b. (a -> b) -> a -> b
$ Number a -> a
forall a. Number a -> a
bot Number a
n
        Integer -> m Integer
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> m Integer) -> Integer -> m Integer
forall a b. (a -> b) -> a -> b
$ Integer
t Integer -> Integer -> Integer
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 then do
            a
t <- Integer -> m a
forall a (m :: * -> *). (Constant a, MonadSAT m) => Integer -> m a
forall (m :: * -> *). MonadSAT m => Integer -> m a
constant Integer
n
            a
b <- Integer -> m a
forall a (m :: * -> *). (Constant a, MonadSAT m) => Integer -> m a
forall (m :: * -> *). MonadSAT m => Integer -> m a
constant Integer
0
            Number a -> m (Number a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number a -> m (Number a)) -> Number a -> m (Number a)
forall a b. (a -> b) -> a -> b
$ Difference { top :: a
top = a
t, bot :: a
bot = a
b }
        else do    
            a
t <- Integer -> m a
forall a (m :: * -> *). (Constant a, MonadSAT m) => Integer -> m a
forall (m :: * -> *). MonadSAT m => Integer -> m a
constant Integer
0
            a
b <- Integer -> m a
forall a (m :: * -> *). (Constant a, MonadSAT m) => Integer -> m a
forall (m :: * -> *). MonadSAT m => Integer -> m a
constant (Integer -> m a) -> Integer -> m a
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Num a => a -> a
negate Integer
n
            Number a -> m (Number a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number a -> m (Number a)) -> Number a -> m (Number a)
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 <- Int -> m a
forall a (m :: * -> *). (Create a, MonadSAT m) => Int -> m a
forall (m :: * -> *). MonadSAT m => Int -> m a
create Int
bits
        a
b <- Int -> m a
forall a (m :: * -> *). (Create a, MonadSAT m) => Int -> m a
forall (m :: * -> *). MonadSAT m => Int -> m a
create Int
bits
        Number a -> m (Number a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number a -> m (Number a)) -> Number a -> m (Number a)
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 <- a -> a -> m a
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => a -> a -> m a
plus ( Number a -> a
forall a. Number a -> a
top Number a
a ) ( Number a -> a
forall a. Number a -> a
bot Number a
b )
        a
b <- a -> a -> m a
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => a -> a -> m a
plus ( Number a -> a
forall a. Number a -> a
bot Number a
a ) ( Number a -> a
forall a. Number a -> a
top Number a
b )
        a -> a -> m Boolean
forall a (m :: * -> *).
(Numeric a, MonadSAT m) =>
a -> a -> m Boolean
forall (m :: * -> *). 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 <- a -> a -> m a
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => a -> a -> m a
plus ( Number a -> a
forall a. Number a -> a
top Number a
a ) ( Number a -> a
forall a. Number a -> a
bot Number a
b )
        a
b <- a -> a -> m a
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => a -> a -> m a
plus ( Number a -> a
forall a. Number a -> a
bot Number a
a ) ( Number a -> a
forall a. Number a -> a
top Number a
b )
        a -> a -> m Boolean
forall a (m :: * -> *).
(Numeric a, MonadSAT m) =>
a -> a -> m Boolean
forall (m :: * -> *). 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 <- a -> a -> m a
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => a -> a -> m a
plus ( Number a -> a
forall a. Number a -> a
top Number a
a ) ( Number a -> a
forall a. Number a -> a
top Number a
b )
        a
b <- a -> a -> m a
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => a -> a -> m a
plus ( Number a -> a
forall a. Number a -> a
bot Number a
a ) ( Number a -> a
forall a. Number a -> a
bot Number a
b )
        Number a -> m (Number a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number a -> m (Number a)) -> Number a -> m (Number a)
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 <- a -> a -> m a
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => a -> a -> m a
plus ( Number a -> a
forall a. Number a -> a
top Number a
a ) ( Number a -> a
forall a. Number a -> a
bot Number a
b )
        a
b <- a -> a -> m a
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => a -> a -> m a
plus ( Number a -> a
forall a. Number a -> a
bot Number a
a ) ( Number a -> a
forall a. Number a -> a
top Number a
b )
        Number a -> m (Number a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number a -> m (Number a)) -> Number a -> m (Number a)
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 <- a -> a -> m a
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => a -> a -> m a
times ( Number a -> a
forall a. Number a -> a
top Number a
a ) ( Number a -> a
forall a. Number a -> a
top Number a
b )
        a
bb <- a -> a -> m a
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => a -> a -> m a
times ( Number a -> a
forall a. Number a -> a
bot Number a
a ) ( Number a -> a
forall a. Number a -> a
bot Number a
b )
        a
t  <- a -> a -> m a
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => a -> a -> m a
plus a
tt a
bb
        a
tb <- a -> a -> m a
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => a -> a -> m a
times ( Number a -> a
forall a. Number a -> a
top Number a
a ) ( Number a -> a
forall a. Number a -> a
bot Number a
b )
        a
bt <- a -> a -> m a
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => a -> a -> m a
times ( Number a -> a
forall a. Number a -> a
bot Number a
a ) ( Number a -> a
forall a. Number a -> a
top Number a
b )
        a
b  <- a -> a -> m a
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => a -> a -> m a
plus a
tb a
bt
        Number a -> m (Number a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number a -> m (Number a)) -> Number a -> m (Number a)
forall a b. (a -> b) -> a -> b
$ Difference { top :: a
top = a
t, bot :: a
bot = a
b }