module SoPSat.Internal.SoP
where

-- External
import Data.Either (partitionEithers)
import Data.List (intercalate, sort)

{- | Atomic part of a @SoP@
like constants and unknown functions
-}
data Atom f c
  = -- | Constant
    C c
  | -- | Unknown function
    F f [SoP f c]
  deriving (Atom f c -> Atom f c -> Bool
(Atom f c -> Atom f c -> Bool)
-> (Atom f c -> Atom f c -> Bool) -> Eq (Atom f c)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall f c. (Eq c, Eq f) => Atom f c -> Atom f c -> Bool
$c== :: forall f c. (Eq c, Eq f) => Atom f c -> Atom f c -> Bool
== :: Atom f c -> Atom f c -> Bool
$c/= :: forall f c. (Eq c, Eq f) => Atom f c -> Atom f c -> Bool
/= :: Atom f c -> Atom f c -> Bool
Eq, Eq (Atom f c)
Eq (Atom f c) =>
(Atom f c -> Atom f c -> Ordering)
-> (Atom f c -> Atom f c -> Bool)
-> (Atom f c -> Atom f c -> Bool)
-> (Atom f c -> Atom f c -> Bool)
-> (Atom f c -> Atom f c -> Bool)
-> (Atom f c -> Atom f c -> Atom f c)
-> (Atom f c -> Atom f c -> Atom f c)
-> Ord (Atom f c)
Atom f c -> Atom f c -> Bool
Atom f c -> Atom f c -> Ordering
Atom f c -> Atom f c -> Atom f c
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall f c. (Ord c, Ord f) => Eq (Atom f c)
forall f c. (Ord c, Ord f) => Atom f c -> Atom f c -> Bool
forall f c. (Ord c, Ord f) => Atom f c -> Atom f c -> Ordering
forall f c. (Ord c, Ord f) => Atom f c -> Atom f c -> Atom f c
$ccompare :: forall f c. (Ord c, Ord f) => Atom f c -> Atom f c -> Ordering
compare :: Atom f c -> Atom f c -> Ordering
$c< :: forall f c. (Ord c, Ord f) => Atom f c -> Atom f c -> Bool
< :: Atom f c -> Atom f c -> Bool
$c<= :: forall f c. (Ord c, Ord f) => Atom f c -> Atom f c -> Bool
<= :: Atom f c -> Atom f c -> Bool
$c> :: forall f c. (Ord c, Ord f) => Atom f c -> Atom f c -> Bool
> :: Atom f c -> Atom f c -> Bool
$c>= :: forall f c. (Ord c, Ord f) => Atom f c -> Atom f c -> Bool
>= :: Atom f c -> Atom f c -> Bool
$cmax :: forall f c. (Ord c, Ord f) => Atom f c -> Atom f c -> Atom f c
max :: Atom f c -> Atom f c -> Atom f c
$cmin :: forall f c. (Ord c, Ord f) => Atom f c -> Atom f c -> Atom f c
min :: Atom f c -> Atom f c -> Atom f c
Ord)

instance (Show f, Show c) => Show (Atom f c) where
  show :: Atom f c -> String
show (C c
c) = c -> String
forall a. Show a => a -> String
show c
c
  show (F f
f [SoP f c]
args) = f -> String
forall a. Show a => a -> String
show f
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((SoP f c -> String) -> [SoP f c] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SoP f c -> String
forall a. Show a => a -> String
show [SoP f c]
args) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

