{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE FlexibleInstances #-}

{-|
Module       : ATP.FirstOrder.Smart
Description  : Smart constructors for terms and formulas in first-order logic.
Copyright    : (c) Evgenii Kotelnikov, 2019-2021
License      : GPL-3
Maintainer   : evgeny.kotelnikov@gmail.com
Stability    : experimental
-}

module ATP.FirstOrder.Smart (
  -- * Smart constructors
  signed,
  unitClause,
  clause,
  singleClause,
  clauses,
  (===),
  (=/=),
  neg,
  (\/),
  (/\),
  (==>),
  (<=>),
  (<~>),
  Binder(..),
  forall,
  exists,
  (|-),

  -- * Monoids
  Conjunction(..),
  conjunction,
  Disjunction(..),
  disjunction,
  Equivalence(..),
  equivalence,
  Inequivalence(..),
  inequivalence,

  -- * Miscellaneous
  flattenConjunction,
  flattenDisjunction
) where

import Data.Coerce (coerce)
import qualified Data.Foldable as Foldable (toList)
#if !MIN_VERSION_base(4, 11, 0)
import Data.Semigroup (Semigroup(..))
#endif

import ATP.FirstOrder.Core

-- $setup
-- >>> :set -XOverloadedStrings
-- >>> :load Property.Generators
-- >>> let eq = binaryPredicate "eq"


-- * Smart constructors

infix  8 ===
infix  8 =/=
infixl 7 /\ --
infixl 6 \/
infixl 6 \./
infix  5 ==>
infixl 5 <=>
infixl 5 <~>
infix  2 |-

-- | A smart constructor for a signed literal.
signed :: Sign -> Literal -> Signed Literal
signed :: Sign -> Literal -> Signed Literal
signed Sign
Negative (Propositional Bool
b) = Sign -> Literal -> Signed Literal
forall e. Sign -> e -> Signed e
Signed Sign
Positive (Bool -> Literal
Propositional (Bool -> Bool
not Bool
b))
signed Sign
s Literal
l = Sign -> Literal -> Signed Literal
forall e. Sign -> e -> Signed e
Signed Sign
s Literal
l

-- | A smart constructor for a unit clause.
unitClause :: Signed Literal -> Clause
unitClause :: Signed Literal -> Clause
unitClause (Signed Sign
s Literal
l) = case Sign -> Literal -> Signed Literal
signed Sign
s Literal
l of
  Signed Literal
FalsityLiteral -> Clause
EmptyClause
  Signed Literal
sl -> Signed Literal -> Clause
UnitClause Signed Literal
sl

-- | A smart contructor for a clause.
-- 'clause' eliminates negated boolean constants, falsums and redundant tautologies.
clause :: Foldable f => f (Signed Literal) -> Clause
clause :: f (Signed Literal) -> Clause
clause = [Clause] -> Clause
forall (f :: * -> *). Foldable f => f Clause -> Clause
clauseUnion ([Clause] -> Clause)
-> (f (Signed Literal) -> [Clause]) -> f (Signed Literal) -> Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Signed Literal -> Clause) -> [Signed Literal] -> [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Signed Literal -> Clause
unitClause ([Signed Literal] -> [Clause])
-> (f (Signed Literal) -> [Signed Literal])
-> f (Signed Literal)
-> [Clause]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (Signed Literal) -> [Signed Literal]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList

-- | A smart constructor for a set of clauses with a single clause in it.
singleClause :: Clause -> Clauses
singleClause :: Clause -> Clauses
singleClause (Literals [Signed Literal]
ls) = case [Signed Literal] -> Clause
forall (f :: * -> *). Foldable f => f (Signed Literal) -> Clause
clause [Signed Literal]
ls of
  Clause
TautologyClause -> Clauses
NoClauses
  Clause
c -> Clause -> Clauses
SingleClause Clause
c

-- | A smart constructor for the set of clauses.
-- 'clauses' eliminates negated boolean constants, falsums and redundant tautologies.
clauses :: Foldable f => f Clause -> Clauses
clauses :: f Clause -> Clauses
clauses = [Clauses] -> Clauses
forall (f :: * -> *). Foldable f => f Clauses -> Clauses
clauseConjunction ([Clauses] -> Clauses)
-> (f Clause -> [Clauses]) -> f Clause -> Clauses
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Clause -> Clauses) -> [Clause] -> [Clauses]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Clause -> Clauses
singleClause ([Clause] -> [Clauses])
-> (f Clause -> [Clause]) -> f Clause -> [Clauses]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f Clause -> [Clause]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList

-- | A smart constructor for equality.
(===) :: Term -> Term -> Formula
Term
a === :: Term -> Term -> Formula
=== Term
b = Literal -> Formula
Atomic (Term -> Term -> Literal
Equality Term
a Term
b)

-- | A smart constructor for inequality.
(=/=) :: Term -> Term -> Formula
Term
a =/= :: Term -> Term -> Formula
=/= Term
b = Formula -> Formula
Negate (Term
a Term -> Term -> Formula
=== Term
b)

-- | A smart constructor for negation.
neg :: Formula -> Formula
neg :: Formula -> Formula
neg = \case
  Formula
Tautology -> Formula
Falsity
  Formula
Falsity   -> Formula
Tautology
  Negate Formula
f  -> Formula
f
  Formula
f         -> Formula -> Formula
Negate Formula
f

