{-# language MultiParamTypeClasses, FlexibleInstances #-}

module Satchmo.Polynomial.Numeric where

import qualified Satchmo.Boolean as B
import Satchmo.Code
import Satchmo.Numeric

import Control.Monad ( forM )

data Poly a = Poly [a] deriving Int -> Poly a -> ShowS
[Poly a] -> ShowS
Poly a -> String
(Int -> Poly a -> ShowS)
-> (Poly a -> String) -> ([Poly a] -> ShowS) -> Show (Poly a)
forall a. Show a => Int -> Poly a -> ShowS
forall a. Show a => [Poly a] -> ShowS
forall a. Show a => Poly a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Poly a -> ShowS
showsPrec :: Int -> Poly a -> ShowS
$cshow :: forall a. Show a => Poly a -> String
show :: Poly a -> String
$cshowList :: forall a. Show a => [Poly a] -> ShowS
showList :: [Poly a] -> ShowS
Show

instance Decode m a b => Decode m ( Poly a ) ( Poly b ) where
    decode :: Poly a -> m (Poly b)
decode ( Poly [a]
xs ) = do
        [b]
ys <- [a] -> (a -> m b) -> m [b]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [a]
xs a -> m b
forall (m :: * -> *) c a. Decode m c a => c -> m a
decode
        Poly b -> m (Poly b)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Poly b -> m (Poly b)) -> Poly b -> m (Poly b)
forall a b. (a -> b) -> a -> b
$ [b] -> Poly b
forall a. [a] -> Poly a
Poly [b]
ys

derive :: Poly a -> m (Poly a)
derive ( Poly [a]
xs ) = do
    [a]
