{-# LANGUAGE CPP, MultiParamTypeClasses, TypeSynonymInstances
  , FlexibleInstances #-}
{- |
Module      :  ./TPTP/Logic_TPTP.hs
Description :  Instance of class Logic for TPTP.
Copyright   :  (c) Eugen Kuksa University of Magdeburg 2017
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Eugen Kuksa <kuksa@iks.cs.ovgu.de>
Stability   :  provisional
Portability :  non-portable (imports Logic)

Instance of class Logic for TPTP.
-}

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