{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./TPTP/Prover/ProverState.hs
Description :  Help functions for all automatic theorem provers.
Copyright   :  (c) Rainer Grabbe
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  needs POSIX

Data structures and initialising functions for Prover state and configurations.

-}

module TPTP.Prover.ProverState ( ProverState (..)
                               , getAxioms
                               , insertSentenceIntoProverState
                               , ioShowTPTPProblem
                               , showTPTPProblemM
                               , tptpProverState
                               ) where

import TPTP.AS
import TPTP.Morphism
import TPTP.Pretty
import TPTP.Sign

import Common.AS_Annotation
import Common.ProofUtils
import Common.Doc
import Logic.Prover

import Data.Data
import Data.List

-- * Data structures

data PProblem = PProblem { PProblem -> String
identifier :: String
                         , PProblem -> PLogicalPart
logicalPart :: PLogicalPart
                         } deriving (Int -> PProblem -> ShowS
[PProblem] -> ShowS
PProblem -> String
(Int -> PProblem -> ShowS)
-> (PProblem -> String) -> ([PProblem] -> ShowS) -> Show PProblem
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PProblem] -> ShowS
$cshowList :: [PProblem] -> ShowS
show :: PProblem -> String
$cshow :: PProblem -> String
showsPrec :: Int -> PProblem -> ShowS
$cshowsPrec :: Int -> PProblem -> ShowS
Show, PProblem -> PProblem -> Bool
(PProblem -> PProblem -> Bool)
-> (PProblem -> PProblem -> Bool) -> Eq PProblem
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PProblem -> PProblem -> Bool
$c/= :: PProblem -> PProblem -> Bool
== :: PProblem -> PProblem -> Bool
$c== :: PProblem -> PProblem -> Bool
Eq, Eq PProblem
Eq PProblem =>
(PProblem -> PProblem -> Ordering)
-> (PProblem -> PProblem -> Bool)
-> (PProblem -> PProblem -> Bool)
-> (PProblem -> PProblem -> Bool)
-> (PProblem -> PProblem -> Bool)
-> (PProblem -> PProblem -> PProblem)
-> (PProblem -> PProblem -> PProblem)
-> Ord PProblem
PProblem -> PProblem -> Bool
PProblem -> PProblem -> Ordering
PProblem -> PProblem -> PProblem
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 :: PProblem -> PProblem -> PProblem
$cmin :: PProblem -> PProblem -> PProblem
max :: PProblem -> PProblem -> PProblem
$cmax :: PProblem -> PProblem -> PProblem
>= :: PProblem -> PProblem -> Bool
$c>= :: PProblem -> PProblem -> Bool
> :: PProblem -> PProblem -> Bool
$c> :: PProblem -> PProblem -> Bool
<= :: PProblem -> PProblem -> Bool
$c<= :: PProblem -> PProblem -> Bool
< :: PProblem -> PProblem -> Bool
$c< :: PProblem -> PProblem -> Bool
compare :: PProblem -> PProblem -> Ordering
$ccompare :: PProblem -> PProblem -> Ordering
$cp1Ord :: Eq PProblem
Ord, Typeable, Typeable PProblem
Constr
DataType
Typeable PProblem =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> PProblem -> c PProblem)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c PProblem)
-> (PProblem -> Constr)
-> (PProblem -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c PProblem))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PProblem))
-> ((forall b. Data b => b -> b) -> PProblem -> PProblem)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PProblem -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PProblem -> r)
-> (forall u. (forall d. Data d => d -> u) -> PProblem -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> PProblem -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PProblem -> m PProblem)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PProblem -> m PProblem)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PProblem -> m PProblem)
-> Data PProblem
PProblem -> Constr
PProblem -> DataType
(forall b. Data b => b -> b) -> PProblem -> PProblem
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PProblem -> c PProblem
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PProblem
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> PProblem -> u
forall u. (forall d. Data d => d -> u) -> PProblem -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PProblem -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PProblem -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PProblem -> m PProblem
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PProblem -> m PProblem
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PProblem
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PProblem -> c PProblem
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PProblem)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PProblem)
$cPProblem :: Constr
$tPProblem :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> PProblem -> m PProblem
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PProblem -> m PProblem
gmapMp :: (forall d. Data d => d -> m d) -> PProblem -> m PProblem
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PProblem -> m PProblem
gmapM :: (forall d. Data d => d -> m d) -> PProblem -> m PProblem
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PProblem -> m PProblem
gmapQi :: Int -> (forall d. Data d => d -> u) -> PProblem -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PProblem -> u
gmapQ :: (forall d. Data d => d -> u) -> PProblem -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PProblem -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PProblem -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PProblem -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PProblem -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PProblem -> r
gmapT :: (forall b. Data b => b -> b) -> PProblem -> PProblem
$cgmapT :: (forall b. Data b => b -> b) -> PProblem -> PProblem
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PProblem)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PProblem)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c PProblem)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PProblem)
dataTypeOf :: PProblem -> DataType
$cdataTypeOf :: PProblem -> DataType
toConstr :: PProblem -> Constr
$ctoConstr :: PProblem -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PProblem
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PProblem
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PProblem -> c PProblem
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PProblem -> c PProblem
$cp1Data :: Typeable PProblem
Data)

