{-# LANGUAGE CPP #-}
#if __GLASGOW_HASKELL__ == 708
{-# LANGUAGE DeriveFunctor, DeriveFoldable #-}
#endif
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE LambdaCase #-}

-- |
-- Module       : Data.TPTP
-- Description  : Data type definitions for the syntax of the TPTP language.
-- Copyright    : (c) Evgenii Kotelnikov, 2019-2021
-- License      : GPL-3
-- Maintainer   : evgeny.kotelnikov@gmail.com
-- Stability    : experimental
--
-- The syntax of the TPTP language.
-- See [the BNF grammar](http://tptp.cs.miami.edu/TPTP/SyntaxBNF.html)
-- definition of TPTP for details.
--

module Data.TPTP (
  -- * Languages
  Language(..),

  -- * Names
  Atom(..),
  isValidAtom,

  Var(..),
  isValidVar,

  DistinctObject(..),
  isValidDistinctObject,

  Reserved(..),
  extended,
  isValidReserved,

  Named(..),

  Function(..),
  Predicate(..),

  Name(..),

  -- * Sorts and types
  Sort(..),
  TFF1Sort(..),
  monomorphizeTFF1Sort,
  Type(..),
  tff1Type,

  -- * First-order logic
  Number(..),
  Term(..),
  Literal(..),
  Sign(..),
  Clause(..),
  unitClause,
  clause,
  Quantifier(..),
  Connective(..),
  isAssociative,
  FirstOrder(..),
  quantified,
  Unsorted(..),
  Sorted(..),
  QuantifiedSort(..),
  UnsortedFirstOrder,
  SortedFirstOrder,
  MonomorphicFirstOrder,
  sortFirstOrder,
  unsortFirstOrder,
  PolymorphicFirstOrder,
  polymorphizeFirstOrder,
  monomorphizeFirstOrder,

  -- * Units
  Formula(..),
  formulaLanguage,
  Role(..),
  Declaration(..),
  declarationLanguage,
  UnitName,
  Unit(..),
  TPTP(..),
  TSTP(..),

  -- * Annotations
  Intro(..),
  Source(..),
  Status,
  SZS(..),
  SZSOntology(..),
  Success(..),
  NoSuccess(..),
  Dataform(..),
  Parent(..),
  Expression(..),
  Info(..),
  Annotation
) where

import Data.Char (isAscii, isAsciiLower, isAsciiUpper, isDigit, isPrint)
import Data.List (find)
import Data.List.NonEmpty (NonEmpty(..), nonEmpty)
import Data.Scientific (Scientific)
import Data.String (IsString, fromString)
import qualified Data.Text as Text (all, null, head, tail)
import Data.Text (Text)

#if !MIN_VERSION_base(4, 8, 0)
import Data.Monoid (Monoid(..))
import Data.Foldable (Foldable)
import Data.Traversable (Traversable, traverse)
#endif

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

-- $setup
-- >>> :set -XOverloadedStrings
-- >>> :load Data.TPTP.Pretty
-- >>> import Test.QuickCheck


-- * Languages

-- | The language of logical formulas available in TPTP.
-- 
-- The languages of TPTP form a hierarchy displayed on the following diagram,
-- where arrows indicate inclusion. E.g. each formula in FOF is syntactically a
-- formula in TFF0, but not the other way around.
--
-- > CNF --> FOF --> TFF0 --> TFF1
--
data Language
  = CNF_ -- ^ __CNF__ - the language of clausal normal forms of
         -- unsorted first-order logic.
  | FOF_ -- ^ __FOF__ - the language of full unsorted first-order logic.
  | TFF_ -- ^ __TFF__ - the language of full sorted first-order logic,
         -- both monomorphic (__TFF0__) and polymorphic (__TFF1__).
  deriving (Language -> Language -> Bool
(Language -> Language -> Bool)
-> (Language -> Language -> Bool) -> Eq Language
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Language -> Language -> Bool
$c/= :: Language -> Language -> Bool
== :: Language -> Language -> Bool
$c== :: Language -> Language -> Bool
Eq, Int -> Language -> ShowS
[Language] -> ShowS
Language -> String
(Int -> Language -> ShowS)
-> (Language -> String) -> ([Language] -> ShowS) -> Show Language
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Language] -> ShowS
$cshowList :: [Language] -> ShowS
show :: Language -> String
$cshow :: Language -> String
showsPrec :: Int -> Language -> ShowS
$cshowsPrec :: Int -> Language -> ShowS
Show, Eq Language
Eq Language
-> (Language -> Language -> Ordering)
-> (Language -> Language -> Bool)
-> (Language -> Language -> Bool)
-> (Language -> Language -> Bool)
-> (Language -> Language -> Bool)
-> (Language -> Language -> Language)
-> (Language -> Language -> Language)
-> Ord Language
Language -> Language -> Bool
Language -> Language -> Ordering
Language -> Language -> Language
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 :: Language -> Language -> Language
$cmin :: Language -> Language -> Language
max :: Language -> Language -> Language
$cmax :: Language -> Language -> Language
>= :: Language -> Language -> Bool
$c>= :: Language -> Language -> Bool
> :: Language -> Language -> Bool
$c> :: Language -> Language -> Bool
<= :: Language -> Language -> Bool
$c<= :: Language -> Language -> Bool
< :: Language -> Language -> Bool
$c< :: Language -> Language -> Bool
compare :: Language -> Language -> Ordering
$ccompare :: Language -> Language -> Ordering
$cp1Ord :: Eq Language
Ord, Int -> Language
Language -> Int
Language -> [Language]
Language -> Language
Language -> Language -> [Language]
Language -> Language -> Language -> [Language]
(Language -> Language)
-> (Language -> Language)
-> (Int -> Language)
-> (Language -> Int)
-> (Language -> [Language])
-> (Language -> Language -> [Language])
-> (Language -> Language -> [Language])
-> (Language -> Language -> Language -> [Language])
-> Enum Language
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 :: Language -> Language -> Language -> [Language]
$cenumFromThenTo :: Language -> Language -> Language -> [Language]
enumFromTo :: Language -> Language -> [Language]
$cenumFromTo :: Language -> Language -> [Language]
enumFromThen :: Language -> Language -> [Language]
$cenumFromThen :: Language -> Language -> [Language]
enumFrom :: Language -> [Language]
$cenumFrom :: Language -> [Language]
fromEnum :: Language -> Int
$cfromEnum :: Language -> Int
toEnum :: Int -> Language
$ctoEnum :: Int -> Language
pred :: Language -> Language
$cpred :: Language -> Language
succ :: Language -> Language
$csucc :: Language -> Language
Enum, Language
Language -> Language -> Bounded Language
forall a. a -> a -> Bounded a
maxBound :: Language
$cmaxBound :: Language
minBound :: Language
$cminBound :: Language
Bounded)

instance Named Language where
  name :: Language -> Text
name = \case
    Language
CNF_ -> Text
"cnf"
    Language
FOF_ -> Text
"fof"
    Language
TFF_ -> Text
"tff"


-- * Names

-- | The atomic word in the TPTP language - a non-empty string of space or
-- visible characters from the ASCII range 0x20 to 0x7E. If the string satisfies
-- the regular expression @[a-z][a-zA-Z0-9_]*@, then it is displayed in the TPTP
-- language as is, otherwise it is displayed in single quotes with the
-- characters @'@ and @\\@ escaped using @\\@.
--
-- >>> print (pretty (Atom "fxYz42"))
-- fxYz42
--
-- >>> print (pretty (Atom "f-'function symbol'"))
-- 'f-\'function symbol\''
--
newtype Atom = Atom Text
  deriving (Atom -> Atom -> Bool
(Atom -> Atom -> Bool) -> (Atom -> Atom -> Bool) -> Eq Atom
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Atom -> Atom -> Bool
$c/= :: Atom -> Atom -> Bool
== :: Atom -> Atom -> Bool
$c== :: Atom -> Atom -> Bool
Eq, Int -> Atom -> ShowS
[Atom] -> ShowS
Atom -> String
(Int -> Atom -> ShowS)
-> (Atom -> String) -> ([Atom] -> ShowS) -> Show Atom
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Atom] -> ShowS
$cshowList :: [Atom] -> ShowS
show :: Atom -> String
$cshow :: Atom -> String
showsPrec :: Int -> Atom -> ShowS
$cshowsPrec :: Int -> Atom -> ShowS
Show, Eq Atom
Eq Atom
-> (Atom -> Atom -> Ordering)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Atom)
-> (Atom -> Atom -> Atom)
-> Ord Atom
Atom -> Atom -> Bool
Atom -> Atom -> Ordering
Atom -> Atom -> Atom
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 :: Atom -> Atom -> Atom
$cmin :: Atom -> Atom -> Atom
max :: Atom -> Atom -> Atom
$cmax :: Atom -> Atom -> Atom
>= :: Atom -> Atom -> Bool
$c>= :: Atom -> Atom -> Bool
> :: Atom -> Atom -> Bool
$c> :: Atom -> Atom -> Bool
<= :: Atom -> Atom -> Bool
$c<= :: Atom -> Atom -> Bool
< :: Atom -> Atom -> Bool
$c< :: Atom -> Atom -> Bool
compare :: Atom -> Atom -> Ordering
$ccompare :: Atom -> Atom -> Ordering
$cp1Ord :: Eq Atom
Ord, String -> Atom
(String -> Atom) -> IsString Atom
forall a. (String -> a) -> IsString a
fromString :: String -> Atom
$cfromString :: String -> Atom
IsString)

instance Semigroup Atom where
  Atom Text
t <> :: Atom -> Atom -> Atom
<> Atom Text
s = Text -> Atom
Atom (Text
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
s)

-- | Check whether a given character is in the ASCII range 0x20 to 0x7E.
isAsciiPrint :: Char -> Bool
isAsciiPrint :: Char -> Bool
isAsciiPrint Char
c = Char -> Bool
isAscii Char
c Bool -> Bool -> Bool
&& Char -> Bool
isPrint Char
c

-- | Check whether a given string is a valid atom.
--
-- >>> isValidAtom ""
-- False
--
-- >>> isValidAtom "\r\n"
-- False
--
-- >>> isValidAtom "fxYz42"
-- True
--
-- >>> isValidAtom "f-'function symbol'"
-- True
isValidAtom :: Text -> Bool
isValidAtom :: Text -> Bool
isValidAtom Text
t = Bool -> Bool
not (Text -> Bool
Text.null Text
t)
             Bool -> Bool -> Bool
&& (Char -> Bool) -> Text -> Bool
Text.all Char -> Bool
isAsciiPrint Text
t

-- | The variable in the TPTP language - a string that satisfies the regular
-- expression @[A-Z][a-zA-Z0-9_]*@.
newtype Var = Var Text
  deriving (Var -> Var -> Bool
(Var -> Var -> Bool) -> (Var -> Var -> Bool) -> Eq Var
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Var -> Var -> Bool
$c/= :: Var -> Var -> Bool
== :: Var -> Var -> Bool
$c== :: Var -> Var -> Bool
Eq, Int -> Var -> ShowS
[Var] -> ShowS
Var -> String
(Int -> Var -> ShowS)
-> (Var -> String) -> ([Var] -> ShowS) -> Show Var
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Var] -> ShowS
$cshowList :: [Var] -> ShowS
show :: Var -> String
$cshow :: Var -> String
showsPrec :: Int -> Var -> ShowS
$cshowsPrec :: Int -> Var -> ShowS
Show, Eq Var
Eq Var
-> (Var -> Var -> Ordering)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Var)
-> (Var -> Var -> Var)
-> Ord Var
Var -> Var -> Bool
Var -> Var -> Ordering
Var -> Var -> Var
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 :: Var -> Var -> Var
$cmin :: Var -> Var -> Var
max :: Var -> Var -> Var
$cmax :: Var -> Var -> Var
>= :: Var -> Var -> Bool
$c>= :: Var -> Var -> Bool
> :: Var -> Var -> Bool
$c> :: Var -> Var -> Bool
<= :: Var -> Var -> Bool
$c<= :: Var -> Var -> Bool
< :: Var -> Var -> Bool
$c< :: Var -> Var -> Bool
compare :: Var -> Var -> Ordering
$ccompare :: Var -> Var -> Ordering
$cp1Ord :: Eq Var
Ord, String -> Var
(String -> Var) -> IsString Var
forall a. (String -> a) -> IsString a
fromString :: String -> Var
$cfromString :: String -> Var
IsString)

instance Semigroup Var where
  Var Text
v <> :: Var -> Var -> Var
<> Var Text
w = Text -> Var
Var (Text
v Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
w)

-- | Check whether a given character matches the regular expression
-- @[a-zA-Z0-9_]@.
isAlphaNumeric :: Char -> Bool
isAlphaNumeric :: Char -> Bool
isAlphaNumeric Char
c = Char -> Bool
isAsciiLower Char
c Bool -> Bool -> Bool
|| Char -> Bool
isAsciiUpper Char
c Bool -> Bool -> Bool
|| Char -> Bool
isDigit Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_'

-- | Check whether a given string is a valid variable.
--
-- >>> isValidVar ""
-- False
--
-- >>> isValidVar "x"
-- False
--
-- >>> isValidVar "X"
-- True
--
-- >>> isValidVar "Cat"
-- True
--
-- >>> isValidVar "C@t"
-- False
isValidVar :: Text -> Bool
isValidVar :: Text -> Bool
isValidVar Text
t = Bool -> Bool
not (Text -> Bool
Text.null Text
t)
            Bool -> Bool -> Bool
&& Char -> Bool
isAsciiUpper (Text -> Char
Text.head Text
t)
            Bool -> Bool -> Bool
&& (Char -> Bool) -> Text -> Bool
Text.all Char -> Bool
isAlphaNumeric (Text -> Text
Text.tail Text
t)

-- | The distinct object in the TPTP language - a (possibly empty) string of
-- space or visible characters from the ASCII range 0x20 to 0x7E. The string is
-- always displayed in the TPTP language in double quotes with the characters
-- @"@ and @\\@ escaped using @\\@.
--
-- >>> print (pretty (DistinctObject "Godel's incompleteness theorem"))
-- "Godel's incompleteness theorem"
--
-- Distinct objects are different from atoms in that they implicitly carry
-- semantic inequality. The TPTP documentation says the following about distinct
-- objects.
--
-- /Distinct objects are different from (but may be equal to) other tokens,/
-- /e.g.,/ @"cat"@ /is different from/ @\'cat\'@ /and/ @cat@. /Distinct objects/
-- /are always interpreted as themselves, so if they are different they are/
-- /unequal, e.g.,/ @\"Apple\" != \"Microsoft\"@ /is implicit./
newtype DistinctObject = DistinctObject Text
  deriving (DistinctObject -> DistinctObject -> Bool
(DistinctObject -> DistinctObject -> Bool)
-> (DistinctObject -> DistinctObject -> Bool) -> Eq DistinctObject
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DistinctObject -> DistinctObject -> Bool
$c/= :: DistinctObject -> DistinctObject -> Bool
== :: DistinctObject -> DistinctObject -> Bool
$c== :: DistinctObject -> DistinctObject -> Bool
Eq, Int -> DistinctObject -> ShowS
[DistinctObject] -> ShowS
DistinctObject -> String
(Int -> DistinctObject -> ShowS)
-> (DistinctObject -> String)
-> ([DistinctObject] -> ShowS)
-> Show DistinctObject
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DistinctObject] -> ShowS
$cshowList :: [DistinctObject] -> ShowS
show :: DistinctObject -> String
$cshow :: DistinctObject -> String
showsPrec :: Int -> DistinctObject -> ShowS
$cshowsPrec :: Int -> DistinctObject -> ShowS
Show, Eq DistinctObject
Eq DistinctObject
-> (DistinctObject -> DistinctObject -> Ordering)
-> (DistinctObject -> DistinctObject -> Bool)
-> (DistinctObject -> DistinctObject -> Bool)
-> (DistinctObject -> DistinctObject -> Bool)
-> (DistinctObject -> DistinctObject -> Bool)
-> (DistinctObject -> DistinctObject -> DistinctObject)
-> (DistinctObject -> DistinctObject -> DistinctObject)
-> Ord DistinctObject
DistinctObject -> DistinctObject -> Bool
DistinctObject -> DistinctObject -> Ordering
DistinctObject -> DistinctObject -> DistinctObject
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 :: DistinctObject -> DistinctObject -> DistinctObject
$cmin :: DistinctObject -> DistinctObject -> DistinctObject
max :: DistinctObject -> DistinctObject -> DistinctObject
$cmax :: DistinctObject -> DistinctObject -> DistinctObject
>= :: DistinctObject -> DistinctObject -> Bool
$c>= :: DistinctObject -> DistinctObject -> Bool
> :: DistinctObject -> DistinctObject -> Bool
$c> :: DistinctObject -> DistinctObject -> Bool
<= :: DistinctObject -> DistinctObject -> Bool
$c<= :: DistinctObject -> DistinctObject -> Bool
< :: DistinctObject -> DistinctObject -> Bool
$c< :: DistinctObject -> DistinctObject -> Bool
compare :: DistinctObject -> DistinctObject -> Ordering
$ccompare :: DistinctObject -> DistinctObject -> Ordering
$cp1Ord :: Eq DistinctObject
Ord, String -> DistinctObject
(String -> DistinctObject) -> IsString DistinctObject
forall a. (String -> a) -> IsString a
fromString :: String -> DistinctObject
$cfromString :: String -> DistinctObject
IsString)

instance Semigroup DistinctObject where
  DistinctObject Text
d <> :: DistinctObject -> DistinctObject -> DistinctObject
<> DistinctObject Text
b = Text -> DistinctObject
DistinctObject (Text
d Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
b)

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

-- | Check whether a given string is a valid distinct object.
--
-- >>> isValidDistinctObject ""
-- True
--
-- >>> isValidDistinctObject "Godel's incompleteness theorem"
-- True
--
-- >>> isValidDistinctObject "\r\n"
-- False
isValidDistinctObject :: Text -> Bool
isValidDistinctObject :: Text -> Bool
isValidDistinctObject = (Char -> Bool) -> Text -> Bool
Text.all Char -> Bool
isAsciiPrint

