{-# 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
[Monomial a] -> ShowS
Monomial a -> String
(Int -> Monomial a -> ShowS)
-> (Monomial a -> String)
-> ([Monomial a] -> ShowS)
-> Show (Monomial a)
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
$cshowsPrec :: forall a. Show a => Int -> Monomial a -> ShowS
showsPrec :: Int -> Monomial a -> ShowS
$cshow :: forall a. Show a => Monomial a -> String
show :: Monomial a -> String
$cshowList :: forall a. Show a => [Monomial a] -> ShowS
showList :: [Monomial a] -> ShowS
Show)
type NumMonomial = Monomial F.Number

data PolynomialN a  = PolynomialN [Monomial a] deriving (Int -> PolynomialN a -> ShowS
[PolynomialN a] -> ShowS
PolynomialN a -> String
(Int -> PolynomialN a -> ShowS)
-> (PolynomialN a -> String)
-> ([PolynomialN a] -> ShowS)
-> Show (PolynomialN a)
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
$cshowsPrec :: forall a. Show a => Int -> PolynomialN a -> ShowS
showsPrec :: Int -> PolynomialN a -> ShowS
$cshow :: forall a. Show a => PolynomialN a -> String
show :: PolynomialN a -> String
$cshowList :: forall a. Show a => [PolynomialN a] -> ShowS
showList :: [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 <- a -> m Integer
forall (m :: * -> *) c a. Decode m c a => c -> m a
decode a
coeff
      Monomial Integer -> m (Monomial Integer)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Monomial Integer -> m (Monomial Integer))
-> Monomial Integer -> m (Monomial Integer)
forall a b. (a -> b) -> a -> b
$ (Integer, Exponents) -> Monomial Integer
forall a. (Coefficient a, Exponents) -> Monomial (Coefficient 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 <- [Monomial a]
-> (Monomial a -> m (Monomial Integer)) -> m [Monomial Integer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Monomial a]
monomials Monomial a -> m (Monomial Integer)
forall (m :: * -> *) c a. Decode m c a => c -> m a
decode
        PolynomialN Integer -> m (PolynomialN Integer)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (PolynomialN Integer -> m (PolynomialN Integer))
-> PolynomialN Integer -> m (PolynomialN Integer)
forall a b. (a -> b) -> a -> b
$ [Monomial Integer] -> PolynomialN Integer
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' <- [(Integer, Exponents)]
-> ((Integer, Exponents) -> m (Monomial Number))
-> m [Monomial Number]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Integer, Exponents)]
monomials (((Integer, Exponents) -> m (Monomial Number))
 -> m [Monomial Number])
-> ((Integer, Exponents) -> m (Monomial Number))
-> m [Monomial Number]
forall a b. (a -> b) -> a -> b
$ \(Integer
c,Exponents
es) -> do
                                 Number
coefficient <- Int -> Integer -> m Number
forall (m :: * -> *). MonadSAT m => Int -> Integer -> m Number
F.constantWidth Int
bits Integer
c
                                 Monomial Number -> m (Monomial Number)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Monomial Number -> m (Monomial Number))
-> Monomial Number -> m (Monomial Number)
forall a b. (a -> b) -> a -> b
$ (Number, Exponents) -> Monomial Number
forall a. (Coefficient a, Exponents) -> Monomial (Coefficient a)
Monomial (Number
coefficient,Exponents
es)
  NumPolynomialN -> m NumPolynomialN
forall (m :: * -> *).
MonadSAT m =>
NumPolynomialN -> m NumPolynomialN
reduce (NumPolynomialN -> m NumPolynomialN)
-> NumPolynomialN -> m NumPolynomialN
forall a b. (a -> b) -> a -> b
$ [Monomial Number] -> NumPolynomialN
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 = Monomial a -> Exponents
forall a. Monomial a -> Exponents
exponents Monomial a
m1 Exponents -> Exponents -> Bool
forall a. Eq a => a -> a -> Bool
== Monomial a -> Exponents
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) =
    NumPolynomialN -> m NumPolynomialN
forall (m :: * -> *).
MonadSAT m =>
NumPolynomialN -> m NumPolynomialN
reduce (NumPolynomialN -> m NumPolynomialN)
-> NumPolynomialN -> m NumPolynomialN
forall a b. (a -> b) -> a -> b
$ [Monomial Number] -> NumPolynomialN
forall a. [Monomial a] -> PolynomialN a
PolynomialN ([Monomial Number] -> NumPolynomialN)
-> [Monomial Number] -> NumPolynomialN
forall a b. (a -> b) -> a -> b
$ [Monomial Number]
xs [Monomial Number] -> [Monomial Number] -> [Monomial Number]
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 Monomial Number -> Monomial Number -> Bool
forall a. Monomial a -> Monomial a -> Bool
sameExponents Monomial Number
m1 Monomial Number
m2 then 
        do Number
