Get ARM examples to build; v7-step regression fails though

change interface to add_persistent_funs (#73) and fix more calls

The new interface takes a list of strings naming theorems.
(The old interface took a list of (string * thm) pairs.)
The new way better ensures consistency of theory development and theory
load behaviour: you can no longer pass a name with a theorem that isn't
actually saved under it.

Theorems are looked up with DB.theorem, or failing that, DB.definition
or DB.axiom.

Alas, I found more examples using add_persistent_funs to add theorems in
ancestor theories. Rather than modify the ancestor theories, I have
opted to make the offending theories save the theorems they want to add
to computeLib themselves so they have a name in the current theory to
pass to add_persistent_funs.

If this behavior was appropriate for patricia too (da47401) change it.
Alternatively, if the ancestor theories should have exported those
things for computeLib anyway, search this commit for new instances of
"save_thm" to see what needs fixing.

Minor fixes.

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

Fix problem with instructions of the form ldm <rn>!,{...,pc}^.

Base register write-back was happening in the wrong mode.

sign_extend has moved to wordsTheory. Also, avoid TeX_notation warning.

Correct spelling. Also move location of SInt and UInt.

Move some definitions from arm_opsem to arm_coretypes.

Added word_sign_extend to src/n-bit.

Minor fix.

Minor change to the predictability of the CPS instruction, to keep up with the
ARM Reference Errata 8.

Fix evaluation with regard to LDM/STM instructions with the base register in
the register list and write-back enabled.

In some places move the position of increment_pc (under operator |||).

A few changes:

- Make use of the new zDefine
- Moved some theorems from arm_stepTheory to arm_opsemTheory and
arm_coretypeTheory, e.g. change_processor_state_thm and encode_psr_bit
- Changed some instruction specifications -- moving the call to
current_mode_is_user_or_system.
- Remove unwanted application of WORD_ARITH_ss in arm_stepLib. This was
inadvertently added in a previous check-in.

Update that adds support for ThumbEE.

/* From the ARM reference...

ThumbEE

Is a variant of the Thumb instruction set that is designed as a target for
dynamically generated code. It is:
* a required extension to the ARMv7-A profile
* an optional extension to the ARMv7-R profile. */

Added support for hardware interrupts: reset, fiq and irq. This adds an extra
argument to the next state functions, i.e. we now have

arm_next : iiid -> HWInterrupt -> unit M

and

ARM_NEXT : HWInterrupt -> arm_state -> arm_state option

In the absence of an interrupt, the previous behaviour is obtained with

ARM_NEXT NoInterrupt : arm_state -> arm_state option

The single-step behaviour for interrupts can be obtained with

armLib.arm_step "" "reset" (* ARM_NEXT HW_Reset *)
armLib.arm_step "" "irq" (* ARM_NEXT HW_Irq *)
armLib.arm_step "" "fiq" (* ARM_NEXT HW_Fiq *)

There has also been some minor tidying-up to the code.

Fix for parsing of "blt" and similar mnemonics. Was attempting to parse
as "bl". Bug reported by Lu Zhao.

Fix parser so that it accepts RRXS.

Some changes to make things up-to-date with the latest ARM Architecture
Reference Manual, i.e. errata version 6. The changes mostly relate to the
specification of Undefined and Unpredictable instruction instances.

Numerous assorted changes, including:

- renamed some constants, e.g. sN -> psrN etc.
- changed handling of IT state for architecture versions < v6T2.
- some fixes to the parser and to the handling of the ADR instruction.
- added a couple of functions (arm_parserLib.calc_itstate and
arm_random_testingLib.arm_step_updates).

Fix bug with condition test for le/gt.

bit_field_insert is now in wordsTheory.

add_with_carry has moved to wordsTheory. Also made some tweaks to evaluation.

Get ror (register), asr (register), lsl (register), asr (register) working
for 32-bit Thumb.

Storing the PC is unpredictable in Thumb mode.

Address bug with 16-bit signed multiply & saturate instructions
(word_bits -> word_extract).

A few changes:

1. Make it clear that the ARMv7-M profile is not properly supported (yet).
2. Fix for EmitML script (following changes to memory).
3. Fixed parsing/encoding for 16-bit Thumb MOV (register) instruction.
4. Fixed bugs in model for BFI, SSAT and SSAT16.

Changes to the memory, to conform with the approach that Magnus explored in
ARM/experimental.

The memory now has type :address -> word8, instead of :address -> word8 option.
Accesses are recorded in a component state.accesses : memory_access list.

Word slice "<>" has been replaced with "''".

Fix bug in the model (relating to encoding of Thumb2 immediate values).

Also add more checks to encoding function and fixed a couple of bugs in
the parser/encoder/disassembler.

A new Monadic ARM instruction set specification. Covers all current ISA
versions i.e. ARMv4 to ARMv7.

Doesn't cover the ThumbEE, VFP and Advanced SIMD extensions. Also doesn't
model hardware interrupts - these will be added at a later date.

To use the armLib tools, Moscow ML users will likely have to apply the patch to
avoid the Chr exception.
<http://hol.sourceforge.net/mosml-chr-instructions.html>