Make type-checking handle antiquotes more efficiently

Previously, all antiquoted terms were converted back into preterms
before the machinery in Preterm ever saw them. Now, these terms get to
stay as terms. They are still scanned so that their free variables can
influence those in any surrounding term. This also preserves the way in
which something like

val t = mk_conj(``x:bool``, ``f x:bool``);
``^t``;

raises an exception.

Add record-upd function to Parse_support env type

Make progress with functional pretype

The change to pretty-printing raises an exception, but parsing simple
cases seems to work.

Begin to make pretypes purely functional

I want to do without the references that are used in the unification
algorithm.

Allow for user "preterm processors"

These are inserted into the process where the abstract syntax gets
turned into preterms, and can call back to the builtin processor if
necessary.

Something like this is necessary if you are going to mess with binding
structure and need to do so in a way that is itself aware of what the
context's free variables are. This technology is needed for
pattern-matching, and should allow us to move the handling of
set-comprehension out of src/parse as well.