{- | The most basic part used during reasoning:
- Numbers
- Atoms
- Exponents
-}
data Symbol f c
  = -- | Number in an expression
    I Integer
  | -- | Atom in an expression
    A (Atom f c)
  | -- | Exponentiation
    E (SoP f c) (Product f c)
  deriving (Symbol f c -> Symbol f c -> Bool
(Symbol f c -> Symbol f c -> Bool)
-> (Symbol f c -> Symbol f c -> Bool) -> Eq (Symbol f c)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall f c. (Eq c, Eq f) => Symbol f c -> Symbol f c -> Bool
$c== :: forall f c. (Eq c, Eq f) => Symbol f c -> Symbol f c -> Bool
== :: Symbol f c -> Symbol f c -> Bool
$c/= :: forall f c. (Eq c, Eq f) => Symbol f c -> Symbol f c -> Bool
/= :: Symbol f c -> Symbol f c -> Bool
Eq, Eq (Symbol f c)
Eq (Symbol f c) =>
(Symbol f c -> Symbol f c -> Ordering)
-> (Symbol f c -> Symbol f c -> Bool)
-> (Symbol f c -> Symbol f c -> Bool)
-> (Symbol f c -> Symbol f c -> Bool)
-> (Symbol f c -> Symbol f c -> Bool)
-> (Symbol f c -> Symbol f c -> Symbol f c)
-> (Symbol f c -> Symbol f c -> Symbol f c)
-> Ord (Symbol f c)
Symbol f c -> Symbol f c -> Bool
Symbol f c -> Symbol f c -> Ordering
Symbol f c -> Symbol f c -> Symbol f c
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall f c. (Ord c, Ord f) => Eq (Symbol f c)
forall f c. (Ord c, Ord f) => Symbol f c -> Symbol f c -> Bool
forall f c. (Ord c, Ord f) => Symbol f c -> Symbol f c -> Ordering
forall f c.
(Ord c, Ord f) =>
Symbol f c -> Symbol f c -> Symbol f c
$ccompare :: forall f c. (Ord c, Ord f) => Symbol f c -> Symbol f c -> Ordering
compare :: Symbol f c -> Symbol f c -> Ordering
$c< :: forall f c. (Ord c, Ord f) => Symbol f c -> Symbol f c -> Bool
< :: Symbol f c -> Symbol f c -> Bool
$c<= :: forall f c. (Ord c, Ord f) => Symbol f c -> Symbol f c -> Bool
<= :: Symbol f c -> Symbol f c -> Bool
$c> :: forall f c. (Ord c, Ord f) => Symbol f c -> Symbol f c -> Bool
> :: Symbol f c -> Symbol f c -> Bool
$c>= :: forall f c. (Ord c, Ord f) => Symbol f c -> Symbol f c -> Bool
>= :: Symbol f c -> Symbol f c -> Bool
$cmax :: forall f c.
(Ord c, Ord f) =>
Symbol f c -> Symbol f c -> Symbol f c
max :: Symbol f c -> Symbol f c -> Symbol f c
$cmin :: forall f c.
(Ord c, Ord f) =>
Symbol f c -> Symbol f c -> Symbol f c
min :: Symbol f c -> Symbol f c -> Symbol f c
Ord)

instance (Show f, Show c) => Show (Symbol f c) where
  show :: Symbol f c -> String
show (E SoP f c
s Product f c
p) = SoP f c -> String
forall a. Show a => a -> String
show SoP f c
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"^" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Product f c -> String
forall a. Show a => a -> String
show Product f c
p
  show (I Integer
i) = Integer -> String
forall a. Show a => a -> String
show Integer
i
  show (A Atom f c
a) = Atom f c -> String
forall a. Show a => a -> String
show Atom f c
a

-- | Product of symbols
newtype Product f c = P {forall f c. Product f c -> [Symbol f c]
unP :: [Symbol f c]}
  deriving (Product f c -> Product f c -> Bool
(Product f c -> Product f c -> Bool)
-> (Product f c -> Product f c -> Bool) -> Eq (Product f c)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall f c. (Eq f, Eq c) => Product f c -> Product f c -> Bool
$c== :: forall f c. (Eq f, Eq c) => Product f c -> Product f c -> Bool
== :: Product f c -> Product f c -> Bool
$c/= :: forall f c. (Eq f, Eq c) => Product f c -> Product f c -> Bool
/= :: Product f c -> Product f c -> Bool
Eq)

instance (Ord f, Ord c) => Ord (Product f c) where
  compare :: Product f c -> Product f c -> Ordering
compare (P [Symbol f c
x]) (P [Symbol f c
y]) = Symbol f c -> Symbol f c -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Symbol f c
x Symbol f c
y
  compare (P [Symbol f c
_]) (P (Symbol f c
_ : [Symbol f c]
_)) = Ordering
LT
  compare (P (Symbol f c
_ : [Symbol f c]
_)) (P [Symbol f c
_]) = Ordering
GT
  compare (P [Symbol f c]
xs) (P [Symbol f c]
ys) = [Symbol f c] -> [Symbol f c] -> Ordering
forall a. Ord a => a -> a -> Ordering
compare [Symbol f c]
xs [Symbol f c]
ys

