{-# LANGUAGE RecordWildCards #-}

module SoPSat.Internal.Unify
where

import Data.Function (on)
import Data.List (find, intersect, nub, partition, (\\))

import SoPSat.Internal.SoP (
  Atom (..),
  Product (..),
  SoP (..),
  Symbol (..),
 )
import SoPSat.SoP (
  toSoP,
  (|*|),
  (|+|),
  (|-|),
  (|^|),
 )
import qualified SoPSat.SoP as SoP

data Unifier f c
  = Subst
  { forall f c. Unifier f c -> Atom f c
sConst :: Atom f c
  , forall f c. Unifier f c -> SoP f c
sSoP :: SoP f c
  }
  deriving (Unifier f c -> Unifier f c -> Bool
(Unifier f c -> Unifier f c -> Bool)
-> (Unifier f c -> Unifier f c -> Bool) -> Eq (Unifier f c)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall f c. (Eq c, Eq f) => Unifier f c -> Unifier f c -> Bool
$c== :: forall f c. (Eq c, Eq f) => Unifier f c -> Unifier f c -> Bool
== :: Unifier f c -> Unifier f c -> Bool
$c/= :: forall f c. (Eq c, Eq f) => Unifier f c -> Unifier f c -> Bool
/= :: Unifier f c -> Unifier f c -> Bool
Eq, Int -> Unifier f c -> ShowS
[Unifier f c] -> ShowS
Unifier f c -> String
(Int -> Unifier f c -> ShowS)
-> (Unifier f c -> String)
-> ([Unifier f c] -> ShowS)
-> Show (Unifier f c)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall f c. (Show f, Show c) => Int -> Unifier f c -> ShowS
forall f c. (Show f, Show c) => [Unifier f c] -> ShowS
forall f c. (Show f, Show c) => Unifier f c -> String
$cshowsPrec :: forall f c. (Show f, Show c) => Int -> Unifier f c -> ShowS
showsPrec :: Int -> Unifier f c -> ShowS
$cshow :: forall f c. (Show f, Show c) => Unifier f c -> String
show :: Unifier f c -> String
$cshowList :: forall f c. (Show f, Show c) => [Unifier f c] -> ShowS
showList :: [Unifier f c] -> ShowS
Show)

substsSoP :: (Ord f, Ord c) => [Unifier f c] -> SoP f c -> SoP f c
substsSoP :: forall f c. (Ord f, Ord c) => [Unifier f c] -> SoP f c -> SoP f c
substsSoP [] SoP f c
u = SoP f c
u
substsSoP ((Subst{SoP f c
Atom f c
sConst :: forall f c. Unifier f c -> Atom f c
sSoP :: forall f c. Unifier f c -> SoP f c
sConst :: Atom f c
sSoP :: SoP f c
..}) : [Unifier f c]
s) SoP f c
u = [Unifier f c] -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => [Unifier f c] -> SoP f c -> SoP f c
substsSoP [Unifier f c]
s (Atom f c -> SoP f c -> SoP f c -> SoP f c
forall f c.
(Ord f, Ord c) =>
Atom f c -> SoP f c -> SoP f c -> SoP f c
substSoP Atom f c
sConst SoP f c
sSoP SoP f c
u)

substSoP :: (Ord f, Ord c) => Atom f c -> SoP f c -> SoP f c -> SoP f c
substSoP :: forall f c.
(Ord f, Ord c) =>
Atom f c -> SoP f c -> SoP f c -> SoP f c
substSoP Atom f c
cons SoP f c
subs = (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
(|+|) ([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) -> [Product f c] -> [SoP f c]
forall a b. (a -> b) -> [a] -> [b]
map (Atom f c -> SoP f c -> Product f c -> SoP f c
forall f c.
(Ord f, Ord c) =>
Atom f c -> SoP f c -> Product f c -> SoP f c
substProduct Atom f c
cons SoP f c
subs) ([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
. SoP f c -> [Product f c]
forall f c. SoP f c -> [Product f c]
unS

substProduct :: (Ord f, Ord c) => Atom f c -> SoP f c -> Product f c -> SoP f c
substProduct :: forall f c.
(Ord f, Ord c) =>
Atom f c -> SoP f c -> Product f c -> SoP f c
substProduct Atom f c
cons SoP f c
subs = (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
(|*|) ([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
. (Symbol f c -> SoP f c) -> [Symbol f c] -> [SoP f c]
forall a b. (a -> b) -> [a] -> [b]
map (Atom f c -> SoP f c -> Symbol f c -> SoP f c
forall f c.
(Ord f, Ord c) =>
Atom f c -> SoP f c -> Symbol f c -> SoP f c
substSymbol Atom f c
cons SoP f c
subs) ([Symbol f c] -> [SoP f c])
-> (Product f c -> [Symbol f c]) -> Product f c -> [SoP 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

substSymbol :: (Ord f, Ord c) => Atom f c -> SoP f c -> Symbol f c -> SoP f c
substSymbol :: forall f c.
(Ord f, Ord c) =>
Atom f c -> SoP f c -> Symbol f c -> SoP f c
substSymbol Atom f c
_ SoP f c
_ s :: Symbol f c
s@(I Integer
_) = Symbol f c -> SoP f c
forall f c a. ToSoP f c a => a -> SoP f c
toSoP Symbol f c
s
substSymbol Atom f c
cons SoP f c
subst s :: Symbol f c
s@(A Atom f c
a)
  | Atom f c
cons Atom f c -> Atom f c -> Bool
forall a. Eq a => a -> a -> Bool
== Atom f c
a = SoP f c
subst
  | Bool
otherwise = [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]]
substSymbol Atom f c
cons SoP f c
subst (E SoP f c
b Product f c
p) = Atom f c -> SoP f c -> SoP f c -> SoP f c
forall f c.
(Ord f, Ord c) =>
Atom f c -> SoP f c -> SoP f c -> SoP f c
substSoP Atom f c
cons SoP f c
subst 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
|^| Atom f c -> SoP f c -> Product f c -> SoP f c
forall f c.
(Ord f, Ord c) =>
Atom f c -> SoP f c -> Product f c -> SoP f c
substProduct Atom f c
cons SoP f c
subst Product f c
p

substsSubst :: (Ord f, Ord c) => [Unifier f c] -> [Unifier f c] -> [Unifier f c]
substsSubst :: forall f c.
(Ord f, Ord c) =>
[Unifier f c] -> [Unifier f c] -> [Unifier f c]
substsSubst [Unifier f c]
s = (Unifier f c -> Unifier f c) -> [Unifier f c] -> [Unifier f c]
forall a b. (a -> b) -> [a] -> [b]
map Unifier f c -> Unifier f c
subst
 where
  subst :: Unifier f c -> Unifier f c
subst sub :: Unifier f c
sub@(Subst{SoP f c
Atom f c
sConst :: forall f c. Unifier f c -> Atom f c
sSoP :: forall f c. Unifier f c -> SoP f c
sConst :: Atom f c
sSoP :: SoP f c
..}) = Unifier f c
sub{sSoP = substsSoP s sSoP}

unifiers :: (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers :: forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers (S [P [A Atom f c
a]]) (S []) = [Atom f c -> SoP f c -> Unifier f c
forall f c. Atom f c -> SoP f c -> Unifier f c
Subst Atom f c
a ([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]])]
unifiers (S []) (S [P [A Atom f c
a]]) = [Atom f c -> SoP f c -> Unifier f c
forall f c. Atom f c -> SoP f c -> Unifier f c
Subst Atom f c
a ([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]])]
unifiers (S [P [I Integer
_]]) (S [P [I Integer
_]]) = []
-- (z ^ a) ~ (z ^ b) ==> [a := b]
unifiers (S [P [E SoP f c
s1 Product f c
p1]]) (S [P [E SoP f c
s2 Product f c
p2]])
  | SoP f c
s1 SoP f c -> SoP f c -> Bool
forall a. Eq a => a -> a -> Bool
== SoP f c
s2 = SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers (Product f c -> SoP f c
forall f c a. ToSoP f c a => a -> SoP f c
toSoP Product f c
p1) (Product f c -> SoP f c
forall f c a. ToSoP f c a => a -> SoP f c
toSoP Product f c
p2)
-- (2*e ^ d) ~ (2*e*a*c) ==> [a*c := 2*e ^ (d-1)]
unifiers (S [P [E (S [P [Symbol f c]
s1]) Product f c
p1]]) (S [P [Symbol f c]
p2])
  | (Symbol f c -> Bool) -> [Symbol f c] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Symbol f c -> [Symbol f c] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol f c]
p2) [Symbol f c]
s1 =
      let base :: [Symbol f c]
base = [Symbol f c]
s1 [Symbol f c] -> [Symbol f c] -> [Symbol f c]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Symbol f c]
p2
          diff :: [Symbol f c]
diff = [Symbol f c]
p2 [Symbol f c] -> [Symbol f c] -> [Symbol f c]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol f c]
s1
       in SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers ([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]
diff]) ([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 ([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]
base]) ([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 -> 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]
base]) Product f c
p1]])
unifiers (S [P [Symbol f c]
p2]) (S [P [E (S [P [Symbol f c]
s1]) Product f c
p1]])
  | (Symbol f c -> Bool) -> [Symbol f c] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Symbol f c -> [Symbol f c] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol f c]