-- | The identifier reserved in the TPTP specification and theorem proving
-- systems that implement it. Reserved identifiers are used to represent
-- function symbols, predicate symbols, sorts, formula roles and others.
-- Reserved identifiers are non-empty strings that satisfy the regular
-- expression @[a-z][a-zA-Z0-9_]*@. Reserved identifiers of functions,
-- predicates, and sorts, used as names, are in addition prepended by @$@.
--
-- >>> print (pretty (Standard I))
-- i
--
-- >>> print (pretty (Standard Axiom))
-- axiom
--
-- >>> print (pretty (Extended "negated_lemma" :: Reserved Role))
-- negated_lemma
data Reserved s
  = Standard s    -- ^ The identifier contained in the TPTP specification.
  | Extended Text -- ^ The identifier not contained in the standard TPTP but
                  -- implemented by some theorem prover. For example, Vampire
                  -- implements the sort constructor @$array@.
  deriving (Reserved s -> Reserved s -> Bool
(Reserved s -> Reserved s -> Bool)
-> (Reserved s -> Reserved s -> Bool) -> Eq (Reserved s)
forall s. Eq s => Reserved s -> Reserved s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Reserved s -> Reserved s -> Bool
$c/= :: forall s. Eq s => Reserved s -> Reserved s -> Bool
== :: Reserved s -> Reserved s -> Bool
$c== :: forall s. Eq s => Reserved s -> Reserved s -> Bool
Eq, Int -> Reserved s -> ShowS
[Reserved s] -> ShowS
Reserved s -> String
(Int -> Reserved s -> ShowS)
-> (Reserved s -> String)
-> ([Reserved s] -> ShowS)
-> Show (Reserved s)
forall s. Show s => Int -> Reserved s -> ShowS
forall s. Show s => [Reserved s] -> ShowS
forall s. Show s => Reserved s -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Reserved s] -> ShowS
$cshowList :: forall s. Show s => [Reserved s] -> ShowS
show :: Reserved s -> String
$cshow :: forall s. Show s => Reserved s -> String
showsPrec :: Int -> Reserved s -> ShowS
$cshowsPrec :: forall s. Show s => Int -> Reserved s -> ShowS
Show, Eq (Reserved s)
Eq (Reserved s)
-> (Reserved s -> Reserved s -> Ordering)
-> (Reserved s -> Reserved s -> Bool)
-> (Reserved s -> Reserved s -> Bool)
-> (Reserved s -> Reserved s -> Bool)
-> (Reserved s -> Reserved s -> Bool)
-> (Reserved s -> Reserved s -> Reserved s)
-> (Reserved s -> Reserved s -> Reserved s)
-> Ord (Reserved s)
Reserved s -> Reserved s -> Bool
Reserved s -> Reserved s -> Ordering
Reserved s -> Reserved s -> Reserved s
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 s. Ord s => Eq (Reserved s)
forall s. Ord s => Reserved s -> Reserved s -> Bool
forall s. Ord s => Reserved s -> Reserved s -> Ordering
forall s. Ord s => Reserved s -> Reserved s -> Reserved s
min :: Reserved s -> Reserved s -> Reserved s
$cmin :: forall s. Ord s => Reserved s -> Reserved s -> Reserved s
max :: Reserved s -> Reserved s -> Reserved s
$cmax :: forall s. Ord s => Reserved s -> Reserved s -> Reserved s
>= :: Reserved s -> Reserved s -> Bool
$c>= :: forall s. Ord s => Reserved s -> Reserved s -> Bool
> :: Reserved s -> Reserved s -> Bool
$c> :: forall s. Ord s => Reserved s -> Reserved s -> Bool
<= :: Reserved s -> Reserved s -> Bool
$c<= :: forall s. Ord s => Reserved s -> Reserved s -> Bool
< :: Reserved s -> Reserved s -> Bool
$c< :: forall s. Ord s => Reserved s -> Reserved s -> Bool
compare :: Reserved s -> Reserved s -> Ordering
$ccompare :: forall s. Ord s => Reserved s -> Reserved s -> Ordering
$cp1Ord :: forall s. Ord s => Eq (Reserved s)
Ord)

-- | A smart 'Extended' constructor - only uses 'Extended' if the given string
-- does not correspond to any of the standard identifiers.
--
-- >>> extended "int" :: Reserved Sort
-- Standard Int
--
-- >>> extended "array" :: Reserved Sort
-- Extended "array"
extended :: (Named a, Enum a, Bounded a) => Text -> Reserved a
extended :: Text -> Reserved a
extended Text
t
  | Just a
a <- (a -> Bool) -> [a] -> Maybe a
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\a
a -> a -> Text
forall a. Named a => a -> Text
name a
a Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
t) [a
forall a. Bounded a => a
minBound..] = a -> Reserved a
forall s. s -> Reserved s
Standard a
a
  | Bool
otherwise = Text -> Reserved a
forall s. Text -> Reserved s
Extended Text
t

instance (Named a, Enum a, Bounded a) => IsString (Reserved a) where
  fromString :: String -> Reserved a
fromString = Text -> Reserved a
forall a. (Named a, Enum a, Bounded a) => Text -> Reserved a
extended (Text -> Reserved a) -> (String -> Text) -> String -> Reserved a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
forall a. IsString a => String -> a
fromString

-- | Check whether a given string is a valid reserved identifier.
--
-- >>> isValidReserved ""
-- False
--
-- >>> isValidReserved "x"
-- True
--
-- >>> isValidReserved "X"
-- False
--
-- >>> isValidReserved "cat"
-- True
--
-- >>> isValidReserved "c@t"
-- False
--
-- >>> isValidReserved "$int"
-- False
--
isValidReserved :: Text -> Bool
isValidReserved :: Text -> Bool
isValidReserved Text
t = Bool -> Bool
not (Text -> Bool
Text.null Text
t)
                 Bool -> Bool -> Bool
&& Char -> Bool
isAsciiLower (Text -> Char
Text.head Text
t)
                 Bool -> Bool -> Bool
&& (Char -> Bool) -> Text -> Bool
Text.all Char -> Bool
isAlphaNumeric (Text -> Text
Text.tail Text
t)

-- | The class 'Named' allows assigning concrete names to reserved constants
-- in the TPTP language.
class Named a where
  name :: a -> Text

-- | The standard function symbol in TPTP.
-- Represents an operation in a first-order theory of arithmetic.
-- See <http://www.tptp.org/TPTP/TR/TPTPTR.shtml#arithmetic> for details.
data Function
  = Uminus     -- ^ @$uminus@ - Unary minus of a number.
  | Sum        -- ^ @$sum@ - Sum of two numbers.
  | Difference -- ^ @$difference@ - Difference between two numbers.
  | Product    -- ^ @$product@ - Product of two numbers.
  | Quotient   -- ^ @$quotient@ - Exact quotient of two @$rat@ or @$real@ numbers.
  | QuotientE  -- ^ @$quotient_e@ - Integral quotient of two numbers.
  | QuotientT  -- ^ @$quotient_t@ - Integral quotient of two numbers.
  | QuotientF  -- ^ @$quotient_f@ - Integral quotient of two numbers.
  | RemainderE -- ^ @$remainder_e@ - Remainder after integral division of two numbers.
  | RemainderT -- ^ @$remainder_t@ - Remainder after integral division of two numbers.
  | RemainderF -- ^ @$remainder_f@ - Remainder after integral division of two numbers.
  | Floor      -- ^ @$floor@ - Floor of a number.
  | Ceiling    -- ^ @$ceiling@ - Ceiling of a number.
  | Truncate   -- ^ @$truncate@ - Truncation of a number.
  | Round      -- ^ @$round@ - Rounding of a number.
  | ToInt      -- ^ @$to_int@ - Coercion of a number to @$int@.
  | ToRat      -- ^ @$to_rat@ - Coercion of a number to @$rat@.
  | ToReal     -- ^ @$to_real@ - Coercion of a number to @$real@.
  deriving (Function -> Function -> Bool
(Function -> Function -> Bool)
-> (Function -> Function -> Bool) -> Eq Function
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Function -> Function -> Bool
$c/= :: Function -> Function -> Bool
== :: Function -> Function -> Bool
$c== :: Function -> Function -> Bool
Eq, Int -> Function -> ShowS
[Function] -> ShowS
Function -> String
(Int -> Function -> ShowS)
-> (Function -> String) -> ([Function] -> ShowS) -> Show Function
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Function] -> ShowS
$cshowList :: [Function] -> ShowS
show :: Function -> String
$cshow :: Function -> String
showsPrec :: Int -> Function -> ShowS
$cshowsPrec :: Int -> Function -> ShowS
Show, Eq Function
Eq Function
-> (Function -> Function -> Ordering)
-> (Function -> Function -> Bool)
-> (Function -> Function -> Bool)
-> (Function -> Function -> Bool)
-> (Function -> Function -> Bool)
-> (Function -> Function -> Function)
-> (Function -> Function -> Function)
-> Ord Function
Function -> Function -> Bool
Function -> Function -> Ordering
Function -> Function -> Function
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 :: Function -> Function -> Function
$cmin :: Function -> Function -> Function
max :: Function -> Function -> Function
$cmax :: Function -> Function -> Function
>= :: Function -> Function -> Bool
$c>= :: Function -> Function -> Bool
> :: Function -> Function -> Bool
$c> :: Function -> Function -> Bool
<= :: Function -> Function -> Bool
$c<= :: Function -> Function -> Bool
< :: Function -> Function -> Bool
$c< :: Function -> Function -> Bool
compare :: Function -> Function -> Ordering
$ccompare :: Function -> Function -> Ordering
$cp1Ord :: Eq Function
Ord, Int -> Function
Function -> Int
Function -> [Function]
Function -> Function
Function -> Function -> [Function]
Function -> Function -> Function -> [Function]
(Function -> Function)
-> (Function -> Function)
-> (Int -> Function)
-> (Function -> Int)
-> (Function -> [Function])
-> (Function -> Function -> [Function])
-> (Function -> Function -> [Function])
-> (Function -> Function -> Function -> [Function])
-> Enum Function
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 :: Function -> Function -> Function -> [Function]
$cenumFromThenTo :: Function -> Function -> Function -> [Function]
enumFromTo :: Function -> Function -> [Function]
$cenumFromTo :: Function -> Function -> [Function]
enumFromThen :: Function -> Function -> [Function]
$cenumFromThen :: Function -> Function -> [Function]
enumFrom :: Function -> [Function]
$cenumFrom :: Function -> [Function]
fromEnum :: Function -> Int
$cfromEnum :: Function -> Int
toEnum :: Int -> Function
$ctoEnum :: Int -> Function
pred :: Function -> Function
$cpred :: Function -> Function
succ :: Function -> Function
$csucc :: Function -> Function
Enum, Function
Function -> Function -> Bounded Function
forall a. a -> a -> Bounded a
maxBound :: Function
$cmaxBound :: Function
minBound :: Function
$cminBound :: Function
Bounded)

instance Named Function where
  name :: Function -> Text
name = \case
    Function
Uminus     -> Text
"uminus"
    Function
Sum        -> Text
"sum"
    Function
Difference -> Text
"difference"
    Function
Product    -> Text
"product"
    Function
Quotient   -> Text
"quotient"
    Function
QuotientE  -> Text
"quotient_e"
    Function
QuotientT  -> Text
"quotient_t"
    Function
QuotientF  -> Text
"quotient_f"
    Function
RemainderE -> Text
"remainder_e"
    Function
RemainderT -> Text
"remainder_t"
    Function
RemainderF -> Text
"remainder_f"
    Function
Floor      -> Text
"floor"
    Function
Ceiling    -> Text
"ceiling"
    Function
Truncate   -> Text
"truncate"
    Function
Round      -> Text
"round"
    Function
ToInt      -> Text
"to_int"
    Function
ToRat      -> Text
"to_rat"
    Function
ToReal     -> Text
"to_real"

-- | The standard predicate symbol in TPTP.
-- See <http://www.tptp.org/TPTP/TR/TPTPTR.shtml#arithmetic> for details.
data Predicate
  = Tautology -- ^ @$true@ - Logical tautology.
  | Falsum    -- ^ @$false@ - Logical falsum.
  | Distinct  -- ^ @$distinct@ - Denotes that its arguments are unequal to each other.
  | Less      -- ^ @$less@ - Less-than comparison of two numbers.
  | Lesseq    -- ^ @$lesseq@ - Less-than-or-equal-to comparison of two numbers.
  | Greater   -- ^ @$greater@ - Greater-than comparison of two numbers.
  | Greatereq -- ^ @$greatereq@ - Greater-than-or-equal-to comparison of two numbers.
  | IsInt     -- ^ @$is_nat@ - Test for coincidence with an integer.
  | IsRat     -- ^ @$is_rat@ - Test for coincidence with a rational.
  deriving (Predicate -> Predicate -> Bool
(Predicate -> Predicate -> Bool)
-> (Predicate -> Predicate -> Bool) -> Eq Predicate
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Predicate -> Predicate -> Bool
$c/= :: Predicate -> Predicate -> Bool
== :: Predicate -> Predicate -> Bool
$c== :: Predicate -> Predicate -> Bool
Eq, Int -> Predicate -> ShowS
[Predicate] -> ShowS
Predicate -> String
(Int -> Predicate -> ShowS)
-> (Predicate -> String)
-> ([Predicate] -> ShowS)
-> Show Predicate
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Predicate] -> ShowS
$cshowList :: [Predicate] -> ShowS
show :: Predicate -> String
$cshow :: Predicate -> String
showsPrec :: Int -> Predicate -> ShowS
$cshowsPrec :: Int -> Predicate -> ShowS
Show, Eq Predicate
Eq Predicate
-> (Predicate -> Predicate -> Ordering)
-> (Predicate -> Predicate -> Bool)
-> (Predicate -> Predicate -> Bool)
-> (Predicate -> Predicate -> Bool)
-> (Predicate -> Predicate -> Bool)
-> (Predicate -> Predicate -> Predicate)
-> (Predicate -> Predicate -> Predicate)
-> Ord Predicate
Predicate -> Predicate -> Bool
Predicate -> Predicate -> Ordering
Predicate -> Predicate -> Predicate
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 :: Predicate -> Predicate -> Predicate
$cmin :: Predicate -> Predicate -> Predicate
max :: Predicate -> Predicate -> Predicate
$cmax :: Predicate -> Predicate -> Predicate
>= :: Predicate -> Predicate -> Bool
$c>= :: Predicate -> Predicate -> Bool
> :: Predicate -> Predicate -> Bool
$c> :: Predicate -> Predicate -> Bool
<= :: Predicate -> Predicate -> Bool
$c<= :: Predicate -> Predicate -> Bool
< :: Predicate -> Predicate -> Bool
$c< :: Predicate -> Predicate -> Bool
compare :: Predicate -> Predicate -> Ordering
$ccompare :: Predicate -> Predicate -> Ordering
$cp1Ord :: Eq Predicate
Ord, Int -> Predicate
Predicate -> Int
Predicate -> [Predicate]
Predicate -> Predicate
Predicate -> Predicate -> [Predicate]
Predicate -> Predicate -> Predicate -> [Predicate]
(Predicate -> Predicate)
-> (Predicate -> Predicate)
-> (Int -> Predicate)
-> (Predicate -> Int)
-> (Predicate -> [Predicate])
-> (Predicate -> Predicate -> [Predicate])
-> (Predicate -> Predicate -> [Predicate])
-> (Predicate -> Predicate -> Predicate -> [Predicate])
-> Enum Predicate
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 :: Predicate -> Predicate -> Predicate -> [Predicate]
$cenumFromThenTo :: Predicate -> Predicate -> Predicate -> [Predicate]
enumFromTo :: Predicate -> Predicate -> [Predicate]
$cenumFromTo :: Predicate -> Predicate -> [Predicate]
enumFromThen :: Predicate -> Predicate -> [Predicate]
$cenumFromThen :: Predicate -> Predicate -> [Predicate]
enumFrom :: Predicate -> [Predicate]
$cenumFrom :: Predicate -> [Predicate]
fromEnum :: Predicate -> Int
$cfromEnum :: Predicate -> Int
toEnum :: Int -> Predicate
$ctoEnum :: Int -> Predicate
pred :: Predicate -> Predicate
$cpred :: Predicate -> Predicate
succ :: Predicate -> Predicate
$csucc :: Predicate -> Predicate
Enum, Predicate
Predicate -> Predicate -> Bounded Predicate
forall a. a -> a -> Bounded a
maxBound :: Predicate
$cmaxBound :: Predicate
minBound :: Predicate
$cminBound :: Predicate
Bounded)

instance Named Predicate where
  name :: Predicate -> Text
name = \case
    Predicate
Tautology -> Text
"true"
    Predicate
Falsum    -> Text
"false"
    Predicate
Distinct  -> Text
"distinct"
    Predicate
Less      -> Text
"less"
    Predicate
Lesseq    -> Text
"lesseq"
    Predicate
Greater   -> Text
"greater"
    Predicate
Greatereq -> Text
"greatereq"
    Predicate
IsInt     -> Text
"is_int"
    Predicate
IsRat     -> Text
"is_rat"

-- | The name of a function symbol, a predicate symbol, a sort, a formula role
-- or other.
--
-- > >>> print (pretty (Reserved (Standard I)))
-- > $i
--
-- > >>> print (pretty (Reserved (Extended "array" :: Reserved Sort)))
-- > $array
--
-- >>> print (pretty (Defined (Atom "array") :: Name Sort))
-- array
data Name s
  = Reserved (Reserved s) -- ^ The name reserved in the TPTP specification.
                          -- This name is parsed and pretty printed with the
                          -- leading @$@ character.
  | Defined Atom          -- ^ The name defined by the user.
  deriving (Name s -> Name s -> Bool
(Name s -> Name s -> Bool)
-> (Name s -> Name s -> Bool) -> Eq (Name s)
forall s. Eq s => Name s -> Name s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Name s -> Name s -> Bool
$c/= :: forall s. Eq s => Name s -> Name s -> Bool
== :: Name s -> Name s -> Bool
$c== :: forall s. Eq s => Name s -> Name s -> Bool
Eq, Int -> Name s -> ShowS
[Name s] -> ShowS
Name s -> String
(Int -> Name s -> ShowS)
-> (Name s -> String) -> ([Name s] -> ShowS) -> Show (Name s)
forall s. Show s => Int -> Name s -> ShowS
forall s. Show s => [Name s] -> ShowS
forall s. Show s => Name s -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Name s] -> ShowS
$cshowList :: forall s. Show s => [Name s] -> ShowS
show :: Name s -> String
$cshow :: forall s. Show s => Name s -> String
showsPrec :: Int -> Name s -> ShowS
$cshowsPrec :: forall s. Show s => Int -> Name s -> ShowS
Show, Eq (Name s)
Eq (Name s)
-> (Name s -> Name s -> Ordering)
-> (Name s -> Name s -> Bool)
-> (Name s -> Name s -> Bool)
-> (Name s -> Name s -> Bool)
-> (Name s -> Name s -> Bool)
-> (Name s -> Name s -> Name s)
-> (Name s -> Name s -> Name s)
-> Ord (Name s)
Name s -> Name s -> Bool
Name s -> Name s -> Ordering
Name s -> Name s -> Name s
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 s. Ord s => Eq (Name s)
forall s. Ord s => Name s -> Name s -> Bool
forall s. Ord s => Name s -> Name s -> Ordering
forall s. Ord s => Name s -> Name s -> Name s
min :: Name s -> Name s -> Name s
$cmin :: forall s. Ord s => Name s -> Name s -> Name s
max :: Name s -> Name s -> Name s
$cmax :: forall s. Ord s => Name s -> Name s -> Name s
>= :: Name s -> Name s -> Bool
$c>= :: forall s. Ord s => Name s -> Name s -> Bool
> :: Name s -> Name s -> Bool
$c> :: forall s. Ord s => Name s -> Name s -> Bool
<= :: Name s -> Name s -> Bool
$c<= :: forall s. Ord s => Name s -> Name s -> Bool
< :: Name s -> Name s -> Bool
$c< :: forall s. Ord s => Name s -> Name s -> Bool
compare :: Name s -> Name s -> Ordering
$ccompare :: forall s. Ord s => Name s -> Name s -> Ordering
$cp1Ord :: forall s. Ord s => Eq (Name s)
Ord)

