4169N/A{- |

1178N/AModule :$Header$

1178N/ADescription : utilitary functions used throughout the CMDL interface

1178N/ACopyright : uni-bremen and DFKI

1178N/ALicense : GPLv2 or higher, see LICENSE.txt

1178N/AMaintainer : r.pascanu@jacobs-university.de

1178N/AStability : provisional

1178N/APortability : portable

1178N/A

1178N/ACMDL.Utils contains different basic functions that are

1178N/Aused throughout the CMDL interface and could not be found in

1178N/APrelude

1178N/A

1178N/A-}

1178N/A

1178N/Amodule CMDL.DataTypesUtils

1178N/A ( getAllNodes

2362N/A , obtainGoalNodeList

2362N/A , getAllGoalNodes

2362N/A , getAllGoalEdges

1178N/A , getSelectedDGNodes

4169N/A , getInputDGNodes

1178N/A , getInputNodes

1178N/A , getTh

4033N/A , baseChannels

4033N/A , genErrorMsg

1178N/A , genMessage

1178N/A , generatePrompter

1178N/A , add2hist

1178N/A , getIdComorphism

4033N/A ) where

1178N/A

1178N/Aimport Interfaces.Command(Command(CommentCmd))

4033N/Aimport Interfaces.DataTypes

1178N/Aimport Interfaces.History(add2history)

1178N/Aimport Interfaces.Utils(getAllEdges, getAllNodes)

4033N/Aimport CMDL.Utils

1178N/Aimport CMDL.DataTypes

1178N/A

4033N/Aimport Static.GTheory(G_theory, mapG_theory)

1178N/Aimport Static.DevGraph(DGNodeLab, DGLinkLab, lookupDGraph, labDG)

1178N/A

4033N/Aimport System.IO(stdout, stdin)

1178N/A

1178N/Aimport Proofs.AbstractState(ProofState(sublogicOfTheory, theoryName))

1178N/Aimport Static.ComputeTheory(computeTheory)

4033N/A

0N/Aimport Data.Graph.Inductive.Graph(LNode, LEdge, Node)

0N/Aimport Data.List (find)

0N/A

0N/Aimport Common.Result(Result(Result))

0N/A

0N/Aimport Logic.Comorphism(AnyComorphism(..), mkIdComorphism)

0N/Aimport Logic.Grothendieck(G_sublogics(..))

0N/A

0N/Aadd2hist :: [UndoRedoElem] -> CmdlState -> CmdlState

0N/Aadd2hist descr st

0N/A = let intst = add2history (CommentCmd "") (intState st) descr

4033N/A in st { intState = intst }

0N/A

1178N/A-- | Given a list of selected theory generate an Id comorphism to the

0N/A-- first selected theory

1178N/AgetIdComorphism :: [Int_NodeInfo] -> Maybe AnyComorphism

4033N/AgetIdComorphism ls = case ls of

1178N/A [] -> Nothing

0N/A Element st _ : _ ->

1178N/A case sublogicOfTheory st of

4033N/A G_sublogics lid sub -> Just $ Comorphism (mkIdComorphism lid sub)

4033N/A

4033N/A-- | Generates the string containing the prompter

0N/AgeneratePrompter :: CmdlState -> String

4033N/AgeneratePrompter st = (case i_state $ intState st of

1178N/A Nothing -> ""

4033N/A Just ist ->

4033N/A let pst = prompter st

4033N/A els = case elements ist of

4033N/A [] -> delExtension (fileLoaded pst)

1178N/A Element sm _ : r -> theoryName sm ++ if null r then "" else ".."

4033N/A cm = if null (elements ist)

0N/A then ""

4033N/A else if cComorphism ist /= getIdComorphism (elements ist)

4033N/A then "*"

4033N/A else ""

4033N/A in els ++ cm) ++ prompterHead (prompter st)

0N/A

1178N/A-- | Given a list of node names and the list of all nodes

0N/A-- the function returns all the nodes that have their name

4033N/A-- in the name list but are also goals

1178N/AobtainGoalNodeList :: CmdlState -> [String] -> [LNode DGNodeLab]

1178N/A -> ([String],[LNode DGNodeLab])

1178N/AobtainGoalNodeList state input ls

0N/A = let (l1,l2) = obtainNodeList input ls

4033N/A l2' = filter (\(nb,nd) ->

1178N/A let nwth = getTh Dont_translate nb state

1178N/A in case nwth of

4033N/A Nothing -> False

1178N/A Just th -> nodeContainsGoals (nb,nd) th) l2

