DataTypesUtils.hs revision 038fc609b1d0dfe9698c4cab26fc7db2225820ef
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyModule :$Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerDescription : utilitary functions used throughout the CMDL interface
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyCopyright : uni-bremen and DFKI
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : r.pascanu@jacobs-university.de
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyStability : provisional
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyPortability : portable
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyPGIP.Utils contains different basic functions that are
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillyused throughout the CMDL interface and could not be found in
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder ( getAllNodes
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder , obtainGoalNodeList
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder , getAllGoalNodes
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder , getAllEdges
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder , getAllGoalEdges
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , initCMDLProofAbstractState
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder , baseChannels
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder , genErrorMsg
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly , addToHistory
f21c7417bdd1c0282025cba0f5cb0ff5bc5c98eeLiam O'Reilly-- | Returns the list of all nodes, if it is not up to date
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly-- the function recomputes the list
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian MaedergetAllNodes :: CMDL_DevGraphState -> [LNode DGNodeLab]
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian MaedergetAllNodes state
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder = labNodesDG $ lookupDGraph (ln state)
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly (libEnv state)
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly-- | Given a list of node names and the list of all nodes
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- the function returns all the nodes that have their name
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- in the name list but are also goals
9e5f4073e948104307d43c3962d624b8416f191fLiam O'ReillyobtainGoalNodeList :: CMDL_State -> [String] -> [LNode DGNodeLab]
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -> ([String],[LNode DGNodeLab])
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederobtainGoalNodeList state input ls
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder = let (l1,l2) = obtainNodeList input ls
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder l2' = filter (\(nb,nd) ->
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder let nwth = getTh Dont_translate nb state
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder in case nwth of
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Nothing -> False
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Just th -> nodeContainsGoals (nb,nd) th) l2
ebd23ec61635b0bebf7969d14f65b9d1e39f2b26Liam O'ReillyaddToHistory :: CMDL_UndoRedoElem -> CMDL_State -> CMDL_State
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian MaederaddToHistory elm state =
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder case proveState state of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Nothing -> state
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly let oH = history state
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder oH' = tail $ undoInstances oH
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder hist = head $ undoInstances oH
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder uhist = fst hist
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder rhist = snd hist
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder history = oH {
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder undoInstances = (elm:uhist,rhist):oH',
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly redoInstances = []
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder-- | Returns the list of all nodes that are goals,
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder-- taking care of the up to date status
fa373bc327620e08861294716b4454be8d25669fChristian MaedergetAllGoalNodes :: CMDL_State -> CMDL_DevGraphState -> [LNode DGNodeLab]
fa373bc327620e08861294716b4454be8d25669fChristian MaedergetAllGoalNodes st state
fa373bc327620e08861294716b4454be8d25669fChristian Maeder = filter (\(nb,nd) ->
fa373bc327620e08861294716b4454be8d25669fChristian Maeder let nwth = getTh Dont_translate nb st
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder in case nwth of
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Nothing -> False
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder Just th -> nodeContainsGoals (nb,nd) th) $
e8d99f05c231b379be702a1aa8c7dd0b3c666928Liam O'Reilly getAllNodes state
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder-- | Returns the list of all edges, if it is not up to date
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder-- the funcrion recomputes the list
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillygetAllEdges :: CMDL_DevGraphState -> [LEdge DGLinkLab]
e8d99f05c231b379be702a1aa8c7dd0b3c666928Liam O'ReillygetAllEdges state
e7cd36335f0f7be9ed5005e71d94c2856b588d62Christian Maeder = labEdgesDG $ lookupDGraph (ln state)
e7cd36335f0f7be9ed5005e71d94c2856b588d62Christian Maeder (libEnv state)
e7cd36335f0f7be9ed5005e71d94c2856b588d62Christian Maeder-- | Returns the list of all goal edges taking care of the
e8d99f05c231b379be702a1aa8c7dd0b3c666928Liam O'Reilly-- up to date status
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedergetAllGoalEdges :: CMDL_DevGraphState -> [LEdge DGLinkLab]
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedergetAllGoalEdges state
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder = filter edgeContainsGoals $ getAllEdges state
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Constructor for CMDLProofGUIState datatype
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederinitCMDLProofAbstractState:: (Logic lid1 sublogics1
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1) =>
c0833539c8cf577dd3f2497792fbdd818442744cChristian Maeder ProofState lid1 sentence1 -> Int
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder -> CMDL_ProofAbstractState
c0833539c8cf577dd3f2497792fbdd818442744cChristian MaederinitCMDLProofAbstractState ps nb
c0833539c8cf577dd3f2497792fbdd818442744cChristian Maeder = Element ps nb
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder--local function that computes the theory of a node
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly--that takes into consideration translated theories in
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder--the selection too and returns the theory as a string
c0833539c8cf577dd3f2497792fbdd818442744cChristian MaedergetTh :: CMDL_UseTranslation -> Int -> CMDL_State -> Maybe G_theory
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillygetTh useTrans x state
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder -- compute the theory for a given node
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly fn n = case devGraphState state of
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder Nothing -> Nothing
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder Just dgState ->
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder case computeTheory False (libEnv dgState)-- ??
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (ln dgState) n of
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Result _ (Just (_le, th)) -> Just th -- le not used !!!
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder case useTrans of
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder Dont_translate -> fn x
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Do_translate ->
ebd23ec61635b0bebf7969d14f65b9d1e39f2b26Liam O'Reilly case proveState state of
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Nothing -> fn x
ebd23ec61635b0bebf7969d14f65b9d1e39f2b26Liam O'Reilly case find (\y -> case y of
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Element _ z -> z == x) $
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder elements ps of
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder Nothing -> fn x
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder case cComorphism ps of
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Nothing -> fn x
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder Nothing -> Nothing
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder case mapG_theory cm sth of
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Result _ Nothing -> Just sth
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder Result _ (Just sth') -> Just sth'
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder-- | Generates the base channels to be used (stdin and stdout)
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian MaederbaseChannels :: [CMDL_Channel]
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder = let ch_in = CMDL_Channel {
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder chName = "stdin",
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder chType = ChStdin,
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder chHandler = stdin,
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder chSocket = Nothing,
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder chProperties = ChRead
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ch_out = CMDL_Channel {
aa4d26536fffe0153cd81d28925985892ac2f300Christian Maeder chName = "stdout",
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder chType = ChStdout,
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder chHandler = stdout,
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder chSocket = Nothing,
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder chProperties = ChWrite
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder in ch_in : ch_out : []
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillygenErrorMsg :: String -> CMDL_State -> CMDL_State
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'ReillygenErrorMsg msg state
580f1724640a78be687e79d0ec95dd2665e77e91Liam O'Reilly output = CMDL_Output {
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder errorMsg = msg,
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder outputMsg = [],
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder fatalError = True
f21c7417bdd1c0282025cba0f5cb0ff5bc5c98eeLiam O'ReillygenMessage :: String -> String -> CMDL_State -> CMDL_State
f21c7417bdd1c0282025cba0f5cb0ff5bc5c98eeLiam O'ReillygenMessage errMsg msg state
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder output = CMDL_Output {
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder errorMsg = errMsg,
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder outputMsg = msg,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder fatalError = False
d381ab99d6e2e56e09030577d65d9a118f246d35Christian MaedergenError :: CMDL_State -> CMDL_State
d381ab99d6e2e56e09030577d65d9a118f246d35Christian MaedergenError state
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder output = CMDL_Output {
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder errorMsg = [],
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder outputMsg = [],
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder fatalError = True