c <- Number -> Number -> m Number
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
F.add (Monomial Number -> Number
forall a. Monomial a -> a
coefficient Monomial Number
m1) (Monomial Number -> Number
forall a. Monomial a -> a
coefficient Monomial Number
m2)
           Monomial Number -> m (Monomial Number)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Monomial Number -> m (Monomial Number))
-> Monomial Number -> m (Monomial Number)
forall a b. (a -> b) -> a -> b
$ (Number, Exponents) -> Monomial Number
forall a. (Coefficient a, Exponents) -> Monomial (Coefficient a)
Monomial (Number
c, Monomial Number -> Exponents
forall a. Monomial a -> Exponents
exponents Monomial Number
m1)
    else
        String -> m (Monomial Number)
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)) = Exponents -> Exponents -> Ordering
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 []) = NumPolynomialN -> m NumPolynomialN
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (NumPolynomialN -> m NumPolynomialN)
-> NumPolynomialN -> m NumPolynomialN
forall a b. (a -> b) -> a -> b
$ [Monomial Number] -> NumPolynomialN
forall a. [Monomial a] -> PolynomialN a
PolynomialN []
reduce (PolynomialN (Monomial Number
x:[Monomial Number]
xs)) =
    let ([Monomial Number]
reducable,[Monomial Number]
notReducable) = (Monomial Number -> Bool)
-> [Monomial Number] -> ([Monomial Number], [Monomial Number])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Monomial Number -> Monomial Number -> Bool
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)) = Exponents -> Exponents -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Exponents
xs Exponents
ys
    in do
      Monomial Number
newMonomial <- (Monomial Number -> Monomial Number -> m (Monomial Number))
-> Monomial Number -> [Monomial Number] -> m (Monomial Number)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Monomial Number -> Monomial Number -> m (Monomial Number)
forall (m :: * -> *).
MonadSAT m =>
Monomial Number -> Monomial Number -> m (Monomial Number)
addMonomial Monomial Number
x [Monomial Number]
reducable
      PolynomialN [Monomial Number]
rest <- NumPolynomialN -> m NumPolynomialN
forall (m :: * -> *).
MonadSAT m =>
NumPolynomialN -> m NumPolynomialN
reduce (NumPolynomialN -> m NumPolynomialN)
-> NumPolynomialN -> m NumPolynomialN
forall a b. (a -> b) -> a -> b
$ [Monomial Number] -> NumPolynomialN
forall a. [Monomial a] -> PolynomialN a
PolynomialN [Monomial Number]
notReducable
      NumPolynomialN -> m NumPolynomialN
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (NumPolynomialN -> m NumPolynomialN)
-> NumPolynomialN -> m NumPolynomialN
forall a b. (a -> b) -> a -> b
$ [Monomial Number] -> NumPolynomialN
forall a. [Monomial a] -> PolynomialN a
PolynomialN ([Monomial Number] -> NumPolynomialN)
-> [Monomial Number] -> NumPolynomialN
forall a b. (a -> b) -> a -> b
$ (Monomial Number -> Monomial Number -> Ordering)
-> [Monomial Number] -> [Monomial Number]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy Monomial Number -> Monomial Number -> Ordering
forall {a} {a}. Monomial a -> Monomial a -> Ordering
strictOrd ([Monomial Number] -> [Monomial Number])
-> [Monomial Number] -> [Monomial Number]
forall a b. (a -> b) -> a -> b
$ Monomial Number
newMonomial Monomial Number -> [Monomial Number] -> [Monomial Number]
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 <- Number -> Number -> m Boolean
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
F.equals (Monomial Number -> Number
forall a. Monomial a -> a
coefficient Monomial Number
m1) (Monomial Number -> Number
forall a. Monomial a -> a
coefficient Monomial Number
m2)
  Boolean
equalsExponents <- Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant (Bool -> m Boolean) -> Bool -> m Boolean
forall a b. (a -> b) -> a -> b
$ (Monomial Number -> Exponents
forall a. Monomial a -> Exponents
exponents Monomial Number
m1) Exponents -> Exponents -> Bool
forall a. Eq a => a -> a -> Bool
== (Monomial Number -> Exponents
forall a. Monomial a -> Exponents
exponents Monomial Number
m2)
  [Boolean] -> m Boolean
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 []) = Bool -> m Boolean
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 <- Monomial Number -> Monomial Number -> m Boolean
forall (m :: * -> *).
MonadSAT m =>
Monomial Number -> Monomial Number -> m Boolean
equalsMonomial Monomial Number
x Monomial Number
y
  Boolean
es <- NumPolynomialN -> NumPolynomialN -> m Boolean
forall (m :: * -> *).
MonadSAT m =>
NumPolynomialN -> NumPolynomialN -> m Boolean
equals ([Monomial Number] -> NumPolynomialN
forall a. [Monomial a] -> PolynomialN a
PolynomialN [Monomial Number]
xs) ([Monomial Number] -> NumPolynomialN
forall a. [Monomial a] -> PolynomialN a
PolynomialN [Monomial Number]
ys)
  [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
B.and [Boolean
e,Boolean
es]