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

@@ -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 ::

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