{-# LANGUAGE CPP #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}

{-|
Module       : ATP.Codec.TPTP
Description  : Coding and decoding of unsorted first-order logic in TPTP.
Copyright    : (c) Evgenii Kotelnikov, 2019-2021
License      : GPL-3
Maintainer   : evgeny.kotelnikov@gmail.com
Stability    : experimental
-}

module ATP.Codec.TPTP (
  encode,
  decode,
  encodeFormula,
  decodeFormula,
  encodeClause,
  decodeClause,
  encodeTheorem,
  encodeClauses,
  decodeSolution
) where

import Control.Applicative (liftA2)
import Control.Monad (foldM)
import Control.Monad.Trans (lift)
import Data.Functor (($>))
import Data.List (genericIndex, find)
import qualified Data.List.NonEmpty as NE (toList)
import Data.Map (Map, (!))
#if !MIN_VERSION_base(4, 11, 0)
import Data.Semigroup (Semigroup(..))
#endif
import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.TPTP as TPTP

import ATP.Internal.Enumeration
import ATP.Error
import ATP.FOL


-- * Coding and decoding

-- | Encode a variable in TPTP.
--
-- >>> encodeVar 0
-- Var "X"
--
-- >>> encodeVar 1
-- Var "Y"
--
-- >>> encodeVar 7
-- Var "X1"
--
-- >>> encodeVar (-1)
-- Var "YY"
--
-- >>> encodeVar (-7)
-- Var "XX1"
--
-- @encodeVar@ is injective.
--
-- prop> (v == v') == (encodeVar v == encodeVar v')
--
encodeVar :: Var -> TPTP.Var
encodeVar :: Var -> Var
encodeVar Var
v = Text -> Var
TPTP.Var (Text -> Var) -> Text -> Var
forall a b. (a -> b) -> a -> b
$ [Text] -> Var -> Text
forall i a. Integral i => [a] -> i -> a
genericIndex [Text]
variables (Var -> Var
forall a. Num a => a -> a
abs Var
v)
  where
    variables :: [Text]
    variables :: [Text]
variables = (Var -> Text -> Text) -> [Var] -> [Text] -> [Text]
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Var -> Text -> Text
prime [Var
0..] [Text
"X", Text
"Y", Text
"Z", Text
"P", Text
"Q", Text
"R", Text
"T"]

    prime :: Integer -> Text -> Text
    prime :: Var -> Text -> Text
prime Var
n Text
w = Text
letter Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
index
      where
        letter :: Text
letter = if Var
v Var -> Var -> Bool
forall a. Ord a => a -> a -> Bool
>= Var
0 then Text
w else Text
w Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
w
        index :: Text
index  = if Var
n Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
0 then Text
T.empty else String -> Text
T.pack (Var -> String
forall a. Show a => a -> String
show Var
n)

type Substitutions = EnumerationT TPTP.Var Partial

-- | Encode a function symbol in TPTP.
encodeFunction :: FunctionSymbol -> TPTP.Name TPTP.Function
encodeFunction :: FunctionSymbol -> Name Function
encodeFunction (FunctionSymbol Text
s) = Atom -> Name Function
forall s. Atom -> Name s
TPTP.Defined (Text -> Atom
TPTP.Atom Text
s)

-- | Decode a function symbol from TPTP.
decodeFunction :: TPTP.Name s -> Partial FunctionSymbol
decodeFunction :: Name s -> Partial FunctionSymbol
decodeFunction = \case
  TPTP.Defined (TPTP.Atom Text
s) -> FunctionSymbol -> Partial FunctionSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> FunctionSymbol
FunctionSymbol Text
s)
  TPTP.Reserved{} -> String -> Partial FunctionSymbol
forall (m :: * -> *) a. Monad m => String -> PartialT m a
parsingError String
"reserved functions are not supported"

-- | Encode a predicate symbol in TPTP.
encodePredicate :: PredicateSymbol -> TPTP.Name TPTP.Predicate
encodePredicate :: PredicateSymbol -> Name Predicate
encodePredicate (PredicateSymbol Text
p) = Atom -> Name Predicate
forall s. Atom -> Name s
TPTP.Defined (Text -> Atom
TPTP.Atom Text
p)

-- | Encode a term in TPTP.
encodeTerm :: Term -> TPTP.Term
encodeTerm :: Term -> Term
encodeTerm = \case
  Variable Var
v    -> Var -> Term
TPTP.Variable (Var -> Var
encodeVar Var
v)
  Function FunctionSymbol
f [Term]
ts -> Name Function -> [Term] -> Term
TPTP.Function (FunctionSymbol -> Name Function
encodeFunction FunctionSymbol
f) ((Term -> Term) -> [Term] -> [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
encodeTerm [Term]
ts)

-- | Decode a term from TPTP.
decodeTermS :: TPTP.Term -> Substitutions Term
decodeTermS :: Term -> Substitutions Term
decodeTermS = \case
  TPTP.Function Name Function
f [Term]
ts  -> FunctionSymbol -> [Term] -> Term
Function (FunctionSymbol -> [Term] -> Term)
-> EnumerationT Var (PartialT Identity) FunctionSymbol
-> EnumerationT Var (PartialT Identity) ([Term] -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Partial FunctionSymbol
-> EnumerationT Var (PartialT Identity) FunctionSymbol
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Name Function -> Partial FunctionSymbol
forall s. Name s -> Partial FunctionSymbol
decodeFunction Name Function
f) EnumerationT Var (PartialT Identity) ([Term] -> Term)
-> EnumerationT Var (PartialT Identity) [Term]
-> Substitutions Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term -> Substitutions Term)
-> [Term] -> EnumerationT Var (PartialT Identity) [Term]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Term -> Substitutions Term
decodeTermS [Term]
ts
  TPTP.Variable Var
