content: {- |
  Module      :  ./GUI/ShowLogicGraph.hs
  Copyright   :  (c) Heng Jiang and Till Mossakowski, Uni Bremen 2002-2006
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable (Logic)
  
  display the logic graph
  -}
  
  module GUI.ShowLogicGraph (showPlainLG, showLG) where
  
  import GUI.UDGUtils as UDG
  import GUI.HTkUtils as HTk
  import qualified GUI.GraphAbstraction as GA
  
  import HTk.Toolkit.DialogWin (useHTk)
  
  import Comorphisms.LogicGraph
  import Comorphisms.LogicList
  import Comorphisms.HetLogicGraph
  import Logic.Grothendieck
  import Logic.Logic
  import Logic.Comorphism
  import Logic.Prover
  
  import qualified Data.Map as Map
  import Data.List
  import qualified Common.Lib.Rel as Rel
  import Common.Consistency
  
  import Data.Typeable
  
  graphParms :: GraphAllConfig graph graphParms node nodeType nodeTypeParms
                                arc arcType arcTypeParms
             => Graph graph graphParms node nodeType nodeTypeParms
                          arc arcType arcTypeParms
             -> String -- ^ title of graph
             -> graphParms
  graphParms _ title =
               GraphTitle title $$
               OptimiseLayout True $$
               AllowClose (return True) $$
               emptyGraphParms
  
  makeNodeMenu :: (GraphAllConfig graph graphParms node
                                      nodeType nodeTypeParms
                                       arc arcType arcTypeParms,
                         Typeable value)
                    => Graph graph graphParms node nodeType nodeTypeParms
                          arc arcType arcTypeParms
                    -> (value -> IO String)
                    -- ^ display the value as a String
                    -> LocalMenu value
                    -> String -- ^ color of node
                    -> nodeTypeParms value
  makeNodeMenu _ showMyValue logicNodeMenu color =
                 logicNodeMenu $$$
                 Ellipse $$$
                 ValueTitle showMyValue $$$
                 Color color $$$
                 emptyNodeTypeParms
  
  stableColor, testingColor, unstableColor, experimentalColor,
     proverColor :: String
  stableColor = "#00FF00"
  testingColor = "#88FF33"
  unstableColor = "#CCFF66"
  experimentalColor = "white"
  proverColor = "lightsteelblue"
  
  normalArcColor :: String
  normalArcColor = "black"
  
  inclusionArcColor :: String
  inclusionArcColor = "blue"
  
  -- | Test whether a comorphism is an ad-hoc inclusion
  isInclComorphism :: AnyComorphism -> Bool
  isInclComorphism (Comorphism cid) =
      Logic (sourceLogic cid) == Logic (targetLogic cid) &&
      isProperSublogic (G_sublogics (sourceLogic cid) (sourceSublogic cid))
                        (G_sublogics (targetLogic cid) (targetSublogic cid))
  
  showLogicGraph :: Bool -> IO GA.OurGraph
  showLogicGraph plain = do
             -- disp s tD = debug (s ++ (show tD))
         logicG <- newGraph daVinciSort
                  $ (if plain then (GlobalMenu (UDG.Menu Nothing [
                  Button "Show detailed logic graph" showHSG ]) $$)
                  else id)
                  $ graphParms daVinciSort $ if plain then "Hets Logic Graph" else
                    "Heterogeneous Sublogic Graph"
         let logicNodeMenu = LocalMenu $ UDG.Menu (Just "Info")
                  $ [Button "Tools" $ \ slg -> let lg = toAnyLogic slg in
                        createTextDisplay
                        ("Parsers, Provers and Cons_Checker of "
                         ++ show lg) (showTools lg) [size (80, 25)]]
                  ++ [Button "Sublogic" $ \ slg -> let lg = toAnyLogic slg in
                         createTextDisplay ("Sublogics of "
                         ++ show lg) (showSublogic lg) [size (80, 25)] | plain]
                  ++ [Button "Sublogic Graph" $ showSubLogicGraph . toAnyLogic,
                  Button "Description" $ \ slg -> let lg = toAnyLogic slg in
                        createTextDisplay
                        ("Description of " ++ show lg) (showDescription lg)
                                        [size (83, 25)]]
             makeLogicNodeMenu = makeNodeMenu daVinciSort
               (return . if plain then show . toAnyLogic else show)
                              logicNodeMenu
         stableNodeType <- newNodeType logicG $ makeLogicNodeMenu stableColor
         testingNodeType <- newNodeType logicG $ makeLogicNodeMenu testingColor
         unstableNodeType <- newNodeType logicG $ makeLogicNodeMenu unstableColor
         experimentalNodeType <- newNodeType logicG $
                                 makeLogicNodeMenu experimentalColor
         proverNodeType <-
             newNodeType logicG $ makeLogicNodeMenu proverColor
         hsGr <- hetSublogicGraph
         let newNode' logic =
               case toAnyLogic logic of
                 Logic lid -> if null $ provers lid then let
                     nodeType = case stability lid of
                       Stable -> stableNodeType
                       Testing -> testingNodeType
                       Unstable -> unstableNodeType
                       Experimental -> experimentalNodeType
                     in newNode logicG nodeType logic
                   else newNode logicG proverNodeType logic
             myMap = if plain then Map.map (\ (Logic l) ->
                                            G_sublogics l $ top_sublogic l)
                       $ Map.fromList $ map addLogicName
                       $ Map.elems $ logics logicGraph
                     else sublogicNodes hsGr
  
         -- production of the nodes (in a list)
         nodeList <- mapM newNode' $ Map.elems myMap
         -- build the map with the node's name and the node.
         let namesAndNodes = Map.fromList (zip (Map.keys myMap)
                                               nodeList)
             lookupLogi gslStr =
                 Map.findWithDefault (error "lookupLogi: Logic not found")
                                     gslStr
                                     namesAndNodes
             {- each edge can also show the informations (the
               description of comorphism and names of
               source/target-Logic as well as the sublogics). -}
             logicArcMenu =
                 LocalMenu $ Button "Info"
                   $ \ c -> createTextDisplay (show c) (showComoDescription c)
                                [size (80, 25)]
             acmName (Comorphism cid) = return $ language_name cid
             normalArcTypeParms = logicArcMenu $$$         -- normal comorphism
                                  Color normalArcColor $$$
                                  ValueTitle acmName $$$
                                  emptyArcTypeParms
             insertArcType tp ((src, trg), acm) =
                    newArc logicG tp acm (lookupLogi src) (lookupLogi trg)
             inclArcTypeParms = logicArcMenu $$$           -- inclusion
                                 Color inclusionArcColor $$$
                                 (if plain then id else (ValueTitle acmName $$$))
                                 emptyArcTypeParms
         normalArcType <- newArcType logicG normalArcTypeParms
         inclArcType <- newArcType logicG inclArcTypeParms
         if plain then do
           let toPair co@(Comorphism c) = ((language_name (sourceLogic c)
                 , language_name (targetLogic c)), co)
               insertComo = insertArcType normalArcType . toPair -- for cormophism
               insertIncl = insertArcType inclArcType . toPair   -- for inclusion
           mapM_ insertIncl inclusionList
           mapM_ insertComo $ filter (`notElem` inclusionList) comorphismList
          else do
           hsg <- hetSublogicGraph
           let (inclCom, notInclCom) =
                 partition ((`elem` inclusionList) . snd) $
                 concatMap (\ (x, ys) -> zip (repeat x) ys) $
                     Map.toList -- [((String,String),[AnyComorphism])]
                            (comorphismEdges hsg)
               (adhocCom, normalCom) =
                 partition (isInclComorphism . snd) notInclCom
               adhocInclArcTypeParms =
                               Color inclusionArcColor $$$ -- ad-hoc inclusion
                               emptyArcTypeParms
           adhocInclArcType <- newArcType logicG adhocInclArcTypeParms
           mapM_ (insertArcType inclArcType) inclCom
           mapM_ (insertArcType adhocInclArcType) adhocCom
           mapM_ (insertArcType normalArcType) normalCom
         redraw logicG
         return logicG
  
  showSubLogicGraph :: AnyLogic -> IO ()
  showSubLogicGraph subl =
            case subl of
              Logic sublid ->
                do subLogicG <- newGraph daVinciSort
                     $ graphParms daVinciSort "SubLogic Graph"
                   let listG_Sublogics = all_sublogics sublid
                       subNodeMenu = LocalMenu (UDG.Menu Nothing [])
                       subNodeTypeParms =
                           subNodeMenu $$$
                           Ellipse $$$
                           ValueTitle (return . sublogicName) $$$
                           Color "yellow" $$$
                           emptyNodeTypeParms
                   subNodeType <- newNodeType subLogicG subNodeTypeParms
                   subNodeList <- mapM (newNode subLogicG subNodeType)
                                  listG_Sublogics
                   let slAndNodes = Map.fromList $
                                    zip listG_Sublogics subNodeList
                       lookupSublogic g_sl =
                           Map.findWithDefault
                                (error "lookupSublogic: node not found")
                                g_sl slAndNodes
                       subArcMenu = LocalMenu (UDG.Menu Nothing [])
                       subArcTypeParms = subArcMenu $$$
                                         Color "green" $$$
                                         emptyArcTypeParms
                   subArcType <- newArcType subLogicG subArcTypeParms
                   let insertSubArc (node1, node2) =
                             newArc subLogicG subArcType ""
                                    (lookupSublogic node1)
                                    (lookupSublogic node2)
                       subl_nodes =
                           Rel.toList $ Rel.intransKernel $ Rel.fromList
                            [ (g1, g2)
                              | g1 <- listG_Sublogics
                              , g2 <- listG_Sublogics
                              , g1 /= g2
                              , isSubElem g1 g2
                            ]
                   mapM_ insertSubArc subl_nodes
                   redraw subLogicG
  
  toAnyLogic :: G_sublogics -> AnyLogic
  toAnyLogic (G_sublogics lid _) = Logic lid
  
  showSublogic :: AnyLogic -> String
  showSublogic (Logic lid) = unlines (map sublogicName (all_sublogics lid))
  
  showSubTitle :: G_sublogics -> String
  showSubTitle (G_sublogics _ lid) = sublogicName lid
  
  showDescription :: AnyLogic -> String
  showDescription (Logic lid) = let s = description lid in
      (if null s then "No description available" else s) ++ "\n\nStability: "
      ++ show (stability lid)
  
  showComoDescription :: AnyComorphism -> String
  showComoDescription (Comorphism cid) =
    let ssid = G_sublogics (sourceLogic cid) (sourceSublogic cid)
        tsid = G_sublogics (targetLogic cid) (targetSublogic cid)
        s = description cid
    in (if null s then "" else s ++ "\n\n")
    ++ "source logic:     " ++ language_name (sourceLogic cid) ++ "\n\n"
    ++ "target logic:     " ++ language_name (targetLogic cid) ++ "\n"
    ++ "source sublogic:  " ++ showSubTitle ssid ++ "\n"
    ++ "target sublogic:  " ++ showSubTitle tsid
  
  showTools :: AnyLogic -> String
  showTools (Logic li) =
      case Map.keys $ parsersAndPrinters li of
        s@(_ : r) -> "Parser for basic specifications.\n"
          ++ if null r then "" else
             unlines . filter (not . null) $ "Additional serializations:"
               : map show s
        [] -> ""
    ++ case parse_symb_items li of
         Just _ -> "Parser for symbol lists.\n"
         Nothing -> ""
    ++ case parse_symb_map_items li of
         Just _ -> "Parser for symbol maps.\n"
         Nothing -> ""
    ++ case basic_analysis li of
         Just _ -> "Analysis of basic specifications.\n"
         Nothing -> ""
    ++ case data_logic li of
         Just _ -> "is a process logic.\n"
         Nothing -> ""
    ++ case provers li of
         [] -> ""
         ls -> unlines $ "\nProvers:" : map proverName ls
    ++ case cons_checkers li of
         [] -> ""
         ls -> unlines $ "\nConsistency checkers:" : map ccName ls
    ++ case conservativityCheck li of
         [] -> ""
         ls -> unlines $ "\nConservatity checkers:" : map checkerId ls
  
  
  showHSG :: IO ()
  showHSG = showLogicGraph False >> return ()
  
  showLG :: IO ()
  showLG = showLogicGraph True >> return ()
  
  showPlainLG :: IO ()
  showPlainLG = do
    wishInst <- HTk.initHTk [HTk.withdrawMainWin]
    useHTk
    lg <- showLogicGraph True
    sync (destroyed lg)
    destroy wishInst
  