Here is a 4th draft of code to merge the new theorems from the Theorem Loader into existing ArrayLists? of theorems. Final tweaks :-)
The problem attempted/solved here is that if the destination list already contains a lot – say 1,000,000 – theorems, and you are adding 100, how do you do it without shifting-down every array element 100 times, which is, on average 100 * 1,000,000 / 2 operations? My idea is to make one pass through the destination array and feed the inserts through a buffer holding the new values of nth element elements. We still have to pass every destination array element through the buffer, but we don't have to move each one 100 / 2 times either.
//********************************************************************/
//* Copyright (C) 2008 MEL O'CAT mmj2 (via) planetmath (dot) org */
//* License terms: GNU General Public License Version 2 */
//* or any later version */
//********************************************************************/
//*4567890123456 (71-character line to adjust editor window) 23456789*/
/*
* MergeSortedArrayLists.java 0.01 08/01/2008
*/
package mmj.util;
import java.util.*;
/**
* Class <code>MergeSortedArrayLists</code> merges elements
* of a sorted source into a sorted destination ArrayList.
*/
public class MergeSortedArrayLists {
private int destGetIndex
= 0;
private int destPutIndex
= 0;
private Object nextDest;
private Object nextSrc;
private ArrayList dest;
private List src;
private Iterator srcIterator;
private LinkedList buf;
private int maxDestBuf;
private int compareResult;
/**
* Does in-place merge of source List into the
* destination ArrayList using the input comparator
* to maintain the sort sequence of the destination
* ArrayList.
* <p>
* A buffer of destination ArrayList elements is used
* as the "in place" merge proceeds. The idea is to
* reduce the number of destination array element shifts
* by making a single pass through the the destination array.
* <p>
* Assumes that input lists are correctly sorted. Makes
* no assumptions about uniqueness of input keys.
* <p>
* @param destList ArrayList sorted in comparator order.
* @param srcList List sorted in comparator order.
* @param comparator Comparator for comparing list object.
* @param abortIfDupsFound triggers IllegalObjectException
* if srcList object equals a destList object
*
* @throws IllegalArgumentException if a srcList object
* equals a destList object and abortIfDupsFound
* is true (the normal situation for Theorem Loader.)
*/
public MergeSortedArrayLists(ArrayList destList,
List srcList,
Comparator comparator,
boolean abortIfDupsFound)
throws IllegalArgumentException {
src = srcList;
srcIterator = src.iterator();
if ((nextSrc = getNextSrc()) == null) {
return;
}
buf = new LinkedList();
dest = destList;
maxDestBuf = dest.size();
dest.ensureCapacity(dest.size() +
src.size());
if ((nextDest = getNextDest()) == null) {
finishUsingSrc();
return;
}
while (true) {
compareResult = comparator.compare(nextSrc,
nextDest);
if (compareResult > 0) { //nextDest < nextSrc
put(nextDest);
if ((nextDest = getNextDest()) == null) {
finishUsingSrc();
break;
}
}
else { //nextSrc <= nextDest
if (compareResult == 0) {
if (abortIfDupsFound) {
throw new IllegalArgumentException(
UtilConstants.
ERRMSG_MERGE_SORTED_LISTS_DUP_ERROR_1
+ nextSrc.toString()
+ UtilConstants.
ERRMSG_MERGE_SORTED_LISTS_DUP_ERROR_2);
}
if ((nextDest = getNextDest()) == null) {
finishUsingSrc();
break;
}
}
//nextSrc < nextDest
put(nextSrc);
if ((nextSrc = getNextSrc()) == null) {
finishUsingDest();
break;
}
}
}
}
private void finishUsingSrc() {
while (nextSrc != null) {
put(nextSrc);
nextSrc = getNextSrc();
}
}
private void finishUsingDest() {
while (nextDest != null) {
put(nextDest);
nextDest = getNextDest();
}
}
private void put(Object object) {
/*
!!! before outputting to dest, make sure that the dest
list element is in the buffer if it is one of the
original dest elements.
*/
if (destPutIndex < dest.size()) {
if (destGetIndex <= destPutIndex) {
// inline: loadNextBufElement();
if (destGetIndex < maxDestBuf) {
buf.addLast(dest.get(destGetIndex++));
}
}
dest.set(destPutIndex,
object);
}
else {
dest.add(object);
}
++destPutIndex;
}
private Object getNextSrc() {
if (srcIterator.hasNext()) {
return srcIterator.next();
}
else {
return null;
}
}
private Object getNextDest() {
if (buf.size() == 0) {
// inline: return loadNextBufElementVirtual();
if (destGetIndex < maxDestBuf) {
return dest.get(destGetIndex++);
}
return null;
}
return buf.removeFirst();
}
// private void loadNextBufElement() {
// if (destGetIndex < maxDestBuf) {
// buf.addLast(dest.get(destGetIndex++));
// }
// }
//
// // used when buf empty and need next element,
// // so buffer is bypassed.
// private Object loadNextBufElementVirtual() {
// if (destGetIndex < maxDestBuf) {
// return dest.get(destGetIndex++);
// }
// return null;
// }
}
P.S. mmj2's LogicalSystem? has one HashMap? of MObj's, while ProofUnifier? and StepSelectorSearch? each maintain a sorted list of Assrt's. In theory, the Proof Unifier could use the StepSelectorSearch? list, which would eliminate some "waste", but the change would not be 100% transparent to users (though still quite acceptable I think, given usage patterns (which I imagine to exist :-) ).