scripts: Fixed excessive rounding when writing floats to csv/json files

This adds __csv__ methods to all Csv* classes to indicate how to write
csv/json output, and adopts Python's default float repr. As a plus, this
also lets us use "inf" for infinity in csv/json files, avoiding
potential unicode issues.

Before this we were reusing __str__ for both table rendering and
csv/json writing, which rounded to a single decimal digit! This made
float output pretty much useless outside of trivial cases.

---

Note Python apparently does some of its own rounding (1/10 -> 0.1?), so
the result may still not be round-trippable, but this is probably fine
for our somewhat hack-infested csv scripts.

scripts/code.py

@@ -66,6 +66,14 @@ class CsvInt(co.namedtuple('CsvInt', 'a')):
         else:
             return str(self.a)
 
+    def __csv__(self):
+        if self.a == mt.inf:
+            return 'inf'
+        elif self.a == -mt.inf:
+            return '-inf'
+        else:
+            return repr(self.a)
+
     def __bool__(self):
         return bool(self.a)
 
@@ -992,7 +1000,7 @@ def write_csv(path, Result, results, *,
                         {k: getattr(r, k)
                                 for k in by
                                 if getattr(r, k) is not None}
-                            | {prefix+k: str(getattr(r, k))
+                            | {prefix+k: getattr(r, k).__csv__()
                                 for k in fields
                                 if getattr(r, k) is not None})
 
@@ -1008,7 +1016,7 @@ def write_csv(path, Result, results, *,
                             {k: getattr(r, k)
                                     for k in by
                                     if getattr(r, k) is not None}
-                                | {prefix+k: str(getattr(r, k))
+                                | {prefix+k: getattr(r, k).__csv__()
                                     for k in fields
                                     if getattr(r, k) is not None}
                                 | ({Result._children: jsonify(