b87033953be26b0dc7dead8febd499b666a54126Peter Major{- |

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter MajorModule : ./SoftFOL/ProverState.hs

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter MajorDescription : Help functions for all automatic theorem provers.

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter MajorCopyright : (c) Rainer Grabbe

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter MajorLicense : GPLv2 or higher, see LICENSE.txt

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter Major

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter MajorMaintainer : Christian.Maeder@dfki.de

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter MajorStability : provisional

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter MajorPortability : needs POSIX

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter Major

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter MajorData structures and initialising functions for Prover state and configurations.

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter Major

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter Major-}

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter Major

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter Majormodule SoftFOL.ProverState where

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter Major

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter Majorimport Logic.Prover

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter Major

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter Majorimport SoftFOL.Sign

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter Majorimport SoftFOL.Conversions

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter Majorimport SoftFOL.Translate

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter Majorimport SoftFOL.PrintTPTP

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter Majorimport SoftFOL.Print ()

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter Major

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter Majorimport qualified Common.AS_Annotation as AS_Anno

b87033953be26b0dc7dead8febd499b666a54126Peter Majorimport Common.ProofUtils

b87033953be26b0dc7dead8febd499b666a54126Peter Majorimport Common.Utils (splitOn)

b87033953be26b0dc7dead8febd499b666a54126Peter Majorimport Common.DocUtils

b87033953be26b0dc7dead8febd499b666a54126Peter Major

b87033953be26b0dc7dead8febd499b666a54126Peter Major-- * Data structures

b87033953be26b0dc7dead8febd499b666a54126Peter Major

a622f6b14edb724c3cdbc8b5836a109d4ac80086Peter Majordata SoftFOLProverState = SoftFOLProverState

b87033953be26b0dc7dead8febd499b666a54126Peter Major { initialLogicalPart :: SPLogicalPart}

a149d11dfee7bcc667e71ec330b7566dd0437c1fjeff.schenk

b87033953be26b0dc7dead8febd499b666a54126Peter Major-- * SoftFOL specific functions for prover GUI

b87033953be26b0dc7dead8febd499b666a54126Peter Major

b87033953be26b0dc7dead8febd499b666a54126Peter Major{- |

b87033953be26b0dc7dead8febd499b666a54126Peter Major Creates an initial SoftFOL prover state with logical part.

b87033953be26b0dc7dead8febd499b666a54126Peter Major-}

b87033953be26b0dc7dead8febd499b666a54126Peter MajorspassProverState

b87033953be26b0dc7dead8febd499b666a54126Peter Major :: Sign -- ^ SoftFOL signature

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> [AS_Anno.Named SPTerm]

b87033953be26b0dc7dead8febd499b666a54126Peter Major -- ^ list of named SoftFOL terms containing axioms

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> SoftFOLProverState

b87033953be26b0dc7dead8febd499b666a54126Peter MajorspassProverState sign oSens' _ = SoftFOLProverState {

b87033953be26b0dc7dead8febd499b666a54126Peter Major initialLogicalPart = foldl insertSentence

b87033953be26b0dc7dead8febd499b666a54126Peter Major (signToSPLogicalPart sign)

b87033953be26b0dc7dead8febd499b666a54126Peter Major (reverse axiomList)}

b87033953be26b0dc7dead8febd499b666a54126Peter Major where nSens = prepareSenNames transSenName oSens'

b87033953be26b0dc7dead8febd499b666a54126Peter Major axiomList = filter AS_Anno.isAxiom nSens

b87033953be26b0dc7dead8febd499b666a54126Peter Major

b87033953be26b0dc7dead8febd499b666a54126Peter Major{- |

b87033953be26b0dc7dead8febd499b666a54126Peter Major Inserts a named SoftFOL term into SoftFOL prover state.

b87033953be26b0dc7dead8febd499b666a54126Peter Major-}

b87033953be26b0dc7dead8febd499b666a54126Peter MajorinsertSentenceGen

b87033953be26b0dc7dead8febd499b666a54126Peter Major :: SoftFOLProverState

b87033953be26b0dc7dead8febd499b666a54126Peter Major -- ^ prover state containing initial logical part

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> AS_Anno.Named SPTerm -- ^ goal to add

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> SoftFOLProverState

b87033953be26b0dc7dead8febd499b666a54126Peter MajorinsertSentenceGen pst s = pst {initialLogicalPart =

b87033953be26b0dc7dead8febd499b666a54126Peter Major insertSentence (initialLogicalPart pst) s}

b87033953be26b0dc7dead8febd499b666a54126Peter Major

b87033953be26b0dc7dead8febd499b666a54126Peter Major{- |

b87033953be26b0dc7dead8febd499b666a54126Peter Major Pretty printing SoftFOL goal in DFG format.

b87033953be26b0dc7dead8febd499b666a54126Peter Major-}

b87033953be26b0dc7dead8febd499b666a54126Peter MajorshowDFGProblem

b87033953be26b0dc7dead8febd499b666a54126Peter Major :: String -- ^ theory name

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> SoftFOLProverState

