Non-commutativity in quanto

[Aleks Kissinger]

I've been thinking about implementing non-commutativity in quanto, and
I thought I would get you all (esp Alex) to weigh in on some design
decisions before I make them.

Non-commutative nodes are implemented via a new (theory-independent)
piece of data attached to !-graphs called a neighbourhood. Nhds are
attached to nodes, and are optional. Any node without a nhd is assumed
to be commutative, so all of the existing theories/graphs/rules in
quanto should keep behaving just as they have been.

A nhd is an edgeterm, which is a list of edge names, annotated with
information about which !-boxes they connect two, and which direction
they should expand when those boxes are expanded. For example:
"(B:<c(A:[ab>)de])f" is a list of 6 edges, where a and b are in a bbox
A that expands to the right and c, d, e, and the nested bbox A are in
a bbox B that expands to the left.

When bboxes are expanded, copies, dropped, or killed, the
corresponding function to called on all the adjacent nhds, so a graph
that starts with valid nhds will keep valid nhds after some bbox
operations. So, non-commutative matching should just be a matter of
adding the appropriate hooks to ProgressiveMatchSearch to die on bad
(partial) nhd matches. The other alternative is to get the matcher to
only choose the next edge to match if it is going to be induce a valid
nhd matching. So, my first question:

* Given how hooks are set up, is one of these better/simpler?

The biggest question mark is over !-graph construction functions.
Probably a big contributing factor in quantomatic actually *working*
these days is we've spent the last year or two making !-graphs
"correct by construction". If you build a graph using the functions
the BANG_GRAPH signature, it is either correct, or something will
throw an exception. Adding nhds introduces a new constraint to
validity, namely that neighbourhood data is consistent with the actual
edges and bboxes the vertex is connected to. See "check_vertex_nhd"
here:

https://github.com/Quantomatic/quantomatic/commit/87ad7

Here's the policy I propose:

1. The only way nhds are added to vertices via "set_vertex_nhd", which
in turn calls "check_vertex_nhd"
2. Nhds are removed by "clear_vertex_nhd"
3. Edges can only be added/removed to vertices with no nhd
4. Vertices can only be added/removed from bboxes if they, and all of
their adjacent vertices, have no nhd
5. Graphs can only be merged if common node-vertices have *identical*
neighbourhoods (or have no nhds in *both* graphs).

Points 3 and 4 may seem a bit extreme. It essentially means that
before editing edges/bboxes, one must clear the nhds of all of the
vertices involved, then re-add them afterwards. However, bearing in
mind that by far the most common ways graphs are built are by loading
JSON (in which case nhds can be added last) and by merging in the RHS
of a rewrite rule, this seems to not create much overhead. So, second
question:

* Is this reasonable? Did I forget anything?