Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Message-Id: <9204131525.AA14974@easynet.crl.dec.com>
Date: Mon, 13 Apr 92 11:25:04 EDT
From: "Tim Leonard, DTN 225-5809, HLO2-3/C11 13-Apr-1992 1126" <leonard@com.dec.enet.ricks>
To: info-hol@edu.uidaho.cs.ted
Apparently-To: info-hol@ted.cs.uidaho.edu
Subject: A wordn library.

Mike Gordon tells me that Wei Wong is working on the wordn routines.  (Please
correct me if I've spelled your name wrong, Wei.)  Since I'm using an old
version of wordn, and I've added a couple of things to it, Mike suggested that
I talk to Wei about what features I'd find useful.  It occurs to me that lots
of other people will likely use a wordn library, so I decided instead to open
the discussion to info-hol.

Here's the list of features I'd like in a wordn library:

  o Allow datatypes to be named something other than word<n>.  For example,
    I use ": word1", but I call it ": bit", and I use ": word8", but I call
    it ": byte".  Since different users will want to use different names, the
    names should be supplied by the user.  I changed the wordn code to allow
    the user to supply a name.  (I'd guess this would be much better done as
    part of abstract theories, but that's way beyond me.)  The change was
    trivial except that now there isn't a canonical name for the conversion
    routines, which is a slight pain.

  o Support both big-endian and little-endian operations.  Some people number
    bits from left to right (big endians), and some number bits right to left
    (little endians).  The library should support both ways of doing things.
    Since it's rare for a user to do both, there's no need to have two sets of
    operators at once.  Perhaps the user should specify the order once, and
    all the operators should then use that order.  I don't have code for this.
    My code is all little-endian, which is confusing, because the words are
    represented as lists that are printed with the first element on the left,
    but they represent words with the first bit on the right.

  o Provide routines for converting to and from whole numbers (": num").  When
    there are HOL libraries for integers, rational numbers, and floating-point
    numbers, either the wordn library or those libraries should provide 
    routines for converting to and from those types, too.

  o Provide routines for converting between words and human-readable strings
    in various radices: decimal, hexadecimal, octal, and binary.  So, for
    example, I want to be able to say "HEX `01F3C`" to specify a wordn value.
    I have untested, hacked-together code for this (and for the stuff later in
    this list), and I'll send it to anyone who wants to embarrass me by asking
    to see it.  Parser and pretty-printer support might be nice, too, since
    word64 is really ugly in its present form, and that's what I work with
    most.  A pretty-printer would fix the little-endian printing confusion, too.

  o Provide routines for rotating the bits of a word, and for shifting left
    and right, and for shifting right while sign-extending.  The more-lists
    library already provides most of the underlying operations for lists.

  o Provide routines to extract or replace bit fields (that is, a subsequence of
    bits within the wordn) by specifing the starting and ending positions of
    the field.  So, for example, "EXTRACT_FIELD (7,3) FOO" should be the value
    of bits 7 through 3 of FOO.  My code for extract returns a wordn, and I
    have two versions: one that returns the value with zeros in the unused
    bits, and one that sign-extends the value into the unused bits.  (I
    initially had a single version of extract that returned a smaller word,
    but as I specified more and more of my machine, I found the number of
    word sizes proliferating and just making things more confusing.  I have now
    picked a single word size as the fundamental size for that spec, and I do
    most computations in that type.  It feels artificial, but it's much easier
    to read in practice.  So now my version of extract just returns a value of
    the same type it's given.)  The term "INSERT_FIELD (5,2) new_value FOO"
    should be the wordn that results from replacing bits 5 through 2 in FOO
    with the value given in the low bits of new_value.

  o Provide routines to divide a large word into a list of smaller words,
    and to pack it back up again.  For example, I want to be able to break a
    64-bit word into 8 8-bit bytes, or pack 8 bytes to form a 64-bit word.

  o Provide bit-wise logical operations.  That is, map the boolean operations
    ("/\", "\/", "~", and others the user may define) onto words, so the
    boolean operation is applied to corresponding bits of the operands.

  o Provide modular-arithmetic routines for wordn.  (I hacked together my own
    version of this to straighten my own thinking, and haven't even looked to
    see if there's a version already available.)

There's probably more that would be useful, but that's all I've thought of.