We may actually want to remove this in future once things stabilise and there
are certain nodes that do not need it. For now though, it seems more flexible to
just make it available to all nodes.

It didn't previously occur to me that these need to be wrapped too.

We'll need to toggle this when we have support for local variables.

It would be nice to get to a point where the checker builds with -W -Wall
-Wextra in the presence of all sane models.

This might seem like a bit of an odd direction to go in. However, I've realised
the advantages we get from C++ in the checker are actually not especially
significant. The main strengths in code like this are being able to write static
code ahead of time using templates and then instantiate it during generation.
However, we need to emit custom classes for almost everything non-trivial (e.g.
records).

None of the data structures we need are especially complex, except the state set
and queue which I think we're best outsourcing. My hypothesis is that this
combination (C source + GLib) can beat a C++ solution, in terms of runtime and
memory usage. I don't know whether this will pan out, but interesting to try.

One notable thing we lost in this change was exception support. Exceptions were
shaping up to be quite an elegant mechanism for reporting a checker failure.
However, my long term plan was always to remove them (or at least make them
optional) to allow better interoperability with other languages. I think we
should probably still be able to come up with a performance, thread-safe
solution.

This is essentially the complete algorithm. We now simply need to implement the
generation of rule bodies.

Note that we convert some state values to pointers in this change. I think this
will be necessary once we start tracking previous pointers.

The checker is now buildable, though it doesn't do anything.

It constantly irritates me (and presumably other C/C++ programmers) that '==' is
not the comparison operator. There's no ambiguity in introducing it, so let's
just accept it as an alias for '='.

Accidental result of refactoring.

Well that was unexpected.

This works, but it makes me slightly nervous that the Var of a quantified
variable is only sustained by shared_ptrs of ExprIDs related to where it is
referenced. I.e. Once we traverse out of parsing the forall expression, the
enclosing scope is closed and the Var is destroyed if it hasn't been referenced.
On the one hand, this seems fine and might even help us later in detecting
useless quantification. On the other hand, the lifetime of this Var object is
quite slippery.

Well that was a rude surprise. VarDecl lookups in the symbol table failed
mysteriously and debugging indicated they had no name. Some digging revealed we
were accidentally shadowing Decl::name.

It is pretty surprising to me that -Wall -Wextra does not enable -Wshadow, which
would have caught this. Unfortunately we can't turn it on right now because it
sprays warnings about the constructors that shadow class members with their
arguments. Sigh. I guess I'll have to refactor this before turning it on.

This expression is used for referring to variables (either parts of the state or
local variables). I'm still not sure this is the natural solution. It feels like
this and ExprID should be a single class, but we'll see how it goes.

Note that you can't currently reference the quantified variables within the
forall expression as explained in the FIXME comment.

This allows us to drop all the destructors and simply let reference counting do
its job. I don't think we should take this approach in the checker because
shared_ptrs aren't free, but the generator is not performance critical. Note
we retain a raw pointer for ExprID::type_of. It's difficult to avoid this
without introducing circular references or memory leaks. I think it's fine for
now.