| #
1d0debf0 |
|
14-Sep-2005 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
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.
|