{-# LANGUAGE CPP #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

{-|
Module       : ATP.FirstOrder.Core
Description  : Data types representing unsorted first-order logic.
Copyright    : (c) Evgenii Kotelnikov, 2019-2021
License      : GPL-3
Maintainer   : evgeny.kotelnikov@gmail.com
Stability    : experimental
-}

module ATP.FirstOrder.Core (
  -- * First-order logic
  Var,
  FunctionSymbol(..),
  Term(..),
  PredicateSymbol(..),
  Literal(..),
  Sign(..),
  Signed(..),
  sign,
  Clause(..),
  Clauses(..),
  Connective(..),
  isAssociative,
  Quantifier(..),
  Formula(..),
  LogicalExpression(..),
  Theorem(..),

  -- * Syntactic sugar
  -- $sugar
  Function,
  Constant,
  UnaryFunction,
  BinaryFunction,
  TernaryFunction,
  pattern Constant,
  pattern UnaryFunction,
  pattern BinaryFunction,
  pattern TernaryFunction,

  Predicate,
  Proposition,
  UnaryPredicate,
  BinaryPredicate,
  TernaryPredicate,
  pattern Proposition,
  pattern UnaryPredicate,
  pattern BinaryPredicate,
  pattern TernaryPredicate,

  pattern TautologyLiteral,
  pattern FalsityLiteral,

  pattern EmptyClause,
  pattern UnitClause,
  pattern TautologyClause,

  pattern NoClauses,
  pattern SingleClause,

  pattern Tautology,
  pattern Falsity,

  pattern Claim
) where

#if !MIN_VERSION_base(4, 11, 0)
import Data.Semigroup (Semigroup(..))
#endif
import Data.String (IsString(..))
import Data.Text (Text)


-- * First-order logic

-- | The type of variables in first-order formulas.
type Var = Integer

-- | The type of function symbols in first-order formulas.
newtype FunctionSymbol = FunctionSymbol Text
  deriving (Int -> FunctionSymbol -> ShowS
[FunctionSymbol] -> ShowS
FunctionSymbol -> String
(Int -> FunctionSymbol -> ShowS)
-> (FunctionSymbol -> String)
-> ([FunctionSymbol] -> ShowS)
-> Show FunctionSymbol
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FunctionSymbol] -> ShowS
$cshowList :: [FunctionSymbol] -> ShowS
show :: FunctionSymbol -> String
$cshow :: FunctionSymbol -> String
showsPrec :: Int -> FunctionSymbol -> ShowS
$cshowsPrec :: Int -> FunctionSymbol -> ShowS
Show, FunctionSymbol -> FunctionSymbol -> Bool
(FunctionSymbol -> FunctionSymbol -> Bool)
-> (FunctionSymbol -> FunctionSymbol -> Bool) -> Eq FunctionSymbol
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FunctionSymbol -> FunctionSymbol -> Bool
$c/= :: FunctionSymbol -> FunctionSymbol -> Bool
== :: FunctionSymbol -> FunctionSymbol -> Bool
$c== :: FunctionSymbol -> FunctionSymbol -> Bool
Eq, Eq FunctionSymbol
Eq FunctionSymbol
-> (FunctionSymbol -> FunctionSymbol -> Ordering)
-> (FunctionSymbol -> FunctionSymbol -> Bool)
-> (FunctionSymbol -> FunctionSymbol -> Bool)
-> (FunctionSymbol -> FunctionSymbol -> Bool)
-> (FunctionSymbol -> FunctionSymbol -> Bool)
-> (FunctionSymbol -> FunctionSymbol -> FunctionSymbol)
-> (FunctionSymbol -> FunctionSymbol -> FunctionSymbol)
-> Ord FunctionSymbol
FunctionSymbol -> FunctionSymbol -> Bool
FunctionSymbol -> FunctionSymbol -> Ordering
FunctionSymbol -> FunctionSymbol -> FunctionSymbol
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 :: FunctionSymbol -> FunctionSymbol -> FunctionSymbol
$cmin :: FunctionSymbol -> FunctionSymbol -> FunctionSymbol
max :: FunctionSymbol -> FunctionSymbol -> FunctionSymbol
$cmax :: FunctionSymbol -> FunctionSymbol -> FunctionSymbol
>= :: FunctionSymbol -> FunctionSymbol -> Bool
$c>= :: FunctionSymbol -> FunctionSymbol -> Bool
> :: FunctionSymbol -> FunctionSymbol -> Bool
$c> :: FunctionSymbol -> FunctionSymbol -> Bool
<= :: FunctionSymbol -> FunctionSymbol -> Bool
$c<= :: FunctionSymbol -> FunctionSymbol -> Bool
< :: FunctionSymbol -> FunctionSymbol -> Bool
$c< :: FunctionSymbol -> FunctionSymbol -> Bool
compare :: FunctionSymbol -> FunctionSymbol -> Ordering
$ccompare :: FunctionSymbol -> FunctionSymbol -> Ordering
$cp1Ord :: Eq FunctionSymbol
Ord, String -> FunctionSymbol
(String -> FunctionSymbol) -> IsString FunctionSymbol
forall a. (String -> a) -> IsString a
fromString :: String -> FunctionSymbol
$cfromString :: String -> FunctionSymbol
IsString)

-- | The term in first-order logic.
data Term
  = Variable Var
    -- ^ A quantified variable.
  | Function FunctionSymbol [Term]
    -- ^ Application of a function symbol. The empty list of arguments
    -- represents a constant.
  deriving (Int -> Term -> ShowS
[Term] -> ShowS
Term -> String
(Int -> Term -> ShowS)
-> (Term -> String) -> ([Term] -> ShowS) -> Show Term
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Term] -> ShowS
$cshowList :: [Term] -> ShowS
show :: Term -> String
$cshow :: Term -> String
showsPrec :: Int -> Term -> ShowS
$cshowsPrec :: Int -> Term -> ShowS
Show, Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c== :: Term -> Term -> Bool
Eq, Eq Term
Eq Term
-> (Term -> Term -> Ordering)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Term)
-> (Term -> Term -> Term)
-> Ord Term
Term -> Term -> Bool
Term -> Term -> Ordering
Term -> Term -> Term
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 :: Term -> Term -> Term
$cmin :: Term -> Term -> Term
max :: Term -> Term -> Term
$cmax :: Term -> Term -> Term
>= :: Term -> Term -> Bool
$c>= :: Term -> Term -> Bool
> :: Term -> Term -> Bool
$c> :: Term -> Term -> Bool
<= :: Term -> Term -> Bool
$c<= :: Term -> Term -> Bool
< :: Term -> Term -> Bool
$c< :: Term -> Term -> Bool
compare :: Term -> Term -> Ordering
$ccompare :: Term -> Term -> Ordering
$cp1Ord :: Eq Term
Ord)

