-
Notifications
You must be signed in to change notification settings - Fork 0
/
Inductive_graphs.fold
256 lines (199 loc) · 9.12 KB
/
Inductive_graphs.fold
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
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
{- | 'Haws.TGraph is an abstract representation of graphs were
nodes and edges are of the same type and where edges can be nodes -}
import Data.Maybe
import Data.Set
import Haws.TContext
import Haws.Subst
import Prelude hiding: [pred, succ, map, null]
interface Graph =
-- An inductive type definition of the Graph.
type Graph =
| Empty
| Context [Edge] Node [Edge] & Graph
-- An empty 'Graph'.
empty <Eq Node> :: Graph Node
-- Match a 'Graph' by decomposing it into the 'Context' found for the given
-- node and the remaining 'Graph'.
match <Ord a, Show a> :: a -> g a -> (Context a, g a)?
-- Returns the nodes of the graph.
nodes <Ord A, Show A> :: G A -> Set A
contains :: <Ord a, Show A> => a -> gr a -> Bool
contains n g = member n (nodes g)
end
fold_graph <Show a, Ord a> :: b -> (Context a -> b -> b) -> g a -> b
fold_graph e h g =
if (empty? (nodes g)) then: e else:
match (match_any g) {
None => Error "fold_graph: Cannot decomp graph"
Some (ctx, g') => h ctx (fold_graph e h g')
}
fold_graph <Show a, Ord a> :: b -> (Context a -> b -> b) -> g a -> b
fold_graph e h g =
if (empty? (nodes g)) then: e
else: match (match_any g) {
None => Error "fold_graph: Cannot decomp graph"
Some (ctx, g') => h ctx (fold_graph e h g')
}
fold_graph <Show a, Ord a> :: b -> (Context a -> b -> b) -> g a -> b
fold_graph e h g =
if | empty? (nodes g) -> e
| else -> case (match_any g)
| None -> Error "cannot match graph"
| Some (ctx, g') -> h ctx (fold_graph e h g')
fold_graph <Show a, Ord a> :: b -> (Context a -> b -> b) -> g a -> b
function fold_graph e h g
if | empty? (nodes g) -> e
| else -> case (match_any g)
| None -> Error "cannot match graph"
| Some (ctx, g') -> h ctx (fold_graph e h g')
end
end
end
instance TGraph gr where
-- essential operations
-- | An empty 'Graph'.
gEmpty :: gr a
-- | Decompose a 'Graph' into the 'TContext' found for the given node and the
-- remaining 'Graph'.
-- This function is similar to 'match' in 'Data.Graph.Inductive' (we prefer the name 'decomp')
decomp :: (Ord a, Show a) => a -> gr a -> Maybe (TContext a, gr a)
-- | returns the nodes of the graph
nodes :: (Ord a, Show a) => gr a -> Set a
contains :: (Ord a, Show a) => a -> gr a -> Bool
contains n g = member n (nodes g)
insertTriple :: (Show a, Ord a) => (a,a,a) -> gr a -> gr a
insertNode :: (Show a, Ord a) => a -> gr a -> gr a
-- | 'decompAny' it decomposes a graph taking an arbitrary node (the head of 'nodes').
-- It is similar 'matchAny' in 'Data.Graph.Inductive'
decompAny :: (Ord a, Show a) => gr a -> Maybe (TContext a, gr a)
decompAny g | null ns = Nothing
| otherwise = decomp (head (elems ns)) g
where ns = nodes g
-- | We could have let 'comp' as primitive and define 'insertTriple' in terms of 'comp'
comp :: (Ord a, Show a) => TContext a -> gr a -> gr a
comp ctx gr =
let n = node ctx
gr0 = insertNode n gr
gr1 = fold (\(p,x) g -> insertTriple (x,p,n) g) gr0 (pred ctx)
gr2 = fold (\(p,y) g -> insertTriple (n,p,y) g) gr1 (succ ctx)
gr3 = fold (\(x,y) g -> insertTriple (x,n,y) g) gr2 (rels ctx)
in gr3
insertTriples :: (Show a, Ord a) => Set (a,a,a) -> gr a -> gr a
insertTriples ts g = Data.Set.foldr (\t r -> insertTriple t r) g ts
fold_graph <Show A, Ord A> :: B -> (Context A -> B -> B) -> G A -> B
fold_graph e h g =
if (empty? (nodes g)) then: e else: {
match (match_any g) {
None => Error "fold_graph: Cannot decomp graph"
Some (ctx, g') => h ctx (fold_graph e h g')
}
}
fold_graph <Show A, Ord A> :: B -> (Context A -> B -> B) -> G A -> B
fold_graph e h g =
if (empty? (nodes g)) then: e else:
match (match_any g)
None => Error "fold_graph: Cannot decomp graph"
Some (ctx, g') => h ctx (fold_graph e h g')
end
end
fold_graph <Show A, Ord A> :: B -> (Context A -> B -> B) -> G A -> B
fold_graph e h g =
if (empty? (nodes g)) then: e else:
match (match_any g):
None => Error "fold_graph: Cannot decomp graph"
Some (ctx, g') => h ctx (fold_graph e h g')
foldTGraphOrd :: (Ord a, Show a) => b -> (TContext a -> b -> b) -> gr a -> b
foldTGraphOrd e h g
| null (nodes g) = e
| otherwise = case decomp (findMin (nodes g)) g of
Nothing -> error $ "foldTGraphOrd: Node not found in graph "
Just (ctx,g') -> h ctx (foldTGraph e h g')
showFolds :: (Show a, Ord a, TGraph gr) => gr a -> String
showFolds = foldTGraphOrd "empty\n" f
where f :: (Show a) => TContext a -> String -> String
f ctx r = show ctx ++ "\n" ++ r
triples :: (Show a, Ord a) => gr a -> Set (a,a,a)
triples = foldTGraph empty (\d r -> triplesCtx d `union` r)
isEmpty :: (Ord a, Show a) => gr a -> Bool
isEmpty gr = null (nodes gr)
context :: (TGraph gr, Ord a, Show a) => a -> gr a -> TContext a
context n gr = case decomp n gr of
Nothing -> error "Cannot get context"
Just (ctx,_) -> ctx
-- simplified map
mapTGraph :: (Ord a, Show a,
Ord b, Show b) => (a -> b) -> gr a -> gr b
mapTGraph f = gmapTGraph (\ctx -> (mapCtx f ctx))
-- mapTGraph2 is equivalent to mapTGraph (prove it?)
mapTGraph2 :: (Ord a, Show a,
Ord b, Show b) => (a -> b) -> gr a -> gr b
mapTGraph2 f = foldTGraph gEmpty (\ctx g -> comp (mapCtx f ctx) g)
-- generalized map
gmapTGraph :: (Ord a, Show a,
Ord b, Show b) => (TContext a -> TContext b) -> gr a -> gr b
gmapTGraph f g = foldTGraph gEmpty (\ctx r -> comp (f ctx) r) g
appSubstTGraph :: ( Ord a, Show a, VarCheck a, TGraph gr
) => Subst a -> gr a -> gr a
appSubstTGraph s = gmapTGraph (appSubstCtx s)
where appSubstCtx :: (Ord a, Show a, VarCheck a) => Subst a -> TContext a -> TContext a
appSubstCtx s = mapCtx (\x -> case varCheck x of
Nothing -> x
Just v -> appSubst s v x)
-- | reverse the edges in a graph
grev :: (Show a, Ord a) => gr a -> gr a
grev = gmapTGraph swapCtx
-- | Generates an undirected graph from a graph (all links will be both directions)
undir :: (Ord a, Show a) => gr a -> gr a
undir = gmapTGraph (\ctx -> let predSucc = pred ctx `union` succ ctx
revRels = map (\(x,y) -> (y,x)) (rels ctx)
in ctx { pred = predSucc,
succ = predSucc,
rels = (rels ctx) `union` revRels
})
-- | returns the successors of a node in a graph
gsuc :: (Ord a, Show a) => a -> gr a -> [a]
gsuc n g = case decomp n g of
Nothing -> []
Just (ctx,g') -> toList (map snd (succ ctx))
-- | returns the successors of a node in a graph
deg :: (Ord a, Show a) => a -> gr a -> Int
deg n g = case decomp n g of
Nothing -> 0
Just (ctx,g') -> size (succ ctx) + size (pred ctx)
-- | returns the successors of a node in a graph
delete :: (Ord a, Show a) => a -> gr a -> Maybe (gr a)
delete n g = case decomp n g of
Nothing -> Nothing
Just (ctx,g') -> Just g'
isEdge :: (Ord a, Show a) => a -> gr a -> Bool
isEdge n gr = case decomp n gr of
Nothing -> False
Just (ctx,_) -> not (null (rels ctx))
isVertex :: (Ord a, Show a) => a -> gr a -> Bool
isVertex n gr = case decomp n gr of
Nothing -> False
Just (ctx,_) -> not (null (succ ctx)) || not (null (pred ctx))
gTake :: (Ord a, Show a) => Int -> gr a -> gr a
gTake n gr
| n == 0 = gEmpty
| n > 0 = case decompAny gr of
Nothing -> error "gTake: Cannot decomp"
Just (ctx,gr') -> let grec = gTake (n - 1) gr'
in comp (filterNodes (nodes grec) ctx) (gTake (n - 1) grec)
| otherwise = error "gTake: Negative argument"
-- This definition generates a decomposed graph...not needed
-- TODO: just remove the following code?
data DecompTGraph a = EmptyTGraph
| Extend (TContext a) (DecompTGraph a)
deriving Show
decompTGraph ::
( Ord a,
Show a
) => TGraph gr => gr a -> DecompTGraph a
decompTGraph gr =
if isEmpty gr then EmptyTGraph
else
let n = findMin (nodes gr)
in case decomp n gr of
Just (mctx,gr) -> Extend mctx (decompTGraph gr)
Nothing -> error ("Not possible to decompose graph from node " ++ show n)