on ee3da18 help sign in
Idris-dev/src/Core/Execute.hs
547 lines 26 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) | Just v <- lookup n env = return v
171doExec env ctxt p@(P Ref n ty) =
172 do let val = lookupDef n ctxt
173 case val of
174 [Function _ tm] -> doExec env ctxt tm
175 [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def
176 [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later
177 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
178 doExec env ctxt tm
179 [CaseOp _ _ _ _ _ ns sc _ _] -> return (EP Ref n EErased)
180 [] -> execFail $ "Could not find " ++ show n ++ " in definitions."
181 thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined
182doExec env ctxt p@(P Bound n ty) =
183 case lookup n env of
184 Nothing -> execFail "not found"
185 Just tm -> return tm
186doExec env ctxt (P (DCon a b) n _) = return (EP (DCon a b) n EErased)
187doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)
188doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))
189 | otherwise = execFail "env too small"
190doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v
191 doExec ((n, v'):env) ctxt body
192doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
193doExec env ctxt tm@(Bind n b body) = return $
194 EBind n (fmap (\_->EErased) b)
195 (\arg -> doExec ((n, arg):env) ctxt body)
196doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)
197doExec env ctxt (Constant c) = return (EConstant c)
198doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
199 doExec env ctxt ((x:xs) !! i)
200doExec env ctxt Erased = return EErased
201doExec env ctxt Impossible = fail "Tried to execute an impossible case"
202doExec env ctxt (TType u) = return (EType u)
204execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal
205execApp env ctxt (f, args) = do newF <- doExec env ctxt f
206 laziness <- (++ repeat False) <$> (getLaziness newF)
207 newArgs <- mapM argExec (zip args laziness)
208 execApp' env ctxt newF newArgs
209 where getLaziness (EP _ (UN "lazy") _) = return [False, True]
210 getLaziness (EP _ n _) = do est <- getExecState
211 let argInfo = exec_implicits est
212 case lookupCtxtName n argInfo of
213 [] -> return (repeat False)
214 [ps] -> return $ map lazyarg (snd ps)
215 many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)
216 getLaziness _ = return (repeat False) -- ok due to zip above
217 argExec :: (Term, Bool) -> Exec ExecVal
218 argExec (tm, False) = doExec env ctxt tm
219 argExec (tm, True) = delay env ctxt tm
222execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
223execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
224execApp' env ctxt (EP _ (UN "unsafePerformIO") _) (ty:action:rest) | (prim__IO, [_, v]) <- unApplyV action =
225 execApp' env ctxt v rest
227execApp' env ctxt (EP _ (UN "io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =
228 do v'' <- tryForce v'
229 res <- execApp' env ctxt k [v''] >>= tryForce
230 execApp' env ctxt res rest
231execApp' env ctxt con@(EP _ (UN "io_return") _) args@(tp:v:rest) =
232 do v' <- tryForce v
233 execApp' env ctxt (mkEApp con [tp, v']) rest
235-- Special cases arising from not having access to the C RTS in the interpreter
236execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str arg):rest)
237 | Just (FFun "putStr" _ _) <- foreignFromTT fn = do execIO (putStr arg)
238 execApp' env ctxt ioUnit rest
239execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
240 | Just (FFun "fileOpen" _ _) <- foreignFromTT fn = do m <- case mode of
241 "r" -> return ReadMode
242 "w" -> return WriteMode
243 "a" -> return AppendMode
244 "rw" -> return ReadWriteMode
245 "wr" -> return ReadWriteMode
246 "r+" -> return ReadWriteMode
247 _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)
248 h <- execIO $ openFile f m
249 execApp' env ctxt (ioWrap (EHandle h)) rest
251execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)
252 | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do eofp <- execIO $ hIsEOF h
253 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
254 execApp' env ctxt res rest
256execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)
257 | Just (FFun "fileClose" _ _) <- foreignFromTT fn = do execIO $ hClose h
258 execApp' env ctxt ioUnit rest
260execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EPtr p):rest)
261 | Just (FFun "isNull" _ _) <- foreignFromTT fn = let res = ioWrap . EConstant . I $
262 if p == nullPtr then 1 else 0
263 in execApp' env ctxt res rest
265execApp' env ctxt f@(EP _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun f argTs retT) <- foreignFromTT fn
266 , length xs >= length argTs =
267 do res <- stepForeign (ty:fn:take (length argTs) xs)
268 case res of
269 Nothing -> fail $ "Could not call foreign function \"" ++ f ++
270 "\" with args " ++ show (take (length argTs) xs)
271 Just r -> return (mkEApp r (drop (length argTs) xs))
272 | otherwise = return (mkEApp f args)
274execApp' env ctxt f@(EP _ n _) args =
275 do let val = lookupDef n ctxt
276 case val of
277 [Function _ tm] -> fail "should already have been eval'd"
278 [TyDecl nt ty] -> return $ mkEApp f args
279 [Operator tp arity op] ->
280 if length args >= arity
281 then do args' <- mapM tryForce $ take arity args
282 case getOp n args' of
283 Just res -> do r <- res
284 execApp' env ctxt r (drop arity args)
285 Nothing -> return (mkEApp f args)
286 else return (mkEApp f args)
287 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
288 do rhs <- doExec env ctxt tm
289 execApp' env ctxt rhs args
290 [CaseOp _ _ _ _ _ ns sc _ _] ->
291 do res <- execCase env ctxt ns sc args
292 return $ fromMaybe (mkEApp f args) res
293 thing -> return $ mkEApp f args
294 where getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
295 getOp (UN "prim__addInt") [EConstant (I i1), EConstant (I i2)] =
296 primRes I (i1 + i2)
297 getOp (UN "prim__andInt") [EConstant (I i1), EConstant (I i2)] =
298 primRes I (i1 .&. i2)
299 getOp (UN "prim__charToInt") [EConstant (Ch c)] =
300 primRes I (fromEnum c)
301 getOp (UN "prim__complInt") [EConstant (I i)] =
302 primRes I (complement i)
303 getOp (UN "prim__concat") [EConstant (Str s1), EConstant (Str s2)] =
304 primRes Str (s1 ++ s2)
305 getOp (UN "prim__divInt") [EConstant (I i1), EConstant (I i2)] =
306 primRes I (i1 `div` i2)
307 getOp (UN "prim__eqChar") [EConstant (Ch c1), EConstant (Ch c2)] =
308 primResBool (c1 == c2)
309 getOp (UN "prim__eqInt") [EConstant (I i1), EConstant (I i2)] =
310 primResBool (i1 == i2)
311 getOp (UN "prim__eqString") [EConstant (Str s1), EConstant (Str s2)] =
312 primResBool (s1 == s2)
313 getOp (UN "prim__gtChar") [EConstant (Ch i1), EConstant (Ch i2)] =
314 primResBool (i1 > i2)
315 getOp (UN "prim__gteChar") [EConstant (Ch i1), EConstant (Ch i2)] =
316 primResBool (i1 >= i2)
317 getOp (UN "prim__gtInt") [EConstant (I i1), EConstant (I i2)] =
318 primResBool (i1 > i2)
319 getOp (UN "prim__gteInt") [EConstant (I i1), EConstant (I i2)] =
320 primResBool (i1 >= i2)
321 getOp (UN "prim__intToFloat") [EConstant (I i)] =
322 primRes Fl (fromRational (toRational i))
323 getOp (UN "prim__intToStr") [EConstant (I i)] =
324 primRes Str (show i)
325 getOp (UN "prim_lenString") [EConstant (Str s)] =
326 primRes I (length s)
327 getOp (UN "prim__ltChar") [EConstant (Ch i1), EConstant (Ch i2)] =
328 primResBool (i1 < i2)
329 getOp (UN "prim__lteChar") [EConstant (Ch i1), EConstant (Ch i2)] =
330 primResBool (i1 <= i2)
331 getOp (UN "prim__lteInt") [EConstant (I i1), EConstant (I i2)] =
332 primResBool (i1 <= i2)
333 getOp (UN "prim__ltInt") [EConstant (I i1), EConstant (I i2)] =
334 primResBool (i1 < i2)
335 getOp (UN "prim__modInt") [EConstant (I i1), EConstant (I i2)] =
336 primRes I (i1 `mod` i2)
337 getOp (UN "prim__mulBigInt") [EConstant (BI i1), EConstant (BI i2)] =
338 primRes BI (i1 * i2)
339 getOp (UN "prim__mulFloat") [EConstant (Fl i1), EConstant (Fl i2)] =
340 primRes Fl (i1 * i2)
341 getOp (UN "prim__mulInt") [EConstant (I i1), EConstant (I i2)] =
342 primRes I (i1 * i2)
343 getOp (UN "prim__orInt") [EConstant (I i1), EConstant (I i2)] =
344 primRes I (i1 .|. i2)
345 getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =
346 Just $ do line <- execIO getLine
347 return (EConstant (Str line))
348 getOp (UN "prim__readString") [EHandle h] =
349 Just $ do contents <- execIO $ hGetLine h
350 return (EConstant (Str contents))
351 getOp (UN "prim__shLInt") [EConstant (I i1), EConstant (I i2)] =
352 primRes I (shiftL i1 i2)
353 getOp (UN "prim__shRInt") [EConstant (I i1), EConstant (I i2)] =
354 primRes I (shiftR i1 i2)
355 getOp (UN "prim__strCons") [EConstant (Ch c), EConstant (Str s)] =
356 primRes Str (c:s)
357 getOp (UN "prim__strHead") [EConstant (Str (c:s))] =
358 primRes Ch c
359 getOp (UN "prim__strRev") [EConstant (Str s)] =
360 primRes Str (reverse s)
361 getOp (UN "prim__strTail") [EConstant (Str (c:s))] =
362 primRes Str s
363 getOp (UN "prim__subFloat") [EConstant (Fl i1), EConstant (Fl i2)] =
364 primRes Fl (i1 - i2)
365 getOp (UN "prim__subInt") [EConstant (I i1), EConstant (I i2)] =
366 primRes I (i1 - i2)
367 getOp (UN "prim__xorInt") [EConstant (I i1), EConstant (I i2)] =
368 primRes I (i1 `xor` i2)
369 getOp n args = trace ("No prim " ++ show n ++ " for " ++ take 1000 (show args)) Nothing
371 primRes :: (a -> Const) -> a -> Maybe (Exec ExecVal)
372 primRes constr = Just . return . EConstant . constr
374 primResBool :: Bool -> Maybe (Exec ExecVal)
375 primResBool b = primRes I (if b then 1 else 0)
377execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
378 let (f', as) = unApplyV ret
379 execApp' env ctxt f' (as ++ args)
380execApp' env ctxt (EThunk i) args = do f <- force i
381 execApp' env ctxt f args
382execApp' env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp' env ctxt f (args1 ++ args2)
383execApp' env ctxt f args = return (mkEApp f args)
389-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
390-- evaluates them, then begins the checks for matching cases.
391execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
392execCase env ctxt ns sc args =
393 let arity = length ns in
394 if arity <= length args
395 then do let amap = zip ns args
396-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()
397 caseRes <- execCase' env ctxt amap sc
398 case caseRes of
399 Just res -> Just <$> execApp' (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)
400 Nothing -> return Nothing
401 else return Nothing
403-- | Take bindings and a case tree and examines them, executing the matching case if possible.
404execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
405execCase' env ctxt amap (UnmatchedCase _) = return Nothing
406execCase' env ctxt amap (STerm tm) =
407 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm
408execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
409 do tm' <- tryForce tm
410 case chooseAlt tm' alts of
411 Just (newCase, newBindings) ->
412 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
413 execCase' env ctxt amap' newCase
414 Nothing -> return Nothing
416chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
417chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])
418chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
419chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm
420 , cn == n = Just (sc, zip ns args)
421 | otherwise = chooseAlt tm alts
422chooseAlt tm (_:alts) = chooseAlt tm alts
423chooseAlt _ [] = Nothing
428data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit deriving (Show, Read)
430idrisType :: FTy -> ExecVal
431idrisType FUnit = EP Ref unitTy EErased
432idrisType ft = EConstant (idr ft)
433 where idr FInt = IType
434 idr FFloat = FlType
435 idr FChar = ChType
436 idr FString = StrType
437 idr FPtr = PtrType
439data Foreign = FFun String [FTy] FTy deriving Show
442call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
443call (FFun name argTypes retType) args =
444 do fn <- findForeign name
445 case fn of
446 Nothing -> return Nothing
447 Just f -> do res <- call' f args retType
448 return . Just . ioWrap $ res
449 where call' :: ForeignFun -> [ExecVal] -> FTy -> Exec ExecVal
450 call' (Fun _ h) args FInt = do res <- execIO $ callFFI h retCInt (prepArgs args)
451 return (EConstant (I (fromIntegral res)))
452 call' (Fun _ h) args FFloat = do res <- execIO $ callFFI h retCDouble (prepArgs args)
453 return (EConstant (Fl (realToFrac res)))
454 call' (Fun _ h) args FChar = do res <- execIO $ callFFI h retCChar (prepArgs args)
455 return (EConstant (Ch (castCCharToChar res)))
456 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
457 hStr <- execIO $ peekCString res
458-- lift $ free res
459 return (EConstant (Str hStr))
461 call' (Fun _ h) args FPtr = do res <- execIO $ callFFI h (retPtr retVoid) (prepArgs args)
462 return (EPtr res)
463 call' (Fun _ h) args FUnit = do res <- execIO $ callFFI h retVoid (prepArgs args)
464 return (EP Ref unitCon EErased)
465-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
468 prepArgs = map prepArg
469 prepArg (EConstant (I i)) = argCInt (fromIntegral i)
470 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)
471 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
472 prepArg (EConstant (Str s)) = argString s
473 prepArg (EPtr p) = argPtr p
474 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined
478foreignFromTT :: ExecVal -> Maybe Foreign
479foreignFromTT t = case (unApplyV t) of
480 (_, [(EConstant (Str name)), args, ret]) ->
481 do argTy <- unEList args
482 argFTy <- sequence $ map getFTy argTy
483 retFTy <- getFTy ret
484 return $ FFun name argFTy retFTy
485 _ -> trace "failed to construct ffun" Nothing
487getFTy :: ExecVal -> Maybe FTy
488getFTy (EP _ (UN t) _) =
489 case t of
490 "FInt" -> Just FInt
491 "FFloat" -> Just FFloat
492 "FChar" -> Just FChar
493 "FString" -> Just FString
494 "FPtr" -> Just FPtr
495 "FUnit" -> Just FUnit
496 _ -> Nothing
497getFTy _ = Nothing
499unList :: Term -> Maybe [Term]
500unList tm = case unApply tm of
501 (nil, [_]) -> Just []
502 (cons, ([_, x, xs])) ->
503 do rest <- unList xs
504 return $ x:rest
505 (f, args) -> Nothing
507unEList :: ExecVal -> Maybe [ExecVal]
508unEList tm = case unApplyV tm of
509 (nil, [_]) -> Just []
510 (cons, ([_, x, xs])) ->
511 do rest <- unEList xs
512 return $ x:rest
513 (f, args) -> Nothing
516toConst :: Term -> Maybe Const
517toConst (Constant c) = Just c
518toConst _ = Nothing
520stepForeign :: [ExecVal] -> Exec (Maybe ExecVal)
521stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
522 f' <- case (call <$> ffun) of
523 Just f -> f args
524 Nothing -> return Nothing
525 return f'
526stepForeign _ = fail "Tried to call foreign function that wasn't mkForeign"
528mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
529mapMaybeM f [] = return []
530mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
531 x' <- f x
532 case x' of
533 Just x'' -> return (x'':rest)
534 Nothing -> return rest
536findForeign :: String -> Exec (Maybe ForeignFun)
537findForeign fn = do est <- getExecState
538 let libs = exec_dynamic_libs est
539 fns <- mapMaybeM getFn libs
540 case fns of
541 [f] -> return (Just f)
542 [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"
543 return Nothing
544 fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
545 show (length fs) ++ " occurrences."
546 return Nothing
547 where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)