-- | The type of predicate symbols in first-order formulas.
newtype PredicateSymbol = PredicateSymbol Text
  deriving (Int -> PredicateSymbol -> ShowS
[PredicateSymbol] -> ShowS
PredicateSymbol -> String
(Int -> PredicateSymbol -> ShowS)
-> (PredicateSymbol -> String)
-> ([PredicateSymbol] -> ShowS)
-> Show PredicateSymbol
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PredicateSymbol] -> ShowS
$cshowList :: [PredicateSymbol] -> ShowS
show :: PredicateSymbol -> String
$cshow :: PredicateSymbol -> String
showsPrec :: Int -> PredicateSymbol -> ShowS
$cshowsPrec :: Int -> PredicateSymbol -> ShowS
Show, PredicateSymbol -> PredicateSymbol -> Bool
(PredicateSymbol -> PredicateSymbol -> Bool)
-> (PredicateSymbol -> PredicateSymbol -> Bool)
-> Eq PredicateSymbol
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PredicateSymbol -> PredicateSymbol -> Bool
$c/= :: PredicateSymbol -> PredicateSymbol -> Bool
== :: PredicateSymbol -> PredicateSymbol -> Bool
$c== :: PredicateSymbol -> PredicateSymbol -> Bool
Eq, Eq PredicateSymbol
Eq PredicateSymbol
-> (PredicateSymbol -> PredicateSymbol -> Ordering)
-> (PredicateSymbol -> PredicateSymbol -> Bool)
-> (PredicateSymbol -> PredicateSymbol -> Bool)
-> (PredicateSymbol -> PredicateSymbol -> Bool)
-> (PredicateSymbol -> PredicateSymbol -> Bool)
-> (PredicateSymbol -> PredicateSymbol -> PredicateSymbol)
-> (PredicateSymbol -> PredicateSymbol -> PredicateSymbol)
-> Ord PredicateSymbol
PredicateSymbol -> PredicateSymbol -> Bool
PredicateSymbol -> PredicateSymbol -> Ordering
PredicateSymbol -> PredicateSymbol -> PredicateSymbol
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 :: PredicateSymbol -> PredicateSymbol -> PredicateSymbol
$cmin :: PredicateSymbol -> PredicateSymbol -> PredicateSymbol
max :: PredicateSymbol -> PredicateSymbol -> PredicateSymbol
$cmax :: PredicateSymbol -> PredicateSymbol -> PredicateSymbol
>= :: PredicateSymbol -> PredicateSymbol -> Bool
$c>= :: PredicateSymbol -> PredicateSymbol -> Bool
> :: PredicateSymbol -> PredicateSymbol -> Bool
$c> :: PredicateSymbol -> PredicateSymbol -> Bool
<= :: PredicateSymbol -> PredicateSymbol -> Bool
$c<= :: PredicateSymbol -> PredicateSymbol -> Bool
< :: PredicateSymbol -> PredicateSymbol -> Bool
$c< :: PredicateSymbol -> PredicateSymbol -> Bool
compare :: PredicateSymbol -> PredicateSymbol -> Ordering
$ccompare :: PredicateSymbol -> PredicateSymbol -> Ordering
$cp1Ord :: Eq PredicateSymbol
Ord, String -> PredicateSymbol
(String -> PredicateSymbol) -> IsString PredicateSymbol
forall a. (String -> a) -> IsString a
fromString :: String -> PredicateSymbol
$cfromString :: String -> PredicateSymbol
IsString)

-- | The literal in first-order logic.
data Literal
  = Propositional Bool
    -- ^ A logical constant - tautology or falsum.
  | Predicate PredicateSymbol [Term]
    -- ^ Application of a predicate symbol. The empty list of arguments
    -- represents a boolean constant.
  | Equality Term Term
    -- ^ Equality between terms.
  deriving (Int -> Literal -> ShowS
[Literal] -> ShowS
Literal -> String
(Int -> Literal -> ShowS)
-> (Literal -> String) -> ([Literal] -> ShowS) -> Show Literal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Literal] -> ShowS
$cshowList :: [Literal] -> ShowS
show :: Literal -> String
$cshow :: Literal -> String
showsPrec :: Int -> Literal -> ShowS
$cshowsPrec :: Int -> Literal -> ShowS
Show, Literal -> Literal -> Bool
(Literal -> Literal -> Bool)
-> (Literal -> Literal -> Bool) -> Eq Literal
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Literal -> Literal -> Bool
$c/= :: Literal -> Literal -> Bool
== :: Literal -> Literal -> Bool
$c== :: Literal -> Literal -> Bool
Eq, Eq Literal
Eq Literal
-> (Literal -> Literal -> Ordering)
-> (Literal -> Literal -> Bool)
-> (Literal -> Literal -> Bool)
-> (Literal -> Literal -> Bool)
-> (Literal -> Literal -> Bool)
-> (Literal -> Literal -> Literal)
-> (Literal -> Literal -> Literal)
-> Ord Literal
Literal -> Literal -> Bool
Literal -> Literal -> Ordering
Literal -> Literal -> Literal
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 :: Literal -> Literal -> Literal
$cmin :: Literal -> Literal -> Literal
max :: Literal -> Literal -> Literal
$cmax :: Literal -> Literal -> Literal
>= :: Literal -> Literal -> Bool
$c>= :: Literal -> Literal -> Bool
> :: Literal -> Literal -> Bool
$c> :: Literal -> Literal -> Bool
<= :: Literal -> Literal -> Bool
$c<= :: Literal -> Literal -> Bool
< :: Literal -> Literal -> Bool
$c< :: Literal -> Literal -> Bool
compare :: Literal -> Literal -> Ordering
$ccompare :: Literal -> Literal -> Ordering
$cp1Ord :: Eq Literal
Ord)

-- | The sign of a logical expression is either positive or negative.
data Sign
  = Positive
  | Negative
  deriving (Sign -> Sign -> Bool
(Sign -> Sign -> Bool) -> (Sign -> Sign -> Bool) -> Eq Sign
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sign -> Sign -> Bool
$c/= :: Sign -> Sign -> Bool
== :: Sign -> Sign -> Bool
$c== :: Sign -> Sign -> Bool
Eq, Int -> Sign -> ShowS
[Sign] -> ShowS
Sign -> String
(Int -> Sign -> ShowS)
-> (Sign -> String) -> ([Sign] -> ShowS) -> Show Sign
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sign] -> ShowS
$cshowList :: [Sign] -> ShowS
show :: Sign -> String
$cshow :: Sign -> String
showsPrec :: Int -> Sign -> ShowS
$cshowsPrec :: Int -> Sign -> ShowS
Show, Eq Sign
Eq Sign
-> (Sign -> Sign -> Ordering)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Sign)
-> (Sign -> Sign -> Sign)
-> Ord Sign
Sign -> Sign -> Bool
Sign -> Sign -> Ordering
Sign -> Sign -> Sign
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 :: Sign -> Sign -> Sign
$cmin :: Sign -> Sign -> Sign
max :: Sign -> Sign -> Sign
$cmax :: Sign -> Sign -> Sign
>= :: Sign -> Sign -> Bool
$c>= :: Sign -> Sign -> Bool
> :: Sign -> Sign -> Bool
$c> :: Sign -> Sign -> Bool
<= :: Sign -> Sign -> Bool
$c<= :: Sign -> Sign -> Bool
< :: Sign -> Sign -> Bool
$c< :: Sign -> Sign -> Bool
compare :: Sign -> Sign -> Ordering
$ccompare :: Sign -> Sign -> Ordering
$cp1Ord :: Eq Sign
Ord, Int -> Sign
Sign -> Int
Sign -> [Sign]
Sign -> Sign
Sign -> Sign -> [Sign]
Sign -> Sign -> Sign -> [Sign]
(Sign -> Sign)
-> (Sign -> Sign)
-> (Int -> Sign)
-> (Sign -> Int)
-> (Sign -> [Sign])
-> (Sign -> Sign -> [Sign])
-> (Sign -> Sign -> [Sign])
-> (Sign -> Sign -> Sign -> [Sign])
-> Enum Sign
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Sign -> Sign -> Sign -> [Sign]
$cenumFromThenTo :: Sign -> Sign -> Sign -> [Sign]
enumFromTo :: Sign -> Sign -> [Sign]
$cenumFromTo :: Sign -> Sign -> [Sign]
enumFromThen :: Sign -> Sign -> [Sign]
$cenumFromThen :: Sign -> Sign -> [Sign]
enumFrom :: Sign -> [Sign]
$cenumFrom :: Sign -> [Sign]
fromEnum :: Sign -> Int
$cfromEnum :: Sign -> Int
toEnum :: Int -> Sign
$ctoEnum :: Int -> Sign
pred :: Sign -> Sign
$cpred :: Sign -> Sign
succ :: Sign -> Sign
$csucc :: Sign -> Sign
Enum, Sign
Sign -> Sign -> Bounded Sign
forall a. a -> a -> Bounded a
maxBound :: Sign
$cmaxBound :: Sign
minBound :: Sign
$cminBound :: Sign
Bounded)