-- | The 'IsString' instance of 'Name' opts for using the 'Defined' constructor.
instance IsString (Name s) where
  fromString :: String -> Name s
fromString = Atom -> Name s
forall s. Atom -> Name s
Defined (Atom -> Name s) -> (String -> Atom) -> String -> Name s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Atom
forall a. IsString a => String -> a
fromString


-- * Sorts and types

-- | The standard sort in TPTP.
data Sort
  = I    -- ^ @$i@ - The sort of individuals.
  | O    -- ^ @$o@ - The sort of booleans.
  | Int  -- ^ @$int@ - The sort of integers.
  | Real -- ^ @$real@ - The sort of real numbers.
  | Rat  -- ^ @$rat@ - The sort of rational numbers.
  deriving (Sort -> Sort -> Bool
(Sort -> Sort -> Bool) -> (Sort -> Sort -> Bool) -> Eq Sort
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sort -> Sort -> Bool
$c/= :: Sort -> Sort -> Bool
== :: Sort -> Sort -> Bool
$c== :: Sort -> Sort -> Bool
Eq, Int -> Sort -> ShowS
[Sort] -> ShowS
Sort -> String
(Int -> Sort -> ShowS)
-> (Sort -> String) -> ([Sort] -> ShowS) -> Show Sort
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sort] -> ShowS
$cshowList :: [Sort] -> ShowS
show :: Sort -> String
$cshow :: Sort -> String
showsPrec :: Int -> Sort -> ShowS
$cshowsPrec :: Int -> Sort -> ShowS
Show, Eq Sort
Eq Sort
-> (Sort -> Sort -> Ordering)
-> (Sort -> Sort -> Bool)
-> (Sort -> Sort -> Bool)
-> (Sort -> Sort -> Bool)
-> (Sort -> Sort -> Bool)
-> (Sort -> Sort -> Sort)
-> (Sort -> Sort -> Sort)
-> Ord Sort
Sort -> Sort -> Bool
Sort -> Sort -> Ordering
Sort -> Sort -> Sort
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 :: Sort -> Sort -> Sort
$cmin :: Sort -> Sort -> Sort
max :: Sort -> Sort -> Sort
$cmax :: Sort -> Sort -> Sort
>= :: Sort -> Sort -> Bool
$c>= :: Sort -> Sort -> Bool
> :: Sort -> Sort -> Bool
$c> :: Sort -> Sort -> Bool
<= :: Sort -> Sort -> Bool
$c<= :: Sort -> Sort -> Bool
< :: Sort -> Sort -> Bool
$c< :: Sort -> Sort -> Bool
compare :: Sort -> Sort -> Ordering
$ccompare :: Sort -> Sort -> Ordering
$cp1Ord :: Eq Sort
Ord, Int -> Sort
Sort -> Int
Sort -> [Sort]
Sort -> Sort
Sort -> Sort -> [Sort]
Sort -> Sort -> Sort -> [Sort]
(Sort -> Sort)
-> (Sort -> Sort)
-> (Int -> Sort)
-> (Sort -> Int)
-> (Sort -> [Sort])
-> (Sort -> Sort -> [Sort])
-> (Sort -> Sort -> [Sort])
-> (Sort -> Sort -> Sort -> [Sort])
-> Enum Sort
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 :: Sort -> Sort -> Sort -> [Sort]
$cenumFromThenTo :: Sort -> Sort -> Sort -> [Sort]
enumFromTo :: Sort -> Sort -> [Sort]
$cenumFromTo :: Sort -> Sort -> [Sort]
enumFromThen :: Sort -> Sort -> [Sort]
$cenumFromThen :: Sort -> Sort -> [Sort]
enumFrom :: Sort -> [Sort]
$cenumFrom :: Sort -> [Sort]
fromEnum :: Sort -> Int
$cfromEnum :: Sort -> Int
toEnum :: Int -> Sort
$ctoEnum :: Int -> Sort
pred :: Sort -> Sort
$cpred :: Sort -> Sort
succ :: Sort -> Sort
$csucc :: Sort -> Sort
Enum, Sort
Sort -> Sort -> Bounded Sort
forall a. a -> a -> Bounded a
maxBound :: Sort
$cmaxBound :: Sort
minBound :: Sort
$cminBound :: Sort
Bounded)

instance Named Sort where
  name :: Sort -> Text
name = \case
    Sort
I    -> Text
"i"
    Sort
O    -> Text
"o"
    Sort
Int  -> Text
"int"
    Sort
Real -> Text
"real"
    Sort
Rat  -> Text
"rat"

-- | The sort in sorted rank-1 polymorphic logic with sort constructors (TFF1) -
-- an application of a sort constructor to zero or more sorts or a sort variable
-- that comes from a sort quantifier. A zero-arity sort application is simply a
-- sort.
--
-- Every TFF0 sort is also a TFF1 sort, but not the other way around.
data TFF1Sort
  = SortVariable Var
  | TFF1Sort (Name Sort) [TFF1Sort]
  deriving (TFF1Sort -> TFF1Sort -> Bool
(TFF1Sort -> TFF1Sort -> Bool)
-> (TFF1Sort -> TFF1Sort -> Bool) -> Eq TFF1Sort
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TFF1Sort -> TFF1Sort -> Bool
$c/= :: TFF1Sort -> TFF1Sort -> Bool
== :: TFF1Sort -> TFF1Sort -> Bool
$c== :: TFF1Sort -> TFF1Sort -> Bool
Eq, Int -> TFF1Sort -> ShowS
[TFF1Sort] -> ShowS
TFF1Sort -> String
(Int -> TFF1Sort -> ShowS)
-> (TFF1Sort -> String) -> ([TFF1Sort] -> ShowS) -> Show TFF1Sort
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TFF1Sort] -> ShowS
$cshowList :: [TFF1Sort] -> ShowS
show :: TFF1Sort -> String
$cshow :: TFF1Sort -> String
showsPrec :: Int -> TFF1Sort -> ShowS
$cshowsPrec :: Int -> TFF1Sort -> ShowS
Show, Eq TFF1Sort
Eq TFF1Sort
-> (TFF1Sort -> TFF1Sort -> Ordering)
-> (TFF1Sort -> TFF1Sort -> Bool)
-> (TFF1Sort -> TFF1Sort -> Bool)
-> (TFF1Sort -> TFF1Sort -> Bool)
-> (TFF1Sort -> TFF1Sort -> Bool)
-> (TFF1Sort -> TFF1Sort -> TFF1Sort)
-> (TFF1Sort -> TFF1Sort -> TFF1Sort)
-> Ord TFF1Sort
TFF1Sort -> TFF1Sort -> Bool
TFF1Sort -> TFF1Sort -> Ordering
TFF1Sort -> TFF1Sort -> TFF1Sort
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 :: TFF1Sort -> TFF1Sort -> TFF1Sort
$cmin :: TFF1Sort -> TFF1Sort -> TFF1Sort
max :: TFF1Sort -> TFF1Sort -> TFF1Sort
$cmax :: TFF1Sort -> TFF1Sort -> TFF1Sort
>= :: TFF1Sort -> TFF1Sort -> Bool
$c>= :: TFF1Sort -> TFF1Sort -> Bool
> :: TFF1Sort -> TFF1Sort -> Bool
$c> :: TFF1Sort -> TFF1Sort -> Bool
<= :: TFF1Sort -> TFF1Sort -> Bool
$c<= :: TFF1Sort -> TFF1Sort -> Bool
< :: TFF1Sort -> TFF1Sort -> Bool
$c< :: TFF1Sort -> TFF1Sort -> Bool
compare :: TFF1Sort -> TFF1Sort -> Ordering
$ccompare :: TFF1Sort -> TFF1Sort -> Ordering
$cp1Ord :: Eq TFF1Sort
Ord)

-- | Attempt to convert a given TFF1 sort to TFF0. This function succeeds iff
-- the given sort is a sort constructor with zero arity.
monomorphizeTFF1Sort :: TFF1Sort -> Maybe (Name Sort)
monomorphizeTFF1Sort :: TFF1Sort -> Maybe (Name Sort)
monomorphizeTFF1Sort = \case
  TFF1Sort Name Sort
f [] -> Name Sort -> Maybe (Name Sort)
forall a. a -> Maybe a
Just Name Sort
f
  TFF1Sort
_ -> Maybe (Name Sort)
forall a. Maybe a
Nothing

-- | The type of a function or a predicate symbol in a sorted first-order logic
-- (TFF0 or TFF1). Each TFF0 type is also a TFF1 type, but not the other way
-- around.
data Type
  -- | The type of a function or a predicate symbol in the sorted monomorphic
  -- first-order logic (TFF0). It is a mapping of zero or more sorts to a sort.
  -- The empty list of argument sorts marks the type of a constant symbol.
  = Type [Name Sort] (Name Sort)

  -- | The type of a function or a predicate symbol in the sorted rank-1
  -- polymorphic first-order logic (TFF1). It is a (possibly quantified)
  -- mapping of zero or more TFF1 sorts to a TFF1 sort. The empty list of sort
  -- variables marks a monomorphic TFF1 type. The empty list of argument sorts
  -- marks the type of a constant symbol.
  | TFF1Type [Var] [TFF1Sort] TFF1Sort

  deriving (Type -> Type -> Bool
(Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c== :: Type -> Type -> Bool
Eq, Int -> Type -> ShowS
[Type] -> ShowS
Type -> String
(Int -> Type -> ShowS)
-> (Type -> String) -> ([Type] -> ShowS) -> Show Type
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Type] -> ShowS
$cshowList :: [Type] -> ShowS
show :: Type -> String
$cshow :: Type -> String
showsPrec :: Int -> Type -> ShowS
$cshowsPrec :: Int -> Type -> ShowS
Show, Eq Type
Eq Type
-> (Type -> Type -> Ordering)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> (Type -> Type -> Type)
-> Ord Type
Type -> Type -> Bool
Type -> Type -> Ordering
Type -> Type -> Type
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 :: Type -> Type -> Type
$cmin :: Type -> Type -> Type
max :: Type -> Type -> Type
$cmax :: Type -> Type -> Type
>= :: Type -> Type -> Bool
$c>= :: Type -> Type -> Bool
> :: Type -> Type -> Bool
$c> :: Type -> Type -> Bool
<= :: Type -> Type -> Bool
$c<= :: Type -> Type -> Bool
< :: Type -> Type -> Bool
$c< :: Type -> Type -> Bool
compare :: Type -> Type -> Ordering
$ccompare :: Type -> Type -> Ordering
$cp1Ord :: Eq Type
Ord)

-- | A smart constructor of a TFF1 type. 'tff1Type' constructs a TFF0 type with
-- its arguments, if it is possible, and otherwise constructs a TFF1 type.
tff1Type :: [Var]      -- ^ Quantified type variables.
         -> [TFF1Sort] -- ^ Sort arguments.
         -> TFF1Sort   -- ^ Return sort.
         -> Type
tff1Type :: [Var] -> [TFF1Sort] -> TFF1Sort -> Type
tff1Type [] [TFF1Sort]
ss TFF1Sort
s
  | Just [Name Sort]
ss' <- (TFF1Sort -> Maybe (Name Sort)) -> [TFF1Sort] -> Maybe [Name Sort]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse TFF1Sort -> Maybe (Name Sort)
monomorphizeTFF1Sort [TFF1Sort]
ss
  , Just Name Sort
s'  <- TFF1Sort -> Maybe (Name Sort)
monomorphizeTFF1Sort TFF1Sort
s = [Name Sort] -> Name Sort -> Type
Type [Name Sort]
ss' Name Sort
s'
tff1Type [Var]
vs [TFF1Sort]
ss TFF1Sort
s = [Var] -> [TFF1Sort] -> TFF1Sort -> Type
TFF1Type [Var]
vs [TFF1Sort]
ss TFF1Sort
s


-- * First-order logic

-- | The integer, rational, or real constant.
data Number
  = IntegerConstant Integer
  -- ^ A positive or negative integer.
  | RationalConstant Integer Integer
  -- ^ A rational number, represented as a pair of its numerator (positive or
  -- negative integer, possibly zero) and denominator (strictly positive
  -- non-zero integer).
  | RealConstant Scientific
  -- ^ A real number, written in the scientific notation.
  deriving (Number -> Number -> Bool
(Number -> Number -> Bool)
-> (Number -> Number -> Bool) -> Eq Number
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Number -> Number -> Bool
$c/= :: Number -> Number -> Bool
== :: Number -> Number -> Bool
$c== :: Number -> Number -> Bool
Eq, Int -> Number -> ShowS
[Number] -> ShowS
Number -> String
(Int -> Number -> ShowS)
-> (Number -> String) -> ([Number] -> ShowS) -> Show Number
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Number] -> ShowS
$cshowList :: [Number] -> ShowS
show :: Number -> String
$cshow :: Number -> String
showsPrec :: Int -> Number -> ShowS
$cshowsPrec :: Int -> Number -> ShowS
Show, Eq Number
Eq Number
-> (Number -> Number -> Ordering)
-> (Number -> Number -> Bool)
-> (Number -> Number -> Bool)
-> (Number -> Number -> Bool)
-> (Number -> Number -> Bool)
-> (Number -> Number -> Number)
-> (Number -> Number -> Number)
-> Ord Number
Number -> Number -> Bool
Number -> Number -> Ordering
Number -> Number -> Number
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 :: Number -> Number -> Number
$cmin :: Number -> Number -> Number
max :: Number -> Number -> Number
$cmax :: Number -> Number -> Number
>= :: Number -> Number -> Bool
$c>= :: Number -> Number -> Bool
> :: Number -> Number -> Bool
$c> :: Number -> Number -> Bool
<= :: Number -> Number -> Bool
$c<= :: Number -> Number -> Bool
< :: Number -> Number -> Bool
$c< :: Number -> Number -> Bool
compare :: Number -> Number -> Ordering
$ccompare :: Number -> Number -> Ordering
$cp1Ord :: Eq Number
Ord)

