{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards #-}

module SoPSat.SoP (
  -- * SoP Types
  Atom,
  Symbol,
  Product,
  SoP,
  SoPE (..),
  ToSoP (..),

  -- * Operators
  (|+|),
  (|-|),
  (|*|),
  (|/|),
  (|^|),

  -- * Relations
  OrdRel (..),

  -- * Related
  constants,
  atoms,
  int,
  cons,
  symbol,
  func,

  -- * Predicates
  isConst,
  isFunction,
)
where

import Data.Set (Set, union)
import qualified Data.Set as S

import SoPSat.Internal.SoP

{- | Convertable to a sum of products
with `f` being type to represent functions
and `c` being type to represent constants
-}
class (Ord f, Ord c) => ToSoP f c a where
  toSoP :: a -> SoP f c

-- | Predicate for constant @Atom@s
isConst :: Atom f c -> Bool
isConst :: forall f c. Atom f c -> Bool
isConst (C c
_) = Bool
True
isConst Atom f c
_ = Bool
False

-- | Predicate for function @Atom@s
isFunction :: Atom f c -> Bool
isFunction :: forall f c. Atom f c -> Bool
isFunction (F f
_ [SoP f c]
_) = Bool
True
isFunction Atom f c
_ = Bool
False

instance (Ord f, Ord c) => ToSoP f c (Symbol f c) where
  toSoP :: Symbol f c -> SoP f c
toSoP Symbol f c
s = 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 [[Symbol f c] -> Product f c
forall f c. [Symbol f c] -> Product f c
P [Symbol f c
s]]

instance (Ord f, Ord c) => ToSoP f c (Product f c) where
  toSoP :: Product f c -> SoP f c
toSoP Product f c
p = 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
p]

instance (Ord f, Ord c) => ToSoP f c (SoP f c) where
  toSoP :: SoP f c -> SoP f c
toSoP = SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c
simplifySoP

-- | Order relationship
data OrdRel
  = -- | Less than or equal relationship
    LeR
  | -- | Equality relationship
    EqR
  | -- | Greater than or equal relationship
    GeR
  deriving (OrdRel -> OrdRel -> Bool
(OrdRel -> OrdRel -> Bool)
-> (OrdRel -> OrdRel -> Bool) -> Eq OrdRel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: OrdRel -> OrdRel -> Bool
== :: OrdRel -> OrdRel -> Bool
$c/= :: OrdRel -> OrdRel -> Bool
/= :: OrdRel -> OrdRel -> Bool
Eq, Eq OrdRel
Eq OrdRel =>
(OrdRel -> OrdRel -> Ordering)
-> (OrdRel -> OrdRel -> Bool)
-> (OrdRel -> OrdRel -> Bool)
-> (OrdRel -> OrdRel -> Bool)
-> (OrdRel -> OrdRel -> Bool)
-> (OrdRel -> OrdRel -> OrdRel)
-> (OrdRel -> OrdRel -> OrdRel)
-> Ord OrdRel
OrdRel -> OrdRel -> Bool
OrdRel -> OrdRel -> Ordering
OrdRel -> OrdRel -> OrdRel
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
$ccompare :: OrdRel -> OrdRel -> Ordering
compare :: OrdRel -> OrdRel -> Ordering
$c< :: OrdRel -> OrdRel -> Bool
< :: OrdRel -> OrdRel -> Bool
$c<= :: OrdRel -> OrdRel -> Bool
<= :: OrdRel -> OrdRel -> Bool
$c> :: OrdRel -> OrdRel -> Bool
> :: OrdRel -> OrdRel -> Bool
$c>= :: OrdRel -> OrdRel -> Bool
>= :: OrdRel -> OrdRel -> Bool
$cmax :: OrdRel -> OrdRel -> OrdRel
max :: OrdRel -> OrdRel -> OrdRel
$cmin :: OrdRel -> OrdRel -> OrdRel
min :: OrdRel -> OrdRel -> OrdRel
Ord)

instance Show OrdRel where
  show :: OrdRel -> String
show OrdRel
LeR = String
"<="
  show OrdRel
