{- |
Module      :  ./SoftFOL/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 SoftFOL.ProverState where

import Logic.Prover

import SoftFOL.Sign
import SoftFOL.Conversions
import SoftFOL.Translate
import SoftFOL.PrintTPTP
import SoftFOL.Print ()

import qualified Common.AS_Annotation as AS_Anno
import Common.ProofUtils
import Common.Utils (splitOn)
import Common.DocUtils

-- * Data structures

data SoftFOLProverState = SoftFOLProverState
    { SoftFOLProverState -> SPLogicalPart
initialLogicalPart :: SPLogicalPart}

-- * SoftFOL specific functions for prover GUI

{- |
  Creates an initial SoftFOL prover state with logical part.
-}
spassProverState
    :: Sign -- ^ SoftFOL signature
    -> [AS_Anno.Named SPTerm]
       -- ^ list of named SoftFOL terms containing axioms
    -> [FreeDefMorphism SPTerm SoftFOLMorphism]  -- ^ freeness constraints
    -> SoftFOLProverState
spassProverState :: Sign
-> [Named SPTerm]
-> [FreeDefMorphism SPTerm SoftFOLMorphism]
-> SoftFOLProverState
spassProverState sign :: Sign
sign oSens' :: [Named SPTerm]
oSens' _ = SoftFOLProverState :: SPLogicalPart -> SoftFOLProverState
SoftFOLProverState {
    initialLogicalPart :: SPLogicalPart
initialLogicalPart = (SPLogicalPart -> Named SPTerm -> SPLogicalPart)
-> SPLogicalPart -> [Named SPTerm] -> SPLogicalPart
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl SPLogicalPart -> Named SPTerm -> SPLogicalPart
insertSentence
                               (Sign -> SPLogicalPart
signToSPLogicalPart Sign
sign)
                               ([Named SPTerm] -> [Named SPTerm]
forall a. [a] -> [a]
reverse [Named SPTerm]
axiomList)}
  where nSens :: [Named SPTerm]
nSens = (String -> String) -> [Named SPTerm] -> [Named SPTerm]
forall a. (String -> String) -> [Named a] -> [Named a]
prepareSenNames String -> String
transSenName [Named SPTerm]
oSens'
        axiomList :: [Named SPTerm]
axiomList = (Named SPTerm -> Bool) -> [Named SPTerm] -> [Named SPTerm]
forall a. (a -> Bool) -> [a] -> [a]
filter Named SPTerm -> Bool
forall s a. SenAttr s a -> Bool
AS_Anno.isAxiom [Named SPTerm]
nSens

{- |
  Inserts a named SoftFOL term into SoftFOL prover state.
-}
insertSentenceGen
    :: SoftFOLProverState
       -- ^ prover state containing initial logical part
    -> AS_Anno.Named SPTerm -- ^ goal to add
    -> SoftFOLProverState
insertSentenceGen :: SoftFOLProverState -> Named SPTerm -> SoftFOLProverState
insertSentenceGen pst :: SoftFOLProverState
pst s :: Named SPTerm
s = SoftFOLProverState
pst {initialLogicalPart :: SPLogicalPart
initialLogicalPart =
                                SPLogicalPart -> Named SPTerm -> SPLogicalPart
insertSentence (SoftFOLProverState -> SPLogicalPart
initialLogicalPart SoftFOLProverState
pst) Named SPTerm
s}

{- |
  Pretty printing SoftFOL goal in DFG format.
-}
showDFGProblem
    :: String -- ^ theory name
    -> SoftFOLProverState
       -- ^ prover state containing initial logical part
    -> AS_Anno.Named SPTerm -- ^ goal to print
    -> [String] -- ^ extra options
    -> IO String -- ^ formatted output of the goal
showDFGProblem :: String
-> SoftFOLProverState -> Named SPTerm -> [String] -> IO String
showDFGProblem thName :: String
thName pst :: SoftFOLProverState
pst nGoal :: Named SPTerm
nGoal opts :: [String]
opts = do
  SPProblem
prob <- String -> SPLogicalPart -> Maybe (Named SPTerm) -> IO SPProblem
genSoftFOLProblem String
thName (SoftFOLProverState -> SPLogicalPart
initialLogicalPart SoftFOLProverState
pst) (Maybe (Named SPTerm) -> IO SPProblem)
-> Maybe (Named SPTerm) -> IO SPProblem
forall a b. (a -> b) -> a -> b
$ Named SPTerm -> Maybe (Named SPTerm)
forall a. a -> Maybe a
Just Named SPTerm
nGoal
  -- add SPASS command line settings and extra options
  let prob' :: SPProblem
prob' = SPProblem
prob { settings :: [SPSetting]
settings = SPProblem -> [SPSetting]
settings SPProblem
prob [SPSetting] -> [SPSetting] -> [SPSetting]
forall a. [a] -> [a] -> [a]
++ [String] -> [SPSetting]
parseSPASSCommands [String]
opts }
  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
$ SPProblem -> String -> String
forall a. Pretty a => a -> String -> String
showDoc SPProblem
prob' ""

{- |
  Pretty printing SoftFOL-model-finding-problem in TPTP format.
-}
showTPTPProblemM
    :: String -- ^ theory name
    -> SoftFOLProverState -- ^ prover state containing initial logical part
    -> [String] -- ^ extra options
    -> IO String -- ^ formatted output of the goal
showTPTPProblemM :: String -> SoftFOLProverState -> [String] -> IO String
showTPTPProblemM thName :: String
thName pst :: SoftFOLProverState
pst = String
-> SoftFOLProverState
-> Maybe (Named SPTerm)
-> [String]
-> IO String
showTPTPProblemAux String
thName SoftFOLProverState
pst Maybe (Named SPTerm)
forall a. Maybe a
Nothing

{- |
  Pretty printing SoftFOL goal in TPTP format.
-}
showTPTPProblem
    :: String -- ^ theory name
    -> SoftFOLProverState -- ^ prover state containing initial logical part
    -> AS_Anno.Named SPTerm -- ^ goal to print
    -> [String] -- ^ extra options
    -> IO String -- ^ formatted output of the goal
showTPTPProblem :: String
-> SoftFOLProverState -> Named SPTerm -> [String] -> IO String
showTPTPProblem thName :: String
thName pst :: SoftFOLProverState
pst = String
-> SoftFOLProverState
-> Maybe (Named SPTerm)
-> [String]
-> IO String
showTPTPProblemAux String
thName SoftFOLProverState
pst (Maybe (Named SPTerm) -> [String] -> IO String)
-> (Named SPTerm -> Maybe (Named SPTerm))
-> Named SPTerm
-> [String]
-> IO String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named SPTerm -> Maybe (Named SPTerm)
forall a. a -> Maybe a
Just

showTPTPProblemAux
    :: String -- ^ theory name
    -> SoftFOLProverState -- ^ prover state containing initial logical part
    -> Maybe (AS_Anno.Named SPTerm) -- ^ possible goal to print
    -> [String] -- ^ extra options
    -> IO String -- ^ formatted output of the goal
showTPTPProblemAux :: String
-> SoftFOLProverState
-> Maybe (Named SPTerm)
-> [String]
-> IO String
showTPTPProblemAux thName :: String
thName pst :: SoftFOLProverState
pst mGoal :: Maybe (Named SPTerm)
mGoal opts :: [String]
opts = do
  SPProblem
prob <- String -> SPLogicalPart -> Maybe (Named SPTerm) -> IO SPProblem
genSoftFOLProblem String
thName (SoftFOLProverState -> SPLogicalPart
initialLogicalPart SoftFOLProverState
pst) Maybe (Named SPTerm)
mGoal
  -- add extra options as SPSettings with only one field filled
  let prob' :: SPProblem
prob' = SPProblem
prob { settings :: [SPSetting]
settings = SPProblem -> [SPSetting]
settings SPProblem
prob
                                [SPSetting] -> [SPSetting] -> [SPSetting]
forall a. [a] -> [a] -> [a]
++ [SPSettingLabel -> [SPSettingBody] -> SPSetting
SPSettings SPSettingLabel
SPASS
                                     ([SPSettingBody] -> SPSetting) -> [SPSettingBody] -> SPSetting
forall a b. (a -> b) -> a -> b
$ (String -> SPSettingBody) -> [String] -> [SPSettingBody]
forall a b. (a -> b) -> [a] -> [b]
map (\ opt :: String
opt ->
                                           String -> [String] -> SPSettingBody
SPFlag "set_flag" [String
opt]) [String]
opts] }
  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
$ SPProblem -> Doc
forall a. PrintTPTP a => a -> Doc
printTPTP SPProblem
prob'

-- | Translates SPASS command line into [SPSetting]
parseSPASSCommands :: [String] -- ^ SPASS command line options
                   -> [SPSetting] -- ^ parsed parameters and options
parseSPASSCommands :: [String] -> [SPSetting]
parseSPASSCommands comLine :: [String]
comLine =
    [SPSettingLabel -> [SPSettingBody] -> SPSetting
SPSettings SPSettingLabel
SPASS ([SPSettingBody] -> SPSetting) -> [SPSettingBody] -> SPSetting
forall a b. (a -> b) -> a -> b
$
            (String -> SPSettingBody) -> [String] -> [SPSettingBody]
forall a b. (a -> b) -> [a] -> [b]
map (\ opt :: String
opt -> case Char -> String -> [String]
forall a. Eq a => a -> [a] -> [[a]]
splitOn '=' (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '-') String
opt of
                 [] -> String -> SPSettingBody
forall a. HasCallStack => String -> a
error "parseSPASSCommands"
                 [h :: String
h] -> String -> [String] -> SPSettingBody
SPFlag "set_flag" [String
h, "1"]
                   -- if multiple '=', texts are concatenated
                 h :: String
h : r :: [String]
r -> String -> [String] -> SPSettingBody
SPFlag "set_flag" [String
h, [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String]
r]
                ) [String]
comLine ]

-- | get all axioms possibly used in a proof
getAxioms :: SoftFOLProverState -> [String]
getAxioms :: SoftFOLProverState -> [String]
getAxioms = (Named SPTerm -> String) -> [Named SPTerm] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Named SPTerm -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr ([Named SPTerm] -> [String])
-> (SoftFOLProverState -> [Named SPTerm])
-> SoftFOLProverState
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SPFormulaList -> [Named SPTerm])
-> [SPFormulaList] -> [Named SPTerm]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SPFormulaList -> [Named SPTerm]
formulae ([SPFormulaList] -> [Named SPTerm])
-> (SoftFOLProverState -> [SPFormulaList])
-> SoftFOLProverState
-> [Named SPTerm]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SPFormulaList -> Bool) -> [SPFormulaList] -> [SPFormulaList]
forall a. (a -> Bool) -> [a] -> [a]
filter SPFormulaList -> Bool
isAxiomFormula
  ([SPFormulaList] -> [SPFormulaList])
-> (SoftFOLProverState -> [SPFormulaList])
-> SoftFOLProverState
-> [SPFormulaList]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPLogicalPart -> [SPFormulaList]
formulaLists (SPLogicalPart -> [SPFormulaList])
-> (SoftFOLProverState -> SPLogicalPart)
-> SoftFOLProverState
-> [SPFormulaList]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SoftFOLProverState -> SPLogicalPart
initialLogicalPart