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.

Promote more functions from Isabelle Library into Portable

- enclose l r mid is "just" an application of string concatenation,
but is useful when partially applied to two arguments
- filter_out is filter with the sense of the predicate flipped
- ? provides a compact way of writing "if b then f x else x"

Finally, move fold_product from Library to Graph, where it is used.
This library function is effectively a fold over a cross product of
two lists + an accumulator. It's nice not to have to compute the
cross product explicitly, but it's a bit too exotic for me. I grepped
for uses of it in the Isabelle sources, and even there it's used only
6 times.

Change big_record_size to be 100 by default

As discussed on the hol-info mailing list and in person on numerous
occasions, this technology is frequently extremely confusing. Users
should probably get around this problem themselves by defining
hierarchies of sub-records themselves.

A limit of 100 is not likely to be a practical issue in the near
future as records of this size will take painfully long to be defined,
and users will follow the manual's new advice to define
sub-records. (Just tested this: 10 fields: 0.08s; 20 fields: 1.0s; 30
fields: 6.2s; 50 fields: 89s.)

Generate "standard" datatype simpl rewrites as tyinfos are loaded

This saves us from having to write them out to disk, which can make
for unnecessarily large theory.dat files.

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

Fix mishandling of record types

Builds core HOL; quotient fails for lack of (temporary) html_theory

Rename TypeBase entrypoints for caseeqsplit and friends

Now use case_eq everywhere.

Work on github issue #345

Refine type variables printed by EmitTeX in record declarations

Now those appearing in the record type on the LHS (e.g., ('a,'c) foo),
and the fields in the type actually match up. Adjusted test-cases to
match. Pleasantly, the existing behaviour of prim_mk_const and the
datatype machinery preserves the type variables as the user gave them.

Fix TeX p/printing bug caused by having multiple types of same name

If the types had different arities, mungers would produce strange
mk_type exceptions.

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.

Properly enable case-expr p/printing overloads

This had been made the responsibility of the process that stored
TypeBase information, but that didn't interact properly with the
user-delta approach to storing grammar changes. Now the persistent
overloads are emitted separately.

Fix ParseDatatype to handle recursive redefinitions

Fix proof of "bigrec" thms for polymorphic records

These are the theorems that are proved to knit together the view of the
record that the user expects and the underlying reality, which is a
record of records. These are stated and proved after the various
underlying record types are defined.

Tests in src/datatype/selftest.sml

This is work on github issue #173

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.

Datatype: qual-ids stop creation of recursive type

Closes #257

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.

Implement most of a new Datatype function with nicer syntax.

(Pair-programming with Magnus who wanted it.) Still need to
implement change to EmitTeX.

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.

Allow "non-datatypes" in TypeBase to have optional induction thm.

Provide appropriate values for this field for finite sets, strings,
integers, finite maps and words.

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

Some other trivial mods as well.

Cleaned up signature Datatype.sig. Added entrypoint
to call Hol_datatype on ParseDatatype.AST list input.

(Fix for) Bug in polymorphic record types with nested recursion.

Bug reported by Ramana Kumar.

Fix a bug reported by Anthony whereby theories exported with Unicode
on couldn't be loaded with Unicode off. Also set up a new trace that
allows generation of annotations for PPBackEnd to be turned off.
Having it off, which is its state when not running interactively,
speeds up the pretty-printing done to the Theory.sig file when a
theory is exported.

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!

Implement ML code generation for large records.

End of the *v saga. I found the spot in Pmatch.sml
that was failing to collect all the free vars
that needed to be renamed away from.

Misc. other tidying, including an incomplete
attempt at getting datatype constructors to
be defined in terms of numerals rather
than successors.

Fix for a Define bug spotted by mjcg. When
dealing with recursive calls under a case,
if variables with certain names (those
starting with v) are bound in the case
pattern then it can happen that variables
generated during pattern matching can be
the same, leading to failed proofs. Totally
obscure, and dealt with properly (I think)
in normal pattern matching. So, a difference
between Pmatch and Functional. The fix is
to invent a class of variables not accepted
by the parser (i.e. starting *v) and to later eliminate
the weird names from any theorems coming out of Hol_defn.

Some other trivial mods made in passing also, plus
tests for the new behaviour.

Also a new conversional, MAP_THM, which applies the
given conversion to the assumptions and conclusion
of the given theorem.

Liberate an AST interface to datatype declarations.

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

Minor efficiency improvement.

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.

Wide-ranging change to make the TypeBase export an interface forcing users
to be concerned about which theory their types are from. Interactive users
of the "induction_of", "axiom_of" and similar functions are thrown the only
bone: they can effectively omit the theory parameter by using "" instead
of a theory name.
Prompted by a bug found by Tom Ridge where it was impossible to define
a pattern matching function on a type with the same name as another type
because the pattern-matching code was using dest_type and TypeBase.read
on just the type-operator name.

Ensure that terms and types are printed out in fully-qualified form when
they appear in theory files (from Datatype anyway). This should solve
a just-discovered bug where the ctl and path theories are incompatible.

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.

Preparatory changes for ML execution.

A slight extension to the way big records are handled, designed to give
users more control, and to also make the default behaviour more reluctant
to use big records (they can induce serious confusion if you're not
expecting them).

