git.iko.soy/Idris-dev
on 267f34d help sign in
Idris-dev/src/Core/Execute.hs
540 lines 24 kB history raw
1{-# LANGUAGE PatternGuards, ExistentialQuantification #-}
2module Core.Execute (execute) where
4import Idris.AbsSyntax
5import Idris.AbsSyntaxTree
6import IRTS.Lang(FType(..))
8import Idris.Primitives(Prim(..), primitives)
10import Core.TT
11import Core.Evaluate
12import Core.CaseTree
14import Debug.Trace
16import Util.DynamicLinker
17import Util.System
19import Control.Applicative hiding (Const)
20import Control.Monad.Trans
21import Control.Monad.Trans.State.Strict
22import Control.Monad.Trans.Error
23import Control.Monad
24import Data.Maybe
25import Data.Bits
26import qualified Data.Map as M
28import Foreign.LibFFI
29import Foreign.C.String
30import Foreign.Marshal.Alloc (free)
31import Foreign.Ptr
33import System.IO
35readMay :: (Read a) => String -> Maybe a
36readMay s = case reads s of
37 [(x, "")] -> Just x
38 _ -> Nothing
40data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show
42data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the result of evaluating "lazy" or calling lazy funcs
43 , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness
44 , exec_implicits :: Ctxt [PArg] -- ^ Necessary info on laziness from idris monad
45 , exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
46 }
48data ExecVal = EP NameType Name ExecVal
49 | EV Int
50 | EBind Name (Binder ExecVal) (ExecVal -> Exec ExecVal)
51 | EApp ExecVal ExecVal
52 | EType UExp
53 | EErased
54 | EConstant Const
55 | forall a. EPtr (Ptr a)
56 | EThunk Int
57 | EHandle Handle
59instance Show ExecVal where
60 show (EP _ n _) = show n
61 show (EV i) = "!!V" ++ show i ++ "!!"
62 show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"
63 show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
64 show (EType _) = "Type"
65 show EErased = "[__]"
66 show (EConstant c) = show c
67 show (EPtr p) = "<<ptr " ++ show p ++ ">>"
68 show (EThunk i) = "<<thunk " ++ show i ++ ">>"
69 show (EHandle h) = "<<handle " ++ show h ++ ">>"
71toTT :: ExecVal -> Exec Term
72toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
73toTT (EV i) = return $ V i
74toTT (EBind n b body) = do body' <- body $ EP Bound n EErased
75 b' <- fixBinder b
76 Bind n b' <$> toTT body'
77 where fixBinder (Lam t) = Lam <$> toTT t
78 fixBinder (Pi t) = Pi <$> toTT t
79 fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
80 fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2
81 fixBinder (Hole t) = Hole <$> toTT t
82 fixBinder (GHole t) = GHole <$> toTT t
83 fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
84 fixBinder (PVar t) = PVar <$> toTT t
85 fixBinder (PVTy t) = PVTy <$> toTT t
86toTT (EApp e1 e2) = do e1' <- toTT e1
87 e2' <- toTT e2
88 return $ App e1' e2'
89toTT (EType u) = return $ TType u
90toTT EErased = return Erased
91toTT (EConstant c) = return (Constant c)
92toTT (EThunk i) = return (P (DCon 0 0) (MN i "THUNK") Erased) --(force i) >>= toTT
93toTT (EHandle _) = return Erased
95unApplyV :: ExecVal -> (ExecVal, [ExecVal])
96unApplyV tm = ua [] tm
97 where ua args (EApp f a) = ua (a:args) f
98 ua args t = (t, args)
100mkEApp :: ExecVal -> [ExecVal] -> ExecVal
101mkEApp f [] = f
102mkEApp f (a:args) = mkEApp (EApp f a) args
104initState :: Idris ExecState
105initState = do ist <- getIState
106 return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)
108type Exec = ErrorT String (StateT ExecState IO)
110runExec :: Exec a -> ExecState -> IO (Either String a)
111runExec ex st = fst <$> runStateT (runErrorT ex) st
113getExecState :: Exec ExecState
114getExecState = lift get
116putExecState :: ExecState -> Exec ()
117putExecState = lift . put
119execFail :: String -> Exec a
120execFail = throwError
122execIO :: IO a -> Exec a
123execIO = lift . lift
125delay :: ExecEnv -> Context -> Term -> Exec ExecVal
126delay env ctxt tm =
127 do st <- getExecState
128 let i = exec_next_thunk st
129 putExecState $ st { exec_thunks = M.insert i (Delayed env ctxt tm) (exec_thunks st)
130 , exec_next_thunk = exec_next_thunk st + 1
131 }
132 return $ EThunk i
134force :: Int -> Exec ExecVal
135force i = do st <- getExecState
136 case M.lookup i (exec_thunks st) of
137 Just (Delayed env ctxt tm) -> do tm' <- doExec env ctxt tm
138 case tm' of
139 EThunk i ->
140 do res <- force i
141 update res i
142 return res
143 _ -> do update tm' i
144 return tm'
145 Just (Forced tm) -> return tm
146 Nothing -> execFail "Tried to exec non-existing thunk. This is a bug!"
147 where update :: ExecVal -> Int -> Exec ()
148 update tm i = do est <- getExecState
149 putExecState $ est { exec_thunks = M.insert i (Forced tm) (exec_thunks est) }
151tryForce :: ExecVal -> Exec ExecVal
152tryForce (EThunk i) = force i
153tryForce tm = return tm
155debugThunks :: Exec ()
156debugThunks = do st <- getExecState
157 execIO $ putStrLn (take 4000 (show (exec_thunks st)))
159execute :: Term -> Idris Term
160execute tm = do est <- initState
161 ctxt <- getContext
162 res <- lift $ flip runExec est $ do res <- doExec [] ctxt tm
163 toTT res
164 case res of
165 Left err -> fail err
166 Right tm' -> return tm'
168ioWrap :: ExecVal -> ExecVal
169ioWrap tm = mkEApp (EP (DCon 0 2) (UN "prim__IO") EErased) [EErased, tm]
171ioUnit :: ExecVal
172ioUnit = ioWrap (EP Ref unitCon EErased)
174type ExecEnv = [(Name, ExecVal)]
176doExec :: ExecEnv -> Context -> Term -> Exec ExecVal
177doExec env ctxt p@(P Ref n ty) | Just v <- lookup n env = return v
178doExec env ctxt p@(P Ref n ty) =
179 do let val = lookupDef n ctxt
180 case val of
181 [Function _ tm] -> doExec env ctxt tm
182 [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def
183 [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later
184 [CaseOp _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
185 doExec env ctxt tm
186 [CaseOp _ _ _ _ (CaseDefs _ (ns, sc) _ _)] -> return (EP Ref n EErased)
187 [] -> execFail $ "Could not find " ++ show n ++ " in definitions."
188 thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined
189doExec env ctxt p@(P Bound n ty) =
190 case lookup n env of
191 Nothing -> execFail "not found"
192 Just tm -> return tm
193doExec env ctxt (P (DCon a b) n _) = return (EP (DCon a b) n EErased)
194doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)
195doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))
196 | otherwise = execFail "env too small"
197doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v
198 doExec ((n, v'):env) ctxt body
199doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
200doExec env ctxt tm@(Bind n b body) = return $
201 EBind n (fmap (\_->EErased) b)
202 (\arg -> doExec ((n, arg):env) ctxt body)
203doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)
204doExec env ctxt (Constant c) = return (EConstant c)
205doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
206 doExec env ctxt ((x:xs) !! i)
207doExec env ctxt Erased = return EErased
208doExec env ctxt Impossible = fail "Tried to execute an impossible case"
209doExec env ctxt (TType u) = return (EType u)
211execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal
212execApp env ctxt (f, args) = do newF <- doExec env ctxt f
213 laziness <- (++ repeat False) <$> (getLaziness newF)
214 newArgs <- mapM argExec (zip args laziness)
215 execApp' env ctxt newF newArgs
216 where getLaziness (EP _ (UN "lazy") _) = return [False, True]
217 getLaziness (EP _ n _) = do est <- getExecState
218 let argInfo = exec_implicits est
219 case lookupCtxtName n argInfo of
220 [] -> return (repeat False)
221 [ps] -> return $ map lazyarg (snd ps)
222 many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)
223 getLaziness _ = return (repeat False) -- ok due to zip above
224 argExec :: (Term, Bool) -> Exec ExecVal
225 argExec (tm, False) = doExec env ctxt tm
226 argExec (tm, True) = delay env ctxt tm
229execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
230execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
231execApp' env ctxt (EP _ (UN "unsafePerformPrimIO") _) (ty:action:rest) | (prim__IO, [_, v]) <- unApplyV action =
232 execApp' env ctxt v rest
234execApp' env ctxt (EP _ (UN "prim_io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =
235 do v'' <- tryForce v'
236 res <- execApp' env ctxt k [v''] >>= tryForce
237 execApp' env ctxt res rest
238execApp' env ctxt con@(EP _ (UN "prim_io_return") _) args@(tp:v:rest) =
239 do v' <- tryForce v
240 execApp' env ctxt (mkEApp con [tp, v']) rest
242-- Special cases arising from not having access to the C RTS in the interpreter
243execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:EConstant (Str arg):_:rest)
244 | Just (FFun "putStr" _ _) <- foreignFromTT fn
245 = do execIO (putStr arg)
246 execApp' env ctxt ioUnit rest
247execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:_:EHandle h:_:rest)
248 | Just (FFun "idris_readStr" _ _) <- foreignFromTT fn
249 = do contents <- execIO $ hGetLine h
250 execApp' env ctxt (EConstant (Str (contents ++ "\n"))) rest
251execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
252 | Just (FFun "fileOpen" _ _) <- foreignFromTT fn
253 = do m <- case mode of
254 "r" -> return ReadMode
255 "w" -> return WriteMode
256 "a" -> return AppendMode
257 "rw" -> return ReadWriteMode
258 "wr" -> return ReadWriteMode
259 "r+" -> return ReadWriteMode
260 _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)
261 h <- execIO $ openFile f m
262 execApp' env ctxt (ioWrap (EHandle h)) (tail rest)
264execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:(EHandle h):rest)
265 | Just (FFun "fileEOF" _ _) <- foreignFromTT fn
266 = do eofp <- execIO $ hIsEOF h
267 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
268 execApp' env ctxt res (tail rest)
270execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:(EHandle h):rest)
271 | Just (FFun "fileClose" _ _) <- foreignFromTT fn
272 = do execIO $ hClose h
273 execApp' env ctxt ioUnit (tail rest)
275execApp' env ctxt (EP _ (UN "mkForeignPrim") _) (_:fn:(EPtr p):rest)
276 | Just (FFun "isNull" _ _) <- foreignFromTT fn
277 = let res = ioWrap . EConstant . I $
278 if p == nullPtr then 1 else 0
279 in execApp' env ctxt res (tail rest)
281-- Throw away the 'World' argument to the foreign function
283execApp' env ctxt f@(EP _ (UN "mkForeignPrim") _) args@(ty:fn:xs)
284 | Just (FFun f argTs retT) <- foreignFromTT fn
285 , length xs >= length argTs =
286 do let (args', xs') = (take (length argTs) xs, -- foreign args
287 drop (length argTs + 1) xs) -- rest
288 res <- stepForeign (ty:fn:args')
289 case res of
290 Nothing -> fail $ "Could not call foreign function \"" ++ f ++
291 "\" with args " ++ show args
292 Just r -> return (mkEApp r xs')
293 | otherwise = return (mkEApp f args)
295execApp' env ctxt c@(EP (DCon _ arity) n _) args =
296 do args' <- mapM tryForce (take arity args)
297 let restArgs = drop arity args
298 execApp' env ctxt (mkEApp c args') restArgs
300execApp' env ctxt c@(EP (TCon _ arity) n _) args =
301 do args' <- mapM tryForce (take arity args)
302 let restArgs = drop arity args
303 execApp' env ctxt (mkEApp c args') restArgs
305execApp' env ctxt f@(EP _ n _) args =
306 do let val = lookupDef n ctxt
307 case val of
308 [Function _ tm] -> fail "should already have been eval'd"
309 [TyDecl nt ty] -> return $ mkEApp f args
310 [Operator tp arity op] ->
311 if length args >= arity
312 then do args' <- mapM tryForce $ take arity args
313 case getOp n args' of
314 Just res -> do r <- res
315 execApp' env ctxt r (drop arity args)
316 Nothing -> return (mkEApp f args)
317 else return (mkEApp f args)
318 [CaseOp _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
319 do rhs <- doExec env ctxt tm
320 execApp' env ctxt rhs args
321 [CaseOp _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->
322 do res <- execCase env ctxt ns sc args
323 return $ fromMaybe (mkEApp f args) res
324 thing -> return $ mkEApp f args
325execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
326 let (f', as) = unApplyV ret
327 execApp' env ctxt f' (as ++ args)
328execApp' env ctxt (EThunk i) args = do f <- force i
329 execApp' env ctxt f args
330execApp' env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp' env ctxt f (args1 ++ args2)
331execApp' env ctxt f args = return (mkEApp f args)
333-- | Look up primitive operations in the global table and transform them into ExecVal functions
334getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
335getOp (UN "prim__believe_me") [_, _, x] = Just (return x)
336getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =
337 Just $ do line <- execIO getLine
338 return (EConstant (Str line))
339getOp (UN "prim__readString") [EHandle h] =
340 Just $ do contents <- execIO $ hGetLine h
341 return (EConstant (Str (contents ++ "\n")))
342getOp n args = getPrim n primitives >>= flip applyPrim args
343 where getPrim :: Name -> [Prim] -> Maybe ([ExecVal] -> Maybe ExecVal)
344 getPrim n [] = Nothing
345 getPrim n ((Prim pn _ arity def _ _) : prims) | n == pn = Just $ execPrim def
346 | otherwise = getPrim n prims
348 execPrim :: ([Const] -> Maybe Const) -> [ExecVal] -> Maybe ExecVal
349 execPrim f args = EConstant <$> (mapM getConst args >>= f)
351 getConst (EConstant c) = Just c
352 getConst _ = Nothing
354 applyPrim :: ([ExecVal] -> Maybe ExecVal) -> [ExecVal] -> Maybe (Exec ExecVal)
355 applyPrim fn args = return <$> fn args
360-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
361-- evaluates them, then begins the checks for matching cases.
362execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
363execCase env ctxt ns sc args =
364 let arity = length ns in
365 if arity <= length args
366 then do let amap = zip ns args
367-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()
368 caseRes <- execCase' env ctxt amap sc
369 case caseRes of
370 Just res -> Just <$> execApp' (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)
371 Nothing -> return Nothing
372 else return Nothing
374-- | Take bindings and a case tree and examines them, executing the matching case if possible.
375execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
376execCase' env ctxt amap (UnmatchedCase _) = return Nothing
377execCase' env ctxt amap (STerm tm) =
378 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm
379execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
380 do tm' <- tryForce tm
381 case chooseAlt tm' alts of
382 Just (newCase, newBindings) ->
383 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
384 execCase' env ctxt amap' newCase
385 Nothing -> return Nothing
387chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
388chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])
389chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
390chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm
391 , cn == n = Just (sc, zip ns args)
392 | otherwise = chooseAlt tm alts
393chooseAlt tm (_:alts) = chooseAlt tm alts
394chooseAlt _ [] = Nothing
399idrisType :: FType -> ExecVal
400idrisType FUnit = EP Ref unitTy EErased
401idrisType ft = EConstant (idr ft)
402 where idr (FArith ty) = AType ty
403 idr FString = StrType
404 idr FPtr = PtrType
406data Foreign = FFun String [FType] FType deriving Show
409call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
410call (FFun name argTypes retType) args =
411 do fn <- findForeign name
412 case fn of
413 Nothing -> return Nothing
414 Just f -> do res <- call' f args retType
415 return . Just . ioWrap $ res
416 where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal
417 call' (Fun _ h) args (FArith (ATInt ITNative)) = do
418 res <- execIO $ callFFI h retCInt (prepArgs args)
419 return (EConstant (I (fromIntegral res)))
420 call' (Fun _ h) args (FArith (ATInt (ITFixed IT8))) = do
421 res <- execIO $ callFFI h retCChar (prepArgs args)
422 return (EConstant (B8 (fromIntegral res)))
423 call' (Fun _ h) args (FArith (ATInt (ITFixed IT16))) = do
424 res <- execIO $ callFFI h retCWchar (prepArgs args)
425 return (EConstant (B16 (fromIntegral res)))
426 call' (Fun _ h) args (FArith (ATInt (ITFixed IT32))) = do
427 res <- execIO $ callFFI h retCInt (prepArgs args)
428 return (EConstant (B32 (fromIntegral res)))
429 call' (Fun _ h) args (FArith (ATInt (ITFixed IT64))) = do
430 res <- execIO $ callFFI h retCLong (prepArgs args)
431 return (EConstant (B64 (fromIntegral res)))
432 call' (Fun _ h) args (FArith ATFloat) = do
433 res <- execIO $ callFFI h retCDouble (prepArgs args)
434 return (EConstant (Fl (realToFrac res)))
435 call' (Fun _ h) args (FArith (ATInt ITChar)) = do
436 res <- execIO $ callFFI h retCChar (prepArgs args)
437 return (EConstant (Ch (castCCharToChar res)))
438 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
439 hStr <- execIO $ peekCString res
440-- lift $ free res
441 return (EConstant (Str hStr))
443 call' (Fun _ h) args FPtr = do res <- execIO $ callFFI h (retPtr retVoid) (prepArgs args)
444 return (EPtr res)
445 call' (Fun _ h) args FUnit = do res <- execIO $ callFFI h retVoid (prepArgs args)
446 return (EP Ref unitCon EErased)
447-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
450 prepArgs = map prepArg
451 prepArg (EConstant (I i)) = argCInt (fromIntegral i)
452 prepArg (EConstant (B8 i)) = argCChar (fromIntegral i)
453 prepArg (EConstant (B16 i)) = argCWchar (fromIntegral i)
454 prepArg (EConstant (B32 i)) = argCInt (fromIntegral i)
455 prepArg (EConstant (B64 i)) = argCLong (fromIntegral i)
456 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)
457 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
458 prepArg (EConstant (Str s)) = argString s
459 prepArg (EPtr p) = argPtr p
460 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined
464foreignFromTT :: ExecVal -> Maybe Foreign
465foreignFromTT t = case (unApplyV t) of
466 (_, [(EConstant (Str name)), args, ret]) ->
467 do argTy <- unEList args
468 argFTy <- sequence $ map getFTy argTy
469 retFTy <- getFTy ret
470 return $ FFun name argFTy retFTy
471 _ -> trace "failed to construct ffun" Nothing
473getFTy :: ExecVal -> Maybe FType
474getFTy (EApp (EP _ (UN "FIntT") _) (EP _ (UN intTy) _)) =
475 case intTy of
476 "ITNative" -> Just (FArith (ATInt ITNative))
477 "ITChar" -> Just (FArith (ATInt ITChar))
478 "IT8" -> Just (FArith (ATInt (ITFixed IT8)))
479 "IT16" -> Just (FArith (ATInt (ITFixed IT16)))
480 "IT32" -> Just (FArith (ATInt (ITFixed IT32)))
481 "IT64" -> Just (FArith (ATInt (ITFixed IT64)))
482 _ -> Nothing
483getFTy (EP _ (UN t) _) =
484 case t of
485 "FFloat" -> Just (FArith ATFloat)
486 "FString" -> Just FString
487 "FPtr" -> Just FPtr
488 "FUnit" -> Just FUnit
489 _ -> Nothing
490getFTy _ = Nothing
492unList :: Term -> Maybe [Term]
493unList tm = case unApply tm of
494 (nil, [_]) -> Just []
495 (cons, ([_, x, xs])) ->
496 do rest <- unList xs
497 return $ x:rest
498 (f, args) -> Nothing
500unEList :: ExecVal -> Maybe [ExecVal]
501unEList tm = case unApplyV tm of
502 (nil, [_]) -> Just []
503 (cons, ([_, x, xs])) ->
504 do rest <- unEList xs
505 return $ x:rest
506 (f, args) -> Nothing
509toConst :: Term -> Maybe Const
510toConst (Constant c) = Just c
511toConst _ = Nothing
513stepForeign :: [ExecVal] -> Exec (Maybe ExecVal)
514stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
515 f' <- case (call <$> ffun) of
516 Just f -> f args
517 Nothing -> return Nothing
518 return f'
519stepForeign _ = fail "Tried to call foreign function that wasn't mkForeignPrim"
521mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
522mapMaybeM f [] = return []
523mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
524 x' <- f x
525 case x' of
526 Just x'' -> return (x'':rest)
527 Nothing -> return rest
529findForeign :: String -> Exec (Maybe ForeignFun)
530findForeign fn = do est <- getExecState
531 let libs = exec_dynamic_libs est
532 fns <- mapMaybeM getFn libs
533 case fns of
534 [f] -> return (Just f)
535 [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"
536 return Nothing
537 fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
538 show (length fs) ++ " occurrences."
539 return Nothing
540 where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)