Remove "big records" optimisation

Improve TypeBase API for reporting on record fields

Datatype code now bypasses treatment of "big records". This stuff can
all be deleted and I will be happy to see it go as it is horrifically
complicated, and usually only serves to confuse users.

Thanks to a CakeML Slack discussion for the push to make the API
change.

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

Make record type definition less chatty

When proving and storing the various helper theorems, don't emit the
"saved theorem" messages to the user. (Interactively, the messages
don't appear; I don't think they need to appear when Holmake is running
either.)

Work on making record fupd fns more polymorphic

This is github issue #173.

Selftest checks for right behaviour. But an earlier test is failing
because the handling of "big records" hasn't been completely updated.

RecordType: use mk_thy_const instead of mk_const

Closes #260

Delete some unused code

Correct a minor indentation glitch

Ensure record type constructor names don't interfere with user names.

When you declare a type like

foo = <| n : num ; b : bool |>

there is an underlying constructor defined called foo:

foo : num -> bool -> foo

This underpins the definition of the various functions over record
types, which are made with the recursion principle for this underlying
algebraic type. However, with sufficient care/malice, this constant
(which users are typically oblivious to), can interfere with other
definitions to ill effect.

The fix is to make the constant take a name that can't even be
generated by the parser, but to then overload the name ("foo" in the
example) to this constant. The parser is happy to have a string
overload to multiple constants; the internal theory signature
mechanism has to prevent multiple constants from having the real name.
(Before the fix, the kernel signature maintenance lets the second
definition of a constant with this name go through but invalidates the
first constant, causing a theory to purge itself of what the user
thinks is a perfectly valid type.)

This solves one of the problems identified in github issue #224.

My change to the behaviour of GEN_TAC caused record proofs to break if
the record name began with the name of a constant. Fixed by making
RecordType's proofs more robust. Test-case also included.

Rename Lib.concat to Lib.strcat so that when Lib is opened (via HolKernel) in
an interactive session, the SML pervasive concat isn't shadowed.

The new changes to records have been fixed so that the system
will rebuild without error. Whether the record stuff actually
does what it should, I am still checking. The big record
stuff will have to be checked in Australia, probably, since
I don't really understand it.

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

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.

I think I've done records to death. This latest (and hopefully
last) improvement speeds things up for a forty field record from 44
seconds to 27 seconds. It does this by eliminating update functions.
Instead, all updates are implemented with functional updates. (The new
documentation in DESCRIPTION explains this.) There are thus many fewer
theorems proved and stored, and initialisation of the stateful rewriter
should be that much faster too.

Missed out some theorems that need exporting.

Prove and export more theorems needed to make big records work properly.
These are conceivably useful in a general setting too. For example:
fld1_fupd f o fld_fupd g = fld1_fupd (f o g)
where
fld1_fupd f : recd -> recd
updates field1 by applying f to it.

This theorem was being written out to be "adjoined" but wasn't being
added to the tyinfos generated at datatype definition time. This meant
that using a type in a loaded theory differed from using it in a
current theory. Now, neither loaded nor current theories include rewrites
to rewrite away functional update constants. These are important to keep
because the big record encoding uses functional updates.

(Shades of earlier discussion about problems in prob. directory!)
I realised that I need to prove both (f o g = g o f), and also
f o (g o h) = g o (f o h), where f and g are record update functions.

Export some new theorems as a result of record type definition. (Also
deleted a couple of exports that have been deadwood for a while.) This is
so that I can fix an exponential blow-up in part of my big record type
"solution" (one designed to fix an O(n^2) problem :-)

Changes to accommodate the efficient definition and manipulation of big
records. It's not a pretty picture underneath, but the pretty-printer is
called on to make everything look as if nothing has changed.

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.

Records now automatically prove one-one-ness result for literal syntax,
and this theorem is added as a simplification to the TypeBase.

Fix for bug when record fields involve option types (inducing a desire
in the code to have variables called "o"; which clashes with a constant
of the same name, which causes STRIP_TAC to pick other names for it,
breaking the tactics. Use of X_CHOOSE_THEN fixes that problem.

Automatically prove some more theorems about records. It would be nice
to replace the "standard" cases/nchotomy theorem with the literal_nchotomy
one but the code in Datatype makes it look as if this would be quite
an undertaking (to do persistently at least).

Change stemming from split of TypeBase into TypeBasePure and TypeBase.

Removed overloading on accessor functions so that field names are not
overloaded to them.

Modifications caused by change of TypeBase signature.

New work aimed at making a single global EVAL function, with
an underlying compset.

Upgraded to build under Kan. 0.

Made it all Kananaskis compatible. Datatype fails to load because of
something going wrong in loading pairTheory. This is BAD.

More bug fixes. Bug found by Steve Brackin who had the temerity to call
a record type "r1" (!). Internal proofs within the package were failing
because GEN_TAC has the temerity to rename generalised variables that
are the names of existing constants, causing later steps in the proof to
go astray.

Bug report from Steve Brackin, a record type whose name started with x
resulted in a type error when something was being parsed. Fixed this
and also got the indentation right.

The function allow_for_overloading_on has been completely removed from
the system. The overload code now uses anti-unification of types to
figure out the least generalisation of all the types that an overloaded
operator needs to represent.

Small changes.

Added definitions of functional updates to the simplification theorems
of a record type.

Updated to use Lib.gen_variant with tmvar_vary, which I prefer to the
loads-a-primes approach of the standard variant function.

Modified to cope with obscure bug. When creating the theorem to prove
for some of the theorems proved, this resulted in goals of the form
! X ... . <some term>
The letter X was chosen to be appropriate for the type. If the type's name
(chosen by the user) began with a capital K, then the letter chosen would be
K, the name of an existing constant. The tactic that attempted
to solve this goal came unstuck because the initial GEN_TAC resulted in
the bound variable X being renamed to X'. The tactic relied on the
name being correct, and failed as a result. But no more!

Changes due to the incorporation of John Harrison's datatype definition
package.
In particular, record type definition is now done elsewhere, code here
just takes a tyinfo and proves all of the extra theorems (including some
definitions) appropriate for a record type.

Fixed a bug when a record type had only one field.

Fairly wide-ranging modifications to make Hol_datatype take record type
definition quotations as well as normal types. The syntax supported is:
tyname = <| fld1 : ty1 ; fld2 : ty2 ; fld3 : ty3 ... |>
Not extensively tested.

Added proofs of two new useful theorems:
1. equality on records is equivalent to equality of fields, saved under
name rtype"_component_equality"
2. complete updates over any argument is equivalent to complete updates
over ARB, and hence to a "literal" record. Saved under the name
rtype"_updates_eq_literal"

Fixes in order to remove library file dependencies on global grammars.

Concrete syntax for records now very close to done. Thanks to Mark Staples
for suggesting that records with singleton updates could be done without
the brackets around the lists, thus: r with fld1 := 10.

Also proved the first of what will probably need to be a number of new
theorems giving fupd_ constants first class status (previously had
been rewriting them away).

Definition function changed to give constants names with the type as a
prefix of the name. Definition also sets up overloading for record
concrete syntax.

When a record type is defined the simplification functions for that type
in the TypeBase are extended to include the update canonicalisation functions
and a variety of other relevant theorems.

Modified to build on top of Datatype.Hol_datatype, thereby making sure that
records are properly recorded in the TypeBase.

Initial revision