git.iko.soy/Idris-dev
on c79fb21 help sign in
Idris-dev/src/Idris/Core/Execute.hs
584 lines 26 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:ch:_:rest)
232 | fp == mkfprim,
233 Just (FFun "putchar" _ _) <- foreignFromTT fn
234 = case ch of
235 EConstant (Ch c) -> do execIO (putChar c)
236 execApp env ctxt ioUnit rest
237 EConstant (I i) -> do execIO (putChar (toEnum i))
238 execApp env ctxt ioUnit rest
239 _ -> execFail . Msg $
240 "The argument to putchar should be a constant character, but it was " ++
241 show str ++
242 ". Are all cases covered?"
243execApp env ctxt (EP _ fp _) (_:fn:_:handle:_:rest)
244 | fp == mkfprim,
245 Just (FFun "idris_readStr" _ _) <- foreignFromTT fn
246 = case handle of
247 EHandle h -> do contents <- execIO $ hGetLine h
248 execApp env ctxt (EConstant (Str (contents ++ "\n"))) rest
249 _ -> execFail . Msg $
250 "The argument to idris_readStr should be a handle, but it was " ++
251 show handle ++
252 ". Are all cases covered?"
253execApp env ctxt (EP _ fp _) (_:fn:fileStr:modeStr:rest)
254 | fp == mkfprim,
255 Just (FFun "fileOpen" _ _) <- foreignFromTT fn
256 = case (fileStr, modeStr) of
257 (EConstant (Str f), EConstant (Str mode)) ->
258 do f <- execIO $
259 catch (do let m = case mode of
260 "r" -> Right ReadMode
261 "w" -> Right WriteMode
262 "a" -> Right AppendMode
263 "rw" -> Right ReadWriteMode
264 "wr" -> Right ReadWriteMode
265 "r+" -> Right ReadWriteMode
266 _ -> Left ("Invalid mode for " ++ f ++ ": " ++ mode)
267 case fmap (openFile f) m of
268 Right h -> do h' <- h; return $ Right (ioWrap (EHandle h'), tail rest)
269 Left err -> return $ Left err)
270 (\e -> let _ = ( e::SomeException)
271 in return $ Right (ioWrap (EPtr nullPtr), tail rest))
272 case f of
273 Left err -> execFail . Msg $ err
274 Right (res, rest) -> execApp env ctxt res rest
275 _ -> execFail . Msg $
276 "The arguments to fileOpen should be constant strings, but they were " ++
277 show fileStr ++ " and " ++ show modeStr ++
278 ". Are all cases covered?"
280execApp env ctxt (EP _ fp _) (_:fn:handle:rest)
281 | fp == mkfprim,
282 Just (FFun "fileEOF" _ _) <- foreignFromTT fn
283 = case handle of
284 EHandle h -> do eofp <- execIO $ hIsEOF h
285 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
286 execApp env ctxt res (tail rest)
287 _ -> execFail . Msg $
288 "The argument to fileEOF should be a file handle, but it was " ++
289 show handle ++
290 ". Are all cases covered?"
292execApp env ctxt (EP _ fp _) (_:fn:handle:rest)
293 | fp == mkfprim,
294 Just (FFun "fileClose" _ _) <- foreignFromTT fn
295 = case handle of
296 EHandle h -> do execIO $ hClose h
297 execApp env ctxt ioUnit (tail rest)
298 _ -> execFail . Msg $
299 "The argument to fileClose should be a file handle, but it was " ++
300 show handle ++
301 ". Are all cases covered?"
303execApp env ctxt (EP _ fp _) (_:fn:ptr:rest)
304 | fp == mkfprim,
305 Just (FFun "isNull" _ _) <- foreignFromTT fn
306 = case ptr of
307 EPtr p -> let res = ioWrap . EConstant . I $
308 if p == nullPtr then 1 else 0
309 in execApp env ctxt res (tail rest)
310 -- Handles will be checked as null pointers sometimes - but if we got a
311 -- real Handle, then it's valid, so just return 1.
312 EHandle h -> let res = ioWrap . EConstant . I $ 0
313 in execApp env ctxt res (tail rest)
314 -- A foreign-returned char* has to be tested for NULL sometimes
315 EConstant (Str s) -> let res = ioWrap . EConstant . I $ 0
316 in execApp env ctxt res (tail rest)
317 _ -> execFail . Msg $
318 "The argument to isNull should be a pointer or file handle or string, but it was " ++
319 show ptr ++
320 ". Are all cases covered?"
323-- Right now, there's no way to send command-line arguments to the executor,
324-- so just return 0.
325execApp env ctxt (EP _ fp _) (_:fn:rest)
326 | fp == mkfprim,
327 Just (FFun "idris_numArgs" _ _) <- foreignFromTT fn
328 = let res = ioWrap . EConstant . I $ 0
329 in execApp env ctxt res (tail rest)
331execApp env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim
332 = case foreignFromTT fn of
333 Just (FFun f argTs retT) | length xs >= length argTs ->
334 do let (args', xs') = (take (length argTs) xs, -- foreign args
335 drop (length argTs + 1) xs) -- rest
336 res <- stepForeign (ty:fn:args')
337 case res of
338 Nothing -> fail $ "Could not call foreign function \"" ++ f ++
339 "\" with args " ++ show args
340 Just r -> return (mkEApp r xs')
341 Nothing -> return (mkEApp f args)
343execApp env ctxt c@(EP (DCon _ arity) n _) args =
344 do let args' = take arity args
345 let restArgs = drop arity args
346 execApp env ctxt (mkEApp c args') restArgs
348execApp env ctxt c@(EP (TCon _ arity) n _) args =
349 do let args' = take arity args
350 let restArgs = drop arity args
351 execApp env ctxt (mkEApp c args') restArgs
353execApp env ctxt f@(EP _ n _) args =
354 do let val = lookupDef n ctxt
355 case val of
356 [Function _ tm] -> fail "should already have been eval'd"
357 [TyDecl nt ty] -> return $ mkEApp f args
358 [Operator tp arity op] ->
359 if length args >= arity
360 then let args' = take arity args in
361 case getOp n args' of
362 Just res -> do r <- res
363 execApp env ctxt r (drop arity args)
364 Nothing -> return (mkEApp f args)
365 else return (mkEApp f args)
366 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
367 do rhs <- doExec env ctxt tm
368 execApp env ctxt rhs args
369 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->
370 do res <- execCase env ctxt ns sc args
371 return $ fromMaybe (mkEApp f args) res
372 thing -> return $ mkEApp f args
373execApp env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
374 let (f', as) = unApplyV ret
375 execApp env ctxt f' (as ++ args)
376execApp env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp env ctxt f (args1 ++ args2)
377execApp env ctxt f args = return (mkEApp f args)
379prs = sUN "prim__readString"
380pbm = sUN "prim__believe_me"
381pstd = sUN "prim__stdin"
382mkfprim = sUN "mkForeignPrim"
383pioret = sUN "prim_io_return"
384piobind = sUN "prim_io_bind"
385upio = sUN "unsafePerformPrimIO"
386delay = sUN "Delay"
387force = sUN "Force"
389-- | Look up primitive operations in the global table and transform them into ExecVal functions
390getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
391getOp fn [_, _, x] | fn == pbm = Just (return x)
392getOp fn [EP _ fn' _]
393 | fn == prs && fn' == pstd =
394 Just $ do line <- execIO getLine
395 return (EConstant (Str line))
396getOp fn [EHandle h]
397 | fn == prs =
398 Just $ do contents <- execIO $ hGetLine h
399 return (EConstant (Str (contents ++ "\n")))
400getOp n args = getPrim n primitives >>= flip applyPrim args
401 where getPrim :: Name -> [Prim] -> Maybe ([ExecVal] -> Maybe ExecVal)
402 getPrim n [] = Nothing
403 getPrim n ((Prim pn _ arity def _ _) : prims) | n == pn = Just $ execPrim def
404 | otherwise = getPrim n prims
406 execPrim :: ([Const] -> Maybe Const) -> [ExecVal] -> Maybe ExecVal
407 execPrim f args = EConstant <$> (mapM getConst args >>= f)
409 getConst (EConstant c) = Just c
410 getConst _ = Nothing
412 applyPrim :: ([ExecVal] -> Maybe ExecVal) -> [ExecVal] -> Maybe (Exec ExecVal)
413 applyPrim fn args = return <$> fn args
418-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
419-- evaluates them, then begins the checks for matching cases.
420execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
421execCase env ctxt ns sc args =
422 let arity = length ns in
423 if arity <= length args
424 then do let amap = zip ns args
425-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()
426 caseRes <- execCase' env ctxt amap sc
427 case caseRes of
428 Just res -> Just <$> execApp (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)
429 Nothing -> return Nothing
430 else return Nothing
432-- | Take bindings and a case tree and examines them, executing the matching case if possible.
433execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
434execCase' env ctxt amap (UnmatchedCase _) = return Nothing
435execCase' env ctxt amap (STerm tm) =
436 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm
437execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
438 case chooseAlt tm alts of
439 Just (newCase, newBindings) ->
440 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
441 execCase' env ctxt amap' newCase
442 Nothing -> return Nothing
444chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
445chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])
446chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
447chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm
448 , cn == n = Just (sc, zip ns args)
449 | otherwise = chooseAlt tm alts
450chooseAlt tm (_:alts) = chooseAlt tm alts
451chooseAlt _ [] = Nothing
456idrisType :: FType -> ExecVal
457idrisType FUnit = EP Ref unitTy EErased
458idrisType ft = EConstant (idr ft)
459 where idr (FArith ty) = AType ty
460 idr FString = StrType
461 idr FPtr = PtrType
463data Foreign = FFun String [FType] FType deriving Show
466call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
467call (FFun name argTypes retType) args =
468 do fn <- findForeign name
469 maybe (return Nothing) (\f -> Just . ioWrap <$> call' f args retType) fn
470 where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal
471 call' (Fun _ h) args (FArith (ATInt ITNative)) = do
472 res <- execIO $ callFFI h retCInt (prepArgs args)
473 return (EConstant (I (fromIntegral res)))
474 call' (Fun _ h) args (FArith (ATInt (ITFixed IT8))) = do
475 res <- execIO $ callFFI h retCChar (prepArgs args)
476 return (EConstant (B8 (fromIntegral res)))
477 call' (Fun _ h) args (FArith (ATInt (ITFixed IT16))) = do
478 res <- execIO $ callFFI h retCWchar (prepArgs args)
479 return (EConstant (B16 (fromIntegral res)))
480 call' (Fun _ h) args (FArith (ATInt (ITFixed IT32))) = do
481 res <- execIO $ callFFI h retCInt (prepArgs args)
482 return (EConstant (B32 (fromIntegral res)))
483 call' (Fun _ h) args (FArith (ATInt (ITFixed IT64))) = do
484 res <- execIO $ callFFI h retCLong (prepArgs args)
485 return (EConstant (B64 (fromIntegral res)))
486 call' (Fun _ h) args (FArith ATFloat) = do
487 res <- execIO $ callFFI h retCDouble (prepArgs args)
488 return (EConstant (Fl (realToFrac res)))
489 call' (Fun _ h) args (FArith (ATInt ITChar)) = do
490 res <- execIO $ callFFI h retCChar (prepArgs args)
491 return (EConstant (Ch (castCCharToChar res)))
492 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
493 if res == nullPtr
494 then return (EPtr res)
495 else do hStr <- execIO $ peekCString res
496 return (EConstant (Str hStr))
498 call' (Fun _ h) args FPtr = EPtr <$> (execIO $ callFFI h (retPtr retVoid) (prepArgs args))
499 call' (Fun _ h) args FUnit = do _ <- execIO $ callFFI h retVoid (prepArgs args)
500 return $ EP Ref unitCon EErased
501-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
504 prepArgs = map prepArg
505 prepArg (EConstant (I i)) = argCInt (fromIntegral i)
506 prepArg (EConstant (B8 i)) = argCChar (fromIntegral i)
507 prepArg (EConstant (B16 i)) = argCWchar (fromIntegral i)
508 prepArg (EConstant (B32 i)) = argCInt (fromIntegral i)
509 prepArg (EConstant (B64 i)) = argCLong (fromIntegral i)
510 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)
511 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
512 prepArg (EConstant (Str s)) = argString s
513 prepArg (EPtr p) = argPtr p
514 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined
518foreignFromTT :: ExecVal -> Maybe Foreign
519foreignFromTT t = case (unApplyV t) of
520 (_, [(EConstant (Str name)), args, ret]) ->
521 do argTy <- unEList args
522 argFTy <- sequence $ map getFTy argTy
523 retFTy <- getFTy ret
524 return $ FFun name argFTy retFTy
525 _ -> trace ("failed to construct ffun") Nothing
527getFTy :: ExecVal -> Maybe FType
528getFTy (EApp (EP _ (UN fi) _) (EP _ (UN intTy) _))
529 | fi == txt "FIntT" =
530 case str intTy of
531 "ITNative" -> Just (FArith (ATInt ITNative))
532 "ITChar" -> Just (FArith (ATInt ITChar))
533 "IT8" -> Just (FArith (ATInt (ITFixed IT8)))
534 "IT16" -> Just (FArith (ATInt (ITFixed IT16)))
535 "IT32" -> Just (FArith (ATInt (ITFixed IT32)))
536 "IT64" -> Just (FArith (ATInt (ITFixed IT64)))
537 _ -> Nothing
538getFTy (EP _ (UN t) _) =
539 case str t of
540 "FFloat" -> Just (FArith ATFloat)
541 "FString" -> Just FString
542 "FPtr" -> Just FPtr
543 "FUnit" -> Just FUnit
544 _ -> Nothing
545getFTy _ = Nothing
547unEList :: ExecVal -> Maybe [ExecVal]
548unEList tm = case unApplyV tm of
549 (nil, [_]) -> Just []
550 (cons, ([_, x, xs])) ->
551 do rest <- unEList xs
552 return $ x:rest
553 (f, args) -> Nothing
556toConst :: Term -> Maybe Const
557toConst (Constant c) = Just c
558toConst _ = Nothing
560stepForeign :: [ExecVal] -> Exec (Maybe ExecVal)
561stepForeign (ty:fn:args) = let ffun = foreignFromTT fn
562 in case (call <$> ffun) of
563 Just f -> f args
564 Nothing -> return Nothing
565stepForeign _ = fail "Tried to call foreign function that wasn't mkForeignPrim"
567mapMaybeM :: (Functor m, Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]
568mapMaybeM f [] = return []
569mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
570 maybe rest (:rest) <$> f x
571findForeign :: String -> Exec (Maybe ForeignFun)
572findForeign fn = do est <- getExecState
573 let libs = exec_dynamic_libs est
574 fns <- mapMaybeM getFn libs
575 case fns of
576 [f] -> return (Just f)
577 [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"
578 return Nothing
579 fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
580 show (length fs) ++ " occurrences."
581 return Nothing
582 where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)
584#endif