```{-# LANGUAGE LambdaCase #-}

{-|
Module       : ATP.FirstOrder.Conversion
Description  : Conversions between first-order expressions.
Copyright    : (c) Evgenii Kotelnikov, 2019-2021
Maintainer   : evgeny.kotelnikov@gmail.com
Stability    : experimental
-}

module ATP.FirstOrder.Conversion (
-- * Conversions
-- ** Formulas
liftSignedLiteral,
unliftSignedLiteral,
liftClause,
unliftClause,

-- ** Proofs
liftRefutation,
unliftRefutation
) where

import qualified Data.Map as M (partition, toList)

import ATP.FirstOrder.Core
import ATP.FirstOrder.Derivation
import ATP.FirstOrder.Occurrence

-- * Conversions

-- ** Formulas

-- | Convert a clause to a full first-order formula.
liftClause :: Clause -> Formula
liftClause :: Clause -> Formula
liftClause = \case
Clause
EmptyClause -> Formula
Falsity
Literals [Signed Literal]
ls -> Formula -> Formula
close (Formula -> Formula)
-> ([Signed Literal] -> Formula) -> [Signed Literal] -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Formula -> Formula -> Formula) -> [Formula] -> Formula
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (Connective -> Formula -> Formula -> Formula
Connected Connective
Or) ([Formula] -> Formula)
-> ([Signed Literal] -> [Formula]) -> [Signed Literal] -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Signed Literal -> Formula) -> [Signed Literal] -> [Formula]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Signed Literal -> Formula
liftSignedLiteral ([Signed Literal] -> Formula) -> [Signed Literal] -> Formula
forall a b. (a -> b) -> a -> b
\$ [Signed Literal]
ls

-- | Try to convert a first-order formula /f/ to a clause.
-- This function succeeds if /f/ is a tree of disjunctions of
-- (negated) atomic formula.
unliftClause :: Formula -> Maybe Clause
unliftClause :: Formula -> Maybe Clause
unliftClause = Formula -> Maybe Clause
unlift (Formula -> Maybe Clause)
-> (Formula -> Formula) -> Formula -> Maybe Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula -> Formula
unprefix
where
unlift :: Formula -> Maybe Clause
unlift = \case
Connected Connective
Or Formula
f Formula
g -> Clause -> Clause -> Clause
forall a. Monoid a => a -> a -> a
mappend (Clause -> Clause -> Clause)
-> Maybe Clause -> Maybe (Clause -> Clause)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<\$> Formula -> Maybe Clause
unlift Formula
f Maybe (Clause -> Clause) -> Maybe Clause -> Maybe Clause
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Formula -> Maybe Clause
unlift Formula
g
Formula
f -> Signed Literal -> Clause
UnitClause (Signed Literal -> Clause)
-> Maybe (Signed Literal) -> Maybe Clause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<\$> Formula -> Maybe (Signed Literal)
unliftSignedLiteral Formula
f

-- | Convert a signed literal to a (negated) atomic formula.
liftSignedLiteral :: Signed Literal -> Formula
liftSignedLiteral :: Signed Literal -> Formula
liftSignedLiteral (Signed Sign
s Literal
l) = case Sign
s of
Sign
Positive -> Literal -> Formula
Atomic Literal
l
Sign
Negative -> Formula -> Formula
Negate (Literal -> Formula
Atomic Literal
l)

-- | Try to convert a first-order formula /f/ to a signed literal.
-- This function succeeds if /f/ is a (negated) atomic formula.
unliftSignedLiteral :: Formula -> Maybe (Signed Literal)
unliftSignedLiteral :: Formula -> Maybe (Signed Literal)
unliftSignedLiteral = \case
Atomic Literal
l -> Signed Literal -> Maybe (Signed Literal)
forall a. a -> Maybe a
Just (Sign -> Literal -> Signed Literal
forall e. Sign -> e -> Signed e
Signed Sign
Positive Literal
l)
Negate Formula
f -> Sign -> Signed Literal -> Signed Literal
forall e. Sign -> Signed e -> Signed e
sign Sign
Negative (Signed Literal -> Signed Literal)
-> Maybe (Signed Literal) -> Maybe (Signed Literal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<\$> Formula -> Maybe (Signed Literal)
unliftSignedLiteral Formula
f
Formula
_ -> Maybe (Signed Literal)
forall a. Maybe a
Nothing

-- ** Proofs

-- | Convert a contradiction to an inference.
liftContradiction :: Contradiction f -> Inference f
liftContradiction :: Contradiction f -> Inference f
r) = Rule f -> LogicalExpression -> Inference f
forall f. Rule f -> LogicalExpression -> Inference f
Inference Rule f
r (Formula -> LogicalExpression
Formula Formula
Falsity)

-- | Try to convert an inference to a contradiction.
unliftContradiction :: Inference f -> Maybe (Contradiction f)
unliftContradiction :: Inference f -> Maybe (Contradiction f)
unliftContradiction (Inference Rule f
r LogicalExpression
e)
| LogicalExpression -> Bool
e = Contradiction f -> Maybe (Contradiction f)
forall a. a -> Maybe a
Just (Rule f -> Contradiction f
forall f. Rule f -> Contradiction f
r)
| Bool
otherwise = Maybe (Contradiction f)
forall a. Maybe a
Nothing

-- | Check whether a given expression is either a falsity or an empty clause.
isContradiction :: LogicalExpression -> Bool
isContradiction :: LogicalExpression -> Bool
Clause Clause
c | Formula
Falsity <- Clause -> Formula
liftClause Clause
c -> Bool
True
Formula Formula
Falsity -> Bool
True
LogicalExpression
_ -> Bool
False

-- | Convert a refutation to a derivation.
liftRefutation :: Ord f => f -> Refutation f -> Derivation f
liftRefutation :: f -> Refutation f -> Derivation f
liftRefutation f
f (Refutation Derivation f
c) = Derivation f -> Sequent f -> Derivation f
forall f. Ord f => Derivation f -> Sequent f -> Derivation f
d (f -> Inference f -> Sequent f
forall f. f -> Inference f -> Sequent f
Sequent f
f (Contradiction f -> Inference f
forall f. Contradiction f -> Inference f
c))

-- | Try to convert a derivation to a refutation.
-- This function succeds if the derivation has exactly one inference
-- resulting in contradiction.
unliftRefutation :: Derivation f -> Maybe (Refutation f)
unliftRefutation :: Derivation f -> Maybe (Refutation f)
unliftRefutation (Derivation Map f (Inference f)
is) = Derivation f -> Contradiction f -> Refutation f
forall f. Derivation f -> Contradiction f -> Refutation f
Refutation (Map f (Inference f) -> Derivation f
forall f. Map f (Inference f) -> Derivation f
Derivation Map f (Inference f)
is') (Contradiction f -> Refutation f)
-> Maybe (Contradiction f) -> Maybe (Refutation f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<\$> Maybe (Contradiction f)
c
where
(Map f (Inference f)
cs, Map f (Inference f)
is') = (Inference f -> Bool)
-> Map f (Inference f)
-> (Map f (Inference f), Map f (Inference f))
forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
M.partition (LogicalExpression -> Bool
isContradiction (LogicalExpression -> Bool)
-> (Inference f -> LogicalExpression) -> Inference f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Inference f -> LogicalExpression
forall f. Inference f -> LogicalExpression
consequent) Map f (Inference f)
is
c :: Maybe (Contradiction f)
c | [(f
_, Inference Rule f
r LogicalExpression
_)] <- Map f (Inference f) -> [(f, Inference f)]
forall k a. Map k a -> [(k, a)]
M.toList Map f (Inference f)
cs = Contradiction f -> Maybe (Contradiction f)
forall a. a -> Maybe a
Just (Rule f -> Contradiction f
forall f. Rule f -> Contradiction f