-- | The term in first-order logic extended with arithmetic.
data Term
  = Function (Name Function) [Term]
    -- ^ Application of a function symbol. The empty list of arguments
    -- represents a constant function symbol.
  | Variable Var
    -- ^ A quantified variable.
  | Number Number
    -- ^ An integer, rational or real constant.
  | DistinctTerm DistinctObject
    -- ^ A distinct object.
  deriving (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, 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, 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 sign of first-order literals and equality.
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 Named Sign where
  name :: Sign -> Text
name = \case
    Sign
Positive -> Text
"="
    Sign
Negative -> Text
"!="

-- | The literal in first-order logic.
-- The logical tautology is represented as
-- @Predicate (Reserved (Standard Tautology)) []@
-- and the logical falsum is represented as
-- @Predicate (Reserved (Standard Falsum)) []@.
data Literal
  = Predicate (Name Predicate) [Term]
    -- ^ Application of a predicate symbol.
  | Equality Term Sign Term
    -- ^ Equality or inequality.
  deriving (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, 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, 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 clause in first-order logic - implicitly universally-quantified
-- disjunction of one or more signed literals. Semantically, a clause is allowed
-- to be empty in which case it is the logical falsum. However, the TPTP syntax
-- does not allow empty clauses, instead the unit clause @$false@ must be used.
newtype Clause = Clause (NonEmpty (Sign, Literal))
  deriving (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, 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, 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)

instance Semigroup Clause where
  Clause NonEmpty (Sign, Literal)
ls <> :: Clause -> Clause -> Clause
<> Clause NonEmpty (Sign, Literal)
ks = NonEmpty (Sign, Literal) -> Clause
Clause (NonEmpty (Sign, Literal)
ls NonEmpty (Sign, Literal)
-> NonEmpty (Sign, Literal) -> NonEmpty (Sign, Literal)
forall a. Semigroup a => a -> a -> a
<> NonEmpty (Sign, Literal)
ks)

-- | Construct a unit clause from a given signed literal.
unitClause :: (Sign, Literal) -> Clause
unitClause :: (Sign, Literal) -> Clause
unitClause (Sign, Literal)
l = NonEmpty (Sign, Literal) -> Clause
Clause ((Sign, Literal)
l (Sign, Literal) -> [(Sign, Literal)] -> NonEmpty (Sign, Literal)
forall a. a -> [a] -> NonEmpty a
:| [])

-- | A smart constructor for 'Clause'. 'clause' constructs a clause from a
-- possibly empty list of signed literals. If the provided list is empty,
-- the unit clause @$false@ is constructed instead.
clause :: [(Sign, Literal)] -> Clause
clause :: [(Sign, Literal)] -> Clause
clause [(Sign, Literal)]
ls
  | Just NonEmpty (Sign, Literal)
ls' <- [(Sign, Literal)] -> Maybe (NonEmpty (Sign, Literal))
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [(Sign, Literal)]
ls = NonEmpty (Sign, Literal) -> Clause
Clause NonEmpty (Sign, Literal)
ls'
  | Bool
otherwise = (Sign, Literal) -> Clause
unitClause (Sign
Positive, Literal
falsum)
  where
    falsum :: Literal
falsum = Name Predicate -> [Term] -> Literal
Predicate (Reserved Predicate -> Name Predicate
forall s. Reserved s -> Name s
Reserved (Predicate -> Reserved Predicate
forall s. s -> Reserved s
Standard Predicate
Falsum)) []

-- | 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)

instance Named Quantifier where
  name :: Quantifier -> Text
name = \case
    Quantifier
Forall -> Text
"!"
    Quantifier
Exists -> Text
"?"

-- | The connective in full first-order logic.
data Connective
  = Conjunction         -- ^ @&@.
  | Disjunction         -- ^ @|@.
  | Implication         -- ^ @=>@.
  | Equivalence         -- ^ @<=>@.
  | ExclusiveOr         -- ^ @<~>@ - XOR.
  | NegatedConjunction  -- ^ @~&@ - NAND.
  | NegatedDisjunction  -- ^ @~|@ - NOR.
  | ReversedImplication -- ^ @<=@.
  deriving (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, 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, 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)

-- | Check associativity of a given connective.
--
-- >>> isAssociative Implication
-- False
--
-- >>> isAssociative Conjunction
-- True
isAssociative :: Connective -> Bool
isAssociative :: Connective -> Bool
isAssociative = \case
  Connective
Conjunction -> Bool
True
  Connective
Disjunction -> Bool
True
  Connective
Implication -> Bool
False
  Connective
Equivalence -> Bool
False
  Connective
ExclusiveOr -> Bool
False
  Connective
NegatedConjunction  -> Bool
False
  Connective
NegatedDisjunction  -> Bool
False
  Connective
ReversedImplication -> Bool
False

instance Named Connective where
  name :: Connective -> Text
name = \case
    Connective
Conjunction -> Text
"&"
    Connective
Disjunction -> Text
"|"
    Connective
Implication -> Text
"=>"
    Connective
Equivalence -> Text
"<=>"
    Connective
ExclusiveOr -> Text
"<~>"
    Connective
NegatedConjunction  -> Text
"~&"
    Connective
NegatedDisjunction  -> Text
"~|"
    Connective
ReversedImplication -> Text
"<="

-- | The formula in sorted or unsorted first-order logic.
-- Syntactically, the difference between sorted and unsorted formulas is that
-- quantified variables in the former might be annotated with their respective
-- sorts. The type parameter @s@ represents the sort annotation - it is empty
-- for unsorted logic and non-empty for sorted logic.
data FirstOrder s
  = Atomic Literal
  | Negated (FirstOrder s)
  | Connected (FirstOrder s) Connective (FirstOrder s)
  | Quantified Quantifier (NonEmpty (Var, s)) (FirstOrder s)
  deriving (FirstOrder s -> FirstOrder s -> Bool
(FirstOrder s -> FirstOrder s -> Bool)
-> (FirstOrder s -> FirstOrder s -> Bool) -> Eq (FirstOrder s)
forall s. Eq s => FirstOrder s -> FirstOrder s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FirstOrder s -> FirstOrder s -> Bool
$c/= :: forall s. Eq s => FirstOrder s -> FirstOrder s -> Bool
== :: FirstOrder s -> FirstOrder s -> Bool
$c== :: forall s. Eq s => FirstOrder s -> FirstOrder s -> Bool
Eq, Int -> FirstOrder s -> ShowS
[FirstOrder s] -> ShowS
FirstOrder s -> String
(Int -> FirstOrder s -> ShowS)
-> (FirstOrder s -> String)
-> ([FirstOrder s] -> ShowS)
-> Show (FirstOrder s)
forall s. Show s => Int -> FirstOrder s -> ShowS
forall s. Show s => [FirstOrder s] -> ShowS
forall s. Show s => FirstOrder s -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FirstOrder s] -> ShowS
$cshowList :: forall s. Show s => [FirstOrder s] -> ShowS
show :: FirstOrder s -> String
$cshow :: forall s. Show s => FirstOrder s -> String
showsPrec :: Int -> FirstOrder s -> ShowS
$cshowsPrec :: forall s. Show s => Int -> FirstOrder s -> ShowS
Show, Eq (FirstOrder s)
Eq (FirstOrder s)
-> (FirstOrder s -> FirstOrder s -> Ordering)
-> (FirstOrder s -> FirstOrder s -> Bool)
-> (FirstOrder s -> FirstOrder s -> Bool)
-> (FirstOrder s -> FirstOrder s -> Bool)
-> (FirstOrder s -> FirstOrder s -> Bool)
-> (FirstOrder s -> FirstOrder s -> FirstOrder s)
-> (FirstOrder s -> FirstOrder s -> FirstOrder s)
-> Ord (FirstOrder s)
FirstOrder s -> FirstOrder s -> Bool
FirstOrder s -> FirstOrder s -> Ordering
FirstOrder s -> FirstOrder s -> FirstOrder s
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 s. Ord s => Eq (FirstOrder s)
forall s. Ord s => FirstOrder s -> FirstOrder s -> Bool
forall s. Ord s => FirstOrder s -> FirstOrder s -> Ordering
forall s. Ord s => FirstOrder s -> FirstOrder s -> FirstOrder s
min :: FirstOrder s -> FirstOrder s -> FirstOrder s
$cmin :: forall s. Ord s => FirstOrder s -> FirstOrder s -> FirstOrder s
max :: FirstOrder s -> FirstOrder s -> FirstOrder s
$cmax :: forall s. Ord s => FirstOrder s -> FirstOrder s -> FirstOrder s
>= :: FirstOrder s -> FirstOrder s -> Bool
$c>= :: forall s. Ord s => FirstOrder s -> FirstOrder s -> Bool
> :: FirstOrder s -> FirstOrder s -> Bool
$c> :: forall s. Ord s => FirstOrder s -> FirstOrder s -> Bool
<= :: FirstOrder s -> FirstOrder s -> Bool
$c<= :: forall s. Ord s => FirstOrder s -> FirstOrder s -> Bool
< :: FirstOrder s -> FirstOrder s -> Bool
$c< :: forall s. Ord s => FirstOrder s -> FirstOrder s -> Bool
compare :: FirstOrder s -> FirstOrder s -> Ordering
$ccompare :: forall s. Ord s => FirstOrder s -> FirstOrder s -> Ordering
$cp1Ord :: forall s. Ord s => Eq (FirstOrder s)
Ord, a -> FirstOrder b -> FirstOrder a
(a -> b) -> FirstOrder a -> FirstOrder b
(forall a b. (a -> b) -> FirstOrder a -> FirstOrder b)
-> (forall a b. a -> FirstOrder b -> FirstOrder a)
-> Functor FirstOrder
forall a b. a -> FirstOrder b -> FirstOrder a
forall a b. (a -> b) -> FirstOrder a -> FirstOrder b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> FirstOrder b -> FirstOrder a
$c<$ :: forall a b. a -> FirstOrder b -> FirstOrder a
fmap :: (a -> b) -> FirstOrder a -> FirstOrder b
$cfmap :: forall a b. (a -> b) -> FirstOrder a -> FirstOrder b
Functor, Functor FirstOrder
Foldable FirstOrder
Functor FirstOrder
-> Foldable FirstOrder
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> FirstOrder a -> f (FirstOrder b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    FirstOrder (f a) -> f (FirstOrder a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> FirstOrder a -> m (FirstOrder b))
-> (forall (m :: * -> *) a.
    Monad m =>
    FirstOrder (m a) -> m (FirstOrder a))
-> Traversable FirstOrder
(a -> f b) -> FirstOrder a -> f (FirstOrder 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 =>
FirstOrder (m a) -> m (FirstOrder a)
forall (f :: * -> *) a.
Applicative f =>
FirstOrder (f a) -> f (FirstOrder a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FirstOrder a -> m (FirstOrder b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FirstOrder a -> f (FirstOrder b)
sequence :: FirstOrder (m a) -> m (FirstOrder a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
FirstOrder (m a) -> m (FirstOrder a)
mapM :: (a -> m b) -> FirstOrder a -> m (FirstOrder b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FirstOrder a -> m (FirstOrder b)
sequenceA :: FirstOrder (f a) -> f (FirstOrder a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
FirstOrder (f a) -> f (FirstOrder a)
traverse :: (a -> f b) -> FirstOrder a -> f (FirstOrder b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FirstOrder a -> f (FirstOrder b)
$cp2Traversable :: Foldable FirstOrder
$cp1Traversable :: Functor FirstOrder
Traversable, FirstOrder a -> Bool
(a -> m) -> FirstOrder a -> m
(a -> b -> b) -> b -> FirstOrder a -> b
(forall m. Monoid m => FirstOrder m -> m)
-> (forall m a. Monoid m => (a -> m) -> FirstOrder a -> m)
-> (forall m a. Monoid m => (a -> m) -> FirstOrder a -> m)
-> (forall a b. (a -> b -> b) -> b -> FirstOrder a -> b)
-> (forall a b. (a -> b -> b) -> b -> FirstOrder a -> b)
-> (forall b a. (b -> a -> b) -> b -> FirstOrder a -> b)
-> (forall b a. (b -> a -> b) -> b -> FirstOrder a -> b)
-> (forall a. (a -> a -> a) -> FirstOrder a -> a)
-> (forall a. (a -> a -> a) -> FirstOrder a -> a)
-> (forall a. FirstOrder a -> [a])
-> (forall a. FirstOrder a -> Bool)
-> (forall a. FirstOrder a -> Int)
-> (forall a. Eq a => a -> FirstOrder a -> Bool)
-> (forall a. Ord a => FirstOrder a -> a)
-> (forall a. Ord a => FirstOrder a -> a)
-> (forall a. Num a => FirstOrder a -> a)
-> (forall a. Num a => FirstOrder a -> a)
-> Foldable FirstOrder
forall a. Eq a => a -> FirstOrder a -> Bool
forall a. Num a => FirstOrder a -> a
forall a. Ord a => FirstOrder a -> a
forall m. Monoid m => FirstOrder m -> m
forall a. FirstOrder a -> Bool
forall a. FirstOrder a -> Int
forall a. FirstOrder a -> [a]
forall a. (a -> a -> a) -> FirstOrder a -> a
forall m a. Monoid m => (a -> m) -> FirstOrder a -> m
forall b a. (b -> a -> b) -> b -> FirstOrder a -> b
forall a b. (a -> b -> b) -> b -> FirstOrder 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 :: FirstOrder a -> a
$cproduct :: forall a. Num a => FirstOrder a -> a
sum :: FirstOrder a -> a
$csum :: forall a. Num a => FirstOrder a -> a
minimum :: FirstOrder a -> a
$cminimum :: forall a. Ord a => FirstOrder a -> a
maximum :: FirstOrder a -> a
$cmaximum :: forall a. Ord a => FirstOrder a -> a
elem :: a -> FirstOrder a -> Bool
$celem :: forall a. Eq a => a -> FirstOrder a -> Bool
length :: FirstOrder a -> Int
$clength :: forall a. FirstOrder a -> Int
null :: FirstOrder a -> Bool
$cnull :: forall a. FirstOrder a -> Bool
toList :: FirstOrder a -> [a]
$ctoList :: forall a. FirstOrder a -> [a]
foldl1 :: (a -> a -> a) -> FirstOrder a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> FirstOrder a -> a
foldr1 :: (a -> a -> a) -> FirstOrder a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> FirstOrder a -> a
foldl' :: (b -> a -> b) -> b -> FirstOrder a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> FirstOrder a -> b
foldl :: (b -> a -> b) -> b -> FirstOrder a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> FirstOrder a -> b
foldr' :: (a -> b -> b) -> b -> FirstOrder a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> FirstOrder a -> b
foldr :: (a -> b -> b) -> b -> FirstOrder a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> FirstOrder a -> b
foldMap' :: (a -> m) -> FirstOrder a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> FirstOrder a -> m
foldMap :: (a -> m) -> FirstOrder a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> FirstOrder a -> m
fold :: FirstOrder m -> m
$cfold :: forall m. Monoid m => FirstOrder m -> m
Foldable)

-- | A smart constructor for 'Quantified' - constructs a quantified first-order
-- formula with a possibly empty list of variables under the quantifier. If the
-- provided list is empty, the underlying formula is returned instead.
quantified :: Quantifier -> [(Var, s)] -> FirstOrder s -> FirstOrder s
quantified :: Quantifier -> [(Var, s)] -> FirstOrder s -> FirstOrder s
quantified Quantifier
q [(Var, s)]
vs FirstOrder s
f
  | Just NonEmpty (Var, s)
vs' <- [(Var, s)] -> Maybe (NonEmpty (Var, s))
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [(Var, s)]
vs = Quantifier -> NonEmpty (Var, s) -> FirstOrder s -> FirstOrder s
forall s.
Quantifier -> NonEmpty (Var, s) -> FirstOrder s -> FirstOrder s
Quantified Quantifier
q NonEmpty (Var, s)
vs' FirstOrder s
f
  | Bool
otherwise = FirstOrder s
f

-- | The (empty) sort annotation in unsorted first-order logic.
newtype Unsorted = Unsorted ()
  deriving (Unsorted -> Unsorted -> Bool
(Unsorted -> Unsorted -> Bool)
-> (Unsorted -> Unsorted -> Bool) -> Eq Unsorted
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Unsorted -> Unsorted -> Bool
$c/= :: Unsorted -> Unsorted -> Bool
== :: Unsorted -> Unsorted -> Bool
$c== :: Unsorted -> Unsorted -> Bool
Eq, Int -> Unsorted -> ShowS
[Unsorted] -> ShowS
Unsorted -> String
(Int -> Unsorted -> ShowS)
-> (Unsorted -> String) -> ([Unsorted] -> ShowS) -> Show Unsorted
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Unsorted] -> ShowS
$cshowList :: [Unsorted] -> ShowS
show :: Unsorted -> String
$cshow :: Unsorted -> String
showsPrec :: Int -> Unsorted -> ShowS
$cshowsPrec :: Int -> Unsorted -> ShowS
Show, Eq Unsorted
Eq Unsorted
-> (Unsorted -> Unsorted -> Ordering)
-> (Unsorted -> Unsorted -> Bool)
-> (Unsorted -> Unsorted -> Bool)
-> (Unsorted -> Unsorted -> Bool)
-> (Unsorted -> Unsorted -> Bool)
-> (Unsorted -> Unsorted -> Unsorted)
-> (Unsorted -> Unsorted -> Unsorted)
-> Ord Unsorted
Unsorted -> Unsorted -> Bool
Unsorted -> Unsorted -> Ordering
Unsorted -> Unsorted -> Unsorted
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 :: Unsorted -> Unsorted -> Unsorted
$cmin :: Unsorted -> Unsorted -> Unsorted
max :: Unsorted -> Unsorted -> Unsorted
$cmax :: Unsorted -> Unsorted -> Unsorted
>= :: Unsorted -> Unsorted -> Bool
$c>= :: Unsorted -> Unsorted -> Bool
> :: Unsorted -> Unsorted -> Bool
$c> :: Unsorted -> Unsorted -> Bool
<= :: Unsorted -> Unsorted -> Bool
$c<= :: Unsorted -> Unsorted -> Bool
< :: Unsorted -> Unsorted -> Bool
$c< :: Unsorted -> Unsorted -> Bool
compare :: Unsorted -> Unsorted -> Ordering
$ccompare :: Unsorted -> Unsorted -> Ordering
$cp1Ord :: Eq Unsorted
Ord)

-- | The formula in unsorted first-order logic.
type UnsortedFirstOrder = FirstOrder Unsorted

-- | The sort annotation in sorted first-order logic. The TPTP language allows
-- a sort annotation to be omitted, in such case the sort of the variable is
-- assumed to be @$i@.
newtype Sorted s = Sorted (Maybe s)
  deriving (Sorted s -> Sorted s -> Bool
(Sorted s -> Sorted s -> Bool)
-> (Sorted s -> Sorted s -> Bool) -> Eq (Sorted s)
forall s. Eq s => Sorted s -> Sorted s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sorted s -> Sorted s -> Bool
$c/= :: forall s. Eq s => Sorted s -> Sorted s -> Bool
== :: Sorted s -> Sorted s -> Bool
$c== :: forall s. Eq s => Sorted s -> Sorted s -> Bool
Eq, Int -> Sorted s -> ShowS
[Sorted s] -> ShowS
Sorted s -> String
(Int -> Sorted s -> ShowS)
-> (Sorted s -> String) -> ([Sorted s] -> ShowS) -> Show (Sorted s)
forall s. Show s => Int -> Sorted s -> ShowS
forall s. Show s => [Sorted s] -> ShowS
forall s. Show s => Sorted s -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sorted s] -> ShowS
$cshowList :: forall s. Show s => [Sorted s] -> ShowS
show :: Sorted s -> String
$cshow :: forall s. Show s => Sorted s -> String
showsPrec :: Int -> Sorted s -> ShowS
$cshowsPrec :: forall s. Show s => Int -> Sorted s -> ShowS
Show, Eq (Sorted s)
Eq (Sorted s)
-> (Sorted s -> Sorted s -> Ordering)
-> (Sorted s -> Sorted s -> Bool)
-> (Sorted s -> Sorted s -> Bool)
-> (Sorted s -> Sorted s -> Bool)
-> (Sorted s -> Sorted s -> Bool)
-> (Sorted s -> Sorted s -> Sorted s)
-> (Sorted s -> Sorted s -> Sorted s)
-> Ord (Sorted s)
Sorted s -> Sorted s -> Bool
Sorted s -> Sorted s -> Ordering
Sorted s -> Sorted s -> Sorted s
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 s. Ord s => Eq (Sorted s)
forall s. Ord s => Sorted s -> Sorted s -> Bool
forall s. Ord s => Sorted s -> Sorted s -> Ordering
forall s. Ord s => Sorted s -> Sorted s -> Sorted s
min :: Sorted s -> Sorted s -> Sorted s
$cmin :: forall s. Ord s => Sorted s -> Sorted s -> Sorted s
max :: Sorted s -> Sorted s -> Sorted s
$cmax :: forall s. Ord s => Sorted s -> Sorted s -> Sorted s
>= :: Sorted s -> Sorted s -> Bool
$c>= :: forall s. Ord s => Sorted s -> Sorted s -> Bool
> :: Sorted s -> Sorted s -> Bool
$c> :: forall s. Ord s => Sorted s -> Sorted s -> Bool
<= :: Sorted s -> Sorted s -> Bool
$c<= :: forall s. Ord s => Sorted s -> Sorted s -> Bool
< :: Sorted s -> Sorted s -> Bool
$c< :: forall s. Ord s => Sorted s -> Sorted s -> Bool
compare :: Sorted s -> Sorted s -> Ordering
$ccompare :: forall s. Ord s => Sorted s -> Sorted s -> Ordering
$cp1Ord :: forall s. Ord s => Eq (Sorted s)
Ord, a -> Sorted b -> Sorted a
(a -> b) -> Sorted a -> Sorted b
(forall a b. (a -> b) -> Sorted a -> Sorted b)
-> (forall a b. a -> Sorted b -> Sorted a) -> Functor Sorted
forall a b. a -> Sorted b -> Sorted a
forall a b. (a -> b) -> Sorted a -> Sorted b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Sorted b -> Sorted a
$c<$ :: forall a b. a -> Sorted b -> Sorted a
fmap :: (a -> b) -> Sorted a -> Sorted b
$cfmap :: forall a b. (a -> b) -> Sorted a -> Sorted b
Functor, Functor Sorted
Foldable Sorted
Functor Sorted
-> Foldable Sorted
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Sorted a -> f (Sorted b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Sorted (f a) -> f (Sorted a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Sorted a -> m (Sorted b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Sorted (m a) -> m (Sorted a))
-> Traversable Sorted
(a -> f b) -> Sorted a -> f (Sorted 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 => Sorted (m a) -> m (Sorted a)
forall (f :: * -> *) a.
Applicative f =>
Sorted (f a) -> f (Sorted a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Sorted a -> m (Sorted b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Sorted a -> f (Sorted b)
sequence :: Sorted (m a) -> m (Sorted a)
$csequence :: forall (m :: * -> *) a. Monad m => Sorted (m a) -> m (Sorted a)
mapM :: (a -> m b) -> Sorted a -> m (Sorted b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Sorted a -> m (Sorted b)
sequenceA :: Sorted (f a) -> f (Sorted a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Sorted (f a) -> f (Sorted a)
traverse :: (a -> f b) -> Sorted a -> f (Sorted b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Sorted a -> f (Sorted b)
$cp2Traversable :: Foldable Sorted
$cp1Traversable :: Functor Sorted
Traversable, a -> Sorted a -> Bool
Sorted m -> m
Sorted a -> [a]
Sorted a -> Bool
Sorted a -> Int
Sorted a -> a
Sorted a -> a
Sorted a -> a
Sorted a -> a
(a -> m) -> Sorted a -> m
(a -> m) -> Sorted a -> m
(a -> b -> b) -> b -> Sorted a -> b
(a -> b -> b) -> b -> Sorted a -> b
(b -> a -> b) -> b -> Sorted a -> b
(b -> a -> b) -> b -> Sorted a -> b
(a -> a -> a) -> Sorted a -> a
(a -> a -> a) -> Sorted a -> a
(forall m. Monoid m => Sorted m -> m)
-> (forall m a. Monoid m => (a -> m) -> Sorted a -> m)
-> (forall m a. Monoid m => (a -> m) -> Sorted a -> m)
-> (forall a b. (a -> b -> b) -> b -> Sorted a -> b)
-> (forall a b. (a -> b -> b) -> b -> Sorted a -> b)
-> (forall b a. (b -> a -> b) -> b -> Sorted a -> b)
-> (forall b a. (b -> a -> b) -> b -> Sorted a -> b)
-> (forall a. (a -> a -> a) -> Sorted a -> a)
-> (forall a. (a -> a -> a) -> Sorted a -> a)
-> (forall a. Sorted a -> [a])
-> (forall a. Sorted a -> Bool)
-> (forall a. Sorted a -> Int)
-> (forall a. Eq a => a -> Sorted a -> Bool)
-> (forall a. Ord a => Sorted a -> a)
-> (forall a. Ord a => Sorted a -> a)
-> (forall a. Num a => Sorted a -> a)
-> (forall a. Num a => Sorted a -> a)
-> Foldable Sorted
forall a. Eq a => a -> Sorted a -> Bool
forall a. Num a => Sorted a -> a
forall a. Ord a => Sorted a -> a
forall m. Monoid m => Sorted m -> m
forall a. Sorted a -> Bool
forall a. Sorted a -> Int
forall a. Sorted a -> [a]
forall a. (a -> a -> a) -> Sorted a -> a
forall m a. Monoid m => (a -> m) -> Sorted a -> m
forall b a. (b -> a -> b) -> b -> Sorted a -> b
forall a b. (a -> b -> b) -> b -> Sorted 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 :: Sorted a -> a
$cproduct :: forall a. Num a => Sorted a -> a
sum :: Sorted a -> a
$csum :: forall a. Num a => Sorted a -> a
minimum :: Sorted a -> a
$cminimum :: forall a. Ord a => Sorted a -> a
maximum :: Sorted a -> a
$cmaximum :: forall a. Ord a => Sorted a -> a
elem :: a -> Sorted a -> Bool
$celem :: forall a. Eq a => a -> Sorted a -> Bool
length :: Sorted a -> Int
$clength :: forall a. Sorted a -> Int
null :: Sorted a -> Bool
$cnull :: forall a. Sorted a -> Bool
toList :: Sorted a -> [a]
$ctoList :: forall a. Sorted a -> [a]
foldl1 :: (a -> a -> a) -> Sorted a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Sorted a -> a
foldr1 :: (a -> a -> a) -> Sorted a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Sorted a -> a
foldl' :: (b -> a -> b) -> b -> Sorted a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Sorted a -> b
foldl :: (b -> a -> b) -> b -> Sorted a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Sorted a -> b
foldr' :: (a -> b -> b) -> b -> Sorted a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Sorted a -> b
foldr :: (a -> b -> b) -> b -> Sorted a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Sorted a -> b
foldMap' :: (a -> m) -> Sorted a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Sorted a -> m
foldMap :: (a -> m) -> Sorted a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Sorted a -> m
fold :: Sorted m -> m
$cfold :: forall m. Monoid m => Sorted m -> m
Foldable)

-- | An alias for 'MonomorphicFirstOrder'.
type SortedFirstOrder = MonomorphicFirstOrder

-- | The formula in sorted monomorphic first-order logic.
type MonomorphicFirstOrder = FirstOrder (Sorted (Name Sort))

-- | Convert a formula in unsorted first-order logic to a formula in sorted
-- monomorphic first-order logic trivially by omitting the sort annotations
-- in all of its quantifiers. This function always succeeds.
sortFirstOrder :: UnsortedFirstOrder -> SortedFirstOrder
sortFirstOrder :: UnsortedFirstOrder -> SortedFirstOrder
sortFirstOrder = (Unsorted -> Sorted (Name Sort))
-> UnsortedFirstOrder -> SortedFirstOrder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Unsorted -> Sorted (Name Sort)
forall p s. p -> Sorted s
omit where omit :: p -> Sorted s
omit p
_ = Maybe s -> Sorted s
forall s. Maybe s -> Sorted s
Sorted Maybe s
forall a. Maybe a
Nothing

-- | Attempt to erase the sort annotations in a sorted monomorphic first-order
-- formula. This function succeeds iff each of the quantifiers omits the sorts
-- of its variables.
unsortFirstOrder :: MonomorphicFirstOrder -> Maybe UnsortedFirstOrder
unsortFirstOrder :: SortedFirstOrder -> Maybe UnsortedFirstOrder
unsortFirstOrder = (Sorted (Name Sort) -> Maybe Unsorted)
-> SortedFirstOrder -> Maybe UnsortedFirstOrder
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((Sorted (Name Sort) -> Maybe Unsorted)
 -> SortedFirstOrder -> Maybe UnsortedFirstOrder)
-> (Sorted (Name Sort) -> Maybe Unsorted)
-> SortedFirstOrder
-> Maybe UnsortedFirstOrder
forall a b. (a -> b) -> a -> b
$ \case
  Sorted Maybe (Name Sort)
Nothing -> Unsorted -> Maybe Unsorted
forall a. a -> Maybe a
Just (() -> Unsorted
Unsorted ())
  Sorted Just{}  -> Maybe Unsorted
forall a. Maybe a
Nothing

-- | The marker of quantified sort.
newtype QuantifiedSort = QuantifiedSort ()
  deriving (QuantifiedSort -> QuantifiedSort -> Bool
(QuantifiedSort -> QuantifiedSort -> Bool)
-> (QuantifiedSort -> QuantifiedSort -> Bool) -> Eq QuantifiedSort
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: QuantifiedSort -> QuantifiedSort -> Bool
$c/= :: QuantifiedSort -> QuantifiedSort -> Bool
== :: QuantifiedSort -> QuantifiedSort -> Bool
$c== :: QuantifiedSort -> QuantifiedSort -> Bool
Eq, Int -> QuantifiedSort -> ShowS
[QuantifiedSort] -> ShowS
QuantifiedSort -> String
(Int -> QuantifiedSort -> ShowS)
-> (QuantifiedSort -> String)
-> ([QuantifiedSort] -> ShowS)
-> Show QuantifiedSort
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [QuantifiedSort] -> ShowS
$cshowList :: [QuantifiedSort] -> ShowS
show :: QuantifiedSort -> String
$cshow :: QuantifiedSort -> String
showsPrec :: Int -> QuantifiedSort -> ShowS
$cshowsPrec :: Int -> QuantifiedSort -> ShowS
Show, Eq QuantifiedSort
Eq QuantifiedSort
-> (QuantifiedSort -> QuantifiedSort -> Ordering)
-> (QuantifiedSort -> QuantifiedSort -> Bool)
-> (QuantifiedSort -> QuantifiedSort -> Bool)
-> (QuantifiedSort -> QuantifiedSort -> Bool)
-> (QuantifiedSort -> QuantifiedSort -> Bool)
-> (QuantifiedSort -> QuantifiedSort -> QuantifiedSort)
-> (QuantifiedSort -> QuantifiedSort -> QuantifiedSort)
-> Ord QuantifiedSort
QuantifiedSort -> QuantifiedSort -> Bool
QuantifiedSort -> QuantifiedSort -> Ordering
QuantifiedSort -> QuantifiedSort -> QuantifiedSort
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 :: QuantifiedSort -> QuantifiedSort -> QuantifiedSort
$cmin :: QuantifiedSort -> QuantifiedSort -> QuantifiedSort
max :: QuantifiedSort -> QuantifiedSort -> QuantifiedSort
$cmax :: QuantifiedSort -> QuantifiedSort -> QuantifiedSort
>= :: QuantifiedSort -> QuantifiedSort -> Bool
$c>= :: QuantifiedSort -> QuantifiedSort -> Bool
> :: QuantifiedSort -> QuantifiedSort -> Bool
$c> :: QuantifiedSort -> QuantifiedSort -> Bool
<= :: QuantifiedSort -> QuantifiedSort -> Bool
$c<= :: QuantifiedSort -> QuantifiedSort -> Bool
< :: QuantifiedSort -> QuantifiedSort -> Bool
$c< :: QuantifiedSort -> QuantifiedSort -> Bool
compare :: QuantifiedSort -> QuantifiedSort -> Ordering
$ccompare :: QuantifiedSort -> QuantifiedSort -> Ordering
$cp1Ord :: Eq QuantifiedSort
Ord)

-- | The formula in sorted polymorphic first-order logic.
type PolymorphicFirstOrder = FirstOrder (Sorted (Either QuantifiedSort TFF1Sort))

-- | Polymorphize a sorted monomorphic first-order formula.
-- This function always succeeds.
polymorphizeFirstOrder :: MonomorphicFirstOrder -> PolymorphicFirstOrder
polymorphizeFirstOrder :: SortedFirstOrder -> PolymorphicFirstOrder
polymorphizeFirstOrder = (Sorted (Name Sort) -> Sorted (Either QuantifiedSort TFF1Sort))
-> SortedFirstOrder -> PolymorphicFirstOrder
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name Sort -> Either QuantifiedSort TFF1Sort)
-> Sorted (Name Sort) -> Sorted (Either QuantifiedSort TFF1Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name Sort -> Either QuantifiedSort TFF1Sort
forall a. Name Sort -> Either a TFF1Sort
polymorphize)
  where polymorphize :: Name Sort -> Either a TFF1Sort
polymorphize Name Sort
s = TFF1Sort -> Either a TFF1Sort
forall a b. b -> Either a b
Right (Name Sort -> [TFF1Sort] -> TFF1Sort
TFF1Sort Name Sort
s [])

-- | Attempt to monomorphize a polymorphic sorted first-order formula.
-- This function succeeds iff each of the quantifiers only uses sort
-- constructors with zero arity and there are no quantified sorts.
monomorphizeFirstOrder :: PolymorphicFirstOrder -> Maybe MonomorphicFirstOrder
monomorphizeFirstOrder :: PolymorphicFirstOrder -> Maybe SortedFirstOrder
monomorphizeFirstOrder = (Sorted (Either QuantifiedSort TFF1Sort)
 -> Maybe (Sorted (Name Sort)))
-> PolymorphicFirstOrder -> Maybe SortedFirstOrder
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((Either QuantifiedSort TFF1Sort -> Maybe (Name Sort))
-> Sorted (Either QuantifiedSort TFF1Sort)
-> Maybe (Sorted (Name Sort))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Either QuantifiedSort TFF1Sort -> Maybe (Name Sort)
forall b. Either b TFF1Sort -> Maybe (Name Sort)
monomorphize)
  where monomorphize :: Either b TFF1Sort -> Maybe (Name Sort)
monomorphize = (b -> Maybe (Name Sort))
-> (TFF1Sort -> Maybe (Name Sort))
-> Either b TFF1Sort
-> Maybe (Name Sort)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe (Name Sort) -> b -> Maybe (Name Sort)
forall a b. a -> b -> a
const Maybe (Name Sort)
forall a. Maybe a
Nothing) TFF1Sort -> Maybe (Name Sort)
monomorphizeTFF1Sort


-- * Units

-- | The formula in either of the supported TPTP languages.
data Formula
  = CNF Clause
  | FOF UnsortedFirstOrder
  | TFF0 MonomorphicFirstOrder
  | TFF1 PolymorphicFirstOrder
  deriving (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, 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, 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)

-- | The TPTP language of a given TPTP formula.
formulaLanguage :: Formula -> Language
formulaLanguage :: Formula -> Language
formulaLanguage = \case
  CNF{}  -> Language
CNF_
  FOF{}  -> Language
FOF_
  TFF0{} -> Language
TFF_
  TFF1{} -> Language
TFF_

-- | The predefined role of a formula in a derivation. Theorem provers might
-- introduce other roles.
data Role
  = Axiom
  | Hypothesis
  | Definition
  | Assumption
  | Lemma
  | Theorem
  | Corollary
  | Conjecture
  | NegatedConjecture
  | Plain
  | FiDomain
  | FiFunctors
  | FiPredicates
  | Unknown
  deriving (Role -> Role -> Bool
(Role -> Role -> Bool) -> (Role -> Role -> Bool) -> Eq Role
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Role -> Role -> Bool
$c/= :: Role -> Role -> Bool
== :: Role -> Role -> Bool
$c== :: Role -> Role -> Bool
Eq, Int -> Role -> ShowS
[Role] -> ShowS
Role -> String
(Int -> Role -> ShowS)
-> (Role -> String) -> ([Role] -> ShowS) -> Show Role
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Role] -> ShowS
$cshowList :: [Role] -> ShowS
show :: Role -> String
$cshow :: Role -> String
showsPrec :: Int -> Role -> ShowS
$cshowsPrec :: Int -> Role -> ShowS
Show, Eq Role
Eq Role
-> (Role -> Role -> Ordering)
-> (Role -> Role -> Bool)
-> (Role -> Role -> Bool)
-> (Role -> Role -> Bool)
-> (Role -> Role -> Bool)
-> (Role -> Role -> Role)
-> (Role -> Role -> Role)
-> Ord Role
Role -> Role -> Bool
Role -> Role -> Ordering
Role -> Role -> Role
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 :: Role -> Role -> Role
$cmin :: Role -> Role -> Role
max :: Role -> Role -> Role
$cmax :: Role -> Role -> Role
>= :: Role -> Role -> Bool
$c>= :: Role -> Role -> Bool
> :: Role -> Role -> Bool
$c> :: Role -> Role -> Bool
<= :: Role -> Role -> Bool
$c<= :: Role -> Role -> Bool
< :: Role -> Role -> Bool
$c< :: Role -> Role -> Bool
compare :: Role -> Role -> Ordering
$ccompare :: Role -> Role -> Ordering
$cp1Ord :: Eq Role
Ord, Int -> Role
Role -> Int
Role -> [Role]
Role -> Role
Role -> Role -> [Role]
Role -> Role -> Role -> [Role]
(Role -> Role)
-> (Role -> Role)
-> (Int -> Role)
-> (Role -> Int)
-> (Role -> [Role])
-> (Role -> Role -> [Role])
-> (Role -> Role -> [Role])
-> (Role -> Role -> Role -> [Role])
-> Enum Role
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 :: Role -> Role -> Role -> [Role]
$cenumFromThenTo :: Role -> Role -> Role -> [Role]
enumFromTo :: Role -> Role -> [Role]
$cenumFromTo :: Role -> Role -> [Role]
enumFromThen :: Role -> Role -> [Role]
$cenumFromThen :: Role -> Role -> [Role]
enumFrom :: Role -> [Role]
$cenumFrom :: Role -> [Role]
fromEnum :: Role -> Int
$cfromEnum :: Role -> Int
toEnum :: Int -> Role
$ctoEnum :: Int -> Role
pred :: Role -> Role
$cpred :: Role -> Role
succ :: Role -> Role
$csucc :: Role -> Role
Enum, Role
Role -> Role -> Bounded Role
forall a. a -> a -> Bounded a
maxBound :: Role
$cmaxBound :: Role
minBound :: Role
$cminBound :: Role
Bounded)

instance Named Role where
  name :: Role -> Text
name = \case
    Role
Axiom             -> Text
"axiom"
    Role
Hypothesis        -> Text
"hypothesis"
    Role
Definition        -> Text
"definition"
    Role
Assumption        -> Text
"assumption"
    Role
Lemma             -> Text
"lemma"
    Role
Theorem           -> Text
"theorem"
    Role
Corollary         -> Text
"corollary"
    Role
Conjecture        -> Text
"conjecture"
    Role
NegatedConjecture -> Text
"negated_conjecture"
    Role
Plain             -> Text
"plain"
    Role
FiDomain          -> Text
"fi_domain"
    Role
FiFunctors        -> Text
"fi_functors"
    Role
FiPredicates      -> Text
"fi_predicates"
    Role
Unknown           -> Text
"unknown"

-- | The logical declaration.
data Declaration
  = Sort Atom Integer
  -- ^ Introduction of a sort contructor. The non-negative integer argument
  -- denotes the arity of the constructor. A constructor with zero arity is
  -- simply a sort.
  | Typing Atom Type
  -- ^ Assignment of a type to a symbol.
  | Formula (Reserved Role) Formula
  -- ^ Logical formula marked with its role.
  deriving (Declaration -> Declaration -> Bool
(Declaration -> Declaration -> Bool)
-> (Declaration -> Declaration -> Bool) -> Eq Declaration
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Declaration -> Declaration -> Bool
$c/= :: Declaration -> Declaration -> Bool
== :: Declaration -> Declaration -> Bool
$c== :: Declaration -> Declaration -> Bool
Eq, Int -> Declaration -> ShowS
[Declaration] -> ShowS
Declaration -> String
(Int -> Declaration -> ShowS)
-> (Declaration -> String)
-> ([Declaration] -> ShowS)
-> Show Declaration
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Declaration] -> ShowS
$cshowList :: [Declaration] -> ShowS
show :: Declaration -> String
$cshow :: Declaration -> String
showsPrec :: Int -> Declaration -> ShowS
$cshowsPrec :: Int -> Declaration -> ShowS
Show, Eq Declaration
Eq Declaration
-> (Declaration -> Declaration -> Ordering)
-> (Declaration -> Declaration -> Bool)
-> (Declaration -> Declaration -> Bool)
-> (Declaration -> Declaration -> Bool)
-> (Declaration -> Declaration -> Bool)
-> (Declaration -> Declaration -> Declaration)
-> (Declaration -> Declaration -> Declaration)
-> Ord Declaration
Declaration -> Declaration -> Bool
Declaration -> Declaration -> Ordering
Declaration -> Declaration -> Declaration
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 :: Declaration -> Declaration -> Declaration
$cmin :: Declaration -> Declaration -> Declaration
max :: Declaration -> Declaration -> Declaration
$cmax :: Declaration -> Declaration -> Declaration
>= :: Declaration -> Declaration -> Bool
$c>= :: Declaration -> Declaration -> Bool
> :: Declaration -> Declaration -> Bool
$c> :: Declaration -> Declaration -> Bool
<= :: Declaration -> Declaration -> Bool
$c<= :: Declaration -> Declaration -> Bool
< :: Declaration -> Declaration -> Bool
$c< :: Declaration -> Declaration -> Bool
compare :: Declaration -> Declaration -> Ordering
$ccompare :: Declaration -> Declaration -> Ordering
$cp1Ord :: Eq Declaration
Ord)

-- | The TPTP language of a given TPTP declaration.
declarationLanguage :: Declaration -> Language
declarationLanguage :: Declaration -> Language
declarationLanguage = \case
  Sort{}      -> Language
TFF_
  Typing{}    -> Language
TFF_
  Formula Reserved Role
_ Formula
f -> Formula -> Language
formulaLanguage Formula
f

-- | The name of a unit - either an atom or an integer.
type UnitName = Either Atom Integer

-- | The unit of the TPTP input.
data Unit
  = Include Atom (Maybe (NonEmpty UnitName))
  -- ^ The @include@ statement.
  | Unit UnitName Declaration (Maybe Annotation)
  -- ^ The named and possibly annotated logical declaration.
  deriving (Unit -> Unit -> Bool
(Unit -> Unit -> Bool) -> (Unit -> Unit -> Bool) -> Eq Unit
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Unit -> Unit -> Bool
$c/= :: Unit -> Unit -> Bool
== :: Unit -> Unit -> Bool
$c== :: Unit -> Unit -> Bool
Eq, Int -> Unit -> ShowS
[Unit] -> ShowS
Unit -> String
(Int -> Unit -> ShowS)
-> (Unit -> String) -> ([Unit] -> ShowS) -> Show Unit
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Unit] -> ShowS
$cshowList :: [Unit] -> ShowS
show :: Unit -> String
$cshow :: Unit -> String
showsPrec :: Int -> Unit -> ShowS
$cshowsPrec :: Int -> Unit -> ShowS
Show, Eq Unit
Eq Unit
-> (Unit -> Unit -> Ordering)
-> (Unit -> Unit -> Bool)
-> (Unit -> Unit -> Bool)
-> (Unit -> Unit -> Bool)
-> (Unit -> Unit -> Bool)
-> (Unit -> Unit -> Unit)
-> (Unit -> Unit -> Unit)
-> Ord Unit
Unit -> Unit -> Bool
Unit -> Unit -> Ordering
Unit -> Unit -> Unit
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 :: Unit -> Unit -> Unit
$cmin :: Unit -> Unit -> Unit
max :: Unit -> Unit -> Unit
$cmax :: Unit -> Unit -> Unit
>= :: Unit -> Unit -> Bool
$c>= :: Unit -> Unit -> Bool
> :: Unit -> Unit -> Bool
$c> :: Unit -> Unit -> Bool
<= :: Unit -> Unit -> Bool
$c<= :: Unit -> Unit -> Bool
< :: Unit -> Unit -> Bool
$c< :: Unit -> Unit -> Bool
compare :: Unit -> Unit -> Ordering
$ccompare :: Unit -> Unit -> Ordering
$cp1Ord :: Eq Unit
Ord)

-- | The TPTP input - zero or more TPTP units.
newtype TPTP = TPTP {
  TPTP -> [Unit]
units :: [Unit]
} deriving (TPTP -> TPTP -> Bool
(TPTP -> TPTP -> Bool) -> (TPTP -> TPTP -> Bool) -> Eq TPTP
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TPTP -> TPTP -> Bool
$c/= :: TPTP -> TPTP -> Bool
== :: TPTP -> TPTP -> Bool
$c== :: TPTP -> TPTP -> Bool
Eq, Int -> TPTP -> ShowS
[TPTP] -> ShowS
TPTP -> String
(Int -> TPTP -> ShowS)
-> (TPTP -> String) -> ([TPTP] -> ShowS) -> Show TPTP
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TPTP] -> ShowS
$cshowList :: [TPTP] -> ShowS
show :: TPTP -> String
$cshow :: TPTP -> String
showsPrec :: Int -> TPTP -> ShowS
$cshowsPrec :: Int -> TPTP -> ShowS
Show, Eq TPTP
Eq TPTP
-> (TPTP -> TPTP -> Ordering)
-> (TPTP -> TPTP -> Bool)
-> (TPTP -> TPTP -> Bool)
-> (TPTP -> TPTP -> Bool)
-> (TPTP -> TPTP -> Bool)
-> (TPTP -> TPTP -> TPTP)
-> (TPTP -> TPTP -> TPTP)
-> Ord TPTP
TPTP -> TPTP -> Bool
TPTP -> TPTP -> Ordering
TPTP -> TPTP -> TPTP
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 :: TPTP -> TPTP -> TPTP
$cmin :: TPTP -> TPTP -> TPTP
max :: TPTP -> TPTP -> TPTP
$cmax :: TPTP -> TPTP -> TPTP
>= :: TPTP -> TPTP -> Bool
$c>= :: TPTP -> TPTP -> Bool
> :: TPTP -> TPTP -> Bool
$c> :: TPTP -> TPTP -> Bool
<= :: TPTP -> TPTP -> Bool
$c<= :: TPTP -> TPTP -> Bool
< :: TPTP -> TPTP -> Bool
$c< :: TPTP -> TPTP -> Bool
compare :: TPTP -> TPTP -> Ordering
$ccompare :: TPTP -> TPTP -> Ordering
$cp1Ord :: Eq TPTP
Ord)

instance Semigroup TPTP where
  TPTP [Unit]
us <> :: TPTP -> TPTP -> TPTP
<> TPTP [Unit]
ys = [Unit] -> TPTP
TPTP ([Unit]
us [Unit] -> [Unit] -> [Unit]
forall a. Semigroup a => a -> a -> a
<> [Unit]
ys)

instance Monoid TPTP where
  mempty :: TPTP
mempty = [Unit] -> TPTP
TPTP [Unit]
forall a. Monoid a => a
mempty
  mappend :: TPTP -> TPTP -> TPTP
mappend = TPTP -> TPTP -> TPTP
forall a. Semigroup a => a -> a -> a
(<>)

-- | The TSTP output - zero or more TSTP units, possibly annotated with the
-- status of the proof search and the resulting dataform.
data TSTP = TSTP SZS [Unit]
  deriving (TSTP -> TSTP -> Bool
(TSTP -> TSTP -> Bool) -> (TSTP -> TSTP -> Bool) -> Eq TSTP
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TSTP -> TSTP -> Bool
$c/= :: TSTP -> TSTP -> Bool
== :: TSTP -> TSTP -> Bool
$c== :: TSTP -> TSTP -> Bool
Eq, Int -> TSTP -> ShowS
[TSTP] -> ShowS
TSTP -> String
(Int -> TSTP -> ShowS)
-> (TSTP -> String) -> ([TSTP] -> ShowS) -> Show TSTP
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TSTP] -> ShowS
$cshowList :: [TSTP] -> ShowS
show :: TSTP -> String
$cshow :: TSTP -> String
showsPrec :: Int -> TSTP -> ShowS
$cshowsPrec :: Int -> TSTP -> ShowS
Show, Eq TSTP
Eq TSTP
-> (TSTP -> TSTP -> Ordering)
-> (TSTP -> TSTP -> Bool)
-> (TSTP -> TSTP -> Bool)
-> (TSTP -> TSTP -> Bool)
-> (TSTP -> TSTP -> Bool)
-> (TSTP -> TSTP -> TSTP)
-> (TSTP -> TSTP -> TSTP)
-> Ord TSTP
TSTP -> TSTP -> Bool
TSTP -> TSTP -> Ordering
TSTP -> TSTP -> TSTP
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 :: TSTP -> TSTP -> TSTP
$cmin :: TSTP -> TSTP -> TSTP
max :: TSTP -> TSTP -> TSTP
$cmax :: TSTP -> TSTP -> TSTP
>= :: TSTP -> TSTP -> Bool
$c>= :: TSTP -> TSTP -> Bool
> :: TSTP -> TSTP -> Bool
$c> :: TSTP -> TSTP -> Bool
<= :: TSTP -> TSTP -> Bool
$c<= :: TSTP -> TSTP -> Bool
< :: TSTP -> TSTP -> Bool
$c< :: TSTP -> TSTP -> Bool
compare :: TSTP -> TSTP -> Ordering
$ccompare :: TSTP -> TSTP -> Ordering
$cp1Ord :: Eq TSTP
Ord)


-- * Annotations

-- | The marking of the way a formula is introduced in a TSTP proof.
-- TPTP recognizes several standard intros and theorem proving systems might use
-- other ones.
data Intro
  = ByDefinition
  | ByAxiomOfChoice
  | ByTautology
  | ByAssumption
  deriving (Intro -> Intro -> Bool
(Intro -> Intro -> Bool) -> (Intro -> Intro -> Bool) -> Eq Intro
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Intro -> Intro -> Bool
$c/= :: Intro -> Intro -> Bool
== :: Intro -> Intro -> Bool
$c== :: Intro -> Intro -> Bool
Eq, Int -> Intro -> ShowS
[Intro] -> ShowS
Intro -> String
(Int -> Intro -> ShowS)
-> (Intro -> String) -> ([Intro] -> ShowS) -> Show Intro
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Intro] -> ShowS
$cshowList :: [Intro] -> ShowS
show :: Intro -> String
$cshow :: Intro -> String
showsPrec :: Int -> Intro -> ShowS
$cshowsPrec :: Int -> Intro -> ShowS
Show, Eq Intro
Eq Intro
-> (Intro -> Intro -> Ordering)
-> (Intro -> Intro -> Bool)
-> (Intro -> Intro -> Bool)
-> (Intro -> Intro -> Bool)
-> (Intro -> Intro -> Bool)
-> (Intro -> Intro -> Intro)
-> (Intro -> Intro -> Intro)
-> Ord Intro
Intro -> Intro -> Bool
Intro -> Intro -> Ordering
Intro -> Intro -> Intro
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 :: Intro -> Intro -> Intro
$cmin :: Intro -> Intro -> Intro
max :: Intro -> Intro -> Intro
$cmax :: Intro -> Intro -> Intro
>= :: Intro -> Intro -> Bool
$c>= :: Intro -> Intro -> Bool
> :: Intro -> Intro -> Bool
$c> :: Intro -> Intro -> Bool
<= :: Intro -> Intro -> Bool
$c<= :: Intro -> Intro -> Bool
< :: Intro -> Intro -> Bool
$c< :: Intro -> Intro -> Bool
compare :: Intro -> Intro -> Ordering
$ccompare :: Intro -> Intro -> Ordering
$cp1Ord :: Eq Intro
Ord, Int -> Intro
Intro -> Int
Intro -> [Intro]
Intro -> Intro
Intro -> Intro -> [Intro]
Intro -> Intro -> Intro -> [Intro]
(Intro -> Intro)
-> (Intro -> Intro)
-> (Int -> Intro)
-> (Intro -> Int)
-> (Intro -> [Intro])
-> (Intro -> Intro -> [Intro])
-> (Intro -> Intro -> [Intro])
-> (Intro -> Intro -> Intro -> [Intro])
-> Enum Intro
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 :: Intro -> Intro -> Intro -> [Intro]
$cenumFromThenTo :: Intro -> Intro -> Intro -> [Intro]
enumFromTo :: Intro -> Intro -> [Intro]
$cenumFromTo :: Intro -> Intro -> [Intro]
enumFromThen :: Intro -> Intro -> [Intro]
$cenumFromThen :: Intro -> Intro -> [Intro]
enumFrom :: Intro -> [Intro]
$cenumFrom :: Intro -> [Intro]
fromEnum :: Intro -> Int
$cfromEnum :: Intro -> Int
toEnum :: Int -> Intro
$ctoEnum :: Int -> Intro
pred :: Intro -> Intro
$cpred :: Intro -> Intro
succ :: Intro -> Intro
$csucc :: Intro -> Intro
Enum, Intro
Intro -> Intro -> Bounded Intro
forall a. a -> a -> Bounded a
maxBound :: Intro
$cmaxBound :: Intro
minBound :: Intro
$cminBound :: Intro
Bounded)

instance Named Intro where
  name :: Intro -> Text
name = \case
    Intro
ByDefinition    -> Text
"definition"
    Intro
ByAxiomOfChoice -> Text
"axiom_of_choice"
    Intro
ByTautology     -> Text
"tautology"
    Intro
ByAssumption    -> Text
"assumption"

-- | The source of a unit in a TSTP proof. Most commonly a formula is either
-- defined in a 'File' or is the result of an 'Inference'.
data Source
  = File Atom (Maybe UnitName)
  | Theory Atom (Maybe [Info])
  | Creator Atom (Maybe [Info])
  | Introduced (Reserved Intro) (Maybe [Info])
  | Inference Atom [Info] [Parent]
  | UnitSource UnitName
  | UnknownSource
  deriving (Source -> Source -> Bool
(Source -> Source -> Bool)
-> (Source -> Source -> Bool) -> Eq Source
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Source -> Source -> Bool
$c/= :: Source -> Source -> Bool
== :: Source -> Source -> Bool
$c== :: Source -> Source -> Bool
Eq, Int -> Source -> ShowS
[Source] -> ShowS
Source -> String
(Int -> Source -> ShowS)
-> (Source -> String) -> ([Source] -> ShowS) -> Show Source
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Source] -> ShowS
$cshowList :: [Source] -> ShowS
show :: Source -> String
$cshow :: Source -> String
showsPrec :: Int -> Source -> ShowS
$cshowsPrec :: Int -> Source -> ShowS
Show, Eq Source
Eq Source
-> (Source -> Source -> Ordering)
-> (Source -> Source -> Bool)
-> (Source -> Source -> Bool)
-> (Source -> Source -> Bool)
-> (Source -> Source -> Bool)
-> (Source -> Source -> Source)
-> (Source -> Source -> Source)
-> Ord Source
Source -> Source -> Bool
Source -> Source -> Ordering
Source -> Source -> Source
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 :: Source -> Source -> Source
$cmin :: Source -> Source -> Source
max :: Source -> Source -> Source
$cmax :: Source -> Source -> Source
>= :: Source -> Source -> Bool
$c>= :: Source -> Source -> Bool
> :: Source -> Source -> Bool
$c> :: Source -> Source -> Bool
<= :: Source -> Source -> Bool
$c<= :: Source -> Source -> Bool
< :: Source -> Source -> Bool
$c< :: Source -> Source -> Bool
compare :: Source -> Source -> Ordering
$ccompare :: Source -> Source -> Ordering
$cp1Ord :: Eq Source
Ord)

-- | The status values of the SZS ontologies of a TPTP text.
data SZS = SZS (Maybe Status) (Maybe Dataform)
  deriving (SZS -> SZS -> Bool
(SZS -> SZS -> Bool) -> (SZS -> SZS -> Bool) -> Eq SZS
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SZS -> SZS -> Bool
$c/= :: SZS -> SZS -> Bool
== :: SZS -> SZS -> Bool
$c== :: SZS -> SZS -> Bool
Eq, Int -> SZS -> ShowS
[SZS] -> ShowS
SZS -> String
(Int -> SZS -> ShowS)
-> (SZS -> String) -> ([SZS] -> ShowS) -> Show SZS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SZS] -> ShowS
$cshowList :: [SZS] -> ShowS
show :: SZS -> String
$cshow :: SZS -> String
showsPrec :: Int -> SZS -> ShowS
$cshowsPrec :: Int -> SZS -> ShowS
Show, Eq SZS
Eq SZS
-> (SZS -> SZS -> Ordering)
-> (SZS -> SZS -> Bool)
-> (SZS -> SZS -> Bool)
-> (SZS -> SZS -> Bool)
-> (SZS -> SZS -> Bool)
-> (SZS -> SZS -> SZS)
-> (SZS -> SZS -> SZS)
-> Ord SZS
SZS -> SZS -> Bool
SZS -> SZS -> Ordering
SZS -> SZS -> SZS
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 :: SZS -> SZS -> SZS
$cmin :: SZS -> SZS -> SZS
max :: SZS -> SZS -> SZS
$cmax :: SZS -> SZS -> SZS
>= :: SZS -> SZS -> Bool
$c>= :: SZS -> SZS -> Bool
> :: SZS -> SZS -> Bool
$c> :: SZS -> SZS -> Bool
<= :: SZS -> SZS -> Bool
$c<= :: SZS -> SZS -> Bool
< :: SZS -> SZS -> Bool
$c< :: SZS -> SZS -> Bool
compare :: SZS -> SZS -> Ordering
$ccompare :: SZS -> SZS -> Ordering
$cp1Ord :: Eq SZS
Ord)

-- | The auxiliary wrapper used to provide 'Named' instances with full names of
-- SZS ontologies to 'Success', 'NoSuccess' and 'Dataform'.
newtype SZSOntology a = SZSOntology { SZSOntology a -> a
unwrapSZSOntology :: a }
  deriving (SZSOntology a -> SZSOntology a -> Bool
(SZSOntology a -> SZSOntology a -> Bool)
-> (SZSOntology a -> SZSOntology a -> Bool) -> Eq (SZSOntology a)
forall a. Eq a => SZSOntology a -> SZSOntology a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SZSOntology a -> SZSOntology a -> Bool
$c/= :: forall a. Eq a => SZSOntology a -> SZSOntology a -> Bool
== :: SZSOntology a -> SZSOntology a -> Bool
$c== :: forall a. Eq a => SZSOntology a -> SZSOntology a -> Bool
Eq, Int -> SZSOntology a -> ShowS
[SZSOntology a] -> ShowS
SZSOntology a -> String
(Int -> SZSOntology a -> ShowS)
-> (SZSOntology a -> String)
-> ([SZSOntology a] -> ShowS)
-> Show (SZSOntology a)
forall a. Show a => Int -> SZSOntology a -> ShowS
forall a. Show a => [SZSOntology a] -> ShowS
forall a. Show a => SZSOntology a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SZSOntology a] -> ShowS
$cshowList :: forall a. Show a => [SZSOntology a] -> ShowS
show :: SZSOntology a -> String
$cshow :: forall a. Show a => SZSOntology a -> String
showsPrec :: Int -> SZSOntology a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> SZSOntology a -> ShowS
Show, Eq (SZSOntology a)
Eq (SZSOntology a)
-> (SZSOntology a -> SZSOntology a -> Ordering)
-> (SZSOntology a -> SZSOntology a -> Bool)
-> (SZSOntology a -> SZSOntology a -> Bool)
-> (SZSOntology a -> SZSOntology a -> Bool)
-> (SZSOntology a -> SZSOntology a -> Bool)
-> (SZSOntology a -> SZSOntology a -> SZSOntology a)
-> (SZSOntology a -> SZSOntology a -> SZSOntology a)
-> Ord (SZSOntology a)
SZSOntology a -> SZSOntology a -> Bool
SZSOntology a -> SZSOntology a -> Ordering
SZSOntology a -> SZSOntology a -> SZSOntology a
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 a. Ord a => Eq (SZSOntology a)
forall a. Ord a => SZSOntology a -> SZSOntology a -> Bool
forall a. Ord a => SZSOntology a -> SZSOntology a -> Ordering
forall a. Ord a => SZSOntology a -> SZSOntology a -> SZSOntology a
min :: SZSOntology a -> SZSOntology a -> SZSOntology a
$cmin :: forall a. Ord a => SZSOntology a -> SZSOntology a -> SZSOntology a
max :: SZSOntology a -> SZSOntology a -> SZSOntology a
$cmax :: forall a. Ord a => SZSOntology a -> SZSOntology a -> SZSOntology a
>= :: SZSOntology a -> SZSOntology a -> Bool
$c>= :: forall a. Ord a => SZSOntology a -> SZSOntology a -> Bool
> :: SZSOntology a -> SZSOntology a -> Bool
$c> :: forall a. Ord a => SZSOntology a -> SZSOntology a -> Bool
<= :: SZSOntology a -> SZSOntology a -> Bool
$c<= :: forall a. Ord a => SZSOntology a -> SZSOntology a -> Bool
< :: SZSOntology a -> SZSOntology a -> Bool
$c< :: forall a. Ord a => SZSOntology a -> SZSOntology a -> Bool
compare :: SZSOntology a -> SZSOntology a -> Ordering
$ccompare :: forall a. Ord a => SZSOntology a -> SZSOntology a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (SZSOntology a)
Ord, Int -> SZSOntology a
SZSOntology a -> Int
SZSOntology a -> [SZSOntology a]
SZSOntology a -> SZSOntology a
SZSOntology a -> SZSOntology a -> [SZSOntology a]
SZSOntology a -> SZSOntology a -> SZSOntology a -> [SZSOntology a]
(SZSOntology a -> SZSOntology a)
-> (SZSOntology a -> SZSOntology a)
-> (Int -> SZSOntology a)
-> (SZSOntology a -> Int)
-> (SZSOntology a -> [SZSOntology a])
-> (SZSOntology a -> SZSOntology a -> [SZSOntology a])
-> (SZSOntology a -> SZSOntology a -> [SZSOntology a])
-> (SZSOntology a
    -> SZSOntology a -> SZSOntology a -> [SZSOntology a])
-> Enum (SZSOntology a)
forall a. Enum a => Int -> SZSOntology a
forall a. Enum a => SZSOntology a -> Int
forall a. Enum a => SZSOntology a -> [SZSOntology a]
forall a. Enum a => SZSOntology a -> SZSOntology a
forall a.
Enum a =>
SZSOntology a -> SZSOntology a -> [SZSOntology a]
forall a.
Enum a =>
SZSOntology a -> SZSOntology a -> SZSOntology a -> [SZSOntology a]
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 :: SZSOntology a -> SZSOntology a -> SZSOntology a -> [SZSOntology a]
$cenumFromThenTo :: forall a.
Enum a =>
SZSOntology a -> SZSOntology a -> SZSOntology a -> [SZSOntology a]
enumFromTo :: SZSOntology a -> SZSOntology a -> [SZSOntology a]
$cenumFromTo :: forall a.
Enum a =>
SZSOntology a -> SZSOntology a -> [SZSOntology a]
enumFromThen :: SZSOntology a -> SZSOntology a -> [SZSOntology a]
$cenumFromThen :: forall a.
Enum a =>
SZSOntology a -> SZSOntology a -> [SZSOntology a]
enumFrom :: SZSOntology a -> [SZSOntology a]
$cenumFrom :: forall a. Enum a => SZSOntology a -> [SZSOntology a]
fromEnum :: SZSOntology a -> Int
$cfromEnum :: forall a. Enum a => SZSOntology a -> Int
toEnum :: Int -> SZSOntology a
$ctoEnum :: forall a. Enum a => Int -> SZSOntology a
pred :: SZSOntology a -> SZSOntology a
$cpred :: forall a. Enum a => SZSOntology a -> SZSOntology a
succ :: SZSOntology a -> SZSOntology a
$csucc :: forall a. Enum a => SZSOntology a -> SZSOntology a
Enum, SZSOntology a
SZSOntology a -> SZSOntology a -> Bounded (SZSOntology a)
forall a. a -> a -> Bounded a
forall a. Bounded a => SZSOntology a
maxBound :: SZSOntology a
$cmaxBound :: forall a. Bounded a => SZSOntology a
minBound :: SZSOntology a
$cminBound :: forall a. Bounded a => SZSOntology a
Bounded)

-- | The status of the proof search.
type Status = Either NoSuccess Success

-- | The SZS Success ontology. Values of this ontology are used to mark
-- the result of the proof search and also the status of an inference in
-- a TSTP proof. See
-- <http://www.tptp.org/Seminars/SZSOntologies/Summary.html The SZS Ontologies>
-- for details.
data Success
  = SUC -- ^ Success.
  | UNP -- ^ UnsatisfiabilityPreserving.
  | SAP -- ^ SatisfiabilityPreserving.
  | ESA -- ^ EquiSatisfiable.
  | SAT -- ^ Satisfiable.
  | FSA -- ^ FinitelySatisfiable.
  | THM -- ^ Theorem.
  | EQV -- ^ Equivalent.
  | TAC -- ^ TautologousConclusion.
  | WEC -- ^ WeakerConclusion.
  | ETH -- ^ EquivalentTheorem.
  | TAU -- ^ Tautology.
  | WTC -- ^ WeakerTautologousConclusion.
  | WTH -- ^ WeakerTheorem.
  | CAX -- ^ ContradictoryAxioms.
  | SCA -- ^ SatisfiableConclusionContradictoryAxioms.
  | TCA -- ^ TautologousConclusionContradictoryAxioms.
  | WCA -- ^ WeakerConclusionContradictoryAxioms.
  | CUP -- ^ CounterUnsatisfiabilityPreserving.
  | CSP -- ^ CounterSatisfiabilityPreserving.
  | ECS -- ^ EquiCounterSatisfiable.
  | CSA -- ^ CounterSatisfiable.
  | CTH -- ^ CounterTheorem.
  | CEQ -- ^ CounterEquivalent.
  | UNC -- ^ UnsatisfiableConclusion.
  | WCC -- ^ WeakerCounterConclusion.
  | ECT -- ^ EquivalentCounterTheorem.
  | FUN -- ^ FinitelyUnsatisfiable.
  | UNS -- ^ Unsatisfiable.
  | WUC -- ^ WeakerUnsatisfiableConclusion.
  | WCT -- ^ WeakerCounterTheorem.
  | SCC -- ^ SatisfiableCounterConclusionContradictoryAxioms.
  | UCA -- ^ UnsatisfiableConclusionContradictoryAxioms.
  | NOC -- ^ NoConsequence.
  deriving (Success -> Success -> Bool
(Success -> Success -> Bool)
-> (Success -> Success -> Bool) -> Eq Success
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Success -> Success -> Bool
$c/= :: Success -> Success -> Bool
== :: Success -> Success -> Bool
$c== :: Success -> Success -> Bool
Eq, Int -> Success -> ShowS
[Success] -> ShowS
Success -> String
(Int -> Success -> ShowS)
-> (Success -> String) -> ([Success] -> ShowS) -> Show Success
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Success] -> ShowS
$cshowList :: [Success] -> ShowS
show :: Success -> String
$cshow :: Success -> String
showsPrec :: Int -> Success -> ShowS
$cshowsPrec :: Int -> Success -> ShowS
Show, Eq Success
Eq Success
-> (Success -> Success -> Ordering)
-> (Success -> Success -> Bool)
-> (Success -> Success -> Bool)
-> (Success -> Success -> Bool)
-> (Success -> Success -> Bool)
-> (Success -> Success -> Success)
-> (Success -> Success -> Success)
-> Ord Success
Success -> Success -> Bool
Success -> Success -> Ordering
Success -> Success -> Success
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 :: Success -> Success -> Success
$cmin :: Success -> Success -> Success
max :: Success -> Success -> Success
$cmax :: Success -> Success -> Success
>= :: Success -> Success -> Bool
$c>= :: Success -> Success -> Bool
> :: Success -> Success -> Bool
$c> :: Success -> Success -> Bool
<= :: Success -> Success -> Bool
$c<= :: Success -> Success -> Bool
< :: Success -> Success -> Bool
$c< :: Success -> Success -> Bool
compare :: Success -> Success -> Ordering
$ccompare :: Success -> Success -> Ordering
$cp1Ord :: Eq Success
Ord, Int -> Success
Success -> Int
Success -> [Success]
Success -> Success
Success -> Success -> [Success]
Success -> Success -> Success -> [Success]
(Success -> Success)
-> (Success -> Success)
-> (Int -> Success)
-> (Success -> Int)
-> (Success -> [Success])
-> (Success -> Success -> [Success])
-> (Success -> Success -> [Success])
-> (Success -> Success -> Success -> [Success])
-> Enum Success
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 :: Success -> Success -> Success -> [Success]
$cenumFromThenTo :: Success -> Success -> Success -> [Success]
enumFromTo :: Success -> Success -> [Success]
$cenumFromTo :: Success -> Success -> [Success]
enumFromThen :: Success -> Success -> [Success]
$cenumFromThen :: Success -> Success -> [Success]
enumFrom :: Success -> [Success]
$cenumFrom :: Success -> [Success]
fromEnum :: Success -> Int
$cfromEnum :: Success -> Int
toEnum :: Int -> Success
$ctoEnum :: Int -> Success
pred :: Success -> Success
$cpred :: Success -> Success
succ :: Success -> Success
$csucc :: Success -> Success
Enum, Success
Success -> Success -> Bounded Success
forall a. a -> a -> Bounded a
maxBound :: Success
$cmaxBound :: Success
minBound :: Success
$cminBound :: Success
Bounded)

instance Named Success where
  name :: Success -> Text
name = \case
    Success
SUC -> Text
"suc"
    Success
UNP -> Text
"unp"
    Success
SAP -> Text
"sap"
    Success
ESA -> Text
"esa"
    Success
SAT -> Text
"sat"
    Success
FSA -> Text
"fsa"
    Success
THM -> Text
"thm"
    Success
EQV -> Text
"eqv"
    Success
TAC -> Text
"tac"
    Success
WEC -> Text
"wec"
    Success
ETH -> Text
"eth"
    Success
TAU -> Text
"tau"
    Success
WTC -> Text
"wtc"
    Success
WTH -> Text
"wth"
    Success
CAX -> Text
"cax"
    Success
SCA -> Text
"sca"
    Success
TCA -> Text
"tca"
    Success
WCA -> Text
"wca"
    Success
CUP -> Text
"cup"
    Success
CSP -> Text
"csp"
    Success
ECS -> Text
"ecs"
    Success
CSA -> Text
"csa"
    Success
CTH -> Text
"cth"
    Success
CEQ -> Text
"ceq"
    Success
UNC -> Text
"unc"
    Success
WCC -> Text
"wcc"
    Success
ECT -> Text
"ect"
    Success
FUN -> Text
"fun"
    Success
UNS -> Text
"uns"
    Success
WUC -> Text
"wuc"
    Success
WCT -> Text
"wct"
    Success
SCC -> Text
"scc"
    Success
UCA -> Text
"uca"
    Success
NOC -> Text
"noc"

instance Named (SZSOntology Success) where
  name :: SZSOntology Success -> Text
name (SZSOntology Success
s) = case Success
s of
    Success
SUC -> Text
"Success"
    Success
UNP -> Text
"UnsatisfiabilityPreserving"
    Success
SAP -> Text
"SatisfiabilityPreserving"
    Success
ESA -> Text
"EquiSatisfiable"
    Success
SAT -> Text
"Satisfiable"
    Success
FSA -> Text
"FinitelySatisfiable"
    Success
THM -> Text
"Theorem"
    Success
EQV -> Text
"Equivalent"
    Success
TAC -> Text
"TautologousConclusion"
    Success
WEC -> Text
"WeakerConclusion"
    Success
ETH -> Text
"EquivalentTheorem"
    Success
TAU -> Text
"Tautology"
    Success
WTC -> Text
"WeakerTautologousConclusion"
    Success
WTH -> Text
"WeakerTheorem"
    Success
CAX -> Text
"ContradictoryAxioms"
    Success
SCA -> Text
"SatisfiableConclusionContradictoryAxioms"
    Success
TCA -> Text
"TautologousConclusionContradictoryAxioms"
    Success
WCA -> Text
"WeakerConclusionContradictoryAxioms"
    Success
CUP -> Text
"CounterUnsatisfiabilityPreserving"
    Success
CSP -> Text
"CounterSatisfiabilityPreserving"
    Success
ECS -> Text
"EquiCounterSatisfiable"
    Success
CSA -> Text
"CounterSatisfiable"
    Success
CTH -> Text
"CounterTheorem"
    Success
CEQ -> Text
"CounterEquivalent"
    Success
UNC -> Text
"UnsatisfiableConclusion"
    Success
WCC -> Text
"WeakerCounterConclusion"
    Success
ECT -> Text
"EquivalentCounterTheorem"
    Success
FUN -> Text
"FinitelyUnsatisfiable"
    Success
UNS -> Text
"Unsatisfiable"
    Success
WUC -> Text
"WeakerUnsatisfiableConclusion"
    Success
WCT -> Text
"WeakerCounterTheorem"
    Success
SCC -> Text
"SatisfiableCounterConclusionContradictoryAxioms"
    Success
UCA -> Text
"UnsatisfiableConclusionContradictoryAxioms"
    Success
NOC -> Text
"NoConsequence"

-- | The SZS NoSuccess ontology. Values of this ontology are used to mark
-- the result of the proof search. See
-- <http://www.tptp.org/Seminars/SZSOntologies/Summary.html The SZS Ontologies>
-- for details.
data NoSuccess
  = NOS -- ^ NoSuccess.
  | OPN -- ^ Open.
  | UNK -- ^ Unknown.
  | ASS -- ^ Assumed.
  | STP -- ^ Stopped.
  | ERR -- ^ Error.
  | OSE -- ^ OSError.
  | INE -- ^ InputError.
  | USE -- ^ UsageError.
  | SYE -- ^ SyntaxError.
  | SEE -- ^ SemanticError.
  | TYE -- ^ TypeError.
  | FOR -- ^ Forced.
  | USR -- ^ User.
  | RSO -- ^ ResourceOut.
  | TMO -- ^ Timeout.
  | MMO -- ^ MemoryOut.
  | GUP -- ^ GaveUp.
  | INC -- ^ Incomplete.
  | IAP -- ^ Inappropriate.
  | INP -- ^ InProgress.
  | NTT -- ^ NotTried.
  | NTY -- ^ NotTriedYet.
  deriving (NoSuccess -> NoSuccess -> Bool
(NoSuccess -> NoSuccess -> Bool)
-> (NoSuccess -> NoSuccess -> Bool) -> Eq NoSuccess
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NoSuccess -> NoSuccess -> Bool
$c/= :: NoSuccess -> NoSuccess -> Bool
== :: NoSuccess -> NoSuccess -> Bool
$c== :: NoSuccess -> NoSuccess -> Bool
Eq, Int -> NoSuccess -> ShowS
[NoSuccess] -> ShowS
NoSuccess -> String
(Int -> NoSuccess -> ShowS)
-> (NoSuccess -> String)
-> ([NoSuccess] -> ShowS)
-> Show NoSuccess
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NoSuccess] -> ShowS
$cshowList :: [NoSuccess] -> ShowS
show :: NoSuccess -> String
$cshow :: NoSuccess -> String
showsPrec :: Int -> NoSuccess -> ShowS
$cshowsPrec :: Int -> NoSuccess -> ShowS
Show, Eq NoSuccess
Eq NoSuccess
-> (NoSuccess -> NoSuccess -> Ordering)
-> (NoSuccess -> NoSuccess -> Bool)
-> (NoSuccess -> NoSuccess -> Bool)
-> (NoSuccess -> NoSuccess -> Bool)
-> (NoSuccess -> NoSuccess -> Bool)
-> (NoSuccess -> NoSuccess -> NoSuccess)
-> (NoSuccess -> NoSuccess -> NoSuccess)
-> Ord NoSuccess
NoSuccess -> NoSuccess -> Bool
NoSuccess -> NoSuccess -> Ordering
NoSuccess -> NoSuccess -> NoSuccess
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 :: NoSuccess -> NoSuccess -> NoSuccess
$cmin :: NoSuccess -> NoSuccess -> NoSuccess
max :: NoSuccess -> NoSuccess -> NoSuccess
$cmax :: NoSuccess -> NoSuccess -> NoSuccess
>= :: NoSuccess -> NoSuccess -> Bool
$c>= :: NoSuccess -> NoSuccess -> Bool
> :: NoSuccess -> NoSuccess -> Bool
$c> :: NoSuccess -> NoSuccess -> Bool
<= :: NoSuccess -> NoSuccess -> Bool
$c<= :: NoSuccess -> NoSuccess -> Bool
< :: NoSuccess -> NoSuccess -> Bool
$c< :: NoSuccess -> NoSuccess -> Bool
compare :: NoSuccess -> NoSuccess -> Ordering
$ccompare :: NoSuccess -> NoSuccess -> Ordering
$cp1Ord :: Eq NoSuccess
Ord, Int -> NoSuccess
NoSuccess -> Int
NoSuccess -> [NoSuccess]
NoSuccess -> NoSuccess
NoSuccess -> NoSuccess -> [NoSuccess]
NoSuccess -> NoSuccess -> NoSuccess -> [NoSuccess]
(NoSuccess -> NoSuccess)
-> (NoSuccess -> NoSuccess)
-> (Int -> NoSuccess)
-> (NoSuccess -> Int)
-> (NoSuccess -> [NoSuccess])
-> (NoSuccess -> NoSuccess -> [NoSuccess])
-> (NoSuccess -> NoSuccess -> [NoSuccess])
-> (NoSuccess -> NoSuccess -> NoSuccess -> [NoSuccess])
-> Enum NoSuccess
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 :: NoSuccess -> NoSuccess -> NoSuccess -> [NoSuccess]
$cenumFromThenTo :: NoSuccess -> NoSuccess -> NoSuccess -> [NoSuccess]
enumFromTo :: NoSuccess -> NoSuccess -> [NoSuccess]
$cenumFromTo :: NoSuccess -> NoSuccess -> [NoSuccess]
enumFromThen :: NoSuccess -> NoSuccess -> [NoSuccess]
$cenumFromThen :: NoSuccess -> NoSuccess -> [NoSuccess]
enumFrom :: NoSuccess -> [NoSuccess]
$cenumFrom :: NoSuccess -> [NoSuccess]
fromEnum :: NoSuccess -> Int
$cfromEnum :: NoSuccess -> Int
toEnum :: Int -> NoSuccess
$ctoEnum :: Int -> NoSuccess
pred :: NoSuccess -> NoSuccess
$cpred :: NoSuccess -> NoSuccess
succ :: NoSuccess -> NoSuccess
$csucc :: NoSuccess -> NoSuccess
Enum, NoSuccess
NoSuccess -> NoSuccess -> Bounded NoSuccess
forall a. a -> a -> Bounded a
maxBound :: NoSuccess
$cmaxBound :: NoSuccess
minBound :: NoSuccess
$cminBound :: NoSuccess
Bounded)

instance Named (SZSOntology NoSuccess) where
  name :: SZSOntology NoSuccess -> Text
name (SZSOntology NoSuccess
ns) = case NoSuccess
ns of
    NoSuccess
NOS -> Text
"NoSuccess"
    NoSuccess
OPN -> Text
"Open"
    NoSuccess
UNK -> Text
"Unknown"
    NoSuccess
ASS -> Text
"Assumed"
    NoSuccess
STP -> Text
"Stopped"
    NoSuccess
ERR -> Text
"Error"
    NoSuccess
OSE -> Text
"OSError"
    NoSuccess
INE -> Text
"InputError"
    NoSuccess
USE -> Text
"UsageError"
    NoSuccess
SYE -> Text
"SyntaxError"
    NoSuccess
SEE -> Text
"SemanticError"
    NoSuccess
TYE -> Text
"TypeError"
    NoSuccess
FOR -> Text
"Forced"
    NoSuccess
USR -> Text
"User"
    NoSuccess
RSO -> Text
"ResourceOut"
    NoSuccess
TMO -> Text
"Timeout"
    NoSuccess
MMO -> Text
"MemoryOut"
    NoSuccess
GUP -> Text
"GaveUp"
    NoSuccess
INC -> Text
"Incomplete"
    NoSuccess
IAP -> Text
"Inappropriate"
    NoSuccess
INP -> Text
"InProgress"
    NoSuccess
NTT -> Text
"NotTried"
    NoSuccess
NTY -> Text
"NotTriedYet"

-- | The SZS Dataform ontology. Values of this ontology are used to mark
-- the form of logical data produced during proof search. See
-- <http://www.tptp.org/Seminars/SZSOntologies/Summary.html The SZS Ontologies>
-- for details.
data Dataform
  = LDa -- ^ LogicalData.
  | Sln -- ^ Solution.
  | Prf -- ^ Proof.
  | Der -- ^ Derivation.
  | Ref -- ^ Refutation.
  | CRf -- ^ CNFRefutation.
  | Int_ -- ^ Interpretation.
  | Mod -- ^ Model.
  | Pin -- ^ PartialInterpretation.
  | PMo -- ^ PartialModel.
  | SIn -- ^ StrictlyPartialInterpretation.
  | SMo -- ^ StrictlyPartialModel.
  | DIn -- ^ DomainInterpretation.
  | DMo -- ^ DomainModel.
  | DPI -- ^ DomainPartialInterpretation.
  | DPM -- ^ DomainPartialModel.
  | DSI -- ^ DomainStrictlyPartialInterpretation.
  | DSM -- ^ DomainStrictlyPartialModel.
  | FIn -- ^ FiniteInterpretation.
  | FMo -- ^ FiniteModel.
  | FPI -- ^ FinitePartialInterpretation.
  | FPM -- ^ FinitePartialModel.
  | FSI -- ^ FiniteStrictlyPartialInterpretation.
  | FSM -- ^ FiniteStrictlyPartialModel.
  | HIn -- ^ HerbrandInterpretation.
  | HMo -- ^ HerbrandModel.
  | TIn -- ^ FormulaInterpretation.
  | TMo -- ^ FormulaModel.
  | TPI -- ^ FormulaPartialInterpretation.
  | TSI -- ^ FormulaStrictlyPartialInterpretation.
  | TSM -- ^ FormulaStrictlyPartialModel.
  | Sat -- ^ Saturation.
  | Lof -- ^ ListOfFormulae.
  | Lth -- ^ ListOfTHF.
  | Ltf -- ^ ListOfTFF.
  | Lfo -- ^ ListOfFOF.
  | Lcn -- ^ ListOfCNF.
  | NSo -- ^ NotASolution.
  | Ass -- ^ Assurance.
  | IPr -- ^ IncompleteProof.
  | IIn -- ^ IncompleteInterpretation.
  | Non -- ^ None.
  deriving (Dataform -> Dataform -> Bool
(Dataform -> Dataform -> Bool)
-> (Dataform -> Dataform -> Bool) -> Eq Dataform
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Dataform -> Dataform -> Bool
$c/= :: Dataform -> Dataform -> Bool
== :: Dataform -> Dataform -> Bool
$c== :: Dataform -> Dataform -> Bool
Eq, Int -> Dataform -> ShowS
[Dataform] -> ShowS
Dataform -> String
(Int -> Dataform -> ShowS)
-> (Dataform -> String) -> ([Dataform] -> ShowS) -> Show Dataform
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Dataform] -> ShowS
$cshowList :: [Dataform] -> ShowS
show :: Dataform -> String
$cshow :: Dataform -> String
showsPrec :: Int -> Dataform -> ShowS
$cshowsPrec :: Int -> Dataform -> ShowS
Show, Eq Dataform
Eq Dataform
-> (Dataform -> Dataform -> Ordering)
-> (Dataform -> Dataform -> Bool)
-> (Dataform -> Dataform -> Bool)
-> (Dataform -> Dataform -> Bool)
-> (Dataform -> Dataform -> Bool)
-> (Dataform -> Dataform -> Dataform)
-> (Dataform -> Dataform -> Dataform)
-> Ord Dataform
Dataform -> Dataform -> Bool
Dataform -> Dataform -> Ordering
Dataform -> Dataform -> Dataform
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 :: Dataform -> Dataform -> Dataform
$cmin :: Dataform -> Dataform -> Dataform
max :: Dataform -> Dataform -> Dataform
$cmax :: Dataform -> Dataform -> Dataform
>= :: Dataform -> Dataform -> Bool
$c>= :: Dataform -> Dataform -> Bool
> :: Dataform -> Dataform -> Bool
$c> :: Dataform -> Dataform -> Bool
<= :: Dataform -> Dataform -> Bool
$c<= :: Dataform -> Dataform -> Bool
< :: Dataform -> Dataform -> Bool
$c< :: Dataform -> Dataform -> Bool
compare :: Dataform -> Dataform -> Ordering
$ccompare :: Dataform -> Dataform -> Ordering
$cp1Ord :: Eq Dataform
Ord, Int -> Dataform
Dataform -> Int
Dataform -> [Dataform]
Dataform -> Dataform
Dataform -> Dataform -> [Dataform]
Dataform -> Dataform -> Dataform -> [Dataform]
(Dataform -> Dataform)
-> (Dataform -> Dataform)
-> (Int -> Dataform)
-> (Dataform -> Int)
-> (Dataform -> [Dataform])
-> (Dataform -> Dataform -> [Dataform])
-> (Dataform -> Dataform -> [Dataform])
-> (Dataform -> Dataform -> Dataform -> [Dataform])
-> Enum Dataform
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 :: Dataform -> Dataform -> Dataform -> [Dataform]
$cenumFromThenTo :: Dataform -> Dataform -> Dataform -> [Dataform]
enumFromTo :: Dataform -> Dataform -> [Dataform]
$cenumFromTo :: Dataform -> Dataform -> [Dataform]
enumFromThen :: Dataform -> Dataform -> [Dataform]
$cenumFromThen :: Dataform -> Dataform -> [Dataform]
enumFrom :: Dataform -> [Dataform]
$cenumFrom :: Dataform -> [Dataform]
fromEnum :: Dataform -> Int
$cfromEnum :: Dataform -> Int
toEnum :: Int -> Dataform
$ctoEnum :: Int -> Dataform
pred :: Dataform -> Dataform
$cpred :: Dataform -> Dataform
succ :: Dataform -> Dataform
$csucc :: Dataform -> Dataform
Enum, Dataform
Dataform -> Dataform -> Bounded Dataform
forall a. a -> a -> Bounded a
maxBound :: Dataform
$cmaxBound :: Dataform
minBound :: Dataform
$cminBound :: Dataform
Bounded)

