Merge pull request ucsd-progsys#1869 from renanroberto/floating-spec

Add spec for Floating typeclass

Author: nikivazou

liquid-base/src/GHC/Float.hs

@@ -1,3 +1,5 @@
 module GHC.Float (module Exports) where
 
+import GHC.Types
+import GHC.Real
 import "base" GHC.Float as Exports

liquid-base/src/GHC/Float.spec

@@ -0,0 +1,27 @@
+module spec GHC.Float where
+
+import GHC.Types
+
+class (GHC.Real.Fractional a) => GHC.Float.Floating a where
+  GHC.Float.pi       :: a
+  GHC.Float.exp      :: a -> {y:a | y > 0}
+  GHC.Float.log      :: {x:a | x > 0} -> a
+  GHC.Float.sqrt     :: {x:a | x >= 0} -> {y:a | y >= 0}
+  (GHC.Float.**)     :: x:a -> {y:a | x = 0 => y >= 0} -> a
+  GHC.Float.logBase  :: {b:a | b > 0 && b /= 1} -> {x:a | x > 0} -> a
+  GHC.Float.sin      :: a -> {y:a | -1 <= y && y <= 1}
+  GHC.Float.cos      :: a -> {y:a | -1 <= y && y <= 1}
+  GHC.Float.tan      :: a -> a
+  GHC.Float.asin     :: {x:a | -1 <= x && x <= 1} -> a
+  GHC.Float.acos     :: {x:a | -1 <= x && x <= 1} -> a
+  GHC.Float.atan     :: a -> a
+  GHC.Float.sinh     :: a -> a
+  GHC.Float.cosh     :: a -> {y:a | y >= 1}
+  GHC.Float.tanh     :: a -> {y:a | -1 < y && y < 1}
+  GHC.Float.asinh    :: a -> a
+  GHC.Float.acosh    :: {y:a | y >= 1} -> a
+  GHC.Float.atanh    :: {y:a | -1 < y && y < 1} -> a
+  GHC.Float.log1p    :: a -> a
+  GHC.Float.expm1    :: a -> a
+  GHC.Float.log1pexp :: a -> a
+  GHC.Float.log1mexp :: a -> a

liquid-base/src/Prelude.hs

@@ -12,6 +12,7 @@ import GHC.List
 import GHC.Maybe
 import GHC.Num
 import GHC.Real
+import GHC.Float
 import GHC.Types
 import GHC.Word
 

liquid-base/src/Prelude.spec

@@ -6,6 +6,7 @@ import GHC.List
 import GHC.Maybe
 import GHC.Num
 import GHC.Real
+import GHC.Float
 import GHC.Word
 
 import Data.Foldable

tests/errors/ElabLocation3.hs

@@ -183,28 +183,6 @@ part1 _ = do
     let allRounds2 = iterate {- (Main.round 8 3 m2) -} id input in
       print $ allRounds2 !! 20
 
-part2 :: () -> IO ()
-part2 _ = do
-  putStrLn "Part 2"
-  let m1 = computeModulus example in do
-    putStrLn $ "Working mod " ++ show m1
-    let allRounds = iterate {- (Main.round 4 1 m1) -} id example in do
-      print $ allRounds !! 1000
-      print $ allRounds !! 2000
-      print $ allRounds !! 3000
-      print $ allRounds !! 4000
-      print $ allRounds !! 5000
-      print $ allRounds !! 6000
-      print $ allRounds !! 7000
-      print $ allRounds !! 8000
-      print $ allRounds !! 9000
-      print $ allRounds !! 10000
-      
-  let m2 = computeModulus input in do
-    putStrLn $ "Working mod " ++ show m2    
-    let allRounds2 = iterate {- (Main.round 8 1 m2) -} id input in
-      print $ allRounds2 !! 10000
-
 mymain :: IO ()
-mymain = part1 () >> part2 ()
+mymain = part1 ()
 

tests/neg/CosNegTest.hs

@@ -0,0 +1,6 @@
+{-@ LIQUID "--expect-error-containing=CosNegTest.hs:6:1" @-}
+module CosNegTest where
+
+{-@ test :: a -> {x:a | x > 1} @-}
+test :: Floating a => a -> a
+test x = cos x

tests/neg/ExpNegTest.hs

@@ -0,0 +1,6 @@
+{-@ LIQUID "--expect-error-containing=ExpNegTest.hs:6:1" @-}
+module ExpNegTest where
+
+{-@ test :: a -> {x:a | x <= 0} @-}
+test :: Floating a => a -> a
+test x = exp x

tests/neg/ExponentiationNegTest.hs

@@ -0,0 +1,5 @@
+{-@ LIQUID "--expect-error-containing=ExponentiationNegTest.hs:5:1" @-}
+module ExponentiationNegTest where
+
+test :: Floating a => a
+test = 0 ** (-1)

tests/neg/LogNegTest.hs

@@ -0,0 +1,5 @@
+{-@ LIQUID "--expect-error-containing=LogNegTest.hs:5:1" @-}
+module LogNegTest where
+
+test :: Floating a => a
+test = log 0

tests/neg/SinNegTest.hs

@@ -0,0 +1,6 @@
+{-@ LIQUID "--expect-error-containing=SinNegTest.hs:6:1" @-}
+module SinNegTest where
+
+{-@ test :: a -> {x:a | x > 1} @-}
+test :: Floating a => a -> a
+test x = sin x