p2) [Symbol f c]
s1 =
      let base :: [Symbol f c]
base = [Symbol f c]
s1 [Symbol f c] -> [Symbol f c] -> [Symbol f c]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Symbol f c]
p2
          diff :: [Symbol f c]
diff = [Symbol f c]
p2 [Symbol f c] -> [Symbol f c] -> [Symbol f c]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol f c]
s1
       in SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers ([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]
diff]) ([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 ([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]
base]) ([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 -> 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]
base]) Product f c
p1]])
-- (i ^ a) ~ j ==> [a := round (logBase i j)], when `i` and `j` are integers,
unifiers (S [P [E (S [P [I Integer
i]]) Product f c
p]]) (S [P [I Integer
j]]) =
  case Integer -> Integer -> Maybe Integer
integerLogBase Integer
i Integer
j of
    Just Integer
k -> SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [Product f c
p]) ([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
k]])
    Maybe Integer
Nothing -> []
unifiers (S [P [I Integer
j]]) (S [P [E (S [P [I Integer
i]]) Product f c
p]]) =
  case Integer -> Integer -> Maybe Integer
integerLogBase Integer
i Integer
j of
    Just Integer
k -> SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [Product f c
p]) ([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
k]])
    Maybe Integer
Nothing -> []
-- x ^ i = j => [x := root i j]
unifiers (S [P [E SoP f c
s (P [I Integer
p])]]) (S [P [I Integer
j]]) =
  case Integer -> Integer -> Maybe Integer