v     -> Var -> Term
Variable (Var -> Term)
-> EnumerationT Var (PartialT Identity) Var -> Substitutions Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Var -> EnumerationT Var (PartialT Identity) Var
forall a (m :: * -> *).
(Ord a, Monad m) =>
a -> EnumerationT a m Var
enumerate Var
v
  TPTP.Number{}       -> PartialT Identity Term -> Substitutions Term
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (PartialT Identity Term -> Substitutions Term)
-> PartialT Identity Term -> Substitutions Term
forall a b. (a -> b) -> a -> b
$ String -> PartialT Identity Term
forall (m :: * -> *) a. Monad m => String -> PartialT m a
parsingError String
"numbers are not supported"
  TPTP.DistinctTerm{} -> PartialT Identity Term -> Substitutions Term
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (PartialT Identity Term -> Substitutions Term)
-> PartialT Identity Term -> Substitutions Term
forall a b. (a -> b) -> a -> b
$ String -> PartialT Identity Term
forall (m :: * -> *) a. Monad m => String -> PartialT m a
parsingError String
"distinct objects are not supported"

-- | Encode a literal in TPTP.
encodeLiteral :: Literal -> TPTP.Literal
encodeLiteral :: Literal -> Literal
encodeLiteral = \case
  Predicate PredicateSymbol
p [Term]
ts  -> Name Predicate -> [Term] -> Literal
TPTP.Predicate (PredicateSymbol -> Name Predicate
encodePredicate PredicateSymbol
p) ((Term -> Term) -> [Term] -> [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
encodeTerm [Term]
ts)
  Equality Term
a Term
b    -> Term -> Sign -> Term -> Literal
TPTP.Equality (Term -> Term
encodeTerm Term
a) Sign
TPTP.Positive (Term -> Term
encodeTerm Term
b)
  Propositional Bool
b -> Name Predicate -> [Term] -> Literal
TPTP.Predicate (Reserved Predicate -> Name Predicate
forall s. Reserved s -> Name s
TPTP.Reserved (Predicate -> Reserved Predicate
forall s. s -> Reserved s
TPTP.Standard Predicate
p)) []
    where p :: Predicate
p = if Bool
b then Predicate
TPTP.Tautology else Predicate
TPTP.Falsum

-- | Decode a literal from TPTP.
decodeLiteral :: TPTP.Literal -> Substitutions (Signed Literal)
decodeLiteral :: Literal -> Substitutions (Signed Literal)
decodeLiteral = \case
  TPTP.Predicate Name Predicate
p [Term]
ts -> do
    [Term] -> Literal
p' <- PartialT Identity ([Term] -> Literal)
-> EnumerationT Var (PartialT Identity) ([Term] -> Literal)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Name Predicate -> PartialT Identity ([Term] -> Literal)
decodePredicate Name Predicate
p)
    [Term]
ts' <- (Term -> Substitutions Term)
-> [Term] -> EnumerationT Var (PartialT Identity) [Term]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Term -> Substitutions Term
decodeTermS [Term]
ts
    Signed Literal -> Substitutions (Signed Literal)
forall (m :: * -> *) a. Monad m => a -> m a
return (Signed Literal -> Substitutions (Signed Literal))
-> Signed Literal -> Substitutions (Signed Literal)
forall a b. (a -> b) -> a -> b
$ Sign -> Literal -> Signed Literal
forall e. Sign -> e -> Signed e
Signed Sign
Positive ([Term] -> Literal
p' [Term]
ts')
  TPTP.Equality Term
a Sign
s Term
b -> Sign -> Term -> Term -> Signed Literal
decodeEquality Sign
s (Term -> Term -> Signed Literal)
-> Substitutions Term
-> EnumerationT Var (PartialT Identity) (Term -> Signed Literal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Substitutions Term
decodeTermS Term
a EnumerationT Var (PartialT Identity) (Term -> Signed Literal)
-> Substitutions Term -> Substitutions (Signed Literal)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> Substitutions Term
decodeTermS Term
b

decodePredicate :: TPTP.Name TPTP.Predicate -> Partial ([Term] -> Literal)
decodePredicate :: Name Predicate -> PartialT Identity ([Term] -> Literal)
decodePredicate = \case
  TPTP.Defined  (TPTP.Atom Text
p)                  -> ([Term] -> Literal) -> PartialT Identity ([Term] -> Literal)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Term] -> Literal) -> PartialT Identity ([Term] -> Literal))
-> ([Term] -> Literal) -> PartialT Identity ([Term] -> Literal)
forall a b. (a -> b) -> a -> b
$ PredicateSymbol -> [Term] -> Literal
Predicate (Text -> PredicateSymbol
PredicateSymbol Text
p)
  TPTP.Reserved (TPTP.Standard Predicate
TPTP.Tautology) -> ([Term] -> Literal) -> PartialT Identity ([Term] -> Literal)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Term] -> Literal) -> PartialT Identity ([Term] -> Literal))
-> ([Term] -> Literal) -> PartialT Identity ([Term] -> Literal)
forall a b. (a -> b) -> a -> b
$ Literal -> [Term] -> Literal
forall a b. a -> b -> a
const (Bool -> Literal
Propositional Bool
True)
  TPTP.Reserved (TPTP.Standard Predicate
TPTP.Falsum)    -> ([Term] -> Literal) -> PartialT Identity ([Term] -> Literal)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Term] -> Literal) -> PartialT Identity ([Term] -> Literal))
-> ([Term] -> Literal) -> PartialT Identity ([Term] -> Literal)
forall a b. (a -> b) -> a -> b
$ Literal -> [Term] -> Literal
forall a b. a -> b -> a
const (Bool -> Literal
Propositional Bool
False)
  TPTP.Reserved (TPTP.Standard Predicate
p) ->
    String -> PartialT Identity ([Term] -> Literal)
forall (m :: * -> *) a. Monad m => String -> PartialT m a
parsingError (String -> PartialT Identity ([Term] -> Literal))
-> String -> PartialT Identity ([Term] -> Literal)
forall a b. (a -> b) -> a -> b
$ String
"unsupported standard reserved predicate " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Predicate -> String
forall a. Show a => a -> String
show Predicate
p
  TPTP.Reserved TPTP.Extended{} ->
    String -> PartialT Identity ([Term] -> Literal)
