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

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.

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.

Handle a dictionary lookup failure with a HOL_ERR

I.e., provide better runtime documentation of possible invariant
failures.

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.

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.

Improve feedback for Holmake.

Theorems proved with `fast_proof` are now regarded as cheated. The use of other oracle theorems is identified, though not marked as cheating.

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.

Add NewBinding as new form of TheoryDelta event

This happens whenever a theory segment is extended with a new fact.

Identify saved theorems that are tainted by the cheat tactic.

Ensure HOL4 works with fixed-width integers under Poly/ML.

Integers under Poly/ML 5.6.1 are likely to be fixed-width by default (up until now they've always been arbitrary precision). Some changes were needed to cope with this:

- The Arbint and Artbnum structures effectively assumed Int.int = IntInf.int.
- The Standard ML structure Time is based on LargeInt.int and not Int.int. Code for printing times has been re-implemented using the Date structure.
- The smart-configure.sml file used the Overflow exception to distinguish between Moscow ML and Poly/ML. This test is now based on a difference in the printing of General.Fail exceptions.

Make new_definition_hook replace a constant on the LHS by a variable

new_definition calls gen_prim_specification which requires an equation
whose left-hand side is a variable, but sometimes (maybe only in obscure
old example script files) users pass an equation with a constant on the
left. The same hook that abstracts arguments now turns a constant on the
left into a variable.

holyhammer 1.0

Prevent bad constant names at Definition level

Enforces a constraint I'd long assumed to be true.

Closes #268

WIP fixing problems with 57d38bd4

Make save_thm etc reject names that will cause uncompilable theory files

This causes exceptions/errors earlier rather than later.

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.

replace calls to new_specification in boolScript.sml

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.

Document new_type_definition's errors better; improve its error-reporting

Closes #128

Make binding-deletion a TheoryDelta so clients can "see" them.

Recall that a binding is a link between a theorem name and a theorem
value.

Revert "export hook" behaviour to the way it was before bb9eb667e2.

In particular, the client code runs before any kernel code is run. My
change thoughtlessly had the client code run after the theory was
"scrubbed" to remove it of out-of-date theorems. But Magnus's use of
the export hook in ml_translatorLib called delete_const resulting in a
bad theory export.

The boss/theory_tests change mimicks that problem in miniature.

This is fallout from issue #73.

Minor code cleanup in Theory.sml's handling of theory data.

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

Give better error when client tries to reuse a theory data key

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

remove unnecessary call to CTname in Theory.sml

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.

trivial edit

Attempt to tidy-up HOL's output in non-interactive mode - mostly through lining
up definition and theorem names.

Magnus wanted times in hours for his sloooow theories.

Move kernelid variable to Thm so that it isn't shared across kernels.

Thanks to Anthony for spotting the problem.

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