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