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
{- |
Module      :  $Header$
Description :  checking consistency of indices
Copyright   :  (c) Jianchun Wang, C. Maeder, Uni Bremen 2002-2007
License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.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 -> 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
    ]