src/main/java/wybs/util/AbstractSyntacticHeap.java
private static SyntacticItem substitute(SyntacticItem item, SyntacticItem from, SyntacticItem to,
			Map<SyntacticItem, SyntacticItem> mapping) {
		SyntacticItem sItem = mapping.get(item);
		if (sItem != null) {
			// We've previously substituted this item already to produce a
			// potentially updated item. Therefore, simply return that item to
			// ensure the original aliasing structure of the ancestor(s) is
			// properly preserved.
			return sItem;
		} else if (item == from) {
			// We've matched the item being replaced, therefore return the item
			// to which it is being replaced.
			return to;
		} else {
			SyntacticItem nItem = item;
			// We need to recursively descend into children of this item looking
			// for the item to replace. The challenge here is that we need to
			// ensure the original item is preserved as is if there is no
			// change.
			SyntacticItem[] children = item.getAll();
			// Initially, this will alias children. In the event of a child
			// which is actually updated, then this will refer to a new array.
			// That will be the signal that we need to create a new item to
			// return.
			SyntacticItem[] nChildren = children;
			if (children != null) {
				for (int i = 0; i != children.length; ++i) {
					SyntacticItem child = children[i];
					// Check for null, since we don't want to try and substitute
					// into null.
					if (child != null) {
						// Perform the substitution in the given child
						SyntacticItem nChild = substitute(child, from, to, mapping);
						// Check whether anything was actually changed by the
						// substitution.
						if (nChild != child && children == nChildren) {
							// Yes, the child changed and we haven't already
							// cloned the children array. Hence, we'd better
							// clone it now to make sure that the original item
							// is preserved.
							nChildren = Arrays.copyOf(children, children.length);
						}
						nChildren[i] = nChild;
					}
				}
				// Now, clone the original item if necessary. This is only
				// necessary if the children array as been updated in some way.
				if (children != nChildren) {
					// Create the new item which, at this point, will be
					// detached.
					nItem = item.clone(nChildren);
				}
			}
			mapping.put(item, nItem);
			return nItem;
		}
	}
private static SyntacticItem substitute(SyntacticItem item, SyntacticItem from, SyntacticItem to,
			Map<SyntacticItem, SyntacticItem> mapping) {
		SyntacticItem sItem = mapping.get(item);
		if (sItem != null) {
			// We've previously substituted this item already to produce a
			// potentially updated item. Therefore, simply return that item to
			// ensure the original aliasing structure of the ancestor(s) is
			// properly preserved.
			return sItem;
		} else if (item == from) {
			// We've matched the item being replaced, therefore return the item
			// to which it is being replaced.
			return to;
		} else {
			SyntacticItem nItem = item;
			// We need to recursively descend into children of this item looking
			// for the item to replace. The challenge here is that we need to
			// ensure the original item is preserved as is if there is no
			// change.
			SyntacticItem[] children = item.getAll();
			// Initially, this will alias children. In the event of a child
			// which is actually updated, then this will refer to a new array.
			// That will be the signal that we need to create a new item to
			// return.
			SyntacticItem[] nChildren = children;
			if (children != null) {
				for (int i = 0; i != children.length; ++i) {
					SyntacticItem child = children[i];
					// Check for null, since we don't want to try and substitute
					// into null.
					if (child != null) {
						// Perform the substitution in the given child
						SyntacticItem nChild = substitute(child, from, to, mapping);
						// Check whether anything was actually changed by the
						// substitution.
						if (nChild != child && children == nChildren) {
							// Yes, the child changed and we haven't already
							// cloned the children array. Hence, we'd better
							// clone it now to make sure that the original item
							// is preserved.
							nChildren = Arrays.copyOf(children, children.length);
						}
						nChildren[i] = nChild;
					}
				}
				// Now, clone the original item if necessary. This is only
				// necessary if the children array as been updated in some way.
				if (children != nChildren) {
					// Create the new item which, at this point, will be
					// detached.
					nItem = item.clone(nChildren);
				}
			}
			mapping.put(item, nItem);
			return nItem;
		}
	}
Helper method for above.

@param mapping
A mapping from the original syntactic items to the cloned
syntactic items. This is necessary to preserve the aliasing
structure in the resulting cloned item.