Move smpp to Portable - get everything up to arithmeticScript working

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

Compiles up to src/parse under Poly/ML

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.

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.

Stop temp consts from being added to grammar

This means that they can't be named directly, and can only be accessed
with the $ notation.

Also make the "_tupled" constants used internally by tfl be temporary
constants of this form so they don't get added either.

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.

Make theory data types provide terms function

This function takes a value of the theory-data type and returns a list
of terms that are contained inside this value. The machinery will use
that to prime the theory's sharing tables to allow for efficient
recording of terms in data.

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.

Add Theory.quote_adjoin_to_theory. Use this in llistTheory.

This should close #304.

This has been implemented using a new function Portable.quote_to_string_list. Other uses of adjoin_to_theory under src/ have been updated.

code style: space after parenthesis in "(x*y)list"

extra semicolons removed from (some) .sig files

WIP fixing problems with 57d38bd4

Add gen_new_specification and remove prim_constant_definition

Implement new_definition in terms of gen_prim_specification.
Leave the existing new_specification in place.
This plan of attack suggested by RDA.

Have only touched the standard kernel, and none of the theories.
Next steps would include updating the other kernels, implementing
new_specification in terms of gen_new_specification (at some point after
pairTheory), and removing uses of new_specification before pairTheory
one by one if possible/desired...

Revert "start experimental implementation of revised new_specification"

This reverts commits 7f58ad8, eae01bc, and c07a105.

remove Theory.new_specification and reimplement new_definition

in terms of the revised Thm.prim_specification. obviously this breaks
anything that depended on Theory.new_specification, so the next job is
to rework those things (and write a backwards-compatible version, but
later in the build sequence because it needs pairs.)

start experimental implementation of revised new_specification

Based on Rob Arthan's "HOL Constant Definition Done Right". The tricky
part is deciding how and where to implement the existing definitional
rules that are theoretically subsumed by the new one.

Allow thy-data to be set to a value as well as merged with what's there.

More theory signature events now reported to hooks.

In particular, {new,remove}{typeOp,constant} events are reported.

Use this to do away with some of the cruftiness in boolLib whereby the
entry-points there had to mask the primitive principles in order to
update the grammar. Now the parser installs hooks to watch for things
being deleted or added and adjusts the grammar as it goes.

The disadvantage is that it's impossible to bypass these changes to
the grammar.

Rework various Theory hooks into one general framework.

The basis for the framework is the TheoryDelta type. Client code can
ask to be notified of theory changes, and will have their provided
call-back function called at appropriate times.

This commit hasn't adjusted the theory functions for
{add,del}{const/typeOp} yet; it has just unified the existing
functionality (register_onload, after_new_theory and
register_onexport).

Add onexport hooks to Theory

You can register a function to be called whenever export_theory is
called subsequently, for example for a library to do some cleanup before
a theory using that library is exported.

Moved prekernel/FinalTheory-sig.sml to be postkernel/Theory.sig.

This simplifies the core a little.

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