Improve efficiency of encoding of theorem classes in .dat files

Throw more exceptions when SharingTables lookups go wrong

Get latest changes to build under Moscow ML

Simplify grammar handling by using abstract ancestral data framework

This is not fully worked out yet, and the abstract framework has only
been instantiated on the one test-case. It's definitely worth it
there though as there can be less awful code smashed into
fooTheory.sml files as a result. Aim is to instantiate theorem-sets
in the same way though so that it will be possible to access srw_ss()
as it was at different points in the theory hierarchy.

Not yet clear if AncestryData should be responsible for holding onto
the underlying references that hold the global "values" (grammars,
simpsets, etc).

Changes in examples fix various adjoin calls that either shouldn't be
there at all (TypeBase now has export; or need to be made "after
completion" so that parses work correctly (these should be using
exportable data themselves)).

Allow users' theory data to share/hash embedded strings

Make stored theory data HOLsexp's rather than strings

It's easy enough to cope with old code because strings can be injected
into sexps trivially. The richer ThyDataSexp type has been updated to
use a nicer encoder though, and clients that use that API are unchanged.

Use "string-hashing" for theory names occuring in thm dep info

Complete refactoring of Sharing code

There's now an API for exporting theorems, terms and types to
s-expressions that should be generally useful (not just in the theory
data management setting).

Start to refactor Sharing code

Change theory files to use an s-expression representation

This wastes some disk-space in the form of extra white-space that the
Oppen pretty-printer introduces for indentation purposes, but with the
string table used, the number of lines and the number of
non-whitespace characters is lower.

The string table can and will be used in more places in subsequent
commits to try to improve file size and sharing. The theory data may
also shift to directly use s-expressions rather than strings (people
wedded to a string representation can always embed those into
s-expressions of course).

Optimise theory dat space a bit

- use a slightly more compact term representation that saves a bit of
space when binary or unary applications happen
- build a table of strings to reuse at the top of theory files

The strings table still needs to be used in a bunch more places
throughout Theory.dat files.

Ensure holpath "macros" are used for files in same dir as .holpath

Issue was that substitution was only attempted against directory name
without the trailing space. Fix is to substitute against directory
name path-concatenated with filename (fooTheory.dat in this case).

With regression test (in Holmakefile, assuming grep).

Closes #665

Make reading of Theory.dat files quicker

Measuring with the time function indicates much less GC, resulting in
load times that are 2 to 3 times faster.

Grammar and lexical format of dat files is now also more explicit.
It'd be interesting to see if using mlyacc would speed things up at
all.

Closes #507

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