```{-# language MultiParamTypeClasses #-}

module Satchmo.Binary.Data

( Number, bits, make
, width, number, constant
, equals, iszero
)

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
{ bits :: [ Boolean ] -- lsb first
, decode :: C.Decoder Integer
}

instance C.Decode Number Integer where
decode = decode

width :: Number -> Int
width n = length \$ bits n

-- | declare a number variable (bit width)
number :: Int -> SAT Number
number w = do
xs <- sequence \$ replicate w boolean
return \$ make xs

make :: [ Boolean ] -> Number
make xs = Number
{ bits = xs
, decode = do ys <- mapM C.decode xs ; return \$ fromBinary ys
}

fromBinary :: [ Bool ] -> Integer
fromBinary xs = foldr ( \ x y -> 2*y + if x then 1 else 0 ) 0 xs

toBinary :: Integer -> [ Bool ]
toBinary 0 = []
toBinary n  =
let (d,m) = divMod n 2
in  toEnum ( fromIntegral m ) : toBinary d

-- | declare a number constant
constant :: Integer -> SAT Number
constant n = do
xs <- mapM B.constant \$ toBinary n
return \$ make xs

iszero :: Number -> SAT Boolean
iszero a = equals a \$ make []

equals :: Number -> Number -> SAT Boolean
equals a b = do
equals' ( bits a ) ( bits b )

equals' :: Booleans -> Booleans -> SAT Boolean
equals' [] [] = B.constant True
equals' (x:xs) (y:ys) = do
z <- xor [x, y]
rest <- equals' xs ys
and [ not z, rest ]
equals' xs [] = and \$ map not xs
equals' [] ys = and \$ map not ys

```