forall (m :: * -> *) a. Monad m => String -> PartialT m a
parsingError String
"extended reserved predicates are not supported"

decodeEquality :: TPTP.Sign -> Term -> Term -> Signed Literal
decodeEquality :: Sign -> Term -> Term -> Signed Literal
decodeEquality Sign
s Term
a Term
b = Sign -> Literal -> Signed Literal
forall e. Sign -> e -> Signed e
Signed (Sign -> Sign
decodeSign Sign
s) (Term -> Term -> Literal
Equality Term
a Term
b)

-- | Encode a logical connective in TPTP.
encodeConnective :: Connective -> TPTP.Connective
encodeConnective :: Connective -> Connective
encodeConnective = \case
  Connective
And        -> Connective
TPTP.Conjunction
  Connective
Or         -> Connective
TPTP.Disjunction
  Connective
Implies    -> Connective
TPTP.Implication
  Connective
Equivalent -> Connective
TPTP.Equivalence
  Connective
Xor        -> Connective
TPTP.ExclusiveOr

decodeConnected :: TPTP.Connective -> Formula -> Formula -> Formula
decodeConnected :: Connective -> Formula -> Formula -> Formula
decodeConnected = \case
  Connective
TPTP.Conjunction -> Connective -> Formula -> Formula -> Formula
Connected Connective
And
  Connective
TPTP.Disjunction -> Connective -> Formula -> Formula -> Formula
Connected Connective
Or
  Connective
TPTP.Implication -> Connective -> Formula -> Formula -> Formula
Connected Connective
Implies
  Connective
TPTP.Equivalence -> Connective -> Formula -> Formula -> Formula
Connected Connective
Equivalent
  Connective
TPTP.ExclusiveOr -> Connective -> Formula -> Formula -> Formula
Connected Connective
Xor
  Connective
TPTP.NegatedConjunction  -> Formula -> Formula
Negate (Formula -> Formula)
-> (Formula -> Formula -> Formula) -> Formula -> Formula -> Formula
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
.: Connective -> Formula -> Formula -> Formula
Connected Connective
And
  Connective
TPTP.NegatedDisjunction  -> Formula -> Formula
Negate (Formula -> Formula)
-> (Formula -> Formula -> Formula) -> Formula -> Formula -> Formula
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
.: Connective -> Formula -> Formula -> Formula
Connected Connective
Or
  Connective
TPTP.ReversedImplication -> (Formula -> Formula -> Formula) -> Formula -> Formula -> Formula
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Connective -> Formula -> Formula -> Formula
Connected Connective
Implies)
  where
    (.:) :: (c -> d) -> (a -> b -> c) -> a -> b -> d
    .: :: (c -> d) -> (a -> b -> c) -> a -> b -> d
(.:) = ((b -> c) -> b -> d) -> (a -> b -> c) -> a -> b -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) (((b -> c) -> b -> d) -> (a -> b -> c) -> a -> b -> d)
-> ((c -> d) -> (b -> c) -> b -> d)
-> (c -> d)
-> (a -> b -> c)
-> a
-> b
-> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (c -> d) -> (b -> c) -> b -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)

-- | Encode a quantifier in TPTP.
encodeQuantifier :: Quantifier -> TPTP.Quantifier
encodeQuantifier :: Quantifier -> Quantifier
encodeQuantifier = \case
  Quantifier
Forall -> Quantifier
TPTP.Forall
  Quantifier
Exists -> Quantifier
TPTP.Exists

-- | Decode a quantifier from TPTP.
decodeQuantifier :: TPTP.Quantifier -> Quantifier
decodeQuantifier :: Quantifier -> Quantifier
decodeQuantifier = \case
  Quantifier
TPTP.Forall -> Quantifier
Forall
  Quantifier
TPTP.Exists -> Quantifier
Exists

-- | Encode a formula in unsorted first-order logic in TPTP.
encodeFormula :: Formula -> TPTP.UnsortedFirstOrder
encodeFormula :: Formula -> UnsortedFirstOrder
encodeFormula = \case
  Atomic Literal
l         -> Literal -> UnsortedFirstOrder
forall s. Literal -> FirstOrder s
TPTP.Atomic (Literal -> Literal
encodeLiteral Literal
l)
  Negate Formula
f         -> UnsortedFirstOrder -> UnsortedFirstOrder
forall s. FirstOrder s -> FirstOrder s
TPTP.Negated (Formula -> UnsortedFirstOrder
encodeFormula Formula
f)
  Connected  Connective
c Formula
f Formula
g -> UnsortedFirstOrder
-> Connective -> UnsortedFirstOrder -> UnsortedFirstOrder
forall s.
FirstOrder s -> Connective -> FirstOrder s -> FirstOrder s
TPTP.Connected (Formula -> UnsortedFirstOrder
encodeFormula Formula
f) (Connective -> Connective
encodeConnective Connective
c) (Formula -> UnsortedFirstOrder
encodeFormula Formula
g)
  Quantified Quantifier
q Var
v Formula
f -> Quantifier
-> [(Var, Unsorted)] -> UnsortedFirstOrder -> UnsortedFirstOrder
forall s. Quantifier -> [(Var, s)] -> FirstOrder s -> FirstOrder s
TPTP.quantified (Quantifier -> Quantifier
encodeQuantifier Quantifier
q) [(Var -> Var
encodeVar Var
v, () -> Unsorted
TPTP.Unsorted ())] (Formula -> UnsortedFirstOrder
encodeFormula Formula
f)

-- | Decode a formula in unsorted first-order logic from TPTP.
decodeFormula :: TPTP.UnsortedFirstOrder -> Partial Formula
decodeFormula :: UnsortedFirstOrder -> Partial Formula
decodeFormula = EnumerationT Var (PartialT Identity) Formula -> Partial Formula
forall (m :: * -> *) a e. Monad m => EnumerationT a m e -> m e
evalEnumerationT (EnumerationT Var (PartialT Identity) Formula -> Partial Formula)
-> (UnsortedFirstOrder
    -> EnumerationT Var (PartialT Identity) Formula)
