git.iko.soy/Idris-dev
on eea6bcb help sign in
Idris-dev/src/Idris/Core/Execute.hs
572 lines 25 kB history raw
1{-# LANGUAGE PatternGuards, ExistentialQuantification, CPP #-}
2module Idris.Core.Execute (execute) where
4import Idris.AbsSyntax
5import Idris.AbsSyntaxTree
6import IRTS.Lang(FType(..))
8import Idris.Primitives(Prim(..), primitives)
10import Idris.Core.TT
11import Idris.Core.Evaluate
12import Idris.Core.CaseTree
14import Idris.Error
16import Debug.Trace
18import Util.DynamicLinker
19import Util.System
21import Control.Applicative hiding (Const)
22import Control.Exception
23import Control.Monad.Trans
24import Control.Monad.Trans.State.Strict
25import Control.Monad.Trans.Error
26import Control.Monad
27import Data.Maybe
28import Data.Bits
29import qualified Data.Map as M
31#ifdef IDRIS_FFI
32import Foreign.LibFFI
33import Foreign.C.String
34import Foreign.Marshal.Alloc (free)
35import Foreign.Ptr
36#endif
38import System.IO
40#ifndef IDRIS_FFI
41execute :: Term -> Idris Term
42execute tm = fail "libffi not supported, rebuild Idris with -f FFI"
43#else
44-- else is rest of file
45readMay :: (Read a) => String -> Maybe a
46readMay s = case reads s of
47 [(x, "")] -> Just x
48 _ -> Nothing
50data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show
52newtype ExecState = ExecState { 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 Context ExecEnv Term
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 _ env tm) = "<<thunk " ++ show env ++ "||||" ++ show tm ++ ">>"
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 ctxt env tm) = do env' <- mapM toBinder env
100 return $ normalise ctxt env' tm
101 where toBinder (n, v) = do v' <- toTT v
102 return (n, Let Erased v')
103toTT (EHandle _) = return Erased
105unApplyV :: ExecVal -> (ExecVal, [ExecVal])
106unApplyV tm = ua [] tm
107 where ua args (EApp f a) = ua (a:args) f
108 ua args t = (t, args)
110mkEApp :: ExecVal -> [ExecVal] -> ExecVal
111mkEApp f [] = f
112mkEApp f (a:args) = mkEApp (EApp f a) args
114initState :: Idris ExecState
115initState = do ist <- getIState
116 return $ ExecState (idris_dynamic_libs ist)
118type Exec = ErrorT Err (StateT ExecState IO)
120runExec :: Exec a -> ExecState -> IO (Either Err a)
121runExec ex st = fst <$> runStateT (runErrorT ex) st
123getExecState :: Exec ExecState
124getExecState = lift get
126putExecState :: ExecState -> Exec ()
127putExecState = lift . put
129execFail :: Err -> Exec a
130execFail = throwError
132execIO :: IO a -> Exec a
133execIO = lift . lift
136execute :: Term -> Idris Term
137execute tm = do est <- initState
138 ctxt <- getContext
139 res <- lift . lift . flip runExec est $
140 do res <- doExec [] ctxt tm
141 toTT res
142 case res of
143 Left err -> ierror err
144 Right tm' -> return tm'
146ioWrap :: ExecVal -> ExecVal
147ioWrap tm = mkEApp (EP (DCon 0 2) (sUN "prim__IO") EErased) [EErased, tm]
149ioUnit :: ExecVal
150ioUnit = ioWrap (EP Ref unitCon EErased)
152type ExecEnv = [(Name, ExecVal)]
154doExec :: ExecEnv -> Context -> Term -> Exec ExecVal
155doExec env ctxt p@(P Ref n ty) | Just v <- lookup n env = return v
156doExec env ctxt p@(P Ref n ty) =
157 do let val = lookupDef n ctxt
158 case val of
159 [Function _ tm] -> doExec env ctxt tm
160 [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def
161 [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later
162 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
163 doExec env ctxt tm
164 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] -> return (EP Ref n EErased)
165 [] -> execFail . Msg $ "Could not find " ++ show n ++ " in definitions."
166 thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined
167doExec env ctxt p@(P Bound n ty) =
168 case lookup n env of
169 Nothing -> execFail . Msg $ "not found"
170 Just tm -> return tm
171doExec env ctxt (P (DCon a b) n _) = return (EP (DCon a b) n EErased)
172doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)
173doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))
174 | otherwise = execFail . Msg $ "env too small"
175doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v
176 doExec ((n, v'):env) ctxt body
177doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
178doExec env ctxt tm@(Bind n b body) = return $
179 EBind n (fmap (\_->EErased) b)
180 (\arg -> doExec ((n, arg):env) ctxt body)
181doExec env ctxt a@(App _ _) =
182 do let (f, args) = unApply a
183 f' <- doExec env ctxt f
184 args' <- case f' of
185 (EP _ d _) | d == delay ->
186 case args of
187 [t,a,tm] -> do t' <- doExec env ctxt t
188 a' <- doExec env ctxt a
189 return [t', a', EThunk ctxt env tm]
190 _ -> mapM (doExec env ctxt) args -- partial applications are fine to evaluate
191 fun' -> do mapM (doExec env ctxt) args
192 execApp env ctxt f' args'
193doExec env ctxt (Constant c) = return (EConstant c)
194doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
195 doExec env ctxt ((x:xs) !! i)
196doExec env ctxt Erased = return EErased
197doExec env ctxt Impossible = fail "Tried to execute an impossible case"
198doExec env ctxt (TType u) = return (EType u)
200execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
201execApp env ctxt v [] = return v -- no args is just a constant! can result from function calls
202execApp env ctxt (EP _ f _) (t:a:delayed:rest)
203 | f == force
204 , (_, [_, _, EThunk tmCtxt tmEnv tm]) <- unApplyV delayed =
205 do tm' <- doExec tmEnv tmCtxt tm
206 execApp env ctxt tm' rest
207execApp env ctxt (EP _ fp _) (ty:action:rest)
208 | fp == upio,
209 (prim__IO, [_, v]) <- unApplyV action
210 = execApp env ctxt v rest
212execApp env ctxt (EP _ fp _) args@(_:_:v:k:rest)
213 | fp == piobind,
214 (prim__IO, [_, v']) <- unApplyV v =
215 do res <- execApp env ctxt k [v']
216 execApp env ctxt res rest
217execApp env ctxt con@(EP _ fp _) args@(tp:v:rest)
218 | fp == pioret = execApp env ctxt (mkEApp con [tp, v]) rest
220-- Special cases arising from not having access to the C RTS in the interpreter
221execApp env ctxt (EP _ fp _) (_:fn:str:_:rest)
222 | fp == mkfprim,
223 Just (FFun "putStr" _ _) <- foreignFromTT fn
224 = case str of
225 EConstant (Str arg) -> do execIO (putStr arg)
226 execApp env ctxt ioUnit rest
227 _ -> execFail . Msg $
228 "The argument to putStr should be a constant string, but it was " ++
229 show str ++
230 ". Are all cases covered?"
231execApp env ctxt (EP _ fp _) (_:fn:_:handle:_:rest)
232 | fp == mkfprim,
233 Just (FFun "idris_readStr" _ _) <- foreignFromTT fn
234 = case handle of
235 EHandle h -> do contents <- execIO $ hGetLine h
236 execApp env ctxt (EConstant (Str (contents ++ "\n"))) rest
237 _ -> execFail . Msg $
238 "The argument to idris_readStr should be a handle, but it was " ++
239 show handle ++
240 ". Are all cases covered?"
241execApp env ctxt (EP _ fp _) (_:fn:fileStr:modeStr:rest)
242 | fp == mkfprim,
243 Just (FFun "fileOpen" _ _) <- foreignFromTT fn
244 = case (fileStr, modeStr) of
245 (EConstant (Str f), EConstant (Str mode)) ->
246 do f <- execIO $
247 catch (do let m = case mode of
248 "r" -> Right ReadMode
249 "w" -> Right WriteMode
250 "a" -> Right AppendMode
251 "rw" -> Right ReadWriteMode
252 "wr" -> Right ReadWriteMode
253 "r+" -> Right ReadWriteMode
254 _ -> Left ("Invalid mode for " ++ f ++ ": " ++ mode)
255 case fmap (openFile f) m of
256 Right h -> do h' <- h; return $ Right (ioWrap (EHandle h'), tail rest)
257 Left err -> return $ Left err)
258 (\e -> let _ = ( e::SomeException)
259 in return $ Right (ioWrap (EPtr nullPtr), tail rest))
260 case f of
261 Left err -> execFail . Msg $ err
262 Right (res, rest) -> execApp env ctxt res rest
263 _ -> execFail . Msg $
264 "The arguments to fileOpen should be constant strings, but they were " ++
265 show fileStr ++ " and " ++ show modeStr ++
266 ". Are all cases covered?"
268execApp env ctxt (EP _ fp _) (_:fn:handle:rest)
269 | fp == mkfprim,
270 Just (FFun "fileEOF" _ _) <- foreignFromTT fn
271 = case handle of
272 EHandle h -> do eofp <- execIO $ hIsEOF h
273 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
274 execApp env ctxt res (tail rest)
275 _ -> execFail . Msg $
276 "The argument to fileEOF should be a file handle, but it was " ++
277 show handle ++
278 ". Are all cases covered?"
280execApp env ctxt (EP _ fp _) (_:fn:handle:rest)
281 | fp == mkfprim,
282 Just (FFun "fileClose" _ _) <- foreignFromTT fn
283 = case handle of
284 EHandle h -> do execIO $ hClose h
285 execApp env ctxt ioUnit (tail rest)
286 _ -> execFail . Msg $
287 "The argument to fileClose should be a file handle, but it was " ++
288 show handle ++
289 ". Are all cases covered?"
291execApp env ctxt (EP _ fp _) (_:fn:ptr:rest)
292 | fp == mkfprim,
293 Just (FFun "isNull" _ _) <- foreignFromTT fn
294 = case ptr of
295 EPtr p -> let res = ioWrap . EConstant . I $
296 if p == nullPtr then 1 else 0
297 in execApp env ctxt res (tail rest)
298 -- Handles will be checked as null pointers sometimes - but if we got a
299 -- real Handle, then it's valid, so just return 1.
300 EHandle h -> let res = ioWrap . EConstant . I $ 0
301 in execApp env ctxt res (tail rest)
302 -- A foreign-returned char* has to be tested for NULL sometimes
303 EConstant (Str s) -> let res = ioWrap . EConstant . I $ 0
304 in execApp env ctxt res (tail rest)
305 _ -> execFail . Msg $
306 "The argument to isNull should be a pointer or file handle or string, but it was " ++
307 show ptr ++
308 ". Are all cases covered?"
311-- Right now, there's no way to send command-line arguments to the executor,
312-- so just return 0.
313execApp env ctxt (EP _ fp _) (_:fn:rest)
314 | fp == mkfprim,
315 Just (FFun "idris_numArgs" _ _) <- foreignFromTT fn
316 = let res = ioWrap . EConstant . I $ 0
317 in execApp env ctxt res (tail rest)
319execApp env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim
320 = case foreignFromTT fn of
321 Just (FFun f argTs retT) | length xs >= length argTs ->
322 do let (args', xs') = (take (length argTs) xs, -- foreign args
323 drop (length argTs + 1) xs) -- rest
324 res <- stepForeign (ty:fn:args')
325 case res of
326 Nothing -> fail $ "Could not call foreign function \"" ++ f ++
327 "\" with args " ++ show args
328 Just r -> return (mkEApp r xs')
329 Nothing -> return (mkEApp f args)
331execApp env ctxt c@(EP (DCon _ arity) n _) args =
332 do let args' = take arity args
333 let restArgs = drop arity args
334 execApp env ctxt (mkEApp c args') restArgs
336execApp env ctxt c@(EP (TCon _ arity) n _) args =
337 do let args' = take arity args
338 let restArgs = drop arity args
339 execApp env ctxt (mkEApp c args') restArgs
341execApp env ctxt f@(EP _ n _) args =
342 do let val = lookupDef n ctxt
343 case val of
344 [Function _ tm] -> fail "should already have been eval'd"
345 [TyDecl nt ty] -> return $ mkEApp f args
346 [Operator tp arity op] ->
347 if length args >= arity
348 then let args' = take arity args in
349 case getOp n args' of
350 Just res -> do r <- res
351 execApp env ctxt r (drop arity args)
352 Nothing -> return (mkEApp f args)
353 else return (mkEApp f args)
354 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
355 do rhs <- doExec env ctxt tm
356 execApp env ctxt rhs args
357 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->
358 do res <- execCase env ctxt ns sc args
359 return $ fromMaybe (mkEApp f args) res
360 thing -> return $ mkEApp f args
361execApp env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
362 let (f', as) = unApplyV ret
363 execApp env ctxt f' (as ++ args)
364execApp env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp env ctxt f (args1 ++ args2)
365execApp env ctxt f args = return (mkEApp f args)
367prs = sUN "prim__readString"
368pbm = sUN "prim__believe_me"
369pstd = sUN "prim__stdin"
370mkfprim = sUN "mkForeignPrim"
371pioret = sUN "prim_io_return"
372piobind = sUN "prim_io_bind"
373upio = sUN "unsafePerformPrimIO"
374delay = sUN "Delay"
375force = sUN "Force"
377-- | Look up primitive operations in the global table and transform them into ExecVal functions
378getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
379getOp fn [_, _, x] | fn == pbm = Just (return x)
380getOp fn [EP _ fn' _]
381 | fn == prs && fn' == pstd =
382 Just $ do line <- execIO getLine
383 return (EConstant (Str line))
384getOp fn [EHandle h]
385 | fn == prs =
386 Just $ do contents <- execIO $ hGetLine h
387 return (EConstant (Str (contents ++ "\n")))
388getOp n args = getPrim n primitives >>= flip applyPrim args
389 where getPrim :: Name -> [Prim] -> Maybe ([ExecVal] -> Maybe ExecVal)
390 getPrim n [] = Nothing
391 getPrim n ((Prim pn _ arity def _ _) : prims) | n == pn = Just $ execPrim def
392 | otherwise = getPrim n prims
394 execPrim :: ([Const] -> Maybe Const) -> [ExecVal] -> Maybe ExecVal
395 execPrim f args = EConstant <$> (mapM getConst args >>= f)
397 getConst (EConstant c) = Just c
398 getConst _ = Nothing
400 applyPrim :: ([ExecVal] -> Maybe ExecVal) -> [ExecVal] -> Maybe (Exec ExecVal)
401 applyPrim fn args = return <$> fn args
406-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
407-- evaluates them, then begins the checks for matching cases.
408execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
409execCase env ctxt ns sc args =
410 let arity = length ns in
411 if arity <= length args
412 then do let amap = zip ns args
413-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()
414 caseRes <- execCase' env ctxt amap sc
415 case caseRes of
416 Just res -> Just <$> execApp (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)
417 Nothing -> return Nothing
418 else return Nothing
420-- | Take bindings and a case tree and examines them, executing the matching case if possible.
421execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
422execCase' env ctxt amap (UnmatchedCase _) = return Nothing
423execCase' env ctxt amap (STerm tm) =
424 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm
425execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
426 case chooseAlt tm alts of
427 Just (newCase, newBindings) ->
428 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
429 execCase' env ctxt amap' newCase
430 Nothing -> return Nothing
432chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
433chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])
434chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
435chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm
436 , cn == n = Just (sc, zip ns args)
437 | otherwise = chooseAlt tm alts
438chooseAlt tm (_:alts) = chooseAlt tm alts
439chooseAlt _ [] = Nothing
444idrisType :: FType -> ExecVal
445idrisType FUnit = EP Ref unitTy EErased
446idrisType ft = EConstant (idr ft)
447 where idr (FArith ty) = AType ty
448 idr FString = StrType
449 idr FPtr = PtrType
451data Foreign = FFun String [FType] FType deriving Show
454call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
455call (FFun name argTypes retType) args =
456 do fn <- findForeign name
457 maybe (return Nothing) (\f -> Just . ioWrap <$> call' f args retType) fn
458 where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal
459 call' (Fun _ h) args (FArith (ATInt ITNative)) = do
460 res <- execIO $ callFFI h retCInt (prepArgs args)
461 return (EConstant (I (fromIntegral res)))
462 call' (Fun _ h) args (FArith (ATInt (ITFixed IT8))) = do
463 res <- execIO $ callFFI h retCChar (prepArgs args)
464 return (EConstant (B8 (fromIntegral res)))
465 call' (Fun _ h) args (FArith (ATInt (ITFixed IT16))) = do
466 res <- execIO $ callFFI h retCWchar (prepArgs args)
467 return (EConstant (B16 (fromIntegral res)))
468 call' (Fun _ h) args (FArith (ATInt (ITFixed IT32))) = do
469 res <- execIO $ callFFI h retCInt (prepArgs args)
470 return (EConstant (B32 (fromIntegral res)))
471 call' (Fun _ h) args (FArith (ATInt (ITFixed IT64))) = do
472 res <- execIO $ callFFI h retCLong (prepArgs args)
473 return (EConstant (B64 (fromIntegral res)))
474 call' (Fun _ h) args (FArith ATFloat) = do
475 res <- execIO $ callFFI h retCDouble (prepArgs args)
476 return (EConstant (Fl (realToFrac res)))
477 call' (Fun _ h) args (FArith (ATInt ITChar)) = do
478 res <- execIO $ callFFI h retCChar (prepArgs args)
479 return (EConstant (Ch (castCCharToChar res)))
480 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
481 if res == nullPtr
482 then return (EPtr res)
483 else do hStr <- execIO $ peekCString res
484 return (EConstant (Str hStr))
486 call' (Fun _ h) args FPtr = EPtr <$> (execIO $ callFFI h (retPtr retVoid) (prepArgs args))
487 call' (Fun _ h) args FUnit = do _ <- execIO $ callFFI h retVoid (prepArgs args)
488 return $ EP Ref unitCon EErased
489-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
492 prepArgs = map prepArg
493 prepArg (EConstant (I i)) = argCInt (fromIntegral i)
494 prepArg (EConstant (B8 i)) = argCChar (fromIntegral i)
495 prepArg (EConstant (B16 i)) = argCWchar (fromIntegral i)
496 prepArg (EConstant (B32 i)) = argCInt (fromIntegral i)
497 prepArg (EConstant (B64 i)) = argCLong (fromIntegral i)
498 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)
499 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
500 prepArg (EConstant (Str s)) = argString s
501 prepArg (EPtr p) = argPtr p
502 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined
506foreignFromTT :: ExecVal -> Maybe Foreign
507foreignFromTT t = case (unApplyV t) of
508 (_, [(EConstant (Str name)), args, ret]) ->
509 do argTy <- unEList args
510 argFTy <- sequence $ map getFTy argTy
511 retFTy <- getFTy ret
512 return $ FFun name argFTy retFTy
513 _ -> trace ("failed to construct ffun") Nothing
515getFTy :: ExecVal -> Maybe FType
516getFTy (EApp (EP _ (UN fi) _) (EP _ (UN intTy) _))
517 | fi == txt "FIntT" =
518 case str intTy of
519 "ITNative" -> Just (FArith (ATInt ITNative))
520 "ITChar" -> Just (FArith (ATInt ITChar))
521 "IT8" -> Just (FArith (ATInt (ITFixed IT8)))
522 "IT16" -> Just (FArith (ATInt (ITFixed IT16)))
523 "IT32" -> Just (FArith (ATInt (ITFixed IT32)))
524 "IT64" -> Just (FArith (ATInt (ITFixed IT64)))
525 _ -> Nothing
526getFTy (EP _ (UN t) _) =
527 case str t of
528 "FFloat" -> Just (FArith ATFloat)
529 "FString" -> Just FString
530 "FPtr" -> Just FPtr
531 "FUnit" -> Just FUnit
532 _ -> Nothing
533getFTy _ = Nothing
535unEList :: ExecVal -> Maybe [ExecVal]
536unEList tm = case unApplyV tm of
537 (nil, [_]) -> Just []
538 (cons, ([_, x, xs])) ->
539 do rest <- unEList xs
540 return $ x:rest
541 (f, args) -> Nothing
544toConst :: Term -> Maybe Const
545toConst (Constant c) = Just c
546toConst _ = Nothing
548stepForeign :: [ExecVal] -> Exec (Maybe ExecVal)
549stepForeign (ty:fn:args) = let ffun = foreignFromTT fn
550 in case (call <$> ffun) of
551 Just f -> f args
552 Nothing -> return Nothing
553stepForeign _ = fail "Tried to call foreign function that wasn't mkForeignPrim"
555mapMaybeM :: (Functor m, Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]
556mapMaybeM f [] = return []
557mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
558 maybe rest (:rest) <$> f x
559findForeign :: String -> Exec (Maybe ForeignFun)
560findForeign fn = do est <- getExecState
561 let libs = exec_dynamic_libs est
562 fns <- mapMaybeM getFn libs
563 case fns of
564 [f] -> return (Just f)
565 [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"
566 return Nothing
567 fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
568 show (length fs) ++ " occurrences."
569 return Nothing
570 where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)
572#endif