data ProverState = ProverState { ProverState -> PLogicalPart
psLogicalPart :: PLogicalPart
                               } deriving (Int -> ProverState -> ShowS
[ProverState] -> ShowS
ProverState -> String
(Int -> ProverState -> ShowS)
-> (ProverState -> String)
-> ([ProverState] -> ShowS)
-> Show ProverState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProverState] -> ShowS
$cshowList :: [ProverState] -> ShowS
show :: ProverState -> String
$cshow :: ProverState -> String
showsPrec :: Int -> ProverState -> ShowS
$cshowsPrec :: Int -> ProverState -> ShowS
Show, Eq ProverState
Eq ProverState =>
(ProverState -> ProverState -> Ordering)
-> (ProverState -> ProverState -> Bool)
-> (ProverState -> ProverState -> Bool)
-> (ProverState -> ProverState -> Bool)
-> (ProverState -> ProverState -> Bool)
-> (ProverState -> ProverState -> ProverState)
-> (ProverState -> ProverState -> ProverState)
-> Ord ProverState
ProverState -> ProverState -> Bool
ProverState -> ProverState -> Ordering
ProverState -> ProverState -> ProverState
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 :: ProverState -> ProverState -> ProverState
$cmin :: ProverState -> ProverState -> ProverState
max :: ProverState -> ProverState -> ProverState
$cmax :: ProverState -> ProverState -> ProverState
>= :: ProverState -> ProverState -> Bool
$c>= :: ProverState -> ProverState -> Bool
> :: ProverState -> ProverState -> Bool
$c> :: ProverState -> ProverState -> Bool
<= :: ProverState -> ProverState -> Bool
$c<= :: ProverState -> ProverState -> Bool
< :: ProverState -> ProverState -> Bool
$c< :: ProverState -> ProverState -> Bool
compare :: ProverState -> ProverState -> Ordering
$ccompare :: ProverState -> ProverState -> Ordering
$cp1Ord :: Eq ProverState
Ord, ProverState -> ProverState -> Bool
(ProverState -> ProverState -> Bool)
-> (ProverState -> ProverState -> Bool) -> Eq ProverState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProverState -> ProverState -> Bool
$c/= :: ProverState -> ProverState -> Bool
== :: ProverState -> ProverState -> Bool
$c== :: ProverState -> ProverState -> Bool
Eq, Typeable ProverState
Constr
DataType
Typeable ProverState =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> ProverState -> c ProverState)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ProverState)
-> (ProverState -> Constr)
-> (ProverState -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ProverState))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c ProverState))
-> ((forall b. Data b => b -> b) -> ProverState -> ProverState)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ProverState -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ProverState -> r)
-> (forall u. (forall d. Data d => d -> u) -> ProverState -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ProverState -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ProverState -> m ProverState)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ProverState -> m ProverState)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ProverState -> m ProverState)
-> Data ProverState
ProverState -> Constr
ProverState -> DataType
(forall b. Data b => b -> b) -> ProverState -> ProverState
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProverState -> c ProverState
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProverState
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> ProverState -> u
forall u. (forall d. Data d => d -> u) -> ProverState -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProverState -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProverState -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ProverState -> m ProverState
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProverState -> m ProverState
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProverState
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProverState -> c ProverState
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProverState)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ProverState)
$cProverState :: Constr
$tProverState :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ProverState -> m ProverState
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProverState -> m ProverState
gmapMp :: (forall d. Data d => d -> m d) -> ProverState -> m ProverState
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ProverState -> m ProverState
gmapM :: (forall d. Data d => d -> m d) -> ProverState -> m ProverState
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ProverState -> m ProverState
gmapQi :: Int -> (forall d. Data d => d -> u) -> ProverState -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ProverState -> u
gmapQ :: (forall d. Data d => d -> u) -> ProverState -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ProverState -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProverState -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ProverState -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProverState -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ProverState -> r
gmapT :: (forall b. Data b => b -> b) -> ProverState -> ProverState
$cgmapT :: (forall b. Data b => b -> b) -> ProverState -> ProverState
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ProverState)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ProverState)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ProverState)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ProverState)
dataTypeOf :: ProverState -> DataType
$cdataTypeOf :: ProverState -> DataType
toConstr :: ProverState -> Constr
$ctoConstr :: ProverState -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProverState
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ProverState
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProverState -> c ProverState
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ProverState -> c ProverState
$cp1Data :: Typeable ProverState
Data, Typeable)

