Add specs for Language.R*

inline-r/inline-r.cabal

@@ -59,20 +59,21 @@ library
     Foreign.R.Internal
     Foreign.R.Parse
     Foreign.R.Type
+    Foreign.R.Type.Singletons
 --    H.Prelude
 --    H.Prelude.Interactive
---    Language.R
+    Language.R
 --    Language.R.Debug
     Language.R.GC
     Language.R.Globals
     Language.R.HExp
     Language.R.Instance
---    Language.R.Internal
+    Language.R.Internal
     Language.R.Internal.FunWrappers
     Language.R.Internal.FunWrappers.TH
---    Language.R.Literal
+    Language.R.Literal
 --    Language.R.Matcher
---    Language.R.QQ
+    Language.R.QQ
   if !os(windows)
     exposed-modules:
       Foreign.R.EventLoop

inline-r/src/Language/R.hs

@@ -7,7 +7,10 @@
 {-# LANGUAGE ForeignFunctionInterface #-}
 {-# Language GADTs #-}
 {-# Language ViewPatterns #-}
+{-# OPTIONS_GHC -fplugin-opt=LiquidHaskell:--skip-module=False #-}
 
+{-@ LIQUID "--exact-data-cons" @-} -- needed to have LH accept specs in module HExp
+{-@ LIQUID "--prune-unsorted" @-}
 module Language.R
   ( module Foreign.R
   , module Foreign.R.Type
@@ -34,19 +37,18 @@ module Language.R
 import           Control.Memory.Region
 import qualified Data.Vector.SEXP as Vector
 import Control.Monad.R.Class
+import Foreign.C.String -- XXX: Needed for LH name resolution
+import Foreign.ForeignPtr -- XXX: imported to help LH name resolution
 import Foreign.R
   ( SEXP
-  , SomeSEXP(..)
   , typeOf
-  , asTypeOf
-  , cast
-  , unSomeSEXP
-  , unsafeCoerce
   )
 import qualified Foreign.R as R
+import qualified Foreign.R.Internal as R
 import qualified Foreign.R.Parse as R
 import qualified Foreign.R.Error as R
 import           Foreign.R.Type
+import           GHC.ST -- Needed to help LH name resolution
 import           Language.R.GC
 import           Language.R.Globals
 import           Language.R.HExp
@@ -59,7 +61,6 @@ import Control.Exception ( throwIO )
 import Control.Monad ( (>=>), when, unless, forM, void )
 import Data.ByteString as B
 import Data.ByteString.Char8 as C8 ( pack, unpack )
-import Data.Singletons (sing)
 import Foreign
   ( alloca
   , castPtr
@@ -73,88 +74,98 @@ import Prelude
 -- the dependency hierarchy.
 
 -- | Parse and then evaluate expression.
-parseEval :: ByteString -> IO (SomeSEXP V)
+{-@ ignore parseEval @-}
+parseEval :: ByteString -> IO (SEXP V)
 parseEval txt = useAsCString txt $ \ctxt ->
   R.withProtected (R.mkString ctxt) $ \rtxt ->
     alloca $ \status -> do
       R.withProtected (R.parseVector rtxt 1 status (R.release nilValue)) $ \exprs -> do
         rc <- fromIntegral <$> peek status
         unless (R.PARSE_OK == toEnum rc) $
           runRegion $ throwRMessage $ "Parse error in: " ++ C8.unpack txt
-        SomeSEXP expr <- peek $ castPtr $ R.unsafeSEXPToVectorPtr exprs
+        expr <- peek $ castPtr $ R.unsafeSEXPToVectorPtr exprs
         runRegion $ do
-          SomeSEXP val <- eval expr
-          return $ SomeSEXP (R.release val)
+          val <- eval expr
+          return (R.release val)
 
 -- | Parse file and perform some actions on parsed file.
 --
 -- This function uses continuation because this is an easy way to make
 -- operations GC-safe.
-parseFile :: FilePath -> (SEXP s 'R.Expr -> IO a) -> IO a
+{-@ assume parseFile :: FilePath -> (TSEXP s Foreign.R.Type.Expr -> IO a) -> IO a @-}
+parseFile :: FilePath -> (SEXP s -> IO a) -> IO a
 {-# DEPRECATED parseFile "Use [r| parse(file=\"path/to/file\") |] instead." #-}
 parseFile fl f = do
     withCString fl $ \cfl ->
       R.withProtected (R.mkString cfl) $ \rfl ->
-        r1 (C8.pack "parse") rfl >>= \(R.SomeSEXP s) ->
-          return (R.unsafeCoerce s) `R.withProtected` f
+        r1 (C8.pack "parse") rfl >>= \s ->
+          return s `R.withProtected` f
 
+{-@ parseText :: String -> Bool -> IO (TSEXP V Foreign.R.Type.Expr) @-}
 parseText
   :: String -- ^ Text to parse
   -> Bool   -- ^ Whether to annotate the AST with source locations.
-  -> IO (R.SEXP V 'R.Expr)
+  -> IO (R.SEXP V)
 {-# DEPRECATED parseText "Use [r| parse(text=...) |] instead." #-}
 parseText txt b = do
     s <- parseEval $ C8.pack $
          "parse(text=" ++ show txt ++ ", keep.source=" ++ keep ++ ")"
-    return $ (sing :: R.SSEXPTYPE 'R.Expr) `R.cast` s
+    return $ R.Expr `R.checkSEXPTYPE` s
   where
     keep | b         = "TRUE"
          | otherwise = "FALSE"
 
 -- | Internalize a symbol name.
-install :: MonadR m => String -> m (SEXP V 'R.Symbol)
-install = io . installIO
+{-@ assume install :: String -> m (TSEXP V Foreign.R.Type.Symbol) @-}
+{-@ ignore install @-}
+install :: MonadR m => String -> m (SEXP V)
+install s = io (installIO s)
 
 {-# DEPRECATED string, strings "Use mkSEXP instead" #-}
 
 -- | Create an R character string from a Haskell string.
-string :: String -> IO (SEXP V 'R.Char)
+{-@ string :: String -> IO (TSEXP V Foreign.R.Type.SChar) @-}
+string :: String -> IO (SEXP V)
 string str = withCString str R.mkChar
 
 -- | Create an R string vector from a Haskell string.
-strings :: String -> IO (SEXP V 'R.String)
+{-@ strings :: String -> IO (TSEXP V Foreign.R.Type.SString) @-}
+strings :: String -> IO (SEXP V)
 strings str = withCString str R.mkString
 
 -- | Evaluate a (sequence of) expression(s) in the given environment, returning the
 -- value of the last.
-evalEnv :: MonadR m => SEXP s a -> SEXP s 'R.Env -> m (SomeSEXP (Region m))
-evalEnv (hexp -> Language.R.HExp.Expr _ v) rho = acquireSome =<< do
+{-@ assume evalEnv :: SEXP s -> TSEXP s Foreign.R.Type.Env -> m (SEXP (Region m)) @-}
+{-@ ignore evalEnv @-}
+evalEnv :: MonadR m => SEXP s -> SEXP s -> m (SEXP (Region m))
+evalEnv (hexp -> Language.R.HExp.Expr _ v) rho = acquire =<< do
     io $ alloca $ \p -> do
-      mapM_ (\(SomeSEXP s) -> void $ R.protect s) (Vector.toList v)
-      x <- Prelude.last <$> forM (Vector.toList v) (\(SomeSEXP s) -> do
+      mapM_ (\s -> void $ R.protect s) (Vector.toList v)
+      x <- Prelude.last <$> forM (Vector.toList v) (\s -> do
           z <- R.tryEvalSilent s (R.release rho) p
           e <- peek p
           when (e /= 0) $ runRegion $ throwR rho
           return z)
       R.unprotect (Vector.length v)
       return x
-evalEnv x rho = acquireSome =<< do
+evalEnv x rho = acquire =<< do
     io $ alloca $ \p -> R.withProtected (return (R.release x)) $ \_ -> do
       v <- R.tryEvalSilent x rho p
       e <- peek p
       when (e /= 0) $ runRegion $ throwR rho
       return v
 
 -- | Evaluate a (sequence of) expression(s) in the global environment.
-eval :: MonadR m => SEXP s a -> m (SomeSEXP (Region m))
+eval :: MonadR m => SEXP s -> m (SEXP (Region m))
 eval x = evalEnv x (R.release globalEnv)
 
 -- | Silent version of 'eval' function that discards it's result.
-eval_ :: MonadR m => SEXP s a -> m ()
+eval_ :: MonadR m => SEXP s -> m ()
 eval_ = void . eval
 
 -- | Throw an R error as an exception.
-throwR :: MonadR m => R.SEXP s 'R.Env   -- ^ Environment in which to find error.
+{-@ throwR :: TSEXP s Foreign.R.Type.Env -> m a @-}
+throwR :: MonadR m => R.SEXP s   -- ^ Environment in which to find error.
        -> m a
 throwR env = getErrorMessage env >>= io . throwIO . R.RError
 
@@ -165,6 +176,7 @@ throwR env = getErrorMessage env >>= io . throwIO . R.RError
 -- the next computaion will be immediately cancelled. Note that R will only
 -- interrupt computations at so-called "safe points" (in particular, not in the
 -- middle of a C call).
+{-@ ignore cancel @-}
 cancel :: IO ()
 cancel = poke R.interruptsPending 1
 
@@ -173,12 +185,14 @@ throwRMessage :: MonadR m => String -> m a
 throwRMessage = io . throwIO . R.RError
 
 -- | Read last error message.
-getErrorMessage :: MonadR m => R.SEXP s 'R.Env -> m String
+{-@ assume getErrorMessage :: TSEXP s Foreign.R.Type.Env -> m String @-}
+{-@ ignore getErrorMessage @-}
+getErrorMessage :: MonadR m => R.SEXP s -> m String
 getErrorMessage e = io $ do
   R.withProtected (withCString "geterrmessage" ((R.install >=> R.lang1))) $ \f -> do
     R.withProtected (return (R.release e)) $ \env -> do
       peekCString
         =<< R.char
         =<< peek
-        =<< R.string . R.cast (sing :: R.SSEXPTYPE 'R.String)
+        =<< R.string . R.checkSEXPTYPE R.SString
         =<< R.eval f env

inline-r/src/Language/R/Globals.hs

@@ -64,12 +64,12 @@ _ = undefined :: (Foreign.C.CString, R.SEXP s)
 
 {-@
 type RVariables =
-    ( Ptr (TSEXP G Env)
-    , Ptr (TSEXP G Env)
-    , Ptr (TSEXP G Env)
-    , Ptr (TSEXP G Nil)
-    , Ptr (TSEXP G Symbol)
-    , Ptr (TSEXP G Symbol)
+    ( Ptr (TSEXP G Foreign.R.Type.Env)
+    , Ptr (TSEXP G Foreign.R.Type.Env)
+    , Ptr (TSEXP G Foreign.R.Type.Env)
+    , Ptr (TSEXP G Foreign.R.Type.Nil)
+    , Ptr (TSEXP G Foreign.R.Type.Symbol)
+    , Ptr (TSEXP G Foreign.R.Type.Symbol)
     , Ptr CInt
     , Ptr CInt
 #ifndef mingw32_HOST_OS
@@ -113,33 +113,33 @@ pokeRVariables = poke rVariables <=< newStablePtr
 #endif
  ) = unsafePerformIO $ peek rVariables >>= deRefStablePtr
 
-{-@ assume unboundValue :: TSEXP G Symbol @-}
+{-@ assume unboundValue :: TSEXP G Foreign.R.Type.Symbol @-}
 -- | Special value to which all symbols unbound in the current environment
 -- resolve to.
 unboundValue :: SEXP G
 unboundValue = unsafePerformIO $ peek unboundValuePtr
 
-{-@ assume nilValue :: TSEXP G Nil @-}
+{-@ assume nilValue :: TSEXP G Foreign.R.Type.Nil @-}
 -- | R's @NULL@ value.
 nilValue :: SEXP G
 nilValue = unsafePerformIO $ peek nilValuePtr
 
-{-@ assume missingArg :: TSEXP G Symbol @-}
+{-@ assume missingArg :: TSEXP G Foreign.R.Type.Symbol @-}
 -- | Value substituted for all missing actual arguments of a function call.
 missingArg :: SEXP G
 missingArg = unsafePerformIO $ peek missingArgPtr
 
-{-@ assume baseEnv :: TSEXP G Env @-}
+{-@ assume baseEnv :: TSEXP G Foreign.R.Type.Env @-}
 -- | The base environment.
 baseEnv :: SEXP G
 baseEnv = unsafePerformIO $ peek baseEnvPtr
 
-{-@ assume emptyEnv :: TSEXP G Env @-}
+{-@ assume emptyEnv :: TSEXP G Foreign.R.Type.Env @-}
 -- | The empty environment.
 emptyEnv :: SEXP G
 emptyEnv = unsafePerformIO $ peek emptyEnvPtr
 
-{-@ assume globalEnv :: TSEXP G Env @-}
+{-@ assume globalEnv :: TSEXP G Foreign.R.Type.Env @-}
 -- | The global environment.
 globalEnv :: SEXP G
 globalEnv = unsafePerformIO $ peek globalEnvPtr

inline-r/src/Language/R/HExp.hs

@@ -198,14 +198,14 @@ htypeOf = \case
     Lang{} -> R.Lang
     Special{} -> R.Special
     Builtin{} -> R.Builtin
-    Char{} -> R.Char
-    Int{} -> R.Int
+    Char{} -> R.SChar
+    Int{} -> R.SInt
     Logical{} -> R.Logical
     Real{} -> R.Real
-    Complex{} -> R.Complex
-    String{} -> R.String
+    Complex{} -> R.SComplex
+    String{} -> R.SString
     DotDotDot{} -> R.List
-    Vector{} -> R.Vector
+    Vector{} -> R.SVector
     Expr{} -> R.Expr
     Bytecode{} -> R.Bytecode
     ExtPtr{} -> R.ExtPtr
@@ -216,7 +216,7 @@ htypeOf = \case
 {-@
 data HExp :: * -> * where
   Nil       :: HExp s
-  Symbol    :: {e1:SEXP s| typeOf e1 == R.Char || typeOf e1 == R.Nil}
+  Symbol    :: {e1:SEXP s| typeOf e1 == R.SChar || typeOf e1 == R.Nil}
             -> SEXP s
             -> SEXP s
             -> HExp s
@@ -226,7 +226,7 @@ data HExp :: * -> * where
             -> HExp s
   Env       :: {e1:SEXP s | typeOf e1 == R.List || typeOf e1 == R.Nil}
             -> {e2:SEXP s | typeOf e2 == R.Env || typeOf e2 == R.Nil}
-            -> {e3:SEXP s | typeOf e3 == R.Vector || typeOf e3 == R.Nil}
+            -> {e3:SEXP s | typeOf e3 == R.SVector || typeOf e3 == R.Nil}
             -> HExp s
   Closure   :: {e1:SEXP s | typeOf e1 == R.List || typeOf e1 == R.Nil}
             -> SEXP s
@@ -241,22 +241,22 @@ data HExp :: * -> * where
             -> HExp s
   Special   :: HExp s
   Builtin   :: HExp s
-  Char      :: TVector Word8 R.Char
+  Char      :: TVector Word8 R.SChar
             -> HExp s
   Logical   :: TVector Foreign.R.Context.Logical R.Logical
             -> HExp s
-  Int       :: TVector Int32 R.Int
+  Int       :: TVector Int32 R.SInt
             -> HExp s
   Real      :: TVector Double R.Real
             -> HExp s
-  Complex   :: TVector (Complex Double) R.Complex
+  Complex   :: TVector (Complex Double) R.SComplex
             -> HExp s
-  String    :: TVector (TSEXP V R.Char) R.String
+  String    :: TVector (TSEXP V R.SChar) R.SString
             -> HExp s
   DotDotDot :: {e1:SEXP s | typeOf e1 == R.List || typeOf e1 == R.Nil}
             -> HExp s
   Vector    :: Int32
-            -> TVector (SEXP V) R.Vector
+            -> TVector (SEXP V) R.SVector
             -> HExp s
   Expr      :: Int32
             -> TVector (SEXP V) R.Expr
@@ -382,14 +382,14 @@ peekHExp s =
                   <*> R.cdr s
       R.Special   -> return Special
       R.Builtin   -> return Builtin
-      R.Char      -> return $ Char    (Vector.unsafeFromSEXP s)
+      R.SChar     -> return $ Char    (Vector.unsafeFromSEXP s)
       R.Logical   -> return $ Logical (Vector.unsafeFromSEXP s)
-      R.Int       -> return $ Int     (Vector.unsafeFromSEXP s)
+      R.SInt      -> return $ Int     (Vector.unsafeFromSEXP s)
       R.Real      -> return $ Real    (Vector.unsafeFromSEXP s)
-      R.Complex   -> return $ Complex (Vector.unsafeFromSEXP s)
-      R.String    -> return $ String  (Vector.unsafeFromSEXP s)
+      R.SComplex  -> return $ Complex (Vector.unsafeFromSEXP s)
+      R.SString   -> return $ String  (Vector.unsafeFromSEXP s)
       R.DotDotDot -> unimplemented $ "peekHExp: " ++ show (R.typeOf s)
-      R.Vector    ->
+      R.SVector   ->
         Vector    <$> (fromIntegral <$> R.trueLength s)
                   <*> pure (Vector.unsafeFromSEXP s)
       R.Expr      ->

inline-r/src/Language/R/Internal.hs

@@ -19,17 +19,18 @@ inVoid = id
 {-# INLINE inVoid #-}
 
 -- | Call a pure unary R function of the given name in the global environment.
-r1 :: ByteString -> SEXP s a -> IO (SomeSEXP V)
+r1 :: ByteString -> SEXP s -> IO (SEXP V)
 r1 fn a =
     useAsCString fn $ \cfn -> R.install cfn >>= \f ->
       R.withProtected (R.lang2 f (R.release a)) (unsafeRunRegion . inVoid . eval)
 
 -- | Call a pure binary R function. See 'r1' for additional comments.
-r2 :: ByteString -> SEXP s a -> SEXP s b -> IO (SomeSEXP V)
+r2 :: ByteString -> SEXP s -> SEXP s -> IO (SEXP V)
 r2 fn a b =
     useAsCString fn $ \cfn -> R.install cfn >>= \f ->
       R.withProtected (R.lang3 f (R.release a) (R.release b)) (unsafeRunRegion . inVoid . eval)
 
 -- | Internalize a symbol name.
-installIO :: String -> IO (SEXP V 'R.Symbol)
+{-@ installIO :: String -> IO (TSEXP V Foreign.R.Type.Symbol) @-}
+installIO :: String -> IO (SEXP V)
 installIO str = withCString str R.install

inline-r/src/Language/R/Internal.hs-boot

@@ -4,9 +4,8 @@ module Language.R.Internal where
 
 import Control.Memory.Region
 import Data.ByteString (ByteString)
-import Foreign.R (SEXP, SomeSEXP(..))
-import qualified Foreign.R.Type as R
+import Foreign.R (SEXP)
 
-r1 :: ByteString -> SEXP s a -> IO (SomeSEXP V)
-r2 :: ByteString -> SEXP s a -> SEXP s b -> IO (SomeSEXP V)
-installIO :: String -> IO (SEXP V 'R.Symbol)
+r1 :: ByteString -> SEXP s -> IO (SEXP V)
+r2 :: ByteString -> SEXP s -> SEXP s -> IO (SEXP V)
+installIO :: String -> IO (SEXP V)