-- | A smart contructor for the 'And' connective.
-- ('/\') has the following properties.
--
-- __Associativity__
--
-- prop> (f /\ g) /\ h == f /\ (g /\ h)
--
-- __Left identity__
--
-- prop> Tautology /\ g == g
--
-- __Right identity__
--
-- prop> f /\ Tautology == f
--
-- __Left zero__
--
-- prop> Falsity /\ g == Falsity
--
-- __Right zero__
--
-- prop> f /\ Falsity == Falsity
--
(/\) :: Formula -> Formula -> Formula
Formula
Falsity   /\ :: Formula -> Formula -> Formula
/\ Formula
_ = Formula
Falsity
Formula
Tautology /\ Formula
g = Formula
g
Formula
_ /\ Formula
Falsity   = Formula
Falsity
Formula
f /\ Formula
Tautology = Formula
f
Connected Connective
And Formula
f Formula
g /\ Formula
h = Formula
f Formula -> Formula -> Formula
/\ (Formula
g Formula -> Formula -> Formula
/\ Formula
h)
Formula
f /\ Formula
g = Connective -> Formula -> Formula -> Formula
Connected Connective
And Formula
f Formula
g

-- | A smart constructor for the 'Or' connective.
-- ('\/') has the following properties.
--
-- __Associativity__
--
-- prop> (f \/ g) \/ h == f \/ (g \/ h)
--
-- __Left identity__
--
-- prop> Falsity \/ g == g
--
-- __Right identity__
--
-- prop> f \/ Falsity == f
--
-- __Left zero__
--
-- prop> Tautology \/ g == Tautology
--
-- __Right zero__
--
-- prop> f \/ Tautology == Tautology
--
(\/) :: Formula -> Formula -> Formula
Formula
Tautology \/ :: Formula -> Formula -> Formula
\/ Formula
_ = Formula
Tautology
Formula
Falsity   \/ Formula
g = Formula
g
Formula
_ \/ Formula
Tautology = Formula
Tautology
Formula
f \/ Formula
Falsity   = Formula
f
Connected Connective
Or Formula
f Formula
g \/ Formula
h = Formula
f Formula -> Formula -> Formula
\/ (Formula
g Formula -> Formula -> Formula
\/ Formula
h)
Formula
f \/ Formula
g = Connective -> Formula -> Formula -> Formula
Connected Connective
Or Formula
f Formula
g

-- | A smart constructor for the 'Implies' connective.
(==>) :: Formula -> Formula -> Formula
Formula
Tautology ==> :: Formula -> Formula -> Formula
==> Formula
g = Formula
g
Formula
Falsity   ==> Formula
_ = Formula
Tautology
Formula
_ ==> Formula
Tautology = Formula
Tautology
Formula
f ==> Formula
Falsity   = Formula -> Formula
neg Formula
f
Formula
f ==> Formula
g = Connective -> Formula -> Formula -> Formula
Connected Connective
Implies Formula
f Formula
g

-- | A smart constructor for the 'Equivalent' connective.
-- ('<=>') has the following properties.
--
-- __Associativity__
--
-- prop> (f <=> g) <=> h == f <=> (g <=> h)
--
-- __Left identity__
--
-- prop> Tautology <=> g == g
--
-- __Right identity__
--
-- prop> f <=> Tautology == f
--
(<=>) :: Formula -> Formula -> Formula
Formula
Tautology <=> :: Formula -> Formula -> Formula
<=> Formula
g = Formula
g
Formula
f <=> Formula
Tautology = Formula
f
Connected Connective
Equivalent Formula
f Formula
g <=> Formula
h = Formula
f Formula -> Formula -> Formula
<=> (Formula
g Formula -> Formula -> Formula
<=> Formula
h)
Formula
f <=> Formula
g = Connective -> Formula -> Formula -> Formula
Connected Connective
Equivalent Formula
f Formula
g

-- | A smart constructor for the 'Xor' connective.
-- ('<~>') has the following properties.
--
-- __Associativity__
--
-- prop> (f <~> g) <~> h == f <~> (g <~> h)
--
-- __Left identity__
--
-- prop> Falsity <~> g == g
--
-- __Right identity__
--
-- prop> f <~> Falsity == f
--
(<~>) :: Formula -> Formula -> Formula
Formula
Falsity <~> :: Formula -> Formula -> Formula
<~> Formula
g = Formula
g
Formula
f <~> Formula
Falsity = Formula
f
Connected Connective
Xor Formula
f Formula
g <~> Formula
h = Formula
f Formula -> Formula -> Formula
<~> (Formula
g Formula -> Formula -> Formula
<~> Formula
h)
Formula
f <~> Formula
g = Connective -> Formula -> Formula -> Formula
Connected Connective
Xor Formula
f Formula
g

-- | A class of binders for quantified variables.
--
-- This class and its instances provides machinery for using polyvariadic
-- functions as higher-order abstract syntax for bindings of
-- quantified variables.
--
-- > eq = binaryPredicate "eq"
--
-- >>> quantified Forall $ \x -> x `eq` x
-- Quantified Forall 1 (Atomic (Predicate "eq" [Variable 1,Variable 1]))
--
-- >>> quantified Forall $ \x y -> x `eq` y ==> y `eq` x
-- Quantified Forall 2 (Quantified Forall 1 (Connected Implies (Atomic (Predicate "eq" [Variable 2,Variable 1])) (Atomic (Predicate "eq" [Variable 1,Variable 2]))))
class Binder b where
  -- | A smart constructor for quantified formulas.
  quantified :: Quantifier -> b -> Formula

-- | The degenerate instance - no variable is bound.
instance Binder Formula where
  quantified :: Quantifier -> Formula -> Formula
quantified Quantifier
_ Formula
f = Formula
f

-- | The trivial instance - binder of the varible with the given name.
instance Binder (Var, Formula) where
  quantified :: Quantifier -> (Var, Formula) -> Formula
quantified Quantifier
q (Var
v, Formula
f) = case Formula
f of
    Formula
Tautology -> Formula
f
    Formula
Falsity   -> Formula
f
    Formula
_         -> Quantifier -> Var -> Formula -> Formula
Quantified Quantifier
q Var
v Formula
f

-- | The recursive instance for polyvariadic bindings of quantified variables.
-- This is a generalized version of
-- <https://emilaxelsson.github.io/documents/axelsson2013using.pdf>.
instance Binder b => Binder (Term -> b) where
  quantified :: Quantifier -> (Term -> b) -> Formula
quantified Quantifier
q Term -> b
b = Quantifier -> (Var, Formula) -> Formula
forall b. Binder b => Quantifier -> b -> Formula
quantified Quantifier
q (Var
v, Formula
f)
    where
      f :: Formula
f = Quantifier -> b -> Formula
forall b. Binder b => Quantifier -> b -> Formula
quantified Quantifier
q (Term -> b
b (Var -> Term
Variable Var
v))
      v :: Var
v = Var
1 Var -> Var -> Var
forall a. Num a => a -> a -> a
+ Formula -> Var
maxvar Formula
f

      maxvar :: Formula -> Var
      maxvar :: Formula -> Var
maxvar = \case
        Atomic{} -> Var
0
        Negate Formula
g -> Formula -> Var
maxvar Formula
g
        Connected Connective
_ Formula
g Formula
h -> Formula -> Var
maxvar Formula
g Var -> Var -> Var
forall a. Ord a => a -> a -> a
`max` Formula -> Var
maxvar Formula
h
        Quantified Quantifier
_ Var
w Formula
_ -> Var
w

-- | A smart constructor for universally quantified formulas.
-- Provides a polyvariadic higher-order abstract syntax for the bindings of
-- universally quantified variables.
forall :: Binder b => b -> Formula
forall :: b -> Formula
forall = Quantifier -> b -> Formula
forall b. Binder b => Quantifier -> b -> Formula
quantified Quantifier
Forall

-- | A smart constructor for existentially quantified formulas.
-- Provides a polyvariadic higher-order abstract syntax for the bindings of
-- existentially quantified variables.
exists :: Binder b => b -> Formula
exists :: b -> Formula
exists = Quantifier -> b -> Formula
forall b. Binder b => Quantifier -> b -> Formula
quantified Quantifier
Exists

-- | A synonym for 'Theorem'.
(|-) :: Foldable f => f Formula -> Formula -> Theorem
f Formula
as |- :: f Formula -> Formula -> Theorem
|- Formula
c = [Formula] -> Formula -> Theorem
Theorem (f Formula -> [Formula]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList f Formula
as) Formula
c


-- * Monoids in first-order logic

-- | The ('Tautology', '/\') monoid.
newtype Conjunction = Conjunction { Conjunction -> Formula
getConjunction :: Formula }
  deriving (Int -> Conjunction -> ShowS
[Conjunction] -> ShowS
Conjunction -> String
(Int -> Conjunction -> ShowS)
-> (Conjunction -> String)
-> ([Conjunction] -> ShowS)
-> Show Conjunction
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Conjunction] -> ShowS
$cshowList :: [Conjunction] -> ShowS
show :: Conjunction -> String
$cshow :: Conjunction -> String
showsPrec :: Int -> Conjunction -> ShowS
$cshowsPrec :: Int -> Conjunction -> ShowS
Show, Conjunction -> Conjunction -> Bool
(Conjunction -> Conjunction -> Bool)
-> (Conjunction -> Conjunction -> Bool) -> Eq Conjunction
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Conjunction -> Conjunction -> Bool
$c/= :: Conjunction -> Conjunction -> Bool
== :: Conjunction -> Conjunction -> Bool
$c== :: Conjunction -> Conjunction -> Bool
Eq, Eq Conjunction
Eq Conjunction
-> (Conjunction -> Conjunction -> Ordering)
-> (Conjunction -> Conjunction -> Bool)
-> (Conjunction -> Conjunction -> Bool)
-> (Conjunction -> Conjunction -> Bool)
-> (Conjunction -> Conjunction -> Bool)
-> (Conjunction -> Conjunction -> Conjunction)
-> (Conjunction -> Conjunction -> Conjunction)
-> Ord Conjunction
Conjunction -> Conjunction -> Bool
Conjunction -> Conjunction -> Ordering
Conjunction -> Conjunction -> Conjunction
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
min :: Conjunction -> Conjunction -> Conjunction
$cmin :: Conjunction -> Conjunction -> Conjunction
max :: Conjunction -> Conjunction -> Conjunction
$cmax :: Conjunction -> Conjunction -> Conjunction
>= :: Conjunction -> Conjunction -> Bool
$c>= :: Conjunction -> Conjunction -> Bool
> :: Conjunction -> Conjunction -> Bool
$c> :: Conjunction -> Conjunction -> Bool
<= :: Conjunction -> Conjunction -> Bool
$c<= :: Conjunction -> Conjunction -> Bool
< :: Conjunction -> Conjunction -> Bool
$c< :: Conjunction -> Conjunction -> Bool
compare :: Conjunction -> Conjunction -> Ordering
$ccompare :: Conjunction -> Conjunction -> Ordering
$cp1Ord :: Eq Conjunction
Ord)

instance Semigroup Conjunction where
  <> :: Conjunction -> Conjunction -> Conjunction
(<>) = (Formula -> Formula -> Formula)
-> Conjunction -> Conjunction -> Conjunction
coerce Formula -> Formula -> Formula
(/\)

instance Monoid Conjunction where
  mempty :: Conjunction
mempty = Formula -> Conjunction
Conjunction Formula
Tautology
  mappend :: Conjunction -> Conjunction -> Conjunction
mappend = Conjunction -> Conjunction -> Conjunction
forall a. Semigroup a => a -> a -> a
(<>)

-- | Build the conjunction of formulas in a list.
conjunction :: Foldable f => f Formula -> Formula
conjunction :: f Formula -> Formula
conjunction = Conjunction -> Formula
getConjunction (Conjunction -> Formula)
-> (f Formula -> Conjunction) -> f Formula -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Conjunction] -> Conjunction
forall a. Monoid a => [a] -> a
mconcat ([Conjunction] -> Conjunction)
-> (f Formula -> [Conjunction]) -> f Formula -> Conjunction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Formula -> Conjunction) -> [Formula] -> [Conjunction]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Formula -> Conjunction
Conjunction ([Formula] -> [Conjunction])
-> (f Formula -> [Formula]) -> f Formula -> [Conjunction]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f Formula -> [Formula]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList

-- | The ('Falsity', '\/') monoid.
newtype Disjunction = Disjunction { Disjunction -> Formula
getDisjunction :: Formula }
  deriving (Int -> Disjunction -> ShowS
[Disjunction] -> ShowS
Disjunction -> String
(Int -> Disjunction -> ShowS)
-> (Disjunction -> String)
-> ([Disjunction] -> ShowS)
-> Show Disjunction
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Disjunction] -> ShowS
$cshowList :: [Disjunction] -> ShowS
show :: Disjunction -> String
$cshow :: Disjunction -> String
showsPrec :: Int -> Disjunction -> ShowS
$cshowsPrec :: Int -> Disjunction -> ShowS
Show, Disjunction -> Disjunction -> Bool
(Disjunction -> Disjunction -> Bool)
-> (Disjunction -> Disjunction -> Bool) -> Eq Disjunction
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Disjunction -> Disjunction -> Bool
$c/= :: Disjunction -> Disjunction -> Bool
== :: Disjunction -> Disjunction -> Bool
$c== :: Disjunction -> Disjunction -> Bool
Eq, Eq Disjunction
Eq Disjunction
-> (Disjunction -> Disjunction -> Ordering)
-> (Disjunction -> Disjunction -> Bool)
-> (Disjunction -> Disjunction -> Bool)
-> (Disjunction -> Disjunction -> Bool)
-> (Disjunction -> Disjunction -> Bool)
-> (Disjunction -> Disjunction -> Disjunction)
-> (Disjunction -> Disjunction -> Disjunction)
-> Ord Disjunction
Disjunction -> Disjunction -> Bool
Disjunction -> Disjunction -> Ordering
Disjunction -> Disjunction -> Disjunction
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
min :: Disjunction -> Disjunction -> Disjunction
$cmin :: Disjunction -> Disjunction -> Disjunction
max :: Disjunction -> Disjunction -> Disjunction
$cmax :: Disjunction -> Disjunction -> Disjunction
>= :: Disjunction -> Disjunction -> Bool
$c>= :: Disjunction -> Disjunction -> Bool
> :: Disjunction -> Disjunction -> Bool
$c> :: Disjunction -> Disjunction -> Bool
<= :: Disjunction -> Disjunction -> Bool
$c<= :: Disjunction -> Disjunction -> Bool
< :: Disjunction -> Disjunction -> Bool
$c< :: Disjunction -> Disjunction -> Bool
compare :: Disjunction -> Disjunction -> Ordering
$ccompare :: Disjunction -> Disjunction -> Ordering
$cp1Ord :: Eq Disjunction
Ord)

instance Semigroup Disjunction where
  <> :: Disjunction -> Disjunction -> Disjunction
(<>) = (Formula -> Formula -> Formula)
-> Disjunction -> Disjunction -> Disjunction
coerce Formula -> Formula -> Formula
(\/)