tptpProverState :: Sign -- ^ TPTP signature
            -> [Named Sentence]
               -- ^ list of named TPTP sentences containing axioms
            -> [FreeDefMorphism Sentence Morphism] -- ^ freeness constraints
            -> ProverState
tptpProverState :: Sign
-> [Named Sentence]
-> [FreeDefMorphism Sentence Morphism]
-> ProverState
tptpProverState _ sentences :: [Named Sentence]
sentences _ = ProverState :: PLogicalPart -> ProverState
ProverState {
  psLogicalPart :: PLogicalPart
psLogicalPart = (Named Sentence -> PLogicalPart -> PLogicalPart)
-> PLogicalPart -> [Named Sentence] -> PLogicalPart
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((PLogicalPart -> Named Sentence -> PLogicalPart)
-> Named Sentence -> PLogicalPart -> PLogicalPart
forall a b c. (a -> b -> c) -> b -> a -> c
flip PLogicalPart -> Named Sentence -> PLogicalPart
insertSentence) PLogicalPart
emptyPLogicalPart [Named Sentence]
axiomList}
  where newSentences :: [Named Sentence]
newSentences = ShowS -> [Named Sentence] -> [Named Sentence]
forall a. ShowS -> [Named a] -> [Named a]
prepareSenNames ShowS
forall a. a -> a
id [Named Sentence]
sentences
        axiomList :: [Named Sentence]
axiomList = (Named Sentence -> Bool) -> [Named Sentence] -> [Named Sentence]
forall a. (a -> Bool) -> [a] -> [a]
filter Named Sentence -> Bool
forall s a. SenAttr s a -> Bool
isAxiom [Named Sentence]
newSentences

-- ** proving Logical Parts

