Again allow ancestral data to consume deltas all at once on theory-load

This allows named simpset-fragments to be added to srw_ss. This then
allows those fragments to be easily removed with calls to
diminish_srw_ss. In the 'fix-ancestry' rework this ability was
removed but this did break proofs when diminish_srw_ss calls had no
effect.

Selftest in coretypes demonstrates this with removal of the "one"
fragment.

Fixes to make sure that uptodate checks work properly

Existing regression tests now pass

Present IndDefLib's rule-induction-map as a theorem-set with ancestry

Only required change to the underlying API is to acknowledge that a
call to merge may result in no value if none of the desired parents
have a value either.

Add export_with_ancestry to ThmSetData signature

It compiles but is completely untested

Improve efficiency of encoding of lists of thm names in ThmSetData

Make grammar-deltas s-expressions when stored in theory .dat files

This makes them more legible, and is also a prelude to being more
uniform in the treatment of theory data that merges deltas across
ancestors.

Tweak ThmSetData API: take callbacks with more honest types

In particular, the callbacks are always only ever called on singleton
lists, so it seems silly to ask the user for functions with types that
have lists.

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

Change "thm-names" (used in various places) to be Thy-Name record

This saves on pulling things apart and looking for dots and the like.
It changes the simpLib API (most significantly for the SSFRAG function
which builds simpset fragments).

Allow users' theory data to share/hash embedded strings

Allow theorems to be stored "locally", with local attributes

Such theorems are not stored in the exported theory, but do
temporarily affect the global contexts that their attributes point at.

The test-case illustrates this, with a local simp not visible in the
later theory.

Change ThmSetData to store just theorem names in .dat files

The recent changes to this file caused theorem values to also be
stored; this is unnecessary (the references must be to existing
theorems), and wastes space in the .dat file, and presumably in what's
loaded.

I'm unsure as to why the stored name changed in the simpset
machinery (requiring a change to delsimps1Script.sml), but I'm going
to change the way simpset modification happens anyway.

Be more careful over handling of ThmSetData and rebinding of thm names

In particular, it was previously possible to do

val thm = store_thm("thm[some_attribute]", tm1, tac2);
val thm = store_thm("thm", tm2, tac2);

and have the second thm be exported but to pick up the attribute from
the first call. This is clearly outrageous, so now the attribute is
lost when the second theorem is slotted into the theory.

Working through all this found three places where this
double-definition pattern was happening (there may yet be more). In
src/finite_map and src/list the second theorem was clearly just
redundant and could be deleted.

The example in fun-op-sem is slightly more interesting: there it
defines a function (which definition gives that function a "compute"
attribute), and then restates the definition, saving it under the same
name ("foo_def"). Though arguably bad style, it's important that the
second theorem replace the first, and that it should have the
"compute" attribute. Here the change is to explicitly add that
attribute to the second theorem.

Finally, all this work revealed that Theory.sml's handling of the
NewBinding theory-delta hook was wrong and caused changes to be
dropped after the hook function was called. Debugging *that* led me to
add a pp field to the LoadableThyData registration process so that
theory-data values could be inspected more easily. There is also a
trace variable to turn on some debugging output in Theory.

Rework ThmSetData implementation to use Theory s-expressions

This makes the encoding more robust, particularly if set "removal
instructions" might include space characters.

Refactor handling of thm attributes ("simp", etc) into new module

A slight backwards incompatibility is that this removes the ability
for script files to declare new attributes (hence removal of
attr[12]Script.sml from src/1/theory_tests). This facility is used
vacuously in CakeML once.

Rework persistent ThmSetData API to allow for "removal" of elements

The removals are strings encoding removal "instructions", which are up
to the underlying consumer to interpret. Still to test any of this
new machinery, but the old behaviours have been preserved.

Move smpp to Portable - get everything up to arithmeticScript working

Up to and boolTheory and slightly beyond

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.

ThmSetData passes thms *and* names to consumers

The names were always available, but the API now changes so that
consumers get names as well as theorem values. They can ignore the
names of course. (In this context, consumers are things like the
stateful rewriter, the monotonicity rule database, the TFL congruence
rule database etc.)

This will be helpful in allowing the stateful simpset to know what its
theorems are called, which is progress with Github issue #313 (to allow
easy removal of rewrites from a call to the simplifier).

Bug fix (w/test case) for ThmSetData's new way to add theorems

Problem was that the callback function attached to the set didn't get
called, even though the theorem was successfully exported. This meant
that a set like "simp" (which feeds into srw_ss()) didn't prompt any
change to the stateful simpset. Being successfully exported did at
least mean that the theorem would get into the simpset in descendent
theories.

Test for ThmSetData bug fixed in 8ffc5dc0b; prettify adjoined SML output

Fix bug in SML emitted/adjoined by new_storage_attribute.

Implement new scheme to allow simple addition of theorems to theorem "sets".

When saving or storing theorems, simply add [name1,name2] strings to the
end of the binding, and the theorem being saved will be added to the
theorem set with that name.

Make ThmSetData handle empty/null data as input.

Closes #130

Get better diagnostic messages out of ThmSetData warnings.

Use hook for binding-deletion to make ThmSetData more robust.

Test-case also uses WARNINGs_as_ERRs to check that nothing untoward
gets warned about in the second theory (the one that imports the
theory which has had lots of delete_{const,binding} events).

Adjust (and reduce) interface to ThmSetData.

The change is to add an extra string parameter to the callback
function that the client provides. This is the name of the theory
which has stored the theorems. This change prompted the changes to
computeLib, IndDefLib and DefnBase.

The reduction was to remove the ThmSetData's new function, forcing
BasicProvers to use new_exporter. This was possible because of the
extra information provided to its call-back.

I also wrote some test-cases mimicking the original problem that
Magnus and Ramana had, and prettied the warning output.

This closes #73.

Get stored ThmSets to notice deletion of relevant consts.

This is progress with #73.

Provide lookup functionality across all stored theorem sets.

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

Make theorem-set loading more robust in face of bad thm-names.

Most attempts to mess with the data will be caught at specification
time, but use of delete_const and friends can cause theorems to not
get exported even if they were present when the call to export_X was
made.

Delete some unused code in ThmSetData.sml

Change src/bool to src/1 as a prelude to experimentation!