#
b4b8e85c |
|
18-Aug-2018 |
Andreas Lööw <AndreasLoow@users.noreply.github.com> |
Don't export ERR from HolKernel
|
#
bb3db6ce |
|
25-Mar-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor clean up of fcpLib.
|
#
20561d78 |
|
20-Mar-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Clean up of fcpTheory. Also added a few new constants. The new constants are: FCP_CONCAT, FCP_ZIP and FCP_FOLD. The definition of V2L has changed — avoiding the unnecessary use of Hilbert choice. Also removed the sub1 type constructor. These were introduced in 102792de.
|
#
c16f1645 |
|
27-Nov-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor bug fix.
|
#
d9777034 |
|
25-Oct-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add fcpSyntax and tidy up related code.
|
#
3b70a2bc |
|
10-Dec-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Avoid possible non-termination with FCP length guessing, e.g. ``L2V [T;T] : word3`` wasn't terminating. Should possibly give a warning if such cases are detected.
|
#
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.
|
#
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
|
#
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.
|
#
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.
|
#
5959b139 |
|
27-Jun-2007 |
Konrad Slind <konrad.slind@gmail.com> |
Trivial change to get rid of "Guessing type variable ..." style mesg when this library loads.
|
#
afa43e48 |
|
20-Mar-2007 |
Joe Hurd <joe@gilith.com> |
Added type guessing for L2V
|
#
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
|
#
44f68827 |
|
17-Jan-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Second go at changing the scheme for index types. The new scheme uses: ``:one``, ``:'a bit0``, and ``:'a bit1``. For example, ``:i18`` is ``:one bit0 bit0 bit1 bit0``. The EmitML code is more like the original version i.e. the performance loss is avoided.
|
#
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...
|
#
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.
|
#
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.
|
#
56d1401a |
|
27-Mar-2006 |
Jianjun Duan <jjduan@cs.utah.edu> |
add mk_index_type_thm ines beginning with `CVS:' are removed automatically
|
#
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).
|
#
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.
|