#
e5fc0f36 |
|
11-Sep-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Improving naming of bit-vector signed division constants. This renaming introduces incompatibilities: • words$word_sdiv -> words$word_quot (this is proved to be related to int_quot for a non-zero divisor). • words$word_srem -> words$word_rem (this is proved to be related to int_rem for a non-zero divisor). • integer_word$word_sdiv (this is a new constant defined directly in terms of int_div). • words$word_smod -> integer_word$word_smod (this is now defined directly in terms of int_mod).
|
#
ac817518 |
|
11-May-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Modify the type of HolKernel.syntax_fns and add some documentation. This is in response to issue #247. The change to the type makes things a little more natural when using partial applications - for example, HolKernel.syntax_fns1 can be used to provide syntax support for regular unary operations.
|
#
bbe4fa68 |
|
27-Jul-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
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.
|
#
e63585cf |
|
14-Jan-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Further small improvements to PTREE_PEEK_CONV. Squeezes out a tiny bit more performance. The wordsLib conversion BIT_SET_CONV has been updated and is now exported.
|
#
ba6a436f |
|
24-Aug-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Move bit_count constants from examples/ARM/v7 to wordsTheory.
|
#
ebff75bd |
|
21-Aug-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update some syntax files to use HolKernel.syntax_fns.
|
#
f0877329 |
|
11-Jun-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor fix for wordsSyntax.dest_word_extract.
|
#
04de767e |
|
12-Mar-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add min and max operations to wordsTheory.
|
#
5cf70d46 |
|
08-Mar-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add toString and fromString to integer_wordTheory. Also, make improvements to syntax files.
|
#
8936acfe |
|
08-Mar-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Overhaul to wordSyntax to make it less verbose. Added some missing constants (word_from_bin_list etc.) at the same time.
|
#
6b27ccd5 |
|
05-Mar-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add support for "word_abs" and "word_len" in wordsSyntax.
|
#
9b64342c |
|
16-Aug-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add wordsSyntax.size_of.
|
#
4b685909 |
|
22-Jun-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added new definitions and theorems for various bit-vector "saturation" operations. These operations return maximal or minimal values instead of, e.g., overflowing (wrapping). For example: |- signed_saturate_add 100w 50w = 127w: thm Also added a new configuration option for printing word literals as 2's complement values. For example: > set_trace "word pp as 2's comp" 1; > ``253w:word8``; val it = ``-3w``: term Be warned that this term is actually ``n2w 253``, it's just being printed as ``word_2comp (n2w 3)``. This printing mode is useful when checking the veracity of machine arithmetic. For example: > EVAL ``signed_saturate_sub 226w 100w : word8``; val it = |- signed_saturate_sub -30w 100w = -128w: thm
|
#
2e079a71 |
|
29-Mar-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added new operations for shifting by a bit-vector value, namely: LSL: <<~ LSR: >>>~ ASR: >>~ ROR: #>>~ ROL: #<<~ These are supported by the procedures in blastLib. For example, one can prove w <+ 10w /\ s <+ 3w ==> w <<~ (s + 1w) <+ 73w : word16 The time-complexity is a pretty shocking but "simple" 32-bit problems seem to be okay. NB. ROR and ROL only bit-blast with word sizes that are a power of two. Added a new conversion WORD_MOD_BITS_CONV for mapping applications of ``word_mod w (n2w n)`` into ``(h -- 0) w`` where n is a power of two. Also added support for bit-blasting arbitrary multiplication, but the word-size limit is set to 8 bits by default. Things seem to be just about feasible with that limit (and become horrendously slow after that). To improve performance, the conversion BBLAST_CONV does not have exactly the same coverage as before. For backward compatibility, a conversion EBLAST_CONV (which calls SAT at every bit position) is now available.
|
#
d9777034 |
|
25-Oct-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add fcpSyntax and tidy up related code.
|
#
afa84c34 |
|
14-Oct-2010 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Added a function word_compare, along with the usual syntax operations.
|
#
64d029ca |
|
14-Oct-2010 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Added functions word_s{rem,mod} (2's complement signed remainder), along with their usual syntax operations.
|
#
c8cecd58 |
|
14-Oct-2010 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Added the usual syntax operations for word_sdiv.
|
#
9e093a19 |
|
06-Sep-2010 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
mk_word_replicate now computes the width of the resulting word when applied to a numeral and a fixed-width word.
|
#
ad74a98b |
|
30-Jul-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Make WORD_MUL_LSL_CONV more robust with respect to oversized word literals. For example, we now have > WORD_MUL_LSL_CONV ``130w * w : word4``; val it = |- 130w * w = w ≪ 1 : thm whereas previously it would fail.
|
#
4d386328 |
|
26-May-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added a bit-blasting conversion: BBLAST_CONV. This goes beyond the capabilities of WORD_BIT_EQ_CONV by expanding out additions / subtractions. This allows the new conversion to automatically handle small but tricky bit vector goals. For example: ``(x && 3w = 0w:word32) ==> ((x + 4w * y) && 3w = 0w)`` and ``!a:word8. a <+ 4w /\ b <+ a /\ c <=+ 5w ==> (b + c) <=+ 7w`` (These aren't provable with wordsLib.WORD_DECIDE.) Obviously bit-blasting is a brute force approach, so the new conversion should be used with care. It will only work well for smallish word sizes and when there is only and handful of additions around. It is also "eager" -- additions are expanded out even when not strictly necessary. For example, in ``(a + b) <+ c /\ c <+ d ==> (a + b) <+ d:word32`` the sum ``a + b`` is expanded. Users may be able to achieve speed-ups by first introducing abbreviations and then proving general forms, e.g. ``x <+ c /\ c <+ d ==> x <+ d:word32`` The conversion handles most operators, however, the following are not covered / interpreted: -- Type variables for word lengths, i.e. terms of type ``:'a word``. -- General multiplication, i.e. ``w1 * w2``. Multiplication by a literal is okay, although this may introduce many additions. -- Bit field selections with non-literal bounds, e.g. ``(exp1 -- exp2) w``. -- Shifting by non-literal amounts, e.g. ``w << exp``. -- ``n2w exp`` and ``w2n w``. Also w2s, s2w, w2l and l2w. -- word_div, word_sdiv, word_mod and word_log2.
|
#
4341ad42 |
|
04-May-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Further extend the bounds generation under WORD_DECIDE. For example, can now prove: wordsLib.WORD_DECIDE ``((4w * (3 >< 1) b + 10w) << 2) // 3w <+ 57w :word16`` Also added WORD_EXTRACT_ss to WORD_CONV. Unfortunately this can break proofs.
|
#
cd6f4cab |
|
18-Mar-2010 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Added the usual syntax functions for word_mod.
|
#
66692150 |
|
17-Mar-2010 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Added the usual syntax functions for word_div.
|
#
9edf20d8 |
|
31-Jan-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add dest_word_literal and uint_of_word to wordsSyntax.
|
#
50d74823 |
|
09-Dec-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add notification for guessing the type of L2V - also added its definition to the words compset. Add syntax support for bit_field_insert.
|
#
59e6f0f8 |
|
08-Dec-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add syntax support for the new words operations.
|
#
4761143b |
|
10-Aug-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed trailing whitespace from all .sml and .sig files. This affects over 900 files and was done using emacs's delete-trailing-whitespace function in batch mode. Building the system with Poly/ML and Moscow ML seems to work, so I'm hoping these changes don't break anything. Please complain if they do!
|
#
33cee0fe |
|
03-Aug-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
If possible ensure that mk_word_concat instantiates the result type.
|
#
4b557ffa |
|
20-Jan-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Free the name "index".
|
#
e0e46b4d |
|
26-Aug-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Extended the Unicode overloading. Also minor changes in evaluation and two new functions: mk_wordi and mk_wordii, which are ML integer versions of mk_word.
|
#
8496cf9c |
|
16-Jan-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added a number of tools for working with words. The main additions are: WORD_ss: Does some basic simplification, evaluation and AC rewriting (over *, +, && and !!). For example, ``a * 3w + a`` -> ``4w * a`` and ``a && 3w !! a && 2w`` -> ``3w && a``. BIT_ss: For example, ``BIT n 3`` -> ``n IN {0; 1}``. WORD_MUL_LSL_ss: Converts multiplications to left-shifts e.g. ``2w * a`` -> ``a << 1``. WORD_BIT_EQ_ss: Can be used to establish bit-wise (in)equality e.g. ``a && ~a = 0w`` -> ``T``. Does not work with *, + etc. WORD_ARITH_EQ_ss: Can be used to establish arithmetic (in)equality e.g. ``~(b + 1w = b + 4294967295w:word32)`` -> ``T``. WORD_EXTRACT_ss: Simplification for shifts and bit extraction. "Simplifies" --, w2w, sw2sw, #>>, @@ etc. and expresses operations using ><, << and !!. WORD_DECIDE: A decision procedure. Will solve Boolean (bitwise) problems and some problems over <, <+ etc.
|
#
82cfb2fa |
|
09-Jan-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added a bunch of new theorems.
|
#
84191604 |
|
02-Mar-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Changed the definition of word_rxx to something more sensible.
|
#
45d08362 |
|
02-Mar-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Changed the definition of word_concat so that it now applies a word-to-word conversion. Thus, it is now possible to do: - EVAL ``((0b1111w:word4) @@ (0b110011w:word6)):word10``; > val it = |- 0b1111w @@ 0b110011w = 0b1111110011w : thm The old definition (which produced something of type :word4+word6) has been renamed to word_join. Apologies to anyone affected by this update.
|
#
16a67e01 |
|
27-Feb-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
A few changes: * Replaced old_arith_ss with the new arith_ss - fixing the broken proofs. * Used names (instead of symbols) when defined some operations e.g. word_bits, word_or etc. * Added a few more functions: word_len, word_div (//, unsigned division) and word_sdiv (/, signed division).
|
#
fcb123bd |
|
03-Nov-2005 |
Konrad Slind <konrad.slind@gmail.com> |
Fixed some syntax operations to project out the dimension types, instead of the bool ** dim types.
|
#
61f34184 |
|
01-Nov-2005 |
Konrad Slind <konrad.slind@gmail.com> |
Fixing types of constructors and destructors for w2w and n2w.
|
#
bcdb58d6 |
|
30-Sep-2005 |
Konrad Slind <konrad.slind@gmail.com> |
Syntax support for words.
|