Remove "big records" optimisation

Fix a record pretty-printing failure

If pretty-printing something like

<ldelim> contents <rdelim>

the PP block has to go around the whole phrase, but the indent on the
block has to be the width of the ldelim.

With test-case.

More fixes given testutils API change

Test and fix for bug caused by not checking reference in right order

Regression test for EVAL over i. field updates; ii. K x o K y

Thanks to Anthony for prompting this by isolating the problem I was
having elsewhere.

Add regression test for printing multi-line records

Fix bug in prove_case_elim_thm

Test-case tweaks old bug, which was caused by conflicting names. If
the first constructor in the type was

C ty

and a later constructor was D (ty -> bool), then the code would end up
with a theorem of the form

x = D f /\ ... |- caseconst x f f1 f2

where the f in the hypotheses corresponded to the argument to the D,
and the f in the conclusion corresponded to the function passed to the
case-constant, taking a ty and returning (in this case) a bool. Then,
when CHOOSE tried to wrap an existential around the f in the
hypothesis, it would fail because we'd inadvertently identified two
variables that were supposed to be different.

Fix is to be even more paranoid about choice of variable names when
stripping the existentials arising in type's nchotomy theorem.

Bug was apparent in examples/lambda/typing/type_schemasScript.sml

Improve datatype parsing, including ; as terminator inside records

More tests included.

Allow trailing semicolons in datatype declarations

Also:
- factor out datatype declarations for related AST types so that they
print nicely in Poly/ML interactive loops
- share more code between parsers of old and new syntax

With test-cases.

Closes #446

Fix bug in repeated Datatype calls with mutual recursion

Closes #435

Allow specific overload to override record upd p/printing

Closes #393

Add another test for ParseDatatype's lexing

Fix bug identified by test in c2fc2ca

Also fix tests themselves and add another in similar vein.

New breaking test-case for datatype parsing

Stop reusing a type name in datatype selftest

This avoids a distracting (and irrelevant) warning message

Get better error messages from datatype selftest

Fix many selftests to have prettier output

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

Fixes with polymorphic record literals

1. When you write <| fld1 := foo ; fld2 := bar |> there is secretly an
ARB term hiding in the result. You don't want that ARB term to be
unnecessarily polymorphic.

2. TypeBase.mk_record has to adjust for the possibility that fupds can
have types of the form

fupd : (α fldty -> β fldty) -> (α,γ) rcd -> (β, γ) rcd

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

Fix another record pretty-printing problem

Another record pretty-printing bug.

It should be reasonable to write

rcdname_fldname_fupd f

which is a function that takes a record, applies f to the given field,
and returns the updated record. Unfortunately, it gets printed in
hideous fashion.

Tests for prettyprinting polymorphic record ops

Github issue #150

Datatype now handles antiquotations.

Closes #258

Datatype: qual-ids stop creation of recursive type

Closes #257

Tidy up Datatype selftest

Implement function to prove a case-constant elimination rewrite

regression test for #91

Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.

Fix a bug where overloads didn't take precedence over field selection pretty-printing.

Demonstrated by the test-case in src/datatype/selftest.sml

Add new Hol_datatype bug to exhibiting TypeNet failure.

Clean the second set of Hol_datatype bugs to do with itself.

They should exemplify one bug, not two. The TypeNet bug can be tested by
another entry in the selftest.

Fix for the bug in Hol_datatype to do with nested types and itself.
Also includes another selftest that discriminates between the current fix and a previous non-fix I tried.

The problem, I believe, was in how the actual new types being defined were filtered out of the domains of functions asserted to exist by the recursion theorem.
The old way was to exclude types with an argument appearing somewhere else in the set of candidate types.
The new way is to simply exclude types with non-variable arguments.
I'm not sure this is right, but it works.

The selftests still fail, but for an entirely different reason: the second test tries to redefine the types t1 and t2 from the first test.
Using distinct names would fix this, but I would rather have the ability to redefine a name.

Selftest for (as yet unfixed) bug in Hol_datatype to do with the itself tyop.

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

Bug reported by Ramana Kumar.

Adjust a whole bunch of selftests to use Unicode at zero. In some
cases this is just for the sake of prettiness (making columns line
up), but in others, where the test is of the pretty-printer, I didn't
want to alter the tests.

I updated the src/datatype/selftest code unnecessarily in response to
my pretty-printing backend change. This revision puts it back to the
way it was.

Separate pretty-printing code into two halves, with a backend
component able to provide special treatment of the basic
pretty-printing functionality. The front-end can call a special
version of add_string in order to let the back-end know that a certain
piece of text has special properties. The handling of the given
annotations is up to the backend.

The raw_terminal backend ignores all annotations.

The emacs_terminal backend is the same as the raw_terminal backend for
the moment because I can't figure out how best to pass information
on.

The vt100_terminal backend colours free and bound variables blue and
green respectively using ANSI/vt100 escape codes. You should see this
if you start up HOL in an xterm (or gnome-terminal, or ...).

The current_backend reference variable in Parse can be set to alter
the backend being used for printing. For example, if you do

Parse.current_backend := PPBackEnd.vt100_terminal

while running in emacs, you will see your terms mangled with lots of
\^[ type junk.

I think a LaTeX backend should be possible, as might some sort of XML
or MathML thingy.

I suspect my token merging avoidance code will need updating.

Also, change std.prelude to set the interactive flag earlier, so that
Parse can see it (it will use raw_terminal if loaded non-interactively).

Fix the test to "work" (it still fails because the underlying code
hasn't been fixed, but at least it compiles). I needed to replace
new_infix_type with add_infix_type. The former asserts a new type,
the latter just adds syntax for an existing type.

A new datatype definition test-case that is not handled (yet). The
code for types is supposed to handle recursions under type operators
that have themselves already been defined using Hol_datatype. This is
how definitions with recursions under the prod operator were
working (mostly) until Peter special-cased prod.

Add test-case for the bug that Tom Ridge reported and Peter Homeier
fixed.

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.

Fix for an error in datatype declaration parsing when the apostrophe
of a type variable immediately follows the colon in a field type
spec. Originally, found in examples/HolCheck, but have also now moved
an example into the selftest.

Variables in the patterns of case expressions are now properly
'fresh'. They bind expressions on the other side of the case-arrow,
but do not affect variables outside the case expression or in other
branches. This revealed a bug in DecodeScript, where a theorem about
encoding sums ended up being about sums of type 'a + 'a only because
case pattern variables that should have been independent weren't.

Modify lexing so that "mixed" tokens are possible if a user puts them
into the grammar. For example, one might do

set_fixity "-->a" (Infix(NONASSOC, 450))

This then causes ``p -->a q`` to be parsed as an infix application of
-->a to p and q. If you wrote ``p --> a q``, the -->a token would not
be seen. Without -->a being in the grammar, it will be lexed as
before, a symbolic token (-->) followed by an alphanumeric one (a).
(Note also that things like --a--> where the mixing up happens in the
middle of the token, are just as possible.)

This change also allows traditional alphanumeric identifiers to
combine with Unicode subscripts. Using LaTeX notation, a_1 is now
possible.

The system builds with selftest level 1, so I believe I have preserved
backwards compatibility. (I have also added a test to
src/bool/selftest.sml to check for _1 working as a case expression
pattern properly.)

Fixes for record printing, and a bunch of self-tests (including some
for "big" records, whose internal structure looks quite different),
particularly after simplification.

Extend the datatype selftest with pretty-printing tests for record types.

Move selftest to datatype directory, where it more rightfully belongs,
and incorporate some new tests from the ParseDatatype.sml file. (These
needed updating because they weren't themselves valid.)