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