{-# language NoMonomorphismRestriction #-}
{-# language ScopedTypeVariables #-}

module Satchmo.Unary.Op.Common 
       
( iszero, equals
, lt, le, ge, eq, gt
, min, max
, minimum, maximum
, select, antiselect
, add_quadratic, add_by_odd_even_merge, add_by_bitonic_sort
)          
       
where


import Prelude 
  hiding ( and, or, not, compare, min, max, minimum, maximum )
import qualified Prelude

import qualified Satchmo.Code as C

import Satchmo.Unary.Data 
    (Number, make, bits, width, constant)

import Satchmo.Boolean (MonadSAT, Boolean, Booleans, fun2, fun3, and, or, not, xor, assert, boolean, monadic)
import qualified  Satchmo.Boolean as B

import Control.Monad ( forM, when, foldM, guard )
import qualified Data.Map as M
import Data.List ( transpose )

iszero :: Number -> m Boolean
iszero Number
n = case Number -> [Boolean]
bits Number
n of
    [] -> forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
True
    Boolean
x : [Boolean]
xs -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Boolean -> Boolean
not Boolean
x
    
extended :: MonadSAT m 
         => ( [(Boolean,Boolean)] -> m a )
         -> Number -> Number
         -> m a
extended :: forall (m :: * -> *) a.
MonadSAT m =>
([(Boolean, Boolean)] -> m a) -> Number -> Number -> m a
extended [(Boolean, Boolean)] -> m a
action Number
a Number
b = do
    Boolean
f <- forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
False
    let zipf :: [Boolean] -> [Boolean] -> [(Boolean, Boolean)]
zipf [] [] = []
        zipf (Boolean
x:[Boolean]
xs) [] = (Boolean
x,Boolean
f) forall a. a -> [a] -> [a]
: [Boolean] -> [Boolean] -> [(Boolean, Boolean)]
zipf [Boolean]
xs []
        zipf [] (Boolean
y:[Boolean]
ys) = (Boolean
f,Boolean
y) forall a. a -> [a] -> [a]
: [Boolean] -> [Boolean] -> [(Boolean, Boolean)]
zipf [] [Boolean]
ys
        zipf (Boolean
x:[Boolean]
xs) (Boolean
y:[Boolean]
ys) = (Boolean
x,Boolean
y) forall a. a -> [a] -> [a]
: [Boolean] -> [Boolean] -> [(Boolean, Boolean)]
zipf [Boolean]
xs [Boolean]
ys
    [(Boolean, Boolean)] -> m a
action forall a b. (a -> b) -> a -> b
$ [Boolean] -> [Boolean] -> [(Boolean, Boolean)]
zipf ( Number -> [Boolean]
bits Number
a ) ( Number -> [Boolean]
bits Number
b )    
        

le, ge, eq, equals, gt, lt 
  :: MonadSAT m => Number -> Number -> m Boolean

for :: [a] -> (a -> b) -> [b]
for = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> [a] -> [b]
map

equals :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
equals = forall (m :: * -> *) a.
MonadSAT m =>
([(Boolean, Boolean)] -> m a) -> Number -> Number -> m a
extended forall a b. (a -> b) -> a -> b
$ \ [(Boolean, Boolean)]
xys -> forall (m :: * -> *) a b. Monad m => ([a] -> m b) -> [m a] -> m b
monadic forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and forall a b. (a -> b) -> a -> b
$ 
    forall {a} {b}. [a] -> (a -> b) -> [b]
for [(Boolean, Boolean)]
xys forall a b. (a -> b) -> a -> b
$ \ (Boolean
x,Boolean
y) -> forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 forall a. Eq a => a -> a -> Bool
(==) Boolean
x Boolean
y

le :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
le = forall (m :: * -> *) a.
MonadSAT m =>
([(Boolean, Boolean)] -> m a) -> Number -> Number -> m a
extended forall a b. (a -> b) -> a -> b
$ \ [(Boolean, Boolean)]
xys -> forall (m :: * -> *) a b. Monad m => ([a] -> m b) -> [m a] -> m b
monadic forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and forall a b. (a -> b) -> a -> b
$ 
    forall {a} {b}. [a] -> (a -> b) -> [b]
for [(Boolean, Boolean)]
xys forall a b. (a -> b) -> a -> b
$ \ (Boolean
x,Boolean
y) -> forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 forall a. Ord a => a -> a -> Bool
(<=) Boolean
x Boolean
y

ge :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
ge = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
le

eq :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
eq = forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
equals

lt :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
lt Number
a Number
b = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Boolean -> Boolean
not forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
ge Number
a Number
b

gt :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
gt = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
lt

min :: Number -> Number -> m Number
min Number
a Number
b = do 
    [Boolean]
cs <- forall (m :: * -> *) a.
MonadSAT m =>
([(Boolean, Boolean)] -> m a) -> Number -> Number -> m a
extended ( \ [(Boolean, Boolean)]
xys -> 
        forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Boolean, Boolean)]
xys forall a b. (a -> b) -> a -> b
$ \ (Boolean
x,Boolean
y) -> forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [Boolean
x,Boolean
y] ) Number
a Number
b
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
cs                              
                          
