satchmo-1.2: Satchmo/Binary/Op/Common.hs

module Satchmo.Binary.Op.Common

( iszero
, equals
, full_adder, half_adder
)

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.Binary.Data

import Satchmo.Counting

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

full_adder :: Boolean -> Boolean -> Boolean
           -> SAT ( Boolean, Boolean )
full_adder a b c = do
    let s x y z = sum $ map fromEnum [x,y,z]
    r <- fun3 ( \ x y z -> odd $ s x y z ) a b c
    d <- fun3 ( \ x y z -> 1   < s x y z ) a b c
    return ( r, d )

half_adder :: Boolean -> Boolean 
           -> SAT ( Boolean, Boolean )
half_adder a b = do
    let s x y = sum $ map fromEnum [x,y]
    r <- fun2 ( \ x y -> odd $ s x y ) a b
    d <- fun2 ( \ x y -> 1   < s x y ) a b
    return ( r, d )