content: {- |
  Module      :./CMDL/ConsCommands.hs
  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
  