instance Named (SZSOntology Dataform) where
  name :: SZSOntology Dataform -> Text
name (SZSOntology Dataform
d) = case Dataform
d of
    Dataform
LDa -> Text
"LogicalData"
    Dataform
Sln -> Text
"Solution"
    Dataform
Prf -> Text
"Proof"
    Dataform
Der -> Text
"Derivation"
    Dataform
Ref -> Text
"Refutation"
    Dataform
CRf -> Text
"CNFRefutation"
    Dataform
Int_ -> Text
"Interpretation"
    Dataform
Mod -> Text
"Model"
    Dataform
Pin -> Text
"PartialInterpretation"
    Dataform
PMo -> Text
"PartialModel"
    Dataform
SIn -> Text
"StrictlyPartialInterpretation"
    Dataform
SMo -> Text
"StrictlyPartialModel"
    Dataform
DIn -> Text
"DomainInterpretation"
    Dataform
DMo -> Text
"DomainModel"
    Dataform
DPI -> Text
"DomainPartialInterpretation"
    Dataform
DPM -> Text
"DomainPartialModel"
    Dataform
DSI -> Text
"DomainStrictlyPartialInterpretation"
    Dataform
DSM -> Text
"DomainStrictlyPartialModel"
    Dataform
FIn -> Text
"FiniteInterpretation"
    Dataform
