hets/Static/CheckGlobalContext.hs

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