@@ -22,6 +22,7 @@ import qualified Data.Map as M
2222import Foreign.LibFFI
2323import Foreign.C.String
2424import Foreign.Marshal.Alloc (free)
25+import Foreign.Ptr
2526
2627import System.IO
2728
@@ -175,6 +176,22 @@ idrisType ft = Constant (idr ft)
175176
176177data Foreign = FFun String [FTy] FTy deriving Show
177178
179+-- | A representation of Ptr values, which otherwise don't work in TT
180+ptrCon :: Name
181+ptrCon = MN 0 "__Ptr"
182+
183+-- | Convert a Haskell pointer to a Ptr term in TT
184+ptr :: Ptr a -> Term
185+ptr p = App (P (DCon 1 0) ptrCon Erased) (Constant (I (addr p)))
186+ where addr p = p `minusPtr` nullPtr
187+
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
192+unPtr _ = Nothing
193+
194+
178195call :: Foreign -> [Term] -> Idris (Maybe Term)
179196call (FFun name argTypes retType) args =
180197 do fn <- findForeign name
@@ -193,17 +210,20 @@ call (FFun name argTypes retType) args =
193210 hStr <- lift $ peekCString res
194211-- lift $ free res
195212 return (Constant (Str hStr))
196−-- awaiting Const constructor for pointers
197−-- call' (Fun _ h) args FPtr = do res <- lift $ callFFI h retPtr (prepArgs args)
198−-- return (Constant (Ch (castCCharToChar res)))
213+
214+ call' (Fun _ h) args FPtr = do res <- lift $ callFFI h (retPtr retVoid) (prepArgs args)
215+ return (ptr res)
199216 call' (Fun _ h) args FUnit = do res <- lift $ callFFI h retVoid (prepArgs args)
200217 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)
219+
201220
202221 prepArgs = map prepArg
203222 prepArg (Constant (I i)) = argCInt (fromIntegral i)
204223 prepArg (Constant (Fl f)) = argCDouble (realToFrac f)
205224 prepArg (Constant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
206225 prepArg (Constant (Str s)) = argString s
226+ prepArg ptr | Just p <- unPtr ptr = argPtr p
207227 prepArg other = trace ("Could not use " ++ show other ++ " as FFI arg.") undefined
208228
209229