Make theory-data format in .dat files slightly prettier

Loading performance is still terrible. Much of the blame for this is
probably in the Coding module, which is the next target.

Move smpp to Portable - get everything up to arithmeticScript working

Updated as far as Pretype.sml

Still no use of smpp tech.

Work towards use of PolyML.pretty type for most pretty-printing

Compiles up to src/parse under Poly/ML

Delete some unused code in TheoryPP

Complete basic Poly implementation of TheoryIO (separate dat files)

Still to tweak Holmake and to make sure it all works on Moscow ML

Use _Theory.dat for loading theory data into _Theory.sml

Provide fn for users to specify ML dependencies for theories

This will be useful when a theory wants to export a specific
pretty-printing or parsing function. For example, the special
printing of if-then-else is not properly exportable at the moment
because there is no way to capture it as a string in a theory file.

The ultimate intention is to give it a name in a special
dictionary, and to make the theory depend on ML code that implements
the function and inserts it into that dictionary under the user's
choice of name.

Allow users to have theorems called "print"

Closes #403

The solution works for print, but hasn't been generalised to cover all
possible problems of this form yet. A brief inspection suggests that
'print' *may* have been the only name not appropriately
protected. (Approach is to make sure that we use qualified names in ML
that appears after the user's theorems have been declared.)

Test-case included.

Unhide auxiliary TFL defns for nested recursions

These, with names including "_aux_" typically need to be visible so that
termination reasoning about the "pre-constant" can go ahead. Failing to
get this right caused the unification examples to fail.

Feed ThyData terms fn into thy file generation

This is necessary so that terms inside theory-data can fed into the
construction of SharingTables. This probably should have been part of
99597a19.

Untested because no existing ThyData types embed terms.

Give Theory Data writers access to term-writing

Just as readers get an additional parameter of type string -> term,
writers will get a parameter of type term -> string.

Give ThyData access to a term-reader function

No useful way to exploit this just yet, but the code compiles and I
think the refactoring is right.

Fix problem introduced by bceece8 in empty theory

Where an "empty theory" is one that doesn't export any theorems.

Fix Theory file name contamination bug

This was identified in aac90b5. There are a number of other names that
almost certainly need to be protected in similar ways.

Make user-provided SML come last in theory files

This is stuff added to theory files with adjoin_to_sml. Previously it
came before "theory data" manipulations.

Add detail to failure reporting on TheoryPP fail

In particular, catch exceptions raised in pp_thm (when theorems are
pretty-printed into xTheory.sig files), print the message and identify
the theorem that caused the problem.

There shouldn't ever be failures of this sort, but the information is
useful for developer-debugging.

WIP fixing problems with 57d38bd4

Allow users to export theorem names that are constructor names.

The hacky trick to allow this is to first use a fun binding to
"de-constructorify" the name. Thus

fun Empty x = x
val Empty = 3

allows you to bind Empty, despite it being an exception name, and thus
a constructor name.

There are still names that just won't work: Poly/ML (at least) doesn't
allow rebinding of ::, true, false, ref and nil. We should probably
immediately raise an error with those cases on an attempt to save.

Closes #225

Remove debugging cruft from work on fixing issue #115.

Extend kernel API with new all_atoms entrypoint.

Use this in theory pretty-printing routine to deal with issue #115.

Closes #115.

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.)