instance Semigroup Sign where
  Sign
Negative <> :: Sign -> Sign -> Sign
<> Sign
Positive = Sign
Negative
  Sign
Positive <> Sign
Negative = Sign
Negative
  Sign
Negative <> Sign
Negative = Sign
Positive
  Sign
Positive <> Sign
Positive = Sign
Positive

instance Monoid Sign where
  mempty :: Sign
mempty = Sign
Positive
  mappend :: Sign -> Sign -> Sign
mappend = Sign -> Sign -> Sign
forall a. Semigroup a => a -> a -> a
(<>)

-- | A signed expression is that annotated with a 'Sign'.
data Signed e = Signed {
  Signed e -> Sign
signof :: Sign,
  Signed e -> e
unsign :: e
} deriving (Signed e -> Signed e -> Bool
(Signed e -> Signed e -> Bool)
-> (Signed e -> Signed e -> Bool) -> Eq (Signed e)
forall e. Eq e => Signed e -> Signed e -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Signed e -> Signed e -> Bool
$c/= :: forall e. Eq e => Signed e -> Signed e -> Bool
== :: Signed e -> Signed e -> Bool
$c== :: forall e. Eq e => Signed e -> Signed e -> Bool
Eq, Int -> Signed e -> ShowS
[Signed e] -> ShowS
Signed e -> String
(Int -> Signed e -> ShowS)
-> (Signed e -> String) -> ([Signed e] -> ShowS) -> Show (Signed e)
forall e. Show e => Int -> Signed e -> ShowS
forall e. Show e => [Signed e] -> ShowS
forall e. Show e => Signed e -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Signed e] -> ShowS
$cshowList :: forall e. Show e => [Signed e] -> ShowS
show :: Signed e -> String
$cshow :: forall e. Show e => Signed e -> String
showsPrec :: Int -> Signed e -> ShowS
$cshowsPrec :: forall e. Show e => Int -> Signed e -> ShowS
Show, Eq (Signed e)
Eq (Signed e)
-> (Signed e -> Signed e -> Ordering)
-> (Signed e -> Signed e -> Bool)
-> (Signed e -> Signed e -> Bool)
-> (Signed e -> Signed e -> Bool)
-> (Signed e -> Signed e -> Bool)
-> (Signed e -> Signed e -> Signed e)
-> (Signed e -> Signed e -> Signed e)
-> Ord (Signed e)
Signed e -> Signed e -> Bool
Signed e -> Signed e -> Ordering
Signed e -> Signed e -> Signed e
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall e. Ord e => Eq (Signed e)
forall e. Ord e => Signed e -> Signed e -> Bool
forall e. Ord e => Signed e -> Signed e -> Ordering
forall e. Ord e => Signed e -> Signed e -> Signed e
min :: Signed e -> Signed e -> Signed e
$cmin :: forall e. Ord e => Signed e -> Signed e -> Signed e
max :: Signed e -> Signed e -> Signed e
$cmax :: forall e. Ord e => Signed e -> Signed e -> Signed e
>= :: Signed e -> Signed e -> Bool
$c>= :: forall e. Ord e => Signed e -> Signed e -> Bool
> :: Signed e -> Signed e -> Bool
$c> :: forall e. Ord e => Signed e -> Signed e -> Bool
<= :: Signed e -> Signed e -> Bool
$c<= :: forall e. Ord e => Signed e -> Signed e -> Bool
< :: Signed e -> Signed e -> Bool
$c< :: forall e. Ord e => Signed e -> Signed e -> Bool
compare :: Signed e -> Signed e -> Ordering
$ccompare :: forall e. Ord e => Signed e -> Signed e -> Ordering
$cp1Ord :: forall e. Ord e => Eq (Signed e)
Ord, a -> Signed b -> Signed a
(a -> b) -> Signed a -> Signed b
(forall a b. (a -> b) -> Signed a -> Signed b)
-> (forall a b. a -> Signed b -> Signed a) -> Functor Signed
forall a b. a -> Signed b -> Signed a
forall a b. (a -> b) -> Signed a -> Signed b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Signed b -> Signed a
$c<$ :: forall a b. a -> Signed b -> Signed a
fmap :: (a -> b) -> Signed a -> Signed b
$cfmap :: forall a b. (a -> b) -> Signed a -> Signed b
Functor, Signed a -> Bool
(a -> m) -> Signed a -> m
(a -> b -> b) -> b -> Signed a -> b
(forall m. Monoid m => Signed m -> m)
-> (forall m a. Monoid m => (a -> m) -> Signed a -> m)
-> (forall m a. Monoid m => (a -> m) -> Signed a -> m)
-> (forall a b. (a -> b -> b) -> b -> Signed a -> b)
-> (forall a b. (a -> b -> b) -> b -> Signed a -> b)
-> (forall b a. (b -> a -> b) -> b -> Signed a -> b)
-> (forall b a. (b -> a -> b) -> b -> Signed a -> b)
-> (forall a. (a -> a -> a) -> Signed a -> a)
-> (forall a. (a -> a -> a) -> Signed a -> a)
-> (forall a. Signed a -> [a])
-> (forall a. Signed a -> Bool)
-> (forall a. Signed a -> Int)
-> (forall a. Eq a => a -> Signed a -> Bool)
-> (forall a. Ord a => Signed a -> a)
-> (forall a. Ord a => Signed a -> a)
-> (forall a. Num a => Signed a -> a)
-> (forall a. Num a => Signed a -> a)
-> Foldable Signed
forall a. Eq a => a -> Signed a -> Bool
forall a. Num a => Signed a -> a
forall a. Ord a => Signed a -> a
forall m. Monoid m => Signed m -> m
forall a. Signed a -> Bool
forall a. Signed a -> Int
forall a. Signed a -> [a]
forall a. (a -> a -> a) -> Signed a -> a
forall m a. Monoid m => (a -> m) -> Signed a -> m
forall b a. (b -> a -> b) -> b -> Signed a -> b
forall a b. (a -> b -> b) -> b -> Signed a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Signed a -> a
$cproduct :: forall a. Num a => Signed a -> a
sum :: Signed a -> a
$csum :: forall a. Num a => Signed a -> a
minimum :: Signed a -> a
$cminimum :: forall a. Ord a => Signed a -> a
maximum :: Signed a -> a
$cmaximum :: forall a. Ord a => Signed a -> a
elem :: a -> Signed a -> Bool
$celem :: forall a. Eq a => a -> Signed a -> Bool
length :: Signed a -> Int
$clength :: forall a. Signed a -> Int
null :: Signed a -> Bool
$cnull :: forall a. Signed a -> Bool
toList :: Signed a -> [a]
$ctoList :: forall a. Signed a -> [a]
foldl1 :: (a -> a -> a) -> Signed a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Signed a -> a
foldr1 :: (a -> a -> a) -> Signed a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Signed a -> a
foldl' :: (b -> a -> b) -> b -> Signed a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Signed a -> b
foldl :: (b -> a -> b) -> b -> Signed a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Signed a -> b
foldr' :: (a -> b -> b) -> b -> Signed a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Signed a -> b
foldr :: (a -> b -> b) -> b -> Signed a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Signed a -> b
foldMap' :: (a -> m) -> Signed a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Signed a -> m
foldMap :: (a -> m) -> Signed a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Signed a -> m
fold :: Signed m -> m
$cfold :: forall m. Monoid m => Signed m -> m
Foldable, Functor Signed
Foldable Signed
Functor Signed
-> Foldable Signed
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Signed a -> f (Signed b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Signed (f a) -> f (Signed a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Signed a -> m (Signed b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Signed (m a) -> m (Signed a))
-> Traversable Signed
(a -> f b) -> Signed a -> f (Signed b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Signed (m a) -> m (Signed a)
forall (f :: * -> *) a.
Applicative f =>
Signed (f a) -> f (Signed a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Signed a -> m (Signed b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Signed a -> f (Signed b)
sequence :: Signed (m a) -> m (Signed a)
$csequence :: forall (m :: * -> *) a. Monad m => Signed (m a) -> m (Signed a)
mapM :: (a -> m b) -> Signed a -> m (Signed b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Signed a -> m (Signed b)
sequenceA :: Signed (f a) -> f (Signed a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Signed (f a) -> f (Signed a)
traverse :: (a -> f b) -> Signed a -> f (Signed b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Signed a -> f (Signed b)
$cp2Traversable :: Foldable Signed
$cp1Traversable :: Functor Signed
Traversable)

-- | Juxtapose a given signed expression with a given sign.
sign :: Sign -> Signed e -> Signed e
sign :: Sign -> Signed e -> Signed e
sign Sign
s (Signed Sign
z e
e) = Sign -> e -> Signed e
forall e. Sign -> e -> Signed e
Signed (Sign
s Sign -> Sign -> Sign
forall a. Semigroup a => a -> a -> a
<> Sign
z) e
e

instance Applicative Signed where
  pure :: a -> Signed a
pure = Sign -> a -> Signed a
forall e. Sign -> e -> Signed e
Signed Sign
Positive
  Signed Sign
s a -> b
f <*> :: Signed (a -> b) -> Signed a -> Signed b
<*> Signed a
e = Sign -> Signed b -> Signed b
forall e. Sign -> Signed e -> Signed e
sign Sign
s ((a -> b) -> Signed a -> Signed b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Signed a
e)

instance Monad Signed where
  Signed Sign
s a
e >>= :: Signed a -> (a -> Signed b) -> Signed b
>>= a -> Signed b
f = Sign -> Signed b -> Signed b
forall e. Sign -> Signed e -> Signed e
sign Sign
s (a -> Signed b
f a
e)

-- | The first-order clause - an implicitly universally-quantified disjunction
-- of positive or negative literals, represented as a list of signed literals.
-- The empty clause is logically equivalent to falsum.
newtype Clause = Literals { Clause -> [Signed Literal]
getLiterals :: [Signed Literal] }
  deriving (Int -> Clause -> ShowS
[Clause] -> ShowS
Clause -> String
(Int -> Clause -> ShowS)
-> (Clause -> String) -> ([Clause] -> ShowS) -> Show Clause
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Clause] -> ShowS
$cshowList :: [Clause] -> ShowS
show :: Clause -> String
$cshow :: Clause -> String
showsPrec :: Int -> Clause -> ShowS
$cshowsPrec :: Int -> Clause -> ShowS
Show, Clause -> Clause -> Bool
(Clause -> Clause -> Bool)
-> (Clause -> Clause -> Bool) -> Eq Clause
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Clause -> Clause -> Bool
$c/= :: Clause -> Clause -> Bool
== :: Clause -> Clause -> Bool
$c== :: Clause -> Clause -> Bool
Eq, Eq Clause
Eq Clause
-> (Clause -> Clause -> Ordering)
-> (Clause -> Clause -> Bool)
-> (Clause -> Clause -> Bool)
-> (Clause -> Clause -> Bool)
-> (Clause -> Clause -> Bool)
-> (Clause -> Clause -> Clause)
-> (Clause -> Clause -> Clause)
-> Ord Clause
Clause -> Clause -> Bool
Clause -> Clause -> Ordering
Clause -> Clause -> Clause
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 :: Clause -> Clause -> Clause
$cmin :: Clause -> Clause -> Clause
max :: Clause -> Clause -> Clause
$cmax :: Clause -> Clause -> Clause
>= :: Clause -> Clause -> Bool
$c>= :: Clause -> Clause -> Bool
> :: Clause -> Clause -> Bool
$c> :: Clause -> Clause -> Bool
<= :: Clause -> Clause -> Bool
$c<= :: Clause -> Clause -> Bool
< :: Clause -> Clause -> Bool
$c< :: Clause -> Clause -> Bool
compare :: Clause -> Clause -> Ordering
$ccompare :: Clause -> Clause -> Ordering
$cp1Ord :: Eq Clause
Ord, b -> Clause -> Clause
NonEmpty Clause -> Clause
Clause -> Clause -> Clause
(Clause -> Clause -> Clause)
-> (NonEmpty Clause -> Clause)
-> (forall b. Integral b => b -> Clause -> Clause)
-> Semigroup Clause
forall b. Integral b => b -> Clause -> Clause
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: b -> Clause -> Clause
$cstimes :: forall b. Integral b => b -> Clause -> Clause
sconcat :: NonEmpty Clause -> Clause
$csconcat :: NonEmpty Clause -> Clause
<> :: Clause -> Clause -> Clause
$c<> :: Clause -> Clause -> Clause
Semigroup, Semigroup Clause
Clause
Semigroup Clause
-> Clause
-> (Clause -> Clause -> Clause)
-> ([Clause] -> Clause)
-> Monoid Clause
[Clause] -> Clause
Clause -> Clause -> Clause
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [Clause] -> Clause
$cmconcat :: [Clause] -> Clause
mappend :: Clause -> Clause -> Clause
$cmappend :: Clause -> Clause -> Clause
mempty :: Clause
$cmempty :: Clause
$cp1Monoid :: Semigroup Clause
Monoid)

-- | A clause set is zero or more first-order clauses.
-- The empty clause set is logically equivalent to tautology.
newtype Clauses = Clauses { Clauses -> [Clause]
getClauses :: [Clause] }
  deriving (Int -> Clauses -> ShowS
[Clauses] -> ShowS
Clauses -> String
(Int -> Clauses -> ShowS)
-> (Clauses -> String) -> ([Clauses] -> ShowS) -> Show Clauses
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Clauses] -> ShowS
$cshowList :: [Clauses] -> ShowS
show :: Clauses -> String
$cshow :: Clauses -> String
showsPrec :: Int -> Clauses -> ShowS
$cshowsPrec :: Int -> Clauses -> ShowS
Show, Clauses -> Clauses -> Bool
(Clauses -> Clauses -> Bool)
-> (Clauses -> Clauses -> Bool) -> Eq Clauses
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Clauses -> Clauses -> Bool
$c/= :: Clauses -> Clauses -> Bool
== :: Clauses -> Clauses -> Bool
$c== :: Clauses -> Clauses -> Bool
Eq, Eq Clauses
Eq Clauses
-> (Clauses -> Clauses -> Ordering)
-> (Clauses -> Clauses -> Bool)
-> (Clauses -> Clauses -> Bool)
-> (Clauses -> Clauses -> Bool)
-> (Clauses -> Clauses -> Bool)
-> (Clauses -> Clauses -> Clauses)
-> (Clauses -> Clauses -> Clauses)
-> Ord Clauses
Clauses -> Clauses -> Bool
Clauses -> Clauses -> Ordering
Clauses -> Clauses -> Clauses
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 :: Clauses -> Clauses -> Clauses
$cmin :: Clauses -> Clauses -> Clauses
max :: Clauses -> Clauses -> Clauses
$cmax :: Clauses -> Clauses -> Clauses
>= :: Clauses -> Clauses -> Bool
$c>= :: Clauses -> Clauses -> Bool
> :: Clauses -> Clauses -> Bool
$c> :: Clauses -> Clauses -> Bool
<= :: Clauses -> Clauses -> Bool
$c<= :: Clauses -> Clauses -> Bool
< :: Clauses -> Clauses -> Bool
$c< :: Clauses -> Clauses -> Bool
compare :: Clauses -> Clauses -> Ordering
$ccompare :: Clauses -> Clauses -> Ordering
$cp1Ord :: Eq Clauses
Ord, b -> Clauses -> Clauses
NonEmpty Clauses -> Clauses
Clauses -> Clauses -> Clauses
(Clauses -> Clauses -> Clauses)
-> (NonEmpty Clauses -> Clauses)
-> (forall b. Integral b => b -> Clauses -> Clauses)
-> Semigroup Clauses
forall b. Integral b => b -> Clauses -> Clauses
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: b -> Clauses -> Clauses
$cstimes :: forall b. Integral b => b -> Clauses -> Clauses
sconcat :: NonEmpty Clauses -> Clauses
$csconcat :: NonEmpty Clauses -> Clauses
<> :: Clauses -> Clauses -> Clauses
$c<> :: Clauses -> Clauses -> Clauses
Semigroup, Semigroup Clauses
Clauses
Semigroup Clauses
-> Clauses
-> (Clauses -> Clauses -> Clauses)
-> ([Clauses] -> Clauses)
-> Monoid Clauses
[Clauses] -> Clauses
Clauses -> Clauses -> Clauses
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [Clauses] -> Clauses
$cmconcat :: [Clauses] -> Clauses
mappend :: Clauses -> Clauses -> Clauses
$cmappend :: Clauses -> Clauses -> Clauses
mempty :: Clauses
$cmempty :: Clauses
$cp1Monoid :: Semigroup Clauses
Monoid)

-- | The quantifier in first-order logic.
data Quantifier
  = Forall -- ^ The universal quantifier.
  | Exists -- ^ The existential quantifier.
  deriving (Quantifier -> Quantifier -> Bool
(Quantifier -> Quantifier -> Bool)
-> (Quantifier -> Quantifier -> Bool) -> Eq Quantifier
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Quantifier -> Quantifier -> Bool
$c/= :: Quantifier -> Quantifier -> Bool
== :: Quantifier -> Quantifier -> Bool
$c== :: Quantifier -> Quantifier -> Bool
Eq, Int -> Quantifier -> ShowS
[Quantifier] -> ShowS
Quantifier -> String
(Int -> Quantifier -> ShowS)
-> (Quantifier -> String)
-> ([Quantifier] -> ShowS)
-> Show Quantifier
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Quantifier] -> ShowS
$cshowList :: [Quantifier] -> ShowS
show :: Quantifier -> String
$cshow :: Quantifier -> String
showsPrec :: Int -> Quantifier -> ShowS
$cshowsPrec :: Int -> Quantifier -> ShowS
Show, Eq Quantifier
Eq Quantifier
-> (Quantifier -> Quantifier -> Ordering)
-> (Quantifier -> Quantifier -> Bool)
-> (Quantifier -> Quantifier -> Bool)
-> (Quantifier -> Quantifier -> Bool)
-> (Quantifier -> Quantifier -> Bool)
-> (Quantifier -> Quantifier -> Quantifier)
-> (Quantifier -> Quantifier -> Quantifier)
-> Ord Quantifier
Quantifier -> Quantifier -> Bool
Quantifier -> Quantifier -> Ordering
Quantifier -> Quantifier -> Quantifier
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 :: Quantifier -> Quantifier -> Quantifier
$cmin :: Quantifier -> Quantifier -> Quantifier
max :: Quantifier -> Quantifier -> Quantifier
$cmax :: Quantifier -> Quantifier -> Quantifier
>= :: Quantifier -> Quantifier -> Bool
$c>= :: Quantifier -> Quantifier -> Bool
> :: Quantifier -> Quantifier -> Bool
$c> :: Quantifier -> Quantifier -> Bool
<= :: Quantifier -> Quantifier -> Bool
$c<= :: Quantifier -> Quantifier -> Bool
< :: Quantifier -> Quantifier -> Bool
$c< :: Quantifier -> Quantifier -> Bool
compare :: Quantifier -> Quantifier -> Ordering
$ccompare :: Quantifier -> Quantifier -> Ordering
$cp1Ord :: Eq Quantifier
Ord, Int -> Quantifier
Quantifier -> Int
Quantifier -> [Quantifier]
Quantifier -> Quantifier
Quantifier -> Quantifier -> [Quantifier]
Quantifier -> Quantifier -> Quantifier -> [Quantifier]
(Quantifier -> Quantifier)
-> (Quantifier -> Quantifier)
-> (Int -> Quantifier)
-> (Quantifier -> Int)
-> (Quantifier -> [Quantifier])
-> (Quantifier -> Quantifier -> [Quantifier])
-> (Quantifier -> Quantifier -> [Quantifier])
-> (Quantifier -> Quantifier -> Quantifier -> [Quantifier])
-> Enum Quantifier
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Quantifier -> Quantifier -> Quantifier -> [Quantifier]
$cenumFromThenTo :: Quantifier -> Quantifier -> Quantifier -> [Quantifier]
enumFromTo :: Quantifier -> Quantifier -> [Quantifier]
$cenumFromTo :: Quantifier -> Quantifier -> [Quantifier]
enumFromThen :: Quantifier -> Quantifier -> [Quantifier]
$cenumFromThen :: Quantifier -> Quantifier -> [Quantifier]
enumFrom :: Quantifier -> [Quantifier]
$cenumFrom :: Quantifier -> [Quantifier]
fromEnum :: Quantifier -> Int
$cfromEnum :: Quantifier -> Int
toEnum :: Int -> Quantifier
$ctoEnum :: Int -> Quantifier
pred :: Quantifier -> Quantifier
$cpred :: Quantifier -> Quantifier
succ :: Quantifier -> Quantifier
$csucc :: Quantifier -> Quantifier
Enum, Quantifier
Quantifier -> Quantifier -> Bounded Quantifier
forall a. a -> a -> Bounded a
maxBound :: Quantifier
$cmaxBound :: Quantifier
minBound :: Quantifier
$cminBound :: Quantifier
Bounded)

-- | The binary logical connective.
data Connective
  = And        -- ^ Conjunction.
  | Or         -- ^ Disjunction.
  | Implies    -- ^ Implication.
  | Equivalent -- ^ Equivalence.
  | Xor        -- ^ Exclusive or.
  deriving (Int -> Connective -> ShowS
[Connective] -> ShowS
Connective -> String
(Int -> Connective -> ShowS)
-> (Connective -> String)
-> ([Connective] -> ShowS)
-> Show Connective
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Connective] -> ShowS
$cshowList :: [Connective] -> ShowS
show :: Connective -> String
$cshow :: Connective -> String
showsPrec :: Int -> Connective -> ShowS
$cshowsPrec :: Int -> Connective -> ShowS
Show, Connective -> Connective -> Bool
(Connective -> Connective -> Bool)
-> (Connective -> Connective -> Bool) -> Eq Connective
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Connective -> Connective -> Bool
$c/= :: Connective -> Connective -> Bool
== :: Connective -> Connective -> Bool
$c== :: Connective -> Connective -> Bool
Eq, Eq Connective
Eq Connective
-> (Connective -> Connective -> Ordering)
-> (Connective -> Connective -> Bool)
-> (Connective -> Connective -> Bool)
-> (Connective -> Connective -> Bool)
-> (Connective -> Connective -> Bool)
-> (Connective -> Connective -> Connective)
-> (Connective -> Connective -> Connective)
-> Ord Connective
Connective -> Connective -> Bool
Connective -> Connective -> Ordering
Connective -> Connective -> Connective
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 :: Connective -> Connective -> Connective
$cmin :: Connective -> Connective -> Connective
max :: Connective -> Connective -> Connective
$cmax :: Connective -> Connective -> Connective
>= :: Connective -> Connective -> Bool
$c>= :: Connective -> Connective -> Bool
> :: Connective -> Connective -> Bool
$c> :: Connective -> Connective -> Bool
<= :: Connective -> Connective -> Bool
$c<= :: Connective -> Connective -> Bool
< :: Connective -> Connective -> Bool
$c< :: Connective -> Connective -> Bool
compare :: Connective -> Connective -> Ordering
$ccompare :: Connective -> Connective -> Ordering
$cp1Ord :: Eq Connective
Ord, Int -> Connective
Connective -> Int
Connective -> [Connective]
Connective -> Connective
Connective -> Connective -> [Connective]
Connective -> Connective -> Connective -> [Connective]
(Connective -> Connective)
-> (Connective -> Connective)
-> (Int -> Connective)
-> (Connective -> Int)
-> (Connective -> [Connective])
-> (Connective -> Connective -> [Connective])
-> (Connective -> Connective -> [Connective])
-> (Connective -> Connective -> Connective -> [Connective])
-> Enum Connective
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Connective -> Connective -> Connective -> [Connective]
$cenumFromThenTo :: Connective -> Connective -> Connective -> [Connective]
enumFromTo :: Connective -> Connective -> [Connective]
$cenumFromTo :: Connective -> Connective -> [Connective]
enumFromThen :: Connective -> Connective -> [Connective]
$cenumFromThen :: Connective -> Connective -> [Connective]
enumFrom :: Connective -> [Connective]
$cenumFrom :: Connective -> [Connective]
fromEnum :: Connective -> Int
$cfromEnum :: Connective -> Int
toEnum :: Int -> Connective
$ctoEnum :: Int -> Connective
pred :: Connective -> Connective
$cpred :: Connective -> Connective
succ :: Connective -> Connective
$csucc :: Connective -> Connective
Enum, Connective
Connective -> Connective -> Bounded Connective
forall a. a -> a -> Bounded a
maxBound :: Connective
$cmaxBound :: Connective
minBound :: Connective
$cminBound :: Connective
Bounded)

-- | Associativity of a given binary logical connective.
--
-- >>> isAssociative Implies
-- False
--
-- >>> isAssociative And
-- True
isAssociative :: Connective -> Bool
isAssociative :: Connective -> Bool
isAssociative = \case
  Connective
And        -> Bool
True
  Connective
Or         -> Bool
True
  Connective
Implies    -> Bool
False
  Connective
Equivalent -> Bool
True
  Connective
Xor        -> Bool
True

-- | The formula in first-order logic.
data Formula
  = Atomic Literal
  | Negate Formula
  | Connected Connective Formula Formula
  | Quantified Quantifier Var Formula
  deriving (Int -> Formula -> ShowS
[Formula] -> ShowS
Formula -> String
(Int -> Formula -> ShowS)
-> (Formula -> String) -> ([Formula] -> ShowS) -> Show Formula
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Formula] -> ShowS
$cshowList :: [Formula] -> ShowS
show :: Formula -> String
$cshow :: Formula -> String
showsPrec :: Int -> Formula -> ShowS
$cshowsPrec :: Int -> Formula -> ShowS
Show, Formula -> Formula -> Bool
(Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool) -> Eq Formula
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Formula -> Formula -> Bool
$c/= :: Formula -> Formula -> Bool
== :: Formula -> Formula -> Bool
$c== :: Formula -> Formula -> Bool
Eq, Eq Formula
Eq Formula
-> (Formula -> Formula -> Ordering)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Formula)
-> (Formula -> Formula -> Formula)
-> Ord Formula
Formula -> Formula -> Bool
Formula -> Formula -> Ordering
Formula -> Formula -> Formula
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 :: Formula -> Formula -> Formula
$cmin :: Formula -> Formula -> Formula
max :: Formula -> Formula -> Formula
$cmax :: Formula -> Formula -> Formula
>= :: Formula -> Formula -> Bool
$c>= :: Formula -> Formula -> Bool
> :: Formula -> Formula -> Bool
$c> :: Formula -> Formula -> Bool
<= :: Formula -> Formula -> Bool
$c<= :: Formula -> Formula -> Bool
< :: Formula -> Formula -> Bool
$c< :: Formula -> Formula -> Bool
compare :: Formula -> Formula -> Ordering
$ccompare :: Formula -> Formula -> Ordering
$cp1Ord :: Eq Formula
Ord)

-- | A logical expression is either a clause or a formula.
data LogicalExpression
  = Clause Clause
  | Formula Formula
  deriving (Int -> LogicalExpression -> ShowS
[LogicalExpression] -> ShowS
LogicalExpression -> String
(Int -> LogicalExpression -> ShowS)
-> (LogicalExpression -> String)
-> ([LogicalExpression] -> ShowS)
-> Show LogicalExpression
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LogicalExpression] -> ShowS
$cshowList :: [LogicalExpression] -> ShowS
show :: LogicalExpression -> String
$cshow :: LogicalExpression -> String
showsPrec :: Int -> LogicalExpression -> ShowS
$cshowsPrec :: Int -> LogicalExpression -> ShowS
Show, LogicalExpression -> LogicalExpression -> Bool
(LogicalExpression -> LogicalExpression -> Bool)
-> (LogicalExpression -> LogicalExpression -> Bool)
-> Eq LogicalExpression
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LogicalExpression -> LogicalExpression -> Bool
$c/= :: LogicalExpression -> LogicalExpression -> Bool
== :: LogicalExpression -> LogicalExpression -> Bool
$c== :: LogicalExpression -> LogicalExpression -> Bool
Eq, Eq LogicalExpression
Eq LogicalExpression
-> (LogicalExpression -> LogicalExpression -> Ordering)
-> (LogicalExpression -> LogicalExpression -> Bool)
-> (LogicalExpression -> LogicalExpression -> Bool)
-> (LogicalExpression -> LogicalExpression -> Bool)
-> (LogicalExpression -> LogicalExpression -> Bool)
-> (LogicalExpression -> LogicalExpression -> LogicalExpression)
-> (LogicalExpression -> LogicalExpression -> LogicalExpression)
-> Ord LogicalExpression
LogicalExpression -> LogicalExpression -> Bool
LogicalExpression -> LogicalExpression -> Ordering
LogicalExpression -> LogicalExpression -> LogicalExpression
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 :: LogicalExpression -> LogicalExpression -> LogicalExpression
$cmin :: LogicalExpression -> LogicalExpression -> LogicalExpression
max :: LogicalExpression -> LogicalExpression -> LogicalExpression
$cmax :: LogicalExpression -> LogicalExpression -> LogicalExpression
>= :: LogicalExpression -> LogicalExpression -> Bool
$c>= :: LogicalExpression -> LogicalExpression -> Bool
> :: LogicalExpression -> LogicalExpression -> Bool
$c> :: LogicalExpression -> LogicalExpression -> Bool
<= :: LogicalExpression -> LogicalExpression -> Bool
$c<= :: LogicalExpression -> LogicalExpression -> Bool
< :: LogicalExpression -> LogicalExpression -> Bool
$c< :: LogicalExpression -> LogicalExpression -> Bool
compare :: LogicalExpression -> LogicalExpression -> Ordering
$ccompare :: LogicalExpression -> LogicalExpression -> Ordering
$cp1Ord :: Eq LogicalExpression
Ord)

