/** \page idsystem The Lurch ID System
*
* <h1>Purpose</h1>
*
* In Lurch Documents, we will need a simple way for one part of a document to refer,
* permanently and unambiguously, to another, with fast lookup. The most prolific example
* is that each line in a proof will need to refer to those lines on which it depends.
* We do not want to have to name such referents; we simply want to make an abstract
* kind of "pointer" to them, and to be able to do so simply in script, and to be able
* to dereference (follow) that pointer equally simply in script.
*
* <h1>Implementational Details</h1>
*
* All details are given here in the order that makes them most readable from start
* to finish. Note, however, that the most important routines for script authors to
* care about are reference() and referent(), and most of the others can be safely
* ignored most of the time (as described below).
*
* <dl>
* <dt>Lob::setIDContext()</dt>
* <dd>Public routine, which script authors can call a Lob L to declare that L
* is an ID "context." This means that L and its sublobs will work together
* to ensure that IDs are unique within L, by watching all modifications to L
* and reacting to them. Details given below; also see below for why you never
* need to call this routine if you're working on a document in a
* LurchEnvironment (i.e., the vast majority of the time).</dd>
* <dt>Lob::getNewID()</dt>
* <dd>Private routine, called internally by reference(), defined below.
* For any Lob L, <code>L.getNewID()</code> returns a new ID (i.e., one unused
* in the smallest context in which L sits) which could therefore be safely
* assigned to L. It follows this algorithm.
* <ol>
* <li>If L has an ID (as per Lob::getID()), return its value.
* In other words, if you don't need a new ID for L, don't bother getting
* one; use the one you already have.</li>
* <li>Search upwards through parents/containers of L until you find a Lob
* marked as a context. Ask that Lob for the highest ID used within it.
* Increment that value by one and use it. (Note that such values are
* cached, and the incremented value is also cached, to make this lookup
* efficient.)</li>
* <li>If the aforementioned search terminated in an OpenMath tree's root
* node that is not a context, so that no context is available, do the
* inefficient solution of traversing that entire tree and enumerating
* all IDs. Take a maximum and add one. Use that value.</li>
* </ol>
* Note that all computations of maximum/increment for IDs take place using the
* incrementID() and lessThanID() routines declard in lob.h and implemented in
* lob.cpp.
*
* Note also that this routine makes clear that contexts are for efficiency's
* sake only; for small to medium sized documents, you can ignore the notion of
* contexts altogether without suffering on efficiency.
* </dd>
* <dt>Lob::reference()</dt>
* <dd>Public routine, which script authors can call in L to get a new Lurch ID Reference
* object pointing to L. This calls getNewID() to construct the ID, then
* simply places it in a newly created Lurch ID Reference object. (To learn
* how such references are formatted, see Lob::isIDReference().)</dd>
* <dt>Lob::referent()</dt>
* <dd>Public routine, which script authors can call in a Lob L to dereference L
* (that is, follow L as a pointer/reference). If
* <code>L.isIDReference()</code> is false, this function returns an empty Lob,
* because you can't dereference a non-reference (follow a non-pointer). If L
* is an ID reference, then an expanding search throughout the OpenMath tree in
* which L sits begins; first L, then its attributes, then its children are
* searched, and if the ID was not found to label any of those, then we recur
* up one level to L's parent/container (except not ever searching back down
* into L again from there). This guarantees that the closest referent to the
* reference will be found, and the reference itself does not need to store any
* notion of a context in which to search.</dd>
* </dl>
*
* Because most Lurch scripting will take place in a document in a LurchEnvironment,
* the situation is really very simple for most script authors. LurchEnvironment
* calls <code>setIDContext(true)</code> on the current document when it is created or
* loaded, and the script author needn't bother doing so. He can simply call
* <code>L.reference()</code> to make a reference to L and <code>R.referent()</code>
* to follow such a reference back to the original Lob. The caching of IDs should
* guarantee efficiency.
*
* <h1>Even futher details</h1>
*
* There are some issues with making copies of subtrees which will then be inserted
* at another part of the same tree, because IDs would no longer be unique. This
* section discusses the gritty details of that issue.
*
* There is an optional boolean argument to Lob::copy(), called changeIDs, which
* defaults to true. When that value is left at its default, the copy() routine,
* after making a copy of the Lob in question, converts all the IDs in it and all
* references local to it. What does this mean?
* <ul>
* <li>By references "local" to the subtree I mean references that are in the subtree
* being copied and which refer to IDs that are also in that subtree.</li>
* <li>By "convert IDs and references" I mean it will use getNewID() repeatedly to
* obtain a new ID to replace each existing ID in the copied subtree, and it will
* systematically do a replace across the entire subtree, converting both IDs and
* local references to them consistently.</li>
* </ul>
* (Note that these details of copy() have not yet been implemented---coming soon!)
*
* The getNewID() calls will be done in the context of the original subtree that is
* being copied; this is most of the time what you want, so that you are able to
* re-insert the copy (perhaps slightly modified, perhaps not) into a different
* location in the same context without ID conflicts arising.
*
* If, however, you wish to insert it into another context, you will need to convert
* the IDs to be all new in that context. In this case, the copy() function's
* conversion is superfluous, and you may wish to skip it by passing false to copy(),
* and doing the conversion yourself into a new context with the routine
* Lob::changeIDs(), to which you pass the new context as a parameter. This issue
* will probably arise in the Lurch GUI when the user wishes to copy from one window
* and paste into another; this is the method for handling that situation.
*
* One last detail which suggests that setIDContext() is useful for avoiding headaches:
* If you are not using the setIDContext() approach, but just using
* the inefficient calculation of IDs on the fly,
* you must be aware of the following pitfall that comes from a lack of caching:
* \code
* // say L is a big Lob with M one of its subtrees
* Lob C = M.copy();
* // now C is a copy of M but with all ids different, and larger
* // than all IDs in L, so we could do L.addChild( C ) safely.
* Lob C2 = M.copy();
* // uh-oh, now what? does C2 know about C? no, so there is this danger:
* L.addChild( C ); // all still okay
* L.addChild( C2 ); // all not okay--conflicts between C and C2 inside L
* \endcode
* You can prevent this in one of three ways.
* <ol>
* <li>Call L.setIDContext() so that it caches the last maximum ID used, even
* if it hasn't yet been inserted back into L as a subtree, so that C2
* will indeed be different from C, with no potential conflicts.</li>
* <li>Call L.addChild( C ) before you call C2 = M.copy(); so that the latter
* of those two calls will spot all the IDs in C when computing the next
* free one for use in C2.</li>
* <li>Call C2 = M.copy( false ); and perform the conversion of IDs yourself,
* using C as a context. That is, do C2.changeIDs( C ) to ensure that
* C2 uses only IDs larger than all those in C. Note that the false
* parameter to the copy is optional in this case.</li>
* </ol>
*
* <h1>Testing</h1>
*
* All of the above is tested in test_ref::test_ids().
* Reading that test (or at least its documentation) may be informative.
*/