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 SoftFOLProverState = SoftFOLProverState
{ SoftFOLProverState -> SPLogicalPart
initialLogicalPart :: SPLogicalPart}
spassProverState
:: Sign
-> [AS_Anno.Named SPTerm]
-> [FreeDefMorphism SPTerm SoftFOLMorphism]
-> 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
insertSentenceGen
:: SoftFOLProverState
-> AS_Anno.Named SPTerm
-> 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}
showDFGProblem
:: String
-> SoftFOLProverState
-> AS_Anno.Named SPTerm
-> [String]
-> IO String
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
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' ""
showTPTPProblemM
:: String
-> SoftFOLProverState
-> [String]
-> IO String
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
showTPTPProblem
:: String
-> SoftFOLProverState
-> AS_Anno.Named SPTerm
-> [String]
-> IO String
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
-> SoftFOLProverState
-> Maybe (AS_Anno.Named SPTerm)
-> [String]
-> IO String
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
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'
parseSPASSCommands :: [String]
-> [SPSetting]
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"]
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 ]
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