copilot-bluespec: Fix translation of special Float values to Bluespec. Refs #697.

`copilot-bluespec`'s translation from Copilot to Bluespec up-casts `Float`
values to `Double` values using the `realToFrac` function. `realToFrac`
incorrectly handles special floating-point values such as negative zero,
infinity, and NaN values, causing `copilot-bluespec` to generate the wrong
`Float` values on the Bluespec end.

This commit removes the use of `realToFrac` in favor of an alternative approach
based on `GHC.Float.float2Double`, which correctly handles most special
floating-point values. A notable exception is NaN values, as `float2Double`
does not reliably preserve the payload of a NaN value. As such, we include a
special case for NaN values that takes care to preserve payloads.

Co-authored-by: Ryan Scott <rscott@galois.com>

Author: tkann-galois

copilot-bluespec/src/Copilot/Compile/Bluespec/Expr.hs

@@ -18,7 +18,7 @@ import Data.String (IsString (..))
 import qualified Language.Bluespec.Classic.AST as BS
 import qualified Language.Bluespec.Classic.AST.Builtin.Ids as BS
 import Numeric.Floating.IEEE.NaN (isSignaling, setPayloadSignaling, setPayload, getPayload)
-import GHC.Float (double2Float, castFloatToWord32, castDoubleToWord64)
+import GHC.Float (double2Float, castFloatToWord32, castDoubleToWord64, float2Double)
 
 -- Internal imports: Copilot
 import Copilot.Core
@@ -535,7 +535,7 @@ constTy ty =
     Word16    -> constInt ty . toInteger
     Word32    -> constInt ty . toInteger
     Word64    -> constInt ty . toInteger
-    Float     -> constFP ty . realToFrac
+    Float     -> constFP ty . nanSafeFloat2Double
     Double    -> constFP ty
 
     -- Translating a Copilot array literal to a Bluespec Vector is somewhat
@@ -563,6 +563,25 @@ constTy ty =
                , constTy ty'' val
                ))
              (toValues v))
+  where
+    -- Convert a Float to a Double. This function takes care to preserve
+    -- special floating-point values, such as negative zero, infinity, and NaN
+    -- values.
+    nanSafeFloat2Double :: Float -> Double
+    nanSafeFloat2Double x
+      | isNaN x   = convertFloatNaNToDoubleNan x
+      | otherwise = float2Double x
+      where
+        payload :: Double
+        payload = float2Double $ getPayload x
+
+        -- float2Double does not preserve the payloads of NaN values, so we
+        -- include a special case for translating NaNs.
+        convertFloatNaNToDoubleNan :: Float -> Double
+        convertFloatNaNToDoubleNan nan =
+          if isSignaling nan
+            then setPayloadSignaling payload
+            else setPayload payload
 
 -- | Transform a list of Copilot Core expressions of a given 'Type' into a
 -- Bluespec @Vector@ expression.