{- |
  A proving logical part consists of a symbol list, a declaration list, and a
  set of formula lists. Support for clause lists and proof lists hasn't
  been implemented yet.
-}
data PLogicalPart = PLogicalPart { PLogicalPart -> [Named Sentence]
formulaeList :: [Named Sentence]
                                 } deriving (Int -> PLogicalPart -> ShowS
[PLogicalPart] -> ShowS
PLogicalPart -> String
(Int -> PLogicalPart -> ShowS)
-> (PLogicalPart -> String)
-> ([PLogicalPart] -> ShowS)
-> Show PLogicalPart
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PLogicalPart] -> ShowS
$cshowList :: [PLogicalPart] -> ShowS
show :: PLogicalPart -> String
$cshow :: PLogicalPart -> String
showsPrec :: Int -> PLogicalPart -> ShowS
$cshowsPrec :: Int -> PLogicalPart -> ShowS
Show, PLogicalPart -> PLogicalPart -> Bool
(PLogicalPart -> PLogicalPart -> Bool)
-> (PLogicalPart -> PLogicalPart -> Bool) -> Eq PLogicalPart
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PLogicalPart -> PLogicalPart -> Bool
$c/= :: PLogicalPart -> PLogicalPart -> Bool
== :: PLogicalPart -> PLogicalPart -> Bool
$c== :: PLogicalPart -> PLogicalPart -> Bool
Eq, Eq PLogicalPart
Eq PLogicalPart =>
(PLogicalPart -> PLogicalPart -> Ordering)
-> (PLogicalPart -> PLogicalPart -> Bool)
-> (PLogicalPart -> PLogicalPart -> Bool)
-> (PLogicalPart -> PLogicalPart -> Bool)
-> (PLogicalPart -> PLogicalPart -> Bool)
-> (PLogicalPart -> PLogicalPart -> PLogicalPart)
-> (PLogicalPart -> PLogicalPart -> PLogicalPart)
-> Ord PLogicalPart
PLogicalPart -> PLogicalPart -> Bool
PLogicalPart -> PLogicalPart -> Ordering
PLogicalPart -> PLogicalPart -> PLogicalPart
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 :: PLogicalPart -> PLogicalPart -> PLogicalPart
$cmin :: PLogicalPart -> PLogicalPart -> PLogicalPart
max :: PLogicalPart -> PLogicalPart -> PLogicalPart
$cmax :: PLogicalPart -> PLogicalPart -> PLogicalPart
>= :: PLogicalPart -> PLogicalPart -> Bool
$c>= :: PLogicalPart -> PLogicalPart -> Bool
> :: PLogicalPart -> PLogicalPart -> Bool
$c> :: PLogicalPart -> PLogicalPart -> Bool
<= :: PLogicalPart -> PLogicalPart -> Bool
$c<= :: PLogicalPart -> PLogicalPart -> Bool
< :: PLogicalPart -> PLogicalPart -> Bool
$c< :: PLogicalPart -> PLogicalPart -> Bool
compare :: PLogicalPart -> PLogicalPart -> Ordering
$ccompare :: PLogicalPart -> PLogicalPart -> Ordering
$cp1Ord :: Eq PLogicalPart
Ord, Typeable, Typeable PLogicalPart
Constr
DataType
Typeable PLogicalPart =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> PLogicalPart -> c PLogicalPart)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c PLogicalPart)
-> (PLogicalPart -> Constr)
-> (PLogicalPart -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c PLogicalPart))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c PLogicalPart))
-> ((forall b. Data b => b -> b) -> PLogicalPart -> PLogicalPart)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PLogicalPart -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PLogicalPart -> r)
-> (forall u. (forall d. Data d => d -> u) -> PLogicalPart -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> PLogicalPart -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PLogicalPart -> m PLogicalPart)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PLogicalPart -> m PLogicalPart)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PLogicalPart -> m PLogicalPart)
-> Data PLogicalPart
PLogicalPart -> Constr
PLogicalPart -> DataType
(forall b. Data b => b -> b) -> PLogicalPart -> PLogicalPart
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PLogicalPart -> c PLogicalPart
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PLogicalPart
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> PLogicalPart -> u
forall u. (forall d. Data d => d -> u) -> PLogicalPart -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PLogicalPart -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PLogicalPart -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PLogicalPart -> m PLogicalPart
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PLogicalPart -> m PLogicalPart
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PLogicalPart
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PLogicalPart -> c PLogicalPart
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PLogicalPart)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PLogicalPart)
$cPLogicalPart :: Constr
$tPLogicalPart :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> PLogicalPart -> m PLogicalPart
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PLogicalPart -> m PLogicalPart
gmapMp :: (forall d. Data d => d -> m d) -> PLogicalPart -> m PLogicalPart
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PLogicalPart -> m PLogicalPart
gmapM :: (forall d. Data d => d -> m d) -> PLogicalPart -> m PLogicalPart
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PLogicalPart -> m PLogicalPart
gmapQi :: Int -> (forall d. Data d => d -> u) -> PLogicalPart -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PLogicalPart -> u
gmapQ :: (forall d. Data d => d -> u) -> PLogicalPart -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PLogicalPart -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PLogicalPart -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PLogicalPart -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PLogicalPart -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PLogicalPart -> r
gmapT :: (forall b. Data b => b -> b) -> PLogicalPart -> PLogicalPart
$cgmapT :: (forall b. Data b => b -> b) -> PLogicalPart -> PLogicalPart
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PLogicalPart)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PLogicalPart)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c PLogicalPart)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PLogicalPart)
dataTypeOf :: PLogicalPart -> DataType
$cdataTypeOf :: PLogicalPart -> DataType
toConstr :: PLogicalPart -> Constr
$ctoConstr :: PLogicalPart -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PLogicalPart
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PLogicalPart
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PLogicalPart -> c PLogicalPart
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PLogicalPart -> c PLogicalPart
$cp1Data :: Typeable PLogicalPart
Data)