integerRt Integer
p Integer
j of
    Just Integer
k -> SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers SoP f c
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
k]])
    Maybe Integer
Nothing -> []
unifiers (S [P [I Integer
j]]) (S [P [E SoP f c
s (P [I Integer
p])]]) =
  case Integer -> Integer -> Maybe Integer
integerRt Integer
p Integer
j of
    Just Integer
k -> SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers SoP f c
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
k]])
    Maybe Integer
Nothing -> []
-- a^d * a^e ~ a^c ==> [c := d + e]
unifiers (S [P [E SoP f c
s1 Product f c
p1]]) (S [Product f c
p2]) = case Product f c -> Maybe ([SoP f c], [Product f c])
forall f c. Product f c -> Maybe ([SoP f c], [Product f c])
collectBases Product f c
p2 of
  Just (SoP f c
b : [SoP f c]
bs, [Product f c]
ps)
    | (SoP f c -> Bool) -> [SoP f c] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SoP f c -> SoP f c -> Bool
forall a. Eq a => a -> a -> Bool
== SoP f c
s1) (SoP f c
b SoP f c -> [SoP f c] -> [SoP f c]
forall a. a -> [a] -> [a]
: [SoP f c]
bs) ->
        SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [Product f c
p1]) ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [Product f c]
ps)
  Maybe ([SoP f c], [Product f c])
