{-# language MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}

module Satchmo.Integer.Data 

( Number, make, number
, constant, decode
, bits, width, sign
)

where

import Prelude hiding ( and, or, not, (&&), (||) )
import qualified Prelude 

import qualified Satchmo.Code as C

import Satchmo.Boolean hiding ( constant )
import qualified  Satchmo.Boolean as B

import Satchmo.Counting
import Control.Monad

data Number = Number 
            { Number -> [Boolean]
bits :: [ Boolean ] -- ^ lsb first,
	         -- using two's complement
            }

instance (Monad m, C.Decode m Boolean Bool) => C.Decode m Number Integer where
    decode :: Number -> m Integer
decode Number
n = do [Bool]
ys <- (Boolean -> m Bool) -> [Boolean] -> m [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Boolean -> m Bool
forall (m :: * -> *) c a. Decode m c a => c -> m a
C.decode (Number -> [Boolean]
bits Number
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
$ [Bool] -> Integer
fromBinary [Bool]
ys

width :: Number -> Int
width :: Number -> Int
width Number
n = [Boolean] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Boolean] -> Int) -> [Boolean] -> Int
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
n

sign :: Number -> Boolean
sign :: Number -> Boolean
sign Number
n = case Number -> [Boolean]
bits Number
n of
  [] -> [Char] -> Boolean
forall a. HasCallStack => [Char] -> a
error [Char]
"Satchmo.Integer.Data:sign no bits"
  [Boolean]
bs -> [Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
last [Boolean]
bs

-- | declare a number variable (bit width)
number :: MonadSAT m => Int -> m Number
number :: forall (m :: * -> *). MonadSAT m => Int -> m Number
number Int
w = do
    [Boolean]
xs <- [m Boolean] -> m [Boolean]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([m Boolean] -> m [Boolean]) -> [m Boolean] -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ Int -> m Boolean -> [m Boolean]
forall a. Int -> a -> [a]
replicate Int
w m Boolean
forall (m :: * -> *). MonadSAT m => m Boolean
boolean
    Number -> m Number
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number -> m Number) -> Number -> m Number
forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
xs

make :: [ Boolean ] -> Number
make :: [Boolean] -> Number
make [Boolean]
xs = Number
           { bits :: [Boolean]
bits = [Boolean]
xs
           }

fromBinary :: [ Bool ] -> Integer
fromBinary :: [Bool] -> Integer
fromBinary [Bool]
xs = (Bool -> Integer -> Integer) -> Integer -> [Bool] -> Integer
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ Bool
x Integer
y -> Integer
2Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
y Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ if Bool
x then Integer
1 else Integer
0 ) Integer
0 [Bool]
xs

toBinary :: Integer -> [ Bool ]
toBinary :: Integer -> [Bool]
toBinary Integer
0 = []
toBinary Integer
n  = 
    let (Integer
d,Integer
m) = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
n Integer
2
    in  Int -> Bool
forall a. Enum a => Int -> a
toEnum ( Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
m ) Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: Integer -> [Bool]
toBinary Integer
d

-- | declare a number constant 
constant :: MonadSAT m 
	 => Int -- ^ bit width
	 -> Integer -- ^ value
	 -> m Number
constant :: forall (m :: * -> *). MonadSAT m => Int -> Integer -> m Number
constant Int
w Integer
n = do
    [Boolean]
xs <- if Integer
0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
n Bool -> Bool -> Bool
Prelude.&& Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
          then (Bool -> m Boolean) -> [Bool] -> m [Boolean]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant ([Bool] -> m [Boolean]) -> [Bool] -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ Integer -> [Bool]
toBinary Integer
n
	  else if Integer -> Integer
forall a. Num a => a -> a
negate ( Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
n Bool -> Bool -> Bool
Prelude.&& Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
	  then (Bool -> m Boolean) -> [Bool] -> m [Boolean]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant ([Bool] -> m [Boolean]) -> [Bool] -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ Integer -> [Bool]
toBinary (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
2Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
w)
	  else [Char] -> m [Boolean]
forall a. HasCallStack => [Char] -> a
error [Char]
"Satchmo.Integer.Data.constant"
    Boolean
z <- Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
False
    Number -> m Number
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number -> m Number) -> Number -> m Number
forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make ([Boolean] -> Number) -> [Boolean] -> Number
forall a b. (a -> b) -> a -> b
$ Int -> [Boolean] -> [Boolean]
forall a. Int -> [a] -> [a]
take Int
w ([Boolean] -> [Boolean]) -> [Boolean] -> [Boolean]
forall a b. (a -> b) -> a -> b
$ [Boolean]
xs [Boolean] -> [Boolean] -> [Boolean]
forall a. [a] -> [a] -> [a]
++ Boolean -> [Boolean]
forall a. a -> [a]
repeat Boolean
z

decode :: b -> Number -> m Integer
decode b
w Number
n = do
  [Bool]
bs <- [Boolean] -> (Boolean -> m Bool) -> m [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Number -> [Boolean]
bits Number
n) Boolean -> m Bool
forall (m :: * -> *) c a. Decode m c a => c -> m a
C.decode
  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
$ [Bool] -> Integer
fromBinary [Bool]
bs
         Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- if [Bool] -> Bool
forall a. HasCallStack => [a] -> a
last [Bool]
bs then Integer
2Integer -> b -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^b
w else Integer
0