{-# 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
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
showList :: [Poly a] -> ShowS
$cshowList :: forall a. Show a => [Poly a] -> ShowS
show :: Poly a -> String
$cshow :: forall a. Show a => Poly a -> String
showsPrec :: Int -> Poly a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [a]
xs 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. [a] -> Poly a
Poly [b]
ys

derive :: Poly a -> m (Poly a)
derive ( Poly [a]
xs ) = do
    [a]
ys <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( forall a. Int -> [a] -> [a]
drop Int
1 forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [ Integer
0 .. ] [a]
xs ) forall a b. (a -> b) -> a -> b
$ \ (Integer
k,a
x) -> do
        a
f <- forall a (m :: * -> *). (Constant a, MonadSAT m) => Integer -> m a
constant Integer
k
        forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
times a
f a
x
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Poly a
Poly [a]
ys
    
constantTerm :: Poly a -> a
constantTerm ( Poly [a]
xs ) = forall a. [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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ Int
0 .. Int
degree ] forall a b. (a -> b) -> a -> b
$ \ Int
k -> forall a (m :: * -> *). (Create a, MonadSAT m) => Int -> m a
create Int
bits
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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
    [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Poly a
Poly []
    a
x : [a]
xs -> do
        Poly a
p <- Poly a -> Poly a -> m (Poly a)
compose ( forall a. [a] -> Poly a
Poly [a]
xs ) Poly a
q
        Poly a
pq <- forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
times Poly a
p Poly a
q
        forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
plus ( 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 <- forall a (m :: * -> *). (Create a, MonadSAT m) => Int -> m a
create Int
0
        [Boolean]
bs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( forall a b. [a] -> [b] -> [(Maybe a, Maybe b)]
fullZip [a]
xs [a]
ys ) 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 ) -> forall a (m :: * -> *).
(Numeric a, MonadSAT m) =>
a -> a -> m Boolean
equal a
x a
y
            ( Just a
x, Maybe a
Nothing ) -> forall a (m :: * -> *).
(Numeric a, MonadSAT m) =>
a -> a -> m Boolean
equal a
x a
z
            ( Maybe a
Nothing, Just a
y ) -> forall a (m :: * -> *).
(Numeric a, MonadSAT m) =>
a -> a -> m Boolean
equal a
z a
y
        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 <- forall a (m :: * -> *). (Create a, MonadSAT m) => Int -> m a
create Int
0
        [Boolean]
bs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( forall a b. [a] -> [b] -> [(Maybe a, Maybe b)]
fullZip [a]
xs [a]
ys ) 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 ) -> forall a (m :: * -> *).
(Numeric a, MonadSAT m) =>
a -> a -> m Boolean
greater_equal a
x a
y
            ( Just a
x, Maybe a
Nothing ) -> forall a (m :: * -> *).
(Numeric a, MonadSAT m) =>
a -> a -> m Boolean
greater_equal a
x a
z
            ( Maybe a
Nothing, Just a
y ) -> forall a (m :: * -> *).
(Numeric a, MonadSAT m) =>
a -> a -> m Boolean
greater_equal a
z a
y
        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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( forall a b. [a] -> [b] -> [(Maybe a, Maybe b)]
fullZip [a]
xs [a]
ys ) 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 ) -> forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
plus a
x a
y
            ( Just a
x, Maybe a
Nothing ) -> forall (m :: * -> *) a. Monad m => a -> m a
return a
x
            ( Maybe a
Nothing, Just a
y ) -> forall (m :: * -> *) a. Monad m => a -> m a
return a
y
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 <- forall a (m :: * -> *). (Create a, MonadSAT m) => Int -> m a
create Int
0
        [a]
bs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( forall a b. [a] -> [b] -> [(Maybe a, Maybe b)]
fullZip [a]
xs [a]
ys ) 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 ) -> forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
minus a
x a
y
            ( Just a
x, Maybe a
Nothing ) -> forall (m :: * -> *) a. Monad m => a -> m a
return a
x
            ( Maybe a
Nothing, Just a
y ) -> forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
minus a
z a
y
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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
        [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Poly a
Poly []
        a
x : [a]
xs -> do
            [a]
xys <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [a]
ys forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
times a
x
            a
z <- forall a (m :: * -> *). (Constant a, MonadSAT m) => Integer -> m a
constant Integer
0
            Poly [a]
rest <- forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
times (forall a. [a] -> Poly a
Poly [a]
xs) (forall a. [a] -> Poly a
Poly [a]
ys)
            forall a (m :: * -> *). (Numeric a, MonadSAT m) => a -> a -> m a
plus ( forall a. [a] -> Poly a
Poly [a]
xys ) ( forall a. [a] -> Poly a
Poly forall a b. (a -> b) -> a -> b
$ a
z 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) = (forall a. Maybe a
Nothing, forall a. a -> Maybe a
Just b
y) forall a. a -> [a] -> [a]
: forall a b. [a] -> [b] -> [(Maybe a, Maybe b)]
fullZip [] [b]
ys
fullZip (a
x:[a]
xs) [] = (forall a. a -> Maybe a
Just a
x, forall a. Maybe a
Nothing) forall a. a -> [a] -> [a]
: forall a b. [a] -> [b] -> [(Maybe a, Maybe b)]
fullZip [a]
xs []
fullZip (a
x:[a]
xs) (b
y:[b]
ys) = (forall a. a -> Maybe a
Just a
x, forall a. a -> Maybe a
Just b
y) forall a. a -> [a] -> [a]
: forall a b. [a] -> [b] -> [(Maybe a, Maybe b)]
fullZip [a]
xs [b]
ys