_ -> []
unifiers (S [Product f c
p2]) (S [P [E SoP f c
s1 Product f c
p1]]) = case Product f c -> Maybe ([SoP f c], [Product f c])
forall f c. Product f c -> Maybe ([SoP f c], [Product f c])
collectBases Product f c
p2 of
  Just (SoP f c
b : [SoP f c]
bs, [Product f c]
ps)
    | (SoP f c -> Bool) -> [SoP f c] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SoP f c -> SoP f c -> Bool
forall a. Eq a => a -> a -> Bool
== SoP f c
s1) (SoP f c
b SoP f c -> [SoP f c] -> [SoP f c]
forall a. a -> [a] -> [a]
: [SoP f c]
bs) ->
        SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [Product f c]
ps) ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [Product f c
p1])
  Maybe ([SoP f c], [Product f c])
_ -> []
-- (i * a) ~ (j * b) ==> [a := (div j i) * b]
-- Where 'a' and 'b' are variables, 'i' and 'j' are integer literals, and j `mod` i == 0
unifiers (S [P ((I Integer
i) : [Symbol f c]
ps)]) (S [P ((I Integer
j) : [Symbol f c]
ps1)])
  | (Just Integer
k) <- Integer -> Integer -> Maybe Integer
safeDiv Integer
j Integer
i = SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers ([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]
ps]) (Integer -> SoP f c
forall f c. Integer -> SoP f c
SoP.int Integer
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
|*| [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]
ps1])
  | (Just Integer
k) <- Integer -> Integer -> Maybe Integer
safeDiv Integer
i Integer
j = SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers (Integer -> SoP f c
forall f c. Integer -> SoP f c
SoP.int Integer
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
|*| [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]
ps]) ([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]
ps1])
  | Bool
otherwise = []
-- (2*a) ~ (2*b) ==> [a := b]
-- unifiers (S [P (p:ps1)]) (S [P (p':ps2)])
--     | p == p'   = unifiers' ct (S [P ps1]) (S [P ps2])
--     | otherwise = []
unifiers (S [P ps1 :: [Symbol f c]
ps1@(Symbol f c
_ : Symbol f c
_ : [Symbol f c]
_)]) (S [P [Symbol f c]
ps2])
  | [Symbol f c] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol f c]
psx = []
  | Bool
otherwise = SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers ([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]
ps1'']) ([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]
ps2''])
 where
  ps1' :: [Symbol f c]
ps1' = [Symbol f c]
ps1 [Symbol f c] -> [Symbol f c] -> [Symbol f c]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol f c]
psx
  ps2' :: [Symbol f c]
ps2' = [Symbol f c]
ps2 [Symbol f c] -> [Symbol f c] -> [Symbol f c]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol f c]
psx
  ps1'' :: [Symbol f c]
ps1''
    | [Symbol f c] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol f c]
ps1' = [Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I Integer
1]
    | Bool
otherwise = [Symbol f c]
ps1'
  ps2'' :: [Symbol f c]
ps2''
    | [Symbol f c] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol f c]
ps2' = [Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I Integer
1]
    | Bool
otherwise = [Symbol f c]
ps2'
  psx :: [Symbol f c]
