json: write NaN/Infinity float values as strings

JSON doesn't support these for some god-awful reason. (JSON would have
been so much better if it weren't based on JavaScript, the plague of
this world.)

We don't really care whether these specific values "round trip", so we
might as well write them in a standard-compliant way.

Untested. I was too lazy to even run this, but it probably works.

See #6691.