max :: Number -> Number -> m Number
max Number
a Number
b = do
    [Boolean]
cs <- forall (m :: * -> *) a.
MonadSAT m =>
([(Boolean, Boolean)] -> m a) -> Number -> Number -> m a
extended ( \ [(Boolean, Boolean)]
xys -> 
        forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Boolean, Boolean)]
xys forall a b. (a -> b) -> a -> b
$ \ (Boolean
x,Boolean
y) -> forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [Boolean
x,Boolean
y] ) Number
a Number
b
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
cs                      

-- | maximum (x:xs) = foldM max x xs
maximum :: [Number] -> m Number
maximum [Number
x] = forall (m :: * -> *) a. Monad m => a -> m a
return Number
x
maximum [Number]
xs | Bool -> Bool
Prelude.not ( forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Number]
xs ) = do
    Boolean
f <- forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
False
    let w :: Int
w = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
Prelude.maximum forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Number -> Int
width [Number]
xs
        fill :: Number -> [Boolean]
fill Number
x = Number -> [Boolean]
bits Number
x forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate (Int
w forall a. Num a => a -> a -> a
- Number -> Int
width Number
x) Boolean
f
    [Boolean]
ys <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( forall a. [[a]] -> [[a]]
transpose forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Number -> [Boolean]
fill [Number]
xs ) forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
B.or
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
ys

-- | minimum (x:xs) = foldM min x xs
minimum :: [Number] -> m Number
minimum [Number
x] = forall (m :: * -> *) a. Monad m => a -> m a
return Number
x
minimum [Number]
xs | Bool -> Bool
Prelude.not ( forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Number]
xs ) = do
    Boolean
f <- forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
False
    let w :: Int
w = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
Prelude.maximum forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Number -> Int
width [Number]
xs
        fill :: Number -> [Boolean]
fill Number
x = Number -> [Boolean]
bits Number
x forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate (Int
w forall a. Num a => a -> a -> a
- Number -> Int
width Number
x) Boolean
f
    [Boolean]
ys <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( forall a. [[a]] -> [[a]]
transpose forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Number -> [Boolean]
fill [Number]
xs ) forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
B.and
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
ys


-- | when f is False, switch off all bits
select :: Boolean -> Number -> m Number
select Boolean
f Number
a = do
    [Boolean]
bs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( Number -> [Boolean]
bits Number
a ) forall a b. (a -> b) -> a -> b
$ \ Boolean
b -> forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [Boolean
f,Boolean
b]
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
bs

-- | when p is True, switch ON all bits
antiselect :: Boolean -> Number -> m Number
antiselect Boolean
p Number
n = do
    [Boolean]
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 a b. (a -> b) -> a -> b
$ \ Boolean
b -> forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
B.or [Boolean
p, Boolean
b]
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
bs

-- | reduce number to given bit width,
-- and return also the carry bit
cutoff_with_carry :: MonadSAT m 
                  => Maybe Int -> Number -> m (Number, Boolean)
cutoff_with_carry :: forall (m :: * -> *).
MonadSAT m =>
Maybe Int -> Number -> m (Number, Boolean)
cutoff_with_carry Maybe Int
mwidth Number
n = do
    Boolean
f <- forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
False
    case Maybe Int
mwidth of
        Maybe Int
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return (Number
n , Boolean
f )
        Just Int
width -> do
            let ( [Boolean]
pre, [Boolean]
post ) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
width forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
n
            forall (m :: * -> *) a. Monad m => a -> m a
return ( [Boolean] -> Number
make [Boolean]
pre, case [Boolean]
post of
                [] -> Boolean
f
                Boolean
carry : [Boolean]
_ -> Boolean
carry )

cutoff :: Maybe Int -> Number -> m Number
cutoff Maybe Int
mwidth Number
n = do
    ( Number
result, Boolean
carry ) <- forall (m :: * -> *).
MonadSAT m =>
Maybe Int -> Number -> m (Number, Boolean)
cutoff_with_carry Maybe Int
mwidth Number
n
    forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [ Boolean -> Boolean
not Boolean
carry ]
    forall (m :: * -> *) a. Monad m => a -> m a