psx = [Symbol f c]
ps1 [Symbol f c] -> [Symbol f c] -> [Symbol f c]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Symbol f c]
ps2
unifiers (S [P [Symbol f c]
ps1]) (S [P ps2 :: [Symbol f c]
ps2@(Symbol f c
_ : Symbol f c
_ : [Symbol f c]
_)])
  | [Symbol f c] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol f c]
psx = []
  | Bool
otherwise = SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers ([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]
ps1'']) ([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]
ps2''])
 where
  ps1' :: [Symbol f c]
ps1' = [Symbol f c]
ps1 [Symbol f c] -> [Symbol f c] -> [Symbol f c]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol f c]
psx
  ps2' :: [Symbol f c]
ps2' = [Symbol f c]
ps2 [Symbol f c] -> [Symbol f c] -> [Symbol f c]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol f c]
psx
  ps1'' :: [Symbol f c]
ps1''
    | [Symbol f c] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol f c]
ps1' = [Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I Integer
1]
    | Bool
otherwise = [Symbol f c]
ps1'
  ps2'' :: [Symbol f c]
ps2''
    | [Symbol f c] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol f c]
ps2' = [Integer -> Symbol f c
forall f c. Integer -> Symbol f c
I Integer
1]
    | Bool
otherwise = [Symbol f c]
ps2'
  psx :: [Symbol f c]
psx = [Symbol f c]
ps1 [Symbol f c] -> [Symbol f c] -> [Symbol f c]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Symbol f c]
ps2
unifiers (S [P [A Atom f c
a]]) SoP f c
s = [Atom f c -> SoP f c -> Unifier f c
forall f c. Atom f c -> SoP f c -> Unifier f c
Subst Atom f c
a SoP f c
s]
unifiers SoP f c
s (S [P [A Atom f c
a]]) = [Atom f c -> SoP f c -> Unifier f c
forall f c. Atom f c -> SoP f c -> Unifier f c
Subst Atom f c
a SoP f c
s]
-- (2 + a) ~ 5 ==> [a := 3]
unifiers (S ((P [I Integer
i]) : [Product f c]
ps1)) (S ((P [I Integer
j]) : [Product f c]
ps2))
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
j = SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [Product f c]
ps1) ([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
j Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
i)] Product f c -> [Product f c] -> [Product f c]
forall a. a -> [a] -> [a]
: [Product f c]
ps2))
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
j = SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers ([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 -> [Product f c] -> [Product f c]
forall a. a -> [a] -> [a]
: [Product f c]
ps1)) ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [Product f c]
ps2)
-- (a + c) ~ (b + c) ==> [a := b]
unifiers s1 :: SoP f c
s1@(S [Product f c]
ps1) s2 :: SoP f c
s2@(S [Product f c]
ps2) = case SoP f c -> 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, SoP f c)
splitSoP SoP f c
s1 SoP f c
s2 of
  (SoP f c
s1', SoP f c
s2')
    | SoP f c
s1' SoP f c -> SoP f c -> Bool
forall a. Eq a => a -> a -> Bool
/= SoP f c
s1 Bool -> Bool -> Bool
|| SoP f c
s2' SoP f c -> SoP f c -> Bool
forall a. Eq a => a -> a -> Bool
/= SoP f c
s2 ->
        SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers SoP f c
s1' SoP f c
s2'
  (SoP f c, SoP f c)
_
    | [Product f c] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Product f c]
psx
    , [Product f c] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Product f c]
ps1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Product f c] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Product f c]
ps2 ->
        case [Unifier f c] -> [Unifier f c]
forall a. Eq a => [a] -> [a]
nub ([[Unifier f c]] -> [Unifier f c]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((Product f c -> Product f c -> [Unifier f c])
-> [Product f c] -> [Product f c] -> [[Unifier f c]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Product f c
x Product f c
y -> SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [Product f c
x]) ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [Product f c
y])) [Product f c]
ps1 [Product f c]
ps2)) of
          [] -> SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers' SoP f c
