TriangleCons.hs revision c208973c890b8f993297720fd0247bc7481d4304
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
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederModule : $Header$
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederDescription : apply triangle-cons rule for all edges in development graphs
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederCopyright : (c) Christian Maeder, DFKI GmbH 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksaMaintainer : Christian.Maeder@dfki.de
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederStability : provisional
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederPortability : non-portable(Logic)
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport qualified Data.Map as Map
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport qualified Data.Set as Set
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaedertriangleConsRule :: DGRule
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaedertriangleConsRule = DGRule "TriangleCons"
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaedertriangleCons :: LibName -> LibEnv -> Result LibEnv
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaedertriangleCons ln le = do
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa let dg = lookupDGraph ln le
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder newDg <- foldM triangleConsDG dg $
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder filter (\ (_, _, l) -> let e = getRealDGLinkType l in
7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc edgeTypeModInc e == GlobalDef
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder && getCons (dgl_type l) == Cons
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder $ labEdgesDG dg
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder (groupHistory dg triangleConsRule newDg) le
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaedertriangleConsDG :: DGraph -> LEdge DGLinkLab -> Result DGraph
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaedertriangleConsDG dg (s, t, l) = do
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder let g = dgBody dg
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder markCons l1 l2 = let
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder l' = l {dgl_type = case dgl_type l of
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder ScopedLink a b _ ->
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder ScopedLink a b $
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa $ Proven triangleConsRule $
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa ProofBasis $ Set.fromList $
7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc map dgl_id [l1, l2]
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder in [DeleteEdge (s, t, l), InsertEdge (s, t, l')]
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder checkThm eType =
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder case eType of
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder ThmType (GlobalOrLocalThm _ _) _ _ _ -> True
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder oThm = filter (\ (_, _, ll) -> let e = getRealDGLinkType ll in
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder checkThm (edgeTypeModInc e)
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder [] -> trace "1" $ return dg -- no outgoing thm link found
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder let bases = filter (\ ((s', _, _), _) -> s == s')
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder $ concatMap (\ dge@(_, tt, _) ->
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder map (\ x -> (x, dge))
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder $ filter (\ (_, _, lx) ->
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder getCons (dgl_type lx) == Cons
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder ) $ inn g tt)
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder case bases of
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder [] -> trace "2" $ return dg -- no cons link found
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder ((_, _, cl), (_, _, tl)) : _ -> do
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder let changes = markCons cl tl
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder return $ changesDGH dg changes