ys <- [(Integer, a)] -> ((Integer, a) -> m a) -> m [a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( Int -> [(Integer, a)] -> [(Integer, a)]
forall a. Int -> [a] -> [a]
drop Int
1 ([(Integer, a)] -> [(Integer, a)])
-> [(Integer, a)] -> [(Integer, a)]
forall a b. (a -> b) -> a -> b
$ [Integer] -> [a] -> [(Integer, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [ Integer
0 .. ] [a]
xs ) (((Integer, a) -> m a) -> m [a]) -> ((Integer, a) -> m a) -> m [a]
forall a b. (a -> b) -> a -> b
$ \ (Integer
k,a
x) -> do
        a
f <- Integer -> m a
forall a (m :: * -> *). (Constant a, MonadSAT m) => Integer -> m a
forall (m :: * -> *). MonadSAT m => Integer -> m a
constant Integer
k
        a -> a -> m a
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => a -> a -> m a
times a
f a
x
    Poly a -> m (Poly a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Poly a -> m (Poly a)) -> Poly a -> m (Poly a)
forall a b. (a -> b) -> a -> b
$ [a] -> Poly a
forall a. [a] -> Poly a
Poly [a]
ys
    
constantTerm :: Poly a -> a
constantTerm ( Poly [a]
xs ) = [a] -> a
forall a. HasCallStack => [a] -> a
head [a]
xs    

polynomial :: ( Create a , B.MonadSAT m )
           => Int -> Int 
           -> m ( Poly a )
polynomial :: forall a (m :: * -> *).
(Create a, MonadSAT m) =>
Int -> Int -> m (Poly a)
polynomial Int
bits Int
degree = do
    [a]
xs <- [Int] -> (Int -> m a) -> m [a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ Int
0 .. Int
degree ] ((Int -> m a) -> m [a]) -> (Int -> m a) -> m [a]
forall a b. (a -> b) -> a -> b
$ \ Int
k -> Int -> m a
forall a (m :: * -> *). (Create a, MonadSAT m) => Int -> m a
forall (m :: * -> *). MonadSAT m => Int -> m a
create Int
bits
    Poly a -> m (Poly a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Poly a -> m (Poly a)) -> Poly a -> m (Poly a)
forall a b. (a -> b) -> a -> b
$ [a] -> Poly a
forall a. [a] -> Poly a
Poly [a]
xs
    
compose :: Poly a -> Poly a -> m (Poly a)
compose ( Poly [a]
xs ) Poly a
q = case [a]
xs of
    [] -> Poly a -> m (Poly a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Poly a -> m (Poly a)) -> Poly a -> m (Poly a)
forall a b. (a -> b) -> a -> b
$ [a] -> Poly a
forall a. [a] -> Poly a
Poly []
    a
x : [a]
xs -> do
        Poly a
p <- Poly a -> Poly a -> m (Poly a)
compose ( [a] -> Poly a
forall a. [a] -> Poly a
Poly [a]
xs ) Poly a
q
        Poly a
pq <- Poly a -> Poly a -> m (Poly a)
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => Poly a -> Poly a -> m (Poly a)
times Poly a
p Poly a
q
        Poly a -> Poly a -> m (Poly a)
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => Poly a -> Poly a -> m (Poly a)
plus ( [a] -> Poly a
forall a. [a] -> Poly a
Poly [a
x] ) Poly a
pq
    

instance ( Create a, Constant a, Numeric a )
         => Numeric ( Poly a ) where
    equal :: forall (m :: * -> *). MonadSAT m => Poly a -> Poly a -> m Boolean
equal ( Poly [a]
xs ) ( Poly [a]
ys ) = do
        a
z <- Int -> m a
forall a (m :: * -> *). (Create a, MonadSAT m) => Int -> m a
forall (m :: * -> *). MonadSAT m => Int -> m a
create Int
0
        [Boolean]
bs <- [(Maybe a, Maybe a)]
-> ((Maybe a, Maybe a) -> m Boolean) -> m [Boolean]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( [a] -> [a] -> [(Maybe a, Maybe a)]
forall a b. [a] -> [b] -> [(Maybe a, Maybe b)]
fullZip [a]
xs [a]
ys ) (((Maybe a, Maybe a) -> m Boolean) -> m [Boolean])
-> ((Maybe a, Maybe a) -> m Boolean) -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ \ (Maybe a, Maybe a)
xy -> case (Maybe a, Maybe a)
xy of
            ( Just a
x, Just a
y ) -> a -> a -> m Boolean
forall a (m :: * -> *).
(Numeric a, MonadSAT m) =>
a -> a -> m Boolean
forall (m :: * -> *). MonadSAT m => a -> a -> m Boolean
equal a
x a
y
            ( Just a
x, Maybe a
Nothing ) -> a -> a -> m Boolean
forall a (m :: * -> *).
(Numeric a, MonadSAT m) =>
a -> a -> m Boolean
forall (m :: * -> *). MonadSAT m => a -> a -> m Boolean
equal a
x a
z
            ( Maybe a
Nothing, Just a
y ) -> a -> a -> m Boolean
forall a (m :: * -> *).
(Numeric a, MonadSAT m) =>
a -> a -> m Boolean
forall (m :: * -> *). MonadSAT m => a -> a -> m Boolean
equal a
z a
y
        [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
B.and [Boolean]
bs
    greater_equal :: forall (m :: * -> *). MonadSAT m => Poly a -> Poly a -> m Boolean
greater_equal  ( Poly [a]
xs ) ( Poly [a]
ys ) = do
        a
z <- Int -> m a
forall a (m :: * -> *). (Create a, MonadSAT m) => Int -> m a
forall (m :: * -> *). MonadSAT m => Int -> m a
create Int
0
        [Boolean]
bs <- [(Maybe a, Maybe a)]
-> ((Maybe a, Maybe a) -> m Boolean) -> m [Boolean]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( [a] -> [a] -> [(Maybe a, Maybe a)]
forall a b. [a] -> [b] -> [(Maybe a, Maybe b)]
fullZip [a]
xs [a]
ys ) (((Maybe a, Maybe a) -> m Boolean) -> m [Boolean])
-> ((Maybe a, Maybe a) -> m Boolean) -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ \ (Maybe a, Maybe a)
xy -> case (Maybe a, Maybe a)
xy of
            ( Just a
x, Just a
y ) -> a -> a -> m Boolean
forall a (m :: * -> *).
(Numeric a, MonadSAT m) =>
a -> a -> m Boolean
forall (m :: * -> *). MonadSAT m => a -> a -> m Boolean
greater_equal a
x a
y
            ( Just a
x, Maybe a
Nothing ) -> a -> a -> m Boolean
forall a (m :: * -> *).
(Numeric a, MonadSAT m) =>
a -> a -> m Boolean
forall (m :: * -> *). MonadSAT m => a -> a -> m Boolean
greater_equal a
x a
z
            ( Maybe a
Nothing, Just a
y ) -> a -> a -> m Boolean
forall a (m :: * -> *).
(Numeric a, MonadSAT m) =>
a -> a -> m Boolean
forall (m :: * -> *). MonadSAT m => a -> a -> m Boolean
greater_equal a
z a
y
        [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
B.and [Boolean]
bs
    plus :: forall (m :: * -> *). MonadSAT m => Poly a -> Poly a -> m (Poly a)
plus  ( Poly [a]
xs ) ( Poly [a]
ys ) = do
        [a]
bs <- [(Maybe a, Maybe a)] -> ((Maybe a, Maybe a) -> m a) -> m [a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( [a] -> [a] -> [(Maybe a, Maybe a)]
forall a b. [a] -> [b] -> [(Maybe a, Maybe b)]
fullZip [a]
xs [a]
ys ) (((Maybe a, Maybe a) -> m a) -> m [a])
-> ((Maybe a, Maybe a) -> m a) -> m [a]
forall a b. (a -> b) -> a -> b
$ \ (Maybe a, Maybe a)
xy -> case (Maybe a, Maybe a)
xy of
            ( Just a
x, Just a
y ) -> a -> a -> m a
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => a -> a -> m a
plus a
x a
y
            ( Just a
x, Maybe a
Nothing ) -> a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
            ( Maybe a
Nothing, Just a
y ) -> a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
y
        Poly a -> m (Poly a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Poly a -> m (Poly a)) -> Poly a -> m (Poly a)
forall a b. (a -> b) -> a -> b
$ [a] -> Poly a
forall a. [a] -> Poly a
Poly [a]
bs
    minus :: forall (m :: * -> *). MonadSAT m => Poly a -> Poly a -> m (Poly a)
minus ( Poly [a]
xs ) ( Poly [a]
ys ) = do
        a
z <- Int -> m a
forall a (m :: * -> *). (Create a, MonadSAT m) => Int -> m a
forall (m :: * -> *). MonadSAT m => Int -> m a
create Int
0
        [a]
bs <- [(Maybe a, Maybe a)] -> ((Maybe a, Maybe a) -> m a) -> m [a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( [a] -> [a] -> [(Maybe a, Maybe a)]
forall a b. [a] -> [b] -> [(Maybe a, Maybe b)]
fullZip [a]
xs [a]
ys ) (((Maybe a, Maybe a) -> m a) -> m [a])
-> ((Maybe a, Maybe a) -> m a) -> m [a]
forall a b. (a -> b) -> a -> b
$ \ (Maybe a, Maybe a)
xy -> case (Maybe a, Maybe a)
xy of
            ( Just a
x, Just a
y ) -> a -> a -> m a
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => a -> a -> m a
minus a
x a
y
            ( Just a
x, Maybe a
Nothing ) -> a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
            ( Maybe a
Nothing, Just a
y ) -> a -> a -> m a
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => a -> a -> m a
minus a
z a
y
        Poly a -> m (Poly a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Poly a -> m (Poly a)) -> Poly a -> m (Poly a)
forall a b. (a -> b) -> a -> b
$ [a] -> Poly a
forall a. [a] -> Poly a
Poly [a]
bs
    times :: forall (m :: * -> *). MonadSAT m => Poly a -> Poly a -> m (Poly a)
times ( Poly [a]
xs ) ( Poly [a]
ys ) = case [a]
xs of
        [] -> Poly a -> m (Poly a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Poly a -> m (Poly a)) -> Poly a -> m (Poly a)
forall a b. (a -> b) -> a -> b
$ [a] -> Poly a
forall a. [a] -> Poly a
Poly []
        a
x : [a]
xs -> do
            [a]
xys <- [a] -> (a -> m a) -> m [a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [a]
ys ((a -> m a) -> m [a]) -> (a -> m a) -> m [a]
forall a b. (a -> b) -> a -> b
$ a -> a -> m a
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => a -> a -> m a
times a
x
            a
z <- Integer -> m a
forall a (m :: * -> *). (Constant a, MonadSAT m) => Integer -> m a
forall (m :: * -> *). MonadSAT m => Integer -> m a
constant Integer
0
            Poly [a]
rest <- Poly a -> Poly a -> m (Poly a)
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => Poly a -> Poly a -> m (Poly a)
times ([a] -> Poly a
forall a. [a] -> Poly a
Poly [a]
xs) ([a] -> Poly a
forall a. [a] -> Poly a
Poly [a]
ys)
            Poly a -> Poly a -> m (Poly a)
forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
forall (m :: * -> *). MonadSAT m => Poly a -> Poly a -> m (Poly a)
plus ( [a] -> Poly a
forall a. [a] -> Poly a
Poly [a]
xys ) ( [a] -> Poly a
forall a. [a] -> Poly a
Poly ([a] -> Poly a) -> [a] -> Poly a
forall a b. (a -> b) -> a -> b
$ a
z a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
rest )

fullZip :: [a] -> [b] -> [ (Maybe a, Maybe b) ]    
fullZip :: forall a b. [a] -> [b] -> [(Maybe a, Maybe b)]
fullZip [] [] = []
fullZip [] (b
y:[b]
ys) = (Maybe a
forall a. Maybe a
Nothing, b -> Maybe b
forall a. a -> Maybe a
Just b
y) (Maybe a, Maybe b) -> [(Maybe a, Maybe b)] -> [(Maybe a, Maybe b)]
forall a. a -> [a] -> [a]
: [a] -> [b] -> [(Maybe a, Maybe b)]
forall a b. [a] -> [b] -> [(Maybe a, Maybe b)]
fullZip [] [b]
ys
fullZip (a
x:[a]
xs) [] = (a -> Maybe a
forall a. a -> Maybe a
Just a
x, Maybe b
forall a. Maybe a
Nothing) (Maybe a, Maybe b) -> [(Maybe a, Maybe b)] -> [(Maybe a, Maybe b)]
forall a. a -> [a] -> [a]
: [a] -> [b] -> [(Maybe a, Maybe b)]
forall a b. [a] -> [b] -> [(Maybe a, Maybe b)]
fullZip [a]
xs []
fullZip (a
x:[a]
xs) (b
y:[b]
ys) = (a -> Maybe a
forall a. a -> Maybe a
Just a
x, b -> Maybe b
forall a. a -> Maybe a
Just b
y) (Maybe a, Maybe b) -> [(Maybe a, Maybe b)] -> [(Maybe a, Maybe b)]
forall a. a -> [a] -> [a]
: [a] -> [b] -> [(Maybe a, Maybe b)]
forall a b. [a] -> [b] -> [(Maybe a, Maybe b)]
fullZip [a]
xs [b]
ys