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

module Satchmo.BinaryTwosComplement.Data
    ( Number, bits, fromBooleans, number, toUnsigned, fromUnsigned
    , width, isNull, msb, constant, constantWidth)

where

import Control.Applicative ((<$>))
import Satchmo.MonadSAT (MonadSAT)
import Satchmo.Boolean (Boolean)
import qualified Satchmo.Boolean as Boolean
import qualified Satchmo.Code as C
import qualified Satchmo.Binary.Data as B 

import Debug.Trace

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]
bs <- forall (m :: * -> *) c a. Decode m c a => c -> m a
C.decode forall a b. (a -> b) -> a -> b
$ 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]
bs

-- | Make a number from its binary representation
fromBooleans :: [Boolean] -> Number
fromBooleans :: [Boolean] -> Number
fromBooleans [Boolean]
xs = [Boolean] -> Number
Number [Boolean]
xs


-- | Convert to unsigned number (see "Satchmo.Binary.Op.Flexible")
toUnsigned :: Number -> B.Number
toUnsigned :: Number -> Number
toUnsigned = [Boolean] -> Number
B.make forall b c a. (b -> c) -> (a -> b) -> a -> c
. Number -> [Boolean]
bits

-- | Convert from unsigned number (see "Satchmo.Binary.Op.Flexible").
-- The result is interpreted as a positive or negative number,
-- depending on its most significant bit.
fromUnsigned :: B.Number -> Number
fromUnsigned :: Number -> Number
fromUnsigned = [Boolean] -> Number
fromBooleans forall b c a. (b -> c) -> (a -> b) -> a -> c
. Number -> [Boolean]
B.bits

-- | Get bit width
width :: Number -> Int
width :: Number -> Int
width = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. Number -> [Boolean]
bits

-- | Most significant bit
msb :: Number -> Boolean
msb :: Number -> Boolean
msb Number
n = if Number -> Bool
isNull Number
n then forall a. HasCallStack => [Char] -> a
error [Char]
"Satchmo.BinaryTwosComplement.Data.msb"
        else Number -> [Boolean]
bits Number
n forall a. [a] -> Int -> a
!! (Number -> Int
width Number
n forall a. Num a => a -> a -> a
- Int
1)

-- | @isNull n == True@ if @width n == 0@
isNull :: Number -> Bool
isNull :: Number -> Bool
isNull Number
n = Number -> Int
width Number
n forall a. Eq a => a -> a -> Bool
== Int
0

-- | Get a number variable of given bit width
number :: MonadSAT m => Int -> m Number
number :: forall (m :: * -> *). MonadSAT m => Int -> m Number
number Int
width = 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
width forall (m :: * -> *). MonadSAT m => m Boolean
Boolean.boolean
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
fromBooleans [Boolean]
xs

fromBinary :: [Bool] -> Integer
fromBinary :: [Bool] -> Integer
fromBinary [Bool]
xs =
    let w :: Int
w = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Bool]
xs
        ([Bool]
bs, [Bool
msb]) = forall a. Int -> [a] -> ([a], [a])
splitAt (Int
w forall a. Num a => a -> a -> a
- Int
1) [Bool]
xs
    in                    
      if Bool
msb then -(Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
wforall a. Num a => a -> a -> a
-Int
1)) forall a. Num a => a -> a -> a
+ ([Bool] -> Integer
B.fromBinary [Bool]
bs)
      else [Bool] -> Integer
B.fromBinary [Bool]
bs

toBinary :: Maybe Int -- ^ Minimal bit width
         -> Integer -> [Bool]
toBinary :: Maybe Int -> Integer -> [Bool]
toBinary Maybe Int
width Integer
i = 
    let i' :: Integer
i' = forall a. Num a => a -> a
abs Integer
i
        binary :: [Bool]
binary = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Integer -> [Bool]
B.toBinary Integer
i') (Int -> Integer -> [Bool]
B.toBinaryWidth forall a b c. (a -> b -> c) -> b -> a -> c
`flip` Integer
i') Maybe Int
width
        flipBits :: (Bool, [Bool]) -> Bool -> (Bool, [Bool])
flipBits (Bool
firstOne,[Bool]
result) Bool
x =
            if Bool
firstOne then (Bool
True, [Bool]
result forall a. [a] -> [a] -> [a]
++ [Bool -> Bool
not Bool
x]) 
            else (Bool
x, [Bool]
result forall a. [a] -> [a] -> [a]
++ [Bool
x])
    in
      if Integer
i forall a. Eq a => a -> a -> Bool
== Integer
0 then
          forall a. Int -> a -> [a]
replicate (forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
1 forall a. a -> a
id Maybe Int
width) Bool
False
      else if Integer
i forall a. Ord a => a -> a -> Bool
< Integer
0 then 
               let flipped :: [Bool]
flipped = forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Bool, [Bool]) -> Bool -> (Bool, [Bool])
flipBits (Bool
False,[]) [Bool]
binary
               in
                 if forall a. [a] -> a
last [Bool]
flipped forall a. Eq a => a -> a -> Bool
== Bool
False then [Bool]
flipped forall a. [a] -> [a] -> [a]
++ [Bool
True]
                 else [Bool]
flipped
           else 
               if Integer
i forall a. Ord a => a -> a -> Bool
> Integer
0 Bool -> Bool -> Bool
&& forall a. [a] -> a
last [Bool]
binary forall a. Eq a => a -> a -> Bool
== Bool
True then [Bool]
binary forall a. [a] -> [a] -> [a]
++ [Bool
False]
               else [Bool]
binary

-- | Get a number constant
constant :: MonadSAT m => Integer -> m Number
constant :: forall (m :: * -> *). MonadSAT m => Integer -> m Number
constant Integer
i = do
  [Boolean]
bs <- 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
Boolean.constant forall a b. (a -> b) -> a -> b
$ Maybe Int -> Integer -> [Bool]
toBinary forall a. Maybe a
Nothing Integer
i
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
fromBooleans [Boolean]
bs
    
-- | @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
i = do
  [Boolean]
bs <- 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
Boolean.constant forall a b. (a -> b) -> a -> b
$ Maybe Int -> Integer -> [Bool]
toBinary (forall a. a -> Maybe a
Just Int
width) Integer
i
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
fromBooleans [Boolean]
bs