-> UnsortedFirstOrder
-> Partial Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnsortedFirstOrder -> EnumerationT Var (PartialT Identity) Formula
decodeFormulaS

decodeFormulaS :: TPTP.UnsortedFirstOrder -> Substitutions Formula
decodeFormulaS :: UnsortedFirstOrder -> EnumerationT Var (PartialT Identity) Formula
decodeFormulaS = \case
  TPTP.Atomic Literal
l          -> Signed Literal -> Formula
liftSignedLiteral (Signed Literal -> Formula)
-> Substitutions (Signed Literal)
-> EnumerationT Var (PartialT Identity) Formula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Literal -> Substitutions (Signed Literal)
decodeLiteral Literal
l
  TPTP.Negated UnsortedFirstOrder
f         -> Formula -> Formula
Negate (Formula -> Formula)
-> EnumerationT Var (PartialT Identity) Formula
-> EnumerationT Var (PartialT Identity) Formula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnsortedFirstOrder -> EnumerationT Var (PartialT Identity) Formula
decodeFormulaS UnsortedFirstOrder
f
  TPTP.Connected UnsortedFirstOrder
f Connective
c UnsortedFirstOrder
g   -> Connective -> Formula -> Formula -> Formula
decodeConnected Connective
c
                        (Formula -> Formula -> Formula)
-> EnumerationT Var (PartialT Identity) Formula
-> EnumerationT Var (PartialT Identity) (Formula -> Formula)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnsortedFirstOrder -> EnumerationT Var (PartialT Identity) Formula
decodeFormulaS UnsortedFirstOrder
f EnumerationT Var (PartialT Identity) (Formula -> Formula)
-> EnumerationT Var (PartialT Identity) Formula
-> EnumerationT Var (PartialT Identity) Formula
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UnsortedFirstOrder -> EnumerationT Var (PartialT Identity) Formula
decodeFormulaS UnsortedFirstOrder
g
  TPTP.Quantified Quantifier
q NonEmpty (Var, Unsorted)
vs UnsortedFirstOrder
f -> (Var -> Formula -> Formula) -> Formula -> NonEmpty Var -> Formula
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (((Var, Formula) -> Formula) -> Var -> Formula -> Formula
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((Var, Formula) -> Formula) -> Var -> Formula -> Formula)
-> ((Var, Formula) -> Formula) -> Var -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ Quantifier -> (Var, Formula) -> Formula
forall b. Binder b => Quantifier -> b -> Formula
quantified (Quantifier -> Quantifier
decodeQuantifier Quantifier
q))
                        (Formula -> NonEmpty Var -> Formula)
-> EnumerationT Var (PartialT Identity) Formula
-> EnumerationT Var (PartialT Identity) (NonEmpty Var -> Formula)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnsortedFirstOrder -> EnumerationT Var (PartialT Identity) Formula
decodeFormulaS UnsortedFirstOrder
f EnumerationT Var (PartialT Identity) (NonEmpty Var -> Formula)
-> EnumerationT Var (PartialT Identity) (NonEmpty Var)
-> EnumerationT Var (PartialT Identity) Formula
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((Var, Unsorted) -> EnumerationT Var (PartialT Identity) Var)
-> NonEmpty (Var, Unsorted)
-> EnumerationT Var (PartialT Identity) (NonEmpty Var)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Var -> EnumerationT Var (PartialT Identity) Var
forall a (m :: * -> *).
(Ord a, Monad m) =>
a -> EnumerationT a m Var
enumerate (Var -> EnumerationT Var (PartialT Identity) Var)
-> ((Var, Unsorted) -> Var)
-> (Var, Unsorted)
-> EnumerationT Var (PartialT Identity) Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, Unsorted) -> Var
forall a b. (a, b) -> a
fst) NonEmpty (Var, Unsorted)
vs

-- | Encode a formula in unsorted first-order logic in TPTP.
encode :: LogicalExpression -> TPTP.Formula
encode :: LogicalExpression -> Formula
encode = \case
  Clause  Clause
c -> Clause -> Formula
TPTP.CNF (Clause -> Clause
encodeClause  Clause
c)
  Formula Formula
f -> UnsortedFirstOrder -> Formula
TPTP.FOF (Formula -> UnsortedFirstOrder
encodeFormula Formula
f)

-- | Decode a formula in unsorted first-order logic from TPTP.
decode :: TPTP.Formula -> Partial LogicalExpression
decode :: Formula -> Partial LogicalExpression
decode = \case
  TPTP.FOF UnsortedFirstOrder
f  -> Formula -> LogicalExpression
Formula (Formula -> LogicalExpression)
-> Partial Formula -> Partial LogicalExpression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnsortedFirstOrder -> Partial Formula
decodeFormula UnsortedFirstOrder
f
  TPTP.CNF Clause
c  -> Clause -> LogicalExpression
Clause  (Clause -> LogicalExpression)
-> PartialT Identity Clause -> Partial LogicalExpression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Clause -> PartialT Identity Clause
decodeClause  Clause
c
  TPTP.TFF0 MonomorphicFirstOrder
f | Just UnsortedFirstOrder
g <- MonomorphicFirstOrder -> Maybe UnsortedFirstOrder
TPTP.unsortFirstOrder MonomorphicFirstOrder
f -> Formula -> LogicalExpression
Formula (Formula -> LogicalExpression)
-> Partial Formula -> Partial LogicalExpression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnsortedFirstOrder -> Partial Formula
decodeFormula UnsortedFirstOrder
g
  TPTP.TFF0{} -> String -> Partial LogicalExpression
forall (m :: * -> *) a. Monad m => String -> PartialT m a
parsingError String
"formulas in TFF0 are not supported"
  TPTP.TFF1{} -> String -> Partial LogicalExpression