instance (Show f, Show c) => Show (Product f c) where
  show :: Product f c -> String
show (P [Symbol f c
s]) = Symbol f c -> String
forall a. Show a => a -> String
show Symbol f c
s
  show (P [Symbol f c]
ss) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" * " ((Symbol f c -> String) -> [Symbol f c] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Symbol f c -> String
forall a. Show a => a -> String
show [Symbol f c]
ss) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

-- | Sum of Products
newtype SoP f c = S {forall f c. SoP f c -> [Product f c]
unS :: [Product f c]}
  deriving (Eq (SoP f c)
Eq (SoP f c) =>
(SoP f c -> SoP f c -> Ordering)
-> (SoP f c -> SoP f c -> Bool)
-> (SoP f c -> SoP f c -> Bool)
-> (SoP f c -> SoP f c -> Bool)
-> (SoP f c -> SoP f c -> Bool)
-> (SoP f c -> SoP f c -> SoP f c)
-> (SoP f c -> SoP f c -> SoP f c)
-> Ord (SoP f c)
SoP f c -> SoP f c -> Bool
SoP f c -> SoP f c -> Ordering
SoP f c -> SoP f c -> SoP f c
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall f c. (Ord f, Ord c) => Eq (SoP f c)
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> Bool
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> Ordering
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
$ccompare :: forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> Ordering
compare :: SoP f c -> SoP f c -> Ordering
$c< :: forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> Bool
< :: SoP f c -> SoP f c -> Bool
$c<= :: forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> Bool
<= :: SoP f c -> SoP f c -> Bool
$c> :: forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> Bool
> :: SoP f c -> SoP f c -> Bool
$c>= :: forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> Bool
>= :: SoP f c -> SoP f c -> Bool
$cmax :: forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
max :: SoP f c -> SoP f c -> SoP f c
$cmin :: forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
min :: SoP f c -> SoP f c -> SoP f c
Ord)

instance (Eq f, Eq c) => Eq (SoP f c) where
  (S []) == :: SoP f c -> SoP f c -> Bool
== (S [P [I Integer
0]]) = Bool
True
  (S [P [I Integer
0]]) == (S []) = Bool
True
  (S [Product f c]
ps1) == (S [Product f c]
ps2) = [Product f c]
ps1 [Product f c] -> [Product f c] -> Bool
forall a. Eq a => a -> a -> Bool
== [Product f c]
ps2

instance (Show f, Show c) => Show (SoP f c) where
  show :: SoP f c -> String
show (S [Product f c
p]) = Product f c -> String
forall a. Show a => a -> String
show Product f c
p
  show (S [Product f c]
ps) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" + " ((Product f c -> String) -> [Product f c] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Product f c -> String
forall a. Show a => a -> String
show [Product f c]
ps) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

mergeWith :: (a -> a -> Either a a) -> [a] -> [a]
mergeWith :: forall a. (a -> a -> Either a a) -> [a] -> [a]
mergeWith a -> a -> Either a a
_ [] = []
mergeWith a -> a -> Either a a
op (a
f : [a]
fs) = case [Either a a] -> ([a], [a])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either a a] -> ([a], [a])) -> [Either a a] -> ([a], [a])
forall a b. (a -> b) -> a -> b
$ (a -> Either a a) -> [a] -> [Either a a]
forall a b. (a -> b) -> [a] -> [b]
map (a -> a -> Either a a
`op` a
f) [a]
fs of
  ([], [a]
_) -> a
f a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (a -> a -> Either a a) -> [a] -> [a]
forall a. (a -> a -> Either a a) -> [a] -> [a]
mergeWith a -> a -> Either a a
op [a]
fs
  ([a]
updated, [a]
untouched) -> (a -> a -> Either a a) -> [a] -> [a]
forall a. (a -> a -> Either a a) -> [a] -> [a]
mergeWith a -> a -> Either a a
op ([a]
updated [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
untouched)

reduceExp :: (Ord f, Ord c) => Symbol f c -> Symbol f c
reduceExp :: forall f c. (Ord f, Ord c) => Symbol f c -> Symbol f c
reduceExp (E SoP f c
_ (P [I Integer
0])) = Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I Integer
1
reduceExp (E (S [P [I Integer
0]]) Product f c
_) = Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I Integer
0
reduceExp (E (S [P [I Integer
i]]) (P [I Integer
j]))
  | Integer
j Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 = Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I (Integer
i Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
j)
reduceExp (E (S [P [E SoP f c
k Product f c
i]]) Product f c
j) =
  case SoP f c -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
normaliseExp SoP f c
k ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [Product f c
e]) of
    (S [P [Symbol f c
s]]) -> Symbol f c
s
    SoP f c
