Get src/datatype to build given tight equality

Fix bug in handling of distinctness for large enumerated types

Previous attempt at regression test for this didn't capture scenario
where srw_ss() had already been initialised and correctness relied on
TypeBase hook telling BasicProvers about newly arriving tyinfo.

Performance is still bad when theories dump large tyinfos to disk.

Re-implement Datatype package with TypeBase sexps (not adjoin)

Rename TypeBase entrypoints for caseeqsplit and friends

Now use case_eq everywhere.

Work on github issue #345

Automatically prove "case-eqsplit" theorems and store in TypeBase

For :num, this theorem looks like

(num_CASE n zc sc = v) <=>
(n = 0) ∧ (zc = v) ∨ ∃x. (n = SUC x) ∧ (sc x = v)

Such theorems can be powerful rewrites when (large) case-expressions
are asserted to be equal to some value or other.

These theorems have to be installed somewhat by hand for early types,
but from list onwards, the Datatype package handles this. This work
leverages earlier work done implementing prove_case_eq_thm (8f16922426).

Take the opportunity to rework TypeBasePure's code to use
FunctionalRecordUpdate.

This is progress with github issue #345.

Support for simplifying and evaluating enumerated type representation/abstraction maps.

For example, given

Datatype `enum = one | two`;

the following now works

> EVAL ``num2enum 1``;
val it = |- num2enum 1 = two: thm
> EVAL ``enum2num two``;
val it = |- enum2num two = 1: thm

> SIMP_CONV (srw_ss()) [] ``enum2num two``;
val it = |- enum2num two = 1: thm
> SIMP_CONV (srw_ss()) [] ``num2enum 1``;
val it = |- num2enum 1 = two: thm

This also works when building custom compsets using computeLib. add_datatype_info.

NOTE: This change may break some proofs (some in example/ARM have been fixed).

WIP fixing problems with 57d38bd4

Clean up code that relies on constant and theorem names for case constants.

Rather than code having to know that the constant is called
“type_CASE” and that its definition is stored in “type_case_def”, use
ML entrypoints in Prim_rec to abstract these details.

This is progress with github issue #97.

Enumerated types were getting the wrong names for their case constants.

This is progress with github issue #97.

Fix generation of case constants for enumerated types.

This is progress with github issue #97.

Don't emit definition bindings for enumerated constants.

Fixes #78.

This commit also

* fixes uses of constructor definitions (the equations are still
present under the "number2<ty>_thm" name)
* provides a regression test
* a bug fix claim in the release notes.

Addition of destructors and recognizers for datatypes.
So far, I've just got basic support put in.

Some other trivial mods as well.

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

Fixes to support code generation for records. Incomplete! So
do not update these changes (I'm just using CVS to transfer
files to work machine).

Changed the TypeBase to be indexed by types. Originally it was
indexed by a single string (representing the type operator), then
Michael changed it to a pair of strings (precise representation
of the type operator). The latest change allows non-datatypes to
be added to the TypeBase. This will allow case analysis and
termination proofs to be supported for non-datatypes.

I reckon there are still a few bugs left after the massive
revision, so you might want to wait a while before upgrading.

Follow-on fixes to changing Term to Parse.Term and Type to Parse.Type
in the quotation pre-processor. A mass of trivial changes, but the
new way of dealing with files containing code that does parsing
(not script files) is to

* grab the ambient grammar(s)
* set the current grammar(s) to the right values
for parsing quotations in the file
* the body of the file
* reset the current grammar to the ambient grammar

For an example, see src/taut/tautLib.sml

A load of changes aimed at supporting records better. And some other
odds and ends.

Adding in support for encoding in the TypeBase.

An efficiency improvement for enumerated types. Here's a little table
giving times taken (in seconds) to define an enumerated type of 50
elements:

dB indices Name-carrying terms
old code 5.5 15.1
new code 4.0 3.9

I don't know why the old code and name-carrying terms interacted so badly,
but will look into this as it may point to a problem in the experimental
kernel.

For what it's worth, the performance graphs for the three good performances
are all linear-looking (for sz = 1..50), but the gradient on the line
for old code is slightly worse than that for the new code.

Modify TypeBases so that they can store conversions as well as theorems
in a tyinfo's "simpls_of" slot. This is then used to implement a conversion
for enumerated type equalities. Previously, we just used a rewrite
directly, which meant that something of the form (x = C10) might turn
into the rather ugly (foo_to_num x = 11). Now, the rewrite is only
applied to equalities between constants.
Some comments in the .sig files in Datatype, RecordType and EnumType
hopefully also make it clearer what the weird string results are
doing, and how they get added into theory files.

At Anthony's suggestion, altered treatment of enumerated type package to
emit one theorem (called <rep>_thm) of form
(rep C1 = 0) /\ (rep C2 = 1) /\ ... (rep Cn = n - 1)
rather than n individual theorems (with names <rep>_Ci) of form
rep Ci = i - 1
Also add <abs>_thm of form
(abs 0 = C1) /\ (abs 1 = C2) /\ ... (abs (n - 1) = Cn)

Change to type of new_specification, and made it tell that parser about
the introduced constants. Lots of knock-on (trivial) mods.

Moved the code to automatically generate "boolify" functions for datatypes
from src/datatype/Datatype.sml to src/Boolify/src/Boolify.sml.

It uses the register_update_function hook to add the boolification
info (more on that later).

Also added a test suite for boolification.

Added boolification functions for enumerated types, and added a
datatype with a single nullary constructor to the test suite to
stop a recent bug from reappearing.

Fixed problem with single-constructor datatypes.

First steps in adding boolification for datatypes. Shouldn't
interfere with others' work.

Change stemming from split of TypeBase into TypeBasePure and TypeBase.

Slight reworking to make sure that additional simplification theorems
created by the enumerated types package are saved properly (i.e., correctly
adjoined to the current theory file).

Code for case_cong_thm moved to Prim_rec.

Minor, and hopefully final, corrections to get case_cong_thm to work
now that the form of the case definition theorem has changed.

Fixing define_case to have the definition be all -- postprocessing
seemed to confuse TypeBase instructions left in Theory files.

More changes, to fix the final shape of the case definition.

Minor fix.

Improvements in speed for define_case and case_cong_thm.

Changes to make case constant definition faster in EnumType.

Now prove case congruence theorem as well as all the rest.

Efficient definition of enumerated types.