1119418Sobrien(*
215813Sse *  gr_t.sml  --  graph implementations based on balanced binary search tress
315813Sse *
415813Sse *  COPYRIGHT (c) 1997 by Martin Erwig.  See COPYRIGHT file for details.
515813Sse *)
615813Sse
715813Sse(*
815813Sse   structures and functors defined:
915813Sse
1015813Sse    Graph,
1115813Sse    UnlabGraph:
1215813Sse      A graph is represented by pair (t,m) where t is a search tree
1315813Sse      storing labels, predecessors, and successors, and m is
1415813Sse      the maximum node value in the domain of t.
1515813Sse
1615813Sse   GraphFwd,
1715813Sse   UnlabGraphFwd:
1815813Sse     Only successors are stored. This speeds up the operations
1915813Sse     "suc" and "anySuc" that do not access the full context
20119418Sobrien
21119418Sobrien   Employed utilities:
22119418Sobrien     UTuple:
2315813Sse       p1 (x,y) = x
2473374Simp       P2 f (x,y) = (x,f y)
2550852Speter     UList:
2615813Sse       cons x l = x::l
2752247Smdodd       select f p l = map f (filter p l)
2850852Speter*)
2950852Speter
3052247Smdodd
3150852Speterlocal (* local scope for auxiliary definitions *)
3252247Smdodd
3352247Smdodd(*
3450852Speter   auxiliary structures:
3550852Speter
3650852Speter     AdjUtil     utilities on adjacency structures, just the definitions
3750852Speter                 shared by MapUtil and MapUtilFwd
3815813Sse     MapUtil     utilities for (node->context) maps
39119277Simp     MapUtilFwd  utilities for maps, for forward represenation
40119277Simp
4152247Smdodd     ShareAll    function definitions shared by all implementations
4251442Speter     ShareFwd    function definitions shared by forward implementations
4350852Speter*)
4424995Sdavidn
4524995Sdavidnstructure AdjUtil =
4650852Speterstruct
4750852Speter  (*
4824995Sdavidn     updAdj (t,l,f)     repeatedly updates the context entries for
4924995Sdavidn                        each node in l by adding either a successor or
5024995Sdavidn                        a predecessor as specified by f
5128210Sdanny     updLabAdj          ... similar for labeled graphs
5224995Sdavidn     remFrom (t,v,l,Fi) remove v from the successor or predecessor lists of
5324995Sdavidn                        all nodes in l.
5424995Sdavidn                        T2 : pred in full tree
5531347Smsmith                        T3 : suc  in full tree
5633893Sse                        P2 : suc  in fwd  tree --> is not used
5734645Sdanny     remFromLab        ... similar in labeled graphs
5824995Sdavidn     any               selects arbitrary node and apply match or matchFwd
5924995Sdavidn  *)
6015813Sse  structure M = IntBinaryMapUpd
6192739Salfred  open GraphExceptions UTuple UGeneral
6292739Salfred
6316289Salex  fun updAdj (t,[],f)   = t
6450852Speter   |  updAdj (t,v::l,f) = updAdj (M.update (t,v,f),l,f)
6550852Speter      handle Binaryset.NotFound => raise Edge
6615813Sse  fun updLabAdj (t,[],f)         = t
6750852Speter   |  updLabAdj (t,(lab,v)::l,f) = updLabAdj (M.update (t,v,f lab),l,f)
6824995Sdavidn      handle Binaryset.NotFound => raise Edge
6924995Sdavidn  fun remFrom (t,v,[],F)   = t
7024995Sdavidn   |  remFrom (t,v,x::l,F) =
7124995Sdavidn      remFrom (M.update (t,x,F (List.filter (neq v))),v,l,F)
7250852Speter  fun remFromLab (t,v,[],F)   = t
7350852Speter   |  remFromLab (t,v,(_,x)::l,F) =
7450852Speter      remFromLab (M.update (t,x,F (List.filter (neq v o p2))),v,l,F)
7550852Speter  fun any proj (g as (t,m)) = proj (#1 (valOf (M.findSome t)),g)
7650852Speter                              handle Option => raise Match
7750852Speterend
7815813Sse
7915813Ssestructure MapUtil =
8050852Speterstruct
8150852Speter  (*
8215813Sse     addSuc, addPred   add a node to successor/predecessor list
8364777Snyan                       (functions to be passed as arguments to M.update)
8464777Snyan     addLabSuc,
8564777Snyan     addLabPred        ... similar for labeled graphs
8652247Smdodd     mkContext         rearranges map entry to a context value
87119690Sjhb  *)
8852247Smdodd  open AdjUtil
8952247Smdodd  fun addSuc v (l,p,s) = (l,p,v::s)
9052247Smdodd  fun addPred v (l,p,s) = (l,v::p,s)
9152247Smdodd  fun addLabSuc v lab (l,p,s) = (l,p,(lab,v)::s)
9252247Smdodd  fun addLabPred v lab (l,p,s) = (l,(lab,v)::p,s)
9352247Smdodd  fun mkContext (n,(l,p,s)) = (p,n,l,s) handle Option => raise Match
9452247Smdodd  fun mkFwdAdj (l,p,s) = (l,s) handle Option => raise Match
9552247Smdodd  fun mkBwdAdj (l,p,s) = (l,p) handle Option => raise Match
9652247Smdoddend
9752247Smdodd
9852247Smdoddstructure MapUtilFwd =
9952247Smdoddstruct
10052247Smdodd  open AdjUtil
10152247Smdodd  fun addSuc v (l,s) = (l,v::s)
10252247Smdodd  fun addLabSuc v lab (l,s) = (l,(lab,v)::s)
10352247Smdodd  fun mkFwd (n,(t,(l,s)),m:int) = ((l,s),(t,if m=n then m-1 else m))
10452247Smdoddend
10552247Smdodd
10652247Smdodd
10750852Speter(*
10815813Sse   shared implementations
10950852Speter*)
11050852Speterstructure ShareAll =
11150852Speterstruct
11250852Speter  structure M = IntBinaryMapUpd
11315813Sse
11450852Speter  val empty              = (M.empty,0)
11550852Speter  fun isEmpty  (t,_)     = case (M.findSome t) of NONE=>true | _=>false
11615813Sse  fun nodes    (t,_)     = map UTuple.p1 (M.listItemsi t)
11750852Speter  fun noNodes  (t,_)     = M.numItems t
11850852Speter  fun newNodes i (_,m)   = UGeneral.to (m+1,m+i)
11950852Speterend
12050852Speter
12150852Speter
12215813Ssestructure ShareFwd =
123113506Smdoddstruct
124113506Smdodd  structure M = IntBinaryMapUpd
125113506Smdodd  open GraphExceptions
126
127  fun match       _  = raise NotImplemented
128  fun matchAny    _  = raise NotImplemented
129  fun matchFwd    _  = raise NotImplemented (* must scan all edges to ...  *)
130  fun matchAnyFwd _  = raise NotImplemented (* ... remove n from suc-lists *)
131  fun context     _  = raise NotImplemented
132  fun bwd         _  = raise NotImplemented
133  fun pred        _  = raise NotImplemented
134  fun ufold _ _ _       = raise NotImplemented
135  fun gfold _ _ _ _ _ _ = raise NotImplemented
136  fun fwd (n,(t,_))  = valOf (M.find (t,n)) handle Option => raise Match
137  fun labNodes (t,_) = map (UTuple.P2 UTuple.p1) (M.listItemsi t)
138end
139
140
141in (* scope of auxiliary definitions *)
142
143
144structure Graph : GRAPH =
145struct
146  structure M = IntBinaryMapUpd
147  open GraphNode GraphExceptions MapUtil UTuple
148
149  type ('a,'b) graph = ('a * ('b * node) list * ('b * node) list) M.map * int
150
151  structure Types = GraphTypes (struct type ('a,'b) graph=('a,'b) graph end)
152  open Types
153
154  (* exported functions *)
155
156  open ShareAll
157
158  fun embed ((pred,n,l,suc),(t,m)) =
159      case M.find (t,n) of NONE =>
160         let val t1 = M.insert (t,n,(l,pred,suc))
161             val t2 = updLabAdj (t1,pred,addLabSuc n)
162             val t3 = updLabAdj (t2,suc,addLabPred n)
163          in
164             (t3,Int.max (n,m))
165         end
166      | _ => raise Node
167
168  fun match (n,(t,m)) =
169      let val (t1,(l,p,s)) = M.remove (t,n)
170          val p' = List.filter (neq n o p2) p
171          val s' = List.filter (neq n o p2) s
172          val t2 = remFromLab (t1,n,s',T2) (* rem. n from each pred-list of s *)
173          val t3 = remFromLab (t2,n,p',T3) (* rem. n from each suc-list of p *)
174       in ((p',n,l,s),(t3,if m=n then m-1 else m)) end
175(*
176      handle Binaryset.NotFound => raise Match
177*)
178      handle Binaryset.NotFound =>
179      (print ("match "^Int.toString n^" in graph:\n");
180       map (fn x=>print (Int.toString x^",")) (nodes (t,m));
181       raise Match)
182
183  fun matchFwd    n_g     = P1 q34 (match n_g)
184  fun matchAny    g       = any match g
185  fun matchAnyFwd g       = any matchFwd g
186  (*
187  fun matchOrd (n,l,l',g) = let val ((p,_,lab,s),g') = match (n,g)
188      in ((SortEdges.labsort (l,p),n,lab,SortEdges.labsort (l',s)),g') end
189  fun matchOrdFwd (n,l,g) = let val ((lab,s),g') = matchFwd (n,g)
190      in ((lab,SortEdges.labsort (l,s)),g') end
191  *)
192
193  fun context  (n,(t,_))  = mkContext (n,valOf (M.find (t,n)))
194  fun fwd      (n,(t,_))  = mkFwdAdj (valOf (M.find (t,n)))
195  fun bwd      (n,(t,_))  = mkBwdAdj (valOf (M.find (t,n)))
196  fun suc      g          = map p2 (p2 (fwd g))
197  fun pred     g          = map p2 (p2 (bwd g))
198  fun labNodes (t,_)      = map (P2 t1) (M.listItemsi t)
199
200  fun ufold f u g = if isEmpty g then u else
201                    let val (c,g') = matchAny g
202                     in f (c,ufold f u g') end
203
204  fun gfold f d b u l g = if isEmpty g then u else
205      let fun gfold1 v g =
206              let val (c as (_,_,l,_),g1) = match (v,g)
207                  val (r,g2) = gfoldn (f c) g1
208               in (d (l,r),g2) end
209          and gfoldn []     g = (u,g)
210           |  gfoldn (v::l) g =
211              let val (x,g1) = gfold1 v g
212                  val (y,g2) = gfoldn l g1
213               in (b (x,y),g2) end
214              handle Match => gfoldn l g
215        in
216           #1 (gfoldn l g)
217       end
218
219  fun mkgr (nl,el) =
220      let fun insNodes (t,i,[])   = t
221           |  insNodes (t,i,v::l) = insNodes (M.insert (t,i,(v,[],[])),i+1,l)
222          fun insEdges (t,[])          = t
223           |  insEdges (t,(v,w,l)::el) =
224              let val t1 = M.update (t,v,addLabSuc w l)
225                  val t2 = M.update (t1,w,addLabPred v l)
226               in insEdges (t2,el) end
227              handle Binaryset.NotFound => raise Edge
228       in
229          (insEdges (insNodes (M.empty,0,nl),el),length nl-1)
230      end
231  fun adj (t,_) = map (fn (v,(l,p,s))=>(v,(l,s))) (M.listItemsi t)
232end (* structure Graph *)
233
234
235structure UnlabGraph : UNLAB_GRAPH =
236struct
237  structure M = IntBinaryMapUpd
238  open GraphNode GraphExceptions MapUtil UTuple
239
240  type 'a graph = ('a * node list * node list) M.map * int
241
242  structure Types = UnlabGraphTypes (struct type 'a graph='a graph end)
243  open Types
244
245  (* exported functions *)
246
247  open ShareAll
248
249  fun embed ((pred,n,l,suc),(t,m)) =
250      case M.find (t,n) of NONE =>
251         let val t1 = M.insert (t,n,(l,pred,suc))
252             val t2 = updAdj (t1,pred,addSuc n)
253             val t3 = updAdj (t2,suc,addPred n)
254          in (t3,Int.max (n,m)) end
255      | _ => raise Node
256
257  fun match (n,(t,m)) =
258      let val (t1,(l,p,s)) = M.remove (t,n)
259          val p' = List.filter (neq n) p
260          val s' = List.filter (neq n) s
261          val t2 = remFrom (t1,n,s',T2) (* rem. n from each pred-list of s *)
262          val t3 = remFrom (t2,n,p',T3) (* rem. n from each suc-list of p *)
263       in ((p',n,l,s),(t3,if m=n then m-1 else m)) end
264      handle Binaryset.NotFound => raise Match
265
266  fun matchFwd    n_g    = P1 q34 (match n_g)
267  fun matchAny    g      = any match g
268  fun matchAnyFwd g      = any matchFwd g
269  fun context  (n,(t,_)) = mkContext (n,valOf (M.find (t,n)))
270  fun fwd      (n,(t,_)) = mkFwdAdj (valOf (M.find (t,n)))
271  fun bwd      (n,(t,_)) = mkBwdAdj (valOf (M.find (t,n)))
272  fun suc      g         = p2 (fwd g)
273  fun pred     g         = p2 (bwd g)
274  fun labNodes (t,_)     = map (P2 t1) (M.listItemsi t)
275
276  fun ufold f u g = if isEmpty g then u else
277                    let val (c,g') = matchAny g
278                     in f (c,ufold f u g') end
279
280  fun gfold f d b u l g = if isEmpty g then u else
281      let fun gfold1 v g =
282              let val (c as (_,_,l,_),g1) = match (v,g)
283                  val (r,g2) = gfoldn (f c) g1
284               in (d (l,r),g2) end
285          and gfoldn []     g = (u,g)
286           |  gfoldn (v::l) g =
287              let val (x,g1) = gfold1 v g
288                  val (y,g2) = gfoldn l g1
289               in (b (x,y),g2) end
290              handle Match => gfoldn l g
291        in
292           #1 (gfoldn l g)
293       end
294
295  fun mkgr (nl,el) =
296      let fun insNodes (t,_,[])   = t
297           |  insNodes (t,i,v::l) = insNodes (M.insert (t,i,(v,[],[])),i+1,l)
298          fun insEdges (t,[])        = t
299           |  insEdges (t,(v,w)::el) =
300              let val t1 = M.update (t,v,addSuc w)
301                  val t2 = M.update (t1,w,addPred v)
302               in insEdges (t2,el) end
303              handle Binaryset.NotFound => raise Edge
304       in
305          (insEdges (insNodes (M.empty,0,nl),el),length nl-1)
306      end
307  fun adj (t,_) = map (fn (v,(l,p,s))=>(v,(l,s))) (M.listItemsi t)
308end (* structure UnlabGraph *)
309
310
311structure GraphFwd : GRAPH =
312struct
313  structure M = IntBinaryMapUpd
314  open GraphExceptions MapUtilFwd UTuple
315
316  type ('a,'b) graph = ('a * ('b * GraphNode.node) list) M.map * int
317
318  structure Types = GraphTypes (struct type ('a,'b) graph=('a,'b) graph end)
319  open Types
320
321  (* exported functions *)
322
323  open ShareAll
324  open ShareFwd
325
326  fun embed ((pred,n,l,suc),(t,m)) =
327      case M.find (t,n) of NONE =>
328         let val t1 = M.insert (t,n,(l,suc))
329             val t2 = updLabAdj (t1,pred,addLabSuc n)
330          in
331             (t2,Int.max (n,m))
332         end
333      | _ => raise Node
334
335  fun matchOrd    _ = raise NotImplemented
336  fun matchOrdFwd _ = raise NotImplemented
337  fun suc         g = map p2 (p2 (fwd g))
338
339  fun mkgr (nl,el) =
340      let fun insNodes (t,i,[])   = t
341           |  insNodes (t,i,v::l) = insNodes (M.insert (t,i,(v,[])),i+1,l)
342          fun insEdges (t,[])          = t
343           |  insEdges (t,(v,w,l)::el) = insEdges (M.update (t,v,addLabSuc w l),el)
344              handle Binaryset.NotFound => raise Edge
345       in
346          (insEdges (insNodes (M.empty,0,nl),el),length nl-1)
347      end
348  fun adj (t,_) = M.listItemsi t
349end (* structure GraphFwd *)
350
351
352structure UnlabGraphFwd : UNLAB_GRAPH =
353struct
354  structure M = IntBinaryMapUpd
355  open GraphNode GraphExceptions MapUtilFwd UTuple
356
357  type 'a graph = ('a * node list) M.map * int
358
359  structure Types = UnlabGraphTypes (struct type 'a graph='a graph end)
360  open Types
361
362  (* exported functions *)
363
364  open ShareAll
365  open ShareFwd
366
367  fun embed ((pred,n,l,suc),(t,m)) =
368      case M.find (t,n) of NONE =>
369         let val t1 = M.insert (t,n,(l,suc))
370             val t2 = updAdj (t1,pred,addSuc n)
371          in
372             (t2,Int.max (n,m))
373         end
374      | _ => raise Node
375
376  fun suc         g         = p2 (fwd g)
377
378  fun mkgr (nl,el) =
379      let fun insNodes (t,_,[])   = t
380           |  insNodes (t,i,v::l) = insNodes (M.insert (t,i,(v,[])),i+1,l)
381          fun insEdges (t,[])        = t
382           |  insEdges (t,(v,w)::el) = insEdges (M.update (t,v,addSuc w),el)
383              handle Binaryset.NotFound => raise Edge
384       in
385          (insEdges (insNodes (M.empty,0,nl),el),length nl-1)
386      end
387  fun adj (t,_) = M.listItemsi t
388end (* structure UnlabGraphFwd *)
389
390end (* of local scope *)
391