CheckGlobalContext.hs revision 12368e292c1abf7eaf975f20ee30ef7820ac5dd5
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederModule : $Header$
81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : checking consistency of indices
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaederCopyright : (c) Jianchun Wang, C. Maeder, Uni Bremen 2002-2007
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederMaintainer : Christian.Maeder@dfki.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederPortability : non-portable(Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maedercompare indices from development graphs to the corresponding maps of
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederthe global context
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederdata Statistics = Statistics
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder { zeroSign, wrongSign, rightSign :: SigId
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder , zeroMor, wrongMor, rightMor :: MorId
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , zeroTh, wrongTh, rightTh :: ThId }
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder deriving Show
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederinitStat :: Statistics
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederinitStat = Statistics
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder { zeroSign = startSigId
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder , wrongSign = startSigId
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder , rightSign = startSigId
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder , zeroMor = startMorId
33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maeder , wrongMor = startMorId
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder , rightMor = startMorId
e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder , zeroTh = startThId
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder , wrongTh = startThId
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder , rightTh = startThId }
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaederincrZeroSign :: Statistics -> Statistics
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederincrZeroSign s = s { zeroSign = succ $ zeroSign s }
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederincrWrongSign :: Statistics -> Statistics
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskiincrWrongSign s = s { wrongSign = succ $ wrongSign s }
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederincrRightSign ::Statistics -> Statistics
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederincrRightSign s = s { rightSign = succ $ rightSign s }
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederincrZeroG_theory :: Statistics -> Statistics
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederincrZeroG_theory s = s { zeroTh = succ $ zeroTh s }
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederincrWrongG_theory :: Statistics -> Statistics
60303deac79adb97a71e55a4d66f95f26688f05aChristian MaederincrWrongG_theory s = s { wrongTh = succ $ wrongTh s }
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederincrRightG_theory :: Statistics -> Statistics
60303deac79adb97a71e55a4d66f95f26688f05aChristian MaederincrRightG_theory s = s { rightTh = succ $ rightTh s }
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederincrZeroGMorphism :: Statistics -> Statistics
4cf9b5b0484a15c0f071ef7898cdcc3a44a15429Christian MaederincrZeroGMorphism s = s { zeroMor = succ $ zeroMor s }
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederincrWrongGMorphism :: Statistics -> Statistics
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederincrWrongGMorphism s = s { wrongMor = succ $ wrongMor s }
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederincrRightGMorphism :: Statistics -> Statistics
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederincrRightGMorphism s = s { rightMor = succ $ rightMor s }
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedercheckG_theory :: G_theory -> DGraph -> State Statistics ()
60303deac79adb97a71e55a4d66f95f26688f05aChristian MaedercheckG_theory g@(G_theory _ _ si _ ti) dgraph = do
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder if si == startSigId then modify incrZeroSign
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder else case lookupSigMapDG si dgraph of
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder Nothing -> error "checkG_theory: Sign"
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder Just signErg -> if signOf g /= signErg then modify incrWrongSign
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder else modify incrRightSign
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder if ti == startThId then modify incrZeroG_theory
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder else case lookupThMapDG ti dgraph of
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder Nothing -> error "checkG_theory: Theory"
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder Just thErg -> if g /= thErg then modify incrWrongG_theory
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder else modify incrRightG_theory
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedercheckG_theoryInNode :: DGraph -> DGNodeLab -> State Statistics ()
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaedercheckG_theoryInNode dgraph dg = checkG_theory (dgn_theory dg) dgraph
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedercheckG_theoryInNodes :: DGraph -> State Statistics ()
961fc5d08256957f68f245f2723085ced14a0a1fChristian MaedercheckG_theoryInNodes dgraph =
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder mapM_ (checkG_theoryInNode dgraph) $ getDGNodeLab dgraph
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaedercheckGMorphism :: GMorphism -> DGraph -> State Statistics ()
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaedercheckGMorphism g@(GMorphism cid sign si _ mi) dgraph = do
961fc5d08256957f68f245f2723085ced14a0a1fChristian Maeder if si == startSigId then modify incrZeroSign
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder else case lookupSigMapDG si dgraph of
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Nothing -> error "checkGMorphism: Sign"
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder Just signErg -> if G_sign (sourceLogic cid) sign si /= signErg
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder then modify incrWrongSign
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder else modify incrRightSign
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder if mi == startMorId then modify incrZeroGMorphism
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder else case lookupMorMapDG mi dgraph of
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder Nothing -> error "checkGMorphism: Morphism"
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder Just morErg -> if g /= gEmbed morErg then modify incrWrongGMorphism
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder else modify incrRightGMorphism
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaedergetDGLinkLab :: DGraph -> [DGLinkLab]
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaedergetDGLinkLab dgraph = map (\ (_, _, l) -> l) $ labEdgesDG dgraph
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaedergetDGNodeLab :: DGraph -> [DGNodeLab]
df2a122c5ecd7d995323c3f0754e1a2a4e3dc0a8Christian MaedergetDGNodeLab dgraph = map snd $ labNodesDG dgraph
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaedercheckGMorphismInNode :: DGraph -> DGNodeLab -> State Statistics ()
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian MaedercheckGMorphismInNode dgraph dg = case dgn_sigma dg of
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder Nothing -> return ()
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder Just gmor -> checkGMorphism gmor dgraph
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian MaedercheckGMorphismInNodes :: DGraph -> State Statistics ()
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaedercheckGMorphismInNodes dgraph =
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder mapM_ (checkGMorphismInNode dgraph) $ getDGNodeLab dgraph
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercheckGMorphismInEdge :: DGraph -> DGLinkLab -> State Statistics ()
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedercheckGMorphismInEdge dgraph (DGLink {dgl_morphism = dgmor}) =
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder checkGMorphism dgmor dgraph
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaedercheckGMorphismInEdges :: DGraph -> State Statistics ()
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedercheckGMorphismInEdges dgraph =
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder mapM_ (checkGMorphismInEdge dgraph) $ getDGLinkLab dgraph
5964438458028e61fdabfa74ca3b4210206cdba6Christian MaedercheckDGraph :: DGraph -> State Statistics ()
5964438458028e61fdabfa74ca3b4210206cdba6Christian MaedercheckDGraph dgraph = do
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder checkGMorphismInNodes dgraph
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder checkG_theoryInNodes dgraph
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder checkGMorphismInEdges dgraph
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederprintStatistics :: DGraph -> String
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederprintStatistics dgraph = unlines
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder [ "maxSigIndex = " ++ show (snd $ sigMapI dgraph)
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian Maeder , "maxGMorphismIndex = " ++ show (snd $ morMapI dgraph)
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder , "maxG_theoryIndex = " ++ show (snd $ thMapI dgraph)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder , show $ execState (checkDGraph dgraph) initStat