instance Monoid Disjunction where
  mempty :: Disjunction
mempty = Formula -> Disjunction
Disjunction Formula
Falsity
  mappend :: Disjunction -> Disjunction -> Disjunction
mappend = Disjunction -> Disjunction -> Disjunction
forall a. Semigroup a => a -> a -> a
(<>)

-- | Build the disjunction of formulas in a list.
disjunction :: Foldable f => f Formula -> Formula
disjunction :: f Formula -> Formula
disjunction = Disjunction -> Formula
getDisjunction (Disjunction -> Formula)
-> (f Formula -> Disjunction) -> f Formula -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Disjunction] -> Disjunction
forall a. Monoid a => [a] -> a
mconcat ([Disjunction] -> Disjunction)
-> (f Formula -> [Disjunction]) -> f Formula -> Disjunction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Formula -> Disjunction) -> [Formula] -> [Disjunction]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Formula -> Disjunction
Disjunction ([Formula] -> [Disjunction])
-> (f Formula -> [Formula]) -> f Formula -> [Disjunction]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f Formula -> [Formula]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList

-- | The ('Tautology', '<=>') monoid.
newtype Equivalence = Equivalence { Equivalence -> Formula
getEquivalence :: Formula }
  deriving (Int -> Equivalence -> ShowS
[Equivalence] -> ShowS
Equivalence -> String
(Int -> Equivalence -> ShowS)
-> (Equivalence -> String)
-> ([Equivalence] -> ShowS)
-> Show Equivalence
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Equivalence] -> ShowS
$cshowList :: [Equivalence] -> ShowS
show :: Equivalence -> String
$cshow :: Equivalence -> String
showsPrec :: Int -> Equivalence -> ShowS
$cshowsPrec :: Int -> Equivalence -> ShowS
Show, Equivalence -> Equivalence -> Bool
(Equivalence -> Equivalence -> Bool)
-> (Equivalence -> Equivalence -> Bool) -> Eq Equivalence
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Equivalence -> Equivalence -> Bool
$c/= :: Equivalence -> Equivalence -> Bool
== :: Equivalence -> Equivalence -> Bool
$c== :: Equivalence -> Equivalence -> Bool
Eq, Eq Equivalence
Eq Equivalence
-> (Equivalence -> Equivalence -> Ordering)
-> (Equivalence -> Equivalence -> Bool)
-> (Equivalence -> Equivalence -> Bool)
-> (Equivalence -> Equivalence -> Bool)
-> (Equivalence -> Equivalence -> Bool)
-> (Equivalence -> Equivalence -> Equivalence)
-> (Equivalence -> Equivalence -> Equivalence)
-> Ord Equivalence
Equivalence -> Equivalence -> Bool
Equivalence -> Equivalence -> Ordering
Equivalence -> Equivalence -> Equivalence
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
min :: Equivalence -> Equivalence -> Equivalence
$cmin :: Equivalence -> Equivalence -> Equivalence
max :: Equivalence -> Equivalence -> Equivalence
$cmax :: Equivalence -> Equivalence -> Equivalence
>= :: Equivalence -> Equivalence -> Bool
$c>= :: Equivalence -> Equivalence -> Bool
> :: Equivalence -> Equivalence -> Bool
$c> :: Equivalence -> Equivalence -> Bool
<= :: Equivalence -> Equivalence -> Bool
$c<= :: Equivalence -> Equivalence -> Bool
< :: Equivalence -> Equivalence -> Bool
$c< :: Equivalence -> Equivalence -> Bool
compare :: Equivalence -> Equivalence -> Ordering
$ccompare :: Equivalence -> Equivalence -> Ordering
$cp1Ord :: Eq Equivalence
Ord)

instance Semigroup Equivalence where
  <> :: Equivalence -> Equivalence -> Equivalence
(<>) = (Formula -> Formula -> Formula)
-> Equivalence -> Equivalence -> Equivalence
coerce Formula -> Formula -> Formula
(<=>)

instance Monoid Equivalence where
  mempty :: Equivalence
mempty = Formula -> Equivalence
Equivalence Formula
Tautology
  mappend :: Equivalence -> Equivalence -> Equivalence
mappend = Equivalence -> Equivalence -> Equivalence
forall a. Semigroup a => a -> a -> a
(<>)

-- | Build the equivalence of formulas in a list.
equivalence :: Foldable f => f Formula -> Formula
equivalence :: f Formula -> Formula
equivalence = Equivalence -> Formula
getEquivalence (Equivalence -> Formula)
-> (f Formula -> Equivalence) -> f Formula -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Equivalence] -> Equivalence
forall a. Monoid a => [a] -> a
mconcat ([Equivalence] -> Equivalence)
-> (f Formula -> [Equivalence]) -> f Formula -> Equivalence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Formula -> Equivalence) -> [Formula] -> [Equivalence]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Formula -> Equivalence
Equivalence ([Formula] -> [Equivalence])
-> (f Formula -> [Formula]) -> f Formula -> [Equivalence]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f Formula -> [Formula]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList

-- | The ('Falsity', '<~>') monoid.
newtype Inequivalence = Inequivalence { Inequivalence -> Formula
getInequivalence :: Formula }
  deriving (Int -> Inequivalence -> ShowS
[Inequivalence] -> ShowS
Inequivalence -> String
(Int -> Inequivalence -> ShowS)
-> (Inequivalence -> String)
-> ([Inequivalence] -> ShowS)
-> Show Inequivalence
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Inequivalence] -> ShowS
$cshowList :: [Inequivalence] -> ShowS
show :: Inequivalence -> String
$cshow :: Inequivalence -> String
showsPrec :: Int -> Inequivalence -> ShowS
$cshowsPrec :: Int -> Inequivalence -> ShowS
Show, Inequivalence -> Inequivalence -> Bool
(Inequivalence -> Inequivalence -> Bool)
-> (Inequivalence -> Inequivalence -> Bool) -> Eq Inequivalence
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Inequivalence -> Inequivalence -> Bool
$c/= :: Inequivalence -> Inequivalence -> Bool
== :: Inequivalence -> Inequivalence -> Bool
$c== :: Inequivalence -> Inequivalence -> Bool
Eq, Eq Inequivalence
Eq Inequivalence
-> (Inequivalence -> Inequivalence -> Ordering)
-> (Inequivalence -> Inequivalence -> Bool)
-> (Inequivalence -> Inequivalence -> Bool)
-> (Inequivalence -> Inequivalence -> Bool)
-> (Inequivalence -> Inequivalence -> Bool)
-> (Inequivalence -> Inequivalence -> Inequivalence)
-> (Inequivalence -> Inequivalence -> Inequivalence)
-> Ord Inequivalence
Inequivalence -> Inequivalence -> Bool
Inequivalence -> Inequivalence -> Ordering
Inequivalence -> Inequivalence -> Inequivalence
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
min :: Inequivalence -> Inequivalence -> Inequivalence
$cmin :: Inequivalence -> Inequivalence -> Inequivalence
max :: Inequivalence -> Inequivalence -> Inequivalence
$cmax :: Inequivalence -> Inequivalence -> Inequivalence
>= :: Inequivalence -> Inequivalence -> Bool
$c>= :: Inequivalence -> Inequivalence -> Bool
> :: Inequivalence -> Inequivalence -> Bool
$c> :: Inequivalence -> Inequivalence -> Bool
<= :: Inequivalence -> Inequivalence -> Bool
$c<= :: Inequivalence -> Inequivalence -> Bool
< :: Inequivalence -> Inequivalence -> Bool
$c< :: Inequivalence -> Inequivalence -> Bool
compare :: Inequivalence -> Inequivalence -> Ordering
$ccompare :: Inequivalence -> Inequivalence -> Ordering
$cp1Ord :: Eq Inequivalence
Ord)