forall (m :: * -> *) a. Monad m => String -> PartialT m a
parsingError String
"formulas in TFF1 are not supported"

-- | Encode a clause in unsorted first-order logic in TPTP.
encodeClause :: Clause -> TPTP.Clause
encodeClause :: Clause -> Clause
encodeClause = [(Sign, Literal)] -> Clause
TPTP.clause ([(Sign, Literal)] -> Clause)
-> (Clause -> [(Sign, Literal)]) -> Clause -> Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Signed Literal -> (Sign, Literal))
-> [Signed Literal] -> [(Sign, Literal)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Signed Literal -> (Sign, Literal)
encodeSignedLiteral ([Signed Literal] -> [(Sign, Literal)])
-> (Clause -> [Signed Literal]) -> Clause -> [(Sign, Literal)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> [Signed Literal]
getLiterals

-- | Decode a clause in unsorted first-order logic from TPTP.
decodeClause :: TPTP.Clause -> Partial Clause
decodeClause :: Clause -> PartialT Identity Clause
decodeClause = EnumerationT Var (PartialT Identity) Clause
-> PartialT Identity Clause
forall (m :: * -> *) a e. Monad m => EnumerationT a m e -> m e
evalEnumerationT (EnumerationT Var (PartialT Identity) Clause
 -> PartialT Identity Clause)
-> (Clause -> EnumerationT Var (PartialT Identity) Clause)
-> Clause
-> PartialT Identity Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> EnumerationT Var (PartialT Identity) Clause
decodeClauseS

decodeClauseS :: TPTP.Clause -> Substitutions Clause
decodeClauseS :: Clause -> EnumerationT Var (PartialT Identity) Clause
decodeClauseS (TPTP.Clause NonEmpty (Sign, Literal)
ls) = [Signed Literal] -> Clause
Literals ([Signed Literal] -> Clause)
-> EnumerationT Var (PartialT Identity) [Signed Literal]
-> EnumerationT Var (PartialT Identity) Clause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Sign, Literal) -> Substitutions (Signed Literal))
-> [(Sign, Literal)]
-> EnumerationT Var (PartialT Identity) [Signed Literal]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Sign, Literal) -> Substitutions (Signed Literal)
decodeSignedLiteralS (NonEmpty (Sign, Literal) -> [(Sign, Literal)]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty (Sign, Literal)
ls)

encodeSign :: Sign -> TPTP.Sign
encodeSign :: Sign -> Sign
encodeSign = \case
  Sign
Positive -> Sign
TPTP.Positive
  Sign
Negative -> Sign
TPTP.Negative

decodeSign :: TPTP.Sign -> Sign
decodeSign :: Sign -> Sign
decodeSign = \case
  Sign
TPTP.Positive -> Sign
Positive
  Sign
TPTP.Negative -> Sign
Negative

encodeSignedLiteral :: Signed Literal -> (TPTP.Sign, TPTP.Literal)
encodeSignedLiteral :: Signed Literal -> (Sign, Literal)
encodeSignedLiteral (Signed Sign
s Literal
l) = (Sign -> Sign
encodeSign Sign
s, Literal -> Literal
encodeLiteral Literal
l)

decodeSignedLiteralS :: (TPTP.Sign, TPTP.Literal) -> Substitutions (Signed Literal)
decodeSignedLiteralS :: (Sign, Literal) -> Substitutions (Signed Literal)
decodeSignedLiteralS (Sign
s, Literal
l) = Sign -> Signed Literal -> Signed Literal
forall e. Sign -> Signed e -> Signed e
sign (Sign -> Sign
decodeSign Sign
s) (Signed Literal -> Signed Literal)
-> Substitutions (Signed Literal) -> Substitutions (Signed Literal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Literal -> Substitutions (Signed Literal)
decodeLiteral Literal
l

-- | Encode a set of first-order clauses in TPTP.
encodeClauses :: Clauses -> TPTP.TPTP
encodeClauses :: Clauses -> TPTP
encodeClauses (Clauses [Clause]
cs) = [Unit] -> TPTP
TPTP.TPTP [Unit]
units
  where
    units :: [Unit]
units = (Var -> Clause -> Unit) -> [Var] -> [Clause] -> [Unit]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Var -> Clause -> Unit
unit [Var
1..] [Clause]
cs
    unit :: Var -> Clause -> Unit
unit Var
n Clause
f = UnitName -> Declaration -> Maybe Annotation -> Unit
TPTP.Unit (Var -> UnitName
forall a b. b -> Either a b
Right Var
n) (Clause -> Declaration
clauze Clause
f) Maybe Annotation
forall a. Maybe a
Nothing
    clauze :: Clause -> Declaration
clauze = Reserved Role -> Formula -> Declaration
TPTP.Formula (Role -> Reserved Role
forall s. s -> Reserved s
TPTP.Standard Role
TPTP.Axiom) (Formula -> Declaration)
-> (Clause -> Formula) -> Clause -> Declaration
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LogicalExpression -> Formula
encode (LogicalExpression -> Formula)
-> (Clause -> LogicalExpression) -> Clause -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> LogicalExpression
Clause

-- | Encode a theorem in unsorted first-order logic in TPTP.
encodeTheorem :: Theorem -> TPTP.TPTP
encodeTheorem :: Theorem -> TPTP
encodeTheorem (Theorem [Formula]
as Formula
c) = [Unit] -> TPTP
TPTP.TPTP [Unit]
units
  where
    units :: [Unit]
units = Role -> Var -> Formula -> Unit
unit Role
TPTP.Conjecture Var
0 Formula
c Unit -> [Unit] -> [Unit]
forall a. a -> [a] -> [a]
: (Var -> Formula -> Unit) -> [Var] -> [Formula] -> [Unit]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Role -> Var -> Formula -> Unit
unit Role
TPTP.Axiom) [Var
1..] [Formula]
as
    unit :: Role -> Var -> Formula -> Unit