emptyPLogicalPart :: PLogicalPart
emptyPLogicalPart :: PLogicalPart
emptyPLogicalPart = PLogicalPart :: [Named Sentence] -> PLogicalPart
PLogicalPart { formulaeList :: [Named Sentence]
formulaeList = [] }

-- | gets all axioms possibly used in a proof
getAxioms :: ProverState -> [String]
getAxioms :: ProverState -> [String]
getAxioms = (Named Sentence -> String) -> [Named Sentence] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Named Sentence -> String
forall s a. SenAttr s a -> a
senAttr ([Named Sentence] -> [String])
-> (ProverState -> [Named Sentence]) -> ProverState -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named Sentence -> Bool) -> [Named Sentence] -> [Named Sentence]
forall a. (a -> Bool) -> [a] -> [a]
filter Named Sentence -> Bool
forall s a. SenAttr s a -> Bool
isAxiom ([Named Sentence] -> [Named Sentence])
-> (ProverState -> [Named Sentence])
-> ProverState
-> [Named Sentence]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PLogicalPart -> [Named Sentence]
formulaeList (PLogicalPart -> [Named Sentence])
-> (ProverState -> PLogicalPart) -> ProverState -> [Named Sentence]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProverState -> PLogicalPart
psLogicalPart

-- * TPTP specific functions for prover GUI

-- Inserts a named TPTP term into TPTP prover state.
insertSentenceIntoProverState :: ProverState
                                 -- ^ prover state containing initial logical part
                              -> Named Sentence -- ^ goal to add
                              -> ProverState
insertSentenceIntoProverState :: ProverState -> Named Sentence -> ProverState
insertSentenceIntoProverState proverState :: ProverState
proverState namedSentence :: Named Sentence
namedSentence =
  ProverState
proverState { psLogicalPart :: PLogicalPart
psLogicalPart =
                  PLogicalPart -> Named Sentence -> PLogicalPart
insertSentence (ProverState -> PLogicalPart
psLogicalPart ProverState
proverState) Named Sentence
namedSentence }

{- |
  Inserts a Named Sentence (axiom or goal) into a PLogicalPart.
-}
insertSentence :: PLogicalPart -> Named Sentence -> PLogicalPart
insertSentence :: PLogicalPart -> Named Sentence -> PLogicalPart
insertSentence pLogicalPart :: PLogicalPart
pLogicalPart newSentence :: Named Sentence
newSentence =
  PLogicalPart
pLogicalPart { formulaeList :: [Named Sentence]
formulaeList = Named Sentence
newSentence Named Sentence -> [Named Sentence] -> [Named Sentence]
forall a. a -> [a] -> [a]
: PLogicalPart -> [Named Sentence]
formulaeList PLogicalPart
pLogicalPart }


{- |
  Generate a TPTP problem with time stamp while maybe adding a goal.
-}
generateTPTPProblem :: PLogicalPart
                    -> Maybe (Named Sentence) -> PProblem
generateTPTPProblem :: PLogicalPart -> Maybe (Named Sentence) -> PProblem
generateTPTPProblem pLogicalPart :: PLogicalPart
pLogicalPart mNewGoal :: Maybe (Named Sentence)
mNewGoal = PProblem :: String -> PLogicalPart -> PProblem
PProblem
    { identifier :: String
identifier = "hets_exported"
    , logicalPart :: PLogicalPart
logicalPart = PLogicalPart
-> (Named Sentence -> PLogicalPart)
-> Maybe (Named Sentence)
-> PLogicalPart
forall b a. b -> (a -> b) -> Maybe a -> b
maybe PLogicalPart
pLogicalPart (PLogicalPart -> Named Sentence -> PLogicalPart
insertSentence PLogicalPart
pLogicalPart) Maybe (Named Sentence)
mNewGoal
    }

