Don't export ERR from HolKernel

Minor clean up of fcpLib.

Clean up of fcpTheory. Also added a few new constants.

The new constants are: FCP_CONCAT, FCP_ZIP and FCP_FOLD.

The definition of V2L has changed — avoiding the unnecessary use of Hilbert choice. Also removed the sub1 type constructor. These were introduced in 102792de.

Minor bug fix.

Add fcpSyntax and tidy up related code.

Avoid possible non-termination with FCP length guessing, e.g.
``L2V [T;T] : word3`` wasn't terminating. Should possibly give a
warning if such cases are detected.

Add notification for guessing the type of L2V - also added its definition to
the words compset.

Add syntax support for bit_field_insert.

Add trace variables for controlling the pretty-printing of words and for
guessing word lengths. The function guess_word_lengths has been renamed
inst_word_lengths and output_words_as_dec is now remove_word_printer.

Trace "word printing" controls reference wordsLib.word_pp_mode.

0 - default: values >= 0x10000 print in Hexadecimal, otherwise in Decimal
1 - Binary
2 - Octal
3 - Decimal
4 - Hexadecimal

For example:

- with_flag (wordsLib.word_pp_mode, 1) term_to_string ``32w:word5``;
> val it = "0b100000w" : string

Trace "guess word lengths" controls flag wordsLib.guessing_word_lengths.

For example:

- with_flag (wordsLib.guessing_word_lengths, true) Term `(7 >< 0) w`;
<<HOL message: inventing new type variable names: 'a, 'b>>
<<HOL message: assigning word length(s): 'b <- 8>>
> val it = ``(7 >< 0) w`` : term

Added some extra functions under EmitML e.g. toWord32 and fromString32.

Made fcpLib.index_to_num more robust. It can now cope with sum types.

Added Cases_word_value and Cases_on_word_value. These do case splitting
on the numeric value of a word.

Made some changes to the pretty-printing support for words.

The functions "pp_word", "pp_word_bin" etc. have been replaced by
"output_word_as", "output_word_as_bin" etc.

The function "output_word_as" is more flexible and a custom printer is
turned on by default when wordsLib is loaded. (Word literals with a
value >= 0x10000 are printed in hex, otherwise they are printed as decimal.)

Added "dont_guess_lengths" function, which undoes "guess_lengths".

Added wordsTheory.WORD_INDUCT. This can be used with wordsLib.Induct_word.

Added WORD_DECIDE_TAC and made some changes to WORD_DECIDE (to handle terms with quantifiers).

Made changes to SIZES_CONV for faster evaluation of ``dimword(:N)`` etc. (Was slow for large N.)

Dropped wordsLib.WORD_GROUND_ss -- this is contained within srw_ss() and WORD_ss.

Trivial change to get rid of "Guessing type variable ..." style mesg
when this library loads.

Added type guessing for L2V

Make INDEX_CONV work with sum types.

Thanks to Michael's last check-in, index types are now directly
supported by the parser/printer, so there is no need to introduce
the "iN" type abbreviations. The function fcpLib.mk_index_type
has been removed.

* Users of the theory must delete all occurrences of "i"
* e.g. ``:i32`` must change to ``:32``.

There is now support for evaluation with non-standard word sizes e.g.

- load "wordsLib";
> val it = () : unit
- EVAL ``123w + 321w:56 word``;
> val it = |- 123w + 321w = 444w : thm

Non-standard word sizes will evaluate more slowly when first used.
However, size theorems are then added to the compset, so subsequent
evaluations will be quicker.

There is no change with standard word sizes e.g. can still use
``:word32`` and

- wordsTheory.dimword_32;
> val it = |- dimword (:32) = 4294967296 : thm

Second go at changing the scheme for index types. The new scheme uses:
``:one``, ``:'a bit0``, and ``:'a bit1``. For example, ``:i18`` is
``:one bit0 bit0 bit1 bit0``. The EmitML code is more like the original
version i.e. the performance loss is avoided.

