{- |

Module :$Header$

Description : CMDL interface commands

Copyright : uni-bremen and DFKI

License : GPLv2 or higher, see LICENSE.txt

Maintainer : r.pascanu@jacobs-university.de

Stability : provisional

Portability : portable

CMDL.ConsCommands contains all commands

related to consistency\/conservativity checks

-}

module CMDL.ConsCommands

( cConservCheck

, cConservCheckAll

, cConsistCheck

, cConsistCheckAll

) where

import Interfaces.DataTypes

import Interfaces.Utils

import CMDL.DataTypes (CmdlState (intState), ProveCmdType (..))

import CMDL.DataTypesUtils

import CMDL.Utils

import CMDL.ProveCommands (cDoLoop)

import Proofs.AbstractState (resetSelection)

import Static.DevGraph

import Static.DgUtils

import Common.Consistency

import Common.LibName (LibName)

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

import Data.List

flatConsRes :: [(String, String)] -> String

flatConsRes = intercalate "\n" . map (\ (s1, s2) -> s1 ++ " : " ++ s2)

. reverse

{- Command that processes the input and applies a

conservativity check -}

cConservCheck :: String -> CmdlState -> IO CmdlState

cConservCheck input state =

case i_state $ intState state of

Nothing ->

return $ genMsgAndCode "No library loaded" 1 state

Just dgState -> do

let (nds, edg, nbEdg, errs) = decomposeIntoGoals input

tmpErrs = prettyPrintErrList errs

case (nds, edg, nbEdg) of

([], [], []) ->

return $ genMsgAndCode (tmpErrs ++ "nothing to check\n") 1 state

_ ->

do

let lsNodes = getAllNodes dgState

lsEdges = getAllEdges dgState

(errs', listNodes) = obtainNodeList nds lsNodes

(errs'', listEdges) = obtainEdgeList edg nbEdg lsNodes lsEdges

tmpErrs' = tmpErrs ++ prettyPrintErrList errs'

tmpErrs'' = tmpErrs' ++ prettyPrintErrList errs''

(allList, nle) <- conservativityList lsNodes listNodes listEdges

(i_libEnv dgState) (i_ln dgState)

return $ genMessage tmpErrs'' (flatConsRes allList)

state { intState = (intState state)

{ i_state = Just dgState {i_libEnv = nle} } }

-- checks conservativity for every possible node

cConservCheckAll :: CmdlState -> IO CmdlState

cConservCheckAll state = case i_state $ intState state of

Nothing -> return $ genMsgAndCode "No library loaded" 1 state

Just dgState -> do

let lsNodes = getAllNodes dgState

(resTxt, nle) <- conservativityList lsNodes

(filter ((> None) . getNodeConservativity) lsNodes)

(getAllEdges dgState)

(i_libEnv dgState)

(i_ln dgState)

let nwst = state { intState = (intState state) {

i_state = Just dgState { i_libEnv = nle } } }

return $ genMessage [] (flatConsRes resTxt) nwst

-- applies consistency check to the input

cConsistCheck :: CmdlState -> IO CmdlState

cConsistCheck = cDoLoop ConsCheck

-- applies consistency check to all possible input

cConsistCheckAll :: CmdlState -> IO CmdlState

cConsistCheckAll state = case i_state $ intState state of

Nothing -> return $ genMsgAndCode "Nothing selected" 1 state

Just pS -> case elements pS of

[] -> return $ genMsgAndCode "Nothing selected" 1 state

ls ->

let ls' = map (\ (Element st nb) ->

Element (resetSelection st) nb) ls

nwSt = add2hist [ListChange [NodesChange $ elements pS]] $

state {

intState = (intState state) {

i_state = Just $ pS {

elements = ls' } } }

in cConsistCheck nwSt

-- applies conservativity check to a given list

conservativityList :: [LNode DGNodeLab] -> [LNode DGNodeLab]

-> [LEdge DGLinkLab] -> LibEnv -> LibName -> IO ([(String, String)], LibEnv)

conservativityList allNodes lsN lsE le libname = do

(acc, libEnv') <- applyEdgeConservativity le libname lsE [] allNodes

applyNodeConservativity libEnv' libname lsN acc

applyNodeConservativity :: LibEnv -> LibName -> [LNode DGNodeLab]

-> [(String, String)] -> IO ([(String, String)], LibEnv)

applyNodeConservativity libEnv ln nds acc = case nds of

[] -> return (acc, libEnv)

n@(_, nlab) : ns -> do

(str, nwLe, _) <- checkConservativityNode False n libEnv ln

applyNodeConservativity nwLe ln ns

((getDGNodeName nlab, str) : acc)

applyEdgeConservativity :: LibEnv -> LibName -> [LEdge DGLinkLab]

-> [(String, String)] -> [LNode DGNodeLab] -> IO ([(String, String)], LibEnv)

applyEdgeConservativity le ln ls acc lsN = do

let nameOf x lls = case find (\ (nb, _) -> nb == x) lls of

Nothing -> "Unknown node"

Just (_, nlab) -> getDGNodeName nlab

case ls of

[] -> return (acc, le)

(x, y, edgLab) : l -> do

(str, nwLe, _, _) <- checkConservativityEdge False (x, y, edgLab) le ln

let nm = nameOf x lsN ++ arrowLink edgLab ++

showEdgeId (dgl_id edgLab) ++ arrowLink edgLab

++ nameOf y lsN

applyEdgeConservativity nwLe ln l ((nm, str) : acc) lsN