#
f2edae9d |
|
24-Nov-2020 |
Anthony Fox <anthony.fox@arm.com> |
make sure wordsLib.WORD_GROUND_ss covers "word_ge/gt/hi/hs" For example, previously ``3w >=+ 2w: word32``.
|
#
d6167e99 |
|
01-Nov-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Make global simpset state easier to recreate with "logged_update" This entry-point records that a change to the global simpset has happened within a piece of code (rather than a script). The change is made (as before), but the change is also recorded so that it can be recreated/applied to different base simpsets.
|
#
5f7b69ef |
|
22-May-2020 |
Hrutvik Kanabar <hrutvikkanabar@yahoo.co.uk> |
Add regression tests for words pretty-printing fixes
|
#
14bfc6e9 |
|
08-May-2020 |
Anthony Fox <anthony.fox@cantab.net> |
Fixes for wordsLib pretty-printing
|
#
fc263107 |
|
19-May-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Fix various breakages caused by 86935be3f42 Along the way adjust WORD_CANCEL_CONV to tidy up after itself so that when it sees x + y + z + u = a + y + b + u it doesn't turn it into x + y + z + u - y - u = a + y + b + u - y - u and wait for something else to clean it up, but rather goes straight to x + z = a + b
|
#
1964f7c3 |
|
01-May-2020 |
Andreas Lööw <AndreasLoow@users.noreply.github.com> |
Add compute cases for 0 for BIT_UPDATE
|
#
18b62363 |
|
11-Apr-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get src/n-bit to build given tight-equality
|
#
e48aefc6 |
|
17-Nov-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fully protect wordsLib's use of parser Because it is using various functions from Q, it can't just rebind the Parse structure, but must update the global grammar variable directly (and then remember to set it back). With regression test
|
#
de063b7a |
|
14-Nov-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make more type-abbrevs printing ones to keep word-emit working
|
#
d35b02e2 |
|
28-Mar-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Restore ppstream_funs as nullary type operator in term_pp_types This name is used in user-written code (users' special purpose pretty-printers), and there is no reason to rebind this name, forcing them to change things.
|
#
523c72e2 |
|
21-Mar-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fixes of bag, container, finite_map and in n-bit/
|
#
51a40c2e |
|
14-Mar-2018 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add facility to print bit-vectors in binary or hex with leading zero padding.
|
#
4888f523 |
|
15-Oct-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove eqtype declaration for term type
|
#
d530f31c |
|
21-Sep-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add conversion INT_WORD_GROUND_CONV.
|
#
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).
|
#
6b915612 |
|
24-Aug-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Avoid "inventing new type variable" messages when loading wordsLib.
|
#
ecb0e313 |
|
15-Mar-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add Conv.memoize. This can be used to build conversions that lookup previous result in a red-black tree. The n-bit libraries are updated to make use of Conv.memoize and new functions in computeLib.
|
#
b4ac84ed |
|
03-Mar-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Remove overloading INT_MINw2 and semicolons. Also make use of "*[simp]" instead of explicitly using export_rewrites.
|
#
e624a8a6 |
|
05-Feb-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Avoid warning message when loading wordsLib.
|
#
758774c8 |
|
29-Jan-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add theorem word_concat_assoc and an associated simpset fragment WORD_CONCAT_ASSOC_ss.
|
#
58b7f2bd |
|
20-Jan-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Various tweaks to bit-vector development. NOTE: It is possible that some bit-vector proofs may break, due to subtle changes in bit-vector simplification. The selftest script now tests calls to WORD_GROUND_CONV. (This conversion's flag is also set to false for use outside of wordsLib.) Some unused tools have been removed from blastLib.
|
#
9adc034d |
|
14-Jan-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
wordsLib.WORD_GROUND_CONV was failing for word_lsb.
|
#
4d38662b |
|
17-Dec-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Make wordsLib.n2w_INTRO_TAC more robust.
|
#
30f78bd2 |
|
14-Dec-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
User pp fns can note terms as binders to system printer This allows better behaviour in a test case shown to me by Mike, where annotations in monad-syntax weren't appearing.
|
#
d9207a99 |
|
02-Jul-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Allow matching over integer literals. Changes the mechanism for supporting new literals.
|
#
3237f4c2 |
|
26-Sep-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix for the definition of bit-string rotate. Bit-string were being padded when rotating by zero. Also improve wordsLib.WORD_GROUND_CONV.
|
#
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.
|
#
1c5b031e |
|
14-Apr-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Provide facilities for extending compsets with support for words, strings and integers.
|
#
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.
|
#
a17bf716 |
|
28-Oct-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Make wordsLib.word_EQ_CONV and stringLib.string_EQ_CONV slightly more efficient. Also extend the coverage of some *Syntax structures.
|
#
a9c9addc |
|
21-Aug-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
wordsLib.SIZES_CONV was not behaving properly when applied to some unsuitable terms. Was causing problems in blastLib.
|
#
318eaaa9 |
|
01-Aug-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Enhance behaviour of wordsLib.EXTEND_EXTRACT_CONV.
|
#
7a2254a5 |
|
14-May-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Move bitTheory into src/num/extra_theories and move evaluations theorems in wordsLib further up the build sequence. Includes some tidying-up work. This closes issue #120. Evaluation for "toNum" and "toString" can now be enabled by loading up stringLib (or, more precisely, ASCIInumbersLib), without the need to load up wordsLib. This check-in can be viewed as finishing off the (many) loose ends left over from work on issue #70.
|
#
e6364b62 |
|
01-Apr-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Remove the constant bit$LSB, which was simply arithmetic$ODD. This may break some user proofs. Also tidy-up bitScript and numeral_bitScript.
|
#
59b9bf6c |
|
05-Feb-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Slight tweak to Cases_{on_}word_value.
|
#
8638647b |
|
11-Nov-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Extend coverage of WORD_GROUND_CONV.
|
#
68acc3f6 |
|
19-Oct-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Make it easier to remove WORD_SUBTRACT_ss from srw_ss.
|
#
5f7ad54b |
|
02-Oct-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add WORD_BIT_INDEX_CONV and tweak word_bit_CONV.
|
#
ba6a436f |
|
24-Aug-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Move bit_count constants from examples/ARM/v7 to wordsTheory.
|
#
8554ea75 |
|
21-Aug-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Another patch following work on Issue #70.
|
#
b55f6c40 |
|
08-Aug-2012 |
Michael Norrish <michael.norrish@nicta.com.au> |
Move n2l and l2n constants (and similar) into new numposrep theory. A number of fixes follow on from this. Also mention the new theories (numposrep and ASCIInumbers) in the release notes. This is progress with #70.
|
#
1126c8b8 |
|
08-Aug-2012 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Move ASCII numbers stuff from bitTheory to ASCIInumbersTheory in src/string. Rather bloody surgery at this point. There may well be rough patches remaining. A number of knock-on effects in src/n-bit, as well as the movement of a nice rewrite about LOG into logrootTheory. This is progress with #70
|
#
7284cfcd |
|
24-Jul-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update wordsLib documentation. Also minor tweaks in wordsLib itself.
|
#
fee4467b |
|
20-Jul-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Tidy-up formatting of wordsLib code. Also add configuration parameter to WORD_GROUND_CONV.
|
#
bf071804 |
|
27-Jun-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor tweaks to various conversions under src/n-bit.
|
#
b99f6206 |
|
26-Jun-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add a theory of bit-strings, which defines word operations over ``:bool list``. The maps "v2w" and "w2v" provide a connection to fixed-width bit vectors.
|
#
87878f5d |
|
19-Mar-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added some theorems. Also ensure EVAL calls wordsLib.SIZES_CONV on `FINITE x` terms.
|
#
b5be4920 |
|
16-Mar-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Export LESS_CONV from wordsLib.
|
#
04de767e |
|
12-Mar-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add min and max operations to wordsTheory.
|
#
c0e456e5 |
|
28-Jun-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix WORD_MUL_LSL_CONV so that it works with ``:'a word`` terms, i.e. words of unspecified width.
|
#
913dbb12 |
|
27-Jun-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Another tweak to WORD_CANCEL_CONV.
|
#
a2f2b007 |
|
27-Jun-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor tweak to implementation of WORD_CANCEL_CONV.
|
#
f3bd4784 |
|
27-Jun-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add wordsLib.WORD_CANCEL_ss, which is a fancy version of WORD_ARITH_EQ_ss. WORD_CANCEL_ss is now used during the preliminary simplification stage of BBLAST_PROVE, which enables the procedure to better handle simple arithmetic properties (i.e. avoiding unnecessary bit-blasting). For example: we have > SIMP_CONV (srw_ss() ++ wordsLib.WORD_CANCEL_ss) [] ``2w * a - b * 2w + -7w = b + 1w + a`` <<HOL message: inventing new type variable names: 'a>> val it = |- (2w * a − b * 2w + -7w = b + 1w + a) ⇔ (3w * b + 8w = a): thm which is preferable to > SIMP_CONV (srw_ss() ++ wordsLib.WORD_ARITH_EQ_ss) [] <<HOL message: inventing new type variable names: 'a>> val it = |- (2w * a − b * 2w + -7w = b + 1w + a) ⇔ (a + -3w * b + -8w = 0w): thm
|
#
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
|
#
58efc826 |
|
06-Jun-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Improve HolSmt's coverage of bit-vector problems. This involves mapping some HOL bit-vector operations into suitable SMT-LIB operations. In particular, provide support for: 1. reduce_and, reduce_or, etc. This is done using wordsLib.EXPAND_REDUCE_CONV. 2. word_lsb, word_msb, word_bit, word_bits, word_slice and bit_field_insert. This is done through rewrites. 3. (w2w:'a word->'b word) and (sw2sw:'a word->'b word) where the word size decreases. Again done using rewrites. 4. ((h >< l) w) : 'a word, where 'a word is larger than h + 1 - l. This is done using wordsLib.EXTEND_EXTRACT_CONV.
|
#
11d15e09 |
|
17-May-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor tweaks to word evaluation (LSL now incorporates a mod).
|
#
9c35830c |
|
14-Apr-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix glitch in WORD_AND_CANON_CONV.
|
#
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.
|
#
f59b5956 |
|
11-Mar-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Assorted extra theorems and tools. Added a new constant word_abs, which gives the absolute value of a bit-vector.
|
#
8610b67b |
|
07-Mar-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix for add_word_cast_printer.
|
#
7a497d52 |
|
24-Jan-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix addressing broken proof in examples/ARM/v7.
|
#
1f607f6f |
|
24-Jan-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Small tidy-up.
|
#
9bc7e4f5 |
|
21-Jan-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Changes to WORD_MUL_LSL_CONV in an attempt to make it more robust - it was failing on some corner cases. It should also be a bit quicker now too.
|
#
6cf565a6 |
|
12-Jan-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add function boolSyntax.dest_strip_comb. boolSyntax.dest_strip_comb ``a + b``; val it = ("arithmetic$+", [``a``, ``b``])
|
#
a4acbc77 |
|
06-Jan-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Significant change to pretty-printing; affects user-printing API. The change allows user-printers to alter the main printer's notion of what is a "seen free variable", and what is bound. The latter causes the colouring. The first notion is important when show_types is on, as types are only given for the first occurrence of a free variable. This allows the monadsyntax to do the right thing with the colouring of variables.
|
#
f6167147 |
|
03-Dec-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add a few extra tools to wordsLib: * WORD_SUB_CONV / WORD_SUB_ss These can be used to simplify applications of unary/binary minus, introducing or eliminating subtractions where possible. These must *not* be used simulataneously with srw_ss, WORD_ARITH_ss or WORD_ss (as this will likely result in non-termination). However, can be used to good effect afterwards. For example: wordsLib.WORD_SUB_CONV ``a + -1w * b`` |- a + -1w * b = a - b wordsLib.WORD_SUB_CONV ``-(a - b)`` |- -(a - b) = b - a wordsLib.WORD_SUB_CONV ``a + b * 3w : word2`` |- a + b * 3w = a - b wordsLib.WORD_SUB_CONV ``192w * a + b : word8`` |- 192w * a + b = b - 64w * a * WORD_DIV_LSR_CONV Convert division by a power of two into a right shift. For example: wordsLib.WORD_DIV_LSR_CONV ``(a:word8) // 8w`` |- a // 8w = a >>> 3 * BITS_INTRO_CONV / BITS_INTRO_ss These convert DIV and MOD by powers of two into application of BITS. For example: wordsLib.BITS_INTRO_CONV ``(a DIV 4) MOD 8``; |- (a DIV 4) MOD 8 = BITS 4 2 a wordsLib.BITS_INTRO_CONV ``(a MOD 32) DIV 8``; |- a MOD 32 DIV 8 = BITS 4 3 a wordsLib.BITS_INTRO_CONV ``a MOD 2 ** 4``; |- a MOD 2 ** 4 = BITS 3 0 a wordsLib.BITS_INTRO_CONV ``a MOD dimword (:'a)``; |- a MOD dimword (:'a) = BITS (dimindex (:'a) - 1) 0 a * n2w_INTRO_TAC <int> Attempts to convert goals of the form ``a = b``, ``a < b`` and ``a <= b`` into goals of the form ``n2w a = n2w b``, ``n2w a <+ n2w b`` and ``n2w a <=+ n2w b``. The integer argument denotes the required word size. This enables some bounded problems (over the naturals) to be proved using bit-vector tactics. For example, the goal: `((11 >< 8) (imm12:word16) : word12) <> 0w ==> ((31 + 2 * w2n ((11 >< 8) imm12 : word12)) MOD 32 = w2n (2w * (11 >< 8) imm12 + -1w : word32))` can be solved with STRIP_TAC THEN n2w_INTRO_TAC 32 THEN FULL_BBLAST_TAC
|
#
1a42b2f2 |
|
25-Oct-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Bug fix.
|
#
6283401d |
|
30-Sep-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix glitch in WORD_OR_CANON_CONV where, for example. ``0x20000000w !! 0w`` would not be converted to ``0x20000000w``.
|
#
8d1454ae |
|
27-Sep-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add ground term evaluation of fcp$:+ to the words simpset.
|
#
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.
|
#
34306e4a |
|
17-May-2010 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Removed Unicode character.
|
#
e3a3572e |
|
06-May-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make wordsLib use a fixed grammar for its internal parsing. This prevents breakage when variables such as 'P' turn out to be constants in the global grammar. This was happening in examples/Crypto/IDEA thanks to ExtendedEuclidTheory.
|
#
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.
|
#
b727df86 |
|
21-Apr-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added some new theorems that help when reasoning about word concatenation.
|
#
d3804cd7 |
|
19-Apr-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor fix.
|
#
0501e97a |
|
16-Apr-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Restore some rewrites that were inadvertently removed in revision 7947. These rewrites are included in srw_ss but this won't always be around.
|
#
f62f1f72 |
|
15-Apr-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Simplification to WORD_BIT_EQ_CONV, making it more closely based on WORD_BIT_EQ_ss. This should help improve the effectiveness of WORD_DECIDE.
|
#
f24d829d |
|
26-Mar-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Tidy up of simpsets and simpset fragments. Also fixes the problem of a bad key in WORD_ADD_ss. Be aware that this change can break proofs -- apologies in advance.
|
#
94586eb1 |
|
17-Feb-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add a new theorem to WORD_EXTRACT_ss.
|
#
dcdc5fd7 |
|
16-Feb-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Better pretty-printing for n2w, e.g. will now print as ``(32w:bool[32])`` when show types is on. Also fix a few things that were picked up by Thomas' new sanity checking tool.
|
#
4d30253a |
|
02-Feb-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Some more lemmas. Also, tweak to word cast pretty-printer.
|
#
f076ad04 |
|
31-Jan-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix bug in changes to wordsLib.WORD_DP.
|
#
a70b492a |
|
31-Jan-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Some changes to wordsLib.WORD_DP. It now takes a pre-processing conversion and is able to prove goals such as ``w2w (w:word4) : word8 <=+ 16w``.
|
#
d526c280 |
|
25-Jan-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Improve word cast pretty-printer and make it cover sw2sw too.
|
#
a56428c6 |
|
20-Jan-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Evaluation wasn't working for fcp index 0.
|
#
58f60751 |
|
20-Jan-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add evaluation support for FCP index and update. This has required fixing a problem with the evaluation of EL, namely EVAL ``EL i x`` didn't terminate.
|
#
1d7d7675 |
|
07-Jan-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Modification to WORD_BIT_EQ_ss to avoid inefficiency in ARITH_ss -- ``n2w n`` is no long expanded out. Instead, it is expected that this fragment will be used in combination with srw_ss() where ``(n2w n) ' i`` can be evaluated on ground instances. Also rewrites |-> named_rewrites to avoid "anonymous" fragment names.
|
#
918698b7 |
|
11-Dec-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add evaluation for bit update.
|
#
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.
|
#
c0cee1d3 |
|
08-Dec-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add word_xnor, word_nand and word_nor.
|
#
ec7b6e45 |
|
04-Dec-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add operation bit_field_insert. The term ``bit_field_insert h l a w`` expresses "w[h:l] <- a".
|
#
0c9baeb3 |
|
02-Dec-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Oops.
|
#
182c237a |
|
02-Dec-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add word_replicate support to WORD_EXTRACT_ss and WORD_BIT_EQ_ss.
|
#
c0e5bd4e |
|
02-Dec-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Two more new operations: * word_replicate n w. Replicates word "n" times. * concat_word_list l. Concatenates a list of words. Both are supported by wordsLib.guess_lengths. For example: ``concat_word_list [x1;x2;x3:word8]`` ``word_replicate 3 (x:word8)`` will both be given length 24. The code for guess_lengths has been completely rewritten -- it's now more general and much simpler. This change does have the potential to break theories (due to different guesses being made) but this is unlikely.
|
#
9bd966c2 |
|
02-Dec-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add a few new operations: * word_reduce op w. Does a bitwise left fold using "op". For example: w = n2w 0b[x1x2x3...xn] |-> n2w 0b[x1 op x2 op x3 op ... op xn] : word1 This has been specialised to reduce_{or,and,xor,nand,nor,xnor}, which occur in Verilog. * add_with_carry (a,b,c). Sums "a" and "b" with carry-in "c". Result is: (sum,carry-out,overflow). The words compset, simpset and emit ML code have been updated.
|
#
277e5140 |
|
27-Nov-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add ground-term evaluation for fcp_index to the words simpset. Also prevent non-termination when the index is too large, e.g. EVAL ``(14w:word4) ' 8`` is okay now.
|
#
db504a6a |
|
19-Nov-2009 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Added styles to the pretty-printer. The recent changes to the pretty-printer use colours to convey extra information about terms and types as they are printed. This is done via annotations containing semantic information. For example, an annotation states that some string represents a variable of some type. It's then up to the backend how to use this extra information for displaying. This checkin adds a concept of "styles". In contrast to annotations, styles express formating instructions. A style states instructions like: "print the following in red and bold". There are two new function: begin_style style_list and end_style. Everything that is outputted between calls of these functions, should be formated in the given style. There are the following styles available: Setting the foreground color to c: FG c Setting the background color to c: BG c Use bold font: Bold Underline text: Underline begin_style takes a list of these styles. Thereby, the colors c can be choosen from a standard 16 color palette: Black, RedBrown, Green, BrownGreen, DarkBlue, Purple, BlueGreen, DarkGrey, LightGrey, OrangeRed, VividGreen, Yellow, Blue, PinkPurple, LightBlue, White In order to provide begin_style and end_style to user defined pretty-printers, the interface of userprinter had to be extended. Instead of getting two functions add_string and add_break, the userprinter now gets a record of a lot of different functions. Old pretty printers have to be adapted by changing fun myprint Gs (sys,str,brk) gravs d pps t = let open Portable term_pp_types ... to fun myprint Gs sys (ppfns:term_pp_types.ppstream_funs) gravs d pps t = let open Portable term_pp_types val (str,brk) = (#add_string ppfns, #add_break ppfns); ... If you want all the functions, you can use fun myprint Gs sys (ppfns:term_pp_types.ppstream_funs) gravs d pps t = let open Portable term_pp_types val {add_string,add_break,begin_block,end_block,add_ann_string,add_newline,begin_style,end_style,...} = ppfns ...
|
#
2c23354d |
|
12-Nov-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix problem with simplification of ``1w : bool[unit]``.
|
#
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!
|
#
2aeb703e |
|
01-Aug-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Prevent evaluation of ``word_log2 0w``.
|
#
7376891c |
|
21-Jul-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Eliminate some occurrences of "handle _".
|
#
3f71a7d7 |
|
18-Jun-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added a (fairly crude) printer for showing the types of ><, w2w and @@. Invoked with wordsLib.add_word_cast_printer() and turned off with wordsLib.remove_word_cast_printer()
|
#
9f6d2d04 |
|
27-May-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added a new word operation "word_signed_bits" with symbol "---". Also added a new theorem WORD_ADD_BIT.
|
#
c7985b41 |
|
01-Apr-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added word_mod and the theorem WORD_DIVISION (from Magnus). Also made some tweaks in wordsLib: guess_word_lengths is a tad smarter (although still fairly naive); WORD_DECIDE now raises HOL_ERR instead of UNCHANGED; and evaluation is improved for sw2sw and word_2comp.
|
#
64b574d6 |
|
27-Feb-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Block evaluation of word_concat, except on ``n2w n @@ n2w m`` when wordsLib is loaded.
|
#
701f93ea |
|
24-Feb-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added wordsLib.dest_word_literal : term -> Arbnum.num Also ensure "/" is affected by deprecate_word and prefer_word.
|
#
d653fb1c |
|
11-Feb-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implement unary minus (the old ~ still also works). Selftest level 2 passes. Changes in the "words world" were replacing $- with -. In the two quotient changes, I made sure that the infix operator that used the - character was part of the grammar before it was parsed. This is necessary because - is now a non-aggregating character, mainly so that ``--p`` parses as three tokens, not two. Of course, if you added -- to your grammar, then it would go back to parsing as two.
|
#
8654de63 |
|
07-Feb-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Attempt to tidy up (fix) EmitML and finish off the transition that Scott started. EmitML has been moved to the end of the build sequence. "Hooks" have been eliminated and all EmitML related stuff has been removed from the various theory directories. All code for generating ML/Caml is now self-contained within src/emit. I've not tested the generated Caml code but the SML seems to build fine. The directories: src/theoryML src/theoryOcaml src/emitScript have been replaced by src/emit/theories/ML src/emit/theories/Caml src/emit/theories
|
#
3faf4042 |
|
13-Jan-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
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
|
#
f46cf548 |
|
25-Nov-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added some definitions for EmitML (words and stings).
|
#
1095191e |
|
24-Nov-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Recast strings as lists of characters. The type :string is now an alias for :char list. The old constant names (STRCAT, STRLEN, STRING, EMPTYSTRING) are retained, but they are now just parsing/printing forms for (APPEND, LENGTH, CONS and NIL). String literals still work. For the moment, the string names are also preferred when printing, though I think there's a case for just printing with the list names. (Of course, the list names are used when the arguments are not of type :char list.)
|
#
6ae78cde |
|
17-Nov-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add integer operations to EmitML.
|
#
658935a1 |
|
25-Oct-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add function LOWEST_SET_BIT to bitTheory.
|
#
a6ecbd7a |
|
14-Oct-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Modify the ability to add user-printers so that they're keyed off term-matches (using first order term-matching). Also give the user's function access to the relevant grammars, and to the "smart" add_string and add_break functions that the system printer uses itself to avoid symbol merging.
|
#
47598937 |
|
28-Aug-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
A missing rewrite was causing problems for WORD_DECIDE. Also some minor changes with regard to the code generated with EmitML.
|
#
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.
|
#
440c80fa |
|
27-Jul-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Provide evaluation for MOD_2EXP_EQ in the words compset.
|
#
2284fe46 |
|
23-Jun-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor update to the evaluation of BIT.
|
#
06c08222 |
|
19-Jun-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added "string, list <-> num, word" conversions: s2n, s2w, l2n, l2w, n2s, w2s, n2l and w2l. These have been instantiated for bases 2, 8, 10 and 16 e.g. word_to_hex_string and word_from_hex_string. Evaluation is efficient for the bases 2, 8 and 16. Have added evaluation of ``LOG m n`` to words_compset and also ensured that WORD_ss does more ground term evaluation e.g. - SIMP_CONV (srw_ss()) [] ``BITWISE 10 $\/ 4 8``; > val it = |- BITWISE 10 $\/ 4 8 = 12 : thm
|
#
4e84f491 |
|
27-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor bug fix.
|
#
8feeb7a4 |
|
20-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix WORD_DECIDE_TAC. Also make the library less susceptible to load errors i.e. following calls to remove_ovl_mapping and defining constants with variable-like names.
|
#
4b42018c |
|
15-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Replace occurrences of failwith.
|
#
4e56be08 |
|
16-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Make word equality testing work for the special literal ``$- 1w``.
|
#
f8b13784 |
|
15-May-2008 |
Konrad Slind <konrad.slind@gmail.com> |
Definitions like (f 0w = T) /\ (f 23w = F) /\ (f 12w = F) now work. Also improved the performance of basic equality conversions between literals (char_EQ_CONV, string_EQ_CONV, NEQ_CONV, and word_EQ_CONV) in the case where the involved literals are actually equal. Now trying to figure out how to teach REDUCE_CONV and EVAL about this.
|
#
d8a63927 |
|
15-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add word_EQ_CONV to the_compset and signature.
|
#
cfc59257 |
|
15-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Make sure word_EQ_CONV fails on unchanged.
|
#
3bc77b82 |
|
15-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add word_EQ_CONV.
|
#
5449fad7 |
|
12-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Make use of WORDS_EMIT_RULE.
|
#
8eeeebdd |
|
13-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added some extra functions under EmitML e.g. toWord32 and fromString32. Made fcpLib.index_to_num more robust. It can now cope with sum types. Added Cases_word_value and Cases_on_word_value. These do case splitting on the numeric value of a word.
|
#
480fc0cf |
|
12-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Suppress messages.
|
#
e41c22a5 |
|
12-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added simplification for exclusive-or. Also sped up evaluation of word equality (now checks one bit at a time and so can break early).
|
#
95ce9bd9 |
|
01-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added a new theorem and fixed a bug in the pretty-printer (was raising an Option exception on ``n2w n : bool['a+'b]``).
|
#
d4b1b2cc |
|
25-Apr-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
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".
|
#
6e25f443 |
|
21-Apr-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added wordsTheory.WORD_INDUCT. This can be used with wordsLib.Induct_word. Added WORD_DECIDE_TAC and made some changes to WORD_DECIDE (to handle terms with quantifiers). Made changes to SIZES_CONV for faster evaluation of ``dimword(:N)`` etc. (Was slow for large N.) Dropped wordsLib.WORD_GROUND_ss -- this is contained within srw_ss() and WORD_ss.
|
#
6236d936 |
|
29-Mar-2008 |
Konrad Slind <konrad.slind@gmail.com> |
Made notion of literal extensible. This allows word literals to be used in pattern-matching, as is done in Anthony's ARM stuff.
|
#
4a69b08d |
|
18-Feb-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Extended WORD_DECIDE to cover orderings of the form ``a + n2w n <+ a``.
|
#
0e672343 |
|
18-Jan-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Have made some tweaks to WORD_ss and added it to srw_ss().
|
#
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.
|
#
2019405b |
|
08-Nov-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added unary $- to the list of preferred or deprecated word operations.
|
#
995bd661 |
|
01-Nov-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added parsing preferences for words (prefer_word and deprecate_word).
|
#
5b702870 |
|
01-Nov-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Changed SIZES_ss - now uses SIZES_CONV.
|
#
49c39b75 |
|
11-Jul-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Ensures word literal case statments work under EmitML.
|
#
f45d90bd |
|
19-Jun-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added one new theorem. Some other minor changes too.
|
#
c1d87db6 |
|
12-Jun-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fixed bug with the evaluation of ``dimword(:'a+'b)`` and, in turn, ``a @@ b``. Also generalised a pair of theorems.
|
#
b2db99ef |
|
07-May-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added some new theorems - mostly to do with word extraction.
|
#
58708f5c |
|
20-Mar-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added call to guess_fcp_lengths in wordsLib.guess_lengths.
|
#
90b87cf3 |
|
20-Mar-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added a top-level function for turning on word length guessing i.e. it is invoked with val _ = wordsLib.guess_lengths() This ensures that existing post_process_term functionality isn't bypassed.
|
#
b1a5f678 |
|
19-Mar-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Post processing for word parsing is supported with the function: wordsLib.guess_word_lengths : term -> term This was requested by Joe Hurd. When possible, word lengths are guessed for the extract and concatenate functions. That is, ``(a >< b) w`` is given type ``: (a + 1 - b) word`` and ``(a: a word) @@ (b: b word)`` is given type ``: (a + b) word``. For example: - val _ = Parse.post_process_term := wordsLib.guess_word_lengths; - ``(3 >< 0) a @@ (7 >< 4) a @@ (16 >< 8) a``; <<HOL message: inventing new type variable names: 'a, 'b, 'c, 'd, 'e, 'f>> <<HOL message: assigning word length(s): 'a <- 4, 'b <- 13, 'c <- 17, 'e <- 4 and 'f <- 9>> > val it = ``(3 >< 0) a @@ (7 >< 4) a @@ (16 >< 8) a`` : term The assignment message is controlled by the trace variable "notify word length guesses".
|
#
95b7103d |
|
02-Mar-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added a rule for use with EmitML i.e. when emitting a definition "th" (containing word operations), you need: EmitML.DEFN (wordsLib.WORDS_EMIT_RULE th)
|
#
34b70215 |
|
19-Feb-2007 |
James Reynolds <jr291@cam.ac.uk> |
DIV_2EXP and TIMES_2EXP now use a strict version of FUNPOW which is approximately 3x faster
|
#
2b95b12e |
|
09-Feb-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Make INDEX_CONV work with sum types.
|
#
db890776 |
|
23-Jan-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
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
|
#
737c356a |
|
11-Dec-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added theorem INT_MIN_SUM, which supports evaluation for word concatenation.
|
#
9d26d3e8 |
|
08-Sep-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Decided to replace the word case tactics with ranged versions.
|
#
bea43d5f |
|
07-Sep-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added theorem word_1_n2w, and tactics Cases_on_word_ranged and Cases_word_ranged.
|
#
f9f161ef |
|
04-Sep-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added WORD_EQ_SUB_ZERO and fixed glitch with WORD_HIGHER not being stored.
|
#
a31e02f5 |
|
27-Jul-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Some minor changes to the code generated by EmitML. DIV_2EXP is moved to arithmeticTheory, so that is can be included in numML. Added theoryML/mlton/numML.sml, which supports fast arithmetic when using MLton.
|
#
32eaeec4 |
|
04-Jul-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add reduction of DIV2 and MOD_2EXP to num compset and standard simpsets.
|
#
acee2670 |
|
30-Jun-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Moved DIV2 and MOD_2EXP to arithmeticTheory. This enables the numML.num data type (wrt EmitML) to be abstract -- without the big slowdown caused by the lack of numeral versions of these functions when running the ML.
|
#
c09ec44d |
|
14-Jun-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Apologies, have done some renaming: TOP -> dimword MSB -> INT_MIN Also added UINT_MAX and INT_MAX. word_L, word_H and word_T have been overloaded with INT_MINw, INT_MAXw and UINT_MAXw.
|
#
212a13a6 |
|
07-Jun-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Some rationalisation with the use of computeLib.auto_import_definitions. Also, TOP and MSB are computed, saved and added to the compsets for the standard word sizes.
|
#
127eb546 |
|
06-Jun-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Using Define for dimindex mucks up evaluation. Added TOP_def to the SIZES_ss fragment and the evaluation compsets.
|
#
9049a2aa |
|
28-Mar-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Having both mk_index_type_thm and mk_index_type is probably unnecessary.
|
#
6bac7473 |
|
15-Mar-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added case for rotate by zero.
|
#
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.
|
#
c4e9aa47 |
|
01-Mar-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Allow pretty-printing of words in different number bases.
|
#
cba9d2c7 |
|
01-Mar-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
The word_modify function can be used to evaluate FCP bindings.
|
#
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).
|
#
f4affa25 |
|
04-Jan-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Renamed wordsLib.mk_word_type to wordsLib.mk_word_size to avoid the name clash with wordsSyntax.mk_word_type
|
#
da919e3f |
|
10-Nov-2005 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Made some changes and fixes for evaluation: "+" and "*" now do a "MOD" e.g. - EVAL ``(5w:word4) + 12w``; > val it = |- 5w + 12w = 1w : thm instead of giving the less helpful ``17w:word4``.
|
#
b505ecfa |
|
01-Nov-2005 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added evaluation for the index operator %%.
|
#
6bccae62 |
|
31-Oct-2005 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added a few more helpful theorems.
|
#
300a7311 |
|
11-Oct-2005 |
Konrad Slind <konrad.slind@gmail.com> |
word_or renamed to !!.
|
#
0c03ff5c |
|
01-Oct-2005 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Have eliminated machine_wordsTheory - the standard word sizes are now provided in wordsTheory.
|
#
70a7f15a |
|
01-Oct-2005 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
* 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).
|
#
6752f613 |
|
23-Sep-2005 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Have added the word "Case" tactics to wordsLib. Also added some theorems - in particular, a few for reasoning about w2w and word_bits.
|
#
80adb28b |
|
21-Sep-2005 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
The standard word sizes are now provided in machine_wordsTheory - previously they could be loaded with machine_wordsLib, but then the type theorems weren't saved in a proper theory.
|
#
81dc454d |
|
21-Sep-2005 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
After selecting a bit range, one typically wishes to map to a new word size. The operator (h >< l) facilitates this. Also noticed that word_lsb was being saved as word_msb, and it wasn't added to the compset.
|
#
6b37d52f |
|
21-Sep-2005 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
The function (word_modify f) takes a word w and sets each bit such that: w[i] := f i w[i]. Works with EVAL e.g. - EVAL ``word_modify (\i b. 3 < i) 0w:word8 = 0b11110000w``; > val it = |- (word_modify (\i b. 3 < i) 0w = 240w) = T : thm
|
#
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.
|