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