{-# language FlexibleInstances #-}
{-# language MultiParamTypeClasses #-}
{-# language FlexibleContexts      #-}

module Satchmo.PolynomialN
    ( Coefficient, Exponents, PolynomialN (), NumPolynomialN
    , fromMonomials, add, equals)
where

import Control.Monad (forM,foldM)
import Data.List (partition,sortBy)
import qualified Satchmo.Binary.Op.Fixed as F
import Satchmo.Code (Decode (..),decode)
import Satchmo.MonadSAT (MonadSAT)
import Satchmo.Boolean (Boolean)
import qualified Satchmo.Boolean as B

type Coefficient a = a

type Exponents = [Integer]

data Monomial a  = Monomial (Coefficient a, Exponents) deriving (Int -> Monomial a -> ShowS
forall a. Show a => Int -> Monomial a -> ShowS
forall a. Show a => [Monomial a] -> ShowS
forall a. Show a => Monomial a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Monomial a] -> ShowS
$cshowList :: forall a. Show a => [Monomial a] -> ShowS
show :: Monomial a -> String
$cshow :: forall a. Show a => Monomial a -> String
showsPrec :: Int -> Monomial a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Monomial a -> ShowS
Show)
type NumMonomial = Monomial F.Number

data PolynomialN a  = PolynomialN [Monomial a] deriving (Int -> PolynomialN a -> ShowS
forall a. Show a => Int -> PolynomialN a -> ShowS
forall a. Show a => [PolynomialN a] -> ShowS
forall a. Show a => PolynomialN a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PolynomialN a] -> ShowS
$cshowList :: forall a. Show a => [PolynomialN a] -> ShowS
show :: PolynomialN a -> String
$cshow :: forall a. Show a => PolynomialN a -> String
showsPrec :: Int -> PolynomialN a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> PolynomialN a -> ShowS
Show)
type NumPolynomialN = PolynomialN F.Number

instance Decode m a Integer => Decode m (Monomial a) (Monomial Integer) where
    decode :: Monomial a -> m (Monomial Integer)
decode (Monomial (a
coeff,Exponents
vars)) = do
      Integer
decodedCoeff <- forall (m :: * -> *) c a. Decode m c a => c -> m a
decode a
coeff
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (a, Exponents) -> Monomial a
Monomial (Integer
decodedCoeff,Exponents
vars)

instance Decode m a Integer => Decode m (PolynomialN a) (PolynomialN Integer) where
    decode :: PolynomialN a -> m (PolynomialN Integer)
decode (PolynomialN [Monomial a]
monomials) = do
        [Monomial Integer]
decodedMonomials <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Monomial a]
monomials forall (m :: * -> *) c a. Decode m c a => c -> m a
decode
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [Monomial a] -> PolynomialN a
PolynomialN [Monomial Integer]
decodedMonomials

fromMonomials :: MonadSAT m 
              => Int -- ^ bit width of coefficients
              -> [(Coefficient Integer,Exponents)] -- ^ monomials
              -> m NumPolynomialN
fromMonomials :: forall (m :: * -> *).
MonadSAT m =>
Int -> [(Integer, Exponents)] -> m NumPolynomialN
fromMonomials Int
bits [(Integer, Exponents)]
monomials = do
  [Monomial Number]
monomials' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Integer, Exponents)]
monomials forall a b. (a -> b) -> a -> b
$ \(Integer
c,Exponents
es) -> do
                                 Number
coefficient <- forall (m :: * -> *). MonadSAT m => Int -> Integer -> m Number
F.constantWidth Int
bits Integer
c
                                 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (a, Exponents) -> Monomial a
Monomial (Number
coefficient,Exponents
es)
  forall (m :: * -> *).
MonadSAT m =>
NumPolynomialN -> m NumPolynomialN
reduce forall a b. (a -> b) -> a -> b
$ forall a. [Monomial a] -> PolynomialN a
PolynomialN [Monomial Number]
monomials'

coefficient :: Monomial a -> Coefficient a
coefficient :: forall a. Monomial a -> a
coefficient (Monomial (a
c,Exponents
_)) = a
c

exponents :: Monomial a -> Exponents
exponents :: forall a. Monomial a -> Exponents
exponents (Monomial (a
_,Exponents
e)) = Exponents
e

monomials :: PolynomialN a -> [Monomial a]
monomials :: forall a. PolynomialN a -> [Monomial a]
monomials (PolynomialN [Monomial a]
xs) = [Monomial a]
xs

sameExponents :: Monomial a -> Monomial a -> Bool
sameExponents :: forall a. Monomial a -> Monomial a -> Bool
sameExponents Monomial a
m1 Monomial a
m2 = forall a. Monomial a -> Exponents
exponents Monomial a
m1 forall a. Eq a => a -> a -> Bool
== forall a. Monomial a -> Exponents
exponents Monomial a
m2

add :: MonadSAT m => NumPolynomialN -> NumPolynomialN -> m NumPolynomialN
add :: forall (m :: * -> *).
MonadSAT m =>
NumPolynomialN -> NumPolynomialN -> m NumPolynomialN
add (PolynomialN [Monomial Number]
xs) (PolynomialN [Monomial Number]
ys) =
    forall (m :: * -> *).