FMo -> Text
"FiniteModel"
    Dataform
FPI -> Text
"FinitePartialInterpretation"
    Dataform
FPM -> Text
"FinitePartialModel"
    Dataform
FSI -> Text
"FiniteStrictlyPartialInterpretation"
    Dataform
FSM -> Text
"FiniteStrictlyPartialModel"
    Dataform
HIn -> Text
"HerbrandInterpretation"
    Dataform
HMo -> Text
"HerbrandModel"
    Dataform
TIn -> Text
"FormulaInterpretation"
    Dataform
TMo -> Text
"FormulaModel"
    Dataform
TPI -> Text
"FormulaPartialInterpretation"
    Dataform
TSI -> Text
"FormulaStrictlyPartialInterpretation"
    Dataform
TSM -> Text
"FormulaStrictlyPartialModel"
    Dataform
Sat -> Text
"Saturation"
    Dataform
Lof -> Text
"ListOfFormulae"
    Dataform
Lth -> Text
"ListOfTHF"
    Dataform
Ltf -> Text
"ListOfTFF"
    Dataform
Lfo -> Text
"ListOfFOF"
    Dataform
Lcn -> Text
"ListOfCNF"
    Dataform
NSo -> Text
"NotASolution"
    Dataform
Ass -> Text
"Assurance"
    Dataform