instance Semigroup Inequivalence where
  <> :: Inequivalence -> Inequivalence -> Inequivalence
(<>) = (Formula -> Formula -> Formula)
-> Inequivalence -> Inequivalence -> Inequivalence
coerce Formula -> Formula -> Formula
(<~>)

instance Monoid Inequivalence where
  mempty :: Inequivalence
mempty = Formula -> Inequivalence
Inequivalence Formula
Falsity
  mappend :: Inequivalence -> Inequivalence -> Inequivalence
mappend = Inequivalence -> Inequivalence -> Inequivalence
forall a. Semigroup a => a -> a -> a
(<>)

-- | Build the inequivalence of formulas in a list.
inequivalence :: Foldable f => f Formula -> Formula
inequivalence :: f Formula -> Formula
inequivalence = Inequivalence -> Formula
getInequivalence (Inequivalence -> Formula)
-> (f Formula -> Inequivalence) -> f Formula -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Inequivalence] -> Inequivalence
forall a. Monoid a => [a] -> a
mconcat ([Inequivalence] -> Inequivalence)
-> (f Formula -> [Inequivalence]) -> f Formula -> Inequivalence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Formula -> Inequivalence) -> [Formula] -> [Inequivalence]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Formula -> Inequivalence
Inequivalence ([Formula] -> [Inequivalence])
-> (f Formula -> [Formula]) -> f Formula -> [Inequivalence]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f Formula -> [Formula]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList


-- * Miscellaneous

-- | Smart conjunction of two clauses.
-- ('/.\') has the following properties.
--
-- __Associativity__
--
-- prop> (f /.\ g) /.\ h == f /.\ (g /.\ h)
--
-- __Left identity__
--
-- prop> NoClauses /.\ g == g
--
-- __Right identity__
--
-- prop> f /.\ NoClauses == f
--
-- __Left zero__
--
-- prop> SingleClause EmptyClause /.\ g == SingleClause EmptyClause
--
-- __Right zero__
--
-- prop> f /.\ SingleClause EmptyClause == SingleClause EmptyClause
--
(/.\) :: Clauses -> Clauses -> Clauses
SingleClause Clause
EmptyClause /.\ :: Clauses -> Clauses -> Clauses
/.\ Clauses
_ = Clause -> Clauses
SingleClause Clause
EmptyClause
Clauses
_ /.\ SingleClause Clause
EmptyClause = Clause -> Clauses
SingleClause Clause
EmptyClause
Clauses [Clause]
cs /.\ Clauses [Clause]
ss = [Clause] -> Clauses
Clauses ([Clause]
cs [Clause] -> [Clause] -> [Clause]
forall a. Semigroup a => a -> a -> a
<> [Clause]
ss)

-- | The ('NoClauses', '/.\') monoid with the absorbing element 'SingleClause EmptyClause'.
newtype ClauseConjunction = ClauseConjunction { ClauseConjunction -> Clauses
getClauseConjunction :: Clauses }
  deriving (Int -> ClauseConjunction -> ShowS
[ClauseConjunction] -> ShowS
ClauseConjunction -> String
(Int -> ClauseConjunction -> ShowS)
-> (ClauseConjunction -> String)
-> ([ClauseConjunction] -> ShowS)
-> Show ClauseConjunction
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ClauseConjunction] -> ShowS
$cshowList :: [ClauseConjunction] -> ShowS
show :: ClauseConjunction -> String
$cshow :: ClauseConjunction -> String
showsPrec :: Int -> ClauseConjunction -> ShowS
$cshowsPrec :: Int -> ClauseConjunction -> ShowS
Show, ClauseConjunction -> ClauseConjunction -> Bool
(ClauseConjunction -> ClauseConjunction -> Bool)
-> (ClauseConjunction -> ClauseConjunction -> Bool)
-> Eq ClauseConjunction
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ClauseConjunction -> ClauseConjunction -> Bool
$c/= :: ClauseConjunction -> ClauseConjunction -> Bool
== :: ClauseConjunction -> ClauseConjunction -> Bool
$c== :: ClauseConjunction -> ClauseConjunction -> Bool
Eq, Eq ClauseConjunction
Eq ClauseConjunction
-> (ClauseConjunction -> ClauseConjunction -> Ordering)
-> (ClauseConjunction -> ClauseConjunction -> Bool)
-> (ClauseConjunction -> ClauseConjunction -> Bool)
-> (ClauseConjunction -> ClauseConjunction -> Bool)
-> (ClauseConjunction -> ClauseConjunction -> Bool)
-> (ClauseConjunction -> ClauseConjunction -> ClauseConjunction)
-> (ClauseConjunction -> ClauseConjunction -> ClauseConjunction)
-> Ord ClauseConjunction
ClauseConjunction -> ClauseConjunction -> Bool
ClauseConjunction -> ClauseConjunction -> Ordering
ClauseConjunction -> ClauseConjunction -> ClauseConjunction
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
min :: ClauseConjunction -> ClauseConjunction -> ClauseConjunction
$cmin :: ClauseConjunction -> ClauseConjunction -> ClauseConjunction
max :: ClauseConjunction -> ClauseConjunction -> ClauseConjunction
$cmax :: ClauseConjunction -> ClauseConjunction -> ClauseConjunction
>= :: ClauseConjunction -> ClauseConjunction -> Bool
$c>= :: ClauseConjunction -> ClauseConjunction -> Bool
> :: ClauseConjunction -> ClauseConjunction -> Bool
$c> :: ClauseConjunction -> ClauseConjunction -> Bool
<= :: ClauseConjunction -> ClauseConjunction -> Bool
$c<= :: ClauseConjunction -> ClauseConjunction -> Bool
< :: ClauseConjunction -> ClauseConjunction -> Bool
$c< :: ClauseConjunction -> ClauseConjunction -> Bool
compare :: ClauseConjunction -> ClauseConjunction -> Ordering
$ccompare :: ClauseConjunction -> ClauseConjunction -> Ordering
$cp1Ord :: Eq ClauseConjunction
Ord)

instance Semigroup ClauseConjunction where
  <> :: ClauseConjunction -> ClauseConjunction -> ClauseConjunction
(<>) = (Clauses -> Clauses -> Clauses)
-> ClauseConjunction -> ClauseConjunction -> ClauseConjunction
coerce Clauses -> Clauses -> Clauses
(/.\)

instance Monoid ClauseConjunction where
  mempty :: ClauseConjunction
mempty = Clauses -> ClauseConjunction
ClauseConjunction Clauses
NoClauses
  mappend :: ClauseConjunction -> ClauseConjunction -> ClauseConjunction
mappend = ClauseConjunction -> ClauseConjunction -> ClauseConjunction
forall a. Semigroup a => a -> a -> a
(<>)

-- | Build the conjunction of a collection of clauses.
clauseConjunction :: Foldable f => f Clauses -> Clauses
clauseConjunction :: f Clauses -> Clauses
clauseConjunction = ClauseConjunction -> Clauses
getClauseConjunction (ClauseConjunction -> Clauses)
-> (f Clauses -> ClauseConjunction) -> f Clauses -> Clauses
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ClauseConjunction] -> ClauseConjunction
forall a. Monoid a => [a] -> a
mconcat ([ClauseConjunction] -> ClauseConjunction)
-> (f Clauses -> [ClauseConjunction])
-> f Clauses
-> ClauseConjunction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Clauses -> ClauseConjunction) -> [Clauses] -> [ClauseConjunction]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Clauses -> ClauseConjunction
ClauseConjunction ([Clauses] -> [ClauseConjunction])
-> (f Clauses -> [Clauses]) -> f Clauses -> [ClauseConjunction]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f Clauses -> [Clauses]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList

-- | Smart union of two clauses.
-- ('\./') has the following properties.
--
-- __Associativity__
--
-- prop> (f \./ g) \./ h == f \./ (g \./ h)
--
-- __Left identity__
--
-- prop> EmptyClause \./ c == c
--
-- __Right identity__
--
-- prop> c \./ EmptyClause == c
--
-- __Left zero__
--
-- prop> TautologyClause \./ c == TautologyClause
--
-- __Right zero__
--
-- prop> c \./ TautologyClause == TautologyClause
--
(\./) :: Clause -> Clause -> Clause
Clause
TautologyClause \./ :: Clause -> Clause -> Clause
\./ Clause
_ = Clause
TautologyClause
Clause
_ \./ Clause
TautologyClause = Clause
TautologyClause
Literals [Signed Literal]
cs \./ Literals [Signed Literal]
ss = [Signed Literal] -> Clause
Literals ([Signed Literal]
cs [Signed Literal] -> [Signed Literal] -> [Signed Literal]
forall a. Semigroup a => a -> a -> a
<> [Signed Literal]
ss)

-- | The ('EmptyClause', '\./') monoid with the absorbing element 'TautologyClause'.
newtype ClauseUnion = ClauseUnion { ClauseUnion -> Clause
getClauseUnion :: Clause }
  deriving (Int -> ClauseUnion -> ShowS
[ClauseUnion] -> ShowS
ClauseUnion -> String
(Int -> ClauseUnion -> ShowS)
-> (ClauseUnion -> String)
-> ([ClauseUnion] -> ShowS)
-> Show ClauseUnion
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ClauseUnion] -> ShowS
$cshowList :: [ClauseUnion] -> ShowS
show :: ClauseUnion -> String
$cshow :: ClauseUnion -> String
showsPrec :: Int -> ClauseUnion -> ShowS
$cshowsPrec :: Int -> ClauseUnion -> ShowS
Show, ClauseUnion -> ClauseUnion -> Bool
(ClauseUnion -> ClauseUnion -> Bool)
-> (ClauseUnion -> ClauseUnion -> Bool) -> Eq ClauseUnion
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ClauseUnion -> ClauseUnion -> Bool
$c/= :: ClauseUnion -> ClauseUnion -> Bool
== :: ClauseUnion -> ClauseUnion -> Bool
$c== :: ClauseUnion -> ClauseUnion -> Bool
Eq, Eq ClauseUnion
Eq ClauseUnion
-> (ClauseUnion -> ClauseUnion -> Ordering)
-> (ClauseUnion -> ClauseUnion -> Bool)
-> (ClauseUnion -> ClauseUnion -> Bool)
-> (ClauseUnion -> ClauseUnion -> Bool)
-> (ClauseUnion -> ClauseUnion -> Bool)
-> (ClauseUnion -> ClauseUnion -> ClauseUnion)
-> (ClauseUnion -> ClauseUnion -> ClauseUnion)
-> Ord ClauseUnion
ClauseUnion -> ClauseUnion -> Bool
ClauseUnion -> ClauseUnion -> Ordering
ClauseUnion -> ClauseUnion -> ClauseUnion
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
min :: ClauseUnion -> ClauseUnion -> ClauseUnion
$cmin :: ClauseUnion -> ClauseUnion -> ClauseUnion
max :: ClauseUnion -> ClauseUnion -> ClauseUnion
$cmax :: ClauseUnion -> ClauseUnion -> ClauseUnion
>= :: ClauseUnion -> ClauseUnion -> Bool
$c>= :: ClauseUnion -> ClauseUnion -> Bool
> :: ClauseUnion -> ClauseUnion -> Bool
$c> :: ClauseUnion -> ClauseUnion -> Bool
<= :: ClauseUnion -> ClauseUnion -> Bool
$c<= :: ClauseUnion -> ClauseUnion -> Bool
< :: ClauseUnion -> ClauseUnion -> Bool
$c< :: ClauseUnion -> ClauseUnion -> Bool
compare :: ClauseUnion -> ClauseUnion -> Ordering
$ccompare :: ClauseUnion -> ClauseUnion -> Ordering
$cp1Ord :: Eq ClauseUnion
Ord)

instance Semigroup ClauseUnion where
  <> :: ClauseUnion -> ClauseUnion -> ClauseUnion
(<>) = (Clause -> Clause -> Clause)
-> ClauseUnion -> ClauseUnion -> ClauseUnion
coerce Clause -> Clause -> Clause
(\./)

instance Monoid ClauseUnion where
  mempty :: ClauseUnion
mempty = Clause -> ClauseUnion
ClauseUnion Clause
EmptyClause
  mappend :: ClauseUnion -> ClauseUnion -> ClauseUnion
mappend = ClauseUnion -> ClauseUnion -> ClauseUnion
forall a. Semigroup a => a -> a -> a
(<>)

