From 143e0395ba7692a21b3eb6dbc11df80278d64413 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Mon, 15 Mar 2021 16:02:58 -0700
Subject: [PATCH] Don't use the `showFreeMin` floating-point printing mode,
 which has highly counterintuitive results.  Instad, use the `showFree` mode,
 which produces results more accurate to the underlying bit representation. 
 The `showFree` mode often produces unfortunate trailing zeros in decimal
 representations, so we take some care to trim those out.

Fixes #1089
---
 src/Cryptol/Backend/FloatHelpers.hs | 20 +++++++++++++++++---
 tests/regression/float.icry.stdout  |  4 ++--
 2 files changed, 19 insertions(+), 5 deletions(-)

diff --git a/src/Cryptol/Backend/FloatHelpers.hs b/src/Cryptol/Backend/FloatHelpers.hs
index b9e9ad341..4aa93d0fd 100644
--- a/src/Cryptol/Backend/FloatHelpers.hs
+++ b/src/Cryptol/Backend/FloatHelpers.hs
@@ -2,6 +2,7 @@
 {-# Language BangPatterns #-}
 module Cryptol.Backend.FloatHelpers where
 
+import Data.Char (isDigit)
 import Data.Ratio(numerator,denominator)
 import LibBF
 
@@ -82,18 +83,31 @@ fpPP opts bf =
   str = bfToString base fmt num
   fmt = addPrefix <> showRnd NearEven <>
         case useFPFormat opts of
-          FloatFree e -> withExp e $ showFreeMin
+          FloatFree e -> withExp e $ showFree
                                    $ Just $ fromInteger precW
           FloatFixed n e -> withExp e $ showFixed $ fromIntegral n
           FloatFrac n    -> showFrac $ fromIntegral n
 
   -- non-base 10 literals are not overloaded so we add an explicit
-  -- .0 if one is not present. 
+  -- .0 if one is not present.  Moreover, we trim any extra zeros
+  -- that appear in a decimal representation.
   hacStr
-    | base == 10 || elem '.' str = str
+    | base == 10   = trimZeros
+    | elem '.' str = str
     | otherwise = case break (== 'p') str of
                     (xs,ys) -> xs ++ ".0" ++ ys
 
+  trimZeros =
+    case break (== '.') str of
+      (xs,'.':ys) ->
+        case break (not . isDigit) ys of
+          (frac, suffix) -> xs ++ '.' : processFraction frac ++ suffix
+      _ -> str
+
+  processFraction frac =
+    case dropWhile (== '0') (reverse frac) of
+      [] -> "0"
+      zs -> reverse zs
 
 -- | Make a literal
 fpLit ::
diff --git a/tests/regression/float.icry.stdout b/tests/regression/float.icry.stdout
index 3168589ea..c46120dec 100644
--- a/tests/regression/float.icry.stdout
+++ b/tests/regression/float.icry.stdout
@@ -26,8 +26,8 @@ Specifies the format to use when showing floating point numbers:
 0b1010.01
 0o12.2
 10.25
-0.4
-0.4
+0.38
+0.38
 0xa.4
 0x0.6
 0x1.234p4