Skip to content

Commit

Permalink
Add specs for Data.Vector.SEXP.Mutable
Browse files Browse the repository at this point in the history
  • Loading branch information
facundominguez committed Dec 7, 2023
1 parent 621d6a1 commit 1c455b6
Show file tree
Hide file tree
Showing 6 changed files with 265 additions and 125 deletions.
8 changes: 4 additions & 4 deletions inline-r/inline-r.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -48,8 +48,8 @@ library
exposed-modules:
Control.Memory.Region
-- Data.Vector.SEXP
-- Data.Vector.SEXP.Base
-- Data.Vector.SEXP.Mutable
Data.Vector.SEXP.Base
Data.Vector.SEXP.Mutable
Foreign.R
Foreign.R.Constraints
Foreign.R.Context
Expand Down Expand Up @@ -79,8 +79,8 @@ library
-- Language.R.Event
other-modules:
Control.Monad.R.Class
-- Control.Monad.R.Internal
-- Data.Vector.SEXP.Mutable.Internal
Control.Monad.R.Internal
Data.Vector.SEXP.Mutable.Internal
Internal.Error
build-depends:
base >=4.7 && <5,
Expand Down
9 changes: 9 additions & 0 deletions inline-r/src/Control/Memory/Region.hs
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,11 @@
-- of an object. That is, regions have scopes, and objects within a region are
-- guaranteed to remain live within the scope of that region.

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Control.Memory.Region where

Expand Down Expand Up @@ -35,3 +38,9 @@ type family a <= b :: Constraint
type instance a <= a = ()
type instance a <= G = ()
type instance V <= b = ()

-- | An alias for (<=).
--
-- XXX: LH complains when using (<=) in type signatures
class SubRegion s' s where
instance s' <= s => SubRegion s' s where
9 changes: 7 additions & 2 deletions inline-r/src/Control/Monad/R/Internal.hs
Original file line number Diff line number Diff line change
Expand Up @@ -12,14 +12,13 @@ import Control.Memory.Region
import Control.Monad.R.Class
import Data.Proxy (Proxy(..))
import Data.Reflection (Reifies, reify)
import Foreign.R (SEXP)
import Foreign.R.Context -- XXX: Needed to help LH name resolution
import Foreign.R.Internal -- XXX: Needed to help LH name resolution

{-@ type AcquireIO s = forall <p :: SEXP s -> Bool > . (SEXP V)<p> -> IO ((SEXP s)<p>) @-}
type AcquireIO s = SEXP V -> IO (SEXP s)

-- XXX: It is not possible to give a specification to withAcquire.
-- XXX: It is not possible to give a specification in LH to withAcquire.
-- Apparently the constraints of the nested function can't be expressed in
-- specs.
withAcquire
Expand All @@ -30,3 +29,9 @@ withAcquire
withAcquire f = do
cxt <- getExecContext
reify (\sx -> unsafeRunWithExecContext (acquire sx) cxt) f

getAcquireIO
:: MonadR m => m (AcquireIO (Region m))
getAcquireIO = do
cxt <- getExecContext
return (\sx -> unsafeRunWithExecContext (acquire sx) cxt)
15 changes: 9 additions & 6 deletions inline-r/src/Data/Vector/SEXP/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
-- Copyright: (C) 2013 Amgen, Inc.
--

{-# OPTIONS_GHC -fplugin-opt=LiquidHaskell:--skip-module=False #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
Expand All @@ -11,7 +12,9 @@ module Data.Vector.SEXP.Base where
import Control.Memory.Region

import Foreign.R.Type
import Foreign.R (SEXP, SomeSEXP)
import Foreign.R.Context -- XXX: needed to help LH name resolution
import Foreign.R.Internal -- XXX: needed to help LH name resolution
import Foreign.R (SEXP)

import Data.Singletons (SingI)

Expand All @@ -28,16 +31,16 @@ type family ElemRep s (a :: SEXPTYPE) where
ElemRep s 'Int = Int32
ElemRep s 'Real = Double
ElemRep s 'Complex = Complex Double
ElemRep s 'String = SEXP s 'Char
ElemRep s 'Vector = SomeSEXP s
ElemRep s 'Expr = SomeSEXP s
ElemRep s 'String = SEXP s -- SEXP s 'Char
ElemRep s 'Vector = SEXP s
ElemRep s 'Expr = SEXP s
ElemRep s 'Raw = Word8

-- | 'ElemRep' in the form of a relation, for convenience.
type E s a b = ElemRep s a ~ b

-- | Constraint synonym for all operations on vectors.
type VECTOR s ty a = (Storable a, IsVector ty, SingI ty)
-- Constraint synonym for all operations on vectors.
-- type VECTOR s ty a = (Storable a, IsVector ty, SingI ty)

-- | Constraint synonym for all operations on vectors.
type SVECTOR ty a = (Storable a, IsVector ty, SingI ty, ElemRep V ty ~ a)
Loading

0 comments on commit 1c455b6

Please sign in to comment.