[ primitive ] fixed compilation of float primitives

agda · Oct 27, 2015 · f9b005f · f9b005f
1 parent 6157e88
commit f9b005f
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 8 deletions.
diff --git a/src/data/uhc-agda-base/src/UHC/Agda/Builtins.hs b/src/data/uhc-agda-base/src/UHC/Agda/Builtins.hs
@@ -271,13 +271,17 @@ primToLower     = C.toLower
 -- ====================
 primShowFloat :: Double -> String
 -- GHC drops trailing zeroes, UHC doesn't seem to do so. Quick fix for now...
-primShowFloat = reverse . dropWhile (=='0') . reverse . show
+primShowFloat x
+  | isNegativeZero x = "0.0"
+  | otherwise        = reverse . dropWhile (=='0') . reverse $ show x
 
 primMkFloat :: String -> Double
 primMkFloat = read
 
 primFloatEquality :: Double -> Double -> Bool
-primFloatEquality = (==)
+primFloatEquality x y
+  | isNaN x && isNaN y = True
+  | otherwise          = x == y
 
 -- ====================
 -- Reflection

diff --git a/src/full/Agda/Compiler/MAlonzo/Primitives.hs b/src/full/Agda/Compiler/MAlonzo/Primitives.hs
@@ -129,21 +129,26 @@ primBody s = maybe unimplemented (either (hsVarUQ . HS.Ident) id <$>) $
   , "primNatLess"      |-> relNat "(<)"
 
   -- Floating point functions
-  , "primIntegerToFloat"    |-> return "(fromIntegral :: Integer -> Double)"
+  , "primNatToFloat"        |-> return "(fromIntegral :: Integer -> Double)"
   , "primFloatPlus"         |-> return "((+) :: Double -> Double -> Double)"
   , "primFloatMinus"        |-> return "((-) :: Double -> Double -> Double)"
   , "primFloatTimes"        |-> return "((*) :: Double -> Double -> Double)"
   , "primFloatDiv"          |-> return "((/) :: Double -> Double -> Double)"
-  , "primFloatEquality"     |-> rel "(==)" "Double"
-  , "primFloatLess"         |-> rel "(<)" "Double"
+  , "primFloatEquality"     |-> return "((\\ x y -> if isNaN x && isNaN y then True else x == y) :: Double -> Double -> Bool)"
+  , "primFloatLess"         |-> return $ unwords
+                                  [ "((\\ x y ->"
+                                  , "let isNegInf z = z < 0 && isInfinite z in"
+                                  , "if isNegInf y then False else"
+                                  , "if isNegInf x then True  else"
+                                  , "if isNaN x    then True  else"
+                                  , "x < y) :: Double -> Double -> Bool)" ]
   , "primRound"             |-> return "(round :: Double -> Integer)"
   , "primFloor"             |-> return "(floor :: Double -> Integer)"
   , "primCeiling"           |-> return "(ceiling :: Double -> Integer)"
   , "primExp"               |-> return "(exp :: Double -> Double)"
-  , "primLog"               |-> return "(log :: Double -> Double)"  -- partial
+  , "primLog"               |-> return "(log :: Double -> Double)"
   , "primSin"               |-> return "(sin :: Double -> Double)"
-  , "primShowFloat"         |-> return "(show :: Double -> String)"
-  , "primRound"             |-> return "(round :: Double -> Integer)"
+  , "primShowFloat"         |-> return "((\\ x -> if isNegativeZero then \"0.0\" else show x) :: Double -> String)"
 
   -- Character functions
   , "primCharEquality"   |-> rel "(==)" "Char"