Cross Reference: /hets/Static/CheckGlobalContext.hs
CheckGlobalContext.hs revision 12368e292c1abf7eaf975f20ee30ef7820ac5dd5
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder{- |
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederModule : $Header$
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederDescription : checking consistency of indices
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederCopyright : (c) Jianchun Wang, C. Maeder, Uni Bremen 2002-2007
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederMaintainer : Christian.Maeder@dfki.de
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederStability : provisional
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederPortability : non-portable(Logic)
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maedercompare indices from development graphs to the corresponding maps of
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederthe global context
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder-}
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maedermodule Static.CheckGlobalContext where
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport Static.DevGraph
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport Static.GTheory
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport Logic.Grothendieck
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport Logic.Comorphism
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport Common.Lib.State
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederdata Statistics = Statistics
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder { zeroSign, wrongSign, rightSign :: SigId
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder , zeroMor, wrongMor, rightMor :: MorId
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder , zeroTh, wrongTh, rightTh :: ThId }
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder deriving Show
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederinitStat :: Statistics
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederinitStat = Statistics
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder { zeroSign = startSigId
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder , wrongSign = startSigId
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder , rightSign = startSigId
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder , zeroMor = startMorId
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder , wrongMor = startMorId
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder , rightMor = startMorId
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder , zeroTh = startThId
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder , wrongTh = startThId
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder , rightTh = startThId }
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederincrZeroSign :: Statistics -> Statistics
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederincrZeroSign s = s { zeroSign = succ $ zeroSign s }
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederincrWrongSign :: Statistics -> Statistics
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederincrWrongSign s = s { wrongSign = succ $ wrongSign s }
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederincrRightSign ::Statistics -> Statistics
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederincrRightSign s = s { rightSign = succ $ rightSign s }
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederincrZeroG_theory :: Statistics -> Statistics
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederincrZeroG_theory s = s { zeroTh = succ $ zeroTh s }
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederincrWrongG_theory :: Statistics -> Statistics
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederincrWrongG_theory s = s { wrongTh = succ $ wrongTh s }
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederincrRightG_theory :: Statistics -> Statistics
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederincrRightG_theory s = s { rightTh = succ $ rightTh s }
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederincrZeroGMorphism :: Statistics -> Statistics
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederincrZeroGMorphism s = s { zeroMor = succ $ zeroMor s }
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederincrWrongGMorphism :: Statistics -> Statistics
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederincrWrongGMorphism s = s { wrongMor = succ $ wrongMor s }
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederincrRightGMorphism :: Statistics -> Statistics
286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederincrRightGMorphism s = s { rightMor = succ $ rightMor s }
286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder
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 -> if signOf g /= signErg then modify incrWrongSign
else modify incrRightSign
if ti == startThId then modify incrZeroG_theory
else case lookupThMapDG ti dgraph of
Nothing -> error "checkG_theory: Theory"
Just thErg -> if g /= thErg then modify incrWrongG_theory
else modify 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 -> if G_sign (sourceLogic cid) sign si /= signErg
then modify incrWrongSign
else modify incrRightSign
if mi == startMorId then modify incrZeroGMorphism
else case lookupMorMapDG mi dgraph of
Nothing -> error "checkGMorphism: Morphism"
Just morErg -> if g /= gEmbed morErg then modify incrWrongGMorphism
else modify 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
]