{-# LANGUAGE CPP #-}
{-# LANGUAGE LambdaCase #-}

{-|
Module       : ATP.FirstOrder.Simplification
Description  : Simplification of first-order expressions.
Copyright    : (c) Evgenii Kotelnikov, 2019-2021
License      : GPL-3
Maintainer   : evgeny.kotelnikov@gmail.com
Stability    : experimental
-}
module ATP.FirstOrder.Simplification (
  -- * Simplification
  Simplify(..)
) where

import ATP.FirstOrder.Core
import ATP.FirstOrder.Smart

-- $setup
-- >>> :set -XOverloadedStrings
-- >>> :load Property.Generators


-- * Simplification

-- | A class of first-order expressions that 'simplify' syntactically shrinks
-- while preserving their evaluation.
class Simplify a where
  simplify :: a -> a

-- | Simplify the given formula by replacing each of its constructors with
-- corresponding smart constructors.
instance Simplify LogicalExpression where
  simplify :: LogicalExpression -> LogicalExpression
simplify = \case
    Clause  Clause
c -> Clause -> LogicalExpression
Clause  (Clause -> Clause
forall a. Simplify a => a -> a
simplify Clause
c)
    Formula Formula
f -> Formula -> LogicalExpression
Formula (Formula -> Formula
forall a. Simplify a => a -> a
simplify Formula
f)

-- | Simplify the given clause by replacing the 'Literals' constructor with
-- the smart constructor 'clause'. The effects of simplification are
-- the following.
--
-- * @'simplify' c@ does not contain negative constant literals.
-- * @'simplify' c@ does not contain falsum literals.
-- * @'simplify' c@ does not contain redundant tautology literals.
--
-- >>> simplify (UnitClause (Signed Negative (Propositional True)))
-- Literals {getLiterals = []}
--
-- >>> simplify (Literals [FalsityLiteral, Signed Positive (Predicate "p" [])])
-- Literals {getLiterals = [Signed {signof = Positive, unsign = Predicate (PredicateSymbol "p") []}]}
--
-- >>> simplify (Literals [TautologyLiteral, Signed Positive (Predicate "p" [])])
-- Literals {getLiterals = [Signed {signof = Positive, unsign = Propositional True}]}
--
instance Simplify Clause where
  simplify :: Clause -> Clause
simplify = [Signed Literal] -> Clause
forall (f :: * -> *). Foldable f => f (Signed Literal) -> Clause
clause ([Signed Literal] -> Clause)
-> (Clause -> [Signed Literal]) -> Clause -> Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> [Signed Literal]
getLiterals

-- | Simplify the given clause set by replacing the 'Clauses' constructor with
-- the smart constructor 'clauses'. The effects of simplification are
-- the following.
--
-- * @'simplify' c@ does not contain negative constant literals.
-- * @'simplify' c@ does not contain falsum literals.
-- * @'simplify' c@ does not contain tautology literals.
-- * @'simplify' c@ does not contain redundant falsum literals.
--
-- >>> simplify (SingleClause (UnitClause (Signed Negative (Propositional True))))
-- Clauses {getClauses = [Literals {getLiterals = []}]}
--
-- >>> simplify (SingleClause (Literals [FalsityLiteral, Signed Positive (Predicate "p" [])]))
-- Clauses {getClauses = [Literals {getLiterals = [Signed {signof = Positive, unsign = Predicate (PredicateSymbol "p") []}]}]}
--
-- >>> simplify (SingleClause (Literals [TautologyLiteral, Signed Positive (Predicate "p" [])]))
-- Clauses {getClauses = []}
--
instance Simplify Clauses where
  simplify :: Clauses -> Clauses
simplify = [Clause] -> Clauses
forall (f :: * -> *). Foldable f => f Clause -> Clauses
clauses ([Clause] -> Clauses)
-> (Clauses -> [Clause]) -> Clauses -> Clauses
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clauses -> [Clause]
getClauses

-- | Simplify the given formula by replacing each of its constructors with
-- corresponding smart constructors. The effects of simplification are
-- the following.
--
-- * @'simplify' f@ does not contain nested negations.
-- * @'simplify' f@ does not contain some of the constant atomic formulas from @f@.
-- * All chained applications of any binary connective inside
--   @'simplify' f@ are right-associative.
--
-- Any formula built only using smart constructors is simplified by construction.
--
-- >>> simplify (Connected Or tautology (Atomic (Predicate "p" [])))
-- Atomic (Propositional True)
--
-- >>> simplify (Negate (Negate (Atomic (Predicate "p" []))))
-- Atomic (Predicate "p" [])
--
-- >>> simplify (Connected And (Connected And (Atomic (Predicate "p" [])) (Atomic (Predicate "q" []))) (Atomic (Predicate "r" [])))
-- Connected And (Atomic (Predicate "p" [])) (Connected And (Atomic (Predicate "q" [])) (Atomic (Predicate "r" [])))
--
instance Simplify Formula where
  simplify :: Formula -> Formula
simplify = \case
    Atomic Literal
l -> Literal -> Formula
Atomic Literal
l
    Negate Formula
f -> Formula -> Formula
neg (Formula -> Formula
forall a. Simplify a => a -> a
simplify Formula
f)
    Connected  Connective
c Formula
f Formula
g -> Formula -> Formula
forall a. Simplify a => a -> a
simplify Formula
f Formula -> Formula -> Formula
# Formula -> Formula
forall a. Simplify a => a -> a
simplify Formula
g where # :: Formula -> Formula -> Formula
(#) = Connective -> Formula -> Formula -> Formula
smartConnective Connective
c
    Quantified Quantifier
q Var
v Formula
f -> Quantifier -> (Var, Formula) -> Formula
forall b. Binder b => Quantifier -> b -> Formula
quantified Quantifier
q (Var
v, Formula -> Formula
forall a. Simplify a => a -> a
simplify Formula
f)

-- | Convert a binary connective to its corresponding smart constructor.
smartConnective :: Connective -> Formula -> Formula -> Formula
smartConnective :: Connective -> Formula -> Formula -> Formula
smartConnective = \case
  Connective
And        -> Formula -> Formula -> Formula
(/\)
  Connective
Or         -> Formula -> Formula -> Formula
(\/)
  Connective
Implies    -> Formula -> Formula -> Formula
(==>)
  Connective
Equivalent -> Formula -> Formula -> Formula
(<=>)
  Connective
Xor        -> Formula -> Formula -> Formula
(<~>)

-- | Simplify the given theorem by flattening the conjunction of its premises
-- and its conjecture.
instance Simplify Theorem where
  simplify :: Theorem -> Theorem
simplify (Theorem [Formula]
as Formula
c) = [Formula] -> [Formula]
forall (f :: * -> *). Foldable f => f Formula -> [Formula]
flattenConjunction ((Formula -> Formula) -> [Formula] -> [Formula]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Formula -> Formula
forall a. Simplify a => a -> a
simplify [Formula]
as) [Formula] -> Formula -> Theorem
forall (f :: * -> *). Foldable f => f Formula -> Formula -> Theorem
|- Formula -> Formula
forall a. Simplify a => a -> a
simplify Formula
c