		Search-engine friendly clone of the ACL2 documentation.

Sharp-f-reader

Read a rational number in floating-point syntax

This topic is about reading expressions starting with #f. See also sharp-d-reader, which reads input starting with #d. Both read a form of floating-point notation as a rational number. However, while #d reads the next token as a Lisp floating-point number, #f is specific to ACL2 and follows rules documented explicitly below, including the use of underscores (_) and hexadecimal notation.

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, indicating base 10 digits, and #fx, indicating base 16 digits. Let {i} be notation representing a sequence of digits and (optionally) underscore (_) characters, optionally preceded by a sign (- or +), that the ACL2 reader reads as the integer i after discarding underscore characters; similarly for {j} and {n}, except that an initial sign is illegal for {j}, and for {n} the digits are always base 10 (even in the case of #fx). Note that each such string is terminated at the first character from the input channel that is not a digit. For the #f case we have the following semantics.

#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 (') as a separator, using underscore (_) instead, which is consistent with another reader macro, #u (see sharp-u-reader). Moreover, unlike the syntax described on the page above, the ACL2 #f reader allows an initial sign (- or +). To see why, note that in Lisp, the string "-#" starts a symbol, for example:

? '-#f23
|-#F23|
?

Since the ACL2 reader is based on the Lisp reader, it would be awkward to provide support to read the string "-#f23" as a number, -23. Instead, ACL2 accepts a sign immediately after the initial "#f" or "#fx":

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