{-# LANGUAGE CPP, MultiParamTypeClasses, TypeSynonymInstances
, FlexibleInstances #-}
module TPTP.Logic_TPTP where
import TPTP.AS hiding (TPTP)
import TPTP.ATC_TPTP ()
import TPTP.Morphism
import TPTP.Morphism.Sentence
import TPTP.Parser
import TPTP.Pretty
import TPTP.Prover.CVC4
import TPTP.Prover.Darwin
import TPTP.Prover.EProver
import TPTP.Prover.Geo3
import TPTP.Prover.Isabelle
import TPTP.Prover.Leo2
import TPTP.Prover.Satallax
import TPTP.Prover.SPASS
import TPTP.Prover.Vampire
import TPTP.Sign
import TPTP.Sublogic as Sublogic
import TPTP.StaticAnalysis
import TPTP.ProveHyper
import TPTP.ConsChecker
import ATC.ProofTree ()
import Common.DefaultMorphism
import Common.ProofTree
import Logic.Logic as Logic
import Data.Monoid ()
import qualified Data.Set as Set
import qualified SoftFOL.ProveDarwin as Darwin
data TPTP = TPTP deriving (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, 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)
instance Language TPTP
where
description :: TPTP -> String
description _ =
"The TPTP (Thousands of Problems for Theorem Provers) Language\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
"See http://www.cs.miami.edu/~tptp/"
instance Syntax TPTP BASIC_SPEC Symbol () ()
where
parse_basic_spec :: TPTP -> Maybe (PrefixMap -> AParser st BASIC_SPEC)
parse_basic_spec TPTP = (PrefixMap -> AParser st BASIC_SPEC)
-> Maybe (PrefixMap -> AParser st BASIC_SPEC)
forall a. a -> Maybe a
Just PrefixMap -> AParser st BASIC_SPEC
forall st. PrefixMap -> AParser st BASIC_SPEC
parseBasicSpec
instance Semigroup BASIC_SPEC where
(Basic_spec l1 :: [Annoted TPTP]
l1) <> :: BASIC_SPEC -> BASIC_SPEC -> BASIC_SPEC
<> (Basic_spec l2 :: [Annoted TPTP]
l2) = [Annoted TPTP] -> BASIC_SPEC
Basic_spec ([Annoted TPTP] -> BASIC_SPEC) -> [Annoted TPTP] -> BASIC_SPEC
forall a b. (a -> b) -> a -> b
$ [Annoted TPTP]
l1 [Annoted TPTP] -> [Annoted TPTP] -> [Annoted TPTP]
forall a. [a] -> [a] -> [a]
++ [Annoted TPTP]
l2
instance Monoid BASIC_SPEC where
mempty :: BASIC_SPEC
mempty = [Annoted TPTP] -> BASIC_SPEC
Basic_spec []
instance Sentences TPTP Sentence Sign Morphism Symbol
where
map_sen :: TPTP -> Morphism -> Sentence -> Result Sentence
map_sen TPTP _ = Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return
sym_of :: TPTP -> Sign -> [Set Symbol]
sym_of TPTP = Set Symbol -> [Set Symbol]
forall a. a -> [a]
singletonList (Set Symbol -> [Set Symbol])
-> (Sign -> Set Symbol) -> Sign -> [Set Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Set Symbol
symbolsOfSign
symsOfSen :: TPTP -> Sign -> Sentence -> [Symbol]
symsOfSen TPTP _ = Set Symbol -> [Symbol]
forall a. Set a -> [a]
Set.toList (Set Symbol -> [Symbol])
-> (Sentence -> Set Symbol) -> Sentence -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sentence -> Set Symbol
symbolsOfSentence
sym_name :: TPTP -> Symbol -> Id
sym_name TPTP = Symbol -> Id
symbolToId
symKind :: TPTP -> Symbol -> String
symKind TPTP = Symbol -> String
symbolTypeS
print_named :: TPTP -> Named Sentence -> Doc
print_named TPTP = Named Sentence -> Doc
printNamedSentence
negation :: TPTP -> Sentence -> Maybe Sentence
negation TPTP = Sentence -> Maybe Sentence
negateSentence
instance StaticAnalysis TPTP BASIC_SPEC Sentence () () Sign Morphism Symbol ()
where
empty_signature :: TPTP -> Sign
empty_signature TPTP = Sign
emptySign
is_subsig :: TPTP -> Sign -> Sign -> Bool
is_subsig TPTP _ _ = Bool
True
subsig_inclusion :: TPTP -> Sign -> Sign -> Result Morphism
subsig_inclusion TPTP = Sign -> Sign -> Result Morphism
forall (m :: * -> *) sign.
Monad m =>
sign -> sign -> m (DefaultMorphism sign)
defaultInclusion
basic_analysis :: TPTP
-> Maybe
((BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence]))
basic_analysis TPTP = ((BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence]))
-> Maybe
((BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence]))
forall a. a -> Maybe a
Just (BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named Sentence])
basicAnalysis
signature_union :: TPTP -> Sign -> Sign -> Result Sign
signature_union TPTP = Sign -> Sign -> Result Sign
signatureUnionR
instance Logic TPTP Sublogic BASIC_SPEC Sentence () () Sign Morphism Symbol () ProofTree
where
stability :: TPTP -> Stability
stability _ = Stability
Stable
all_sublogics :: TPTP -> [Sublogic]
all_sublogics TPTP = [Sublogic
CNF, Sublogic
FOF, Sublogic
TFF, Sublogic
THF]
provers :: TPTP -> [Prover Sign Sentence Morphism Sublogic ProofTree]
provers TPTP = [Prover Sign Sentence Morphism Sublogic ProofTree
cvc4, Prover Sign Sentence Morphism Sublogic ProofTree
darwin, Prover Sign Sentence Morphism Sublogic ProofTree
eprover, Prover Sign Sentence Morphism Sublogic ProofTree
geo3, Prover Sign Sentence Morphism Sublogic ProofTree
isabelle, Prover Sign Sentence Morphism Sublogic ProofTree
leo2, Prover Sign Sentence Morphism Sublogic ProofTree
satallax,
Prover Sign Sentence Morphism Sublogic ProofTree
spass, Prover Sign Sentence Morphism Sublogic ProofTree
vampire]
cons_checkers :: TPTP -> [ConsChecker Sign Sentence Sublogic Morphism ProofTree]
cons_checkers TPTP = [ConsChecker Sign Sentence Sublogic Morphism ProofTree
hyperConsChecker] [ConsChecker Sign Sentence Sublogic Morphism ProofTree]
-> [ConsChecker Sign Sentence Sublogic Morphism ProofTree]
-> [ConsChecker Sign Sentence Sublogic Morphism ProofTree]
forall a. [a] -> [a] -> [a]
++
(ProverBinary
-> ConsChecker Sign Sentence Sublogic Morphism ProofTree)
-> [ProverBinary]
-> [ConsChecker Sign Sentence Sublogic Morphism ProofTree]
forall a b. (a -> b) -> [a] -> [b]
map ProverBinary
-> ConsChecker Sign Sentence Sublogic Morphism ProofTree
darwinConsChecker [ProverBinary]
Darwin.tptpProvers
instance SublogicName Sublogic where
sublogicName :: Sublogic -> String
sublogicName = Sublogic -> String
Sublogic.sublogicName
instance SemiLatticeWithTop Sublogic where
lub :: Sublogic -> Sublogic -> Sublogic
lub = Sublogic -> Sublogic -> Sublogic
leastUpperBound
top :: Sublogic
top = Sublogic
Sublogic.top
instance MinSublogic Sublogic () where
minSublogic :: () -> Sublogic
minSublogic = Sublogic -> () -> Sublogic
sublogicOfUnit Sublogic
bottom
instance MinSublogic Sublogic BASIC_SPEC where
minSublogic :: BASIC_SPEC -> Sublogic
minSublogic = Sublogic -> BASIC_SPEC -> Sublogic
sublogicOfBaiscSpec Sublogic
bottom
instance MinSublogic Sublogic Sentence where
minSublogic :: Sentence -> Sublogic
minSublogic = Sublogic -> Sentence -> Sublogic
sublogicOfSentence Sublogic
bottom
instance MinSublogic Sublogic Symbol where
minSublogic :: Symbol -> Sublogic
minSublogic = Sublogic -> Symbol -> Sublogic
sublogicOfSymbol Sublogic
bottom
instance MinSublogic Sublogic Sign where
minSublogic :: Sign -> Sublogic
minSublogic = Sublogic -> Sign -> Sublogic
sublogicOfSign Sublogic
bottom
instance MinSublogic Sublogic Morphism where
minSublogic :: Morphism -> Sublogic
minSublogic = Sublogic -> Morphism -> Sublogic
sublogicOfMorphism Sublogic
bottom
instance ProjectSublogic Sublogic BASIC_SPEC where
projectSublogic :: Sublogic -> BASIC_SPEC -> BASIC_SPEC
projectSublogic = Sublogic -> BASIC_SPEC -> BASIC_SPEC
projectSublogicBasicSpec
instance ProjectSublogic Sublogic Sentence where
projectSublogic :: Sublogic -> Sentence -> Sentence
projectSublogic = Sublogic -> Sentence -> Sentence
projectSublogicSentence
instance ProjectSublogic Sublogic Sign where
projectSublogic :: Sublogic -> Sign -> Sign
projectSublogic = Sublogic -> Sign -> Sign
projectSublogicSign
instance ProjectSublogic Sublogic Morphism where
projectSublogic :: Sublogic -> Morphism -> Morphism
projectSublogic = Sublogic -> Morphism -> Morphism
projectSublogicMorphism
instance ProjectSublogicM Sublogic () where
projectSublogicM :: Sublogic -> () -> Maybe ()
projectSublogicM = Sublogic -> () -> Maybe ()
projectSublogicMUnit
instance ProjectSublogicM Sublogic Symbol where
projectSublogicM :: Sublogic -> Symbol -> Maybe Symbol
projectSublogicM = Sublogic -> Symbol -> Maybe Symbol
projectSublogicMSymbol