| 
					
				 | 
			
			
				@@ -1,79 +1,117 @@ 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				 (* Mesh = Zusammenhangskomponente eines einfachen Graphen *) 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				  
			 | 
		
	
		
			
				 | 
				 | 
			
			
				+(* XXX Unterschiedliche key Typen (statt beide = int) 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				+       für die Maps node2meshindex und meshes 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				+       um Verwechslungen durch den type checker zu erkennen *) 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				+ 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				 structure Mesh = 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				 struct 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				  
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-	structure OrdInt : ORD_KEY = 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				+	functor PairKeyFn ( Key : ORD_KEY ) : ORD_KEY = 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				 	struct 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-		type ord_key = Int.int 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-		val compare = Int.compare 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				+		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 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				  
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-	structure OrdIntPair : ORD_KEY = 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				+	structure Key = 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				 	struct 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-		type ord_key = OrdInt.ord_key * OrdInt.ord_key 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-		fun compare (i as (i1, i2), j as (j1, j2)) = 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-			let val (ia, ib) = if i2 < i1 then (i2, i1) else i 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-			    val (ja, jb) = if j2 < j1 then (j2, j1) else j 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-			in case OrdInt.compare (ia, ja) 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-			     of EQUAL => OrdInt.compare (ib, jb) 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-			      | unequal => unequal 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-		end 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				+		type ord_key = Int.int 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				+		val compare = Int.compare 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				+		val minkey = 0 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				+		fun nextkey k = k + 1 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				 	end 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				  
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-	structure Set = SplaySetFn (OrdInt) 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-	structure PairSet = SplaySetFn (OrdIntPair) 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				+	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 list 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				+	type meshes = mesh Map.map 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				+	type graph = { meshes : meshes, 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				+		       node2meshindex : Key.ord_key Map.map } 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				+ 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				+	val empty = { meshes = Map.empty, node2meshindex = Map.empty } 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				  
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-	fun find_mesh _  [] = NONE 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-	  | find_mesh id ((mesh : mesh) :: meshes) = 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-		if Set.member ((#nodes mesh), id) 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-		then SOME mesh 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-		else find_mesh id meshes 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				+	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)) 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				  
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-	local 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-		fun add_link' (k as (k1, k2)) [] = 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-			[{ nodes = Set.add (Set.singleton k1, k2), 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-			   edges = PairSet.singleton k }] 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-		  | add_link' (k as (k1, k2)) ((mesh as { nodes, edges }) :: meshes) = 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-			if Set.member (nodes, k1) 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-			then 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-				if Set.member (nodes, k2) 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-				then { nodes = nodes, 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-				       edges = PairSet.add (edges, k) } 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-				     :: meshes 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-				else case find_mesh k2 meshes 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-				       of NONE => { nodes = Set.add (nodes, k2), 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-						    edges = PairSet.add (edges, k) } 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-						  :: meshes 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-					| SOME { nodes = nodes2, edges = edges2 } 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-					       => { nodes = Set.union (nodes, nodes2), 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-						    edges = PairSet.add 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-								(PairSet.union (edges, edges2), 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-								 k) } 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-						  :: (List.filter 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-							(fn m => not (Set.member (#nodes m, k2))) 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-							meshes) 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-			else 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-				if Set.member (nodes, k2) 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-				then case find_mesh k1 meshes 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-				       of NONE => { nodes = Set.add (nodes, k1), 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-						    edges = PairSet.add (edges, k) } 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-						  :: meshes 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-					| SOME { nodes = nodes1, edges = edges1 } 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-					       => { nodes = Set.union (nodes, nodes1), 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-						    edges = PairSet.add (PairSet.union (edges, edges1), k) } 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-						  :: (List.filter 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-							(fn m => not (Set.member (#nodes m, k1))) 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-							meshes) 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-				else mesh :: (add_link' k meshes) 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-	in 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-		fun add_link (k as (k1, k2)) meshes = 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-			let val (ka, kb) = if k2 < k1 then (k2, k1) else k 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-			in add_link' (ka, kb) meshes 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				+	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 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				-	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 
			 | 
		
	
		
			
				 | 
				 | 
			
			
				 end 
			 |