EqR = String
"="
  show OrdRel
GeR = String
">="

-- | Expression
data SoPE f c
  = SoPE
  { forall f c. SoPE f c -> SoP f c
lhs :: SoP f c
  -- ^ Left hand side of the expression
  , forall f c. SoPE f c -> SoP f c
rhs :: SoP f c
  -- ^ Right hand side of the expression
  , forall f c. SoPE f c -> OrdRel
op :: OrdRel
  -- ^ Relationship between sides
  }

instance (Eq f, Eq c) => Eq (SoPE f c) where
  (SoPE SoP f c
l1 SoP f c
r1 OrdRel
op1) == :: SoPE f c -> SoPE f c -> Bool
== (SoPE SoP f c
l2 SoP f c
r2 OrdRel
op2)
    | OrdRel
op1 OrdRel -> OrdRel -> Bool
forall a. Eq a => a -> a -> Bool
== OrdRel
op2
    , OrdRel
op1 OrdRel -> OrdRel -> Bool
forall a. Eq a => a -> a -> Bool
== OrdRel
EqR =
        -- a = b is the same as b = a
        (SoP f c
l1 SoP f c -> SoP f c -> Bool
forall a. Eq a => a -> a -> Bool
== SoP f c
l2) Bool -> Bool -> Bool
&& (SoP f c
r1 SoP f c -> SoP f c -> Bool
forall a. Eq a => a -> a -> Bool
== SoP f c
r2) Bool -> Bool -> Bool
|| (SoP f c
l1 SoP f c -> SoP f c -> Bool
forall a. Eq a => a -> a -> Bool
== SoP f c
r2) Bool -> Bool -> Bool
&& (SoP f c
r1 SoP f c -> SoP f c -> Bool
forall a. Eq a => a -> a -> Bool
== SoP f c
l2)
    | OrdRel
op1 OrdRel -> OrdRel -> Bool
forall a. Eq a => a -> a -> Bool
== OrdRel
op2 =
        -- (a <= b) is itself
        (SoP f c
l1 SoP f c -> SoP f c -> Bool
forall a. Eq a => a -> a -> Bool
== SoP f c
l2) Bool -> Bool -> Bool
&& (SoP f c
r1 SoP f c -> SoP f c -> Bool
forall a. Eq a => a -> a -> Bool
== SoP f c
r2)
    | OrdRel
EqR OrdRel -> [OrdRel] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [OrdRel
op1, OrdRel
op2] =
        -- (a <= b) is the same as (b >= a)
        (SoP f c
l1 SoP f c -> SoP f c -> Bool
forall a. Eq a => a -> a -> Bool
== SoP f c
r2) Bool -> Bool -> Bool
&& (SoP f c
r1 SoP f c -> SoP f c -> Bool
forall a. Eq a => a -> a -> Bool
== SoP f c
l2)
    | Bool
otherwise =
        Bool
False

instance (Show f, Show c) => Show (SoPE f c) where
  show :: SoPE f c -> String
show SoPE{SoP f c
OrdRel
lhs :: forall f c. SoPE f c -> SoP f c
rhs :: forall f c. SoPE f c -> SoP f c
op :: forall f c. SoPE f c -> OrdRel
lhs :: SoP f c
rhs :: SoP f c
op :: OrdRel
..} = [String] -> String
unwords [SoP f c -> String
forall a. Show a => a -> String
show SoP f c
lhs, OrdRel -> String
forall a. Show a => a -> String
show OrdRel
op, SoP f c -> String
forall a. Show a => a -> String
show SoP f c
rhs]

-- | Creates an integer expression
int :: Integer -> SoP f c
int :: forall f c. Integer -> SoP f c
int Integer
i = [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]]

-- | Creates expression from an atom
symbol :: Atom f c -> SoP f c
symbol :: forall f c. Atom f c -> SoP f c
symbol 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 [Atom f c -> Symbol f c
forall f c. Atom f c -> Symbol f c
A Atom f c
a]]

