{-# LANGUAGE CPP, MultiParamTypeClasses, TypeSynonymInstances
  , FlexibleInstances #-}
{- |
Module      :  ./SoftFOL/Logic_SoftFOL.hs
Description :  Instance of class Logic for SoftFOL.
Copyright   :  (c) Rene Wagner, Klaus Luettich, Uni Bremen 2005-2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (imports Logic)

Instance of class Logic for SoftFOL.
-}

module SoftFOL.Logic_SoftFOL where

import Data.Set (toList)

import Common.DefaultMorphism
import Common.DocUtils
import Common.ProofTree

import ATC.ProofTree ()

import Logic.Logic

import SoftFOL.ATC_SoftFOL ()
import SoftFOL.Sign
import SoftFOL.StatAna
import SoftFOL.Print
import SoftFOL.Conversions
import SoftFOL.Morphism
import SoftFOL.PrintTPTP ()

import SoftFOL.ProveSPASS
import SoftFOL.ProveHyperHyper
#ifndef NOHTTP
import SoftFOL.ProveMathServ
import SoftFOL.ProveVampire
#endif
import SoftFOL.ProveDarwin
import SoftFOL.ProveMetis

instance Pretty Sign where
  pretty :: Sign -> Doc
pretty = SPLogicalPart -> Doc
forall a. Pretty a => a -> Doc
pretty (SPLogicalPart -> Doc) -> (Sign -> SPLogicalPart) -> Sign -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> SPLogicalPart
signToSPLogicalPart

{- |
  A dummy datatype for the LogicGraph and for identifying the right
  instances
-}
data SoftFOL = SoftFOL deriving (Int -> SoftFOL -> ShowS
[SoftFOL] -> ShowS
SoftFOL -> String
(Int -> SoftFOL -> ShowS)
-> (SoftFOL -> String) -> ([SoftFOL] -> ShowS) -> Show SoftFOL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SoftFOL] -> ShowS
$cshowList :: [SoftFOL] -> ShowS
show :: SoftFOL -> String
$cshow :: SoftFOL -> String
showsPrec :: Int -> SoftFOL -> ShowS
$cshowsPrec :: Int -> SoftFOL -> ShowS
Show)

instance Language SoftFOL where
 description :: SoftFOL -> String
description _ =
  "SoftFOL - Softly typed First Order Logic for " String -> ShowS
forall a. [a] -> [a] -> [a]
++
       "Automated Theorem Proving Systems\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
  "This logic corresponds to the logic of SPASS, \n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
  "but the generation of TPTP is also possible.\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
  "See http://spass.mpi-sb.mpg.de/\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
  "and http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html"

instance Logic.Logic.Syntax SoftFOL [TPTP] SFSymbol () ()
    -- default implementation is fine!

instance Sentences SoftFOL Sentence Sign
                           SoftFOLMorphism SFSymbol where
      map_sen :: SoftFOL -> SoftFOLMorphism -> Sentence -> Result Sentence
map_sen SoftFOL _ = Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return
      sym_of :: SoftFOL -> Sign -> [Set SFSymbol]
