{- |

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))

import CMDL.DataTypesUtils

import CMDL.Utils (arrowLink, decomposeIntoGoals, prettyPrintErrList)

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 (groupBy, find, sortBy)

{- 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 $ genErrorMsg "No library loaded" state

Just dgState -> do

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

tmpErrs = prettyPrintErrList errs

case (edg, nbEdg) of

([], []) ->

return $ genErrorMsg ( tmpErrs ++ "No edges in input string\n") state

(_, _) ->

do

let lsNodes = getAllNodes dgState

lsEdges = getAllEdges dgState

(allList, nle) <- conservativityList lsNodes lsEdges

(i_libEnv dgState) (i_ln dgState)

let edgLs = concatMap (\ x -> case find (

\ (s1, _) -> s1 == x) allList of

Nothing -> []

Just (s1, s2) -> [(s1, s2)]) edg

nbEdgLs = concatMap (\ x -> case find (

\ (s1, _) -> s1 == x) allList of

Nothing -> []

Just (s1, s2) -> [(s1, s2)]) nbEdg

nwst = state {

intState = (intState state) {

i_state = Just dgState {

i_libEnv = nle} } }

case edgLs ++ nbEdgLs of

[] -> return $ genErrorMsg (tmpErrs ++ "No edge in input string\n")

nwst

_ -> return $ genMessage tmpErrs

(concatMap (\ (s1, s2) -> s1 ++ " : " ++ s2 ++ "\n")

(edgLs ++ nbEdgLs) ) nwst

-- checks conservativity for every possible node

cConservCheckAll :: CmdlState -> IO CmdlState

cConservCheckAll state = case i_state $ intState state of

Nothing -> return $ genErrorMsg "No library loaded" state

Just dgState -> do

(resTxt, nle) <- conservativityList (getAllNodes dgState)

(getAllEdges dgState)

(i_libEnv dgState)

(i_ln dgState)

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

i_state = Just dgState { i_libEnv = nle } } }

return $ genMessage []

(concatMap (\ (s1, s2) -> s1 ++ " : " ++ s2 ++ "\n") resTxt) nwst

-- applies consistency check to the input

cConsistCheck :: CmdlState -> IO CmdlState

cConsistCheck = cDoLoop True

-- applies consistency check to all possible input

cConsistCheckAll :: CmdlState -> IO CmdlState

cConsistCheckAll state = case i_state $ intState state of

Nothing -> return $ genErrorMsg "Nothing selected" state

Just pS -> case elements pS of

[] -> return $ genErrorMsg "Nothing selected" 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] -> [LEdge DGLinkLab] -> LibEnv

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

conservativityList lsN lsE le libname = do

let

ordFn x y = let (x1, x2, _) = x

(y1, y2, _) = y

in if (x1, x2) > (y1, y2) then GT

else if (x1, x2) < (y1, y2) then LT

else EQ

-- sorted and grouped list of edges

edgs = groupBy ( \ (x1, x2, _) (y1, y2, _) -> (x1, x2) == (y1, y2)) $

sortBy ordFn lsE

edgtm = concatMap (\ l -> case l of

[(x, y, edgLab)] -> [((x, y, edgLab), True)]

_ -> map (\ (x, y, edgLab) -> ((x, y, edgLab),

False)) l)

edgs

(acc, libEnv') <- applyEdgeConservativity le libname edgtm [] lsN

applyNodeConservativity libEnv' libname

[ n | n <- lsN, getNodeConservativity n > None ] 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

((showName $ dgn_name nlab, str) : acc)

applyEdgeConservativity :: LibEnv -> LibName -> [(LEdge DGLinkLab, Bool)]

-> [(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) -> showName $ dgn_name nlab

case ls of

[] -> return (acc, le)

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

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

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

(if vl then "" else showEdgeId (dgl_id edgLab)

++ arrowLink edgLab)

++ nameOf y lsN

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