return Number
result

-- | for both "add" methods: if first arg is Nothing, 
-- then result length is sum of argument lengths (cannot overflow).
-- else result is cut off (overflow => unsatisfiable)
add_quadratic :: MonadSAT m => Maybe Int -> Number -> Number -> m Number
add_quadratic :: forall (m :: * -> *).
MonadSAT m =>
Maybe Int -> Number -> Number -> m Number
add_quadratic Maybe Int
mwidth Number
a Number
b = do
    Boolean
t <- forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
True
    [(Int, [Boolean])]
pairs <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall a b. (a -> b) -> a -> b
$ do
        (Int
i,Boolean
x) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 .. ] forall a b. (a -> b) -> a -> b
$ Boolean
t forall a. a -> [a] -> [a]
: Number -> [Boolean]
bits Number
a
        (Int
j,Boolean
y) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 .. ] forall a b. (a -> b) -> a -> b
$ Boolean
t forall a. a -> [a] -> [a]
: Number -> [Boolean]
bits Number
b
        forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Int
iforall a. Num a => a -> a -> a
+Int
j forall a. Ord a => a -> a -> Bool
> Int
0
        forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ case Maybe Int
mwidth of
            Just Int
width -> Int
iforall a. Num a => a -> a -> a
+Int
j forall a. Ord a => a -> a -> Bool
<= Int
width forall a. Num a => a -> a -> a
+ Int
1
            Maybe Int
Nothing    -> Bool
True
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do Boolean
z <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [Boolean
x,Boolean
y] ; forall (m :: * -> *) a. Monad m => a -> m a
return (Int
iforall a. Num a => a -> a -> a
+Int
j, [Boolean
z])
    [Boolean]
cs <- 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]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toAscList forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith forall a. [a] -> [a] -> [a]
(++) [(Int, [Boolean])]
pairs ) forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or
    forall {m :: * -> *}. MonadSAT m => Maybe Int -> Number -> m Number
cutoff Maybe Int
mwidth forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
cs


  
-- | works for all widths
add_by_odd_even_merge :: Maybe Int -> Number -> Number -> m Number
add_by_odd_even_merge Maybe Int
mwidth Number
a Number
b = do
    [Boolean]
zs <- forall {m :: * -> *}.
MonadSAT m =>
[Boolean] -> [Boolean] -> m [Boolean]
oe_merge (Number -> [Boolean]
bits Number
a) (Number -> [Boolean]
bits Number
b)
    forall {m :: * -> *}. MonadSAT m => Maybe Int -> Number -> m Number
cutoff Maybe Int
mwidth forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
zs
    
-- | will fill up the input 
-- such that length is a power of two.
-- it seems to be hard to improve this, cf
-- <http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2009/CS/CS-2009-07>
add_by_bitonic_sort :: Maybe Int -> Number -> Number -> m Number
add_by_bitonic_sort Maybe Int
mwidth Number
a Number
b = do
    let n :: Int
n = forall (t :: * -> *) a. Foldable t => t a -> Int
length ( Number -> [Boolean]
bits Number
a) forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Int
length (Number -> [Boolean]
bits Number
b)
    Boolean
f <- forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
False        
    let input :: [Boolean]
input =    (Number -> [Boolean]
bits Number
a) -- decreasing
                forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate (forall {t}. Integral t => t -> t
fill Int
n) Boolean
f
                forall a. [a] -> [a] -> [a]
++ (forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
b) -- increasing
    [Boolean]
zs <- forall {m :: * -> *}. MonadSAT m => [Boolean] -> m [Boolean]
bitonic_sort [Boolean]
input
    forall {m :: * -> *}. MonadSAT m => Maybe Int -> Number -> m Number
cutoff Maybe Int
mwidth forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
zs

-- | distance to next power of two
fill :: t -> t
fill t
n = if t
n forall a. Ord a => a -> a -> Bool
<= t
1 then t
0 else
            let (t
d,t
m) = forall a. Integral a => a -> a -> (a, a)
divMod t
n t
2
            in  t
m forall a. Num a => a -> a -> a
+ t
2forall a. Num a => a -> a -> a
*t -> t
fill (t
dforall a. Num a => a -> a -> a
+t
m) 