unit Role
r Var
n Formula
f = UnitName -> Declaration -> Maybe Annotation -> Unit
TPTP.Unit (Var -> UnitName
forall a b. b -> Either a b
Right Var
n) (Role -> Formula -> Declaration
formula Role
r Formula
f) Maybe Annotation
forall a. Maybe a
Nothing
    formula :: Role -> Formula -> Declaration
formula Role
r = Reserved Role -> Formula -> Declaration
TPTP.Formula (Role -> Reserved Role
forall s. s -> Reserved s
TPTP.Standard Role
r) (Formula -> Declaration)
-> (Formula -> Formula) -> Formula -> Declaration
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LogicalExpression -> Formula
encode (LogicalExpression -> Formula)
-> (Formula -> LogicalExpression) -> Formula -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula -> LogicalExpression
Formula (Formula -> LogicalExpression)
-> (Formula -> Formula) -> Formula -> LogicalExpression
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula -> Formula
close

-- | Decode a solution from a TSTP output.
decodeSolution :: TPTP.TSTP -> Partial Solution
decodeSolution :: TSTP -> Partial Solution
decodeSolution (TPTP.TSTP SZS
szs [Unit]
units)
  | TPTP.SZS (Just (Right Success
status)) Maybe Dataform
_dataform <- SZS
szs = if
    | Success -> Bool
isProof Success
status -> Refutation Var -> Solution
Proof (Refutation Var -> Solution)
-> PartialT Identity (Refutation Var) -> Partial Solution
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Unit] -> PartialT Identity (Refutation Var)
decodeRefutation [Unit]
units
    | Success -> Bool
isSaturation Success
status -> Derivation Var -> Solution
Saturation (Derivation Var -> Solution)
-> PartialT Identity (Derivation Var) -> Partial Solution
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Unit] -> PartialT Identity (Derivation Var)
decodeDerivation [Unit]
units
    | Bool
otherwise -> String -> Partial Solution
forall (m :: * -> *) a. Monad m => String -> PartialT m a
parsingError (String -> Partial Solution) -> String -> Partial Solution
forall a b. (a -> b) -> a -> b
$ String
"unsupported SZS " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Success -> String
forall a. Show a => a -> String
show Success
status
  | Bool
otherwise = String -> Partial Solution
forall (m :: * -> *) a. Monad m => String -> PartialT m a
proofError String
"malformed input: missing SZS ontologies"

isProof :: TPTP.Success -> Bool
isProof :: Success -> Bool
isProof = \case
  Success
TPTP.UNS -> Bool
True
  Success
TPTP.THM -> Bool
True
  Success
_ -> Bool
False

isSaturation :: TPTP.Success -> Bool
isSaturation :: Success -> Bool
isSaturation = \case
  Success
TPTP.SAT -> Bool
True
  Success
TPTP.CSA -> Bool
True
  Success
_ -> Bool
False

decodeRefutation :: [TPTP.Unit] -> Partial (Refutation Integer)
decodeRefutation :: [Unit] -> PartialT Identity (Refutation Var)
decodeRefutation [Unit]
units = do
  Derivation Var
derivation <- [Unit] -> PartialT Identity (Derivation Var)
decodeDerivation [Unit]
units
  case Derivation Var -> Maybe (Refutation Var)
forall f. Derivation f -> Maybe (Refutation f)
unliftRefutation Derivation Var
derivation of
    Just Refutation Var
refutation -> Refutation Var -> PartialT Identity (Refutation Var)
forall (m :: * -> *) a. Monad m => a -> m a
return Refutation Var
refutation
    Maybe (Refutation Var)
Nothing -> String -> PartialT Identity (Refutation Var)
forall (m :: * -> *) a. Monad m => String -> PartialT m a
proofError String
"malformed input: refutation not found"

decodeDerivation :: [TPTP.Unit] -> Partial (Derivation Integer)
decodeDerivation :: [Unit] -> PartialT Identity (Derivation Var)
decodeDerivation [Unit]
units = do
  [Sequent UnitName]
decodedSequents <- (Unit -> PartialT Identity (Sequent UnitName))
-> [Unit] -> PartialT Identity [Sequent UnitName]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Unit -> PartialT Identity (Sequent UnitName)
decodeSequent [Unit]
units
  let expressions :: Map UnitName LogicalExpression
expressions = [Sequent UnitName] -> Map UnitName LogicalExpression
forall f. Ord f => [Sequent f] -> Map f LogicalExpression
labeling [Sequent UnitName]
decodedSequents
  Derivation Var -> PartialT Identity (Derivation Var)
forall (m :: * -> *) a. Monad m => a -> m a
return (Derivation Var -> PartialT Identity (Derivation Var))
-> ([Sequent UnitName] -> Derivation Var)
-> [Sequent UnitName]
-> PartialT Identity (Derivation Var)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Enumeration UnitName (Derivation Var) -> Derivation Var
forall a e. Enumeration a e -> e
evalEnumeration
         (Enumeration UnitName (Derivation Var) -> Derivation Var)
-> ([Sequent UnitName] -> Enumeration UnitName (Derivation Var))
-> [Sequent UnitName]
-> Derivation Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Derivation Var
 -> Sequent UnitName -> Enumeration UnitName (Derivation Var))
-> Derivation Var
-> [Sequent UnitName]
-> Enumeration UnitName (Derivation Var)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Map UnitName LogicalExpression
-> Derivation Var
-> Sequent UnitName
-> Enumeration UnitName (Derivation Var)
forall n.
Ord n =>
Map n LogicalExpression
-> Derivation Var -> Sequent n -> Enumeration n (Derivation Var)
decodeSequentS Map UnitName LogicalExpression
expressions) Derivation Var
forall a. Monoid a => a
mempty
         ([Sequent UnitName] -> PartialT Identity (Derivation Var))
-> [Sequent UnitName] -> PartialT Identity (Derivation Var)
forall a b. (a -> b) -> a -> b
$ [Sequent UnitName]
decodedSequents

decodeSequentS :: Ord n => Map n LogicalExpression -> Derivation Integer ->
                           Sequent n -> Enumeration n (Derivation Integer)
