{-# 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 <- [Boolean] -> m [Bool]
forall (m :: * -> *) c a. Decode m c a => c -> m a
C.decode ([Boolean] -> m [Bool]) -> [Boolean] -> m [Bool]
forall a b. (a -> b) -> a -> b
$ 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]
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 ([Boolean] -> Number) -> (Number -> [Boolean]) -> Number -> Number
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 ([Boolean] -> Number) -> (Number -> [Boolean]) -> Number -> Number
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Number -> [Boolean]
B.bits

-- | Get bit width
width :: Number -> Int
width :: Number -> Int
width = [Boolean] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Boolean] -> Int) -> (Number -> [Boolean]) -> Number -> Int
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 [Char] -> Boolean
forall a. HasCallStack => [Char] -> a
error [Char]
"Satchmo.BinaryTwosComplement.Data.msb"
        else Number -> [Boolean]
bits Number
n [Boolean] -> Int -> Boolean
forall a. HasCallStack => [a] -> Int -> a
!! (Number -> Int
width Number
n Int -> Int -> Int
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 Int -> Int -> Bool
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 <- [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
width m Boolean
forall (m :: * -> *). MonadSAT m => m Boolean
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
fromBooleans [Boolean]
xs

fromBinary :: [Bool] -> Integer
fromBinary :: [Bool] -> Integer
fromBinary [Bool]
xs =
    let w :: Int
w = [Bool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Bool]
xs
        ([Bool]
bs, [Bool
msb]) = Int -> [Bool] -> ([Bool], [Bool])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Bool]
xs
    in                    
      if Bool
msb then -(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 -> Integer
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' = Integer -> Integer
forall a. Num a => a -> a
abs Integer
i
        binary :: [Bool]
binary = [Bool] -> (Int -> [Bool]) -> Maybe Int -> [Bool]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Integer -> [Bool]
B.toBinary Integer
i') (Int -> Integer -> [Bool]
B.toBinaryWidth (Int -> Integer -> [Bool]) -> Integer -> Int -> [Bool]
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 [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [Bool -> Bool
not Bool
x]) 
            else (Bool
x, [Bool]
result [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [Bool
x])
    in
      if Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then
          Int -> Bool -> [Bool]
forall a. Int -> a -> [a]
replicate (Int -> (Int -> Int) -> Maybe Int -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
1 Int -> Int
forall a. a -> a
id Maybe Int
width) Bool
False
      else if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 then 
               let flipped :: [Bool]
flipped = (Bool, [Bool]) -> [Bool]
forall a b. (a, b) -> b
snd ((Bool, [Bool]) -> [Bool]) -> (Bool, [Bool]) -> [Bool]
forall a b. (a -> b) -> a -> b
$ ((Bool, [Bool]) -> Bool -> (Bool, [Bool]))
-> (Bool, [Bool]) -> [Bool] -> (Bool, [Bool])
forall b a. (b -> a -> b) -> 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 [Bool] -> Bool
forall a. HasCallStack => [a] -> a
last [Bool]
flipped Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
False then [Bool]
flipped [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [Bool
True]
                 else [Bool]
flipped
           else 
               if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 Bool -> Bool -> Bool
&& [Bool] -> Bool
forall a. HasCallStack => [a] -> a
last [Bool]
binary Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
True then [Bool]
binary [Bool] -> [Bool] -> [Bool]
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 <- (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
Boolean.constant ([Bool] -> m [Boolean]) -> [Bool] -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ Maybe Int -> Integer -> [Bool]
toBinary Maybe Int
forall a. Maybe a
Nothing Integer
i
  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
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 <- (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
Boolean.constant ([Bool] -> m [Boolean]) -> [Bool] -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ Maybe Int -> Integer -> [Bool]
toBinary (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
width) Integer
i
  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
fromBooleans [Boolean]
bs