{-# language MultiParamTypeClasses #-}
{-# language FlexibleInstances #-}
{-# language FlexibleContexts #-}
{-# language UndecidableInstances #-}
module Satchmo.Unary.Data
( Number, bits, make
, width, number, constant )
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 Control.Monad ( forM, when )
data Number = Number
{ Number -> [Boolean]
bits :: [ Boolean ]
}
instance (Monad m, C.Decode m Boolean Bool) => C.Decode m Number Int where
decode :: Number -> m Int
decode Number
n = do
[Bool]
bs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( Number -> [Boolean]
bits Number
n ) forall (m :: * -> *) c a. Decode m c a => c -> m a
C.decode
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter forall a. a -> a
id [Bool]
bs
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 (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( Number -> [Boolean]
bits Number
n ) forall (m :: * -> *) c a. Decode m c a => c -> m a
C.decode
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter forall a. a -> a
id [Bool]
bs
width :: Number -> Int
width :: Number -> Int
width Number
n = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
n
number :: MonadSAT m => Int -> m Number
number :: forall (m :: * -> *). MonadSAT m => Int -> m Number
number Int
w = 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
w forall (m :: * -> *). MonadSAT m => m Boolean
boolean
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( forall a b. [a] -> [b] -> [(a, b)]
zip [Boolean]
xs forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
tail [Boolean]
xs ) forall a b. (a -> b) -> a -> b
$ \ (Boolean
p, Boolean
q) ->
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [ Boolean
p, Boolean -> Boolean
not Boolean
q ]
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
xs
make :: [ Boolean ] -> Number
make :: [Boolean] -> Number
make [Boolean]
xs = Number { bits :: [Boolean]
bits = [Boolean]
xs }
constant :: MonadSAT m => Integer -> m Number
constant :: forall (m :: * -> *). MonadSAT m => Integer -> m Number
constant Integer
k = do
[Boolean]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ Integer
1 .. Integer
k ] forall a b. (a -> b) -> a -> b
$ \ Integer
i -> forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
True
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
xs