decodeSequentS :: Map n LogicalExpression
-> Derivation Var -> Sequent n -> Enumeration n (Derivation Var)
decodeSequentS Map n LogicalExpression
es Derivation Var
d s :: Sequent n
s@(Sequent n
l Inference n
i) =
  case (n -> Bool) -> [n] -> Maybe n
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find n -> Bool
synonymous (Inference n -> [n]
forall f. Inference f -> [f]
antecedents Inference n
i) of
    Just n
a  -> n -> n -> EnumerationT n Identity ()
forall a (m :: * -> *).
(Ord a, Monad m) =>
a -> a -> EnumerationT a m ()
alias n
l n
a EnumerationT n Identity ()
-> Derivation Var -> Enumeration n (Derivation Var)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Derivation Var
d
    Maybe n
Nothing -> Derivation Var -> Sequent Var -> Derivation Var
forall f. Ord f => Derivation f -> Sequent f -> Derivation f
addSequent Derivation Var
d (Sequent Var -> Derivation Var)
-> EnumerationT n Identity (Sequent Var)
-> Enumeration n (Derivation Var)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (n -> EnumerationT n Identity Var)
-> Sequent n -> EnumerationT n Identity (Sequent Var)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse n -> EnumerationT n Identity Var
forall a (m :: * -> *).
(Ord a, Monad m) =>
a -> EnumerationT a m Var
enumerate Sequent n
s
  where synonymous :: n -> Bool
synonymous n
a = Map n LogicalExpression
es Map n LogicalExpression -> n -> LogicalExpression
forall k a. Ord k => Map k a -> k -> a
! n
a LogicalExpression -> LogicalExpression -> Bool
forall e. FirstOrder e => e -> e -> Bool
~= Inference n -> LogicalExpression
forall f. Inference f -> LogicalExpression
consequent Inference n
i

decodeSequent :: TPTP.Unit -> Partial (Sequent TPTP.UnitName)
decodeSequent :: Unit -> PartialT Identity (Sequent UnitName)
decodeSequent = \case
  TPTP.Unit UnitName
name (TPTP.Formula (TPTP.Standard Role
TPTP.Axiom) Formula
formula) Maybe Annotation
Nothing -> do
    LogicalExpression
expression <- Formula -> Partial LogicalExpression
decode Formula
formula
    Sequent UnitName -> PartialT Identity (Sequent UnitName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sequent UnitName -> PartialT Identity (Sequent UnitName))
-> Sequent UnitName -> PartialT Identity (Sequent UnitName)
forall a b. (a -> b) -> a -> b
$ UnitName -> Inference UnitName -> Sequent UnitName
forall f. f -> Inference f -> Sequent f
Sequent UnitName
name (Rule UnitName -> LogicalExpression -> Inference UnitName
forall f. Rule f -> LogicalExpression -> Inference f
Inference Rule UnitName
forall f. Rule f
Axiom LogicalExpression
expression)
  TPTP.Unit UnitName
name (TPTP.Formula Reserved Role
role Formula
formula) (Just (Source
source, Maybe [Info]
_)) -> do
    Rule UnitName
rule <- Source -> Reserved Role -> [UnitName] -> Partial (Rule UnitName)
forall f. Source -> Reserved Role -> [f] -> Partial (Rule f)
decodeRule Source
source Reserved Role
role (Source -> [UnitName]
collectParents Source
source)
    LogicalExpression
expression <- Formula -> Partial LogicalExpression
decode Formula
formula
    Sequent UnitName -> PartialT Identity (Sequent UnitName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sequent UnitName -> PartialT Identity (Sequent UnitName))
-> Sequent UnitName -> PartialT Identity (Sequent UnitName)
forall a b. (a -> b) -> a -> b
$ UnitName -> Inference UnitName -> Sequent UnitName
forall f. f -> Inference f -> Sequent f
Sequent UnitName
name (Rule UnitName -> LogicalExpression -> Inference UnitName
forall f. Rule f -> LogicalExpression -> Inference f
Inference Rule UnitName
rule LogicalExpression
expression)
  Unit
_ -> String -> PartialT Identity (Sequent UnitName)
forall (m :: * -> *) a. Monad m => String -> PartialT m a
proofError String
"malformed input: unexpected unit"

collectParents :: TPTP.Source -> [TPTP.UnitName]
collectParents :: Source -> [UnitName]
collectParents = \case
  TPTP.File{}           -> []
  TPTP.Theory{}         -> []
  TPTP.Creator{}        -> []
  TPTP.Introduced{}     -> []
  TPTP.Inference Atom
_ [Info]
_ [Parent]
ps -> (Parent -> [UnitName]) -> [Parent] -> [UnitName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(TPTP.Parent Source
p [Info]
_) -> Source -> [UnitName]
collectParents Source
p) [Parent]
ps
  TPTP.UnitSource UnitName
p     -> [UnitName
p]
  Source
TPTP.UnknownSource    -> []

decodeRule :: TPTP.Source -> TPTP.Reserved TPTP.Role -> [f] -> Partial (Rule f)
decodeRule :: Source -> Reserved Role -> [f] -> Partial (Rule f)
decodeRule Source
s Reserved Role
role [f]
as = case Source
s of
  TPTP.Theory{}           -> String -> Partial (Rule f)
forall (m :: * -> *) a. Monad m => String -> PartialT m a
parsingError (String -> Partial (Rule f)) -> String -> Partial (Rule f)
forall a b. (a -> b) -> a -> b
$ String
"unsupported unit source " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Source -> String
forall a. Show a => a -> String
show Source
s
  TPTP.Creator{}          -> String -> Partial (Rule f)
forall (m :: * -> *) a. Monad m => String -> PartialT m a
parsingError (String -> Partial (Rule f)) -> String -> Partial (Rule f)
forall a b. (a -> b) -> a -> b
$ String
"unsupported unit source " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Source -> String
forall a. Show a => a -> String
show Source
s
  TPTP.UnitSource{}       -> Rule f -> Partial (Rule f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Rule f -> Partial (Rule f)) -> Rule f -> Partial (Rule f)
