{-# language MultiParamTypeClasses #-}

-- | operations with fixed bit width.
-- still they are non-overflowing:
-- if overflow occurs, the constraints are not satisfiable.
-- the bit width of the result of binary operations
-- is the max of the bit width of the inputs.

module Satchmo.Binary.Op.Fixed

( restricted
, add, times
, module Satchmo.Binary.Data
)

where

import Prelude hiding ( and, or, not )

import qualified Satchmo.Code as C

import Satchmo.Boolean
import Satchmo.Binary.Data
import qualified Satchmo.Binary.Op.Flexible as Flexible

import Satchmo.Counting

-- | give only lower k bits, upper bits must be zero,
-- (else unsatisfiable)
restricted :: Int -> Number -> SAT Number
restricted w a = do
    let ( low, high ) = splitAt w $ bits a
    sequence $ do x <- high ; return $ assert [ not x ]
    return $ make low

-- | result bit width is max of argument bit widths.
-- if overflow occurs, then formula is unsatisfiable.
add :: Number -> Number -> SAT Number
add a b = do
    false <- Satchmo.Boolean.constant False
    let w = max ( width a ) ( width b )
    zs <- add_with_carry w false ( bits a ) ( bits b )
    return $ make zs 

add_with_carry :: Int -> Boolean -> Booleans -> Booleans -> SAT Booleans
add_with_carry w c xxs yys = case ( xxs, yys ) of
    _ | w <= 0 -> do
        sequence_ $ do p <- c : xxs ++ yys ; return $ assert [ not p ]
        return []
    ( [] , [] ) -> return [ c ]
    ( [], y : ys) -> do
        r <- xor [ c, y ]
        d <- and [ c, y ]
        rest <- add_with_carry (w-1) d [] ys
        return $ r : rest
    ( x : xs, [] ) -> add_with_carry w c yys xxs
    (x : xs, y:ys) -> do
        r <- xor [c,x,y]
        d <- atleast 2 [c,x,y]
        rest <- add_with_carry (w-1) d xs ys
        return $ r : rest

-- | result bit width is at most max of argument bit widths.
-- if overflow occurs, then formula is unsatisfiable.
times :: Number -> Number -> SAT Number
times a b = do 
    let w = max ( width a ) ( width b ) 
    restricted_times w a b

restricted_times :: Int -> Number -> Number -> SAT Number
restricted_times w a b = case bits a of
    [] -> return $ make []
    _ | w <= 0 -> do
        monadic assert [ Flexible.iszero a, Flexible.iszero b ]
        return $ make []
    x : xs -> do 
        xys  <- Flexible.times1 x b
        xsys <- if null $ bits b 
                then return $ make [] 
                else do
                       zs <- restricted_times (w-1) b (make xs)
                       Flexible.shift zs
        s <- Flexible.add xys xsys
        restricted w s