From 1e783e15504f144b9187c9f625e3b374f5ec9c20 Mon Sep 17 00:00:00 2001
From: Ben Gamari <ben@smart-cactus.org>
Date: Sun, 23 Jan 2022 21:15:04 -0500
Subject: [PATCH] WIP

---
 src/CCall.hs          |  1 +
 src/Expr.hs           | 12 ++++++++++--
 src/Expr.hs-boot      |  6 +++++-
 src/RefInterpreter.hs | 13 +++++++++++++
 test-primops.cabal    |  1 +
 5 files changed, 30 insertions(+), 3 deletions(-)

diff --git a/src/CCall.hs b/src/CCall.hs
index 8632bde..f3936bb 100644
--- a/src/CCall.hs
+++ b/src/CCall.hs
@@ -39,6 +39,7 @@ testCCall
     -> CCallDesc
     -> Property
 testCCall comp c = 
+    counterexample (cStub c) $ counterexample (cCallCmm c) $ 
     ioProperty $ withTempDirectory "." "tmp" $ \tmpDir -> do
         writeFile (tmpDir </> "test_c.c") (cStub c)
         writeFile (tmpDir </> "test.cmm") (cCallCmm c)
diff --git a/src/Expr.hs b/src/Expr.hs
index 4d947e5..4f9d1d2 100644
--- a/src/Expr.hs
+++ b/src/Expr.hs
@@ -17,8 +17,6 @@ module Expr
     , genExpr
     ) where
 
-import Data.Foldable (foldl')
-import qualified Data.ByteString as BS
 import Numeric.Natural
 import Control.Monad
 import Data.Bits as Bits
@@ -29,6 +27,7 @@ import Data.Proxy
 import Prelude hiding (truncate)
 
 import {-# SOURCE #-} RefInterpreter
+import {-# SOURCE #-} FExpr
 import Width
 import Number
 
@@ -100,6 +99,10 @@ data Expr (width :: Width) where
     EZeroExt :: forall narrow wide. (KnownWidth narrow, wide `WiderThan` narrow)
              => Expr narrow -> Expr wide
 
+    -- | Floating-point to signed integer conversion
+    EFSConv  :: FExpr width -> Expr width
+    EFRel    :: FRelationalOp -> FExpr width -> FExpr width -> Expr WordSize
+
     ELoad    :: Expr WordSize -> Expr width
     ELit     :: Number width -> Expr width
 
@@ -165,6 +168,8 @@ instance KnownWidth width => Arbitrary (Expr width) where
                           ++ [ EZeroExt a ]
           EZeroExt a   -> shrinkUnOp  EZeroExt a
                           ++ [ EZeroExt b | EZeroExt b <- pure a, Wider <- pure $ e `compareWidths` b ]
+          EFSConv  a   -> EFSConv <$> shrink a
+          EFRel op a b -> EFRel op <$> shrink a <*> shrink b
           ELoad    a   -> shrinkUnOp  ELoad a
           ELit     a   -> map ELit (shrink a)
       where
@@ -195,6 +200,7 @@ genExpr' _width = sized gen
         oneof $
             [ litGen
             , loadGen
+            , EFSConv <$> arbitrary
             ]
             ++ arithmeticGens
             ++ bitwiseGens
@@ -257,6 +263,8 @@ genExpr' _width = sized gen
       | SameWidth <- Proxy @width `compareWidths` Proxy @WordSize
       = [ do op <- arbitrary
              binOp (ERel op)
+        , EFRel @W32 <$> arbitrary <*> arbitrary <*> arbitrary
+        , EFRel @W64 <$> arbitrary <*> arbitrary <*> arbitrary
         ]
       | otherwise = []
 
diff --git a/src/Expr.hs-boot b/src/Expr.hs-boot
index 9d68166..411ec50 100644
--- a/src/Expr.hs-boot
+++ b/src/Expr.hs-boot
@@ -2,8 +2,12 @@
 
 module Expr where
 
-import Width (Width)
+import Test.QuickCheck
+
+import Width (Width, KnownWidth)
 
 data Expr (width :: Width)
 
 type role Expr nominal
+
+instance (KnownWidth width) => Arbitrary (Expr width)
diff --git a/src/RefInterpreter.hs b/src/RefInterpreter.hs
index 7d492d3..eb5832b 100644
--- a/src/RefInterpreter.hs
+++ b/src/RefInterpreter.hs
@@ -3,6 +3,7 @@ module RefInterpreter
     , memoryContents
     , memoryOracle
     , interpret
+    , interpretFloat
     ) where
 
 import Data.Bits
@@ -12,6 +13,7 @@ import Numeric.Natural
 
 import Width
 import Expr
+import FExpr
 import Number
 
 boolVal :: Bool -> Number WordSize
@@ -64,6 +66,17 @@ interpret (EZeroExt a) = zeroExtNumber (interpret a)
 interpret (ELoad off)  = memoryOracle $ toUnsigned $ interpret off
 interpret (ELit n)     = n
 
+interpretFloat
+    :: forall width. (KnownWidth width)
+    => FExpr width -> FloatType width
+interpretFloat (FEAdd a b)   = interpretFloat a + interpretFloat b
+interpretFloat (FESub a b)   = interpretFloat a - interpretFloat b
+interpretFloat (FEMul a b)   = interpretFloat a - interpretFloat b
+interpretFloat (FEQuot a b)  = interpretFloat a `quot` interpretFloat b
+interpretFloat (FENegate a)  = negate (interpretFloat a)
+interpretFloat (FFromSInt a) = realToFrac $ toSigned $ interpret a
+interpretFloat (FConv a)     = realToFrac (interpretFloat a)
+
 memorySize :: Natural
 memorySize = 1 `shiftL` 22
 
diff --git a/test-primops.cabal b/test-primops.cabal
index c02de6e..3d76307 100644
--- a/test-primops.cabal
+++ b/test-primops.cabal
@@ -14,6 +14,7 @@ executable test-primops
     other-modules:    Width,
                       Number,
                       Expr,
+                      FExpr,
                       Expr.Parse,
                       Interpreter,
                       ToCmm,
-- 
GitLab