1178N/A in (l1,l2')

4033N/A

1178N/A

4033N/A-- | Returns the list of all nodes that are goals,

1178N/A-- taking care of the up to date status

1178N/AgetAllGoalNodes :: CmdlState -> [LNode DGNodeLab]

1178N/AgetAllGoalNodes st

1178N/A = case i_state $ intState st of

4033N/A Nothing -> []

1178N/A Just ist ->

4033N/A filter (\(nb,nd) ->

4033N/A let nwth = getTh Dont_translate nb st

0N/A in case nwth of

4033N/A Nothing -> False

4033N/A Just th -> nodeContainsGoals (nb,nd) th) $

0N/A getAllNodes ist

0N/A

0N/A-- | Returns the list of all goal edges taking care of the

0N/A-- up to date status

0N/AgetAllGoalEdges :: CmdlState -> [LEdge DGLinkLab]

0N/AgetAllGoalEdges st

0N/A = case i_state $ intState st of

0N/A Nothing -> []

0N/A Just ist ->

4033N/A filter edgeContainsGoals $ getAllEdges ist

0N/A

1178N/A-- Returns the selected DGNodes along with a possible error message

0N/AgetSelectedDGNodes :: IntIState -> (String, [LNode DGNodeLab])

4033N/AgetSelectedDGNodes dgState =

1178N/A let nds = map (\ (Element _ n) -> n) $ elements dgState

4033N/A dg = lookupDGraph (i_ln dgState) (i_libEnv dgState)

4033N/A nds' = zip nds $ map (labDG dg) nds

1178N/A in (if null nds' then "No node(s) selected!" else "", nds')

4033N/A

4033N/A-- Returns the selected DGNodes

0N/A-- or if the selection is empty the DGNodes specified by the input string

4033N/AgetInputDGNodes :: String -> IntIState -> (String, [LNode DGNodeLab])

4033N/AgetInputDGNodes input dgState =

1178N/A if null input

1178N/A then getSelectedDGNodes dgState

0N/A else let (nds,_,_,errs) = decomposeIntoGoals input

4033N/A tmpErrs = prettyPrintErrList errs

0N/A in case nds of

0N/A [] -> (tmpErrs, [])

0N/A _ -> let lsNodes = getAllNodes dgState

1178N/A (errs',listNodes) = obtainNodeList nds lsNodes

1178N/A tmpErrs' = tmpErrs ++ prettyPrintErrList errs'

4033N/A in (tmpErrs', listNodes)

0N/A

0N/A-- Returns the selected Nodes

1178N/A-- or if the selection is empty the Nodes specified by the input string

1178N/AgetInputNodes :: String -> IntIState -> (String, [Node])

0N/AgetInputNodes input dgState =

4033N/A let (errors, nodes) = getInputDGNodes input dgState

0N/A in (errors, map (\ x -> case x of (n, _) -> n) nodes)

0N/A

0N/A--local function that computes the theory of a node

0N/A--that takes into consideration translated theories in

0N/A--the selection too and returns the theory as a string

0N/AgetTh :: CmdlUseTranslation -> Int -> CmdlState -> Maybe G_theory

getTh useTrans x st

= let

-- compute the theory for a given node

fn n = case i_state $ intState st of

Nothing -> Nothing

Just ist -> computeTheory (i_libEnv ist) (i_ln ist) n

in

case useTrans of

Dont_translate -> fn x

Do_translate ->

case i_state $ intState st of

Nothing -> Nothing

Just ist ->

case elements ist of

[] -> fn x

_ ->

case find (\y -> case y of

Element _ z -> z == x) $

elements ist of

Nothing -> fn x

Just _ ->

case cComorphism ist of

Nothing -> fn x

Just cm ->

case fn x of

Nothing -> Nothing

Just sth->

case mapG_theory cm sth of

Result _ Nothing -> Just sth

Result _ (Just sth') -> Just sth'

-- | Generates the base channels to be used (stdin and stdout)

baseChannels :: [CmdlChannel]

baseChannels

= let ch_in = CmdlChannel {

chName = "stdin",

chType = ChStdin,

chHandler = stdin,

chSocket = Nothing,

chProperties = ChRead

}

ch_out = CmdlChannel {

chName = "stdout",

chType = ChStdout,

chHandler = stdout,

chSocket = Nothing,

chProperties = ChWrite

}

in [ch_in, ch_out]

genErrorMsg :: String -> CmdlState -> CmdlState

genErrorMsg msg st

= st {

output = CmdlMessage {

outputMsg = [],

warningMsg = [],

errorMsg = msg

}

}

genMessage :: String -> String -> CmdlState -> CmdlState

genMessage warnings msg st

= st{

output = CmdlMessage {

outputMsg = msg,

warningMsg = warnings,

errorMsg = []

}

}