_ -> SoP f c -> Product f c -> Symbol f c
forall f c. SoP f c -> Product f c -> Symbol f c
E SoP f c
k Product f c
e
 where
  e :: Product f c
e = [Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P ([Symbol f c] -> Product f c)
-> ([Symbol f c] -> [Symbol f c]) -> [Symbol f c] -> Product f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Symbol f c] -> [Symbol f c]
forall a. Ord a => [a] -> [a]
sort ([Symbol f c] -> [Symbol f c])
-> ([Symbol f c] -> [Symbol f c]) -> [Symbol f c] -> [Symbol f c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol f c -> Symbol f c) -> [Symbol f c] -> [Symbol f c]
forall a b. (a -> b) -> [a] -> [b]
map Symbol f c -> Symbol f c
forall f c. (Ord f, Ord c) => Symbol f c -> Symbol f c
reduceExp ([Symbol f c] -> Product f c) -> [Symbol f c] -> Product f c
forall a b. (a -> b) -> a -> b
$ (Symbol f c -> Symbol f c -> Either (Symbol f c) (Symbol f c))
-> [Symbol f c] -> [Symbol f c]
forall a. (a -> a -> Either a a) -> [a] -> [a]
mergeWith Symbol f c -> Symbol f c -> Either (Symbol f c) (Symbol f c)
forall f c.
(Ord f, Ord c) =>
Symbol f c -> Symbol f c -> Either (Symbol f c) (Symbol f c)
mergeS (Product f c -> [Symbol f c]
forall f c. Product f c -> [Symbol f c]
unP Product f c
i [Symbol f c] -> [Symbol f c] -> [Symbol f c]
forall a. [a] -> [a] -> [a]
++ Product f c -> [Symbol f c]
forall f c. Product f c -> [Symbol f c]
unP Product f c
j)
reduceExp Symbol f c
s = Symbol f c
s

mergeS ::
  (Ord f, Ord c) =>
  Symbol f c ->
  Symbol f c ->
  Either (Symbol f c) (Symbol f c)