s1 SoP f c
s2
          [Unifier f c
k] -> [Unifier f c
k]
          [Unifier f c]
_ -> []
    | [Product f c] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Product f c]
psx ->
        SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers' SoP f c
s1 SoP f c
s2
  (SoP f c, SoP f c)
_ -> SoP f c -> SoP f c -> [Unifier f c]
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers' ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [Product f c]
ps1'') ([Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [Product f c]
ps2'')
 where
  ps1' :: [Product f c]
ps1' = [Product f c]
ps1 [Product f c] -> [Product f c] -> [Product f c]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Product f c]
psx
  ps2' :: [Product f c]
ps2' = [Product f c]
ps2 [Product f c] -> [Product f c] -> [Product f c]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Product f c]
psx
  ps1'' :: [Product f c]
ps1''
    | [Product f c] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Product f c]
ps1' = [[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]]
    | Bool
otherwise = [Product f c]
ps1'
  ps2'' :: [Product f c]
ps2''
    | [Product f c] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Product f c]
ps2' = [[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]]
    | Bool
otherwise = [Product f c]
ps2'
  psx :: [Product f c]
psx = [Product f c]
ps1 [Product f c] -> [Product f c] -> [Product f c]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Product f c]
ps2

unifiers' :: (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers' :: forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c]
unifiers' (S [P [I Integer
i], P [A Atom f c
a]]) SoP f c
s2 =
  [Atom f c -> SoP f c -> Unifier f c
forall f c. Atom f c -> SoP f c -> Unifier f c
Subst Atom f c
a (SoP f c
s2 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
|+| [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 -> Integer
forall a. Num a => a -> a
negate Integer
i)]])]
unifiers' SoP f c
s1 (S [P [I Integer
i], P [A Atom f c
a]]) =
  [Atom f c -> SoP f c -> Unifier f c
forall f c. Atom f c -> SoP f c -> Unifier f c
Subst Atom f c
a (SoP f c
s1 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
|+| [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 -> Integer
forall a. Num a => a -> a
negate Integer
i)]])]
unifiers' SoP f c
_ SoP f c
_ = []

splitSoP :: (Ord f, Ord c) => SoP f c -> SoP f c -> (SoP f c, SoP f c)
splitSoP :: forall f c.
(Ord f, Ord c) =>
SoP f c -> SoP f c -> (SoP f c, SoP f c)
splitSoP SoP f c
u SoP f c
v = (SoP f c
lhs, SoP f c
rhs)
 where
  reduced :: SoP f c
reduced = SoP f c
v 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
|-| SoP f c
u
  ([Product f c]
lhs', [Product f c]
rhs') = (Product f c -> Bool)
-> [Product f c] -> ([Product f c], [Product f c])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Product f c -> Bool
forall {f} {c}. Product f c -> Bool
neg (SoP f c -> [Product f c]
forall f c. SoP f c -> [Product f c]
unS SoP f c
reduced)
  lhs :: SoP f c
lhs
    | [Product f c] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Product f c]
lhs' = Integer -> SoP f c
forall f c. Integer -> SoP f c
SoP.int Integer
0
    | Bool
