GenericATPState.hs revision ad270004874ce1d0697fb30d7309f180553bb315
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederModule : $Header$
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederDescription : Help functions for GUI.GenericATP
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) Klaus L�ttich, Rainer Grabbe, Uni Bremen 2006
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : rainer25@tzi.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederPortability : ?
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaederData structures and initialising functions for Prover state and configurations.
c0c2380bced8159ff0297ece14eba948bd236471Christian Maederimport qualified Common.AS_Annotation as AS_Anno
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettichimport qualified Data.Map as Map
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maederimport qualified Data.Set as Set
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Common.OrderedMap as OMap
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder-- * Data Structures
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maedertype ATPIdentifier = String
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederdata GenericConfig proof_tree = GenericConfig {
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder -- | Time limit in seconds passed
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- to prover via extra option. Default will be used if Nothing.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder timeLimit :: Maybe Int,
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder -- | True if timelimit exceeded during last prover run.
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder timeLimitExceeded :: Bool,
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder -- | Extra options passed verbatimely to prover.
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder -- -DocProof, -Stdin, and -TimeLimit will be overridden.
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder extraOpts :: [String],
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder -- | Represents the result of a prover run.
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder proof_status :: Proof_status proof_tree,
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder resultOutput :: [String],
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder -- | global time used in milliseconds
c3053d57f642ca507cdf79512e604437c4546cb9Christian Maeder timeUsed :: Int
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder } deriving (Eq, Ord, Show)
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder Creates an empty GenericConfig with a given goal name.
05a62e84edac8c64de04f8349dee418598d216b9Christian Maeder Default time limit, no resultOutput and no extra options.
1aee4aaddde105264c1faf394d88e302c05094ffChristian MaederemptyConfig :: (Ord proof_tree) =>
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder String -- ^ name of the prover
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder -> String -- ^ name of the goal
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder -> proof_tree -- ^ initial empty proof_tree
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder -> GenericConfig proof_tree
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaederemptyConfig prName n pt =
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder GenericConfig {timeLimit = Nothing,
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder timeLimitExceeded = False,
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder extraOpts = [],
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder proof_status = openProof_status n prName pt,
b5da047a9a875dec3f968b6c0df96af326f90fa9Alexis Tsogias resultOutput = [],
014dc30f64ec25e4790cca987d4d1e6635430510Christian Maeder Performs a lookup on the ConfigsMap. Returns the config for the goal or an
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich empty config if none is set yet.
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian MaedergetConfig :: (Ord proof_tree) =>
feca1d35123d8c31aee238c9ce79947b0bf65494Christian Maeder String -- ^ name of the prover
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder -> ATPIdentifier -- ^ name of the goal
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder -> proof_tree -- ^ initial empty proof_tree
2a2c652d2445d76e28ca75da2a5392f8cf870820Christian Maeder -> GenericConfigsMap proof_tree
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder -> GenericConfig proof_tree
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian MaedergetConfig prName genid pt m = maybe (emptyConfig prName genid pt)
23ffcc44ca8612feccbd8fda63fa5be7ab5f9dc3Christian Maeder lookupId = Map.lookup genid m
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder We need to store one GenericConfig per goal.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maedertype GenericConfigsMap proof_tree = Map.Map ATPIdentifier
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (GenericConfig proof_tree)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Map to identifiers
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maedertype GenericGoalNameMap = Map.Map String String
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Represents the global state of the prover GUI.
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maederdata GenericState sign sentence proof_tree pst = GenericState {
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder -- | currently selected goal or Nothing
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder currentGoal :: Maybe ATPIdentifier,
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder -- | initial empty proof_tree
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder proof_tree :: proof_tree,
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder -- | stores the prover configurations for each goal
a42fbfe7becf0eae2d624123eb0db73a794593f0Christian Maeder -- and the results retrieved by running prover for each goal
a42fbfe7becf0eae2d624123eb0db73a794593f0Christian Maeder configsMap :: GenericConfigsMap proof_tree,
b363eb04791e7f735633b9b4088502c2bc50ebfcChristian Maeder -- | stores a mapping to SPASS compliant
a42fbfe7becf0eae2d624123eb0db73a794593f0Christian Maeder -- identifiers for all goals
1cd4f6541984962658add5cfaa9f28a93879881bChristian Maeder namesMap :: GenericGoalNameMap,
1cd4f6541984962658add5cfaa9f28a93879881bChristian Maeder -- | list of all goals
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder goalsList :: [AS_Anno.Named sentence],
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder -- | logical part without theorems
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder proverState :: pst
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder Initialising the specific prover state containing logical part.
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maedertype InitialProverState sign sentence pst =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder sign -> [AS_Anno.Named sentence] -> pst
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maedertype TransSenName = String -> String
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder Creates an initial GenericState around a Theory.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederinitialGenericState :: (Show sentence, Ord sentence, Ord proof_tree) =>
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder String -- ^ name of the prover
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> InitialProverState sign sentence pst
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder -> TransSenName
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder -> Theory sign sentence proof_tree
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder -> proof_tree -- ^ initial empty proof_tree
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder -> GenericState sign sentence proof_tree pst
b568982efd0997d877286faa592d81b03c8c67b8Christian MaederinitialGenericState prName ips trSenName th pt =
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder GenericState {currentGoal = Nothing,
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich proof_tree = pt,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ec = emptyConfig prName gName pt
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder in (gName, ec {proof_status =
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder updateTactic_script (proof_status ec) gName}))
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder namesMap = collectNameMapping nSens oSens',
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder goalsList = goals,
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder proverState = ips sign oSens'
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder where Theory sign oSens = th
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- Search in list of Proof_status for first occurence of an Open goal
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- with non-empty Tactic_script and update Tactic_script if found.
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder updateTactic_script prStat gn =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let validThmStatus = filter (\tStatus ->
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (goalStatus tStatus == Open) &&
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (not $ tacticScript tStatus == Tactic_script ""))
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder $ thmStatus senSt
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder in if null validThmStatus
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder else prStat { tacticScript = tacticScript
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder $ head validThmStatus })
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder oSens' = toNamedList oSens
e4f4d096e5e6d60dd91c746d0e833d0ac7a29c50Christian Maeder nSens = disambiguateSens Set.empty $ prepareSenNames trSenName oSens'
eb74267cf39e4e95f9eeb5c765f4c8dac33971b4Christian Maeder goals = filter (not . AS_Anno.isAxiom) nSens
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder Represents the general return value of a prover run.
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederdata ATPRetval
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder -- | prover completed successfully
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder -- | prover did not terminate before the time limit exceeded
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder | ATPTLimitExceeded
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder -- | an error occured while running the prover
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder | ATPError String
59138b404f12352d103eeffbeaeb3957b90e75fdChristian Maeder -- | ATP batch mode was stopped with killthread
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder | ATPBatchStopped
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder deriving (Eq, Show)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maedertype RunProver sentence proof_tree pst =
10883d13973c46cac98964b66ace7a52b2d059abChristian Maeder pst -- ^ prover state containing logical part
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder -> GenericConfig proof_tree -- ^ configuration to use
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder -> Bool -- ^ True means save problem file
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder -> String -- ^ name of the theory in the DevGraph
0e5b095a19790411e5352fa7cf57cb0388e70472Christian Maeder -> AS_Anno.Named sentence -- ^ goal to prove
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder -> IO (ATPRetval, GenericConfig proof_tree) -- ^ (retval, configuration with proof_status and complete output)
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder Prover specific functions
f1a913f880e409e7327b5deae95738b5448379a1Christian Maederdata ATPFunctions sign sentence proof_tree pst = ATPFunctions {
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder -- | initial prover specific state
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder initialProverState :: InitialProverState sign sentence pst,
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder -- | prover specific translation of goal name
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder atpTransSenName :: TransSenName,
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder -- | inserts a goal into prover state
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder atpInsertSentence :: pst -> AS_Anno.Named sentence -> pst,
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder -- | output of a goal in a prover specific format
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder goalOutput :: pst -> AS_Anno.Named sentence-> [String] -> IO String,
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder -- | help text
328a85c807f2a95c3f147d10b05927eaf862ebebChristian Maeder proverHelpText :: String,
a6db617ca58eb6a0587b6366e913107dfecb71b5Heng Jiang -- | environment variable containing time limit for batch time
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblett batchTimeEnv :: String,
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder -- | file extensions for all output formats
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder fileExtensions :: FileExtensions,
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder -- | runs the prover
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder runProver :: RunProver sentence proof_tree pst,
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers -- | list of all options the prover finally runs with
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder createProverOptions :: GenericConfig proof_tree -> [String]
d6697ad2479099b816203fd2c36f593c72c73c76Christian Maeder File extensions for all prover specific output formats.
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder Given extensions should begin with a dot.
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maederdata FileExtensions = FileExtensions {
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers -- | file extension for saving problem
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder problemOutput :: String,
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder -- | file extension for saving prover output
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder proverOutput :: String,
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder -- | file extension for saving theory configuration
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder theoryConfiguration :: String
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder Tactic script implementation for ATPs. Read and show functions are provided.
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maederdata ATPTactic_script = ATPTactic_script
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder { ts_timeLimit :: Int, -- ^ used time limit
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder ts_extraOpts :: [String] -- ^ used extra options (if any)
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder } deriving (Eq, Ord)
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maederinstance Show ATPTactic_script where
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder show ts = "Time limit: " ++ (show $ ts_timeLimit ts)
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder ++ "\nExtra options: " ++ (show $ ts_extraOpts ts)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederinstance Read ATPTactic_script where
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder readsPrec _ ts =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder let emptyATPTactic_script = ATPTactic_script {
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder ts_timeLimit = 0, ts_extraOpts = [] }
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder re_atp = mkRegex "Time limit: +([0-9]+).*\nExtra options: +(.*) *"
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder readMatch = matchRegex re_atp ts
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder in maybe [(emptyATPTactic_script, "")]
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder (\sl -> [(ATPTactic_script {
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder ts_timeLimit = (read $ sl !! 0) :: Int,
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder ts_extraOpts = (read $ sl !! 1) :: [String]}