DgCommands.hs revision ae87f69900b16eef225117da3ca2c268238d690e
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerModule :$Header$
6b26240dca29e026900a83d51c75ca230a072a16Thiemo WiedemeyerDescription : CMDL interface development graph commands
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerCopyright : uni-bremen and DFKI
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerMaintainer : r.pascanu@jacobs-university.de
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederStability : provisional
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerPortability : portable
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerCMDL.DgCommands contains all development graph commands
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerthat can be called from the CMDL interface
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer ( commandDgAll
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , cDgThmHideShift
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , cDgSelectAll
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , wrapResultDg
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer , wrapResultDgAll
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Interfaces.Utils (emptyIntIState, getAllEdges, initNodeInfo)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (CMDL_PrompterState(fileLoaded), CMDL_State(prompter, intState))
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (getAllNodes, add2hist, genErrorMsg, genMessage, getIdComorphism)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (decomposeIntoGoals, obtainEdgeList, obtainNodeList, prettyPrintErrList)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (ProofState(selectedGoals), getProvers, initialState)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Proofs.ComputeTheory (computeTheory)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Proofs.TheoremHideShift (theoremHideShiftFromList)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Static.GTheory (G_theory(G_theory), sublogicOfTh)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Static.DevGraph (LibEnv, DGLinkLab, getDGNodeName)
0193c86704431f83731015a77cb613d67ae4e3c2Thiemo Wiedemeyerimport Driver.AnaLib (anaLib, anaLibExt)
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyerimport Driver.Options (hetcatsOpts)
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyerimport Common.LibName (LIB_NAME(getLIB_ID))
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyerimport Common.Result (Diagnosis(diagString), Result(Result))
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Comorphisms.KnownProvers (knownProversWithKind, shrinkKnownProvers)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Comorphisms.LogicGraph (logicGraph)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Logic.Comorphism (hasModelExpansion)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Logic.Grothendieck (findComorphismPaths)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Logic.Prover (ProverKind(ProveCMDLautomatic))
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Data.List ((++), filter, find, take, concatMap)
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder-- | Wraps Result structure around the result of a dg all style command
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerwrapResultDgAll :: (LIB_NAME->LibEnv -> LibEnv) ->
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer LIB_NAME -> LibEnv -> Result LibEnv
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerwrapResultDgAll fn lib_name lib_env
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer = let res = fn lib_name lib_env
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer in Result [] $ Just res
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer-- | Wraps Result structure around the result of a dg style command
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerwrapResultDg :: (LIB_NAME->[LEdge DGLinkLab] -> LibEnv -> LibEnv) ->
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer LIB_NAME->[LEdge DGLinkLab] -> LibEnv -> Result LibEnv
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerwrapResultDg fn lib_name ls lib_env
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer = let res = fn lib_name ls lib_env
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer in Result [] $ Just res
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer-- | General function for implementing dg all style commands
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo WiedemeyercommandDgAll :: ( LIB_NAME->LibEnv->Result LibEnv) -> CMDL_State
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -> IO CMDL_State
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyercommandDgAll fn state
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer = case i_state $ intState state of
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- just an error message and leave
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- the internal state intact so that
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- the interface can recover
d5f9a0b274192a496eb8d2fb8ce81c33ac2f1717Thiemo Wiedemeyer return $ genErrorMsg "No library loaded" state
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer case fn (i_ln ist) (i_libEnv ist) of
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Result _ (Just nwLibEnv) ->
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- Name of function is not known here, so an empty text is
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- added as name, in a later stage (Shell.hs) the name will
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- be inserted
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer return $ add2hist [IStateChange $ Just ist] $ state {
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder intState = (intState state) {
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer i_state=Just$ emptyIntIState nwLibEnv $ i_ln ist}
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer Result diag Nothing -> return $ genErrorMsg
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer (concatMap diagString diag) state
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer-- | Generic function for a dg command, all other dg
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer-- commands are derived from this command by simply
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer-- specifing the function
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyercommandDg :: (LIB_NAME -> [LEdge DGLinkLab]->LibEnv->
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Result LibEnv) -> String -> CMDL_State
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -> IO CMDL_State
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyercommandDg fn input state
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer = case i_state $ intState state of
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Nothing -> -- leave the internal state intact so
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer -- that the interface can recover
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer return $ genErrorMsg "No library loaded" state
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Just ist -> do
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer let (_,edg,nbEdg,errs) = decomposeIntoGoals input
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer tmpErrs = prettyPrintErrList errs
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer case (edg,nbEdg) of
a96ea65117eaf61ed34248bdf76e4e2144288c9dThiemo Wiedemeyer ([],[]) -> -- leave the internal state intact so
a96ea65117eaf61ed34248bdf76e4e2144288c9dThiemo Wiedemeyer -- that the interface can recover
a96ea65117eaf61ed34248bdf76e4e2144288c9dThiemo Wiedemeyer return $ genErrorMsg (tmpErrs++"No edges in input string\n")
a96ea65117eaf61ed34248bdf76e4e2144288c9dThiemo Wiedemeyer let lsNodes = getAllNodes ist
a96ea65117eaf61ed34248bdf76e4e2144288c9dThiemo Wiedemeyer lsEdges = getAllEdges ist
a96ea65117eaf61ed34248bdf76e4e2144288c9dThiemo Wiedemeyer -- compute the list of edges from the input
a96ea65117eaf61ed34248bdf76e4e2144288c9dThiemo Wiedemeyer (errs',listEdges) = obtainEdgeList edg nbEdg lsNodes
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer tmpErrs' = tmpErrs ++ prettyPrintErrList errs'
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer case listEdges of
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer [] -> return $ genErrorMsg (tmpErrs' ++ "No edge in input string\n")
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer case fn (i_ln ist) listEdges (i_libEnv ist) of
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer Result _ (Just nwLibEnv) ->
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer -- name added later !!
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer return $ add2hist [IStateChange $ Just ist]
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer $ genMessage tmpErrs' []
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer intState = (intState state){
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer i_state=Just$ emptyIntIState nwLibEnv $ i_ln ist}
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer Result diag Nothing -> return $ genErrorMsg
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer (concatMap diagString diag) state
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer-- | The function 'cUse' implements the Use commands, i.e.
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer-- given a path it tries to load the library at that path
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo WiedemeyercUse::String ->CMDL_State -> IO CMDL_State
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo WiedemeyercUse input state
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer -- options should be passed through from the top-level
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer opts <- getArgs >>= hetcatsOpts
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer let file = trim input
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer tmp <- case i_state $ intState state of
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer Nothing -> anaLib opts file
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer Just dgState ->
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer anaLibExt opts file $ i_libEnv dgState
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer Nothing -> -- leave internal state intact so that
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer -- the interface can recover
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer return$ genErrorMsg ("Unable to load library "++input) state
a96ea65117eaf61ed34248bdf76e4e2144288c9dThiemo Wiedemeyer Just (nwLn, nwLibEnv) ->
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer intState = IntState {
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer i_hist = IntHistory { undoList = [],
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer i_state = Just $ emptyIntIState nwLibEnv nwLn,
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer filename = file
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer prompter = (prompter state) {
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer fileLoaded = file }
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer-- The only command that requires a list of nodes instead
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo WiedemeyercDgThmHideShift :: String -> CMDL_State -> IO CMDL_State
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo WiedemeyercDgThmHideShift input state
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer = case i_state $ intState state of
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer Nothing -> -- leave internal state intact so
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer -- that the interface can recover
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer return $ genErrorMsg "No library loaded" state
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer Just dgState -> do
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer let (nds,_,_,errs) = decomposeIntoGoals input
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer tmpErrs = prettyPrintErrList errs
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer [] -> -- leave internal state intact so
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer -- that the interface can recover
c40b7badd217089d8a256dabdf8f7d4e219ca215Thiemo Wiedemeyer return $ genErrorMsg (tmpErrs++"No nodes in input string\n")
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer let lsNodes = getAllNodes dgState
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer (errs',listNodes) = obtainNodeList nds lsNodes
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer tmpErrs' = tmpErrs ++ prettyPrintErrList errs'
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer case listNodes of
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer [] -> return $ genErrorMsg (tmpErrs'++"No nodes in input string\n")
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Result diag nwLibEnv = theoremHideShiftFromList (i_ln dgState)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer listNodes (i_libEnv dgState)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- diag not used, how should it?
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer case nwLibEnv of
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Nothing -> return $ genErrorMsg (concatMap diagString diag)
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer -- ADD TO HISTORY ??
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer Just newEnv ->
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer return $ add2hist [IStateChange $ Just dgState] $
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer genMessage tmpErrs' []
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer (intState state) {
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer i_state =Just $ emptyIntIState newEnv $ i_ln dgState
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer-- selection commands
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerselectANode :: Int -> IntIState
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -> [Int_NodeInfo]
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerselectANode x dgState
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- computes the theory of a given node
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- (i.e. solves DGRef cases and so on,
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- see CASL Reference Manual, p.294, Def 4.9)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer gth = computeTheory (i_libEnv dgState) (i_ln dgState)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer nodeName t=case find(\(n,_)-> n==t) $ getAllNodes dgState of
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Nothing -> "Unknown node"
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Just (_,ll)-> getDGNodeName ll
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer case knownProversWithKind ProveCMDLautomatic of
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Result _ Nothing -> []
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Result _ (Just kpMap) ->
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- if compute theory was successful give the
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- result as one element list, otherwise an
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Result _ (Just th@(G_theory lid _ _ _ _)) ->
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- le not used and should be
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer let sl = sublogicOfTh th
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer tmp<-initialState
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (shows (getLIB_ID $ i_ln dgState) "_" ++ nodeName x)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (shrinkKnownProvers sl kpMap)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (getProvers ProveCMDLautomatic sl $
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer filter hasModelExpansion $
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer findComorphismPaths logicGraph $
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer sublogicOfTh th
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- make so that nothing (no goals, no axioms) are
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- selected initialy in the goal proof status
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer return (initNodeInfo tmp
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer { selectedGoals = take 1 $ selectedGoals tmp } x)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer-- | function swithces interface in proving mode and also
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer-- selects a list of nodes to be used inside this mode
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyercDgSelect :: String -> CMDL_State -> IO CMDL_State
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyercDgSelect input state
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer =case i_state $ intState state of
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Nothing -> -- leave internal state intact so
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- that the interface can recover
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer return $ genErrorMsg "No library loaded" state
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Just dgState -> do
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer let (nds,_,_,errs) = decomposeIntoGoals input
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer tmpErrs = prettyPrintErrList errs
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer [] -> return $ genErrorMsg (tmpErrs++"No nodes in input string\n") state
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer case knownProversWithKind ProveCMDLautomatic of
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Result _ Nothing ->
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer return $ genErrorMsg (tmpErrs++"No prover found\n") state
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Result _ (Just _) ->
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- list of all nodes
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer let lsNodes = getAllNodes dgState
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer -- list of input nodes
6c59ae2c44a1fe22ef1712a57afe129e9dbd3368Thiemo Wiedemeyer (errs',listNodes) = obtainNodeList nds lsNodes
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer tmpErrs' = tmpErrs ++ prettyPrintErrList errs'
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer case listNodes of
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer [] -> return $ genErrorMsg(tmpErrs'++"No nodes in input string\n")
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- elems is the list of all results (i.e.
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer -- concat of all one element lists)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer elems = concatMap
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (\x -> case x of
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer (n,_) -> selectANode n dgState
97b8e548427713e0089a30fcc2df84e0f6aa7ffaCui Jian nwist = emptyIntIState (i_libEnv dgState) (i_ln dgState)
97b8e548427713e0089a30fcc2df84e0f6aa7ffaCui Jian return $ add2hist [IStateChange $ Just dgState] $
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer genMessage tmpErrs' []
97b8e548427713e0089a30fcc2df84e0f6aa7ffaCui Jian -- add the prove state to the status
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer -- containing all information selected
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer -- in the input
152e9fe73d97a51ab34ea7e6e6118521776a0e22Thiemo Wiedemeyer intState = (intState state) {
ddc662fdf0207eae2034d7b68ae5e2225c575207Thiemo Wiedemeyer i_state = Just nwist {
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer elements = elems,
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer cComorphism = getIdComorphism elems
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer-- | Function switches the interface in proving mode by
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer-- selecting all nodes
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo WiedemeyercDgSelectAll :: CMDL_State -> IO CMDL_State
aa07f9c4585a94514dcff2979d853d6e04c12fb9Thiemo WiedemeyercDgSelectAll state
40c18e3f63c23085e5bb36ea35efe141a87df8e4Klaus Luettich =case i_state $ intState state of
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer Nothing -> return $ genErrorMsg "No library loaded" state
aa07f9c4585a94514dcff2979d853d6e04c12fb9Thiemo Wiedemeyer Just dgState ->
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer case knownProversWithKind ProveCMDLautomatic of
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer Result _ Nothing -> return $ genErrorMsg "No prover found" state
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer Result _ (Just _) ->
40c18e3f63c23085e5bb36ea35efe141a87df8e4Klaus Luettich -- list of all nodes
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer let lsNodes = getAllNodes dgState
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer -- elems is the list of all results (i.e. concat
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer -- of all one element lists)
aa07f9c4585a94514dcff2979d853d6e04c12fb9Thiemo Wiedemeyer elems = concatMap
aa07f9c4585a94514dcff2979d853d6e04c12fb9Thiemo Wiedemeyer (\x -> case x of
aa07f9c4585a94514dcff2979d853d6e04c12fb9Thiemo Wiedemeyer (n,_) -> selectANode n dgState
40c18e3f63c23085e5bb36ea35efe141a87df8e4Klaus Luettich nwist = emptyIntIState (i_libEnv dgState) (i_ln dgState)
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer -- ADD TO HISTORY
76ecd8e01387d1edc9197f3464073264fa2c789aThiemo Wiedemeyer return $ add2hist [IStateChange $ Just dgState] $ state {
76ecd8e01387d1edc9197f3464073264fa2c789aThiemo Wiedemeyer -- add the prove state to the status containing
76ecd8e01387d1edc9197f3464073264fa2c789aThiemo Wiedemeyer -- all information selected in the input
40c18e3f63c23085e5bb36ea35efe141a87df8e4Klaus Luettich intState = (intState state) {
76ecd8e01387d1edc9197f3464073264fa2c789aThiemo Wiedemeyer i_state = Just nwist {
76ecd8e01387d1edc9197f3464073264fa2c789aThiemo Wiedemeyer elements = elems,
40c18e3f63c23085e5bb36ea35efe141a87df8e4Klaus Luettich cComorphism = getIdComorphism elems