content: {-# LANGUAGE CPP, RankNTypes #-}
  {- |
  Module      :./CMDL/InfoCommands.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.InfoCommands contains all commands
  that provides information about the state
  of the development graph and selected
  theories
  -}
  
  module CMDL.InfoCommands
         ( cNodes
         , cShowDgGoals
         , cShowNodeProvenGoals
         , cShowNodeUnprovenGoals
         , cRedoHistory
         , cCurrentComorphism
         , cShowTaxonomy
         , cShowTheory
         , cShowTheoryGoals
         , cUndoHistory
         , cEdges
         , cShowNodeAxioms
         , cInfo
         , cComorphismsTo
         , cInfoCurrent
         , cShowConcept
         , cNodeNumber
         , cHelp
         ) where
  
  
  #ifdef UNI_PACKAGE
  import GUI.Taxonomy
  #endif
  
  import CMDL.DataTypesUtils
  import CMDL.DataTypes
  import CMDL.Shell (nodeNames)
  import CMDL.Utils
  
  import Static.GTheory
  import Static.DevGraph
  import Static.PrintDevGraph (showLEdge)
  
  import Common.AS_Annotation (SenAttr (isAxiom))
  import Common.DocUtils (showDoc)
  import Common.Taxonomy (TaxoGraphKind (..))
  import Common.Utils (trim)
  import qualified Common.OrderedMap as OMap
  import Common.GraphAlgo (yen)
  
  import Proofs.AbstractState (isSubElemG, pathToComorphism)
  
  import Data.Graph.Inductive.Graph (LNode, LEdge, Node)
  import Data.List
  
  import Logic.Prover (SenStatus)
  import Logic.Comorphism (AnyComorphism)
  import Logic.Grothendieck (logicGraph2Graph)
  
  import Comorphisms.LogicGraph (logicGraph)
  
  import Interfaces.Command (cmdNameStr, describeCmd, showCmd)
  import Interfaces.DataTypes
  import Interfaces.Utils
  
  -- show list of all goals(i.e. prints their name)
  cShowDgGoals :: CmdlState -> IO CmdlState
  cShowDgGoals state
   = case i_state $ intState state of
      -- nothing to print
      Nothing -> return state
      Just dgState -> let
           -- list of all nodes
           ls = getAllNodes dgState
           -- compute list of node goals
           nodeGoals = nodeNames $ filter (hasOpenGoals . snd) ls
           -- list of all goal edge names
           edgeGoals = map fst $ filter (edgeContainsGoals . snd)
             $ createEdgeNames ls $ getAllEdges dgState
       -- print sorted version of the list
        in return $ genMessage [] (unlines $ sort (nodeGoals ++ edgeGoals)) state
  
  
  {- local function that computes the theory of a node but it
     keeps only the goal theory -}
  getGoalThS :: CmdlUseTranslation -> Int -> CmdlState -> [String]
  getGoalThS useTrans x state
   = case getTh useTrans x state of
      Nothing -> []
      Just th ->
        let nwth = case th of
                    G_theory x1 syn x2 x3 thSens x4 ->
                      G_theory x1 syn x2 x3
                         (OMap.filter (\ s -> not (isAxiom s) &&
                                            not (isProvenSenStatus s))
                         thSens) x4
        in [showDoc nwth "\n"]
  
  {- local function that computes the theory of a node
     that takes into consideration translated theories in
     the selection too and returns the theory as a string -}
  getThS :: CmdlUseTranslation -> Int -> CmdlState -> [String]
  getThS useTrans x state =
    case getTh useTrans x state of
      Nothing -> ["Could not find a theory"]
      Just th -> [showDoc th "\n"]
  
  getInfoFromNodes :: String -> ([Node] -> [String]) -> CmdlState -> IO CmdlState
  getInfoFromNodes input f state =
    case i_state $ intState state of
      Nothing -> return state
      Just dgState -> let (errors, nodes) = getInputNodes input dgState
                       in return (if null nodes
                                    then genMsgAndCode errors 1 state
                                    else genMessage errors
                                           (intercalate "\n" $ f nodes) state)
  
  cShowFromNode :: (forall a . SenStatus a (AnyComorphism, BasicProof) -> Bool)
                                       -- ^ what sentences to show
                 -> String             -- input string containing node-names
                 -> CmdlState          -- the state
                 -> IO CmdlState
  cShowFromNode f input state =
    getInfoFromNodes input (concatMap (\ n ->
                  case getTh Dont_translate n state of
                    Nothing -> []
                    Just th -> case th of
                                   G_theory _ _ _ _ sens _ -> OMap.keys $
                                     OMap.filter f sens)) state
  
  cShowNodeProvenGoals :: String -> CmdlState -> IO CmdlState
  cShowNodeProvenGoals =
    cShowFromNode (\ s -> not (isAxiom s) && isProvenSenStatus s)
  
  cShowNodeUnprovenGoals :: String -> CmdlState -> IO CmdlState
  cShowNodeUnprovenGoals =
    cShowFromNode (\ s -> not (isAxiom s) && not (isProvenSenStatus s))
  
  cShowNodeAxioms :: String -> CmdlState -> IO CmdlState
  cShowNodeAxioms = cShowFromNode isAxiom
  
  -- show theory of input nodes
  cShowTheory :: CmdlUseTranslation -> String -> CmdlState -> IO CmdlState
  cShowTheory useTrans input state =
    getInfoFromNodes input (concatMap (\ n -> getThS useTrans n state)) state
  
  -- show theory of all goals
  cShowTheoryGoals :: String -> CmdlState -> IO CmdlState
  cShowTheoryGoals input st =
    getInfoFromNodes input (concatMap (\ n -> getGoalThS Do_translate n st)) st
  
  showNodeInfo :: LNode DGNodeLab -> String
  showNodeInfo (i, l) =
    (if isDGRef l
       then ("reference " ++)
       else if isInternalNode l then ("internal " ++) else id)
    "node " ++ getDGNodeName l ++ " " ++ show i ++ "\n" ++ showDoc l ""
  
  showEdgeInfo :: LEdge DGLinkLab -> String
  showEdgeInfo e@(_, _, l) = showLEdge e ++ "\n" ++ showDoc l ""
  
  -- show all information of selection
  cInfoCurrent :: CmdlState -> IO CmdlState
  cInfoCurrent state =
    case i_state $ intState state of
      -- nothing selected
      Nothing -> return state
      Just ps -> let (errors, nodes) = getSelectedDGNodes ps
                  in if null nodes
                       then return $ genMsgAndCode errors 1 state
                       else cInfo (unwords $ nodeNames nodes) state
  
  cComorphismsTo :: String -> CmdlState -> IO CmdlState
  cComorphismsTo input state =
    case i_state $ intState state of
      -- nothing selected
      Nothing -> return state
      Just ps -> case getCurrentSublogic ps of
                  Just start -> case parseSublogics input of
                                  Just end ->
                                   let cmors = yen 10 (start, Nothing)
                                            (\ (l, _) -> isSubElemG l end)
                                            (logicGraph2Graph logicGraph)
                                       cmor = map (show . pathToComorphism) cmors
                                   in return $ genMessage ""
                                                (unlines cmor) state
                                  Nothing -> return $ genMsgAndCode
                                              ("Invalid logic " ++ input) 1 state
                  Nothing -> return $ genMsgAndCode
                                       "No node(s) selected!" 1 state
  
  -- show all information of input
  cInfo :: String -> CmdlState -> IO CmdlState
  cInfo input state =
    case i_state $ intState state of
      -- error message
      Nothing -> return $ genMsgAndCode "No library loaded" 1 state
      Just dgS ->
       let (nds, edg, nbEdg, errs) = decomposeIntoGoals input
           tmpErrs = prettyPrintErrList errs
       in case (nds, edg, nbEdg) of
            ([], [], []) -> return $ genMsgAndCode ("Nothing from the input "
                                         ++ "could be processed") 1 state
            (_, _, _) ->
              let lsNodes = getAllNodes dgS
                  lsEdges = getAllEdges dgS
                  (errs'', listEdges) = obtainEdgeList edg nbEdg lsNodes lsEdges
                  (errs', listNodes) = obtainNodeList nds lsNodes
                  strsNode = map showNodeInfo listNodes
                  strsEdge = map showEdgeInfo listEdges
                  tmpErrs' = tmpErrs ++ prettyPrintErrList errs'
                  tmpErrs'' = tmpErrs' ++ prettyPrintErrList errs''
               in return $ genMessage tmpErrs''
                           (intercalate "\n\n" (strsNode ++ strsEdge)) state
  
  taxoShowGeneric :: TaxoGraphKind -> CmdlState -> [LNode DGNodeLab] -> IO ()
  #ifdef UNI_PACKAGE
  taxoShowGeneric kind state ls =
    case ls of
      (nb, nlab) : ll ->
       case i_state $ intState state of
        Nothing -> return ()
        Just _ ->
         case getTh Do_translate nb state of
         -- the theory was computed
          Just th ->
           do
            -- display graph
            displayGraph kind
                      (getDGNodeName nlab) th
            taxoShowGeneric kind state ll
          -- theory couldn't be computed so just go next
          _ -> taxoShowGeneric kind state ll
      _ -> return ()
  #else
  taxoShowGeneric _ _ _ = return ()
  #endif
  
  cShowTaxoGraph :: TaxoGraphKind -> String -> CmdlState -> IO CmdlState
  cShowTaxoGraph kind input state =
    case i_state $ intState state of
      Nothing -> return state
      Just dgState ->
        do
          let (errors, nodes) = getInputDGNodes input dgState
          taxoShowGeneric kind state nodes
          return $ genMessage errors [] state
  
  cShowTaxonomy :: String -> CmdlState -> IO CmdlState
  cShowTaxonomy = cShowTaxoGraph KSubsort
  
  cShowConcept :: String -> CmdlState -> IO CmdlState
  cShowConcept = cShowTaxoGraph KConcept
  
  -- show node number of input
  cNodeNumber :: String -> CmdlState -> IO CmdlState
  cNodeNumber input state =
    case i_state $ intState state of
      Nothing -> return state
      Just dgState ->
        let (errors, nodes) = getInputDGNodes input dgState
            ls = map (\ (i, n) -> getDGNodeName n ++ " is node number " ++
                      show i) nodes
         in return $ genMessage errors (intercalate "\n" ls) state
  
  -- print the name of all edges
  cEdges :: CmdlState -> IO CmdlState
  cEdges state
   = case i_state $ intState state of
      Nothing -> return state
      Just dgState ->
       do
        -- list of all nodes
        let lsNodes = getAllNodes dgState
            -- compute all edges names
            lsEdg = getAllEdges dgState
            lsEdges = map fst $ createEdgeNames lsNodes lsEdg
        -- print edge list in a sorted fashion
        return $ genMessage [] (intercalate "\n" $ sort lsEdges) state
  
  cUndoHistory :: CmdlState -> IO CmdlState
  cUndoHistory = return . cHistory True
  
  cRedoHistory :: CmdlState -> IO CmdlState
  cRedoHistory = return . cHistory False
  
  cCurrentComorphism :: CmdlState -> IO CmdlState
  cCurrentComorphism st =
   case i_state $ intState st of
    Nothing -> return $ genMessage "" "No comorphism!" st
    Just ist -> case cComorphism ist of
                 Just cmor -> return $ genMessage "" (show cmor) st
                 Nothing -> return $ genMessage "" "No comorphism!" st
  
  cHistory :: Bool -> CmdlState -> CmdlState
  cHistory isUndo state = genMessage []
    (unlines $ ((if isUndo then "Un" else "Re") ++ "do history :")
      : map (showCmd . command)
        ((if isUndo then undoList else redoList) $ i_hist $ intState state)
    ) state
  
  -- print the name of all nodes
  cNodes :: CmdlState -> IO CmdlState
  cNodes state
   = case i_state $ intState state of
      -- no library loaded, so nothing to print
      Nothing -> return state
      Just dgState ->
       do
       -- compute the list of node names
       let ls = nodeNames $ getAllNodes dgState
       -- print a sorted version of it
       return $ genMessage [] (intercalate "\n" $ sort ls) state
  
  cHelp :: [CmdlCmdDescription] -> CmdlState -> IO CmdlState
  cHelp allcmds state = do
    putStrLn $ formatLine ("Command", "Parameter", "Description")
    putStrLn $ replicate maxLineWidth '-'
    mapM_ (\ cm -> do
                     let cmd = cmdDescription cm
                         name = cmdNameStr cmd
                         req = formatRequirement $ cmdReq cm
                         descL = formatDesc $ describeCmd cmd
                         desc = head descL ++
                                concatMap (('\n' : replicate descStart ' ') ++)
                                (tail descL)
                     putStrLn $ formatLine (name, req, desc)) allcmds
    return state
    where
      maxLineWidth = 80
      maxNameLen = maximum $ map (length . cmdNameStr . cmdDescription) allcmds
      maxParamLen = maximum $ map (length . formatRequirement . cmdReq ) allcmds
      descStart = maxNameLen + 1 + maxParamLen + 1
      descWidth = maxLineWidth - descStart
      formatDesc :: String -> [String]
      formatDesc = reverse . filter (not . null) . map trim .
                   foldl (\ l w -> if length (head l) + length w > descWidth
                                     then (w ++ " ") : l
                                     else (head l ++ w ++ " ") : tail l)
                         [""] . words
      formatLine :: (String, String, String) -> String
      formatLine (c1, c2, c3) =
        c1 ++ replicate (maxNameLen - length c1 + 1) ' ' ++
        c2 ++ replicate (maxParamLen - length c2 + 1) ' ' ++ c3
  