From aa5333b922e626ae7c5b6d9d31b717f01facb510 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Wed, 10 Jan 2024 14:00:08 -0300 Subject: [PATCH] Add specs for Language.R* --- inline-r/inline-r.cabal | 7 +- inline-r/src/Language/R.hs | 58 +++++----- inline-r/src/Language/R/Internal.hs | 7 +- inline-r/src/Language/R/Internal.hs-boot | 9 +- inline-r/src/Language/R/Literal.hs | 135 +++++++++++++++-------- 5 files changed, 133 insertions(+), 83 deletions(-) diff --git a/inline-r/inline-r.cabal b/inline-r/inline-r.cabal index cbcaca90..17b180ac 100644 --- a/inline-r/inline-r.cabal +++ b/inline-r/inline-r.cabal @@ -59,18 +59,19 @@ 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 if !os(windows) diff --git a/inline-r/src/Language/R.hs b/inline-r/src/Language/R.hs index 79c2555b..768069ed 100644 --- a/inline-r/src/Language/R.hs +++ b/inline-r/src/Language/R.hs @@ -36,12 +36,7 @@ import qualified Data.Vector.SEXP as Vector import Control.Monad.R.Class import Foreign.R ( SEXP - , SomeSEXP(..) , typeOf - , asTypeOf - , cast - , unSomeSEXP - , unsafeCoerce ) import qualified Foreign.R as R import qualified Foreign.R.Parse as R @@ -73,7 +68,7 @@ import Prelude -- the dependency hierarchy. -- | Parse and then evaluate expression. -parseEval :: ByteString -> IO (SomeSEXP V) +parseEval :: ByteString -> IO (SEXP V) parseEval txt = useAsCString txt $ \ctxt -> R.withProtected (R.mkString ctxt) $ \rtxt -> alloca $ \status -> do @@ -81,64 +76,71 @@ parseEval txt = useAsCString txt $ \ctxt -> 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 +{-@ parseFile :: FilePath -> (SEXP 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 (R.SEXP 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 :: String -> m (SEXP V Foreign.R.Type.Symbol) @-} +install :: MonadR m => String -> m (SEXP V) install = io . installIO {-# 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 (SEXP V Foreign.R.Type.Char) @-} +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 (SEXP V Foreign.R.Type.String) @-} +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 a -> 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 @@ -146,15 +148,16 @@ evalEnv x rho = acquireSome =<< do 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 @@ -173,12 +176,13 @@ 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 +{-@ getErrorMessage :: TSEXP s Foreign.R.Type.Env -> m String @-} +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 . checkSEXPTYPE R.String =<< R.eval f env diff --git a/inline-r/src/Language/R/Internal.hs b/inline-r/src/Language/R/Internal.hs index 3aecf408..45bdf114 100644 --- a/inline-r/src/Language/R/Internal.hs +++ b/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 diff --git a/inline-r/src/Language/R/Internal.hs-boot b/inline-r/src/Language/R/Internal.hs-boot index 3457a22e..25489f8a 100644 --- a/inline-r/src/Language/R/Internal.hs-boot +++ b/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) diff --git a/inline-r/src/Language/R/Literal.hs b/inline-r/src/Language/R/Literal.hs index 7a7ccca6..8cc496a1 100644 --- a/inline-r/src/Language/R/Literal.hs +++ b/inline-r/src/Language/R/Literal.hs @@ -9,6 +9,7 @@ {-# Language FlexibleInstances #-} {-# Language FunctionalDependencies #-} {-# Language GADTs #-} +{-# Language KindSignatures #-} {-# Language LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -17,8 +18,11 @@ {-# Language ViewPatterns #-} -- required to not warn about IsVector usage. -{-# OPTIONS_GHC -fno-warn-redundant-constraints #-} +{-# OPTIONS_GHC -fno-warn-redundant-constraints -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.Literal + {- ( -- * Literals conversion Literal(..) , toPairList @@ -33,16 +37,20 @@ module Language.R.Literal , mkProtectedSEXPVectorIO -- * Internal , funToSEXP - ) where + ) -} where import Control.Memory.Region import Control.Monad.R.Class import qualified Data.Vector.SEXP as SVector import qualified Data.Vector.SEXP.Mutable as SMVector +import qualified Data.Vector.SEXP.Mutable as Mutable -- Needed to help LH name resolution +import Foreign.C -- Needed to help LH name resolution import qualified Foreign.R as R -import qualified Foreign.R.Internal as R (somesexp) -import Foreign.R.Type ( IsVector, SSEXPTYPE ) -import Foreign.R ( SEXP, SomeSEXP(..) ) +import Foreign.R.Type ( IsVector ) +import Foreign.R.Type.Singletons (SSEXPTYPE) +import Foreign.R ( SEXP ) +import GHC.ForeignPtr -- Needed to help LH name resolution +import GHC.ST -- Needed to help LH name resolution import Internal.Error import {-# SOURCE #-} Language.R.Internal (r1) import Language.R.Globals (nilValue) @@ -67,82 +75,117 @@ import qualified GHC.Foreign as GHC import GHC.IO.Encoding.UTF8 import System.IO.Unsafe ( unsafePerformIO ) +{-@ measure Language.R.Literal.literalRType :: a -> R.SEXPTYPE @-} + +{- +{-@ +class Literal a ty where + mkSEXPIO :: x:a -> IO (TSEXP V (literalRType x)) + fromSEXP :: forall s. x:SEXP s -> {v:a | literalRType v == typeOf x} + literalRType :: x:a -> {v:R.SEXPTYPE | v == literalRType x } +@-} + -- | Values that can be converted to 'SEXP'. -class SingI ty => Literal a ty | a -> ty where +class Literal a (ty :: R.SEXPTYPE) | a -> ty where -- | Internal function for converting a literal to a 'SEXP' value. You -- probably want to be using 'mkSEXP' instead. - mkSEXPIO :: a -> IO (SEXP V ty) - fromSEXP :: SEXP s ty -> a + mkSEXPIO :: a -> IO (SEXP V) + fromSEXP :: SEXP s -> a + literalRType :: a -> R.SEXPTYPE +-} + + + +{-@ +class Literal a ty where + literalRType :: x:a -> {v:R.SEXPTYPE | v == literalRType x } +ignore Literal [R.Logical] R.Logical +@-} + +-- | Values that can be converted to 'SEXP'. +class Literal a (ty :: R.SEXPTYPE) | a -> ty where + literalRType :: a -> R.SEXPTYPE + +instance Literal [R.Logical] 'R.Logical where + literalRType _ = R.Logical - default mkSEXPIO :: (IsVector ty, Literal [a] ty) => a -> IO (SEXP V ty) + +{- + default mkSEXPIO :: (IsVector ty, Literal [a] ty) => a -> IO (SEXP V) mkSEXPIO x = mkSEXPIO [x] - default fromSEXP :: (IsVector ty, Literal [a] ty) => SEXP s ty -> a + default fromSEXP :: (IsVector ty, Literal [a] ty) => SEXP s -> a fromSEXP (fromSEXP -> [x]) = x fromSEXP _ = failure "fromSEXP" "Not a singleton vector." -- | Create a SEXP value and protect it in current region -mkSEXP :: (Literal a b, MonadR m) => a -> m (SEXP (Region m) b) -mkSEXP x = acquire =<< io (mkSEXPIO x) - --- | Like 'fromSEXP', but with no static type satefy. Performs a dynamic --- (i.e. at runtime) check instead. -fromSomeSEXP :: forall s a form. (Literal a form) => R.SomeSEXP s -> a -fromSomeSEXP = fromSEXP . R.cast (sing :: Sing form) +{-@ assume mkSEXP :: x:a -> m (TSEXP (Region m) (literalRType x)) @-} +mkSEXP :: (Literal a b, MonadR m) => a -> m (SEXP (Region m)) +mkSEXP x = io (mkSEXPIO x) >>= \a -> acquire a -- | Like 'fromSomeSEXP', but behaves like the @as.*@ family of functions -- in R, by performing a best effort conversion to the target form (e.g. rounds -- reals to integers, etc) for atomic types. -dynSEXP :: forall a s ty. (Literal a ty) => SomeSEXP s -> a -dynSEXP (SomeSEXP sx) = - fromSomeSEXP $ unsafePerformIO $ case fromSing (sing :: SSEXPTYPE ty) of +dynSEXP :: forall a s ty. (Literal a ty) => SEXP s -> a +dynSEXP sx = + fromSEXP $ unsafePerformIO $ case literalRType (undefined :: a) of R.Char -> r1 "as.character" sx R.Int -> r1 "as.integer" sx R.Real -> r1 "as.double" sx R.Complex -> r1 "as.complex" sx R.Logical -> r1 "as.logical" sx R.Raw -> r1 "as.raw" sx - _ -> return $ SomeSEXP $ R.release sx + _ -> return $ R.release sx +-} {-# NOINLINE mkSEXPVector #-} -mkSEXPVector :: (Storable (SVector.ElemRep s a), IsVector a) - => SSEXPTYPE a - -> [IO (SVector.ElemRep s a)] - -> SEXP s a +{-@ mkSEXPVector :: vt:VSEXPTYPE s a -> [IO a] -> TSEXP s (vstypeOf vt) @-} +mkSEXPVector :: Storable a + => SVector.VSEXPTYPE s a + -> [IO a] + -> SEXP s mkSEXPVector ty allocators = unsafePerformIO $ mkSEXPVectorIO ty allocators -mkSEXPVectorIO :: (Storable (SVector.ElemRep s a), IsVector a) - => SSEXPTYPE a - -> [IO (SVector.ElemRep s a)] - -> IO (SEXP s a) +{-@ assume mkSEXPVectorIO :: vt:VSEXPTYPE s a -> [IO a] -> IO (TSEXP s (vstypeOf vt)) @-} +{-@ ignore mkSEXPVectorIO @-} +mkSEXPVectorIO :: Storable a + => SVector.VSEXPTYPE s a + -> [IO a] + -> IO (SEXP s) mkSEXPVectorIO ty allocators = - R.withProtected (R.allocVector ty $ length allocators) $ \vec -> do - let ptr = castPtr $ R.unsafeSEXPToVectorPtr vec + R.withProtected (R.allocVector (SVector.vstypeOf ty) $ length allocators) $ \vec -> do + let ptr = castPtr (R.unsafeSEXPToVectorPtr vec) zipWithM_ (\i -> (>>= pokeElemOff ptr i)) [0..] allocators return vec {-# NOINLINE mkProtectedSEXPVector #-} -mkProtectedSEXPVector :: IsVector b - => SSEXPTYPE b - -> [SEXP s a] - -> SEXP s b -mkProtectedSEXPVector ty xs = unsafePerformIO $ mkProtectedSEXPVectorIO ty xs - -mkProtectedSEXPVectorIO :: IsVector b - => SSEXPTYPE b - -> [SEXP s a] - -> IO (SEXP s b) +{-@ +mkProtectedSEXPVector :: vt:VSEXPTYPE s a -> [SEXP s] -> TSEXP s (vstypeOf vt) +@-} +mkProtectedSEXPVector :: SVector.VSEXPTYPE s a + -> [SEXP s] + -> SEXP s +mkProtectedSEXPVector ty xs = unsafePerformIO (mkProtectedSEXPVectorIO ty xs) + +{-@ +assume mkProtectedSEXPVectorIO :: vt:VSEXPTYPE s a -> [SEXP s] -> IO (TSEXP s (vstypeOf vt)) +ignore mkProtectedSEXPVectorIO +@-} +mkProtectedSEXPVectorIO :: SVector.VSEXPTYPE s a + -> [SEXP s] + -> IO (SEXP s) mkProtectedSEXPVectorIO ty xs = do mapM_ (void . R.protect) xs - z <- R.withProtected (R.allocVector ty $ length xs) $ \vec -> do - let ptr = castPtr $ R.unsafeSEXPToVectorPtr vec + z <- R.withProtected (R.allocVector (SVector.vstypeOf ty) $ length xs) $ \vec -> do + let ptr = castPtr (R.unsafeSEXPToVectorPtr vec) zipWithM_ (pokeElemOff ptr) [0..] xs return vec R.unprotect (length xs) return z +{- instance Literal [R.Logical] 'R.Logical where - mkSEXPIO = mkSEXPVectorIO sing . map return + mkSEXPIO = mkSEXPVectorIO SVector.VLogical . map return fromSEXP (hexp -> Logical v) = SVector.toList v instance Literal [Int32] 'R.Int where @@ -256,7 +299,8 @@ instance (NFData a, Literal a la) => HFunWrap (R s a) (IO R.SEXP0) where instance (Literal a la, HFunWrap b wb) => HFunWrap (a -> b) (R.SEXP0 -> wb) where - hFunWrap f a = hFunWrap $ f $! fromSEXP (R.cast sing (R.somesexp a) :: SEXP s la) + hFunWrap f a = hFunWrap $ f $! + fromSEXP (checkSEXPTYPE (literalRType (undefined :: a)) (R.SEXP a :: SEXP s la)) foreign import ccall "missing_r.h funPtrToSEXP" funPtrToSEXP :: FunPtr a -> IO (SEXP s 'R.ExtPtr) @@ -265,3 +309,4 @@ funToSEXP :: HFunWrap a b => (b -> IO (FunPtr b)) -> a -> IO (SEXP s 'R.ExtPtr) funToSEXP w x = funPtrToSEXP =<< w (hFunWrap x) $(thWrapperLiterals 3 12) +-}