Allow :exhaust to work directly on floating-point values

by enumerating all bitpatterns.

Note, this overcounts somewhat the number of distinct floating point
values there are, since all NaNs are considered identical
as `Float` values.  We could be more careful here to avoid
generating more NaN values than required, but I'm not sure it's worth
the effort.

Fixes #1051

src/Cryptol/Testing/Random.hs

@@ -36,6 +36,7 @@ import qualified Data.Sequence as Seq
 import System.Random          (RandomGen, split, random, randomR)
 
 import Cryptol.Backend        (Backend(..), SRational(..))
+import Cryptol.Backend.FloatHelpers (floatFromBits)
 import Cryptol.Backend.Monad  (runEval,Eval,EvalErrorEx(..))
 import Cryptol.Backend.Concrete
 
@@ -353,7 +354,7 @@ typeSize ty = case ty of
   TVInteger -> Nothing
   TVRational -> Nothing
   TVIntMod n -> Just n
-  TVFloat{} -> Nothing -- TODO?
+  TVFloat e p -> Just (2 ^ (e+p))
   TVArray{} -> Nothing
   TVStream{} -> Nothing
   TVSeq n el -> (^ n) <$> typeSize el
@@ -368,13 +369,13 @@ for types where 'typeSize' returned 'Nothing'. -}
 typeValues :: TValue -> [Value]
 typeValues ty =
   case ty of
-    TVBit      -> [ VBit False, VBit True ]
-    TVInteger  -> []
-    TVRational -> []
-    TVIntMod n -> [ VInteger x | x <- [ 0 .. (n-1) ] ]
-    TVFloat{}  -> [] -- TODO?
-    TVArray{}  -> []
-    TVStream{} -> []
+    TVBit       -> [ VBit False, VBit True ]
+    TVInteger   -> []
+    TVRational  -> []
+    TVIntMod n  -> [ VInteger x | x <- [ 0 .. (n-1) ] ]
+    TVFloat e p -> [ VFloat (floatFromBits e p v) | v <- [0 .. 2^(e+p) - 1] ]
+    TVArray{}   -> []
+    TVStream{}  -> []
     TVSeq n TVBit ->
       [ VWord n (pure (WordVal (BV n x)))
       | x <- [ 0 .. 2^n - 1 ]

tests/issues/issue1049.icry

@@ -1,2 +1,3 @@
 :m Float
 :exhaust (\x -> (y != y \/ x == fpToBits y  where y = fpFromBits x : Float16))
+:exhaust (\x -> (x : Float16)  =.= fpFromBits (fpToBits x))

tests/issues/issue1049.icry.stdout

@@ -4,3 +4,6 @@ Loading module Float
 Using exhaustive testing.
 Testing... Passed 65536 tests.
 Q.E.D.
+Using exhaustive testing.
+Testing... Passed 65536 tests.
+Q.E.D.