DgCommands.hs revision dd5e505efb3641bf74ade0ba3adabf4ceaf94e60
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederModule :$Header$
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettDescription : CMDL interface development graph commands
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederCopyright : uni-bremen and DFKI
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : r.pascanu@jacobs-university.de
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederPortability : portable
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPGIP.DgCommands contains all development graph commands
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachthat can be called from the CMDL interface
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach ( commandDgAll
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , cDgThmHideShift
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , cDgSelectAll
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , selectANode
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , wrapResultDg
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maeder , wrapResultDgAll
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | Wraps Result structure around the result of a dg all style command
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederwrapResultDgAll :: (LIB_NAME->LibEnv -> LibEnv) ->
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett LIB_NAME -> LibEnv -> Result LibEnv
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederwrapResultDgAll fn lib_name lib_env
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder = let res = fn lib_name lib_env
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder in Result [] $ Just res
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder-- | Wraps Result structure around the result of a dg style command
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian MaederwrapResultDg :: (LIB_NAME->[LEdge DGLinkLab] -> LibEnv -> LibEnv) ->
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder LIB_NAME->[LEdge DGLinkLab] -> LibEnv -> Result LibEnv
7e7d791d2f643ffd82843b78e424b6f9f68c24eeChristian MaederwrapResultDg fn lib_name ls lib_env
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder = let res = fn lib_name ls lib_env
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder in Result [] $ Just res
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder-- | General function for implementing dg all style commands
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian MaedercommandDgAll :: ( LIB_NAME->LibEnv->Result LibEnv) -> CMDL_State
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder -> IO CMDL_State
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaedercommandDgAll fn state
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder = case devGraphState state of
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder -- just an error message and leave
8db2221917c1bc569614f3481bcdb3b988facaedChristian Maeder -- the internal state intact so that
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder -- the interface can recover
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder return $ genErrorMsg "No library loaded" state
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett Just dgState ->
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett case fn (ln dgState) (libEnv dgState) of
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Result _ (Just nwLibEnv) ->
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly return state {
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett devGraphState = Just dgState { libEnv = nwLibEnv },
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett -- delete any selection if a dg command is used
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett proveState = Nothing,
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett prompter = (prompter state) { selectedNodes = [],
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett selectedTranslations = [] }
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder Result diag Nothing -> return $ genErrorMsg
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder (concat $ map diagString diag) state
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | Generic function for a dg command, all other dg
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- commands are derived from this command by simply
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- specifing the function
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettcommandDg :: (LIB_NAME -> [LEdge DGLinkLab]->LibEnv->
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder Result LibEnv) -> String -> CMDL_State
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -> IO CMDL_State
842ae753ab848a8508c4832ab64296b929167a97Christian MaedercommandDg fn input state
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder = case devGraphState state of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Nothing -> -- leave the internal state intact so
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -- that the interface can recover
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder return $ genErrorMsg "No library loaded" state
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Just dgState -> do
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let (_,edg,nbEdg,errs) = decomposeIntoGoals input
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder tmpErrs = prettyPrintErrList errs
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett case (edg,nbEdg) of
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ([],[]) -> -- leave the internal state intact so
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach -- that the interface can recover
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett return $genErrorMsg (tmpErrs++"No edges in input string\n")
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maeder let lsNodes = getAllNodes dgState
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maeder lsEdges = getAllEdges dgState
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly -- compute the list of edges from the input
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly (errs',listEdges) = obtainEdgeList edg nbEdg lsNodes
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly tmpErrs' = tmpErrs ++ (prettyPrintErrList errs')
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly case listEdges of
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly [] -> return $genErrorMsg (tmpErrs' ++ "No edge in input string\n")
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett case fn (ln dgState) listEdges (libEnv dgState) of
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Result _ (Just nwLibEnv) ->
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett return $ genMessage tmpErrs' []
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder devGraphState = Just
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett dgState { libEnv = nwLibEnv },
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- delete any selection if a dg command is
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett proveState = Nothing,
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett prompter = (prompter state) { selectedNodes = [],
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly selectedTranslations = [] }
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Result diag Nothing -> return $ genErrorMsg
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (concat $ map diagString diag) state
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | The function 'cUse' implements the Use commands, i.e.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- given a path it tries to load the library at that path
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillycUse::String ->CMDL_State -> IO CMDL_State
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillycUse input state
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let opts = defaultHetcatsOpts
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder file = trim input
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly tmp <- case devGraphState state of
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder Nothing -> anaLib opts file
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder Just dgState ->
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett anaLibExt opts file $ libEnv dgState
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Nothing -> -- leave internal state intact so that
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -- the interface can recover
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder return$ genErrorMsg ("Unable to load library "++input) state
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Just (nwLn, nwLibEnv) ->
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly devGraphState = Just
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly CMDL_DevGraphState {
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly libEnv = nwLibEnv },
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly prompter = (prompter state) {
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly fileLoaded = file,
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly selectedNodes = [],
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly selectedTranslations = [] },
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- delete any selection if a dg command is
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly proveState = Nothing,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly history = CMDL_History {
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly oldEnv = Just nwLibEnv,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly undoList = [],
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly redoList = [],
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly undoInstances = [],
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly redoInstances = []
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- The only command that requires a list of nodes instead
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedercDgThmHideShift :: String -> CMDL_State -> IO CMDL_State
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedercDgThmHideShift input state
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder = case devGraphState state of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Nothing -> -- leave internal state intact so
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- that the interface can recover
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return $ genErrorMsg "No library loaded" state
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Just dgState -> do
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly let (nds,_,_,errs) = decomposeIntoGoals input
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly tmpErrs = prettyPrintErrList errs
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly [] -> -- leave internal state intact so
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly -- that the interface can recover
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return $ genErrorMsg (tmpErrs++"No nodes in input string\n")
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder let lsNodes = getAllNodes dgState
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (errs',listNodes) = obtainNodeList nds lsNodes
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder tmpErrs' = tmpErrs ++ (prettyPrintErrList errs')
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder case listNodes of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder [] -> return $ genErrorMsg (tmpErrs'++"No nodes in input string\n")
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Result diag nwLibEnv = theoremHideShiftFromList (ln dgState)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly listNodes (libEnv dgState)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- diag not used, how should it?
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly case nwLibEnv of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Nothing -> return $ genErrorMsg (concat $ map diagString diag)
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly Just newEnv -> return $ genMessage tmpErrs' []
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly devGraphState = Just
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder dgState { libEnv = newEnv },
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder proveState = Nothing,
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder prompter = (prompter state) {
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder selectedNodes = [],
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder selectedTranslations = [] }
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder-- selection commands
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'ReillyselectANode :: Int -> CMDL_DevGraphState
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -> [CMDL_ProofAbstractState]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederselectANode x dgState
7e7d791d2f643ffd82843b78e424b6f9f68c24eeChristian Maeder -- computes the theory of a given node
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -- (i.e. solves DGRef cases and so on,
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -- see CASL Reference Manual, p.294, Def 4.9)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder gth n = computeTheory False (libEnv dgState)
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder nodeName t=case find(\(n,_)-> n==t) $ getAllNodes dgState of
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly Nothing -> "Unknown node"
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett Just (_,ll)-> getDGNodeName ll
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly case knownProversWithKind ProveCMDLautomatic of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Result _ Nothing -> []
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Result _ (Just kpMap) ->
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -- if compute theory was successful give the
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -- result as one element list, otherwise an
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -- empty list
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder case gth x of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Result _ (Just (_le, th@(G_theory lid _ _ _ _))) ->
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -- le not used and should be
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett let sl = sublogicOfTh th
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly tmp<-initialState
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (getLIB_ID $ ln dgState) "_" ++(nodeName x)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (shrinkKnownProvers sl kpMap)
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett (getProvers ProveCMDLautomatic sl $
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett filter hasModelExpansion $
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett findComorphismPaths logicGraph $
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder sublogicOfTh th
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -- make so that nothing (no goals, no axioms) are
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -- selected initialy in the goal proof status
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder return (initCMDLProofAbstractState tmp{
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder selectedGoals =case selectedGoals tmp of
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | function swithces interface in proving mode and also
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett-- selects a list of nodes to be used inside this mode
842ae753ab848a8508c4832ab64296b929167a97Christian MaedercDgSelect :: String -> CMDL_State -> IO CMDL_State
842ae753ab848a8508c4832ab64296b929167a97Christian MaedercDgSelect input state
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly =case devGraphState state of
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Nothing -> -- leave internal state intact so
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -- that the interface can recover
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder return $ genErrorMsg "No library loaded" state
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Just dgState -> do
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett let (nds,_,_,errs) = decomposeIntoGoals input
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder tmpErrs = prettyPrintErrList errs
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly [] -> return $ genErrorMsg (tmpErrs++"No nodes in input string\n") state
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly case knownProversWithKind ProveCMDLautomatic of
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Result _ Nothing ->
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly return $ genErrorMsg (tmpErrs++"No prover found\n") state
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Result _ (Just _) ->
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly -- list of all nodes
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly let lsNodes = getAllNodes dgState
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly -- list of input nodes
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly (errs',listNodes) = obtainNodeList nds lsNodes
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett tmpErrs' = tmpErrs ++ (prettyPrintErrList errs')
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder case listNodes of
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder [] -> return $ genErrorMsg(tmpErrs'++"No nodes in input string\n")
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly -- elems is the list of all results (i.e.
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly -- concat of all one element lists)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett elems = concatMap
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (\x -> case x of
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (n,_) -> selectANode n dgState
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder oldH = history state
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly nwPrompter = case nds of
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly hd:[] -> (prompter state) {
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett selectedNodes = hd,
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder selectedTranslations = []}
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder hd:_ -> (prompter state) {
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder selectedNodes =hd++"..",
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder selectedTranslations = []}
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly _ -> prompter state
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly return $ genMessage tmpErrs' []
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder -- add the prove state to the status
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder -- containing all information selected
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -- in the input
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder proveState = Just
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly CMDL_ProveState {
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly elements = elems,
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett cComorphism = Nothing,
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder prover = Nothing,
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder consChecker = Nothing,
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder save2file = False,
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder useTheorems = False,
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly loadScript = False
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder history = oldH {
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder undoInstances = ([],[]):(undoInstances oldH),
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder redoInstances = []},
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder prompter = nwPrompter
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder-- | Function switches the interface in proving mode by
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly-- selecting all nodes
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaedercDgSelectAll :: CMDL_State -> IO CMDL_State
842ae753ab848a8508c4832ab64296b929167a97Christian MaedercDgSelectAll state
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder =case devGraphState state of
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Nothing -> return $ genErrorMsg "No library loaded" state
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Just dgState ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly case knownProversWithKind ProveCMDLautomatic of
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Result _ Nothing -> return $ genErrorMsg "No prover found" state
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder Result _ (Just _) ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly -- list of all nodes
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly let lsNodes = getAllNodes dgState
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder -- elems is the list of all results (i.e. concat
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett -- of all one element lists)
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett elems = concatMap
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (\x -> case x of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (n,_) -> selectANode n dgState
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly oldH = history state
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly nwPrompter = case lsNodes of
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder (prompter state) {
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly selectedNodes = (getDGNodeName $ snd hd),
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder selectedTranslations = []}
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (prompter state) {
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly selectedNodes =(getDGNodeName $ snd hd)++"..",
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett selectedTranslations = []}
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder _ -> prompter state
5a859092c242b0e37183a44c3c79479125b2920aChristian Maeder return state {
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -- add the prove state to the status containing
5a859092c242b0e37183a44c3c79479125b2920aChristian Maeder -- all information selected in the input
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder proveState = Just
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly CMDL_ProveState {
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly elements = elems,
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett cComorphism = Nothing,
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder prover = Nothing,
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder consChecker = Nothing,
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly save2file = False,
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder useTheorems = False,
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder loadScript = False
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder history = oldH {
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly undoInstances= ([],[]):(undoInstances oldH),
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly redoInstances= []
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly prompter = nwPrompter