#
b4b8e85c |
|
18-Aug-2018 |
Andreas Lööw <AndreasLoow@users.noreply.github.com> |
Don't export ERR from HolKernel
|
#
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).
|
#
55622e44 |
|
24-Apr-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get core HOL to build with new definition of "by" Progress with github issue #407
|
#
fa30bf2b |
|
04-Dec-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Improve/add some word theorems.
|
#
f9f2c8a1 |
|
16-Nov-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Simplification theorems for wordsTheory and integer_wordTheory.
|
#
4a0d8598 |
|
08-Sep-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Set grammar ancestries in fcp and word theories These are test cases for the new machinery
|
#
a0d0d124 |
|
28-Jul-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix wordsScript in light of pat_assum rename One interesting case requires a more specific pattern than earlier because a purely general pattern has the parser guessing the wrong addition-constant when the pattern looks to general (and this happens before any matching is attempted). I want to deal with this situation by having the parse-in-context primitives try all possible parses when generating patterns.
|
#
9777de8e |
|
15-Jun-2016 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
New rewrites for word_bits/word_extract. Thm word_extract_w2w_mask generalises word_extract_mask to the case where the extracted word isn't of the same type as the original. Helps make decompiler's exporter more general.
|
#
f5c45e4d |
|
03-May-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add word theorem from CakeML.
|
#
ad24df64 |
|
19-Apr-2016 |
Ramana Kumar <ramana@member.fsf.org> |
Remove unnecessary qualified calls to things in Theory These are re-exported by HolKernel anyway, and we want to rebind HolKernel for proof-recording purposes.
|
#
e8457c3a |
|
23-Mar-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add Theory.quote_adjoin_to_theory. Use this in llistTheory. This should close #304. This has been implemented using a new function Portable.quote_to_string_list. Other uses of adjoin_to_theory under src/ have been updated.
|
#
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.
|
#
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.
|
#
07421c10 |
|
03-Jul-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add a small theory about address alignment. This will eventually be used to rationalise examples in l3-machine-code/.
|
#
e5d9a24e |
|
17-Feb-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Remove some non-ASCII characters (Unicode subtractions in this case)
|
#
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.
|
#
3aa000c4 |
|
04-Mar-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Remove a side-condition from n2w_DIV.
|
#
1ccf4f99 |
|
15-Feb-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add w2n_minus1 theorem.
|
#
8c27fb3e |
|
08-Feb-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add theorem word_extract_mask.
|
#
1ee7f40d |
|
14-Oct-2012 |
Michael Norrish <michael.norrish@nicta.com.au> |
Delete trailing whitespace in src and examples.
|
#
ca964e05 |
|
08-Oct-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Some theorems concerning bit_count.
|
#
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.
|
#
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
|
#
78e66da8 |
|
06-Aug-2012 |
Magnus Myreen <magnus.myreen@gmail.com> |
Added lemma about word_reverse
|
#
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.
|
#
5b587535 |
|
26-Jun-2012 |
Konrad Slind <konrad.slind@gmail.com> |
Allow "non-datatypes" in TypeBase to have optional induction thm. Provide appropriate values for this field for finite sets, strings, integers, finite maps and words.
|
#
d4471915 |
|
30-May-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add a new theorem about bit-vector overflow. Includes an improvement to the Cases_on_i2w tactic.
|
#
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.
|
#
788cc263 |
|
16-Mar-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Save helpful theorem.
|
#
04de767e |
|
12-Mar-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add min and max operations to wordsTheory.
|
#
0cccf12f |
|
26-Sep-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
The old `!!` symbol was accidentally dropped. For now it's being kept for compatibility reasons.
|
#
a2328149 |
|
23-Sep-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.
|
#
845531b5 |
|
14-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove trailing whitespace in source files.
|
#
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
|
#
dbee7d85 |
|
17-Jun-2011 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Changed the definition of word_smod (again), to match Clark Barrett's update to the definition of bvsmod in SMT-LIB from 14 June, 2011.
|
#
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.
|
#
62627d47 |
|
01-Jun-2011 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Changed the definition of word_smod to be equivalent to SMT-LIB's bvsmod.
|
#
1a32829e |
|
11-Apr-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add theorem word_shift_bv.
|
#
08369277 |
|
04-Apr-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
A few extra theorems.
|
#
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.
|
#
b956e730 |
|
16-Mar-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add word_sign_extend operator.
|
#
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.
|
#
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
|
#
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.
|
#
7a3f0cb6 |
|
17-Sep-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add theorem WORD_MODIFY_BIT + other minor changes.
|
#
df8228ab |
|
05-May-2010 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Added a theorem relating xor and add.
|
#
18e66b0f |
|
21-Apr-2010 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Remove unnecessary antecedent to a theorem.
|
#
2357de9b |
|
20-Apr-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Remove unnecessary antecedent to a theorem.
|
#
b727df86 |
|
21-Apr-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added some new theorems that help when reasoning about word concatenation.
|
#
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.
|
#
8bdde93f |
|
25-Mar-2010 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Added a type ``:word1`` of 1-bit words. (:word1 abbreviates :bool[unit], and hence is equivalent to :bool semantically.)
|
#
1c223f08 |
|
20-Mar-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Move more TeX-notations out of EmitTeX and into their 'home' theories. Next step will be to completely remove the remaining entries in EmitTeX's string_map.
|
#
46d9a7b6 |
|
01-Mar-2010 |
Ramana Kumar <ramana.kumar@gmail.com> |
Fixed another proof broken by automatic LIST_EQ_SIMP_ss.
|
#
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.
|
#
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``.
|
#
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".
|
#
9a8b0830 |
|
03-Dec-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Turn some implications into equalities, so that they can be used as rewrites. (As suggested by Michael.)
|
#
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.
|
#
b52a1779 |
|
11-Nov-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Bind a bunch of free variables.
|
#
47519c9e |
|
01-Oct-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Despite Michael's best efforts, have decided to replace word slice "<>" with "''". Apologies for any inconvenience caused.
|
#
52bbe051 |
|
02-Oct-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make the interface supported by Unicode slightly richer so that I can make the Unicode not-equals not overlap entirely with <>, thereby allowing <> to be used both for word_slice and for not-equals, without it inheriting the \neq symbol when Unicode is on.
|
#
2eddf2db |
|
30-Sep-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Make sure that word slice "<>" does not print as ≠.
|
#
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!
|
#
359c7e8f |
|
05-Aug-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Added two theorems to wordsTheory. The first theorem states that all sets of n-bit words are finite: |- !s:'a word set. FINITE s The second theorem states that one can induct on any set of n-bit words (an immediate consequence of the first theorem): |- !P. P {} /\ (!s. P s ==> !e. e NOTIN s ==> P (e INSERT s)) ==> !s. P s
|
#
15c5338d |
|
16-Jun-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added new theorems: WORD_EXTRACT_OVER_ADD and some for addition/subtraction wrt integer_word$i2w.
|
#
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.
|
#
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
|
#
2fbb9b76 |
|
14-Jan-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Let "not equals" take priority over "word slice" for the overloading "<>".
|
#
a642994f |
|
27-Nov-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix for a bug found by Anthony, caused by syntactic patterns not getting their pretype variables assigned properly during inference. Also adjust wordsScript to remove its change to <>'s precedence, and adjust the other operators in the same place (-- and ><) to use set_fixity rather than add_infix. The advantage of set_fixity is that it removes other rules for the same token. This avoids complaints about grammar ambiguity. Calls to add_infix can result in multiple rules for the same token through the grammar. So, Anthony, if you really wants <> back at original level, please put it there with set_fixity. Users inheriting wordsTheory can then cope with <> having a different precedence from elsewhere.
|
#
d9003833 |
|
26-Nov-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fairly dramatic change, supporting the use of "syntactic patterns". It is now possible to overload a name to term (typically a lambda-abstraction) in order to create syntax-only definitions. For example, there is a definition of not-equals now in the system: val _ = overload_on ("<>", ``\x y. ~(x = y)``) val _ = set_fixity "<>" (Infix(NONASSOC, 450)) This definition is parsed and pretty-printed. Two other annoying changes. The interface for adding unicode variants has changed, and I have made precedence level 450 of the parser non-associative. This latter change has caused most of the (minor) adjustments to the files below. The regression test doesn't go through yet. (Currently there is a failure in quotient/examples/sigma that I don't understand.)
|
#
6ae78cde |
|
17-Nov-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add integer operations to EmitML.
|
#
effc431b |
|
01-Oct-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Change export_rewrites back to its old API (without requiring an extra string). When exported, the resulting simpset fragment always picked up the name of the theory to be the base of its name, so there didn't seem much point in giving users a false impression of naming power.
|
#
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.
|
#
77687ebf |
|
26-Aug-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Another fix to the way Unicode-overloading works. It now checks to see if the term you are overloading to has an ASCII concrete syntax. (For example, integer$int_le has an ASCII concrete syntax of <= as an infix.) If so, it will set up the Unicode symbol as an alias for that concrete syntax. This means that subsequent overloads on the same ASCII symbol will also pick up the Unicode symbol. Graphically, we have something like x <= y +----- arithmetic$<= \ | >---> COMB(COMB(<=,x),y) >---+----- integer$int_le / | x ≤ y +----- words$word_le | ... etc where the middle column is the result of Absyn applied to the given quotation.
|
#
a1436e90 |
|
23-Aug-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix some problems identified by Anthony, and ensure that when Unicode is turned back off, that old overloads are properly restored. Still not totally happy with the interface; once <= is identified with UChar.leq, perhaps that should just happen for all the constants that are overloaded to <=.
|
#
aed05f4e |
|
20-Jul-2008 |
Konrad Slind <konrad.slind@gmail.com> |
A whole mess of small changes intended at making simpsets prettyprint informatively in the interactive loop. Very possibly I haven't updated all the files in the examples directories.
|
#
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
|
#
c2f88483 |
|
21-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Restore printing of numeral types prior to exporting the theory.
|
#
11f29b21 |
|
17-May-2008 |
Konrad Slind <konrad.slind@gmail.com> |
Added simple rewrite rule.
|
#
4e56be08 |
|
16-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Make word equality testing work for the special literal ``$- 1w``.
|
#
3bc77b82 |
|
15-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add word_EQ_CONV.
|
#
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.
|
#
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]``).
|
#
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.
|
#
d080e6cd |
|
19-Mar-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Have rationalised the treatment cases for words, changing word_nchotomy to ranged_word_nchotomy. This means that "Cases" and "Cases_on" now subsume "wordsLib.Cases_word" and "wordsLib.Cases_on_word". Have eliminated some occurrences of the latter.
|
#
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``.
|
#
44d99bb3 |
|
24-Jan-2008 |
Peter Homeier <palantir@trustworthytools.com> |
Revised expressions of the form <term>:<type> ' <term> to be (<term><type>) ' <term> to avoid confusion with the type variable ' .
|
#
6c5d8404 |
|
17-Jan-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Changed the standard symbol for fcp$index, from %% to '. The old symbol can still be used, so existing code shouldn't break.
|
#
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.
|
#
2e60beb1 |
|
12-Oct-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
A couple more theorems.
|
#
2f5f5719 |
|
28-Aug-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Turns off bracket syntax for array types when using EmitML.
|
#
87e1af9f |
|
23-Aug-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Removed references to ``:bool ** 'a`` in wordsScript.sml
|
#
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.
|
#
af813f41 |
|
15-May-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added some theorems for sw2sw (signed word conversion) and #<< (rotate left).
|
#
b2db99ef |
|
07-May-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added some new theorems - mostly to do with word extraction.
|
#
b5d0edd6 |
|
03-May-2007 |
Konrad Slind <konrad.slind@gmail.com> |
Added support for termination proofs for recursions on words. Mechanism knows about subtracting 1 and also right shifting.
|
#
187644f1 |
|
28-Apr-2007 |
Konrad Slind <konrad.slind@gmail.com> |
Getting simple termination proofs for recursions on words to work.
|
#
a0e83ef9 |
|
26-Apr-2007 |
Konrad Slind <konrad.slind@gmail.com> |
Added code to make installation of n2w_itself in ConstMap persistent.
|
#
dd370bc7 |
|
12-Apr-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added one new theorem.
|
#
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)
|
#
122b778a |
|
06-Feb-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Moved the function substitution operation (:-) to standard part of the distribution. substTheory.SUBST_EVAL: |- !f a b c. (a :- b) f c = (if a = c then b else f c) A couple of theorems have been renamed in the process: SUBST_EQ2 -> SUBST_IMP_ID SUBST_EQ3 -> SUBST_ID Likewise renamed these theorems for FCP substitution (:+).
|
#
1f327341 |
|
01-Feb-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added a substitute operation :+ for FCPs. Also made EmitML work with numeric types e.g. ``:2`` gets the ML type "unit bit0".
|
#
3331a1b2 |
|
29-Jan-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
A cleaner solution for emitting ML code for Finite Cartesian Products. The ``:'a itself`` type is given a type constructor "ITSELF n" in ML, where "n" is the dimindex size of ``:'a``.
|
#
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
|
#
cf00641c |
|
23-Dec-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Updated the code for handling words using EmitML -- now works with the new index type construction (i.e. using :bool # 'a and :'a option). The code is slower (by about 30%) - probably due to the less compact representation of the index type.
|
#
3b931fc5 |
|
20-Dec-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Have changed the way that index types are created. The new scheme uses a canonical form, with ``:bool # 'a`` used to double the index size and ``:'a option`` used to increment it. The index type is generated by a new function fcpLib.index_type; for example: - fcpLib.index_type 5; > val it = ``:(bool # bool) option`` : hol_type The function fcpLib.mk_index_type performs roughly as it did before, however, a type abbreviation is now used for the index type. These abbreviations are printed for indexes > 8. For example: - fcpLib.mk_index_type 5; > val it = (|- FINITE UNIV, |- CARD UNIV = 5, |- dimindex (:(bool # bool) option) = 5) : thm * thm * thm - ``:i5``; > val it = ``:(bool # bool) option`` : hol_type - fcpLib.mk_index_type 30; > val it = (|- FINITE UNIV, |- CARD UNIV = 30, |- dimindex (:i30) = 30) : thm * thm * thm It is not expected that these changes will break anything...
|
#
22a60ba5 |
|
14-Dec-2006 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Added some theorems under "Support for termination proofs".
|
#
737c356a |
|
11-Dec-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added theorem INT_MIN_SUM, which supports evaluation for word concatenation.
|
#
17bd7905 |
|
09-Oct-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fixed EmitML code for the n-bit library.
|
#
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.
|
#
bbc18a37 |
|
23-Aug-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added a theorem about concatenating sub-words.
|
#
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.
|
#
ed7c2be6 |
|
14-Jul-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Some changes to make wordsML work with MLton.
|
#
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.
|
#
36cf23d3 |
|
28-Jun-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added word_eq.
|
#
5c8f5906 |
|
22-Jun-2006 |
Konrad Slind <konrad.slind@gmail.com> |
Minor changes and bugfixes to ML code generation. Have renamed EmitML.exportML to EmitML.emitML, since exportML is used in SML/NJ to dump the image. Also renamed Globals.exportMLPath to Globals.emitMLDir (since it's a directory and not a path). Also fixed bug in code generated for constructors and tuples.
|
#
e64acbf9 |
|
22-Jun-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fixed bug in EmitML's printing of constructor arguments.
|
#
7a2bd1d1 |
|
21-Jun-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Export the n-bit words library with EmitML.
|
#
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.
|
#
c64ec72f |
|
05-Jun-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Alter the n-bit word theories to use the :'a itself type, and also add new constants (TOP(:'a) and MSB(:'a)) to stand for the numeric value of 2 ** width, and 2 ** (width - 1). Using these makes the expression of several results a lot nicer. As the updated proofs in integer_wordScript demonstrate, you don't always have to expand these definitions either, which is nice. I'm not 100% sure that these are the best names for these constants.
|
#
6b36ae74 |
|
25-May-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Export some more rewrites for srw_ss, and prove a new theorem about the numeric meaning of a word's msb being set.
|
#
a7abb380 |
|
17-May-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add more aggressive simplification of terms involving EXP (natural number exponentiation). This affects the behaviour both of std_ss and srw_ss(). Various proofs break, so I've fixed these.
|
#
8b02730b |
|
15-May-2006 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added the obvious type abbreviation for words e.g. i32 word for bool ** i32.
|
#
42af083c |
|
09-Apr-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
A minor new theorem.
|
#
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.
|
#
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).
|
#
d8e57a78 |
|
16-Feb-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add more aggressive normalisation of multiplicative expressions to ARITH_ss. Also provide old_arith_ss values for scripts that don't want this new behaviour. Update proofs to go through again. Some should be a bit more robust in the face of future changes to arith_ss. Others just punt and refer to old_arith_ss.
|
#
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
|
#
87d811e7 |
|
03-Nov-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Moved a whole bunch of "obvious" arithmetic rewrites into std_ss. This simpset already does arithmetic on ground terms (2 + 3 = 5, sort of thing), and it seems silly to have it not prove 0 <= x, and other simple things like this. The change does break some proofs, which I have fixed.
|
#
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.
|
#
cf735afb |
|
11-Oct-2005 |
Konrad Slind <konrad.slind@gmail.com> |
Removed idiotic debugging messages.
|
#
300a7311 |
|
11-Oct-2005 |
Konrad Slind <konrad.slind@gmail.com> |
word_or renamed to !!.
|
#
2ce35441 |
|
06-Oct-2005 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Changed the definition of concat. The new definition should be slightly easier to work with.
|
#
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).
|
#
40200f63 |
|
23-Sep-2005 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Just added a theorem that was already there under another name.
|
#
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.
|
#
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
|
#
76dfff0f |
|
19-Sep-2005 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Changed theorem word_asr_n2w - the new version has a much simpler proof.
|
#
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.
|