@@ -8,6 +8,10 @@ import Core.Evaluate
88
99import Debug.Trace
1010
11+import Foreign.LibFFI
12+import Foreign.Ptr (nullPtr)
13+import System.Posix.DynamicLinker
14+
1115-- | Attempt to perform a side effect. Return either Just the next step in
1216-- evaluation (after performing the side effect through IO), or Nothing if no
1317-- IO was performed.
@@ -26,7 +30,45 @@ execute tm = do stepped <- step tm
2630 Nothing -> return tm
2731 Just tm' -> execute tm'
2832
33+data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving Show
34+
35+data Foreign = FFun String [FTy] FTy deriving Show
36+
37+call :: Foreign -> [TT Name] -> Idris (TT Name)
38+call (FFun name argTypes retType) args = undefined
39+
40+foreignFromTT :: TT Name -> Maybe Foreign
41+foreignFromTT t = case (unApply t) of
42+ (_, [(Constant (Str name)), args, ret]) ->
43+ do trace (show $ unList args) $ return ()
44+ argTy <- unList args
45+ argFTy <- sequence $ map getFTy argTy
46+ retFTy <- getFTy ret
47+ return $ FFun name argFTy retFTy
48+ _ -> Nothing
49+
50+getFTy :: TT Name -> Maybe FTy
51+getFTy (P _ (UN t) _) = case t of
52+ "FInt" -> Just FInt
53+ "FFloat" -> Just FFloat
54+ "FChar" -> Just FChar
55+ "FString" -> Just FString
56+ "FPtr" -> Just FPtr
57+ "FUnit" -> Just FUnit
58+ _ -> Nothing
59+getFTy _ = Nothing
60+
61+unList :: TT Name -> Maybe [TT Name]
62+unList tm = case unApply tm of
63+ (nil, [_]) -> Just []
64+ (cons, ([_, x, xs])) ->
65+ do rest <- unList xs
66+ return $ x:rest
67+ (f, args) -> Nothing
2968
3069stepForeign :: [TT Name] -> Idris (TT Name)
31−stepForeign args = do iputStrLn $ "FOREIGN CALL" ++ show args
32− return $ mkApp (P Bound (UN "mkForeign") Erased) args
70+stepForeign (ty:fn:args) = do iputStrLn $ "FOREIGN CALL " ++ show (ty:fn:args)
71+ iputStrLn $ show $ foreignFromTT fn
72+ iputStrLn ""
73+ return $ mkApp (P Bound (UN "mkForeign") Erased) args
74+stepForeign _ = fail "Tried to call foreign function that wasn't mkForeign"