Have changed the way that index types are created. The new scheme
uses a canonical form, with ``:bool # 'a`` used to double the index
size and ``:'a option`` used to increment it. The index type is
generated by a new function fcpLib.index_type; for example:

- fcpLib.index_type 5;
> val it = ``:(bool # bool) option`` : hol_type

The function fcpLib.mk_index_type performs roughly as it did before,
however, a type abbreviation is now used for the index type. These
abbreviations are printed for indexes > 8. For example:

- fcpLib.mk_index_type 5;
> val it =
(|- FINITE UNIV, |- CARD UNIV = 5, |- dimindex (:(bool # bool) option) = 5)
: thm * thm * thm
- ``:i5``;
> val it = ``:(bool # bool) option`` : hol_type

- fcpLib.mk_index_type 30;
> val it = (|- FINITE UNIV, |- CARD UNIV = 30, |- dimindex (:i30) = 30) :
thm * thm * thm

It is not expected that these changes will break anything...

Alter the n-bit word theories to use the :'a itself type, and also add
new constants (TOP(:'a) and MSB(:'a)) to stand for the numeric value of
2 ** width, and 2 ** (width - 1). Using these makes the expression
of several results a lot nicer. As the updated proofs in integer_wordScript
demonstrate, you don't always have to expand these definitions either,
which is nice.
I'm not 100% sure that these are the best names for these constants.

Having both mk_index_type_thm and mk_index_type is probably unnecessary.

add mk_index_type_thm
ines beginning with `CVS:' are removed automatically

* Added a theorem w2w, which makes proofs about w2w a little easier.

* bitLib and machine_wordsLib have been dropped and wordsLib extended.

* wordsLib now has a function mk_word_type, which adds a type abbreviation
for a new word size.

* Fixed Cases_on_word so that it does type instantiation.

* Increased the number of word sizes provided by machine_wordsTheory.

* Added a couple of simpset fragments (SIZES_ss and FCP_ss).

A new theory of words - based on an idea from John Harrison.
This is now a unified theory of words - so there's no more need
for the Functor or mkword.exe.

The old library (n_bit) will eventually be dropped, so current
users are advised to adopt the new library as soon as possible.
NB. bitTheory is nearly identical to the old bitsTheory.

The new representing type is finite Cartesian products e.g.
:bool ** 'a is the type for words whose length is the size
of the indexing type 'a.

The function fcpLib.mk_index_type can be used to create the
required index type.

Most theorems from the old theory should be present (if I've
missed any out then let me know). NB. A few theorems have
changed name and some have been dropped (e.g. there is no longer
a word_suc function).

Some symbols have changed. This avoids complaints from the
parser and should hopefully aid readability.

old new
two's comp. : ~ $-
bitwise not : NOT ~
bitwise or : | !!
bitwise and : & &&
bitwise xor : # ??
unsigned < : <. <+
unsigned <= : <=. <=+
unsigned > : >. >+
unsigned >= : >=. >=+

The bits and slice functions no longer map to :num - they now
map from :bool ** 'a to :bool ** 'a.

bits : WORD_BITS h l w (h -- l) w
slice : WORD_SLICE h l w (h <> l) w

The function w2w converts between words of different sizes
(unsigned) and sw2sw is a signed (2's complement)
word-word conversion.

The library machine_wordsLib provides the types word4, word8
word16, word32 and word64. Ground term evaluation with
EVAL should work here. Some operations (+, *) can be evaluated
with alpha types e.g.

EVAL ``6w + 4w``;
<<HOL message: inventing new type variable names: 'a>>
> val it = |- 6w + 4w = 10w : thm

Subtraction only works when the word size is known e.g.

EVAL ``6w:word8 - 4w``;
> val it = |- 6w - 4w = 258w : thm

An attempt to do evaluation with alpha types around will likely
result in gibberish.