git.iko.soy/Idris-dev
on d1de0f4 help sign in
Idris-dev/src/Core/Execute.hs
543 lines 25 kB history raw
1{-# LANGUAGE PatternGuards, ExistentialQuantification #-}
2module Core.Execute (execute) where
4import Idris.AbsSyntax
5import Idris.AbsSyntaxTree
7import Core.TT
8import Core.Evaluate
9import Core.CaseTree
11import Debug.Trace
13import Util.DynamicLinker
14import Util.System
16import Control.Applicative hiding (Const)
17import Control.Monad.Trans
18import Control.Monad.Trans.State.Strict
19import Control.Monad.Trans.Error
20import Control.Monad
21import Data.Maybe
22import Data.Bits
23import qualified Data.Map as M
25import Foreign.LibFFI
26import Foreign.C.String
27import Foreign.Marshal.Alloc (free)
28import Foreign.Ptr
30import System.IO
33data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show
35data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the result of evaluating "lazy" or calling lazy funcs
36 , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness
37 , exec_implicits :: Ctxt [PArg] -- ^ Necessary info on laziness from idris monad
38 , exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
39 }
41data ExecVal = EP NameType Name ExecVal
42 | EV Int
43 | EBind Name (Binder ExecVal) (ExecVal -> Exec ExecVal)
44 | EApp ExecVal ExecVal
45 | EType UExp
46 | EErased
47 | EConstant Const
48 | forall a. EPtr (Ptr a)
49 | EThunk Int
50 | EHandle Handle
52instance Show ExecVal where
53 show (EP _ n _) = show n
54 show (EV i) = "!!V" ++ show i ++ "!!"
55 show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"
56 show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
57 show (EType _) = "Type"
58 show EErased = "[__]"
59 show (EConstant c) = show c
60 show (EPtr p) = "<<ptr " ++ show p ++ ">>"
61 show (EThunk i) = "<<thunk " ++ show i ++ ">>"
62 show (EHandle h) = "<<handle " ++ show h ++ ">>"
64toTT :: ExecVal -> Exec Term
65toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
66toTT (EV i) = return $ V i
67toTT (EBind n b body) = do body' <- body $ EP Bound n EErased
68 b' <- fixBinder b
69 Bind n b' <$> toTT body'
70 where fixBinder (Lam t) = Lam <$> toTT t
71 fixBinder (Pi t) = Pi <$> toTT t
72 fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
73 fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2
74 fixBinder (Hole t) = Hole <$> toTT t
75 fixBinder (GHole t) = GHole <$> toTT t
76 fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
77 fixBinder (PVar t) = PVar <$> toTT t
78 fixBinder (PVTy t) = PVTy <$> toTT t
79toTT (EApp e1 e2) = do e1' <- toTT e1
80 e2' <- toTT e2
81 return $ App e1' e2'
82toTT (EType u) = return $ TType u
83toTT EErased = return Erased
84toTT (EConstant c) = return (Constant c)
85toTT (EThunk i) = return (P (DCon 0 0) (MN i "THUNK") Erased) --(force i) >>= toTT
86toTT (EHandle _) = return Erased
88unApplyV :: ExecVal -> (ExecVal, [ExecVal])
89unApplyV tm = ua [] tm
90 where ua args (EApp f a) = ua (a:args) f
91 ua args t = (t, args)
93mkEApp :: ExecVal -> [ExecVal] -> ExecVal
94mkEApp f [] = f
95mkEApp f (a:args) = mkEApp (EApp f a) args
97initState :: Idris ExecState
98initState = do ist <- getIState
99 return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)
101type Exec = ErrorT String (StateT ExecState IO)
103runExec :: Exec a -> ExecState -> IO (Either String a)
104runExec ex st = fst <$> runStateT (runErrorT ex) st
106getExecState :: Exec ExecState
107getExecState = lift get
109putExecState :: ExecState -> Exec ()
110putExecState = lift . put
112execFail :: String -> Exec a
113execFail = throwError
115execIO :: IO a -> Exec a
116execIO = lift . lift
118delay :: ExecEnv -> Context -> Term -> Exec ExecVal
119delay env ctxt tm =
120 do st <- getExecState
121 let i = exec_next_thunk st
122 putExecState $ st { exec_thunks = M.insert i (Delayed env ctxt tm) (exec_thunks st)
123 , exec_next_thunk = exec_next_thunk st + 1
124 }
125 return $ EThunk i
127force :: Int -> Exec ExecVal
128force i = do st <- getExecState
129 case M.lookup i (exec_thunks st) of
130 Just (Delayed env ctxt tm) -> do tm' <- doExec env ctxt tm
131 case tm' of
132 EThunk i ->
133 do res <- force i
134 update res i
135 return res
136 _ -> do update tm' i
137 return tm'
138 Just (Forced tm) -> return tm
139 Nothing -> execFail "Tried to exec non-existing thunk. This is a bug!"
140 where update :: ExecVal -> Int -> Exec ()
141 update tm i = do est <- getExecState
142 putExecState $ est { exec_thunks = M.insert i (Forced tm) (exec_thunks est) }
144tryForce :: ExecVal -> Exec ExecVal
145tryForce (EThunk i) = force i
146tryForce tm = return tm
148debugThunks :: Exec ()
149debugThunks = do st <- getExecState
150 execIO $ putStrLn (take 4000 (show (exec_thunks st)))
152execute :: Term -> Idris Term
153execute tm = do est <- initState
154 ctxt <- getContext
155 res <- lift $ flip runExec est $ do res <- doExec [] ctxt tm
156 toTT res
157 case res of
158 Left err -> fail err
159 Right tm' -> return tm'
161ioWrap :: ExecVal -> ExecVal
162ioWrap tm = mkEApp (EP (DCon 0 2) (UN "prim__IO") EErased) [EErased, tm]
164ioUnit :: ExecVal
165ioUnit = ioWrap (EP Ref unitCon EErased)
167type ExecEnv = [(Name, ExecVal)]
169doExec :: ExecEnv -> Context -> Term -> Exec ExecVal
170doExec env ctxt p@(P Ref n ty) =
171 do let val = lookupDef n ctxt
172 case val of
173 [Function _ tm] -> doExec env ctxt tm
174 [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def
175 [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later
176 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
177 doExec env ctxt tm
178 [CaseOp _ _ _ _ _ ns sc _ _] -> return (EP Ref n EErased)
179 [] -> execFail $ "Could not find " ++ show n ++ " in definitions."
180 thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined
181doExec env ctxt p@(P Bound n ty) =
182 case lookup n env of
183 Nothing -> execFail "not found"
184 Just tm -> return tm
185doExec env ctxt (P (DCon a b) n _) = return (EP (DCon a b) n EErased)
186doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)
187doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))
188 | otherwise = execFail "env too small"
189doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v
190 doExec ((n, v'):env) ctxt body
191doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
192doExec env ctxt tm@(Bind n b body) = return $
193 EBind n (fmap (\_->EErased) b)
194 (\arg -> doExec ((n, arg):env) ctxt body)
195doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)
196doExec env ctxt (Constant c) = return (EConstant c)
197doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
198 doExec env ctxt ((x:xs) !! i)
199doExec env ctxt Erased = return EErased
200doExec env ctxt Impossible = fail "Tried to execute an impossible case"
201doExec env ctxt (TType u) = return (EType u)
203execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal
204execApp env ctxt (f, args) = do newF <- doExec env ctxt f
205 laziness <- (++ repeat False) <$> (getLaziness newF)
206 newArgs <- mapM argExec (zip args laziness)
207 execApp' env ctxt newF newArgs
208 where getLaziness (EP _ (UN "lazy") _) = return [False, True]
209 getLaziness (EP _ n _) = do est <- getExecState
210 let argInfo = exec_implicits est
211 case lookupCtxtName n argInfo of
212 [] -> return (repeat False)
213 [ps] -> return $ map lazyarg (snd ps)
214 many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)
215 getLaziness _ = return (repeat False) -- ok due to zip above
216 argExec :: (Term, Bool) -> Exec ExecVal
217 argExec (tm, False) = doExec env ctxt tm
218 argExec (tm, True) = delay env ctxt tm
221execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
222execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
223execApp' env ctxt (EP _ (UN "unsafePerformIO") _) (ty:action:rest) | (prim__IO, [_, v]) <- unApplyV action =
224 execApp' env ctxt v rest
226execApp' env ctxt (EP _ (UN "io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =
227 do v'' <- tryForce v'
228 res <- execApp' env ctxt k [v''] >>= tryForce
229 execApp' env ctxt res rest
230execApp' env ctxt con@(EP _ (UN "io_return") _) args@(tp:v:rest) =
231 do v' <- tryForce v
232 execApp' env ctxt (mkEApp con [tp, v']) rest
234-- Special cases arising from not having access to the C RTS in the interpreter
235execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str arg):rest)
236 | Just (FFun "putStr" _ _) <- foreignFromTT fn = do execIO (putStr arg)
237 execApp' env ctxt ioUnit rest
238execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
239 | Just (FFun "fileOpen" _ _) <- foreignFromTT fn = do m <- case mode of
240 "r" -> return ReadMode
241 "w" -> return WriteMode
242 "a" -> return AppendMode
243 "rw" -> return ReadWriteMode
244 "wr" -> return ReadWriteMode
245 "r+" -> return ReadWriteMode
246 _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)
247 h <- execIO $ openFile f m
248 execApp' env ctxt (ioWrap (EHandle h)) rest
250execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)
251 | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do eofp <- execIO $ hIsEOF h
252 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
253 execApp' env ctxt res rest
255execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)
256 | Just (FFun "fileClose" _ _) <- foreignFromTT fn = do execIO $ hClose h
257 execApp' env ctxt ioUnit rest
259execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EPtr p):rest)
260 | Just (FFun "isNull" _ _) <- foreignFromTT fn = let res = if p == nullPtr then 1 else 0 in
261 execApp' env ctxt (EConstant (I res)) rest
263execApp' env ctxt f@(EP _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun _ argTs retT) <- foreignFromTT fn
264 , length xs >= length argTs =
265 do res <- stepForeign (ty:fn:take (length argTs) xs)
266 case res of
267 Nothing -> fail "Could not call foreign function"
268 Just r -> return (mkEApp r (drop (length argTs) xs))
269 | otherwise = return (mkEApp f args)
271execApp' env ctxt f@(EP _ n _) args =
272 do let val = lookupDef n ctxt
273 case val of
274 [Function _ tm] -> fail "should already have been eval'd"
275 [TyDecl nt ty] -> return $ mkEApp f args
276 [Operator tp arity op] ->
277 if length args >= arity
278 then do args' <- mapM tryForce $ take arity args
279 case getOp n args' of
280 Just res -> do r <- res
281 execApp' env ctxt r (drop arity args)
282 Nothing -> return (mkEApp f args)
283 else return (mkEApp f args)
284 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
285 do rhs <- doExec env ctxt tm
286 execApp' env ctxt rhs args
287 [CaseOp _ _ _ _ _ ns sc _ _] ->
288 do res <- execCase env ctxt ns sc args
289 return $ fromMaybe (mkEApp f args) res
290 thing -> return $ mkEApp f args
291 where getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
292 getOp (UN "prim__addInt") [EConstant (I i1), EConstant (I i2)] =
293 primRes I (i1 + i2)
294 getOp (UN "prim__andInt") [EConstant (I i1), EConstant (I i2)] =
295 primRes I (i1 .&. i2)
296 getOp (UN "prim__charToInt") [EConstant (Ch c)] =
297 primRes I (fromEnum c)
298 getOp (UN "prim__complInt") [EConstant (I i)] =
299 primRes I (complement i)
300 getOp (UN "prim__concat") [EConstant (Str s1), EConstant (Str s2)] =
301 primRes Str (s1 ++ s2)
302 getOp (UN "prim__divInt") [EConstant (I i1), EConstant (I i2)] =
303 primRes I (i1 `div` i2)
304 getOp (UN "prim__eqChar") [EConstant (Ch c1), EConstant (Ch c2)] =
305 primResBool (c1 == c2)
306 getOp (UN "prim__eqInt") [EConstant (I i1), EConstant (I i2)] =
307 primResBool (i1 == i2)
308 getOp (UN "prim__eqString") [EConstant (Str s1), EConstant (Str s2)] =
309 primResBool (s1 == s2)
310 getOp (UN "prim__gtChar") [EConstant (Ch i1), EConstant (Ch i2)] =
311 primResBool (i1 > i2)
312 getOp (UN "prim__gteChar") [EConstant (Ch i1), EConstant (Ch i2)] =
313 primResBool (i1 >= i2)
314 getOp (UN "prim__gtInt") [EConstant (I i1), EConstant (I i2)] =
315 primResBool (i1 > i2)
316 getOp (UN "prim__gteInt") [EConstant (I i1), EConstant (I i2)] =
317 primResBool (i1 >= i2)
318 getOp (UN "prim__intToFloat") [EConstant (I i)] =
319 primRes Fl (fromRational (toRational i))
320 getOp (UN "prim__intToStr") [EConstant (I i)] =
321 primRes Str (show i)
322 getOp (UN "prim_lenString") [EConstant (Str s)] =
323 primRes I (length s)
324 getOp (UN "prim__ltChar") [EConstant (Ch i1), EConstant (Ch i2)] =
325 primResBool (i1 < i2)
326 getOp (UN "prim__lteChar") [EConstant (Ch i1), EConstant (Ch i2)] =
327 primResBool (i1 <= i2)
328 getOp (UN "prim__lteInt") [EConstant (I i1), EConstant (I i2)] =
329 primResBool (i1 <= i2)
330 getOp (UN "prim__ltInt") [EConstant (I i1), EConstant (I i2)] =
331 primResBool (i1 < i2)
332 getOp (UN "prim__modInt") [EConstant (I i1), EConstant (I i2)] =
333 primRes I (i1 `mod` i2)
334 getOp (UN "prim__mulBigInt") [EConstant (BI i1), EConstant (BI i2)] =
335 primRes BI (i1 * i2)
336 getOp (UN "prim__mulFloat") [EConstant (Fl i1), EConstant (Fl i2)] =
337 primRes Fl (i1 * i2)
338 getOp (UN "prim__mulInt") [EConstant (I i1), EConstant (I i2)] =
339 primRes I (i1 * i2)
340 getOp (UN "prim__orInt") [EConstant (I i1), EConstant (I i2)] =
341 primRes I (i1 .|. i2)
342 getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =
343 Just $ do line <- execIO getLine
344 return (EConstant (Str line))
345 getOp (UN "prim__readString") [EHandle h] =
346 Just $ do contents <- execIO $ hGetLine h
347 return (EConstant (Str contents))
348 getOp (UN "prim__shLInt") [EConstant (I i1), EConstant (I i2)] =
349 primRes I (shiftL i1 i2)
350 getOp (UN "prim__shRInt") [EConstant (I i1), EConstant (I i2)] =
351 primRes I (shiftR i1 i2)
352 getOp (UN "prim__strCons") [EConstant (Ch c), EConstant (Str s)] =
353 primRes Str (c:s)
354 getOp (UN "prim__strHead") [EConstant (Str (c:s))] =
355 primRes Ch c
356 getOp (UN "prim__strRev") [EConstant (Str s)] =
357 primRes Str (reverse s)
358 getOp (UN "prim__strTail") [EConstant (Str (c:s))] =
359 primRes Str s
360 getOp (UN "prim__subFloat") [EConstant (Fl i1), EConstant (Fl i2)] =
361 primRes Fl (i1 - i2)
362 getOp (UN "prim__subInt") [EConstant (I i1), EConstant (I i2)] =
363 primRes I (i1 - i2)
364 getOp (UN "prim__xorInt") [EConstant (I i1), EConstant (I i2)] =
365 primRes I (i1 `xor` i2)
366 getOp n args = trace ("No prim " ++ show n ++ " for " ++ take 1000 (show args)) Nothing
368 primRes :: (a -> Const) -> a -> Maybe (Exec ExecVal)
369 primRes constr = Just . return . EConstant . constr
371 primResBool :: Bool -> Maybe (Exec ExecVal)
372 primResBool b = primRes I (if b then 1 else 0)
374execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
375 let (f', as) = unApplyV ret
376 execApp' env ctxt f' (as ++ args)
377execApp' env ctxt (EThunk i) args = do f <- force i
378 execApp' env ctxt f args
379execApp' env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp' env ctxt f (args1 ++ args2)
380execApp' env ctxt f args = return (mkEApp f args)
386-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
387-- evaluates them, then begins the checks for matching cases.
388execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
389execCase env ctxt ns sc args =
390 let arity = length ns in
391 if arity <= length args
392 then do let amap = zip ns args
393 caseRes <- execCase' env ctxt amap sc
394 case caseRes of
395 Just res -> Just <$> execApp' (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)
396 Nothing -> return Nothing
397 else return Nothing
399-- | Take bindings and a case tree and examines them, executing the matching case if possible.
400execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
401execCase' env ctxt amap (UnmatchedCase _) = return Nothing
402execCase' env ctxt amap (STerm tm) =
403 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm
404execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
405 do tm' <- tryForce tm
406 case chooseAlt tm' alts of
407 Just (newCase, newBindings) ->
408 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
409 execCase' env ctxt amap' newCase
410 Nothing -> return Nothing
412chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
413chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])
414chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
415chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm
416 , cn == n = Just (sc, zip ns args)
417 | otherwise = chooseAlt tm alts
418chooseAlt tm (_:alts) = chooseAlt tm alts
419chooseAlt _ [] = Nothing
424data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
426idrisType :: FTy -> ExecVal
427idrisType FUnit = EP Ref unitTy EErased
428idrisType ft = EConstant (idr ft)
429 where idr FInt = IType
430 idr FFloat = FlType
431 idr FChar = ChType
432 idr FString = StrType
433 idr FPtr = PtrType
435data Foreign = FFun String [FTy] FTy deriving Show
438call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
439call (FFun name argTypes retType) args =
440 do fn <- findForeign name
441 case fn of
442 Nothing -> return Nothing
443 Just f -> do res <- call' f args retType
444 return . Just . ioWrap $ res
445 where call' :: ForeignFun -> [ExecVal] -> FTy -> Exec ExecVal
446 call' (Fun _ h) args FInt = do res <- execIO $ callFFI h retCInt (prepArgs args)
447 return (EConstant (I (fromIntegral res)))
448 call' (Fun _ h) args FFloat = do res <- execIO $ callFFI h retCDouble (prepArgs args)
449 return (EConstant (Fl (realToFrac res)))
450 call' (Fun _ h) args FChar = do res <- execIO $ callFFI h retCChar (prepArgs args)
451 return (EConstant (Ch (castCCharToChar res)))
452 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
453 hStr <- execIO $ peekCString res
454-- lift $ free res
455 return (EConstant (Str hStr))
457 call' (Fun _ h) args FPtr = do res <- execIO $ callFFI h (retPtr retVoid) (prepArgs args)
458 return (EPtr res)
459 call' (Fun _ h) args FUnit = do res <- execIO $ callFFI h retVoid (prepArgs args)
460 return (EP Ref unitCon EErased)
461-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
464 prepArgs = map prepArg
465 prepArg (EConstant (I i)) = argCInt (fromIntegral i)
466 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)
467 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
468 prepArg (EConstant (Str s)) = argString s
469 prepArg (EPtr p) = argPtr p
470 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined
474foreignFromTT :: ExecVal -> Maybe Foreign
475foreignFromTT t = case (unApplyV t) of
476 (_, [(EConstant (Str name)), args, ret]) ->
477 do argTy <- unEList args
478 argFTy <- sequence $ map getFTy argTy
479 retFTy <- getFTy ret
480 return $ FFun name argFTy retFTy
481 _ -> trace "failed to construct ffun" Nothing
483getFTy :: ExecVal -> Maybe FTy
484getFTy (EP _ (UN t) _) =
485 case t of
486 "FInt" -> Just FInt
487 "FFloat" -> Just FFloat
488 "FChar" -> Just FChar
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) = do let ffun = foreignFromTT fn
518 f' <- case (call <$> ffun) of
519 Just f -> f args
520 Nothing -> return Nothing
521 return f'
522stepForeign _ = fail "Tried to call foreign function that wasn't mkForeign"
524mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
525mapMaybeM f [] = return []
526mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
527 x' <- f x
528 case x' of
529 Just x'' -> return (x'':rest)
530 Nothing -> return rest
532findForeign :: String -> Exec (Maybe ForeignFun)
533findForeign fn = do est <- getExecState
534 let libs = exec_dynamic_libs est
535 fns <- mapMaybeM getFn libs
536 case fns of
537 [f] -> return (Just f)
538 [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"
539 return Nothing
540 fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
541 show (length fs) ++ " occurrences."
542 return Nothing
543 where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)