DgCommands.hs revision 124c859ba4741d5e36d5d98634886b430b7af093
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknerModule :$Header$
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederDescription : CMDL interface development graph commands
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknerCopyright : uni-bremen and DFKI
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknerLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknerMaintainer : r.pascanu@jacobs-university.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknerPortability : portable
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCMDL.DgCommands contains all development graph commands
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elknerthat can be called from the CMDL interface
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner ( commandDgAll
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner , cDgThmHideShift
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner , cDgSelectAll
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner , selectANode
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner , wrapResultDg
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner , wrapResultDgAll
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner-- | Wraps Result structure around the result of a dg all style command
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian MaederwrapResultDgAll :: (LIB_NAME->LibEnv -> LibEnv) ->
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder LIB_NAME -> LibEnv -> Result LibEnv
e7757995211bd395dc79d26fe017d99375f7d2a6Christian MaederwrapResultDgAll fn lib_name lib_env
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder = let res = fn lib_name lib_env
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder in Result [] $ Just res
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder-- | Wraps Result structure around the result of a dg style command
ad270004874ce1d0697fb30d7309f180553bb315Christian MaederwrapResultDg :: (LIB_NAME->[LEdge DGLinkLab] -> LibEnv -> LibEnv) ->
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich LIB_NAME->[LEdge DGLinkLab] -> LibEnv -> Result LibEnv
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederwrapResultDg fn lib_name ls lib_env
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder = let res = fn lib_name ls lib_env
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder in Result [] $ Just res
fa8878c6145f652f615a04a5e9c15a1d1327bc92cmaeder-- | General function for implementing dg all style commands
ce5b44277ea06257548ff625e928cb1290c6d297cmaedercommandDgAll :: ( LIB_NAME->LibEnv->Result LibEnv) -> CMDL_State
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> IO CMDL_State
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedercommandDgAll fn state
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder = case i_state $ intState state of
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder -- just an error message and leave
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder -- the internal state intact so that
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder -- the interface can recover
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder return $ genErrorMsg "No library loaded" state
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder case fn (i_ln ist) (i_libEnv ist) of
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder Result _ (Just nwLibEnv) ->
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder -- Name of function is not known here, so an empty text is
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder -- added as name, in a later stage (Shell.hs) the name will
825a1e4ca1e768de4b4883c65a6cb1dce6aa0002Christian Maeder -- be inserted
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder return $ add2hist [IStateChange $ Just ist] $ state {
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder intState = (intState state) {
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder i_state=Just$ emptyIntIState nwLibEnv $ i_ln ist}
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder Result diag Nothing -> return $ genErrorMsg
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder (concat $ map diagString diag) state
4b4a0b61b72cf8478a5d4d5002bca9f699401363Christian Maeder-- | Generic function for a dg command, all other dg
4b4a0b61b72cf8478a5d4d5002bca9f699401363Christian Maeder-- commands are derived from this command by simply
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder-- specifing the function
bab2d88d650448628730ed3b65c9f99c52500e8cChristian MaedercommandDg :: (LIB_NAME -> [LEdge DGLinkLab]->LibEnv->
d62661e54e2662d53b583ae48609f5037701078dcmaeder Result LibEnv) -> String -> CMDL_State
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder -> IO CMDL_State
6a2dad705deefd1b7a7e09b84fd2d75f2213be47Christian MaedercommandDg fn input state
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder = case i_state $ intState state of
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder Nothing -> -- leave the internal state intact so
014dc30f64ec25e4790cca987d4d1e6635430510Christian Maeder -- that the interface can recover
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich return $ genErrorMsg "No library loaded" state
6aea82c63ba1d2efc0329bc784a14e521469ec20Christian Maeder Just ist -> do
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder let (_,edg,nbEdg,errs) = decomposeIntoGoals input
feca1d35123d8c31aee238c9ce79947b0bf65494Christian Maeder tmpErrs = prettyPrintErrList errs
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder case (edg,nbEdg) of
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder ([],[]) -> -- leave the internal state intact so
f5c0884429b01e74c6e658ded921fb2e16dfb478Christian Maeder -- that the interface can recover
db675e8302ddb0d6528088ce68f5e98a00e890e3Christian Maeder return $ genErrorMsg (tmpErrs++"No edges in input string\n")
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder let lsNodes = getAllNodes ist
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner lsEdges = getAllEdges ist
961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner -- compute the list of edges from the input
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner (errs',listEdges) = obtainEdgeList edg nbEdg lsNodes
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder tmpErrs' = tmpErrs ++ (prettyPrintErrList errs')
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder case listEdges of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder [] -> return $ genErrorMsg (tmpErrs' ++ "No edge in input string\n")
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner case fn (i_ln ist) listEdges (i_libEnv ist) of
961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner Result _ (Just nwLibEnv) ->
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder -- name added later !!
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder return $ add2hist [IStateChange $ Just ist]
dc679edd4ca027663212afdf00926ae2ce19b555Christian Maeder $ genMessage tmpErrs' []
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder intState = (intState state){
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder i_state=Just$ emptyIntIState nwLibEnv $ i_ln ist}
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Result diag Nothing -> return $ genErrorMsg
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (concat $ map diagString diag) state
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder-- | The function 'cUse' implements the Use commands, i.e.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- given a path it tries to load the library at that path
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedercUse::String ->CMDL_State -> IO CMDL_State
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedercUse input state
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder let opts = defaultHetcatsOpts
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder file = trim input
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder tmp <- case i_state $ intState state of
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder Nothing -> anaLib opts file
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder Just dgState ->
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner anaLibExt opts file $ i_libEnv dgState
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Nothing -> -- leave internal state intact so that
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- the interface can recover
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder return$ genErrorMsg ("Unable to load library "++input) state
961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner Just (nwLn, nwLibEnv) ->
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder intState = IntState {
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder i_hist = IntHistory { undoList = [],
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder redoList = []
961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner i_state = Just $ emptyIntIState nwLibEnv nwLn,
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder filename = file
961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner prompter = (prompter state) {
e6d5dbbc3308f05197868806e0b860f4f53875f1Christian Maeder fileLoaded = file }
961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner-- The only command that requires a list of nodes instead
961087225d1d2b9534152a346d1a3755ed952fcdJens ElknercDgThmHideShift :: String -> CMDL_State -> IO CMDL_State
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian MaedercDgThmHideShift input state
961087225d1d2b9534152a346d1a3755ed952fcdJens Elkner = case i_state $ intState state of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Nothing -> -- leave internal state intact so
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -- that the interface can recover
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder return $ genErrorMsg "No library loaded" state
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Just dgState -> do
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder let (nds,_,_,errs) = decomposeIntoGoals input
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder tmpErrs = prettyPrintErrList errs
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder [] -> -- leave internal state intact so
328a85c807f2a95c3f147d10b05927eaf862ebebChristian Maeder -- that the interface can recover
8fb127028cb7dd361e348a3252e33487f73428bcJonathan von Schroeder return $ genErrorMsg (tmpErrs++"No nodes in input string\n")
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder let lsNodes = getAllNodes dgState
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder (errs',listNodes) = obtainNodeList nds lsNodes
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers tmpErrs' = tmpErrs ++ (prettyPrintErrList errs')
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder case listNodes of
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder [] -> return $ genErrorMsg (tmpErrs'++"No nodes in input string\n")
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder Result diag nwLibEnv = theoremHideShiftFromList (i_ln dgState)
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder listNodes (i_libEnv dgState)
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder -- diag not used, how should it?
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers case nwLibEnv of
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Nothing -> return $ genErrorMsg (concat $ map diagString diag)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -- ADD TO HISTORY ??
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Just newEnv ->
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder return $ add2hist [IStateChange $ Just dgState] $
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder genMessage tmpErrs' []
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder (intState state) {
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder i_state =Just $ emptyIntIState newEnv $ i_ln dgState
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder-- selection commands
aded505f9b42cc38975559c2a5d175ae95de436bChristian MaederselectANode :: Int -> IntIState
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder -> [Int_NodeInfo]
aded505f9b42cc38975559c2a5d175ae95de436bChristian MaederselectANode x dgState
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder -- computes the theory of a given node
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder -- (i.e. solves DGRef cases and so on,
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder -- see CASL Reference Manual, p.294, Def 4.9)
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder gth n = computeTheory (i_libEnv dgState)
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder (i_ln dgState)
3554301a34639efb6c9961a8571775d0061284c9Christian Maeder nodeName t=case find(\(n,_)-> n==t) $ getAllNodes dgState of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Nothing -> "Unknown node"
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder Just (_,ll)-> getDGNodeName ll
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder case knownProversWithKind ProveCMDLautomatic of
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder Result _ Nothing -> []
db6729e623b4053149084ccf4b35e5308ac7e359Christian Maeder Result _ (Just kpMap) ->
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder -- if compute theory was successful give the
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder -- result as one element list, otherwise an
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder -- empty list
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder case gth x of
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder Result _ (Just th@(G_theory lid _ _ _ _)) ->
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder -- le not used and should be
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder let sl = sublogicOfTh th
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder tmp<-initialState
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder (getLIB_ID $ i_ln dgState) "_" ++(nodeName x)
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder (shrinkKnownProvers sl kpMap)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder (getProvers ProveCMDLautomatic sl $
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder filter hasModelExpansion $
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder findComorphismPaths logicGraph $
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder sublogicOfTh th
ac34194a668399bb8ef238da77c3a09e93fb253bChristian Maeder -- make so that nothing (no goals, no axioms) are
4fc9de0da898448f1d3597ebbd8c04a066464c21Christian Maeder -- selected initialy in the goal proof status
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder return (initNodeInfo tmp
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder { selectedGoals = take 1 $ selectedGoals tmp } x)
c208973c890b8f993297720fd0247bc7481d4304Christian Maeder-- | function swithces interface in proving mode and also
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder-- selects a list of nodes to be used inside this mode
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaedercDgSelect :: String -> CMDL_State -> IO CMDL_State
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian MaedercDgSelect input state
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder =case i_state $ intState state of
0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder Nothing -> -- leave internal state intact so
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder -- that the interface can recover
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder return $ genErrorMsg "No library loaded" state
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just dgState -> do
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder let (nds,_,_,errs) = decomposeIntoGoals input
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder tmpErrs = prettyPrintErrList errs
01e278bdd7dce13b9303ed3d79683d83c89d09f9Liam O'Reilly [] -> return $ genErrorMsg (tmpErrs++"No nodes in input string\n") state
5ad5dffe06818a13e1632b1119fbca7881085fc1Dominik Luecke case knownProversWithKind ProveCMDLautomatic of
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder Result _ Nothing ->
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder return $ genErrorMsg (tmpErrs++"No prover found\n") state
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder Result _ (Just _) ->
31d6d9286988dc31639d105841296759aeb743e0Jonathan von Schroeder -- list of all nodes
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescu let lsNodes = getAllNodes dgState
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder -- list of input nodes
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder (errs',listNodes) = obtainNodeList nds lsNodes
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder tmpErrs' = tmpErrs ++ (prettyPrintErrList errs')
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder case listNodes of
05a206508bc898f87fe6ab6e069814df3c29d303Dominik Luecke [] -> return $ genErrorMsg(tmpErrs'++"No nodes in input string\n")
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder -- elems is the list of all results (i.e.
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder -- concat of all one element lists)
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder elems = concatMap
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder (\x -> case x of
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski (n,_) -> selectANode n dgState
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder nwist = emptyIntIState (i_libEnv dgState) (i_ln dgState)
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder return $ add2hist [IStateChange $ Just dgState] $
0b349288edfa50fdf38fda1a14e1562d03f92574Christian Maeder genMessage tmpErrs' []
5afff1a0f62394414c33b06141175b3ab0b117a5Christian Maeder -- add the prove state to the status
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder -- containing all information selected
1b3a2f98d1cd01fc9e0591f69507e20526727559Dominik Luecke -- in the input
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich intState = (intState state) {
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder i_state = Just nwist {
f8e1a1eca871a26a535a4ee7d51902ba94b1db1eChristian Maeder elements = elems,
ea3bff3e547a1ac714d4db39c5efef95e02b2e7dChristian Maeder cComorphism = getIdComorphism elems
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder-- | Function switches the interface in proving mode by
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder-- selecting all nodes
76b9b2974795a6fb31f242fd032de3ff66df6204Christian MaedercDgSelectAll :: CMDL_State -> IO CMDL_State
74a992bd019d3319df2f21f9d358ff06cafb5f7eMihaela TurcucDgSelectAll state
8a78868bae2ec6838c87366c35c57e109154c51eChristian Maeder =case i_state $ intState state of
878a5ecd6acf973907e25e5be6e4a792ea19a05eEwaryst Schulz Nothing -> return $ genErrorMsg "No library loaded" state
878a5ecd6acf973907e25e5be6e4a792ea19a05eEwaryst Schulz Just dgState ->
c2e192ace9ef7cfb0e59563f1b24477b2b65cff3Dominik Dietrich case knownProversWithKind ProveCMDLautomatic of
6b75c206b317eb30a08d88a8f27e0295ffeb1546Christian Maeder Result _ Nothing -> return $ genErrorMsg "No prover found" state
9a4b469ca0a7f44a598e551a973c75195207db58Eugen Kuksa Result _ (Just _) ->
01645eac73dbc789392674930adc5745c935f3a0Christian Maeder -- list of all nodes
01645eac73dbc789392674930adc5745c935f3a0Christian Maeder let lsNodes = getAllNodes dgState
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder -- elems is the list of all results (i.e. concat
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder -- of all one element lists)
3a9fce5398f4621558ca220c66c87cee59adc258Jonathan von Schroeder elems = concatMap
b5da047a9a875dec3f968b6c0df96af326f90fa9Alexis Tsogias (\x -> case x of
0a03acf9fa28e6ff00f4d7c9c6acbae64cf09c56Ewaryst Schulz (n,_) -> selectANode n dgState
a604cbad8e2202147b5c6bb9f2e06ae61162d654Felix Gabriel Mance nwist = emptyIntIState (i_libEnv dgState) (i_ln dgState)
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder -- ADD TO HISTORY
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder return $ add2hist [IStateChange $ Just dgState] $ state {
7834a982096d93301a4626f444dd9ea5f9fe17eaChristian Maeder -- add the prove state to the status containing
1f9274bb2aa44ea236327814dce99946be52e348Felix Gabriel Mance -- all information selected in the input
1f9274bb2aa44ea236327814dce99946be52e348Felix Gabriel Mance intState = (intState state) {
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maeder i_state = Just nwist {
8fd6a3f938496a502bc62f1923ff7c15f59acf91Christian Maeder elements = elems,
4b4a0b61b72cf8478a5d4d5002bca9f699401363Christian Maeder cComorphism = getIdComorphism elems