Preliminary addition of support for ML execution.

Adding in support for encoding in the TypeBase.

Detect and report situation where a new type is declared with constructors
that overlap with those of an existing type of a different name.

Got rid of QConv, and made all conversions do the "raise exception to
indicate reflexivity" thing. (Also fixed bug in new implementation
of ABS_CONV that attempted renaming on failure of conv, and not just
failure of ABS.)

Next step will be to rework the simplifier's implementation so that
it also uses Conv.UNCHANGED, rather than in its own internal version
of the same. This will let the simplifier play efficiently with
others.

May also assess making ABS_CONV not do renaming, and give the rewriter
its own special traverser. This might make some things more efficient.

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.

More efficiency gains for this code. Defines a 40-field record in about
45 seconds on my lap-top.

Efficiency improvement for these proofs.

Generate theorems for big record types that look the way the user expects,
and don't involve ugly references to fields including the string "brss".

A new (more efficient) scheme for representing big records.
Update functions are
fld1_update v r = subfld_fupd (leaffld1_update v) r
rather than
fld1_update v r = subfld_update (leaffd1_update v (subfld r)) r
The two occurrences of r on that RHS led to exponential behaviour
when writing away occurrences of fld_update functions and doing
subsequent simplifications.

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.

This change is a necessary prelude to my scheme for making big records
more efficient, but is useful in its own right. I do a topological
sort of the reference graph of the requested datatypes to split the
input up, and then make the definitions in phases. Stuff like
Hol_datatype `foo = C1 of num | C2 of bool ;
bar = D1 of num => foo ; D2 of bool`
(or even the same with the two lines reversed in order) will now work
the way they ought to (currently, the system thinks this is some sort
of mutually recursive type).

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.

Made parse errors automatically write messages to stdout rather than
just raise an exception. This is consistent with the behaviour of
other parts of the system's parsing technology (e.g., type checking
failures), and seems a worthwhile principle.

Making this dependency explicit helps Holmake avoid getting confused.

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 support for boolification of user-defined datatypes.

This is done by some "polytypic programming" in Datatype.sml copying
Konrad's existing code for generating size functions. However, since
it makes heavy use of lists, and lists come after Datatype in the
build sequence, this probably isn't the right place for the code to
live.

After discussing this with Michael, it would probably be best to move
the code to a module in src/Boolify/src, and register it using the
hook mechanism in the TypeBase.

Note that src/Boolify/src comes immediately after tfl in the build
sequence, because it defines some functions (such as num_to_bool)
using non-primitive recursion. Even if this could be "done by hand",
decoding boolean lists into datatypes will undoubtedly involve defining
some functions with hairy termination properties.

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

Minor changes.

Better diagnostics. Acknowledge successful type definition with a
HOL message, and also catch attempt to use an out-of-date type before
a definition is made.

Change stemming from split of TypeBase into TypeBasePure and TypeBase.

Changing arithLib to numLib.

Idiotic hacking about to get aligned with EnumType.

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

Changes to make case constant definition faster in EnumType.

Efficient definition of enumerated types.

Modifications caused by change of TypeBase signature.

Changes forced by change to type-parsing code, which now accommodates
specification of types using "dollared" syntax; e.g. min$bool.

Made Hol_datatypes print out a message when it fails. Saves the user
having to replicate the invocation wrapping it with handle e => Raise e.

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.

Bug in name being given to the exported size definition for mutual types.

Changes to accomodate proper definition of size functions for nested types.
Also, elimination of dependence on Ho_theorems.

Proper size definitions.

Catch duplicate field names in a record type error.

WHen a type has duplicate constructor names this is caught and reported
before a type definition is made. Bizarre errors happened otherwise.
Thanks to Dan Zhou of Florida Atlantic University for reporting this one.

Minor changes.

Fix for Datatype.sml bug that was causing export_theory to fail.

When defining more than one type at once, give the size definition the
name ty1_size_full_def; this is the name of the theorem, looking just
the same as the term that was passed to new_recursive_definition. Each
tyinfo then gets another theorem consisting of just the equations pertaining
to its type. These are saved with names "ty1_size_def", "ty2_size_def"
etc.

Modified to allow for possibility that defining the size function will
fail. Even prints out a "helpful" error message to this effect.

Modified to put size definitions correctly into the various tyinfos that
are generated, rather than defining the same set of constants once for
every type.

Changes due to the incorporation of John Harrison's datatype definition
package.
Here are the rest of the significant changes. The interface in Datatype
has been fleshed out quite a bit, but what was there has stayed pretty
much the same (except that prim_Hol_datatype doesn't write stuff out
to disk anymore; it's hardly very pure if it does so).

The ind_type theory is the basis for ind_types, which is in turn called
from Datatype.

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.

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

Moved function for defining case constants over standard datatypes to
Prim_rec from Datatype.

gen_tyinfo now needs fewer arguments; so calling it here has to change.

Removed reference to now-removed module ConstrProofs.

Moved type_size and tysize to basicHol90/TypeBase. This lowers the
support required to apply these functions.

Changes to accomodate new look portableML.

Fixed to bring it up to date with Taupo release 0.
(Changes have come across from parse_branch development.)

Initial revision