{- |

Module : $Header$

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

]