Sharp-u-reader
Allow underscore characters in numbers
Example:
ACL2 !>#ub1000_1000_1000_
2184
ACL2 !>#b100010001000
2184
ACL2 !>#uo1_1
9
ACL2 !>#o11
9
ACL2 !>#u34_5
345
ACL2 !>#u345
345
ACL2 !>345
345
ACL2 !>#ux12_a
298
ACL2 !>#ux12a
298
ACL2 !>#u x12a
298
ACL2 !>#x12a
298
ACL2 !>#u123_456/7_919
123456/7919
ACL2 !>
The ACL2 reader supports the use of #ub, #uo, and #ux where
one would otherwise write #b, #o, and #x, respectively (for
binary, octal, and hexadecimal numerals), but where underscore characters
(`_') are allowed but ignored. Also supported is the prefix #u in
front of a an expression that is a decimal numeral except that underscore
characters are allowed but ignored.
The precise specification of #u is as follows. The ACL2 reader reads
one expression after the #u. If the result is a number, then that number
is returned by the reader. Otherwise the result must be a symbol. Let N
be the symbol-name of the symbol; thus N is a string. If N
begins with one of the characters `B', `O', or `X', then first
obtain a string S1 by prefixing N with the character, `#';
otherwise let S1 be N. Next, remove all underscore characters
`_' from S1, obtaining S2. The result is obtained by applying
the ACL2 reader to S2; that result must be a number, or else an error
occurs.
