Cross Reference: /hets/Proofs/TriangleCons.hs
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 Maeder{- |
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
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen KuksaMaintainer : Christian.Maeder@dfki.de
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederStability : provisional
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaederPortability : non-portable(Logic)
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc-}
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maedermodule Proofs.TriangleCons where
75067b1beba1380cde707c30e7fc050d86f6927fKarl Luc
7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Lucimport Static.DevGraph
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Static.DgUtils
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Static.History
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Common.Consistency
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Common.Result
e036e115761fe7c09c210c337440a1864d794093Martha Rohteimport Common.LibName
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport qualified Data.Map as Map
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport qualified Data.Set as Set
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Data.Graph.Inductive.Graph
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Control.Monad
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maederimport Debug.Trace
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaedertriangleConsRule :: DGRule
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian MaedertriangleConsRule = DGRule "TriangleCons"
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder
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 )
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder $ labEdgesDG dg
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder return $ Map.insert ln
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder (groupHistory dg triangleConsRule newDg) le
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder
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 $
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder ConsStatus
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder Cons
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder Cons
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa $ Proven triangleConsRule $
a8ddb13beb092672c9f537ef1cf2e14f1f8a8f26Eugen Kuksa ProofBasis $ Set.fromList $
7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc map dgl_id [l1, l2]
7b1111ca3b126f71cce47e60ce4b56e6f92422e9Karl Luc dt -> dt}
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 _ -> False
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder oThm = filter (\ (_, _, ll) -> let e = getRealDGLinkType ll in
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder checkThm (edgeTypeModInc e)
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder ) $ out g t
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder case oThm of
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder [] -> trace "1" $ return dg -- no outgoing thm link found
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder _ -> do
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 oThm
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
5096f518ac5380a0834a09b22a8b38fabe247bf5Christian Maeder