forall a b. (a -> b) -> a -> b
$ RuleName -> [f] -> Rule f
forall f. RuleName -> [f] -> Rule f
Other RuleName
"triviality" [f]
as
  TPTP.Introduced Reserved Intro
taut Maybe [Info]
_  -> Rule f -> Partial (Rule f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Rule f -> Partial (Rule f)) -> Rule f -> Partial (Rule f)
forall a b. (a -> b) -> a -> b
$ Reserved Intro -> Rule f
forall f. Reserved Intro -> Rule f
decodeTautologyRule Reserved Intro
taut
  Source
TPTP.UnknownSource      -> Rule f -> Partial (Rule f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Rule f -> Partial (Rule f)) -> Rule f -> Partial (Rule f)
forall a b. (a -> b) -> a -> b
$ [f] -> Rule f
forall f. [f] -> Rule f
Unknown [f]
as
  TPTP.File{}             -> Reserved Role -> [f] -> Partial (Rule f)
forall a f. Reserved Role -> [a] -> Partial (Rule f)
decodeIntroductionRule Reserved Role
role [f]
as
  TPTP.Inference Atom
rule [Info]
_ [Parent]
_ -> Rule f -> Partial (Rule f)
forall (m :: * -> *) a. Monad m => a -> m a
return (Rule f -> Partial (Rule f)) -> Rule f -> Partial (Rule f)
forall a b. (a -> b) -> a -> b
$ Atom -> [f] -> Rule f
forall f. Atom -> [f] -> Rule f
decodeInferenceRule Atom
rule [f]
as

decodeTautologyRule :: TPTP.Reserved TPTP.Intro -> Rule f
decodeTautologyRule :: Reserved Intro -> Rule f
decodeTautologyRule = \case
  TPTP.Standard Intro
TPTP.ByAxiomOfChoice -> Rule f
forall f. Rule f
AxiomOfChoice
  TPTP.Extended Text
"choice_axiom" -> Rule f
forall f. Rule f
AxiomOfChoice
  Reserved Intro
_ -> Rule f
forall f. Rule f
Axiom

decodeIntroductionRule :: TPTP.Reserved TPTP.Role -> [a] -> Partial (Rule f)
decodeIntroductionRule :: Reserved Role -> [a] -> Partial (Rule f)
decodeIntroductionRule Reserved Role
role [a]
as = case (Reserved Role
role, [a]
as) of
  (TPTP.Standard Role
TPTP.Axiom,      []) -> Rule f -> Partial (Rule f)
forall (m :: * -> *) a. Monad m => a -> m a
return Rule f
forall f. Rule f
Axiom
  (TPTP.Standard Role
TPTP.Conjecture, []) -> Rule f -> Partial (Rule f)
forall (m :: * -> *) a. Monad m => a -> m a
return Rule f
forall f. Rule f
Conjecture
  (Reserved Role, [a])
_ -> String -> Partial (Rule f)
forall (m :: * -> *) a. Monad m => String -> PartialT m a
proofError (String -> Partial (Rule f)) -> String -> Partial (Rule f)
forall a b. (a -> b) -> a -> b
$ String
"unexpected unit role " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Reserved Role -> String
forall a. Show a => a -> String
show Reserved Role
role

decodeInferenceRule :: TPTP.Atom -> [f] -> Rule f
decodeInferenceRule :: Atom -> [f] -> Rule f
decodeInferenceRule (TPTP.Atom Text
rule) [f]
as = case (Text
rule, [f]
as) of
  (Text
"negated_conjecture",         [f
f]) -> f -> Rule f
forall f. f -> Rule f
NegatedConjecture       f
f
  (Text
"assume_negation",            [f
f]) -> f -> Rule f
forall f. f -> Rule f
NegatedConjecture       f
f
  (Text
"flattening",                 [f
f]) -> f -> Rule f
forall f. f -> Rule f
Flattening              f
f
  (Text
"skolemisation",              [f
f]) -> f -> Rule f
forall f. f -> Rule f
Skolemisation           f
f
  (Text
"skolemize",                  [f
f]) -> f -> Rule f
forall f. f -> Rule f
Skolemisation           f
f
  (Text
"ennf_transformation",        [f
f]) -> f -> Rule f
forall f. f -> Rule f
EnnfTransformation      f
f
  (Text
"nnf_transformation",         [f
f]) -> f -> Rule f
forall f. f -> Rule f
NnfTransformation       f
f
  (Text
"cnf_transformation",         [f
f]) -> f -> Rule f
forall f. f -> Rule f
Clausification          f
f
  (Text
"trivial_inequality_removal", [f
f]) -> f -> Rule f
forall f. f -> Rule f
TrivialInequality       f
f
  (Text
"superposition",           [f
f, f
g]) -> f -> f -> Rule f
forall f. f -> f -> Rule f
Superposition         f
f f
g
  (Text
"resolution",              [f
f, f
g]) -> f -> f -> Rule f
forall f. f -> f -> Rule f
Resolution            f
f f
g
  (Text
"pm",                      [f
f, f
g]) -> f -> f -> Rule f
forall f. f -> f -> Rule f
Paramodulation        f
f f
g
  (Text
"subsumption_resolution",  [f
f, f
g]) -> f -> f -> Rule f
forall f. f -> f -> Rule f
SubsumptionResolution f
f f
g
  (Text
"forward_demodulation",    [f
f, f
g]) -> f -> f -> Rule f
forall f. f -> f -> Rule f
ForwardDemodulation   f
f f
g
  (Text
"backward_demodulation",   [f
f, f
g]) -> f -> f -> Rule f
forall f. f -> f -> Rule f
BackwardDemodulation  f
f f
g
  (Text, [f])
_ -> RuleName -> [f] -> Rule f
forall f. RuleName -> [f] -> Rule f
Other (Text -> RuleName
RuleName Text
rule) [f]
as