showTPTPProblemM
    :: String -- ^ theory name
    -> ProverState -- ^ prover state containing initial logical part
    -> [String] -- ^ extra options
    -> IO String -- ^ formatted output of the goal
showTPTPProblemM :: String -> ProverState -> [String] -> IO String
showTPTPProblemM thName :: String
thName pst :: ProverState
pst _opts :: [String]
_opts = do
  let problem :: PProblem
problem = PLogicalPart -> Maybe (Named Sentence) -> PProblem
generateTPTPProblem
                  (ProverState -> PLogicalPart
psLogicalPart ProverState
pst)
                   Maybe (Named Sentence)
forall a. Maybe a
Nothing
  String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ String -> PProblem -> Doc
printTPTPProblem String
thName PProblem
problem

{- |
  Pretty printing TPTP goal in TPTP format.
-}
ioShowTPTPProblem :: String -- ^ theory name
                  -> ProverState -- ^ prover state containing initial logical part
                  -> Named Sentence -- ^ goal to print
                  -> [String] -- ^ extra options
                  -> IO String -- ^ formatted output of the goal
ioShowTPTPProblem :: String -> ProverState -> Named Sentence -> [String] -> IO String
ioShowTPTPProblem theoryName :: String
theoryName proverState :: ProverState
proverState newGoal :: Named Sentence
newGoal _ = do
  let problem :: PProblem
problem = PLogicalPart -> Maybe (Named Sentence) -> PProblem
generateTPTPProblem
                  (ProverState -> PLogicalPart
psLogicalPart ProverState
proverState)
                  (Named Sentence -> Maybe (Named Sentence)
forall a. a -> Maybe a
Just Named Sentence
newGoal)
  String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ String -> PProblem -> Doc
printTPTPProblem String
theoryName PProblem
problem

-- Print a newline at the end of the document for good style.
printTPTPProblem :: String -> PProblem -> Doc
printTPTPProblem :: String -> PProblem -> Doc
printTPTPProblem theoryName :: String
theoryName problem :: PProblem
problem =
  String -> Doc
text "% Problem: " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text (PProblem -> String
identifier PProblem
problem)
  Doc -> Doc -> Doc
$+$ String -> Doc
text "% generated from the library " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
theoryName
  Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vsep ((Named Sentence -> Doc) -> [Named Sentence] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Named Sentence -> Doc
printNamedSentence ([Named Sentence] -> [Doc]) -> [Named Sentence] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Named Sentence -> Named Sentence -> Ordering)
-> [Named Sentence] -> [Named Sentence]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy Named Sentence -> Named Sentence -> Ordering
sentenceOrder ([Named Sentence] -> [Named Sentence])
-> [Named Sentence] -> [Named Sentence]
forall a b. (a -> b) -> a -> b
$ PLogicalPart -> [Named Sentence]
formulaeList (PLogicalPart -> [Named Sentence])
-> PLogicalPart -> [Named Sentence]
forall a b. (a -> b) -> a -> b
$
             PProblem -> PLogicalPart
logicalPart PProblem
problem)
  Doc -> Doc -> Doc
$+$ String -> Doc
text ""
  where
    sentenceOrder :: Named Sentence -> Named Sentence -> Ordering
    sentenceOrder :: Named Sentence -> Named Sentence -> Ordering
sentenceOrder s :: Named Sentence
s t :: Named Sentence
t =
      case (Sentence -> Formula_role
formulaRole (Sentence -> Formula_role) -> Sentence -> Formula_role
forall a b. (a -> b) -> a -> b
$ Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
s, Sentence -> Formula_role
formulaRole (Sentence -> Formula_role) -> Sentence -> Formula_role
forall a b. (a -> b) -> a -> b
$ Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
t) of
        (Unknown, _) -> Ordering
LT
        (Type, _) -> Ordering
LT
        (Definition, _) -> Ordering
LT
        (Conjecture, _) -> Ordering
GT
        (_, _) -> Ordering
EQ