{- |
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 :: [(String, String)] -> String
flatConsRes = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" ([String] -> String)
-> ([(String, String)] -> [String]) -> [(String, String)] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, String) -> String) -> [(String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s1 :: String
s1, s2 :: String
s2) -> String
s1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s2)
  ([(String, String)] -> [String])
-> ([(String, String)] -> [(String, String)])
-> [(String, String)]
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(String, String)] -> [(String, String)]
forall a. [a] -> [a]
reverse

{- Command that processes the input and applies a
conservativity check -}
cConservCheck :: String -> CmdlState -> IO CmdlState
cConservCheck :: String -> CmdlState -> IO CmdlState
cConservCheck input :: String
input state :: CmdlState
state =
  case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
   Nothing ->
     CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode "No library loaded" 1 CmdlState
state
   Just dgState :: IntIState
dgState -> do
     let (nds :: [String]
nds, edg :: [String]
edg, nbEdg :: [String]
nbEdg, errs :: [String]
errs) = String -> ([String], [String], [String], [String])
decomposeIntoGoals String
input
         tmpErrs :: String
tmpErrs = [String] -> String
prettyPrintErrList [String]
errs
     case ([String]
nds, [String]
edg, [String]
nbEdg) of
      ([], [], []) ->
        CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode (String
tmpErrs String -> String -> String
forall a. [a] -> [a] -> [a]
++ "nothing to check\n") 1 CmdlState
state
      _ ->
        do
         let lsNodes :: [LNode DGNodeLab]
lsNodes = IntIState -> [LNode DGNodeLab]
getAllNodes IntIState
dgState
             lsEdges :: [LEdge DGLinkLab]
lsEdges = IntIState -> [LEdge DGLinkLab]
getAllEdges IntIState
dgState
             (errs' :: [String]
errs', listNodes :: [LNode DGNodeLab]
listNodes) = [String] -> [LNode DGNodeLab] -> ([String], [LNode DGNodeLab])
obtainNodeList [String]
nds [LNode DGNodeLab]
lsNodes
             (errs'' :: [String]
errs'', listEdges :: [LEdge DGLinkLab]
listEdges) = [String]
-> [String]
-> [LNode DGNodeLab]
-> [LEdge DGLinkLab]
-> ([String], [LEdge DGLinkLab])
obtainEdgeList [String]
edg [String]
nbEdg [LNode DGNodeLab]
lsNodes [LEdge DGLinkLab]
lsEdges
             tmpErrs' :: String
tmpErrs' = String
tmpErrs String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
prettyPrintErrList [String]
errs'
             tmpErrs'' :: String
tmpErrs'' = String
tmpErrs' String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
prettyPrintErrList [String]
errs''
         (allList :: [(String, String)]
allList, nle :: LibEnv
nle) <- [LNode DGNodeLab]
-> [LNode DGNodeLab]
-> [LEdge DGLinkLab]
-> LibEnv
-> LibName
-> IO ([(String, String)], LibEnv)
conservativityList [LNode DGNodeLab]
lsNodes [LNode DGNodeLab]
listNodes [LEdge DGLinkLab]
listEdges
                                  (IntIState -> LibEnv
i_libEnv IntIState
dgState) (IntIState -> LibName
i_ln IntIState
dgState)
         CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> String -> CmdlState -> CmdlState
genMessage String
tmpErrs'' ([(String, String)] -> String
flatConsRes [(String, String)]
allList)
           CmdlState
state { intState :: IntState
intState = (CmdlState -> IntState
intState CmdlState
state)
                   { i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just IntIState
dgState {i_libEnv :: LibEnv
i_libEnv = LibEnv
nle} } }

-- checks conservativity for every possible node
cConservCheckAll :: CmdlState -> IO CmdlState
cConservCheckAll :: CmdlState -> IO CmdlState
cConservCheckAll state :: CmdlState
state = case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
    Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode "No library loaded" 1 CmdlState
state
    Just dgState :: IntIState
dgState -> do
      let lsNodes :: [LNode DGNodeLab]
lsNodes = IntIState -> [LNode DGNodeLab]
getAllNodes IntIState
dgState
      (resTxt :: [(String, String)]
resTxt, nle :: LibEnv
nle) <- [LNode DGNodeLab]
-> [LNode DGNodeLab]
-> [LEdge DGLinkLab]
-> LibEnv
-> LibName
-> IO ([(String, String)], LibEnv)
conservativityList [LNode DGNodeLab]
lsNodes
         ((LNode DGNodeLab -> Bool) -> [LNode DGNodeLab] -> [LNode DGNodeLab]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Conservativity -> Conservativity -> Bool
forall a. Ord a => a -> a -> Bool
> Conservativity
None) (Conservativity -> Bool)
-> (LNode DGNodeLab -> Conservativity) -> LNode DGNodeLab -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LNode DGNodeLab -> Conservativity
getNodeConservativity) [LNode DGNodeLab]
lsNodes)
                                   (IntIState -> [LEdge DGLinkLab]
getAllEdges IntIState
dgState)
                                   (IntIState -> LibEnv
i_libEnv IntIState
dgState)
                                   (IntIState -> LibName
i_ln IntIState
dgState)
      let nwst :: CmdlState
