git.iko.soy/Idris-dev
on 22d09c9 help sign in
Idris-dev/src/Core/Execute.hs
144 lines 6.3 kB history raw
1module Core.Execute (execute) where
3import Idris.AbsSyntax
4import Idris.AbsSyntaxTree
6import Core.TT
7import Core.Evaluate
9import Debug.Trace
11import Util.DynamicLinker
13import Control.Applicative hiding (Const)
14import Control.Monad.Trans
15import Control.Monad
16import Data.Maybe
18import Foreign.LibFFI
19import Foreign.C.String
20import Foreign.Marshal.Alloc (free)
22-- | Attempt to perform a side effect. Return either Just the next step in
23-- evaluation (after performing the side effect through IO), or Nothing if no
24-- IO was performed.
25--
26-- This function is exceedingly generous about what it will accept in order to
27-- enable convenient testing at the REPL.
28step :: TT Name -> Idris (Maybe (TT Name))
29step tm = step' (unApply tm)
30 where step' (P _ (UN "unsafePerformIO") _, [_, arg] ) = step arg -- Only step if arg can be stepped
31 step' (P _ (UN "mkForeign") _, args) = stepForeign args
32 step' (P _ (UN "prim__IO") _, [_, arg]) = return (Just arg)
33 step' (P _ (UN "prim__readString") _, [(P _ (UN "prim__stdin") _)]) =
34 do line <- lift $ getLine
35 return . Just . Constant . Str $ line
36 step' _ = return Nothing
38-- | Perform side effects until no more can be performed, then return the
39-- resulting term (possibly the argument).
40execute :: TT Name -> Idris (TT Name)
41execute tm = case unApply tm of
42 (P _ (UN "unsafePerformIO") _, [_, arg] ) -> execute' arg
43 _ -> return tm
44 where execute' tm = do stepped <- step tm
45 case stepped of
46 Nothing -> return tm
47 Just tm' -> execute' tm'
51data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
53data Foreign = FFun String [FTy] FTy deriving Show
55call :: Foreign -> [TT Name] -> Idris (Maybe (TT Name))
56call (FFun name argTypes retType) args = do fn <- findForeign name
57 case fn of
58 Nothing -> return Nothing
59 Just f -> return . Just =<< call' f args retType
60 where call' :: ForeignFun -> [TT Name] -> FTy -> Idris (TT Name)
61 call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)
62 return (Constant (I (fromIntegral res)))
63 call' (Fun _ h) args FFloat = do res <- lift $ callFFI h retCDouble (prepArgs args)
64 return (Constant (Fl (realToFrac res)))
65 call' (Fun _ h) args FChar = do res <- lift $ callFFI h retCChar (prepArgs args)
66 return (Constant (Ch (castCCharToChar res)))
67 call' (Fun _ h) args FString = do res <- lift $ callFFI h retCString (prepArgs args)
68 hStr <- lift $ peekCString res
69-- lift $ free res
70 return (Constant (Str hStr))
71-- awaiting Const constructor for pointers
72-- call' (Fun _ h) args FPtr = do res <- lift $ callFFI h retPtr (prepArgs args)
73-- return (Constant (Ch (castCCharToChar res)))
74 call' (Fun _ h) args FUnit = do res <- lift $ callFFI h retVoid (prepArgs args)
75 return (P Ref unitCon (P Ref unitTy (TType (UVal 0)))) -- FIXME check universe level
77 prepArgs = map prepArg
78 prepArg (Constant (I i)) = argCInt (fromIntegral i)
79 prepArg (Constant (Fl f)) = argCDouble (realToFrac f)
80 prepArg (Constant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
81 prepArg (Constant (Str s)) = argString s
85foreignFromTT :: TT Name -> Maybe Foreign
86foreignFromTT t = case (unApply t) of
87 (_, [(Constant (Str name)), args, ret]) ->
88 do argTy <- unList args
89 argFTy <- sequence $ map getFTy argTy
90 retFTy <- getFTy ret
91 return $ FFun name argFTy retFTy
92 _ -> Nothing
94getFTy :: TT Name -> Maybe FTy
95getFTy (P _ (UN t) _) = case t of
96 "FInt" -> Just FInt
97 "FFloat" -> Just FFloat
98 "FChar" -> Just FChar
99 "FString" -> Just FString
100 "FPtr" -> Just FPtr
101 "FUnit" -> Just FUnit
102 _ -> Nothing
103getFTy _ = Nothing
105unList :: TT Name -> Maybe [TT Name]
106unList tm = case unApply tm of
107 (nil, [_]) -> Just []
108 (cons, ([_, x, xs])) ->
109 do rest <- unList xs
110 return $ x:rest
111 (f, args) -> Nothing
113toConst :: TT Name -> Maybe Const
114toConst (Constant c) = Just c
115toConst _ = Nothing
117stepForeign :: [TT Name] -> Idris (Maybe (TT Name))
118stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
119 f' <- case (call <$> ffun) of
120 Just f -> f args
121 Nothing -> return Nothing
122 return f'
123stepForeign _ = fail "Tried to call foreign function that wasn't mkForeign"
125mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
126mapMaybeM f [] = return []
127mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
128 x' <- f x
129 case x' of
130 Just x'' -> return (x'':rest)
131 Nothing -> return rest
133findForeign :: String -> Idris (Maybe ForeignFun)
134findForeign fn = do i <- getIState
135 let libs = idris_dynamic_libs i
136 fns <- mapMaybeM (lift . tryLoadFn fn) libs
137 case fns of
138 [f] -> return (Just f)
139 [] -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" not found"
140 return Nothing
141 fs -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
142 show (length fs) ++ " occurrences."
143 return Nothing