-- |  <http://www.iti.fh-flensburg.de/lang/algorithmen/sortieren/bitonic/bitonicen.htm>
bitonic_sort :: [Boolean] -> m [Boolean]
bitonic_sort [ ] = forall (m :: * -> *) a. Monad m => a -> m a
return [ ]    
bitonic_sort [Boolean
z] = forall (m :: * -> *) a. Monad m => a -> m a
return [Boolean
z]
bitonic_sort [Boolean]
zs = do 
    let (Int
h,Int
0) = forall a. Integral a => a -> a -> (a, a)
divMod (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Boolean]
zs) Int
2
        ([Boolean]
pre, [Boolean]
post) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
h [Boolean]
zs
    [Boolean]
hi <- 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]
pre [Boolean]
post ) forall a b. (a -> b) -> a -> b
$ \ (Boolean
x,Boolean
y) -> forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or  [Boolean
x,Boolean
y]
    [Boolean]
lo <- 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]
pre [Boolean]
post ) forall a b. (a -> b) -> a -> b
$ \ (Boolean
x,Boolean
y) -> forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [Boolean
x,Boolean
y]
    [Boolean]
shi <- [Boolean] -> m [Boolean]
bitonic_sort [Boolean]
hi
    [Boolean]
slo <- [Boolean] -> m [Boolean]
bitonic_sort [Boolean]
lo
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean]
shi forall a. [a] -> [a] -> [a]
++ [Boolean]
slo
    
-- | <http://www.iti.fh-flensburg.de/lang/algorithmen/sortieren/networks/oemen.htm>

oe_merge :: [Boolean] -> [Boolean] -> m [Boolean]
oe_merge  [] [Boolean]
ys = forall (m :: * -> *) a. Monad m => a -> m a
return [Boolean]
ys
oe_merge  [Boolean]
xs [] = forall (m :: * -> *) a. Monad m => a -> m a
return [Boolean]
xs
oe_merge  [Boolean
x] [Boolean
y] = do
    forall {m :: * -> *}.
MonadSAT m =>
Boolean -> Boolean -> m [Boolean]
comparator Boolean
x Boolean
y
oe_merge  [Boolean]
xs [Boolean]
ys = do
    let ( [Boolean]
xo, [Boolean]
xe ) = forall {a}. [a] -> ([a], [a])
divide [Boolean]
xs
        ( [Boolean]
yo, [Boolean]
ye ) = forall {a}. [a] -> ([a], [a])
divide [Boolean]
ys
    ~(Boolean
m : [Boolean]
mo) <- [Boolean] -> [Boolean] -> m [Boolean]
oe_merge  [Boolean]
xo [Boolean]
yo
    [Boolean]
me <- [Boolean] -> [Boolean] -> m [Boolean]
oe_merge  [Boolean]
xe [Boolean]
ye
    [Boolean]
re <- forall {m :: * -> *}.
MonadSAT m =>
[Boolean] -> [Boolean] -> m [Boolean]
repair [Boolean]
me [Boolean]
mo
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Boolean
m forall a. a -> [a] -> [a]
: [Boolean]
re

divide :: [a] -> ([a], [a])
divide (a
x : [a]
xs) = 
    let ( [a]
this, [a]
that ) = [a] -> ([a], [a])
divide [a]
xs
    in  ( a
x forall a. a -> [a] -> [a]
: [a]
that, [a]
this )
divide [] = ( [], [] )

repair :: [Boolean] -> [Boolean] -> m [Boolean]
repair (Boolean
x:[Boolean]
xs) (Boolean
y:[Boolean]
ys) = do
    [Boolean]
here <- forall {m :: * -> *}.
MonadSAT m =>
Boolean -> Boolean -> m [Boolean]
comparator Boolean
x Boolean
y
    [Boolean]
later <- [Boolean] -> [Boolean] -> m [Boolean]
repair [Boolean]
xs [Boolean]
ys
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean]
here forall a. [a] -> [a] -> [a]
++ [Boolean]
later
repair [] [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
repair [Boolean
x] [] = forall (m :: * -> *) a. Monad m => a -> m a
return [Boolean
x]
repair [] [Boolean
y] = forall (m :: * -> *) a. Monad m => a -> m a
return [Boolean
y]

comparator :: Boolean -> Boolean -> m [Boolean]
comparator Boolean
x Boolean
y = do
    Boolean
hi <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
Satchmo.Boolean.or [Boolean
x, Boolean
y]
    Boolean
lo <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
Satchmo.Boolean.and [Boolean
x, Boolean
y]
    forall (m :: * -> *) a. Monad m => a -> m a
return [ Boolean
hi, Boolean
lo ]