Read a rational number in floating-point (scientific notation) syntax

Examples: ACL2 !>#f567 567 ACL2 !>#f_5_6__7_ ; underscores are allowed, and discarded 567 ACL2 !> ACL2 !>#f-567 -567 ACL2 !>#f+567 567 ACL2 !>#f5.67 567/100 ACL2 !>#f-5.67 -567/100 ACL2 !>#f5.67e3 5670 ACL2 !>#f-5.67e3 -5670 ACL2 !>#f-5.67e-3 -567/100000 ACL2 !>#f.67e2 67 ACL2 !>#f-.67e2 -67 ACL2 !>#f-.67e+4 -6700 ACL2 !>#f-0.67e+4 -6700 ACL2 !>#fx101 257 ACL2 !>#fx10.1 257/16 ACL2 !>#fx10.1p3 257/2 ACL2 !>#fx10.1p-4 257/256 ACL2 !>#fx-10.1p-4 -257/256 ACL2 !>#fx.1p4 1 ACL2 !>#fx.1p+8 16 ACL2 !>#fx.1p-2 1/64 ACL2 !>#fx-0_4p1_0 -4096 ACL2 !>

As illustrated above, we support two forms of this reader:

#f{i} => i #f{i}e{n} => i * 10^n #f{i}.{j} => i + (/ j 10^k) where k is the length of {j} #f{i}.{j}e{n} => (i + (/ j 10^k)) * 10^n where k is the length of {j}

We have the following similar semantics for the #('#fx') case, except that {i} and {j} are now read in base 16. Note that {n} is still read in base 10.

#fx{i} => i #fx{i}p{n} => i * 2^n #fx{i}.{j} => i + (/ j 16^k) where k is the length of {j} #fx{i}.{j}p{n} => (i + (/ j 16^k)) * 2^n where k is the length of {j}

We thank Dmitry Nadezhin for pointing us to the following page, which explains an analogous ``floating point literal'' syntax for C++:

http://en.cppreference.com/w/cpp/language/floating_literal

Note, however, that in ACL2 we do not support the use of single quote
(

? '-#f23 |-#F23| ?

Since the ACL2 reader is based on the Lisp reader, it would be awkward to
provide support to read the string

ACL2 !>#f-23 -23 ACL2 !>