bin/57184: awk should support hexadecimal floating-point input like 0x1.23456789abcdefp+123

[campbell+netbsd%mumble.net@localhost]

>Number:         57184
>Category:       bin
>Synopsis:       awk should support hexadecimal floating-point input like 0x1.23456789abcdefp+123
>Confidential:   no
>Severity:       serious
>Priority:       medium
>Responsible:    bin-bug-people
>State:          open
>Class:          sw-bug
>Submitter-Id:   net
>Arrival-Date:   Sat Jan 14 18:45:01 +0000 2023
>Originator:     Taylor R Campbell
>Release:        9.2
>Organization:
The NetBSD Flotation
>Environment:
being burned by the paperclip maximizer of capitalism
>Description:
awk supports decimal floating-point input, and hexadecimal floating-point output:

% awk 'BEGIN { OFMT = "%a"; print 1.1102230246251565e-16 }'
0x1p-53

But the hexadecimal notation doesn't work on input:

% awk 'BEGIN { print 0x1p-53 }'
0-53

The hexadecimal floating-point notation is a much clearer way to write many floating-point constants without the deception of decimal approximations.
>How-To-Repeat:
Try to enter hexadecimal floating-point input.
>Fix:
Yes please!