-- | A theorem is zero or more axioms and a conjecture.
data Theorem = Theorem {
  Theorem -> [Formula]
axioms :: [Formula],
  Theorem -> Formula
conjecture :: Formula
} deriving (Int -> Theorem -> ShowS
[Theorem] -> ShowS
Theorem -> String
(Int -> Theorem -> ShowS)
-> (Theorem -> String) -> ([Theorem] -> ShowS) -> Show Theorem
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Theorem] -> ShowS
$cshowList :: [Theorem] -> ShowS
show :: Theorem -> String
$cshow :: Theorem -> String
showsPrec :: Int -> Theorem -> ShowS
$cshowsPrec :: Int -> Theorem -> ShowS
Show, Theorem -> Theorem -> Bool
(Theorem -> Theorem -> Bool)
-> (Theorem -> Theorem -> Bool) -> Eq Theorem
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Theorem -> Theorem -> Bool
$c/= :: Theorem -> Theorem -> Bool
== :: Theorem -> Theorem -> Bool
$c== :: Theorem -> Theorem -> Bool
Eq, Eq Theorem
Eq Theorem
-> (Theorem -> Theorem -> Ordering)
-> (Theorem -> Theorem -> Bool)
-> (Theorem -> Theorem -> Bool)
-> (Theorem -> Theorem -> Bool)
-> (Theorem -> Theorem -> Bool)
-> (Theorem -> Theorem -> Theorem)
-> (Theorem -> Theorem -> Theorem)
-> Ord Theorem
Theorem -> Theorem -> Bool
Theorem -> Theorem -> Ordering
Theorem -> Theorem -> Theorem
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 :: Theorem -> Theorem -> Theorem
$cmin :: Theorem -> Theorem -> Theorem
max :: Theorem -> Theorem -> Theorem
$cmax :: Theorem -> Theorem -> Theorem
>= :: Theorem -> Theorem -> Bool
$c>= :: Theorem -> Theorem -> Bool
> :: Theorem -> Theorem -> Bool
$c> :: Theorem -> Theorem -> Bool
<= :: Theorem -> Theorem -> Bool
$c<= :: Theorem -> Theorem -> Bool
< :: Theorem -> Theorem -> Bool
$c< :: Theorem -> Theorem -> Bool
compare :: Theorem -> Theorem -> Ordering
$ccompare :: Theorem -> Theorem -> Ordering
$cp1Ord :: Eq Theorem
Ord)