-- | Creates a constant expression
cons :: c -> SoP f c
cons :: forall c f. c -> SoP f c
cons c
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 [Atom f c -> Symbol f c
forall f c. Atom f c -> Symbol f c
A (c -> Atom f c
forall f c. c -> Atom f c
C c
c)]]

-- | Creates a function expression
func :: (Ord f, Ord c) => f -> [SoP f c] -> SoP f c
func :: forall f c. (Ord f, Ord c) => f -> [SoP f c] -> SoP f c
func f
f [SoP f c]
args = [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 [Atom f c -> Symbol f c
forall f c. Atom f c -> Symbol f c
A (f -> [SoP f c] -> Atom f c
forall f c. f -> [SoP f c] -> Atom f c
F f
f ((SoP f c -> SoP f c) -> [SoP f c] -> [SoP f c]
forall a b. (a -> b) -> [a] -> [b]
map SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c
simplifySoP [SoP f c]
args))]]

infixr 8 |^|

-- | Exponentiation of @SoP@s
(|^|) :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
-- It's a B2 combinator,
|^| :: 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
. 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)
-> (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
. 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

infixl 6 |+|

-- | Addition of @SoP@s
(|+|) :: (Ord f, Ord 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 -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
mergeSoPAdd

infixl 7 |*|

-- | Multiplication of @SoP@s
(|*|) :: (Ord f, Ord 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 -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
mergeSoPMul

infixl 6 |-|

-- | Subtraction of @SoP@s
(|-|) :: (Ord f, Ord 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 -> SoP f c -> SoP f c
forall f c. (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
mergeSoPSub

infixl 7 |/|

{- | Division of @SoP@s

Produces a tuple of a quotient and a remainder
NB. Not implemented
-}
(|/|) :: (Ord f, Ord c) => 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)
(|/|) = 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)
mergeSoPDiv

-- | Collects @Atom@s used in a @SoP@
atoms :: (Ord f, Ord c) => SoP f c -> Set (Atom f c)
atoms :: forall f c. (Ord f, Ord c) => SoP f c -> Set (Atom f c)
atoms = [Set (Atom f c)] -> Set (Atom f c)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set (Atom f c)] -> Set (Atom f c))
-> (SoP f c -> [Set (Atom f c)]) -> SoP f c -> Set (Atom f c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Product f c -> Set (Atom f c))
-> [Product f c] -> [Set (Atom f c)]
forall a b. (a -> b) -> [a] -> [b]
map Product f c -> Set (Atom f c)
forall f c. (Ord f, Ord c) => Product f c -> Set (Atom f c)
atomsProduct ([Product f c] -> [Set (Atom f c)])
-> (SoP f c -> [Product f c]) -> SoP f c -> [Set (Atom 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

{- | Collects @Atom@s used in a @Product@

Used by @atoms@
-}
atomsProduct :: (Ord f, Ord c) => Product f c -> Set (Atom f c)
atomsProduct :: forall f c. (Ord f, Ord c) => Product f c -> Set (Atom f c)
atomsProduct = [Set (Atom f c)] -> Set (Atom f c)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set (Atom f c)] -> Set (Atom f c))
-> (Product f c -> [Set (Atom f c)])
-> Product f c
-> Set (Atom f c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol f c -> Set (Atom f c)) -> [Symbol f c] -> [Set (Atom f c)]
forall a b. (a -> b) -> [a] -> [b]
map Symbol f c -> Set (Atom f c)
forall f c. (Ord f, Ord c) => Symbol f c -> Set (Atom f c)
atomsSymbol ([Symbol f c] -> [Set (Atom f c)])
-> (Product f c -> [Symbol f c]) -> Product f c -> [Set (Atom 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

{- | Collect @Atom@s used in @Symbol@s

Used by @atomsProduct@
-}
atomsSymbol ::
  (Ord f, Ord c) =>
  Symbol f c ->
  -- | - Empty - if the symbol is an integer
  --   - Singleton - if the symbol is an atom
  --   - Set of symbols - if the symbol is an exponentiation
  Set (Atom f c)
atomsSymbol :: forall f c. (Ord f, Ord c) => Symbol f c -> Set (Atom f c)
atomsSymbol (I Integer
_) = Set (Atom f c)
forall a. Set a
S.empty
atomsSymbol (A Atom f c
a) = Atom f c -> Set (Atom f c)
forall a. a -> Set a
S.singleton Atom f c
a
atomsSymbol (E SoP f c
b Product f c
p) = SoP f c -> Set (Atom f c)
forall f c. (Ord f, Ord c) => SoP f c -> Set (Atom f c)
atoms SoP f c
b Set (Atom f c) -> Set (Atom f c) -> Set (Atom f c)
forall a. Ord a => Set a -> Set a -> Set a
`union` Product f c -> Set (Atom f c)
forall f c. (Ord f, Ord c) => Product f c -> Set (Atom f c)
atomsProduct Product f c
p

{- | Collects constants used in @SoP@

Almost equivalent to
@Data.Set.filter isConst . atoms@
, but also collects constants used in functions
-}
constants :: (Ord f, Ord c) => SoP f c -> Set c
constants :: forall f c. (Ord f, Ord c) => SoP f c -> Set c
constants = [Set c] -> Set c
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set c] -> Set c) -> (SoP f c -> [Set c]) -> SoP f c -> Set c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Product f c -> Set c) -> [Product f c] -> [Set c]
forall a b. (a -> b) -> [a] -> [b]
map Product f c -> Set c
forall f c. (Ord f, Ord c) => Product f c -> Set c
constsProduct ([Product f c] -> [Set c])
-> (SoP f c -> [Product f c]) -> SoP f c -> [Set 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

{- | Collects constants used in @Product@

Used by @constants@
-}
constsProduct :: (Ord f, Ord c) => Product f c -> Set c
constsProduct :: forall f c. (Ord f, Ord c) => Product f c -> Set c
constsProduct = [Set c] -> Set c
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set c] -> Set c)
-> (Product f c -> [Set c]) -> Product f c -> Set c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol f c -> Set c) -> [Symbol f c] -> [Set c]
forall a b. (a -> b) -> [a] -> [b]
map Symbol f c -> Set c
forall f c. (Ord f, Ord c) => Symbol f c -> Set c
constsSymbol ([Symbol f c] -> [Set c])
-> (Product f c -> [Symbol f c]) -> Product f c -> [Set 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

{- | Collects constants used in @Symbol@

Used by @constsProduct@
-}
constsSymbol :: (Ord f, Ord c) => Symbol f c -> Set c
constsSymbol :: forall f c. (Ord f, Ord c) => Symbol f c -> Set c
constsSymbol (I Integer
_) = Set c
forall a. Set a
S.empty
constsSymbol (A Atom f c
a) = Atom f c -> Set c
forall f c. (Ord f, Ord c) => Atom f c -> Set c
constsAtom Atom f c
a
constsSymbol (E SoP f c
b Product f c
p) = SoP f c -> Set c
forall f c. (Ord f, Ord c) => SoP f c -> Set c
constants SoP f c
b Set c -> Set c -> Set c
forall a. Ord a => Set a -> Set a -> Set a
`union` Product f c -> Set c
forall f c. (Ord f, Ord c) => Product f c -> Set c
constsProduct Product f c
p

{- | Collects constants used in @Atom@

Used by @constsSymbol@
-}
constsAtom ::
  (Ord f, Ord c) =>
  Atom f c ->
  -- | Singleton - if the atom is a constant
  --   Set of constants - if the atom is a function
  Set c
constsAtom :: forall f c. (Ord f, Ord c) => Atom f c -> Set c
constsAtom (C c
c) = c -> Set c
forall a. a -> Set a
S.singleton c
c
constsAtom (F f
_ [SoP f c]
args) = [Set c] -> Set c
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set c] -> Set c) -> [Set c] -> Set c
forall a b. (a -> b) -> a -> b
$ (SoP f c -> Set c) -> [SoP f c] -> [Set c]
forall a b. (a -> b) -> [a] -> [b]
map SoP f c -> Set c
forall f c. (Ord f, Ord c) => SoP f c -> Set c
constants [SoP f c]
args