-- | Build the union of a collection of clauses.
clauseUnion :: Foldable f => f Clause -> Clause
clauseUnion :: f Clause -> Clause
clauseUnion = ClauseUnion -> Clause
getClauseUnion (ClauseUnion -> Clause)
-> (f Clause -> ClauseUnion) -> f Clause -> Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ClauseUnion] -> ClauseUnion
forall a. Monoid a => [a] -> a
mconcat ([ClauseUnion] -> ClauseUnion)
-> (f Clause -> [ClauseUnion]) -> f Clause -> ClauseUnion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Clause -> ClauseUnion) -> [Clause] -> [ClauseUnion]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Clause -> ClauseUnion
ClauseUnion ([Clause] -> [ClauseUnion])
-> (f Clause -> [Clause]) -> f Clause -> [ClauseUnion]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f Clause -> [Clause]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList

-- | A multi-conjunction.
-- ('//\\') has the following properties.
--
-- __Associativity__
--
-- prop> (f //\\ g) //\\ h == f //\\ (g //\\ h)
--
-- __Left identity__
--
-- prop> [] //\\ g == g
--
-- __Right identity__
--
-- prop> f //\\ [] == f
--
-- __Left zero__
--
-- prop> [Falsity] //\\ g == [Falsity]
--
-- __Right zero__
--
-- prop> f //\\ [Falsity] == [Falsity]
--
(//\\) :: [Formula] -> [Formula] -> [Formula]
[Formula
Falsity] //\\ :: [Formula] -> [Formula] -> [Formula]
//\\ [Formula]
_ = [Formula
Falsity]
[Formula]
_ //\\ [Formula
Falsity] = [Formula
Falsity]
[Formula]
fs //\\ [Formula]
gs = [Formula]
fs [Formula] -> [Formula] -> [Formula]
forall a. Semigroup a => a -> a -> a
<> [Formula]
gs

-- | The ('[]', '//\\') monoid with the absorbing element '[Falsity]'.
newtype MultiConjunction = MultiConjunction { MultiConjunction -> [Formula]
getMultiConjunction :: [Formula] }
  deriving (Int -> MultiConjunction -> ShowS
[MultiConjunction] -> ShowS
MultiConjunction -> String
(Int -> MultiConjunction -> ShowS)
-> (MultiConjunction -> String)
-> ([MultiConjunction] -> ShowS)
-> Show MultiConjunction
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MultiConjunction] -> ShowS
$cshowList :: [MultiConjunction] -> ShowS
show :: MultiConjunction -> String
$cshow :: MultiConjunction -> String
showsPrec :: Int -> MultiConjunction -> ShowS
$cshowsPrec :: Int -> MultiConjunction -> ShowS
Show, MultiConjunction -> MultiConjunction -> Bool
(MultiConjunction -> MultiConjunction -> Bool)
-> (MultiConjunction -> MultiConjunction -> Bool)
-> Eq MultiConjunction
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MultiConjunction -> MultiConjunction -> Bool
$c/= :: MultiConjunction -> MultiConjunction -> Bool
== :: MultiConjunction -> MultiConjunction -> Bool
$c== :: MultiConjunction -> MultiConjunction -> Bool
Eq, Eq MultiConjunction
Eq MultiConjunction
-> (MultiConjunction -> MultiConjunction -> Ordering)
-> (MultiConjunction -> MultiConjunction -> Bool)
-> (MultiConjunction -> MultiConjunction -> Bool)
-> (MultiConjunction -> MultiConjunction -> Bool)
-> (MultiConjunction -> MultiConjunction -> Bool)
-> (MultiConjunction -> MultiConjunction -> MultiConjunction)
-> (MultiConjunction -> MultiConjunction -> MultiConjunction)
-> Ord MultiConjunction
MultiConjunction -> MultiConjunction -> Bool
MultiConjunction -> MultiConjunction -> Ordering
MultiConjunction -> MultiConjunction -> MultiConjunction
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
min :: MultiConjunction -> MultiConjunction -> MultiConjunction
$cmin :: MultiConjunction -> MultiConjunction -> MultiConjunction
max :: MultiConjunction -> MultiConjunction -> MultiConjunction
$cmax :: MultiConjunction -> MultiConjunction -> MultiConjunction
>= :: MultiConjunction -> MultiConjunction -> Bool
$c>= :: MultiConjunction -> MultiConjunction -> Bool
> :: MultiConjunction -> MultiConjunction -> Bool
$c> :: MultiConjunction -> MultiConjunction -> Bool
<= :: MultiConjunction -> MultiConjunction -> Bool
$c<= :: MultiConjunction -> MultiConjunction -> Bool
< :: MultiConjunction -> MultiConjunction -> Bool
$c< :: MultiConjunction -> MultiConjunction -> Bool
compare :: MultiConjunction -> MultiConjunction -> Ordering
$ccompare :: MultiConjunction -> MultiConjunction -> Ordering
$cp1Ord :: Eq MultiConjunction
Ord)

multiConjunction :: Formula -> MultiConjunction
multiConjunction :: Formula -> MultiConjunction
multiConjunction = \case
  Formula
Tautology -> [Formula] -> MultiConjunction
MultiConjunction []
  Formula
f -> [Formula] -> MultiConjunction
MultiConjunction [Formula
f]

instance Semigroup MultiConjunction where
  <> :: MultiConjunction -> MultiConjunction -> MultiConjunction
(<>) = ([Formula] -> [Formula] -> [Formula])
-> MultiConjunction -> MultiConjunction -> MultiConjunction
coerce [Formula] -> [Formula] -> [Formula]
(//\\)

instance Monoid MultiConjunction where
  mempty :: MultiConjunction
mempty = Formula -> MultiConjunction
multiConjunction Formula
Tautology
  mappend :: MultiConjunction -> MultiConjunction -> MultiConjunction
mappend = MultiConjunction -> MultiConjunction -> MultiConjunction
forall a. Semigroup a => a -> a -> a
(<>)

-- | Remove redundant boolean constants from a list of conjuncted formulas.
--
-- >>> flattenConjunction []
-- []
--
-- >>> flattenConjunction [Tautology]
-- []
--
-- >>> flattenConjunction [Falsity]
-- [Atomic (Propositional False)]
--
-- >>> flattenConjunction ["p", Tautology]
-- [Atomic (Predicate (PredicateSymbol "p") [])]
--
-- >>> flattenConjunction ["p", Falsity, "q"]
-- [Atomic (Propositional False)]
--
flattenConjunction :: Foldable f => f Formula -> [Formula]
flattenConjunction :: f Formula -> [Formula]
flattenConjunction = MultiConjunction -> [Formula]
getMultiConjunction (MultiConjunction -> [Formula])
-> (f Formula -> MultiConjunction) -> f Formula -> [Formula]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [MultiConjunction] -> MultiConjunction
forall a. Monoid a => [a] -> a
mconcat ([MultiConjunction] -> MultiConjunction)
-> (f Formula -> [MultiConjunction])
-> f Formula
-> MultiConjunction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Formula -> MultiConjunction) -> [Formula] -> [MultiConjunction]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Formula -> MultiConjunction
multiConjunction ([Formula] -> [MultiConjunction])
-> (f Formula -> [Formula]) -> f Formula -> [MultiConjunction]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f Formula -> [Formula]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList

-- | A multi-disjunction.
-- ('\\//') has the following properties.
--
-- __Associativity__
--
-- prop> (f \\// g) \\// h == f \\// (g \\// h)
--
-- __Left identity__
--
-- prop> [] \\// g == g
--
-- __Right identity__
--
-- prop> f \\// [] == f
--
-- __Left zero__
--
-- prop> [Tautology] \\// g == [Tautology]
--
-- __Right zero__
--
-- prop> f \\// [Tautology] == [Tautology]
--
(\\//) :: [Formula] -> [Formula] -> [Formula]
[Formula
Tautology] \\// :: [Formula] -> [Formula] -> [Formula]
\\// [Formula]
_ = [Formula
Tautology]
[Formula]
_ \\// [Formula
Tautology] = [Formula
Tautology]
[Formula]
fs \\// [Formula]
gs = [Formula]
fs [Formula] -> [Formula] -> [Formula]
forall a. Semigroup a => a -> a -> a
<> [Formula]
gs

-- | The ('[]', '\\//') monoid with the absorbing element '[Tautology]'.
newtype MultiDisjunction = MultiDisjunction { MultiDisjunction -> [Formula]
getMultiDisjunction :: [Formula] }
  deriving (Int -> MultiDisjunction -> ShowS
[MultiDisjunction] -> ShowS
MultiDisjunction -> String
(Int -> MultiDisjunction -> ShowS)
-> (MultiDisjunction -> String)
-> ([MultiDisjunction] -> ShowS)
-> Show MultiDisjunction
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MultiDisjunction] -> ShowS
$cshowList :: [MultiDisjunction] -> ShowS
show :: MultiDisjunction -> String
$cshow :: MultiDisjunction -> String
showsPrec :: Int -> MultiDisjunction -> ShowS
$cshowsPrec :: Int -> MultiDisjunction -> ShowS
Show, MultiDisjunction -> MultiDisjunction -> Bool
(MultiDisjunction -> MultiDisjunction -> Bool)
-> (MultiDisjunction -> MultiDisjunction -> Bool)
-> Eq MultiDisjunction
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MultiDisjunction -> MultiDisjunction -> Bool
$c/= :: MultiDisjunction -> MultiDisjunction -> Bool
== :: MultiDisjunction -> MultiDisjunction -> Bool
$c== :: MultiDisjunction -> MultiDisjunction -> Bool
Eq, Eq MultiDisjunction
Eq MultiDisjunction
-> (MultiDisjunction -> MultiDisjunction -> Ordering)
-> (MultiDisjunction -> MultiDisjunction -> Bool)
-> (MultiDisjunction -> MultiDisjunction -> Bool)
-> (MultiDisjunction -> MultiDisjunction -> Bool)
-> (MultiDisjunction -> MultiDisjunction -> Bool)
-> (MultiDisjunction -> MultiDisjunction -> MultiDisjunction)
-> (MultiDisjunction -> MultiDisjunction -> MultiDisjunction)
-> Ord MultiDisjunction
MultiDisjunction -> MultiDisjunction -> Bool
MultiDisjunction -> MultiDisjunction -> Ordering
MultiDisjunction -> MultiDisjunction -> MultiDisjunction
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
min :: MultiDisjunction -> MultiDisjunction -> MultiDisjunction
$cmin :: MultiDisjunction -> MultiDisjunction -> MultiDisjunction
max :: MultiDisjunction -> MultiDisjunction -> MultiDisjunction
$cmax :: MultiDisjunction -> MultiDisjunction -> MultiDisjunction
>= :: MultiDisjunction -> MultiDisjunction -> Bool
$c>= :: MultiDisjunction -> MultiDisjunction -> Bool
> :: MultiDisjunction -> MultiDisjunction -> Bool
$c> :: MultiDisjunction -> MultiDisjunction -> Bool
<= :: MultiDisjunction -> MultiDisjunction -> Bool
$c<= :: MultiDisjunction -> MultiDisjunction -> Bool
< :: MultiDisjunction -> MultiDisjunction -> Bool
$c< :: MultiDisjunction -> MultiDisjunction -> Bool
compare :: MultiDisjunction -> MultiDisjunction -> Ordering
$ccompare :: MultiDisjunction -> MultiDisjunction -> Ordering
$cp1Ord :: Eq MultiDisjunction
Ord)

multiDisjunction :: Formula -> MultiDisjunction
multiDisjunction :: Formula -> MultiDisjunction
multiDisjunction = \case
  Formula
Falsity -> [Formula] -> MultiDisjunction
MultiDisjunction []
  Formula
f -> [Formula] -> MultiDisjunction
MultiDisjunction [Formula
f]

instance Semigroup MultiDisjunction where
  <> :: MultiDisjunction -> MultiDisjunction -> MultiDisjunction
(<>) = ([Formula] -> [Formula] -> [Formula])
-> MultiDisjunction -> MultiDisjunction -> MultiDisjunction
coerce [Formula] -> [Formula] -> [Formula]
(\\//)

instance Monoid MultiDisjunction where
  mempty :: MultiDisjunction
mempty = Formula -> MultiDisjunction
multiDisjunction Formula
Falsity
  mappend :: MultiDisjunction -> MultiDisjunction -> MultiDisjunction
mappend = MultiDisjunction -> MultiDisjunction -> MultiDisjunction
forall a. Semigroup a => a -> a -> a
(<>)

-- | Remove redundant boolean constants from a list of disjuncted formulas.
--
-- >>> flattenDisjunction []
-- []
--
-- >>> flattenDisjunction [Tautology]
-- [Atomic (Propositional True)]
--
-- >>> flattenDisjunction [Falsity]
-- []
--
-- >>> flattenDisjunction ["p", Tautology, "q"]
-- [Atomic (Propositional True)]
--
-- >>> flattenDisjunction ["p", Falsity]
-- [Atomic (Predicate (PredicateSymbol "p") [])]
--
flattenDisjunction :: Foldable f => f Formula -> [Formula]
flattenDisjunction :: f Formula -> [Formula]
flattenDisjunction = MultiDisjunction -> [Formula]
getMultiDisjunction (MultiDisjunction -> [Formula])
-> (f Formula -> MultiDisjunction) -> f Formula -> [Formula]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [MultiDisjunction] -> MultiDisjunction
forall a. Monoid a => [a] -> a
mconcat ([MultiDisjunction] -> MultiDisjunction)
-> (f Formula -> [MultiDisjunction])
-> f Formula
-> MultiDisjunction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Formula -> MultiDisjunction) -> [Formula] -> [MultiDisjunction]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Formula -> MultiDisjunction
multiDisjunction ([Formula] -> [MultiDisjunction])
-> (f Formula -> [Formula]) -> f Formula -> [MultiDisjunction]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f Formula -> [Formula]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList