{-# LANGUAGE LambdaCase #-}

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

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

  -- ** Proofs
  liftContradiction,
  unliftContradiction,
  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
liftContradiction (Contradiction Rule 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
isContradiction LogicalExpression
e = Contradiction f -> Maybe (Contradiction f)
forall a. a -> Maybe a
Just (Rule f -> Contradiction f
forall f. Rule f -> Contradiction f
Contradiction Rule 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
isContradiction = \case
  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
d Contradiction f
c) = Derivation f -> Sequent f -> Derivation f
forall f. Ord f => Derivation f -> Sequent f -> Derivation f
addSequent 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
liftContradiction Contradiction 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
Contradiction Rule f
r)
      | Bool
otherwise = Maybe (Contradiction f)
forall a. Maybe a
Nothing