-- * Syntactic sugar

-- $sugar
--
-- Instances, type synonyms and pattern synonyms for syntactic convenience.

instance IsString Term where
  fromString :: String -> Term
fromString = FunctionSymbol -> Term
Constant (FunctionSymbol -> Term)
-> (String -> FunctionSymbol) -> String -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> FunctionSymbol
forall a. IsString a => String -> a
fromString

instance IsString Literal where
  fromString :: String -> Literal
fromString = (PredicateSymbol -> [Term] -> Literal)
-> [Term] -> PredicateSymbol -> Literal
forall a b c. (a -> b -> c) -> b -> a -> c
flip PredicateSymbol -> [Term] -> Literal
Predicate [] (PredicateSymbol -> Literal)
-> (String -> PredicateSymbol) -> String -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> PredicateSymbol
forall a. IsString a => String -> a
fromString

instance IsString e => IsString (Signed e) where
  fromString :: String -> Signed e
fromString = Sign -> e -> Signed e
forall e. Sign -> e -> Signed e
Signed Sign
Positive (e -> Signed e) -> (String -> e) -> String -> Signed e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> e
forall a. IsString a => String -> a
fromString

instance IsString Clause where
  fromString :: String -> Clause
fromString = Signed Literal -> Clause
UnitClause (Signed Literal -> Clause)
-> (String -> Signed Literal) -> String -> Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Signed Literal
forall a. IsString a => String -> a
fromString

