Fix examples/l3-machine-code

Add conversion INT_WORD_GROUND_CONV.

Avoid "inventing new type variable" messages when loading some Lib files.

Add some extra helper functions within utilsLib.

Use <=> instead of = for some boolean equalities

Make l3-machine-code/utilsLib parse wrt a specific grammar

Add brackets to reduce sensitivity to equality looseness

Speedup CASE_RAND_CONV.

Remove a print_thm in CASE_RAND_CONV (used in testing).

Implement CASE_RAND_CONV.

This is still somewhat experimental - it can convert instances of

f (case x of .. => y1 | .. => y2 | .. => yn)

to

case x of .. => f y1 | .. => f y2 | .. => f yn

Update some Holmake files to use CLINE_OPTIONS.

Update for the latest version of L3.

Changes have been made when exporting operations of the form:

`f : args -> state -> value * state`

If the state is not changed then this is now exported as

`f : args -> state -> value`

If the state is changed but the `value` type is `unit` then it this is now exported as

`f : args -> state -> state`.

Support for simplifying and evaluating enumerated type representation/abstraction maps.

For example, given

Datatype `enum = one | two`;

the following now works

> EVAL ``num2enum 1``;
val it = |- num2enum 1 = two: thm
> EVAL ``enum2num two``;
val it = |- enum2num two = 1: thm

> SIMP_CONV (srw_ss()) [] ``enum2num two``;
val it = |- enum2num two = 1: thm
> SIMP_CONV (srw_ss()) [] ``num2enum 1``;
val it = |- num2enum 1 = two: thm

This also works when building custom compsets using computeLib. add_datatype_info.

NOTE: This change may break some proofs (some in example/ARM have been fixed).

Update L3 examples.

Most changes relate to Poly/ML moving to fixed-width integers.

Various updates to the L3 examples.

Most changes are brought about by improvements and generalisations within stateLib and utilsLib.

A Holmakefile has been added to a new decompilers sub-directory and some *decomp_demoScript files have also been added. This makes it easier to perform regression testing.

Print out configuration options when an unrecognised option is supplied.

Update model for latest version of L3.

Towards decompilation of MIPS.

Fails for code with branches.

Contains minor changes elsewhere (e.g. handling of endianness and quotations).

Update ARM tools.

Provides support for a few more instructions.

Improvement for utilsLib.add_datatypes.

Update for L3 examples.

Fixes a potential problem with the handling of word replicate.

Moves some shared code into stateLib (the register_combinations function).

Some other minor fixes.

Fix for utilsLib.Run_CONV.

Tweaks within utilsLib.

Move some shared code into utilsLib.

Updates for machine-code tools.

Added support for introducing SEP_ARRAY predicates for memory operations (applied to the ARM and M0 models).

The ARM-M0 model is now hooked up to the "core/fast" decompiler.

The Hoare-triples for PC-relative loads now have immediate values appearing in the code-pool.

This affects the triples that are generated for instruction such as "ldr r1, [pc, #12]".

The tools for the other ISA models need minor updates following changes in stateLib.

Support more ARM VFP instructions.

Adds VMOV, VCMP and VMRS.

Changes to the standard L3 ARM model.

These have been brought about by minor modifications to the L3 export (a little bit more simplification occurs).

Updates to l3-machine-code.

Includes a monadic version of the ARM model, which includes data aborts.

Add tool support for LDM instructions that load to the PC, i.e. those that
perform a branch.

New ARM and x86 instruction set models, with tool support for generating Hoare triples.

The new models are generated using a domain specific language; see ITP 2012 paper: "Directions in ISA Specification" (LNCS 7406).

The tools should be quite a bit faster than those found in examples/ARM/v7 and examples/machine-code. However, they are less extensive (this is work-in-progress).