nwst = CmdlState
state { intState :: IntState
intState = (CmdlState -> IntState
intState CmdlState
state) {
                            i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just IntIState
dgState { i_libEnv :: LibEnv
i_libEnv = LibEnv
nle } } }
      CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> String -> CmdlState -> CmdlState
genMessage [] ([(String, String)] -> String
flatConsRes [(String, String)]
resTxt) CmdlState
nwst

-- applies consistency check to the input
cConsistCheck :: CmdlState -> IO CmdlState
cConsistCheck :: CmdlState -> IO CmdlState
cConsistCheck = ProveCmdType -> CmdlState -> IO CmdlState
cDoLoop ProveCmdType
ConsCheck

-- applies consistency check to all possible input
cConsistCheckAll :: CmdlState -> IO CmdlState
cConsistCheckAll :: CmdlState -> IO CmdlState
cConsistCheckAll state :: CmdlState
state = case IntState -> Maybe IntIState
i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ CmdlState -> IntState
intState CmdlState
state of
      Nothing -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode "Nothing selected" 1 CmdlState
state
      Just pS :: IntIState
pS -> case IntIState -> [Int_NodeInfo]
elements IntIState
pS of
          [] -> CmdlState -> IO CmdlState
forall (m :: * -> *) a. Monad m => a -> m a
return (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState
forall a b. (a -> b) -> a -> b
$ String -> Int -> CmdlState -> CmdlState
genMsgAndCode "Nothing selected" 1 CmdlState
state
          ls :: [Int_NodeInfo]
ls ->
             let ls' :: [Int_NodeInfo]
ls' = (Int_NodeInfo -> Int_NodeInfo) -> [Int_NodeInfo] -> [Int_NodeInfo]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Element st :: ProofState
st nb :: Int
nb) ->
                               ProofState -> Int -> Int_NodeInfo
Element (ProofState -> ProofState
resetSelection ProofState
st) Int
nb) [Int_NodeInfo]
ls
                 nwSt :: CmdlState
nwSt = [UndoRedoElem] -> CmdlState -> CmdlState
add2hist [[ListChange] -> UndoRedoElem
ListChange [[Int_NodeInfo] -> ListChange
NodesChange ([Int_NodeInfo] -> ListChange) -> [Int_NodeInfo] -> ListChange
forall a b. (a -> b) -> a -> b
$ IntIState -> [Int_NodeInfo]
elements IntIState
pS]] (CmdlState -> CmdlState) -> CmdlState -> CmdlState
forall a b. (a -> b) -> a -> b
$
                          CmdlState
