Add fcpSyntax and tidy up related code.

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

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 type guessing for L2V

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

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

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.