IPr -> Text
"IncompleteProof"
    Dataform
IIn -> Text
"IncompleteInterpretation"
    Dataform
Non -> Text
"None"

-- | The parent of a formula in an inference.
data Parent = Parent Source [Info]
  deriving (Parent -> Parent -> Bool
(Parent -> Parent -> Bool)
-> (Parent -> Parent -> Bool) -> Eq Parent
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Parent -> Parent -> Bool
$c/= :: Parent -> Parent -> Bool
== :: Parent -> Parent -> Bool
$c== :: Parent -> Parent -> Bool
Eq, Int -> Parent -> ShowS
[Parent] -> ShowS
Parent -> String
(Int -> Parent -> ShowS)
-> (Parent -> String) -> ([Parent] -> ShowS) -> Show Parent
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Parent] -> ShowS
$cshowList :: [Parent] -> ShowS
show :: Parent -> String
$cshow :: Parent -> String
showsPrec :: Int -> Parent -> ShowS
$cshowsPrec :: Int -> Parent -> ShowS
Show, Eq Parent
Eq Parent
-> (Parent -> Parent -> Ordering)
-> (Parent -> Parent -> Bool)
-> (Parent -> Parent -> Bool)
-> (Parent -> Parent -> Bool)
-> (Parent -> Parent -> Bool)
-> (Parent -> Parent -> Parent)
-> (Parent -> Parent -> Parent)
-> Ord Parent
Parent -> Parent -> Bool
Parent -> Parent -> Ordering
Parent -> Parent -> Parent
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 :: Parent -> Parent -> Parent
$cmin :: Parent -> Parent -> Parent
max :: Parent -> Parent -> Parent
$cmax :: Parent -> Parent -> Parent
>= :: Parent -> Parent -> Bool
$c>= :: Parent -> Parent -> Bool
> :: Parent -> Parent -> Bool
$c> :: Parent -> Parent -> Bool
<= :: Parent -> Parent -> Bool
$c<= :: Parent -> Parent -> Bool
< :: Parent -> Parent -> Bool
$c< :: Parent -> Parent -> Bool
compare :: Parent -> Parent -> Ordering
$ccompare :: Parent -> Parent -> Ordering
$cp1Ord :: Eq Parent
Ord)

