{- |

Module :./CMDL/DataTypesUtils.hs

Description : utilitary functions used throughout the CMDL interface

Copyright : uni-bremen and DFKI

License : GPLv2 or higher, see LICENSE.txt

Maintainer : r.pascanu@jacobs-university.de

Stability : provisional

Portability : portable

CMDL.Utils contains different basic functions that are

used throughout the CMDL interface and could not be found in

Prelude

-}

module CMDL.DataTypesUtils

( getSelectedDGNodes

, getCurrentSublogic

, parseSublogics

, getInputDGNodes

, getInputNodes

, getTh

, baseChannels

, genErrorMsg

, genMessage

, genAddMessage

, generatePrompter

, add2hist

, getIdComorphism

, resetErrorCode

, genMsgAndCode

, getExitCode

, getExitCodeInt

) where

import Interfaces.Command (Command (CommentCmd))

import Interfaces.DataTypes

import Interfaces.History (add2history)

import Interfaces.Utils (getAllNodes)

import CMDL.Utils

import CMDL.DataTypes

import Static.GTheory (G_theory, mapG_theory, sublogicOfTh)

import Static.DevGraph (DGNodeLab (..), lookupDGraph, labDG)

import System.IO (stdout, stdin)

import System.Exit

import Proofs.AbstractState (sublogicOfTheory, theoryName)

import Static.ComputeTheory (computeTheory)

import Data.Graph.Inductive.Graph (LNode, Node)

import Data.List (find, break)

import Data.Map (lookup)

import Common.Result (Result (Result))

import Logic.Logic

import Logic.Comorphism (AnyComorphism (..), mkIdComorphism)

import Logic.Grothendieck (G_sublogics (..), joinSublogics, LogicGraph (logics))

import Comorphisms.LogicGraph (logicGraph)

add2hist :: [UndoRedoElem] -> CmdlState -> CmdlState

add2hist descr st

= let intst = add2history (CommentCmd "") (intState st) descr

in st { intState = intst }

{- | Given a list of selected theory generate an Id comorphism to the

first selected theory -}

getIdComorphism :: [Int_NodeInfo] -> Maybe AnyComorphism

getIdComorphism ls = case ls of

[] -> Nothing

Element st _ : _ ->

case sublogicOfTheory st of

G_sublogics lid sub -> Just $ Comorphism (mkIdComorphism lid sub)

-- | Generates the string containing the prompter

generatePrompter :: CmdlState -> String

generatePrompter st = let pst = prompter st in

(case i_state $ intState st of

Nothing -> ""

Just ist ->

let els = case elements ist of

[] -> delExtension (fileLoaded pst)

Element sm _ : r -> theoryName sm ++ if null r then "" else ".."

cm = case elements ist of

[] -> ""

es -> if cComorphism ist /= getIdComorphism es

then "*"

else ""

in els ++ cm) ++ prompterHead pst

-- Returns the selected DGNodes along with a possible error message

getSelectedDGNodes :: IntIState -> (String, [LNode DGNodeLab])

getSelectedDGNodes dgState =

let nds = map (\ (Element _ n) -> n) $ elements dgState

dg = lookupDGraph (i_ln dgState) (i_libEnv dgState)

nds' = zip nds $ map (labDG dg) nds

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

getCurrentSublogic :: IntIState -> Maybe G_sublogics

getCurrentSublogic dgState =

case getSelectedDGNodes dgState of

(_, []) -> Nothing

(_, ns) -> case map (sublogicOfTh . dgn_theory . snd) ns of

[] -> Nothing

sl1 : sl' -> foldl (maybe (const Nothing) joinSublogics)

(Just sl1) sl'

parseSublogics :: String -> Maybe G_sublogics

parseSublogics input =

if elem '.' input then let (l, _ : sl) = Data.List.break (== '.') input

in case Data.Map.lookup l $ logics logicGraph of

Just (Logic lid) ->

case parseSublogic lid sl of

Just subl -> Just $ G_sublogics lid subl

Nothing -> Nothing

Nothing -> Nothing

else case Data.Map.lookup input $ logics logicGraph of

Just (Logic lid) -> Just $ G_sublogics lid (top_sublogic lid)

Nothing -> Nothing

{- Returns the selected DGNodes

or if the selection is empty the DGNodes specified by the input string -}

getInputDGNodes :: String -> IntIState -> (String, [LNode DGNodeLab])

getInputDGNodes input dgState =

if null input

then getSelectedDGNodes dgState

else let

(nds, _, _, errs) = decomposeIntoGoals input

tmpErrs = prettyPrintErrList errs

in case nds of

[] -> (tmpErrs, [])

_ -> let

lsNodes = getAllNodes dgState

(errs', listNodes) = obtainNodeList nds lsNodes

tmpErrs' = tmpErrs ++ prettyPrintErrList errs'

in (tmpErrs', listNodes)

{- Returns the selected Nodes

or if the selection is empty the Nodes specified by the input string -}

getInputNodes :: String -> IntIState -> (String, [Node])

getInputNodes input dgState =

let (errors, nodes) = getInputDGNodes input dgState

in (errors, map fst nodes)

{- local function that computes the theory of a node

that takes into consideration translated theories in

the selection too and returns the theory as a string -}

getTh :: 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]

-- first changes the error code then generates a message

genMsgAndCode :: String -> Int -> CmdlState -> CmdlState

genMsgAndCode msg code st = genErrorMsg msg (st {errorCode = code})

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 = []

}

}

genAddMessage :: String -> String -> CmdlState -> CmdlState

genAddMessage warnings msg st = genMessage warnings

(case outputMsg $ output st of

"" -> msg

msg1 -> msg1 ++ "\n" ++ msg) st

resetErrorCode :: CmdlState -> CmdlState

resetErrorCode st = st {errorCode = 0}

getExitCode :: CmdlState -> ExitCode

getExitCode st = if errorCode st == 0 then ExitSuccess

else ExitFailure $ errorCode st

getExitCodeInt :: CmdlState -> Int

getExitCodeInt = errorCode