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


module Satchmo.Binary.Data

( Number, bits, make
, width, number, constant, constantWidth
, fromBinary, toBinary, toBinaryWidth
)

where

import Prelude hiding ( and, or, not )

import qualified Satchmo.Code as C

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

-- import Satchmo.Counting

data Number = Number 
            { Number -> [Boolean]
bits :: [ Boolean ] -- lsb first
            }

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

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

-- | 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 <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall a b. (a -> b) -> a -> b
$ forall a. Int -> a -> [a]
replicate Int
w forall (m :: * -> *). MonadSAT m => m Boolean
boolean
    forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ Bool
x Integer
y -> Integer
2forall a. Num a => a -> a -> a
*Integer
y 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) = forall a. Integral a => a -> a -> (a, a)
divMod Integer
n Integer
2
    in  forall a. Enum a => Int -> a
toEnum ( forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
m ) forall a. a -> [a] -> [a]
: Integer -> [Bool]
toBinary Integer
d

-- | @toBinaryWidth w@ converts to binary using at least @w@ bits
toBinaryWidth :: Int -> Integer -> [Bool]
toBinaryWidth :: Int -> Integer -> [Bool]
toBinaryWidth Int
width Integer
n =
    let bs :: [Bool]
bs = Integer -> [Bool]
toBinary Integer
n
        leadingZeros :: Int
leadingZeros = forall a. Ord a => a -> a -> a
max Int
0 forall a b. (a -> b) -> a -> b
$ Int
width forall a. Num a => a -> a -> a
- (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Bool]
bs)
    in
      [Bool]
bs forall a. [a] -> [a] -> [a]
++ (forall a. Int -> a -> [a]
replicate Int
leadingZeros Bool
False)

-- | Declare a number constant 
constant :: MonadSAT m => Integer -> m Number
constant :: forall (m :: * -> *). MonadSAT m => Integer -> m Number
constant Integer
n = do
    [Boolean]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant forall a b. (a -> b) -> a -> b
$ Integer -> [Bool]
toBinary Integer
n
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
xs

-- | @constantWidth w@ declares a number constant using at least @w@ bits
constantWidth :: MonadSAT m => Int -> Integer -> m Number
constantWidth :: forall (m :: * -> *). MonadSAT m => Int -> Integer -> m Number
constantWidth Int
width Integer
n = do
  [Boolean]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant forall a b. (a -> b) -> a -> b
$ Int -> Integer -> [Bool]
toBinaryWidth Int
width Integer
n
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
xs