{-# 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 ] 
            -- ^ contents is [ 1 .. 1 0 .. 0 ]
            -- number of 1 is value of number  
            }  
            
instance (Monad m, C.Decode m Boolean Bool) => C.Decode m Number Int where            
    decode :: Number -> m Int
decode Number
n = do
        [Bool]
bs <- [Boolean] -> (Boolean -> m Bool) -> m [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( Number -> [Boolean]
bits Number
n ) Boolean -> m Bool
forall (m :: * -> *) c a. Decode m c a => c -> m a
C.decode
        Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> m Int) -> Int -> m Int
forall a b. (a -> b) -> a -> b
$ [Bool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Bool] -> Int) -> [Bool] -> Int
forall a b. (a -> b) -> a -> b
$ (Bool -> Bool) -> [Bool] -> [Bool]
forall a. (a -> Bool) -> [a] -> [a]
filter Bool -> Bool
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 <- [Boolean] -> (Boolean -> m Bool) -> m [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( Number -> [Boolean]
bits Number
n ) Boolean -> m Bool
forall (m :: * -> *) c a. Decode m c a => c -> m a
C.decode
        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
$ Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ [Bool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Bool] -> Int) -> [Bool] -> Int
forall a b. (a -> b) -> a -> b
$ (Bool -> Bool) -> [Bool] -> [Bool]
forall a. (a -> Bool) -> [a] -> [a]
filter Bool -> Bool
forall a. a -> a
id [Bool]
bs

width :: Number -> Int
width :: Number -> Int
width Number
n = [Boolean] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Boolean] -> Int) -> [Boolean] -> Int
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
n

-- | declare a number with range (0, w)
number :: MonadSAT m => Int -> m  Number 
number :: forall (m :: * -> *). MonadSAT m => Int -> m Number
number Int
w = 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
w m Boolean
forall (m :: * -> *). MonadSAT m => m Boolean
boolean
    [(Boolean, Boolean)] -> ((Boolean, Boolean) -> m ()) -> m [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( [Boolean] -> [Boolean] -> [(Boolean, Boolean)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Boolean]
xs ([Boolean] -> [(Boolean, Boolean)])
-> [Boolean] -> [(Boolean, Boolean)]
forall a b. (a -> b) -> a -> b
$ [Boolean] -> [Boolean]
forall a. HasCallStack => [a] -> [a]
tail [Boolean]
xs ) (((Boolean, Boolean) -> m ()) -> m [()])
-> ((Boolean, Boolean) -> m ()) -> m [()]
forall a b. (a -> b) -> a -> b
$ \ (Boolean
p, Boolean
q) ->
        [Boolean] -> m ()
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [ Boolean
p, Boolean -> Boolean
not Boolean
q ]
    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
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 <- [Integer] -> (Integer -> m Boolean) -> m [Boolean]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ Integer
1 .. Integer
k ] ((Integer -> m Boolean) -> m [Boolean])
-> (Integer -> m Boolean) -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ \ Integer
i -> Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
True
    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
make [Boolean]
xs