state {
                           intState :: IntState
intState = (CmdlState -> IntState
intState CmdlState
state) {
                              i_state :: Maybe IntIState
i_state = IntIState -> Maybe IntIState
forall a. a -> Maybe a
Just (IntIState -> Maybe IntIState) -> IntIState -> Maybe IntIState
forall a b. (a -> b) -> a -> b
$ IntIState
pS {
                                                  elements :: [Int_NodeInfo]
elements = [Int_NodeInfo]
ls' } } }
             in CmdlState -> IO CmdlState
cConsistCheck CmdlState
nwSt

-- applies conservativity check to a given list
conservativityList :: [LNode DGNodeLab] -> [LNode DGNodeLab]
   -> [LEdge DGLinkLab] -> LibEnv -> LibName -> IO ([(String, String)], LibEnv)
conservativityList :: [LNode DGNodeLab]
-> [LNode DGNodeLab]
-> [LEdge DGLinkLab]
-> LibEnv
-> LibName
-> IO ([(String, String)], LibEnv)
conservativityList allNodes :: [LNode DGNodeLab]
allNodes lsN :: [LNode DGNodeLab]
lsN lsE :: [LEdge DGLinkLab]
lsE le :: LibEnv
le libname :: LibName
libname = do
   (acc :: [(String, String)]
acc, libEnv' :: LibEnv
libEnv') <- LibEnv
-> LibName
-> [LEdge DGLinkLab]
-> [(String, String)]
-> [LNode DGNodeLab]
-> IO ([(String, String)], LibEnv)
applyEdgeConservativity LibEnv
le LibName
libname [LEdge DGLinkLab]
lsE [] [LNode DGNodeLab]
allNodes
   LibEnv
-> LibName
-> [LNode DGNodeLab]
-> [(String, String)]
-> IO ([(String, String)], LibEnv)
applyNodeConservativity LibEnv
libEnv' LibName
libname [LNode DGNodeLab]
lsN [(String, String)]
acc

applyNodeConservativity :: LibEnv -> LibName -> [LNode DGNodeLab]
  -> [(String, String)] -> IO ([(String, String)], LibEnv)
applyNodeConservativity :: LibEnv
-> LibName
-> [LNode DGNodeLab]
-> [(String, String)]
-> IO ([(String, String)], LibEnv)
applyNodeConservativity libEnv :: LibEnv
libEnv ln :: LibName
ln nds :: [LNode DGNodeLab]
nds acc :: [(String, String)]
acc = case [LNode DGNodeLab]
nds of
    [] -> ([(String, String)], LibEnv) -> IO ([(String, String)], LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(String, String)]
acc, LibEnv
libEnv)
    n :: LNode DGNodeLab
n@(_, nlab :: DGNodeLab
nlab) : ns :: [LNode DGNodeLab]
ns -> do
      (str :: String
str, nwLe :: LibEnv
nwLe, _) <- Bool
-> LNode DGNodeLab
-> LibEnv
-> LibName
-> IO (String, LibEnv, ProofHistory)
checkConservativityNode Bool
False LNode DGNodeLab
n LibEnv
libEnv LibName
ln
      LibEnv
-> LibName
-> [LNode DGNodeLab]
-> [(String, String)]
-> IO ([(String, String)], LibEnv)
applyNodeConservativity LibEnv
nwLe LibName
ln [LNode DGNodeLab]
ns
                         ((DGNodeLab -> String
getDGNodeName DGNodeLab
nlab, String
str) (String, String) -> [(String, String)] -> [(String, String)]
forall a. a -> [a] -> [a]
: [(String, String)]
acc)

applyEdgeConservativity :: LibEnv -> LibName -> [LEdge DGLinkLab]
  -> [(String, String)] -> [LNode DGNodeLab] -> IO ([(String, String)], LibEnv)
applyEdgeConservativity :: LibEnv
-> LibName
-> [LEdge DGLinkLab]
-> [(String, String)]
-> [LNode DGNodeLab]
-> IO ([(String, String)], LibEnv)
applyEdgeConservativity le :: LibEnv
le ln :: LibName
ln ls :: [LEdge DGLinkLab]
ls acc :: [(String, String)]
acc lsN :: [LNode DGNodeLab]
lsN = do
   let nameOf :: a -> t (a, DGNodeLab) -> String
nameOf x :: a
x lls :: t (a, DGNodeLab)
lls = case ((a, DGNodeLab) -> Bool)
-> t (a, DGNodeLab) -> Maybe (a, DGNodeLab)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\ (nb :: a
nb, _) -> a
nb a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x) t (a, DGNodeLab)
lls of
                      Nothing -> "Unknown node"
                      Just (_, nlab :: DGNodeLab
nlab) -> DGNodeLab -> String
getDGNodeName DGNodeLab
nlab
   case [LEdge DGLinkLab]
ls of
    [] -> ([(String, String)], LibEnv) -> IO ([(String, String)], LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(String, String)]
acc, LibEnv
le)
    (x :: Int
x, y :: Int
y, edgLab :: DGLinkLab
edgLab) : l :: [LEdge DGLinkLab]
l -> do
      (str :: String
str, nwLe :: LibEnv
nwLe, _, _) <- Bool
-> LEdge DGLinkLab
-> LibEnv
-> LibName
-> IO (String, LibEnv, LEdge DGLinkLab, ProofHistory)
checkConservativityEdge Bool
False (Int
x, Int
y, DGLinkLab
edgLab) LibEnv
le LibName
ln
      let nm :: String
nm = Int -> [LNode DGNodeLab] -> String
forall (t :: * -> *) a.
(Foldable t, Eq a) =>
a -> t (a, DGNodeLab) -> String
nameOf Int
x [LNode DGNodeLab]
lsN String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGLinkLab -> String
arrowLink DGLinkLab
edgLab String -> String -> String
forall a. [a] -> [a] -> [a]
++
               EdgeId -> String
showEdgeId (DGLinkLab -> EdgeId
dgl_id DGLinkLab
edgLab) String -> String -> String
forall a. [a] -> [a] -> [a]
++ DGLinkLab -> String
arrowLink DGLinkLab
edgLab
               String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> [LNode DGNodeLab] -> String
forall (t :: * -> *) a.
(Foldable t, Eq a) =>
a -> t (a, DGNodeLab) -> String
nameOf Int
y [LNode DGNodeLab]
lsN
      LibEnv
-> LibName
-> [LEdge DGLinkLab]
-> [(String, String)]
-> [LNode DGNodeLab]
-> IO ([(String, String)], LibEnv)
applyEdgeConservativity LibEnv
nwLe LibName
ln [LEdge DGLinkLab]
l ((String
nm, String
str) (String, String) -> [(String, String)] -> [(String, String)]
forall a. a -> [a] -> [a]
: [(String, String)]
acc) [LNode DGNodeLab]
lsN