@@ -22,6 +22,7 @@ import qualified Data.Map as M
22import Foreign.LibFFI
22import Foreign.LibFFI
23import Foreign.C.String
23import Foreign.C.String
24import Foreign.Marshal.Alloc (free)
24import Foreign.Marshal.Alloc (free)
26import System.IO
27import System.IO
@@ -175,6 +176,22 @@ idrisType ft = Constant (idr ft)
176data Foreign = FFun String [FTy] FTy deriving Show
177data Foreign = FFun String [FTy] FTy deriving Show
179+-- | A representation of Ptr values, which otherwise don't work in TT
181+ptrCon = MN 0 "__Ptr"
183+-- | Convert a Haskell pointer to a Ptr term in TT
185+ptr p = App (P (DCon 1 0) ptrCon Erased) (Constant (I (addr p)))
186+ where addr p = p `minusPtr` nullPtr
188+-- | Convert a Ptr term in TT to a Haskell pointer
189+unPtr :: Term -> Maybe (Ptr a)
190+unPtr (App (P _ con _) (Constant (I addr))) | con == ptrCon = Just (unAddr addr)
191+ where unAddr a = nullPtr `plusPtr` a
178call :: Foreign -> [Term] -> Idris (Maybe Term)
195call :: Foreign -> [Term] -> Idris (Maybe Term)
179call (FFun name argTypes retType) args =
196call (FFun name argTypes retType) args =
180 do fn <- findForeign name
197 do fn <- findForeign name
@@ -193,17 +210,20 @@ call (FFun name argTypes retType) args =
193 hStr <- lift $ peekCString res
210 hStr <- lift $ peekCString res
194-- lift $ free res
211-- lift $ free res
195 return (Constant (Str hStr))
212 return (Constant (Str hStr))
196−-- awaiting Const constructor for pointers
213+
197−-- call' (Fun _ h) args FPtr = do res <- lift $ callFFI h retPtr (prepArgs args)
214+ call' (Fun _ h) args FPtr = do res <- lift $ callFFI h (retPtr retVoid) (prepArgs args)
198−-- return (Constant (Ch (castCCharToChar res)))
215+ return (ptr res)
199 call' (Fun _ h) args FUnit = do res <- lift $ callFFI h retVoid (prepArgs args)
216 call' (Fun _ h) args FUnit = do res <- lift $ callFFI h retVoid (prepArgs args)
200 return (P Ref unitCon (P Ref unitTy (TType (UVal 0)))) -- FIXME check universe level
217 return (P Ref unitCon (P Ref unitTy (TType (UVal 0)))) -- FIXME check universe level
218+-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
202 prepArgs = map prepArg
221 prepArgs = map prepArg
203 prepArg (Constant (I i)) = argCInt (fromIntegral i)
222 prepArg (Constant (I i)) = argCInt (fromIntegral i)
204 prepArg (Constant (Fl f)) = argCDouble (realToFrac f)
223 prepArg (Constant (Fl f)) = argCDouble (realToFrac f)
205 prepArg (Constant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
224 prepArg (Constant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
206 prepArg (Constant (Str s)) = argString s
225 prepArg (Constant (Str s)) = argString s
226+ prepArg ptr | Just p <- unPtr ptr = argPtr p
207 prepArg other = trace ("Could not use " ++ show other ++ " as FFI arg.") undefined
227 prepArg other = trace ("Could not use " ++ show other ++ " as FFI arg.") undefined