content: {- |
  Module      :  ./Static/CheckGlobalContext.hs
  Description :  checking consistency of indices
  Copyright   :  (c) Jianchun Wang, C. Maeder, Uni Bremen 2002-2007
  License     :  GPLv2 or higher, see LICENSE.txt
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable(Logic)
  
  compare indices from development graphs to the corresponding maps of
  the global context
  -}
  
  module Static.CheckGlobalContext where
  
  import Static.DevGraph
  import Static.GTheory
  import Logic.Grothendieck
  import Logic.Comorphism
  
  import Common.Lib.State
  
  data Statistics = Statistics
      { zeroSign, wrongSign, rightSign :: SigId
      , zeroMor, wrongMor, rightMor :: MorId
      , zeroTh, wrongTh, rightTh :: ThId }
      deriving Show
  
  initStat :: Statistics
  initStat = Statistics
    { zeroSign = startSigId
    , wrongSign = startSigId
    , rightSign = startSigId
    , zeroMor = startMorId
    , wrongMor = startMorId
    , rightMor = startMorId
    , zeroTh = startThId
    , wrongTh = startThId
    , rightTh = startThId }
  
  incrZeroSign :: Statistics -> Statistics
  incrZeroSign s = s { zeroSign = succ $ zeroSign s }
  
  incrWrongSign :: Statistics -> Statistics
  incrWrongSign s = s { wrongSign = succ $ wrongSign s }
  
  incrRightSign :: Statistics -> Statistics
  incrRightSign s = s { rightSign = succ $ rightSign s }
  
  incrZeroG_theory :: Statistics -> Statistics
  incrZeroG_theory s = s { zeroTh = succ $ zeroTh s }
  
  incrWrongG_theory :: Statistics -> Statistics
  incrWrongG_theory s = s { wrongTh = succ $ wrongTh s }
  
  incrRightG_theory :: Statistics -> Statistics
  incrRightG_theory s = s { rightTh = succ $ rightTh s }
  
  incrZeroGMorphism :: Statistics -> Statistics
  incrZeroGMorphism s = s { zeroMor = succ $ zeroMor s }
  
  incrWrongGMorphism :: Statistics -> Statistics
  incrWrongGMorphism s = s { wrongMor = succ $ wrongMor s }
  
  incrRightGMorphism :: Statistics -> Statistics
  incrRightGMorphism s = s { rightMor = succ $ rightMor s }
  
  checkG_theory :: G_theory -> DGraph -> State Statistics ()
  checkG_theory g@(G_theory _ _ _ si _ ti) dgraph = do
      if si == startSigId then modify incrZeroSign
         else case lookupSigMapDG si dgraph of
            Nothing -> error "checkG_theory: Sign"
            Just signErg -> modify $ if signOf g /= signErg then incrWrongSign
                            else incrRightSign
      if ti == startThId then modify incrZeroG_theory
         else case lookupThMapDG ti dgraph of
            Nothing -> error "checkG_theory: Theory"
            Just thErg -> modify $ if g /= thErg then incrWrongG_theory
                          else incrRightG_theory
  
  checkG_theoryInNode :: DGraph -> DGNodeLab -> State Statistics ()
  checkG_theoryInNode dgraph dg = checkG_theory (dgn_theory dg) dgraph
  
  checkG_theoryInNodes :: DGraph -> State Statistics ()
  checkG_theoryInNodes dgraph =
      mapM_ (checkG_theoryInNode dgraph) $ getDGNodeLab dgraph
  
  checkGMorphism :: GMorphism -> DGraph -> State Statistics ()
  checkGMorphism g@(GMorphism cid sign si _ mi) dgraph = do
      if si == startSigId then modify incrZeroSign
         else case lookupSigMapDG si dgraph of
             Nothing -> error "checkGMorphism: Sign"
             Just signErg -> modify $
                             if G_sign (sourceLogic cid) sign si /= signErg
                             then incrWrongSign else incrRightSign
      if mi == startMorId then modify incrZeroGMorphism
         else case lookupMorMapDG mi dgraph of
             Nothing -> error "checkGMorphism: Morphism"
             Just morErg -> modify $ if g /= gEmbed morErg then incrWrongGMorphism
                            else incrRightGMorphism
  
  getDGLinkLab :: DGraph -> [DGLinkLab]
  getDGLinkLab dgraph = map (\ (_, _, l) -> l) $ labEdgesDG dgraph
  
  getDGNodeLab :: DGraph -> [DGNodeLab]
  getDGNodeLab dgraph = map snd $ labNodesDG dgraph
  
  checkGMorphismInNode :: DGraph -> DGNodeLab -> State Statistics ()
  checkGMorphismInNode dgraph dg = case dgn_sigma dg of
      Nothing -> return ()
      Just gmor -> checkGMorphism gmor dgraph
  
  checkGMorphismInNodes :: DGraph -> State Statistics ()
  checkGMorphismInNodes dgraph =
      mapM_ (checkGMorphismInNode dgraph) $ getDGNodeLab dgraph
  
  checkGMorphismInEdge :: DGraph -> DGLinkLab -> State Statistics ()
  checkGMorphismInEdge dgraph (DGLink {dgl_morphism = dgmor}) =
      checkGMorphism dgmor dgraph
  
  checkGMorphismInEdges :: DGraph -> State Statistics ()
  checkGMorphismInEdges dgraph =
      mapM_ (checkGMorphismInEdge dgraph) $ getDGLinkLab dgraph
  
  checkDGraph :: DGraph -> State Statistics ()
  checkDGraph dgraph = do
      checkGMorphismInNodes dgraph
      checkG_theoryInNodes dgraph
      checkGMorphismInEdges dgraph
  
  printStatistics :: DGraph -> String
  printStatistics dgraph = unlines
      [ "maxSigIndex = " ++ show (snd $ sigMapI dgraph)
      , "maxGMorphismIndex = " ++ show (snd $ morMapI dgraph)
      , "maxG_theoryIndex = " ++ show (snd $ thMapI dgraph)
      , show $ execState (checkDGraph dgraph) initStat
      ]
  