instance IsString Formula where
  fromString :: String -> Formula
fromString = PredicateSymbol -> Formula
Proposition (PredicateSymbol -> Formula)
-> (String -> PredicateSymbol) -> String -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> PredicateSymbol
forall a. IsString a => String -> a
fromString


-- ** Function symbols

-- | The type of a function symbol - a mapping from zero or more terms
-- to a term.
type Function = [Term] -> Term

-- | The type of a constant symbol.
type Constant = Term

-- | The type of a function symbol with one argument.
type UnaryFunction = Term -> Term

-- | The type of a function symbol with two arguments.
type BinaryFunction = Term -> Term -> Term

-- | The type of a function symbol with three arguments.
type TernaryFunction = Term -> Term -> Term -> Term

-- | Build a proposition from a predicate symbol.
#if __GLASGOW_HASKELL__ == 800
pattern Constant :: FunctionSymbol -> Term
#else
pattern Constant :: FunctionSymbol -> Constant
#endif
pattern $bConstant :: FunctionSymbol -> Term
$mConstant :: forall r. Term -> (FunctionSymbol -> r) -> (Void# -> r) -> r
Constant f = Function f []

-- | Build a unary function from a function symbol.
#if __GLASGOW_HASKELL__ == 800
pattern UnaryFunction :: FunctionSymbol -> Term -> Term
#else
pattern UnaryFunction :: FunctionSymbol -> UnaryFunction
#endif
pattern $bUnaryFunction :: FunctionSymbol -> Term -> Term
$mUnaryFunction :: forall r.
Term -> (FunctionSymbol -> Term -> r) -> (Void# -> r) -> r
UnaryFunction f a = Function f [a]

-- | Build a binary function from a function symbol.
#if __GLASGOW_HASKELL__ == 800
pattern BinaryFunction :: FunctionSymbol -> Term -> Term -> Term
#else
pattern BinaryFunction :: FunctionSymbol -> BinaryFunction
#endif
pattern $bBinaryFunction :: FunctionSymbol -> Term -> Term -> Term
$mBinaryFunction :: forall r.
Term -> (FunctionSymbol -> Term -> Term -> r) -> (Void# -> r) -> r
BinaryFunction f a b = Function f [a, b]

-- | Build a ternary function from a function symbol.
#if __GLASGOW_HASKELL__ == 800
pattern TernaryFunction :: FunctionSymbol -> Term -> Term -> Term -> Term
#else
pattern TernaryFunction :: FunctionSymbol -> TernaryFunction
#endif
pattern $bTernaryFunction :: FunctionSymbol -> Term -> Term -> Term -> Term
$mTernaryFunction :: forall r.
Term
-> (FunctionSymbol -> Term -> Term -> Term -> r)
-> (Void# -> r)
-> r
TernaryFunction f a b c = Function f [a, b, c]


-- ** Predicate symbols

-- | The type of a predicate symbol - a mapping from zero or more terms
-- to a formula.
type Predicate = [Term] -> Formula

-- | The type of a proposition.
type Proposition = Formula

-- | The type of a predicate symbol with one argument.
type UnaryPredicate = Term -> Formula

-- | The type of a predicate symbol with two arguments.
type BinaryPredicate = Term -> Term -> Formula

-- | The type of a function symbol with three arguments.
type TernaryPredicate = Term -> Term -> Term -> Formula

-- | Build a proposition from a predicate symbol.
#if __GLASGOW_HASKELL__ == 800
pattern Proposition :: PredicateSymbol -> Formula
#else
pattern Proposition :: PredicateSymbol -> Proposition
#endif
pattern $bProposition :: PredicateSymbol -> Formula
$mProposition :: forall r. Formula -> (PredicateSymbol -> r) -> (Void# -> r) -> r
Proposition p = Atomic (Predicate p [])

-- | Build a unary predicate from a predicate symbol.
#if __GLASGOW_HASKELL__ == 800
pattern UnaryPredicate :: PredicateSymbol -> Term -> Formula
#else
pattern UnaryPredicate :: PredicateSymbol -> UnaryPredicate
#endif
pattern $bUnaryPredicate :: PredicateSymbol -> Term -> Formula
$mUnaryPredicate :: forall r.
Formula -> (PredicateSymbol -> Term -> r) -> (Void# -> r) -> r
UnaryPredicate p a = Atomic (Predicate p [a])

-- | Build a binary predicate from a predicate symbol.
#if __GLASGOW_HASKELL__ == 800
pattern BinaryPredicate :: PredicateSymbol -> Term -> Term -> Formula
#else
pattern BinaryPredicate :: PredicateSymbol -> BinaryPredicate
#endif
pattern $bBinaryPredicate :: PredicateSymbol -> Term -> Term -> Formula
$mBinaryPredicate :: forall r.
Formula
-> (PredicateSymbol -> Term -> Term -> r) -> (Void# -> r) -> r
BinaryPredicate p a b = Atomic (Predicate p [a, b])

-- | Build a ternary predicate from a predicate symbol.
#if __GLASGOW_HASKELL__ == 800
pattern TernaryPredicate :: PredicateSymbol -> Term -> Term -> Term -> Formula
#else
pattern TernaryPredicate :: PredicateSymbol -> TernaryPredicate
#endif
pattern $bTernaryPredicate :: PredicateSymbol -> Term -> Term -> Term -> Formula
$mTernaryPredicate :: forall r.
Formula
-> (PredicateSymbol -> Term -> Term -> Term -> r)
-> (Void# -> r)
-> r
TernaryPredicate p a b c = Atomic (Predicate p [a, b, c])


-- ** Literals

-- | The positive tautology literal.
pattern TautologyLiteral :: Signed Literal
pattern $bTautologyLiteral :: Signed Literal
$mTautologyLiteral :: forall r. Signed Literal -> (Void# -> r) -> (Void# -> r) -> r
TautologyLiteral = Signed Positive (Propositional True)

-- | The positive falsity literal.
pattern FalsityLiteral :: Signed Literal
pattern $bFalsityLiteral :: Signed Literal
$mFalsityLiteral :: forall r. Signed Literal -> (Void# -> r) -> (Void# -> r) -> r
FalsityLiteral = Signed Positive (Propositional False)


-- ** Clauses

-- | A unit clause with a single positive tautology literal.
-- 'TautologyClause' is semantically (but not syntactically) equivalent to
-- 'Tautology'.
pattern TautologyClause :: Clause
pattern $bTautologyClause :: Clause
$mTautologyClause :: forall r. Clause -> (Void# -> r) -> (Void# -> r) -> r
TautologyClause = UnitClause TautologyLiteral

-- | The empty clause.
-- 'EmptyClause' is semantically (but not syntactically) equivalent to 'Falsity'.
pattern EmptyClause :: Clause
pattern $bEmptyClause :: Clause
$mEmptyClause :: forall r. Clause -> (Void# -> r) -> (Void# -> r) -> r
EmptyClause = Literals []

-- | The unit clause.
pattern UnitClause :: Signed Literal -> Clause
pattern $bUnitClause :: Signed Literal -> Clause
$mUnitClause :: forall r. Clause -> (Signed Literal -> r) -> (Void# -> r) -> r
UnitClause l = Literals [l]

-- | The set of clauses with a single clause in it.
pattern NoClauses :: Clauses
pattern $bNoClauses :: Clauses
$mNoClauses :: forall r. Clauses -> (Void# -> r) -> (Void# -> r) -> r
NoClauses = Clauses []

-- | The set of clauses with a single clause in it.
pattern SingleClause :: Clause -> Clauses
pattern $bSingleClause :: Clause -> Clauses
$mSingleClause :: forall r. Clauses -> (Clause -> r) -> (Void# -> r) -> r
SingleClause c = Clauses [c]


-- ** Formulas

-- | The logical tautology.
pattern Tautology :: Formula
pattern $bTautology :: Formula
$mTautology :: forall r. Formula -> (Void# -> r) -> (Void# -> r) -> r
Tautology = Atomic (Propositional True)

-- | The logical false.
-- 'Falsity' is semantically (but not syntactically) equivalent to 'EmptyClause'.
pattern Falsity :: Formula
pattern $bFalsity :: Formula
$mFalsity :: forall r. Formula -> (Void# -> r) -> (Void# -> r) -> r
Falsity = Atomic (Propositional False)

-- | A logical claim is a conjecture entailed by the empty set of axioms.
pattern Claim :: Formula -> Theorem
pattern $bClaim :: Formula -> Theorem
$mClaim :: forall r. Theorem -> (Formula -> r) -> (Void# -> r) -> r
Claim f = Theorem [] f