-- | An expression is either a formula or a term.
-- Expressions occur in TSTP proofs.
data Expression
  = Logical Formula
  | Term Term
  deriving (Expression -> Expression -> Bool
(Expression -> Expression -> Bool)
-> (Expression -> Expression -> Bool) -> Eq Expression
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Expression -> Expression -> Bool
$c/= :: Expression -> Expression -> Bool
== :: Expression -> Expression -> Bool
$c== :: Expression -> Expression -> Bool
Eq, Int -> Expression -> ShowS
[Expression] -> ShowS
Expression -> String
(Int -> Expression -> ShowS)
-> (Expression -> String)
-> ([Expression] -> ShowS)
-> Show Expression
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Expression] -> ShowS
$cshowList :: [Expression] -> ShowS
show :: Expression -> String
$cshow :: Expression -> String
showsPrec :: Int -> Expression -> ShowS
$cshowsPrec :: Int -> Expression -> ShowS
Show, Eq Expression
Eq Expression
-> (Expression -> Expression -> Ordering)
-> (Expression -> Expression -> Bool)
-> (Expression -> Expression -> Bool)
-> (Expression -> Expression -> Bool)
-> (Expression -> Expression -> Bool)
-> (Expression -> Expression -> Expression)
-> (Expression -> Expression -> Expression)
-> Ord Expression
Expression -> Expression -> Bool
Expression -> Expression -> Ordering
Expression -> Expression -> Expression
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 :: Expression -> Expression -> Expression
$cmin :: Expression -> Expression -> Expression
max :: Expression -> Expression -> Expression
$cmax :: Expression -> Expression -> Expression
>= :: Expression -> Expression -> Bool
$c>= :: Expression -> Expression -> Bool
> :: Expression -> Expression -> Bool
$c> :: Expression -> Expression -> Bool
<= :: Expression -> Expression -> Bool
$c<= :: Expression -> Expression -> Bool
< :: Expression -> Expression -> Bool
$c< :: Expression -> Expression -> Bool
compare :: Expression -> Expression -> Ordering
$ccompare :: Expression -> Expression -> Ordering
$cp1Ord :: Eq Expression
Ord)

-- | The information about a formula.
data Info
  = Description Atom
  | Iquote Atom
  | Status (Reserved Success)
  | Assumptions (NonEmpty UnitName)
  | NewSymbols Atom [Either Var Atom]
  | Refutation Atom
  | Expression Expression
  | Bind Var Expression
  | Application Atom [Info]
  | InfoNumber Number
  | Infos [Info]
  deriving (Info -> Info -> Bool
(Info -> Info -> Bool) -> (Info -> Info -> Bool) -> Eq Info
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Info -> Info -> Bool
$c/= :: Info -> Info -> Bool
== :: Info -> Info -> Bool
$c== :: Info -> Info -> Bool
Eq, Int -> Info -> ShowS
[Info] -> ShowS
Info -> String
(Int -> Info -> ShowS)
-> (Info -> String) -> ([Info] -> ShowS) -> Show Info
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Info] -> ShowS
$cshowList :: [Info] -> ShowS
show :: Info -> String
$cshow :: Info -> String
showsPrec :: Int -> Info -> ShowS
$cshowsPrec :: Int -> Info -> ShowS
Show, Eq Info
Eq Info
-> (Info -> Info -> Ordering)
-> (Info -> Info -> Bool)
-> (Info -> Info -> Bool)
-> (Info -> Info -> Bool)
-> (Info -> Info -> Bool)
-> (Info -> Info -> Info)
-> (Info -> Info -> Info)
-> Ord Info
Info -> Info -> Bool
Info -> Info -> Ordering
Info -> Info -> Info
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 :: Info -> Info -> Info
$cmin :: Info -> Info -> Info
max :: Info -> Info -> Info
$cmax :: Info -> Info -> Info
>= :: Info -> Info -> Bool
$c>= :: Info -> Info -> Bool
> :: Info -> Info -> Bool
$c> :: Info -> Info -> Bool
<= :: Info -> Info -> Bool
$c<= :: Info -> Info -> Bool
< :: Info -> Info -> Bool
$c< :: Info -> Info -> Bool
compare :: Info -> Info -> Ordering
$ccompare :: Info -> Info -> Ordering
$cp1Ord :: Eq Info
Ord)

-- | The annotation of a unit. Most commonly, annotations are attached to units
-- in TSTP proofs.
type Annotation = (Source, Maybe [Info])