+
+ // In this loop we have to be very careful not to get into infinite loops and
+ // other problem cases. Specifically, we loop through all of the abstract
+ // type users in the user list, notifying them that the type has been refined.
+ // At their choice, they may or may not choose to remove themselves from the
+ // list of users. Regardless of whether they do or not, we have to be sure
+ // that we only notify each user exactly once. Because the refineAbstractType
+ // method can cause an arbitrary permutation to the user list, we cannot loop
+ // through it in any particular order and be guaranteed that we will be
+ // successful at this aim. Because of this, we keep track of all the users we
+ // have visited and only visit users we have not seen. Because this user list
+ // should be small, we use a vector instead of a full featured set to keep
+ // track of what users we have notified so far.
+ //
+ vector<AbstractTypeUser*> Refined;
+ while (1) {
+ unsigned i;
+ for (i = AbstractTypeUsers.size(); i != 0; --i)
+ if (find(Refined.begin(), Refined.end(), AbstractTypeUsers[i-1]) ==
+ Refined.end())
+ break; // Found an unrefined user?
+
+ if (i == 0) break; // Noone to refine left, break out of here!
+
+ AbstractTypeUser *ATU = AbstractTypeUsers[--i];
+ Refined.push_back(ATU); // Keep track of which users we have refined!
+