123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140 |
- (* Mesh = Zusammenhangskomponente eines einfachen Graphen *)
- signature MESH =
- sig
- structure Key : ORD_KEY
- structure Set : ORD_SET
- structure PairSet : ORD_SET
- structure Map : ORD_MAP
- type mesh = { nodes : Set.set,
- edges : PairSet.set }
- type meshes = mesh Map.map
- type graph = { meshes : meshes,
- node2meshindex : Key.ord_key Map.map }
- val empty_graph : graph
- val add_link : graph -> int * int -> graph
- val links2graph : (int * int) list -> graph
- end
- structure Mesh : MESH =
- struct
- functor PairKeyFn ( Key : ORD_KEY ) : ORD_KEY =
- struct
- type ord_key = Key.ord_key * Key.ord_key
- fun compare (i as (i1, i2), j as (j1, j2)) =
- let val (ia, ib) = if Key.compare (i1, i2) = GREATER
- then (i2, i1) else i
- val (ja, jb) = if Key.compare (i1, i2) = GREATER
- then (j2, j1) else j
- in case Key.compare (ia, ja)
- of EQUAL => Key.compare (ib, jb)
- | unequal => unequal
- end
- end
- (* XXX Unterschiedliche key Typen (statt beide = int)
- fuer die Maps node2meshindex und meshes
- damit der type checker Verwechslungen erkennen kann *)
- structure Key =
- struct
- type ord_key = Int.int
- val compare = Int.compare
- val minkey = 0
- fun nextkey k = k + 1
- end
- structure PairKey = PairKeyFn (Key)
- structure Set = SplaySetFn (Key)
- structure PairSet = SplaySetFn (PairKey)
- structure Map = SplayMapFn (Key)
- type mesh = { nodes : Set.set,
- edges : PairSet.set }
- type meshes = mesh Map.map
- type graph = { meshes : meshes,
- node2meshindex : Key.ord_key Map.map }
- val empty_graph = { meshes = Map.empty,
- node2meshindex = Map.empty }
- fun n2im (g : graph) n =
- case Map.find (#node2meshindex g, n)
- of NONE => NONE
- | SOME mi =>
- SOME (mi, valOf (Map.find (#meshes g, mi)))
- handle Option =>
- raise Fail ("n2im: n = " ^ (Int.toString n) ^
- ", mi = " ^ (Int.toString mi))
- fun maxkey map = Map.foldli (fn (k, _, i) =>
- if Key.compare (k, i) = GREATER
- then k else i)
- Key.minkey
- map
- fun add_link' (g : graph as { meshes, node2meshindex })
- (e as (n1, n2)) =
- case (n2im g n1, n2im g n2)
- of (NONE, NONE) =>
- let val m = { nodes = Set.add (Set.singleton n1, n2),
- edges = PairSet.singleton e }
- val mi = Key.nextkey (maxkey meshes)
- in { meshes = Map.insert (meshes, mi, m),
- node2meshindex = Map.insert
- (Map.insert (node2meshindex,
- n1, mi),
- n2, mi) }
- end
- | (SOME (m1i, { nodes, edges }), NONE) =>
- let val m1' = { nodes = Set.add (nodes, n2),
- edges = PairSet.add (edges, e) }
- in { meshes = Map.insert (meshes, m1i, m1'),
- node2meshindex = Map.insert (node2meshindex, n2, m1i) }
- end
- | (NONE, SOME (m2i, { nodes, edges })) =>
- let val m2' = { nodes = Set.add (nodes, n1),
- edges = PairSet.add (edges, e) }
- in { meshes = Map.insert (meshes, m2i, m2'),
- node2meshindex = Map.insert (node2meshindex, n1, m2i) }
- end
- | (SOME (m1i, { nodes = nodes1, edges = edges1 }),
- SOME (m2i, { nodes = nodes2, edges = edges2 })) =>
- case Key.compare (m1i, m2i)
- of EQUAL =>
- let val m1' = { nodes = nodes1,
- edges = PairSet.add (edges1, e) }
- in { meshes = Map.insert (meshes, m1i, m1'),
- node2meshindex = node2meshindex }
- end
- | unequal =>
- let val (mai, mbi) = if unequal = GREATER
- then (m2i, m1i) else (m1i, m2i)
- val nodesb = if unequal = GREATER
- then nodes1 else nodes2
- val ma = { nodes = Set.union (nodes1, nodes2),
- edges = PairSet.add
- (PairSet.union (edges1, edges2),
- e) }
- in { meshes = #1 (Map.remove (Map.insert (meshes, mai, ma),
- mbi)),
- node2meshindex = foldl (fn (n, map) =>
- Map.insert (map, n, mai))
- node2meshindex
- (Set.listItems nodesb) }
- end
- fun add_link g (e as (n1, n2)) =
- let val (na, nb) = if Key.compare (n1, n2) = GREATER
- then (n2, n1) else e
- in add_link' g (na, nb)
- end
- fun links2graph links = foldl (fn (e, g) => add_link g e)
- empty_graph
- links
- end
|