sym_of SoftFOL = Set SFSymbol -> [Set SFSymbol]
forall a. a -> [a]
singletonList (Set SFSymbol -> [Set SFSymbol])
-> (Sign -> Set SFSymbol) -> Sign -> [Set SFSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Set SFSymbol
symOf
      symsOfSen :: SoftFOL -> Sign -> Sentence -> [SFSymbol]
symsOfSen SoftFOL sign :: Sign
sign = Set SFSymbol -> [SFSymbol]
forall a. Set a -> [a]
toList (Set SFSymbol -> [SFSymbol])
-> (Sentence -> Set SFSymbol) -> Sentence -> [SFSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Sentence -> Set SFSymbol
symsOfTerm Sign
sign
      sym_name :: SoftFOL -> SFSymbol -> Id
sym_name SoftFOL = SFSymbol -> Id
symbolToId
      symKind :: SoftFOL -> SFSymbol -> String
symKind SoftFOL = SFSymbType -> String
sfSymbKind (SFSymbType -> String)
-> (SFSymbol -> SFSymbType) -> SFSymbol -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SFSymbol -> SFSymbType
sym_type
      print_named :: SoftFOL -> Named Sentence -> Doc
print_named SoftFOL = Named Sentence -> Doc
printFormula
      negation :: SoftFOL -> Sentence -> Maybe Sentence
negation _ = Sentence -> Maybe Sentence
negateSentence
    -- other default implementations are fine

instance StaticAnalysis SoftFOL [TPTP] Sentence
               () ()
               Sign
               SoftFOLMorphism SFSymbol () where
         empty_signature :: SoftFOL -> Sign
empty_signature SoftFOL = Sign
emptySign
         is_subsig :: SoftFOL -> Sign -> Sign -> Bool
is_subsig SoftFOL _ _ = Bool
True
         subsig_inclusion :: SoftFOL -> Sign -> Sign -> Result SoftFOLMorphism
subsig_inclusion SoftFOL = Sign -> Sign -> Result SoftFOLMorphism
forall (m :: * -> *) sign.
Monad m =>
sign -> sign -> m (DefaultMorphism sign)
defaultInclusion
         basic_analysis :: SoftFOL
-> Maybe
     (([TPTP], Sign, GlobalAnnos)
      -> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence]))
basic_analysis SoftFOL = (([TPTP], Sign, GlobalAnnos)
 -> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence]))
-> Maybe
     (([TPTP], Sign, GlobalAnnos)
      -> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence]))
forall a. a -> Maybe a
Just ([TPTP], Sign, GlobalAnnos)
-> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence])
basicAnalysis

instance Logic SoftFOL () [TPTP] Sentence () ()
               Sign
               SoftFOLMorphism SFSymbol () ProofTree where
         stability :: SoftFOL -> Stability
stability _ = Stability
Stable
         provers :: SoftFOL -> [Prover Sign Sentence SoftFOLMorphism () ProofTree]
provers SoftFOL = [Prover Sign Sentence SoftFOLMorphism () ProofTree
spassProver]
#ifndef NOHTTP
           [Prover Sign Sentence SoftFOLMorphism () ProofTree]
-> [Prover Sign Sentence SoftFOLMorphism () ProofTree]
-> [Prover Sign Sentence SoftFOLMorphism () ProofTree]
forall a. [a] -> [a] -> [a]
++ [Prover Sign Sentence SoftFOLMorphism () ProofTree
mathServBroker, Prover Sign Sentence SoftFOLMorphism () ProofTree
vampire]
#endif
           [Prover Sign Sentence SoftFOLMorphism () ProofTree]
-> [Prover Sign Sentence SoftFOLMorphism () ProofTree]
-> [Prover Sign Sentence SoftFOLMorphism () ProofTree]
forall a. [a] -> [a] -> [a]
++ (ProverBinary -> Prover Sign Sentence SoftFOLMorphism () ProofTree)
-> [ProverBinary]
-> [Prover Sign Sentence SoftFOLMorphism () ProofTree]
forall a b. (a -> b) -> [a] -> [b]
map ProverBinary -> Prover Sign Sentence SoftFOLMorphism () ProofTree
darwinProver [ProverBinary]
tptpProvers
           [Prover Sign Sentence SoftFOLMorphism () ProofTree]
-> [Prover Sign Sentence SoftFOLMorphism () ProofTree]
-> [Prover Sign Sentence SoftFOLMorphism () ProofTree]
forall a. [a] -> [a] -> [a]
++ [Prover Sign Sentence SoftFOLMorphism () ProofTree
metisProver, Prover Sign Sentence SoftFOLMorphism () ProofTree
hyperProver]
         cons_checkers :: SoftFOL -> [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree]
cons_checkers SoftFOL = (ProverBinary
 -> ConsChecker Sign Sentence () SoftFOLMorphism ProofTree)
-> [ProverBinary]
-> [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree]
forall a b. (a -> b) -> [a] -> [b]
map ProverBinary
-> ConsChecker Sign Sentence () SoftFOLMorphism ProofTree
darwinConsChecker [ProverBinary]
tptpProvers
           [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree]
-> [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree]
-> [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree]
forall a. [a] -> [a] -> [a]
++ [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree
hyperConsChecker]