b87033953be26b0dc7dead8febd499b666a54126Peter Major -- ^ prover state containing initial logical part

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> AS_Anno.Named SPTerm -- ^ goal to print

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> [String] -- ^ extra options

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> IO String -- ^ formatted output of the goal

b87033953be26b0dc7dead8febd499b666a54126Peter MajorshowDFGProblem thName pst nGoal opts = do

b87033953be26b0dc7dead8febd499b666a54126Peter Major prob <- genSoftFOLProblem thName (initialLogicalPart pst) $ Just nGoal

b87033953be26b0dc7dead8febd499b666a54126Peter Major -- add SPASS command line settings and extra options

b87033953be26b0dc7dead8febd499b666a54126Peter Major let prob' = prob { settings = settings prob ++ parseSPASSCommands opts }

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter Major return $ showDoc prob' ""

b87033953be26b0dc7dead8febd499b666a54126Peter Major

b87033953be26b0dc7dead8febd499b666a54126Peter Major{- |

dfc4e0fc3052835b2a069aa9d869fa1161c33fe6Peter Major Pretty printing SoftFOL-model-finding-problem in TPTP format.

b87033953be26b0dc7dead8febd499b666a54126Peter Major-}

b87033953be26b0dc7dead8febd499b666a54126Peter MajorshowTPTPProblemM

b87033953be26b0dc7dead8febd499b666a54126Peter Major :: String -- ^ theory name

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> SoftFOLProverState -- ^ prover state containing initial logical part

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> [String] -- ^ extra options

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> IO String -- ^ formatted output of the goal

b87033953be26b0dc7dead8febd499b666a54126Peter MajorshowTPTPProblemM thName pst = showTPTPProblemAux thName pst Nothing

b87033953be26b0dc7dead8febd499b666a54126Peter Major

b87033953be26b0dc7dead8febd499b666a54126Peter Major{- |

1f48f8236de7de97be1c6b9d06bef50b379c8801jenkins Pretty printing SoftFOL goal in TPTP format.

b87033953be26b0dc7dead8febd499b666a54126Peter Major-}

b87033953be26b0dc7dead8febd499b666a54126Peter MajorshowTPTPProblem

b87033953be26b0dc7dead8febd499b666a54126Peter Major :: String -- ^ theory name

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> SoftFOLProverState -- ^ prover state containing initial logical part

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> AS_Anno.Named SPTerm -- ^ goal to print

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> [String] -- ^ extra options

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> IO String -- ^ formatted output of the goal

b87033953be26b0dc7dead8febd499b666a54126Peter MajorshowTPTPProblem thName pst = showTPTPProblemAux thName pst . Just

23e304384f98fca4ab2e6f9f07a53465c1bfc645Peter Major

23e304384f98fca4ab2e6f9f07a53465c1bfc645Peter MajorshowTPTPProblemAux

23e304384f98fca4ab2e6f9f07a53465c1bfc645Peter Major :: String -- ^ theory name

23e304384f98fca4ab2e6f9f07a53465c1bfc645Peter Major -> SoftFOLProverState -- ^ prover state containing initial logical part

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> Maybe (AS_Anno.Named SPTerm) -- ^ possible goal to print

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> [String] -- ^ extra options

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> IO String -- ^ formatted output of the goal

b87033953be26b0dc7dead8febd499b666a54126Peter MajorshowTPTPProblemAux thName pst mGoal opts = do

b87033953be26b0dc7dead8febd499b666a54126Peter Major prob <- genSoftFOLProblem thName (initialLogicalPart pst) mGoal

b87033953be26b0dc7dead8febd499b666a54126Peter Major -- add extra options as SPSettings with only one field filled

b87033953be26b0dc7dead8febd499b666a54126Peter Major let prob' = prob { settings = settings prob

b87033953be26b0dc7dead8febd499b666a54126Peter Major ++ [SPSettings SPASS

b87033953be26b0dc7dead8febd499b666a54126Peter Major $ map (\ opt ->

b87033953be26b0dc7dead8febd499b666a54126Peter Major SPFlag "set_flag" [opt]) opts] }

b87033953be26b0dc7dead8febd499b666a54126Peter Major return $ show $ printTPTP prob'

b87033953be26b0dc7dead8febd499b666a54126Peter Major

b87033953be26b0dc7dead8febd499b666a54126Peter Major-- | Translates SPASS command line into [SPSetting]

b87033953be26b0dc7dead8febd499b666a54126Peter MajorparseSPASSCommands :: [String] -- ^ SPASS command line options

b87033953be26b0dc7dead8febd499b666a54126Peter Major -> [SPSetting] -- ^ parsed parameters and options

b87033953be26b0dc7dead8febd499b666a54126Peter MajorparseSPASSCommands comLine =

[SPSettings SPASS $

map (\ opt -> case splitOn '=' $ dropWhile (== '-') opt of

[] -> error "parseSPASSCommands"

[h] -> SPFlag "set_flag" [h, "1"]

-- if multiple '=', texts are concatenated

h : r -> SPFlag "set_flag" [h, concat r]

) comLine ]

-- | get all axioms possibly used in a proof

getAxioms :: SoftFOLProverState -> [String]

getAxioms = map AS_Anno.senAttr . concatMap formulae . filter isAxiomFormula

. formulaLists . initialLogicalPart