(CMDL_PrompterState(fileLoaded), CMDL_State(prompter, intState))
(getAllNodes, add2hist, genErrorMsg, genMessage, getIdComorphism)
(decomposeIntoGoals, obtainEdgeList, obtainNodeList, prettyPrintErrList)
-- | Wraps Result structure around the result of a dg all style command
wrapResultDgAll :: (LIB_NAME->LibEnv -> LibEnv) ->
LIB_NAME -> LibEnv -> Result LibEnv
wrapResultDgAll fn lib_name lib_env
= let res = fn lib_name lib_env
-- | Wraps Result structure around the result of a dg style command
wrapResultDg :: (LIB_NAME->[LEdge DGLinkLab] -> LibEnv -> LibEnv) ->
LIB_NAME->[LEdge DGLinkLab] -> LibEnv -> Result LibEnv
wrapResultDg fn lib_name ls lib_env
= let res = fn lib_name ls lib_env
-- | General function for implementing dg all style commands
commandDgAll :: ( LIB_NAME->LibEnv->Result LibEnv) -> CMDL_State
= case i_state $ intState state of
-- just an error message and leave
-- the internal state intact so that
-- the interface can recover
return $ genErrorMsg "No library loaded" state
case fn (i_ln ist) (i_libEnv ist) of
Result _ (Just nwLibEnv) ->
-- Name of function is not known here, so an empty text is
-- added as name, in a later stage (
Shell.hs) the name will
return $ add2hist [IStateChange $ Just ist] $ state {
intState = (intState state) {
i_state=Just$ emptyIntIState nwLibEnv $ i_ln ist}
Result diag Nothing -> return $ genErrorMsg
(concatMap diagString diag) state
-- | Generic function for a dg command, all other dg
-- commands are derived from this command by simply
-- specifing the function
commandDg :: (LIB_NAME -> [LEdge DGLinkLab]->LibEnv->
Result LibEnv) -> String -> CMDL_State
= case i_state $ intState state of
Nothing -> -- leave the internal state intact so
-- that the interface can recover
return $ genErrorMsg "No library loaded" state
let (_,edg,nbEdg,errs) = decomposeIntoGoals input
tmpErrs = prettyPrintErrList errs
([],[]) -> -- leave the internal state intact so
-- that the interface can recover
return $ genErrorMsg (tmpErrs++"No edges in input string\n")
let lsNodes = getAllNodes ist
lsEdges = getAllEdges ist
-- compute the list of edges from the input
(errs',listEdges) = obtainEdgeList edg nbEdg lsNodes
tmpErrs' = tmpErrs ++ prettyPrintErrList errs'
[] -> return $ genErrorMsg (tmpErrs' ++ "No edge in input string\n")
case fn (i_ln ist) listEdges (i_libEnv ist) of
Result _ (Just nwLibEnv) ->
return $ add2hist [IStateChange $ Just ist]
intState = (intState state){
i_state=Just$ emptyIntIState nwLibEnv $ i_ln ist}
Result diag Nothing -> return $ genErrorMsg
(concatMap diagString diag) state
-- | The function 'cUse' implements the Use commands,
i.e.-- given a path it tries to load the library at that path
cUse::String ->CMDL_State -> IO CMDL_State
-- options should be passed through from the top-level
opts <- getArgs >>= hetcatsOpts
tmp <- case i_state $ intState state of
Nothing -> anaLib opts file
anaLibExt opts file $ i_libEnv dgState
Nothing -> -- leave internal state intact so that
-- the interface can recover
return$ genErrorMsg ("Unable to load library "++input) state
i_hist = IntHistory { undoList = [],
i_state = Just $ emptyIntIState nwLibEnv nwLn,
prompter = (prompter state) {
-- The only command that requires a list of nodes instead
cDgThmHideShift :: String -> CMDL_State -> IO CMDL_State
cDgThmHideShift input state
= case i_state $ intState state of
Nothing -> -- leave internal state intact so
-- that the interface can recover
return $ genErrorMsg "No library loaded" state
let (nds,_,_,errs) = decomposeIntoGoals input
tmpErrs = prettyPrintErrList errs
[] -> -- leave internal state intact so
-- that the interface can recover
return $ genErrorMsg (tmpErrs++"No nodes in input string\n")
let lsNodes = getAllNodes dgState
(errs',listNodes) = obtainNodeList nds lsNodes
tmpErrs' = tmpErrs ++ prettyPrintErrList errs'
[] -> return $ genErrorMsg (tmpErrs'++"No nodes in input string\n")
Result diag nwLibEnv = theoremHideShiftFromList (i_ln dgState)
listNodes (i_libEnv dgState)
-- diag not used, how should it?
Nothing -> return $ genErrorMsg (concatMap diagString diag)
return $ add2hist [IStateChange $ Just dgState] $
i_state =Just $ emptyIntIState newEnv $ i_ln dgState
selectANode :: Int -> IntIState
-- computes the theory of a given node
-- (
i.e. solves DGRef cases and so on,
-- see CASL Reference Manual, p.294, Def 4.9)
gth = computeTheory (i_libEnv dgState) (i_ln dgState)
nodeName t = case lookup t $ getAllNodes dgState of
Nothing -> "Unknown node"
Just ll -> getDGNodeName ll
case knownProversWithKind ProveCMDLautomatic of
-- if compute theory was successful give the
-- result as one element list, otherwise an
Result _ (Just th@(G_theory lid _ _ _ _)) ->
-- le not used and should be
(shows (getLIB_ID $ i_ln dgState) "_" ++ nodeName x)
(shrinkKnownProvers sl kpMap)
(getProvers ProveCMDLautomatic sl $
filter hasModelExpansion $
findComorphismPaths logicGraph $
-- all goals and axioms are selected initialy in the proof status
return (initNodeInfo tmp x)
-- | function swithces interface in proving mode and also
-- selects a list of nodes to be used inside this mode
cDgSelect :: String -> CMDL_State -> IO CMDL_State
=case i_state $ intState state of
Nothing -> -- leave internal state intact so
-- that the interface can recover
return $ genErrorMsg "No library loaded" state
let (nds,_,_,errs) = decomposeIntoGoals input
tmpErrs = prettyPrintErrList errs
[] -> return $ genErrorMsg (tmpErrs++"No nodes in input string\n") state
case knownProversWithKind ProveCMDLautomatic of
return $ genErrorMsg (tmpErrs++"No prover found\n") state
let lsNodes = getAllNodes dgState
(errs',listNodes) = obtainNodeList nds lsNodes
tmpErrs' = tmpErrs ++ prettyPrintErrList errs'
[] -> return $ genErrorMsg(tmpErrs'++"No nodes in input string\n")
-- elems is the list of all results (
i.e. -- concat of all one element lists)
(n,_) -> selectANode n dgState
nwist = emptyIntIState (i_libEnv dgState) (i_ln dgState)
return $ add2hist [IStateChange $ Just dgState] $
-- add the prove state to the status
-- containing all information selected
intState = (intState state) {
cComorphism = getIdComorphism elems
-- | Function switches the interface in proving mode by
cDgSelectAll :: CMDL_State -> IO CMDL_State
=case i_state $ intState state of
Nothing -> return $ genErrorMsg "No library loaded" state
case knownProversWithKind ProveCMDLautomatic of
Result _ Nothing -> return $ genErrorMsg "No prover found" state
let lsNodes = getAllNodes dgState
-- elems is the list of all results (
i.e. concat
-- of all one element lists)
(n,_) -> selectANode n dgState
nwist = emptyIntIState (i_libEnv dgState) (i_ln dgState)
return $ add2hist [IStateChange $ Just dgState] $ state {
-- add the prove state to the status containing
-- all information selected in the input
intState = (intState state) {
cComorphism = getIdComorphism elems