Reimplement variable name-gen operations in kernel with sync-vars

BIG refactor: mainly to allow stdknl to use SharingTables technology.

SharingTables implements hash-consing for types as they are written
out to disk. This can make a big difference to the theory file size,
and thus to theory-loading times.

The big visible change is that Theory, TheoryPP and Definition are no
longer really part of the kernel, and are found in src/postkernel
instead. They don't need to know about secret implementation details
in terms, types or theorems. They do need to have access to

Term.{write,read}_raw

and primitive definition principles (which are in Thm).

Another API change is that Tags no longer use user-visible string refs
to record use of axioms. Instead, the refs are hidden behind a new
Nonce type. This in turn means that the Tag.axioms_of function can
move to be visible to all users after the kernel. (If we kept the
axioms as string refs, users could alter the strings being pointed
to.)

Size functions for terms and types that count the size of the
respective trees. Have written these so many times that it seems
useful to have them in the kernel and available for all. (The
term_size function doesn't include the sizes of the attached types;
haven't ever felt the need for this.)

Rework a bunch of code in the two kernels so that they can share even
more stuff in src/prekernel. In particular, the latter is now home to
a special purpose symbol table that knows all about things being
up-to-date. Also move the final signatures for Terms and Types that
are what is ultimately presented to the user into prekernel so that
both kernels can use them.
In src/0 also move the signatures in Raw-sig into Type.sig and
Term.sig so that {Type,Term}.sml can be compiled in normal mode
against those signatures. I think this makes things a deal cleaner
there.
Finally, witnesses have entirely disappeared from src/0. If we
wanted to reinstate them for whatever reason, they could be stored in
a KernelSig.symbol_table along with arities and base types.

Constants are no longer considered out of date if their witnesses
become out of date. Thus, one might define
c = rhs
and save this definition with name "c_def". Subsequently, if
something in rhs becomes out-of-date, then c_def will be removed from
the theory. However, this change means that the constant c will
remain, as will any theorems mentioning it and not otherwise
out-of-date.

Next change in this area will be to attempt to share Sig or something
like it between both kernels.

Added some more information to error messages coming from
match_type and match_term. Now "double-bind" errors and
print out which variables get multiple bindings and
"unequal constant" errors get the named constants mentioned.
This can slow down searches for matches in a list, but
the improvement in functionality for dealing with large
terms seems worthwhile.

Provide a trace variable enabling users to turn off the complaints the kernel is wont to
make about type-variables with unusual names.

Minor changes to increase portability. In particular, added the Interrupt
exception to Portable instead of assuming that it is in General, and added type
annotations to resolve the types of non-expansive definitions that the smlnj
typechecker doesn't handle (Moscow ML is more flexible with respect to the
value restriction).

Allow multiple "ticks" before type variables, so that eqtype variables
can be lexically OK in HOL.

Minor changes, most having to do with the interfaces to matching. Needs
to be finalized.

Fixing performance bug for matching against big terms. Also, subst
has been improved to internally use a balanced binary tree representation
of substitutions. Also, substitutions that only involve variables are
more efficient since not every internal node in the tree is examined.

Not sure about what's different in Type.sml, but Term.sml has a fix
to an over-clever implementation of variant.

Fixed term matching so that the pattern (u,u) wouldn't match the term
(u,v).

Duh.

Revisions to type and term matching. Part code clean up and maybe some
bugs have been fixed too. The changes were prompted by Mike G. finding
some differences with some old code.

There is a difference with old code, namely that the matching algorithms
take sets of type variables and variables that are not allowed to be
instantiated in the course of matching. This serves as a cut-off for
some proof procedures. A scenario would be one where a match succeeded,
but subsequent instantiation failed because variables moved in the
resulting substitution were actually free on the assumption list of the
theorem being instantiated.

However, used by themselves, with non-empty "avoid" sets, one could spot
a difference between old and new versions of matching. I'd be interested
to see such examples.

Big terms can be constructed in finite time now. On my laptop,

list_mk_abs(1Mvars,list_mk_conj 1Mvars)

gets built in about 20 seconds. list_mk_forall and list_mk_exists are
twice as slow. If you are going to build terms with lots of
binding, please use these things in favour of

itlist (curry mk_forall) vlist tm

which 1) is slow because of the iterated mk_forall and 2) blows the stack
because of the itlist, at least in MoscowML, which allocates the call stack
on the stack.

Still to do: 1) upgrading this treatment to strip_abs, strip_forall, and
strip_exists; 2) upgrading it to paired abstractions; 3) efficienct versions
of SPECL and GENL (if possible); and 4) a rewriter that uses these facilities
to traverse deeply nested binders efficiently (this will (1) be a first
order rewriter and ... uh lost my train of thought).

There are some tests in src/0/big.term.tests. These should also be fleshed
out to have more strenuous tests, say ones with multiple parallel deeply
nested scopes.

... uh, the above 20 second claim is true if the list_mk_conj had
been done previously (I was mainly testing list_mk_abs).

The implementation uses Polyhash to represent the list of variables to
be bound, and utilizes continuation passing style to get tail recursion.
Otherwise, I couldn't get to 500K variables without blowing the stack.

minor additions and alterations.

Fairly radical changes: theorems' hypotheses now stored in a binary tree.

Minor changes.

Added an op_arity function to the Type signature. It's useful to know
how many arguments a type operator is expecting.

Minor alterations.

Fixed non-informative errrror messages for type formation, and added
Type.decls.

I moved nameStrm from Term to Lexis. More should be done to integrate
that with the renaming stuff already in Lexis.

I attempted to make variant be like in hol88 (the variable's name and
type are both used to compute whether renaming should happen), but that
broke a lot of proofs, so I went back to the hol90 variant (in
which only the name of the variable is used to decide if renaming is
necessary).

Updates to support functionality needed by Joe Hurd: genvars for type
variables.

Instituting paired syntax. Long live paired syntax!

Don't need the all target in the Holmakefile; various changes of
Konrad's. Addition of Type.gamma and Type.delta, and also the
ability to delete definitions.

New Kananaskis kernel.

Deletion of "dummy" type. No longer needed because of MN's new
type inference implementation.

Removed references (Link and Stv constructors) as type unification is now
done at the level of the TCPretype in the parse directory. This simplifies
the implementation considerably.

Fixed to bring it up to date with Taupo release 0.
(Changes have come across from parse_branch development.)

Initial revision