mergeS :: forall f c.
(Ord f, Ord c) =>
Symbol f c -> Symbol f c -> Either (Symbol f c) (Symbol f c)
mergeS (I Integer
i) (I Integer
j) = Symbol f c -> Either (Symbol f c) (Symbol f c)
forall a b. a -> Either a b
Left (Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
j))
mergeS (I Integer
1) Symbol f c
r = Symbol f c -> Either (Symbol f c) (Symbol f c)
forall a b. a -> Either a b
Left Symbol f c
r
mergeS Symbol f c
l (I Integer
1) = Symbol f c -> Either (Symbol f c) (Symbol f c)
forall a b. a -> Either a b
Left Symbol f c
l
mergeS (I Integer
0) Symbol f c
_ = Symbol f c -> Either (Symbol f c) (Symbol f c)
forall a b. a -> Either a b
Left (Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I Integer
0)
mergeS Symbol f c
_ (I Integer
0) = Symbol f c -> Either (Symbol f c) (Symbol f c)
forall a b. a -> Either a b
Left (Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I Integer
0)
-- x * x^4 ==> x^5
mergeS Symbol f c
s (E (S [P [Symbol f c
s']]) (P [I Integer
i]))
  | Symbol f c
s Symbol f c -> Symbol f c -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol f c
s' =
      Symbol f c -> Either (Symbol f c) (Symbol f c)
forall a b. a -> Either a b
Left (SoP f c -> Product f c -> Symbol f c
forall f c. SoP f c -> Product f c -> Symbol f c
E ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [[Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P [Symbol f c
s']]) ([Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P [Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)]))
-- x^4 * x ==> x^5
mergeS (E (S [P [Symbol f c
s']]) (P [I Integer
i])) Symbol f c
s
  | Symbol f c
s Symbol f c -> Symbol f c -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol f c
s' =
      Symbol f c -> Either (Symbol f c) (Symbol f c)
forall a b. a -> Either a b
Left (SoP f c -> Product f c -> Symbol f c
forall f c. SoP f c -> Product f c -> Symbol f c
E ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [[Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P [Symbol f c
s']]) ([Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P [Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)]))
-- 4^x * 2^x ==> 8^x
mergeS (E (S [P [I Integer
i]]) Product f c
p) (E (S [P [I Integer
j]]) Product f c
p')
  | Product f c
p Product f c -> Product f c -> Bool
forall a. Eq a => a -> a -> Bool
== Product f c
p' =
      Symbol f c -> Either (Symbol f c) (Symbol f c)
forall a b. a -> Either a b
Left (SoP f c -> Product f c -> Symbol f c
forall f c. SoP f c -> Product f c -> Symbol f c
E ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [[Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P [Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
j)]]) Product f c
p)
-- y*y ==> y^2
mergeS Symbol f c
l Symbol f c
r
  | Symbol f c
l Symbol f c -> Symbol f c -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol f c
r =
      case SoP f c -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
normaliseExp ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [[Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P [Symbol f c
l]]) ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [[Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P [Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I Integer
2]]) of
        (S [P [Symbol f c
e]]) -> Symbol f c -> Either (Symbol f c) (Symbol f c)
forall a b. a -> Either a b
Left Symbol f c
e
        SoP f c
_ -> Symbol f c -> Either (Symbol f c) (Symbol f c)
forall a b. b -> Either a b
Right Symbol f c
l
-- x^y * x^(-y) ==> 1
mergeS (E SoP f c
s1 (P [Symbol f c]
p1)) (E SoP f c
s2 (P (I Integer
i : [Symbol f c]
p2)))
  | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== (-Integer
1)
  , SoP f c
s1 SoP f c -> SoP f c -> Bool
forall a. Eq a => a -> a -> Bool
== SoP f c
s2
  , [Symbol f c]
p1 [Symbol f c] -> [Symbol f c] -> Bool
forall a. Eq a => a -> a -> Bool
== [Symbol f c]
p2 =
      Symbol f c -> Either (Symbol f c) (Symbol f c)
forall a b. a -> Either a b
Left (Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I Integer
1)
-- x^(-y) * x^y ==> 1
mergeS (E SoP f c
s1 (P (I Integer
i : [Symbol f c]
p1))) (E SoP f c
s2 (P [Symbol f c]
p2))
  | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== (-Integer
1)
  , SoP f c
s1 SoP f c -> SoP f c -> Bool
forall a. Eq a => a -> a -> Bool
== SoP f c
s2
  , [Symbol f c]
p1 [Symbol f c] -> [Symbol f c] -> Bool
forall a. Eq a => a -> a -> Bool
== [Symbol f c]
p2 =
      Symbol f c -> Either (Symbol f c) (Symbol f c)
forall a b. a -> Either a b
Left (Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I Integer
1)
mergeS Symbol f c
l Symbol f c
_ = Symbol f c -> Either (Symbol f c) (Symbol f c)
forall a b. b -> Either a b
Right Symbol f c
l

mergeP ::
  (Eq f, Eq c) =>
  Product f c ->
  Product f c ->
  Either (Product f c) (Product f c)
-- 2xy + 3xy ==> 5xy
mergeP :: forall f c.
(Eq f, Eq c) =>
Product f c -> Product f c -> Either (Product f c) (Product f c)
mergeP (P ((I Integer
i) : [Symbol f c]
is)) (P ((I Integer
j) : [Symbol f c]
js))
  | [Symbol f c]
is [Symbol f c] -> [Symbol f c] -> Bool
forall a. Eq a => a -> a -> Bool
== [Symbol f c]
js = Product f c -> Either (Product f c) (Product f c)
forall a b. a -> Either a b
Left (Product f c -> Either (Product f c) (Product f c))
-> ([Symbol f c] -> Product f c)
-> [Symbol f c]
-> Either (Product f c) (Product f c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P ([Symbol f c] -> Either (Product f c) (Product f c))
-> [Symbol f c] -> Either (Product f c) (Product f c)
forall a b. (a -> b) -> a -> b
$ Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j) Symbol f c -> [Symbol f c] -> [Symbol f c]
forall a. a -> [a] -> [a]
: [Symbol f c]
is
-- 2xy + xy  ==> 3xy
mergeP (P ((I Integer
i) : [Symbol f c]
is)) (P [Symbol f c]
js)
  | [Symbol f c]
is [Symbol f c] -> [Symbol f c] -> Bool
forall a. Eq a => a -> a -> Bool
== [Symbol f c]
js = Product f c -> Either (Product f c) (Product f c)
forall a b. a -> Either a b
Left (Product f c -> Either (Product f c) (Product f c))
-> ([Symbol f c] -> Product f c)
-> [Symbol f c]
-> Either (Product f c) (Product f c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P ([Symbol f c] -> Either (Product f c) (Product f c))
-> [Symbol f c] -> Either (Product f c) (Product f c)
forall a b. (a -> b) -> a -> b
$ Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Symbol f c -> [Symbol f c] -> [Symbol f c]
forall a. a -> [a] -> [a]
: [Symbol f c]
is
-- xy + 2xy  ==> 3xy
mergeP (P [Symbol f c]
is) (P ((I Integer
j) : [Symbol f c]
js))
  | [Symbol f c]
is [Symbol f c] -> [Symbol f c] -> Bool
forall a. Eq a => a -> a -> Bool
== [Symbol f c]
js = Product f c -> Either (Product f c) (Product f c)
forall a b. a -> Either a b
Left (Product f c -> Either (Product f c) (Product f c))
-> ([Symbol f c] -> Product f c)
-> [Symbol f c]
-> Either (Product f c) (Product f c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P ([Symbol f c] -> Either (Product f c) (Product f c))
-> [Symbol f c] -> Either (Product f c) (Product f c)
forall a b. (a -> b) -> a -> b
$ Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I (Integer
j Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Symbol f c -> [Symbol f c] -> [Symbol f c]
forall a. a -> [a] -> [a]
: [Symbol f c]
is
-- xy + xy ==> 2xy
mergeP (P [Symbol f c]
is) (P [Symbol f c]
js)
  | [Symbol f c]
is [Symbol f c] -> [Symbol f c] -> Bool
forall a. Eq a => a -> a -> Bool
== [Symbol f c]
js = Product f c -> Either (Product f c) (Product f c)
forall a b. a -> Either a b
Left (Product f c -> Either (Product f c) (Product f c))
-> ([Symbol f c] -> Product f c)
-> [Symbol f c]
-> Either (Product f c) (Product f c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P ([Symbol f c] -> Either (Product f c) (Product f c))
-> [Symbol f c] -> Either (Product f c) (Product f c)
forall a b. (a -> b) -> a -> b
$ Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I Integer
2 Symbol f c -> [Symbol f c] -> [Symbol f c]
forall a. a -> [a] -> [a]
: [Symbol f c]
is
  | Bool
otherwise = Product f c -> Either (Product f c) (Product f c)
forall a b. b -> Either a b
Right (Product f c -> Either (Product f c) (Product f c))
-> Product f c -> Either (Product f c) (Product f c)
forall a b. (a -> b) -> a -> b
$ [Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P [Symbol f c]
is

normaliseExp :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
-- b^1 ==> b
normaliseExp :: forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
normaliseExp SoP f c
b (S [P [I Integer
1]]) = SoP f c
b
-- x^(2xy) ==> x^(2xy)
normaliseExp b :: SoP f c
b@(S [P [A Atom f c
_]]) (S [Product f c
e]) = [Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [[Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P [SoP f c -> Product f c -> Symbol f c
forall f c. SoP f c -> Product f c -> Symbol f c
E SoP f c
b Product f c
e]]
-- 2^(y^2) ==> 4^y
normaliseExp b :: SoP f c
b@(S [P [Symbol f c
_]]) (S [e :: Product f c
e@(P [Symbol f c
_])]) = [Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [[Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P [Symbol f c -> Symbol f c
forall f c. (Ord f, Ord c) => Symbol f c -> Symbol f c
reduceExp (SoP f c -> Product f c -> Symbol f c
forall f c. SoP f c -> Product f c -> Symbol f c
E SoP f c
b Product f c
e)]]
-- (x + 2)^2 ==> x^2 + 4xy + 4
normaliseExp SoP f c
b (S [P [I Integer
i]])
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 =
      (SoP f c -> SoP f c -> SoP f c) -> [SoP f c] -> SoP f c
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 SoP f c -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
mergeSoPMul (Int -> SoP f c -> [SoP f c]
forall a. Int -> a -> [a]
replicate (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i) SoP f c
b)
-- (x + 2)^(2x) ==> (x^2 + 4xy + 4)^x
normaliseExp SoP f c
b (S [P (e :: Symbol f c
e@(I Integer
i) : [Symbol f c]
es)])
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 =
      -- Without the "| i >= 0" guard, normaliseExp can loop with itself
      -- for exponentials such as: 2^(n-k)
      SoP f c -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
normaliseExp (SoP f c -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
normaliseExp SoP f c
b ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [[Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P [Symbol f c
e]])) ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [[Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P [Symbol f c]
es])
-- (x + 2)^(xy) ==> (x+2)^(xy)
normaliseExp SoP f c
b (S [Product f c
e]) = [Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [[Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P [Symbol f c -> Symbol f c
forall f c. (Ord f, Ord c) => Symbol f c -> Symbol f c
reduceExp (SoP f c -> Product f c -> Symbol f c
forall f c. SoP f c -> Product f c -> Symbol f c
E SoP f c
b Product f c
e)]]
-- (x + 2)^(y + 2) ==> 4x(2 + x)^y + 4(2 + x)^y + (2 + x)^yx^2
normaliseExp SoP f c
b (S [Product f c]
e) = (SoP f c -> SoP f c -> SoP f c) -> [SoP f c] -> SoP f c
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 SoP f c -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
mergeSoPMul ((Product f c -> SoP f c) -> [Product f c] -> [SoP f c]
forall a b. (a -> b) -> [a] -> [b]
map (SoP f c -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
normaliseExp SoP f c
b (SoP f c -> SoP f c)
-> (Product f c -> SoP f c) -> Product f c -> SoP f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S ([Product f c] -> SoP f c)
-> (Product f c -> [Product f c]) -> Product f c -> SoP f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Product f c -> [Product f c] -> [Product f c]
forall a. a -> [a] -> [a]
: [])) [Product f c]
e)

zeroP :: Product f c -> Bool
zeroP :: forall f c. Product f c -> Bool
zeroP (P ((I Integer
0) : [Symbol f c]
_)) = Bool
True
zeroP Product f c
_ = Bool
False

mkNonEmpty :: (Ord f, Ord c) => SoP f c -> SoP f c
mkNonEmpty :: forall f c. (Ord f, Ord c) => SoP f c -> SoP f c
mkNonEmpty (S []) = [Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [[Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P [Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I Integer
0]]
mkNonEmpty SoP f c
s = SoP f c
s

simplifySoP :: (Ord f, Ord c) => SoP f c -> SoP f c
simplifySoP :: forall f c. (Ord f, Ord c) => SoP f c -> SoP f c
simplifySoP = (SoP f c -> SoP f c) -> SoP f c -> SoP f c
forall {t}. Eq t => (t -> t) -> t -> t
repeatF SoP f c -> SoP f c
go
 where
  go :: SoP f c -> SoP f c
go =
    SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c
mkNonEmpty
      (SoP f c -> SoP f c) -> (SoP f c -> SoP f c) -> SoP f c -> SoP f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S
      ([Product f c] -> SoP f c)
-> (SoP f c -> [Product f c]) -> SoP f c -> SoP f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Product f c] -> [Product f c]
forall a. Ord a => [a] -> [a]
sort
      ([Product f c] -> [Product f c])
-> (SoP f c -> [Product f c]) -> SoP f c -> [Product f c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Product f c -> Bool) -> [Product f c] -> [Product f c]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Product f c -> Bool) -> Product f c -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Product f c -> Bool
forall f c. Product f c -> Bool
zeroP)
      ([Product f c] -> [Product f c])
-> (SoP f c -> [Product f c]) -> SoP f c -> [Product f c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Product f c -> Product f c -> Either (Product f c) (Product f c))
-> [Product f c] -> [Product f c]
forall a. (a -> a -> Either a a) -> [a] -> [a]
mergeWith Product f c -> Product f c -> Either (Product f c) (Product f c)
forall f c.
(Eq f, Eq c) =>
Product f c -> Product f c -> Either (Product f c) (Product f c)
mergeP
      ([Product f c] -> [Product f c])
-> (SoP f c -> [Product f c]) -> SoP f c -> [Product f c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Product f c -> Product f c) -> [Product f c] -> [Product f c]
forall a b. (a -> b) -> [a] -> [b]
map ([Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P ([Symbol f c] -> Product f c)
-> (Product f c -> [Symbol f c]) -> Product f c -> Product f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Symbol f c] -> [Symbol f c]
forall a. Ord a => [a] -> [a]
sort ([Symbol f c] -> [Symbol f c])
-> (Product f c -> [Symbol f c]) -> Product f c -> [Symbol f c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol f c -> Symbol f c) -> [Symbol f c] -> [Symbol f c]
forall a b. (a -> b) -> [a] -> [b]
map Symbol f c -> Symbol f c
forall f c. (Ord f, Ord c) => Symbol f c -> Symbol f c
reduceExp ([Symbol f c] -> [Symbol f c])
-> (Product f c -> [Symbol f c]) -> Product f c -> [Symbol f c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol f c -> Symbol f c -> Either (Symbol f c) (Symbol f c))
-> [Symbol f c] -> [Symbol f c]
forall a. (a -> a -> Either a a) -> [a] -> [a]
mergeWith Symbol f c -> Symbol f c -> Either (Symbol f c) (Symbol f c)
forall f c.
(Ord f, Ord c) =>
Symbol f c -> Symbol f c -> Either (Symbol f c) (Symbol f c)
mergeS ([Symbol f c] -> [Symbol f c])
-> (Product f c -> [Symbol f c]) -> Product f c -> [Symbol f c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Product f c -> [Symbol f c]
forall f c. Product f c -> [Symbol f c]
unP)
      ([Product f c] -> [Product f c])
-> (SoP f c -> [Product f c]) -> SoP f c -> [Product f c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SoP f c -> [Product f c]
forall f c. SoP f c -> [Product f c]
unS

  repeatF :: (t -> t) -> t -> t
repeatF t -> t
f t
x =
    let x' :: t
x' = t -> t
f t
x
     in if t
x' t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
x
          then t
x
          else (t -> t) -> t -> t
repeatF t -> t
f t
x'
{-# INLINEABLE simplifySoP #-}

mergeSoPAdd :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
mergeSoPAdd :: forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
mergeSoPAdd (S [Product f c]
ps1) (S [Product f c]
ps2) = SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c
simplifySoP (SoP f c -> SoP f c) -> SoP f c -> SoP f c
forall a b. (a -> b) -> a -> b
$ [Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S ([Product f c]
ps1 [Product f c] -> [Product f c] -> [Product f c]
forall a. [a] -> [a] -> [a]
++ [Product f c]
ps2)

mergeSoPMul :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
mergeSoPMul :: forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
mergeSoPMul (S [Product f c]
ps1) (S [Product f c]
ps2) =
  SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c
simplifySoP (SoP f c -> SoP f c)
-> ([Product f c] -> SoP f c) -> [Product f c] -> SoP f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S ([Product f c] -> SoP f c) -> [Product f c] -> SoP f c
forall a b. (a -> b) -> a -> b
$
    (Product f c -> [Product f c]) -> [Product f c] -> [Product f c]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Product f c -> Product f c -> Product f c)
-> [Product f c] -> [Product f c] -> [Product f c]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Product f c
p1 Product f c
p2 -> [Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P (Product f c -> [Symbol f c]
forall f c. Product f c -> [Symbol f c]
unP Product f c
p1 [Symbol f c] -> [Symbol f c] -> [Symbol f c]
forall a. [a] -> [a] -> [a]
++ Product f c -> [Symbol f c]
forall f c. Product f c -> [Symbol f c]
unP Product f c
p2)) [Product f c]
ps1 ([Product f c] -> [Product f c])
-> (Product f c -> [Product f c]) -> Product f c -> [Product f c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Product f c -> [Product f c]
forall a. a -> [a]
repeat) [Product f c]
ps2

mergeSoPSub :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
mergeSoPSub :: forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
mergeSoPSub SoP f c
a SoP f c
b = SoP f c -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
mergeSoPAdd SoP f c
a (SoP f c -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
mergeSoPMul ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [[Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P [Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I (-Integer
1)]]) SoP f c
b)

mergeSoPDiv :: (Ord f, Ord c) => SoP f c -> SoP f c -> (SoP f c, SoP f c)
mergeSoPDiv :: forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> (SoP f c, SoP f c)
mergeSoPDiv (S [Product f c]
_ps1) (S [Product f c]
_ps2) = (SoP f c, SoP f c)
forall a. HasCallStack => a
undefined