git.iko.soy/Idris-dev
on 3dfa841 help sign in
Idris-dev/src/Idris/Core/Execute.hs
563 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 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) (sMN 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) (sUN "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 res <- execApp' env ctxt newF newArgs
223 return res
224 where getLaziness (EP _ l _) | l == sUN "lazy" = return [False, True]
225 getLaziness (EP _ n _) = do est <- getExecState
226 let argInfo = exec_implicits est
227 case lookupCtxtName n argInfo of
228 [] -> return (repeat False)
229 [ps] -> return $ map lazyarg (snd ps)
230 many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)
231 getLaziness _ = return (repeat False) -- ok due to zip above
232 argExec :: (Term, Bool) -> Exec ExecVal
233 argExec (tm, False) = doExec env ctxt tm
234 argExec (tm, True) = delay env ctxt tm
237execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
238execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
239execApp' env ctxt (EP _ fp _) (ty:action:rest)
240 | fp == upio,
241 (prim__IO, [_, v]) <- unApplyV action
242 = execApp' env ctxt v rest
244execApp' env ctxt (EP _ fp _) args@(_:_:v:k:rest)
245 | fp == piobind,
246 (prim__IO, [_, v']) <- unApplyV v =
247 do v'' <- tryForce v'
248 res <- execApp' env ctxt k [v''] >>= tryForce
249 execApp' env ctxt res rest
250execApp' env ctxt con@(EP _ fp _) args@(tp:v:rest)
251 | fp == pioret =
252 do v' <- tryForce v
253 execApp' env ctxt (mkEApp con [tp, v']) rest
255-- Special cases arising from not having access to the C RTS in the interpreter
256execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str arg):_:rest)
257 | fp == mkfprim,
258 Just (FFun "putStr" _ _) <- foreignFromTT fn
259 = do execIO (putStr arg)
260 execApp' env ctxt ioUnit rest
261execApp' env ctxt (EP _ fp _) (_:fn:_:EHandle h:_:rest)
262 | fp == mkfprim,
263 Just (FFun "idris_readStr" _ _) <- foreignFromTT fn
264 = do contents <- execIO $ hGetLine h
265 execApp' env ctxt (EConstant (Str (contents ++ "\n"))) rest
266execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
267 | fp == mkfprim,
268 Just (FFun "fileOpen" _ _) <- foreignFromTT fn
269 = do m <- case mode of
270 "r" -> return ReadMode
271 "w" -> return WriteMode
272 "a" -> return AppendMode
273 "rw" -> return ReadWriteMode
274 "wr" -> return ReadWriteMode
275 "r+" -> return ReadWriteMode
276 _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)
277 h <- execIO $ openFile f m
278 execApp' env ctxt (ioWrap (EHandle h)) (tail rest)
280execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)
281 | fp == mkfprim,
282 Just (FFun "fileEOF" _ _) <- foreignFromTT fn
283 = do eofp <- execIO $ hIsEOF h
284 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
285 execApp' env ctxt res (tail rest)
287execApp' env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)
288 | fp == mkfprim,
289 Just (FFun "fileClose" _ _) <- foreignFromTT fn
290 = do execIO $ hClose h
291 execApp' env ctxt ioUnit (tail rest)
293execApp' env ctxt (EP _ fp _) (_:fn:(EPtr p):rest)
294 | fp == mkfprim,
295 Just (FFun "isNull" _ _) <- foreignFromTT fn
296 = let res = ioWrap . EConstant . I $
297 if p == nullPtr then 1 else 0
298 in execApp' env ctxt res (tail rest)
300-- A foreign-returned char* has to be tested for NULL sometimes
301execApp' env ctxt (EP _ fp _) (_:fn:EConstant (Str s):rest)
302 | fp == mkfprim,
303 Just (FFun "isNull" _ _) <- foreignFromTT fn
304 = let res = ioWrap . EConstant . I $ 0
305 in execApp' env ctxt res (tail rest)
307-- Throw away the 'World' argument to the foreign function
309execApp' env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim
310 = case foreignFromTT fn of
311 Just (FFun f argTs retT) | length xs >= length argTs ->
312 do let (args', xs') = (take (length argTs) xs, -- foreign args
313 drop (length argTs + 1) xs) -- rest
314 res <- stepForeign (ty:fn:args')
315 case res of
316 Nothing -> fail $ "Could not call foreign function \"" ++ f ++
317 "\" with args " ++ show args
318 Just r -> return (mkEApp r xs')
319 Nothing -> return (mkEApp f args)
321execApp' env ctxt c@(EP (DCon _ arity) n _) args =
322 do args' <- mapM tryForce (take arity args)
323 let restArgs = drop arity args
324 execApp' env ctxt (mkEApp c args') restArgs
326execApp' env ctxt c@(EP (TCon _ arity) n _) args =
327 do args' <- mapM tryForce (take arity args)
328 let restArgs = drop arity args
329 execApp' env ctxt (mkEApp c args') restArgs
331execApp' env ctxt f@(EP _ n _) args =
332 do let val = lookupDef n ctxt
333 case val of
334 [Function _ tm] -> fail "should already have been eval'd"
335 [TyDecl nt ty] -> return $ mkEApp f args
336 [Operator tp arity op] ->
337 if length args >= arity
338 then do args' <- mapM tryForce $ take arity args
339 case getOp n args' of
340 Just res -> do r <- res
341 execApp' env ctxt r (drop arity args)
342 Nothing -> return (mkEApp f args)
343 else return (mkEApp f args)
344 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
345 do rhs <- doExec env ctxt tm
346 execApp' env ctxt rhs args
347 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->
348 do res <- execCase env ctxt ns sc args
349 return $ fromMaybe (mkEApp f args) res
350 thing -> return $ mkEApp f args
351execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
352 let (f', as) = unApplyV ret
353 execApp' env ctxt f' (as ++ args)
354execApp' env ctxt (EThunk i) args = do f <- force i
355 execApp' env ctxt f args
356execApp' env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp' env ctxt f (args1 ++ args2)
357execApp' env ctxt f args = return (mkEApp f args)
359prs = sUN "prim__readString"
360pbm = sUN "prim__believe_me"
361pstd = sUN "prim__stdin"
362mkfprim = sUN "mkForeignPrim"
363pioret = sUN "prim_io_return"
364piobind = sUN "prim_io_bind"
365upio = sUN "unsafePerformPrimIO"
367-- | Look up primitive operations in the global table and transform them into ExecVal functions
368getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
369getOp fn [_, _, x] | fn == pbm = Just (return x)
370getOp fn [EP _ fn' _]
371 | fn == prs && fn' == pstd =
372 Just $ do line <- execIO getLine
373 return (EConstant (Str line))
374getOp fn [EHandle h]
375 | fn == prs =
376 Just $ do contents <- execIO $ hGetLine h
377 return (EConstant (Str (contents ++ "\n")))
378getOp n args = getPrim n primitives >>= flip applyPrim args
379 where getPrim :: Name -> [Prim] -> Maybe ([ExecVal] -> Maybe ExecVal)
380 getPrim n [] = Nothing
381 getPrim n ((Prim pn _ arity def _ _) : prims) | n == pn = Just $ execPrim def
382 | otherwise = getPrim n prims
384 execPrim :: ([Const] -> Maybe Const) -> [ExecVal] -> Maybe ExecVal
385 execPrim f args = EConstant <$> (mapM getConst args >>= f)
387 getConst (EConstant c) = Just c
388 getConst _ = Nothing
390 applyPrim :: ([ExecVal] -> Maybe ExecVal) -> [ExecVal] -> Maybe (Exec ExecVal)
391 applyPrim fn args = return <$> fn args
396-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
397-- evaluates them, then begins the checks for matching cases.
398execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
399execCase env ctxt ns sc args =
400 let arity = length ns in
401 if arity <= length args
402 then do let amap = zip ns args
403-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()
404 caseRes <- execCase' env ctxt amap sc
405 case caseRes of
406 Just res -> Just <$> execApp' (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)
407 Nothing -> return Nothing
408 else return Nothing
410-- | Take bindings and a case tree and examines them, executing the matching case if possible.
411execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
412execCase' env ctxt amap (UnmatchedCase _) = return Nothing
413execCase' env ctxt amap (STerm tm) =
414 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm
415execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
416 do tm' <- tryForce tm
417 case chooseAlt tm' alts of
418 Just (newCase, newBindings) ->
419 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
420 execCase' env ctxt amap' newCase
421 Nothing -> return Nothing
423chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
424chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])
425chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
426chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm
427 , cn == n = Just (sc, zip ns args)
428 | otherwise = chooseAlt tm alts
429chooseAlt tm (_:alts) = chooseAlt tm alts
430chooseAlt _ [] = Nothing
435idrisType :: FType -> ExecVal
436idrisType FUnit = EP Ref unitTy EErased
437idrisType ft = EConstant (idr ft)
438 where idr (FArith ty) = AType ty
439 idr FString = StrType
440 idr FPtr = PtrType
442data Foreign = FFun String [FType] FType deriving Show
445call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
446call (FFun name argTypes retType) args =
447 do fn <- findForeign name
448 maybe (return Nothing) (\f -> Just . ioWrap <$> call' f args retType) fn
449 where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal
450 call' (Fun _ h) args (FArith (ATInt ITNative)) = do
451 res <- execIO $ callFFI h retCInt (prepArgs args)
452 return (EConstant (I (fromIntegral res)))
453 call' (Fun _ h) args (FArith (ATInt (ITFixed IT8))) = do
454 res <- execIO $ callFFI h retCChar (prepArgs args)
455 return (EConstant (B8 (fromIntegral res)))
456 call' (Fun _ h) args (FArith (ATInt (ITFixed IT16))) = do
457 res <- execIO $ callFFI h retCWchar (prepArgs args)
458 return (EConstant (B16 (fromIntegral res)))
459 call' (Fun _ h) args (FArith (ATInt (ITFixed IT32))) = do
460 res <- execIO $ callFFI h retCInt (prepArgs args)
461 return (EConstant (B32 (fromIntegral res)))
462 call' (Fun _ h) args (FArith (ATInt (ITFixed IT64))) = do
463 res <- execIO $ callFFI h retCLong (prepArgs args)
464 return (EConstant (B64 (fromIntegral res)))
465 call' (Fun _ h) args (FArith ATFloat) = do
466 res <- execIO $ callFFI h retCDouble (prepArgs args)
467 return (EConstant (Fl (realToFrac res)))
468 call' (Fun _ h) args (FArith (ATInt ITChar)) = do
469 res <- execIO $ callFFI h retCChar (prepArgs args)
470 return (EConstant (Ch (castCCharToChar res)))
471 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
472 if res == nullPtr
473 then return (EPtr res)
474 else do hStr <- execIO $ peekCString res
475 return (EConstant (Str hStr))
477 call' (Fun _ h) args FPtr = EPtr <$> (execIO $ callFFI h (retPtr retVoid) (prepArgs args))
478 call' (Fun _ h) args FUnit = do _ <- execIO $ callFFI h retVoid (prepArgs args)
479 return $ EP Ref unitCon EErased
480-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
483 prepArgs = map prepArg
484 prepArg (EConstant (I i)) = argCInt (fromIntegral i)
485 prepArg (EConstant (B8 i)) = argCChar (fromIntegral i)
486 prepArg (EConstant (B16 i)) = argCWchar (fromIntegral i)
487 prepArg (EConstant (B32 i)) = argCInt (fromIntegral i)
488 prepArg (EConstant (B64 i)) = argCLong (fromIntegral i)
489 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)
490 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
491 prepArg (EConstant (Str s)) = argString s
492 prepArg (EPtr p) = argPtr p
493 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined
497foreignFromTT :: ExecVal -> Maybe Foreign
498foreignFromTT t = case (unApplyV t) of
499 (_, [(EConstant (Str name)), args, ret]) ->
500 do argTy <- unEList args
501 argFTy <- sequence $ map getFTy argTy
502 retFTy <- getFTy ret
503 return $ FFun name argFTy retFTy
504 _ -> trace ("failed to construct ffun") Nothing
506getFTy :: ExecVal -> Maybe FType
507getFTy (EApp (EP _ (UN fi) _) (EP _ (UN intTy) _))
508 | fi == txt "FIntT" =
509 case str intTy of
510 "ITNative" -> Just (FArith (ATInt ITNative))
511 "ITChar" -> Just (FArith (ATInt ITChar))
512 "IT8" -> Just (FArith (ATInt (ITFixed IT8)))
513 "IT16" -> Just (FArith (ATInt (ITFixed IT16)))
514 "IT32" -> Just (FArith (ATInt (ITFixed IT32)))
515 "IT64" -> Just (FArith (ATInt (ITFixed IT64)))
516 _ -> Nothing
517getFTy (EP _ (UN t) _) =
518 case str t of
519 "FFloat" -> Just (FArith ATFloat)
520 "FString" -> Just FString
521 "FPtr" -> Just FPtr
522 "FUnit" -> Just FUnit
523 _ -> Nothing
524getFTy _ = Nothing
526unEList :: ExecVal -> Maybe [ExecVal]
527unEList tm = case unApplyV tm of
528 (nil, [_]) -> Just []
529 (cons, ([_, x, xs])) ->
530 do rest <- unEList xs
531 return $ x:rest
532 (f, args) -> Nothing
535toConst :: Term -> Maybe Const
536toConst (Constant c) = Just c
537toConst _ = Nothing
539stepForeign :: [ExecVal] -> Exec (Maybe ExecVal)
540stepForeign (ty:fn:args) = let ffun = foreignFromTT fn
541 in case (call <$> ffun) of
542 Just f -> f args
543 Nothing -> return Nothing
544stepForeign _ = fail "Tried to call foreign function that wasn't mkForeignPrim"
546mapMaybeM :: (Functor m, Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]
547mapMaybeM f [] = return []
548mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
549 maybe rest (:rest) <$> f x
550findForeign :: String -> Exec (Maybe ForeignFun)
551findForeign fn = do est <- getExecState
552 let libs = exec_dynamic_libs est
553 fns <- mapMaybeM getFn libs
554 case fns of
555 [f] -> return (Just f)
556 [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"
557 return Nothing
558 fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
559 show (length fs) ++ " occurrences."
560 return Nothing
561 where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)
563#endif