MonadSAT m =>
NumPolynomialN -> m NumPolynomialN
reduce forall a b. (a -> b) -> a -> b
$ forall a. [Monomial a] -> PolynomialN a
PolynomialN forall a b. (a -> b) -> a -> b
$ [Monomial Number]
xs forall a. [a] -> [a] -> [a]
++ [Monomial Number]
ys

addMonomial :: MonadSAT m => NumMonomial -> NumMonomial -> m NumMonomial
addMonomial :: forall (m :: * -> *).
MonadSAT m =>
Monomial Number -> Monomial Number -> m (Monomial Number)
addMonomial Monomial Number
m1 Monomial Number
m2 =
    if forall a. Monomial a -> Monomial a -> Bool
sameExponents Monomial Number
m1 Monomial Number
m2 then 
        do Number
c <- forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
F.add (forall a. Monomial a -> a
coefficient Monomial Number
m1) (forall a. Monomial a -> a
coefficient Monomial Number
m2)
           forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (a, Exponents) -> Monomial a
Monomial (Number
c, forall a. Monomial a -> Exponents
exponents Monomial Number
m1)
    else
        forall a. HasCallStack => String -> a
error String
"PolynomialN.addMonomial"

strictOrdering :: Monomial a -> Monomial a -> Ordering
strictOrdering :: forall a. Monomial a -> Monomial a -> Ordering
strictOrdering (Monomial (a
_,Exponents
xs)) (Monomial (a
_,Exponents
ys)) = forall a. Ord a => a -> a -> Ordering
compare Exponents
xs Exponents
ys

reduce :: MonadSAT m => NumPolynomialN -> m NumPolynomialN
reduce :: forall (m :: * -> *).
MonadSAT m =>
NumPolynomialN -> m NumPolynomialN
reduce (PolynomialN []) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [Monomial a] -> PolynomialN a
PolynomialN []
reduce (PolynomialN (Monomial Number
x:[Monomial Number]
xs)) =
    let ([Monomial Number]
reducable,[Monomial Number]
notReducable) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (forall a. Monomial a -> Monomial a -> Bool
sameExponents Monomial Number
x) [Monomial Number]
xs
        strictOrd :: Monomial a -> Monomial a -> Ordering
strictOrd (Monomial (a
_,Exponents
xs)) (Monomial (a
_,Exponents
ys)) = forall a. Ord a => a -> a -> Ordering
compare Exponents
xs Exponents
ys
    in do
      Monomial Number
newMonomial <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM forall (m :: * -> *).
MonadSAT m =>
Monomial Number -> Monomial Number -> m (Monomial Number)
addMonomial Monomial Number
x [Monomial Number]
reducable
      PolynomialN [Monomial Number]
rest <- forall (m :: * -> *).
MonadSAT m =>
NumPolynomialN -> m NumPolynomialN
reduce forall a b. (a -> b) -> a -> b
$ forall a. [Monomial a] -> PolynomialN a
PolynomialN [Monomial Number]
notReducable
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [Monomial a] -> PolynomialN a
PolynomialN forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy forall {a} {a}. Monomial a -> Monomial a -> Ordering
strictOrd forall a b. (a -> b) -> a -> b
$ Monomial Number
newMonomial forall a. a -> [a] -> [a]
: [Monomial Number]
rest
    
equalsMonomial :: MonadSAT m => NumMonomial -> NumMonomial -> m Boolean
equalsMonomial :: forall (m :: * -> *).
MonadSAT m =>
Monomial Number -> Monomial Number -> m Boolean
equalsMonomial Monomial Number
m1 Monomial Number
m2 = do
  Boolean
equalsCoefficient <- forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
F.equals (forall a. Monomial a -> a
coefficient Monomial Number
m1) (forall a. Monomial a -> a
coefficient Monomial Number
m2)
  Boolean
equalsExponents <- forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant forall a b. (a -> b) -> a -> b
$ (forall a. Monomial a -> Exponents
exponents Monomial Number
m1) forall a. Eq a => a -> a -> Bool
== (forall a. Monomial a -> Exponents
exponents Monomial Number
m2)
  forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
B.and [Boolean
equalsCoefficient,Boolean
equalsExponents]

equals :: MonadSAT m => NumPolynomialN -> NumPolynomialN -> m Boolean
equals :: forall (m :: * -> *).
MonadSAT m =>
NumPolynomialN -> NumPolynomialN -> m Boolean
equals (PolynomialN []) (PolynomialN []) = forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
True
equals (PolynomialN (Monomial Number
x:[Monomial Number]
xs)) (PolynomialN (Monomial Number
y:[Monomial Number]
ys)) = do
  Boolean
e <- forall (m :: * -> *).
MonadSAT m =>
Monomial Number -> Monomial Number -> m Boolean
equalsMonomial Monomial Number
x Monomial Number
y
  Boolean
es <- forall (m :: * -> *).
MonadSAT m =>
NumPolynomialN -> NumPolynomialN -> m Boolean
equals (forall a. [Monomial a] -> PolynomialN a
PolynomialN [Monomial Number]
xs) (forall a. [Monomial a] -> PolynomialN a
PolynomialN [Monomial Number]
ys)
  forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
B.and [Boolean
e,Boolean
es]