otherwise = (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
(|*|) (SoP f c -> SoP f c -> SoP f c)
-> ([Product f c] -> SoP f c)
-> [Product f c]
-> [Product f c]
-> SoP f c
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` [Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S) [Product f c]
lhs' [[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)]]
  rhs :: SoP f c
rhs
    | [Product f c] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Product f c]
rhs' = Integer -> SoP f c
forall f c. Integer -> SoP f c
SoP.int Integer
0
    | Bool
otherwise = [Product f c] -> SoP f c
forall f c. [Product f c] -> SoP f c
S [Product f c]
rhs'

  neg :: Product f c -> Bool
neg (P ((I Integer
i) : [Symbol f c]
_)) = Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
  neg Product f c
_ = Bool
False

collectBases :: Product f c -> Maybe ([SoP f c], [Product f c])
collectBases :: forall f c. Product f c -> Maybe ([SoP f c], [Product f c])
collectBases = ([(SoP f c, Product f c)] -> ([SoP f c], [Product f c]))
-> Maybe [(SoP f c, Product f c)]
-> Maybe ([SoP f c], [Product f c])
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(SoP f c, Product f c)] -> ([SoP f c], [Product f c])
forall a b. [(a, b)] -> ([a], [b])
unzip (Maybe [(SoP f c, Product f c)]
 -> Maybe ([SoP f c], [Product f c]))
-> (Product f c -> Maybe [(SoP f c, Product f c)])
-> Product f c
-> Maybe ([SoP f c], [Product f c])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol f c -> Maybe (SoP f c, Product f c))
-> [Symbol f c] -> Maybe [(SoP f c, Product f c)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Symbol f c -> Maybe (SoP f c, Product f c)
forall {f} {c}. Symbol f c -> Maybe (SoP f c, Product f c)
go ([Symbol f c] -> Maybe [(SoP f c, Product f c)])
-> (Product f c -> [Symbol f c])
-> Product f c
-> Maybe [(SoP f c, Product 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
 where
  go :: Symbol f c -> Maybe (SoP f c, Product f c)
go (E SoP f c
s1 Product f c
p1) = (SoP f c, Product f c) -> Maybe (SoP f c, Product f c)
forall a. a -> Maybe a
Just (SoP f c
s1, Product f c
p1)
  go Symbol f c
_ = Maybe (SoP f c, Product f c)
forall a. Maybe a
Nothing

safeDiv :: Integer -> Integer -> Maybe Integer
safeDiv :: Integer -> Integer -> Maybe Integer
safeDiv Integer
i Integer
j
  | Integer
j Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
  | Bool
otherwise = case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
i Integer
j of
      (Integer
k, Integer
0) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
k
      (Integer, Integer)
_ -> Maybe Integer
forall a. Maybe a
Nothing

integerLogBase :: Integer -> Integer -> Maybe Integer
integerLogBase :: Integer -> Integer -> Maybe Integer
integerLogBase Integer
x Integer
y
  | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
1 Bool -> Bool -> Bool
&& Integer
y Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 =
      let z1 :: Integer
z1 = Integer -> Integer -> Integer
integerLogBase' Integer
x Integer
y
          z2 :: Integer
z2 = Integer -> Integer -> Integer
integerLogBase' Integer
x (Integer
y Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
       in if Integer
z1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
z2
            then Maybe Integer
forall a. Maybe a
Nothing
            else Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
z1
integerLogBase Integer
_ Integer
_ = Maybe Integer
forall a. Maybe a
Nothing

integerLogBase' :: Integer -> Integer -> Integer
integerLogBase' :: Integer -> Integer -> Integer
integerLogBase' Integer
b Integer
m = (Integer, Integer) -> Integer
forall a b. (a, b) -> b
snd (Integer -> (Integer, Integer)
go Integer
b)
 where
  go :: Integer -> (Integer, Integer)
  go :: Integer -> (Integer, Integer)
go Integer
pw | Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
pw = (Integer
m, Integer
0)
  go Integer
pw = case Integer -> (Integer, Integer)
go (Integer
pw Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
2 :: Int)) of
    (Integer
q, Integer
e) | Integer
q Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
pw -> (Integer
q, Integer
2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
e)
    (Integer
q, Integer
e) -> (Integer
q Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
pw, Integer
2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
e Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)

-- Naive implementation of exact integer root
integerRt :: Integer -> Integer -> Maybe Integer
integerRt :: Integer -> Integer -> Maybe Integer
integerRt Integer
1 Integer
y = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
y
integerRt Integer
x Integer
y = (Integer -> Bool) -> [Integer] -> Maybe Integer
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
y) (Integer -> Bool) -> (Integer -> Integer) -> Integer -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
x)) [Integer
1 .. Integer
y]