@@ -10,10 +10,14 @@ import Debug.Trace
11import Util.DynamicLinker
11import Util.DynamicLinker
13+import Control.Applicative hiding (Const)
13import Control.Monad.Trans
14import Control.Monad.Trans
14import Control.Monad
15import Control.Monad
15import Data.Maybe
16import Data.Maybe
19+import Foreign.C.String
20+import Foreign.Marshal.Alloc (free)
18-- | Attempt to perform a side effect. Return either Just the next step in
22-- | Attempt to perform a side effect. Return either Just the next step in
19-- evaluation (after performing the side effect through IO), or Nothing if no
23-- evaluation (after performing the side effect through IO), or Nothing if no
@@ -21,8 +25,7 @@ import Data.Maybe
21step :: TT Name -> Idris (Maybe (TT Name))
25step :: TT Name -> Idris (Maybe (TT Name))
22step tm = step' (unApply tm)
26step tm = step' (unApply tm)
23 where step' (P _ (UN "unsafePerformIO") _, [_, arg] ) = return $ Just arg
27 where step' (P _ (UN "unsafePerformIO") _, [_, arg] ) = return $ Just arg
24− step' (P _ (UN "mkForeign") _, args) = do newTerm <- stepForeign args
28+ step' (P _ (UN "mkForeign") _, args) = stepForeign args
26 step' _ = return Nothing
29 step' _ = return Nothing
28-- | Perform side effects until no more can be performed, then return the
31-- | Perform side effects until no more can be performed, then return the
@@ -39,8 +42,37 @@ data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
40data Foreign = FFun String [FTy] FTy deriving Show
43data Foreign = FFun String [FTy] FTy deriving Show
42−call :: Foreign -> [TT Name] -> Idris (TT Name)
45+call :: Foreign -> [TT Name] -> Idris (Maybe (TT Name))
43−call (FFun name argTypes retType) args = undefined
46+call (FFun name argTypes retType) args = do fn <- findForeign name
48+ Nothing -> return Nothing
49+ Just f -> do res <- call' f args retType
51+ where call' :: ForeignFun -> [TT Name] -> FTy -> Idris (TT Name)
52+ call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)
53+ return (Constant (I (fromIntegral res)))
54+ call' (Fun _ h) args FFloat = do res <- lift $ callFFI h retCDouble (prepArgs args)
55+ return (Constant (Fl (realToFrac res)))
56+ call' (Fun _ h) args FChar = do res <- lift $ callFFI h retCChar (prepArgs args)
57+ return (Constant (Ch (castCCharToChar res)))
58+ call' (Fun _ h) args FString = do res <- lift $ callFFI h retCString (prepArgs args)
59+ hStr <- lift $ peekCString res
61+ return (Constant (Str hStr))
62+-- awaiting Const constructor for pointers
63+-- call' (Fun _ h) args FPtr = do res <- lift $ callFFI h retPtr (prepArgs args)
64+-- return (Constant (Ch (castCCharToChar res)))
65+ call' (Fun _ h) args FUnit = do res <- lift $ callFFI h retVoid (prepArgs args)
66+ return (P Ref unitCon (P Ref unitTy (TType (UVal 0)))) -- FIXME check universe level
69+ prepArgs = map prepArg
70+ prepArg (Constant (I i)) = argCInt (fromIntegral i)
71+ prepArg (Constant (Fl f)) = argCDouble (realToFrac f)
72+ prepArg (Constant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
73+ prepArg (Constant (Str s)) = argString s
45foreignFromTT :: TT Name -> Maybe Foreign
77foreignFromTT :: TT Name -> Maybe Foreign
46foreignFromTT t = case (unApply t) of
78foreignFromTT t = case (unApply t) of
@@ -74,11 +106,12 @@ toConst :: TT Name -> Maybe Const
74toConst (Constant c) = Just c
106toConst (Constant c) = Just c
75toConst _ = Nothing
107toConst _ = Nothing
77−stepForeign :: [TT Name] -> Idris (TT Name)
109+stepForeign :: [TT Name] -> Idris (Maybe (TT Name))
78−stepForeign (ty:fn:args) = do iputStrLn $ show $ foreignFromTT fn
110+stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
79− iputStrLn $ show $ sequence $ map toConst args
111+ f' <- case (call <$> ffun) of
80− iputStrLn ""
112+ Just f -> f args
81− return $ mkApp (P Bound (UN "mkForeign") Erased) args
113+ Nothing -> return Nothing
82stepForeign _ = fail "Tried to call foreign function that wasn't mkForeign"
115stepForeign _ = fail "Tried to call foreign function that wasn't mkForeign"
84mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
117mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
@@ -95,4 +128,9 @@ findForeign fn = do i <- getIState
95 fns <- mapMaybeM (lift . tryLoadFn fn) libs
128 fns <- mapMaybeM (lift . tryLoadFn fn) libs
96 case fns of
129 case fns of
97 [f] -> return (Just f)
130 [f] -> return (Just f)
131+ [] -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" not found"
133+ fs -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
134+ show (length fs) ++ " occurrences."
98− _ -> return Nothing
135+ return Nothing