git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/src/Idris/Core/Execute.hs
611 lines 27 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 hiding (forM)
27import Data.Maybe
28import Data.Bits
29import Data.Traversable (forM)
30import Data.Time.Clock.POSIX (getPOSIXTime)
31import qualified Data.Map as M
33#ifdef IDRIS_FFI
34import Foreign.LibFFI
35import Foreign.C.String
36import Foreign.Marshal.Alloc (free)
37import Foreign.Ptr
38#endif
40import System.IO
42#ifndef IDRIS_FFI
43execute :: Term -> Idris Term
44execute tm = fail "libffi not supported, rebuild Idris with -f FFI"
45#else
46-- else is rest of file
47readMay :: (Read a) => String -> Maybe a
48readMay s = case reads s of
49 [(x, "")] -> Just x
50 _ -> Nothing
52data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show
54data ExecState = ExecState { exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
55 , binderNames :: [Name] -- ^ Used to uniquify binders when converting to TT
56 }
58data ExecVal = EP NameType Name ExecVal
59 | EV Int
60 | EBind Name (Binder ExecVal) (ExecVal -> Exec ExecVal)
61 | EApp ExecVal ExecVal
62 | EType UExp
63 | EUType Universe
64 | EErased
65 | EConstant Const
66 | forall a. EPtr (Ptr a)
67 | EThunk Context ExecEnv Term
68 | EHandle Handle
70instance Show ExecVal where
71 show (EP _ n _) = show n
72 show (EV i) = "!!V" ++ show i ++ "!!"
73 show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"
74 show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
75 show (EType _) = "Type"
76 show (EUType _) = "UType"
77 show EErased = "[__]"
78 show (EConstant c) = show c
79 show (EPtr p) = "<<ptr " ++ show p ++ ">>"
80 show (EThunk _ env tm) = "<<thunk " ++ show env ++ "||||" ++ show tm ++ ">>"
81 show (EHandle h) = "<<handle " ++ show h ++ ">>"
83toTT :: ExecVal -> Exec Term
84toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
85toTT (EV i) = return $ V i
86toTT (EBind n b body) = do n' <- newN n
87 body' <- body $ EP Bound n' EErased
88 b' <- fixBinder b
89 Bind n' b' <$> toTT body'
90 where fixBinder (Lam t) = Lam <$> toTT t
91 fixBinder (Pi t k) = Pi <$> toTT t <*> toTT k
92 fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
93 fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2
94 fixBinder (Hole t) = Hole <$> toTT t
95 fixBinder (GHole i t) = GHole i <$> toTT t
96 fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
97 fixBinder (PVar t) = PVar <$> toTT t
98 fixBinder (PVTy t) = PVTy <$> toTT t
99 newN n = do (ExecState hs ns) <- lift get
100 let n' = uniqueName n ns
101 lift (put (ExecState hs (n':ns)))
102 return n'
103toTT (EApp e1 e2) = do e1' <- toTT e1
104 e2' <- toTT e2
105 return $ App e1' e2'
106toTT (EType u) = return $ TType u
107toTT (EUType u) = return $ UType u
108toTT EErased = return Erased
109toTT (EConstant c) = return (Constant c)
110toTT (EThunk ctxt env tm) = do env' <- mapM toBinder env
111 return $ normalise ctxt env' tm
112 where toBinder (n, v) = do v' <- toTT v
113 return (n, Let Erased v')
114toTT (EHandle _) = return Erased
116unApplyV :: ExecVal -> (ExecVal, [ExecVal])
117unApplyV tm = ua [] tm
118 where ua args (EApp f a) = ua (a:args) f
119 ua args t = (t, args)
121mkEApp :: ExecVal -> [ExecVal] -> ExecVal
122mkEApp f [] = f
123mkEApp f (a:args) = mkEApp (EApp f a) args
125initState :: Idris ExecState
126initState = do ist <- getIState
127 return $ ExecState (idris_dynamic_libs ist) []
129type Exec = ErrorT Err (StateT ExecState IO)
131runExec :: Exec a -> ExecState -> IO (Either Err a)
132runExec ex st = fst <$> runStateT (runErrorT ex) st
134getExecState :: Exec ExecState
135getExecState = lift get
137putExecState :: ExecState -> Exec ()
138putExecState = lift . put
140execFail :: Err -> Exec a
141execFail = throwError
143execIO :: IO a -> Exec a
144execIO = lift . lift
147execute :: Term -> Idris Term
148execute tm = do est <- initState
149 ctxt <- getContext
150 res <- lift . lift . flip runExec est $
151 do res <- doExec [] ctxt tm
152 toTT res
153 case res of
154 Left err -> ierror err
155 Right tm' -> return tm'
157ioWrap :: ExecVal -> ExecVal
158ioWrap tm = mkEApp (EP (DCon 0 2 False) (sUN "prim__IO") EErased) [EErased, tm]
160ioUnit :: ExecVal
161ioUnit = ioWrap (EP Ref unitCon EErased)
163type ExecEnv = [(Name, ExecVal)]
165doExec :: ExecEnv -> Context -> Term -> Exec ExecVal
166doExec env ctxt p@(P Ref n ty) | Just v <- lookup n env = return v
167doExec env ctxt p@(P Ref n ty) =
168 do let val = lookupDef n ctxt
169 case val of
170 [Function _ tm] -> doExec env ctxt tm
171 [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def
172 [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later
173 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
174 doExec env ctxt tm
175 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] -> return (EP Ref n EErased)
176 [] -> execFail . Msg $ "Could not find " ++ show n ++ " in definitions."
177 other | length other > 1 -> execFail . Msg $ "Multiple definitions found for " ++ show n
178 | otherwise -> execFail . Msg . take 500 $ "got to " ++ show other ++ " lookup up " ++ show n
179doExec env ctxt p@(P Bound n ty) =
180 case lookup n env of
181 Nothing -> execFail . Msg $ "not found"
182 Just tm -> return tm
183doExec env ctxt (P (DCon a b u) n _) = return (EP (DCon a b u) n EErased)
184doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)
185doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))
186 | otherwise = execFail . Msg $ "env too small"
187doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v
188 doExec ((n, v'):env) ctxt body
189doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
190doExec env ctxt tm@(Bind n b body) = do b' <- forM b (doExec env ctxt)
191 return $
192 EBind n b' (\arg -> doExec ((n, arg):env) ctxt body)
193doExec env ctxt a@(App _ _) =
194 do let (f, args) = unApply a
195 f' <- doExec env ctxt f
196 args' <- case f' of
197 (EP _ d _) | d == delay ->
198 case args of
199 [t,a,tm] -> do t' <- doExec env ctxt t
200 a' <- doExec env ctxt a
201 return [t', a', EThunk ctxt env tm]
202 _ -> mapM (doExec env ctxt) args -- partial applications are fine to evaluate
203 fun' -> do mapM (doExec env ctxt) args
204 execApp env ctxt f' args'
205doExec env ctxt (Constant c) = return (EConstant c)
206doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
207 doExec env ctxt ((x:xs) !! i)
208doExec env ctxt Erased = return EErased
209doExec env ctxt Impossible = fail "Tried to execute an impossible case"
210doExec env ctxt (TType u) = return (EType u)
211doExec env ctxt (UType u) = return (EUType u)
213execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
214execApp env ctxt v [] = return v -- no args is just a constant! can result from function calls
215execApp env ctxt (EP _ f _) (t:a:delayed:rest)
216 | f == force
217 , (_, [_, _, EThunk tmCtxt tmEnv tm]) <- unApplyV delayed =
218 do tm' <- doExec tmEnv tmCtxt tm
219 execApp env ctxt tm' rest
220execApp env ctxt (EP _ fp _) (ty:action:rest)
221 | fp == upio,
222 (prim__IO, [_, v]) <- unApplyV action
223 = execApp env ctxt v rest
225execApp env ctxt (EP _ fp _) args@(_:_:v:k:rest)
226 | fp == piobind,
227 (prim__IO, [_, v']) <- unApplyV v =
228 do res <- execApp env ctxt k [v']
229 execApp env ctxt res rest
230execApp env ctxt con@(EP _ fp _) args@(tp:v:rest)
231 | fp == pioret = execApp env ctxt (mkEApp con [tp, v]) rest
233-- Special cases arising from not having access to the C RTS in the interpreter
234execApp env ctxt (EP _ fp _) (_:fn:str:_:rest)
235 | fp == mkfprim,
236 Just (FFun "putStr" _ _) <- foreignFromTT fn
237 = case str of
238 EConstant (Str arg) -> do execIO (putStr arg)
239 execApp env ctxt ioUnit rest
240 _ -> execFail . Msg $
241 "The argument to putStr should be a constant string, but it was " ++
242 show str ++
243 ". Are all cases covered?"
244execApp env ctxt (EP _ fp _) (_:fn:ch:_:rest)
245 | fp == mkfprim,
246 Just (FFun "putchar" _ _) <- foreignFromTT fn
247 = case ch of
248 EConstant (Ch c) -> do execIO (putChar c)
249 execApp env ctxt ioUnit rest
250 EConstant (I i) -> do execIO (putChar (toEnum i))
251 execApp env ctxt ioUnit rest
252 _ -> execFail . Msg $
253 "The argument to putchar should be a constant character, but it was " ++
254 show str ++
255 ". Are all cases covered?"
256execApp env ctxt (EP _ fp _) (_:fn:_:handle:_:rest)
257 | fp == mkfprim,
258 Just (FFun "idris_readStr" _ _) <- foreignFromTT fn
259 = case handle of
260 EHandle h -> do contents <- execIO $ hGetLine h
261 execApp env ctxt (EConstant (Str (contents ++ "\n"))) rest
262 _ -> execFail . Msg $
263 "The argument to idris_readStr should be a handle, but it was " ++
264 show handle ++
265 ". Are all cases covered?"
266execApp env ctxt (EP _ fp _) (_:fn:rest)
267 | fp == mkfprim,
268 Just (FFun "idris_time" _ _) <- foreignFromTT fn
269 = do execIO $ fmap (ioWrap . EConstant . I . round) getPOSIXTime
270execApp env ctxt (EP _ fp _) (_:fn:fileStr:modeStr:rest)
271 | fp == mkfprim,
272 Just (FFun "fileOpen" _ _) <- foreignFromTT fn
273 = case (fileStr, modeStr) of
274 (EConstant (Str f), EConstant (Str mode)) ->
275 do f <- execIO $
276 catch (do let m = case mode of
277 "r" -> Right ReadMode
278 "w" -> Right WriteMode
279 "a" -> Right AppendMode
280 "rw" -> Right ReadWriteMode
281 "wr" -> Right ReadWriteMode
282 "r+" -> Right ReadWriteMode
283 _ -> Left ("Invalid mode for " ++ f ++ ": " ++ mode)
284 case fmap (openFile f) m of
285 Right h -> do h' <- h
286 hSetBinaryMode h' True
287 return $ Right (ioWrap (EHandle h'), tail rest)
288 Left err -> return $ Left err)
289 (\e -> let _ = ( e::SomeException)
290 in return $ Right (ioWrap (EPtr nullPtr), tail rest))
291 case f of
292 Left err -> execFail . Msg $ err
293 Right (res, rest) -> execApp env ctxt res rest
294 _ -> execFail . Msg $
295 "The arguments to fileOpen should be constant strings, but they were " ++
296 show fileStr ++ " and " ++ show modeStr ++
297 ". Are all cases covered?"
299execApp env ctxt (EP _ fp _) (_:fn:handle:rest)
300 | fp == mkfprim,
301 Just (FFun "fileEOF" _ _) <- foreignFromTT fn
302 = case handle of
303 EHandle h -> do eofp <- execIO $ hIsEOF h
304 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
305 execApp env ctxt res (tail rest)
306 _ -> execFail . Msg $
307 "The argument to fileEOF should be a file handle, but it was " ++
308 show handle ++
309 ". Are all cases covered?"
311execApp env ctxt (EP _ fp _) (_:fn:handle:rest)
312 | fp == mkfprim,
313 Just (FFun "fileClose" _ _) <- foreignFromTT fn
314 = case handle of
315 EHandle h -> do execIO $ hClose h
316 execApp env ctxt ioUnit (tail rest)
317 _ -> execFail . Msg $
318 "The argument to fileClose should be a file handle, but it was " ++
319 show handle ++
320 ". Are all cases covered?"
322execApp env ctxt (EP _ fp _) (_:fn:ptr:rest)
323 | fp == mkfprim,
324 Just (FFun "isNull" _ _) <- foreignFromTT fn
325 = case ptr of
326 EPtr p -> let res = ioWrap . EConstant . I $
327 if p == nullPtr then 1 else 0
328 in execApp env ctxt res (tail rest)
329 -- Handles will be checked as null pointers sometimes - but if we got a
330 -- real Handle, then it's valid, so just return 1.
331 EHandle h -> let res = ioWrap . EConstant . I $ 0
332 in execApp env ctxt res (tail rest)
333 -- A foreign-returned char* has to be tested for NULL sometimes
334 EConstant (Str s) -> let res = ioWrap . EConstant . I $ 0
335 in execApp env ctxt res (tail rest)
336 _ -> execFail . Msg $
337 "The argument to isNull should be a pointer or file handle or string, but it was " ++
338 show ptr ++
339 ". Are all cases covered?"
342-- Right now, there's no way to send command-line arguments to the executor,
343-- so just return 0.
344execApp env ctxt (EP _ fp _) (_:fn:rest)
345 | fp == mkfprim,
346 Just (FFun "idris_numArgs" _ _) <- foreignFromTT fn
347 = let res = ioWrap . EConstant . I $ 0
348 in execApp env ctxt res (tail rest)
350execApp env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim
351 = case foreignFromTT fn of
352 Just (FFun f argTs retT) | length xs >= length argTs ->
353 do let (args', xs') = (take (length argTs) xs, -- foreign args
354 drop (length argTs + 1) xs) -- rest
355 res <- stepForeign (ty:fn:args')
356 case res of
357 Nothing -> fail $ "Could not call foreign function \"" ++ f ++
358 "\" with args " ++ show args
359 Just r -> return (mkEApp r xs')
360 Nothing -> return (mkEApp f args)
362execApp env ctxt c@(EP (DCon _ arity _) n _) args =
363 do let args' = take arity args
364 let restArgs = drop arity args
365 execApp env ctxt (mkEApp c args') restArgs
367execApp env ctxt c@(EP (TCon _ arity) n _) args =
368 do let args' = take arity args
369 let restArgs = drop arity args
370 execApp env ctxt (mkEApp c args') restArgs
372execApp env ctxt f@(EP _ n _) args =
373 do let val = lookupDef n ctxt
374 case val of
375 [Function _ tm] -> fail "should already have been eval'd"
376 [TyDecl nt ty] -> return $ mkEApp f args
377 [Operator tp arity op] ->
378 if length args >= arity
379 then let args' = take arity args in
380 case getOp n args' of
381 Just res -> do r <- res
382 execApp env ctxt r (drop arity args)
383 Nothing -> return (mkEApp f args)
384 else return (mkEApp f args)
385 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
386 do rhs <- doExec env ctxt tm
387 execApp env ctxt rhs args
388 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->
389 do res <- execCase env ctxt ns sc args
390 return $ fromMaybe (mkEApp f args) res
391 thing -> return $ mkEApp f args
392execApp env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
393 let (f', as) = unApplyV ret
394 execApp env ctxt f' (as ++ args)
395execApp env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp env ctxt f (args1 ++ args2)
396execApp env ctxt f args = return (mkEApp f args)
398prs = sUN "prim__readString"
399pbm = sUN "prim__believe_me"
400pstd = sUN "prim__stdin"
401mkfprim = sUN "mkForeignPrim"
402pioret = sUN "prim_io_return"
403piobind = sUN "prim_io_bind"
404upio = sUN "unsafePerformPrimIO"
405delay = sUN "Delay"
406force = sUN "Force"
408-- | Look up primitive operations in the global table and transform them into ExecVal functions
409getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
410getOp fn [_, _, x] | fn == pbm = Just (return x)
411getOp fn [EP _ fn' _]
412 | fn == prs && fn' == pstd =
413 Just $ do line <- execIO getLine
414 return (EConstant (Str line))
415getOp fn [EHandle h]
416 | fn == prs =
417 Just $ do contents <- execIO $ hGetLine h
418 return (EConstant (Str (contents ++ "\n")))
419getOp n args = getPrim n primitives >>= flip applyPrim args
420 where getPrim :: Name -> [Prim] -> Maybe ([ExecVal] -> Maybe ExecVal)
421 getPrim n [] = Nothing
422 getPrim n ((Prim pn _ arity def _ _) : prims) | n == pn = Just $ execPrim def
423 | otherwise = getPrim n prims
425 execPrim :: ([Const] -> Maybe Const) -> [ExecVal] -> Maybe ExecVal
426 execPrim f args = EConstant <$> (mapM getConst args >>= f)
428 getConst (EConstant c) = Just c
429 getConst _ = Nothing
431 applyPrim :: ([ExecVal] -> Maybe ExecVal) -> [ExecVal] -> Maybe (Exec ExecVal)
432 applyPrim fn args = return <$> fn args
437-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
438-- evaluates them, then begins the checks for matching cases.
439execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
440execCase env ctxt ns sc args =
441 let arity = length ns in
442 if arity <= length args
443 then do let amap = zip ns args
444-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()
445 caseRes <- execCase' env ctxt amap sc
446 case caseRes of
447 Just res -> Just <$> execApp (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)
448 Nothing -> return Nothing
449 else return Nothing
451-- | Take bindings and a case tree and examines them, executing the matching case if possible.
452execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
453execCase' env ctxt amap (UnmatchedCase _) = return Nothing
454execCase' env ctxt amap (STerm tm) =
455 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm
456execCase' env ctxt amap (Case sh n alts) | Just tm <- lookup n amap =
457 case chooseAlt tm alts of
458 Just (newCase, newBindings) ->
459 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
460 execCase' env ctxt amap' newCase
461 Nothing -> return Nothing
463chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
464chooseAlt tm (DefaultCase sc : alts) | ok tm = Just (sc, [])
465 | otherwise = Nothing
466 where -- Default cases should only work on applications of constructors or on constants
467 ok (EApp f x) = ok f
468 ok (EP Bound _ _) = False
469 ok (EP Ref _ _) = False
470 ok _ = True
473chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
474chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm
475 , cn == n = Just (sc, zip ns args)
476 | otherwise = chooseAlt tm alts
477chooseAlt tm (_:alts) = chooseAlt tm alts
478chooseAlt _ [] = Nothing
483idrisType :: FType -> ExecVal
484idrisType FUnit = EP Ref unitTy EErased
485idrisType ft = EConstant (idr ft)
486 where idr (FArith ty) = AType ty
487 idr FString = StrType
488 idr FPtr = PtrType
490data Foreign = FFun String [FType] FType deriving Show
493call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
494call (FFun name argTypes retType) args =
495 do fn <- findForeign name
496 maybe (return Nothing) (\f -> Just . ioWrap <$> call' f args retType) fn
497 where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal
498 call' (Fun _ h) args (FArith (ATInt ITNative)) = do
499 res <- execIO $ callFFI h retCInt (prepArgs args)
500 return (EConstant (I (fromIntegral res)))
501 call' (Fun _ h) args (FArith (ATInt (ITFixed IT8))) = do
502 res <- execIO $ callFFI h retCChar (prepArgs args)
503 return (EConstant (B8 (fromIntegral res)))
504 call' (Fun _ h) args (FArith (ATInt (ITFixed IT16))) = do
505 res <- execIO $ callFFI h retCWchar (prepArgs args)
506 return (EConstant (B16 (fromIntegral res)))
507 call' (Fun _ h) args (FArith (ATInt (ITFixed IT32))) = do
508 res <- execIO $ callFFI h retCInt (prepArgs args)
509 return (EConstant (B32 (fromIntegral res)))
510 call' (Fun _ h) args (FArith (ATInt (ITFixed IT64))) = do
511 res <- execIO $ callFFI h retCLong (prepArgs args)
512 return (EConstant (B64 (fromIntegral res)))
513 call' (Fun _ h) args (FArith ATFloat) = do
514 res <- execIO $ callFFI h retCDouble (prepArgs args)
515 return (EConstant (Fl (realToFrac res)))
516 call' (Fun _ h) args (FArith (ATInt ITChar)) = do
517 res <- execIO $ callFFI h retCChar (prepArgs args)
518 return (EConstant (Ch (castCCharToChar res)))
519 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
520 if res == nullPtr
521 then return (EPtr res)
522 else do hStr <- execIO $ peekCString res
523 return (EConstant (Str hStr))
525 call' (Fun _ h) args FPtr = EPtr <$> (execIO $ callFFI h (retPtr retVoid) (prepArgs args))
526 call' (Fun _ h) args FUnit = do _ <- execIO $ callFFI h retVoid (prepArgs args)
527 return $ EP Ref unitCon EErased
528-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
531 prepArgs = map prepArg
532 prepArg (EConstant (I i)) = argCInt (fromIntegral i)
533 prepArg (EConstant (B8 i)) = argCChar (fromIntegral i)
534 prepArg (EConstant (B16 i)) = argCWchar (fromIntegral i)
535 prepArg (EConstant (B32 i)) = argCInt (fromIntegral i)
536 prepArg (EConstant (B64 i)) = argCLong (fromIntegral i)
537 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)
538 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
539 prepArg (EConstant (Str s)) = argString s
540 prepArg (EPtr p) = argPtr p
541 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined
545foreignFromTT :: ExecVal -> Maybe Foreign
546foreignFromTT t = case (unApplyV t) of
547 (_, [(EConstant (Str name)), args, ret]) ->
548 do argTy <- unEList args
549 argFTy <- sequence $ map getFTy argTy
550 retFTy <- getFTy ret
551 return $ FFun name argFTy retFTy
552 _ -> trace ("failed to construct ffun") Nothing
554getFTy :: ExecVal -> Maybe FType
555getFTy (EApp (EP _ (UN fi) _) (EP _ (UN intTy) _))
556 | fi == txt "FIntT" =
557 case str intTy of
558 "ITNative" -> Just (FArith (ATInt ITNative))
559 "ITChar" -> Just (FArith (ATInt ITChar))
560 "IT8" -> Just (FArith (ATInt (ITFixed IT8)))
561 "IT16" -> Just (FArith (ATInt (ITFixed IT16)))
562 "IT32" -> Just (FArith (ATInt (ITFixed IT32)))
563 "IT64" -> Just (FArith (ATInt (ITFixed IT64)))
564 _ -> Nothing
565getFTy (EP _ (UN t) _) =
566 case str t of
567 "FFloat" -> Just (FArith ATFloat)
568 "FString" -> Just FString
569 "FPtr" -> Just FPtr
570 "FUnit" -> Just FUnit
571 _ -> Nothing
572getFTy _ = Nothing
574unEList :: ExecVal -> Maybe [ExecVal]
575unEList tm = case unApplyV tm of
576 (nil, [_]) -> Just []
577 (cons, ([_, x, xs])) ->
578 do rest <- unEList xs
579 return $ x:rest
580 (f, args) -> Nothing
583toConst :: Term -> Maybe Const
584toConst (Constant c) = Just c
585toConst _ = Nothing
587stepForeign :: [ExecVal] -> Exec (Maybe ExecVal)
588stepForeign (ty:fn:args) = let ffun = foreignFromTT fn
589 in case (call <$> ffun) of
590 Just f -> f args
591 Nothing -> return Nothing
592stepForeign _ = fail "Tried to call foreign function that wasn't mkForeignPrim"
594mapMaybeM :: (Functor m, Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]
595mapMaybeM f [] = return []
596mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
597 maybe rest (:rest) <$> f x
598findForeign :: String -> Exec (Maybe ForeignFun)
599findForeign fn = do est <- getExecState
600 let libs = exec_dynamic_libs est
601 fns <- mapMaybeM getFn libs
602 case fns of
603 [f] -> return (Just f)
604 [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"
605 return Nothing
606 fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
607 show (length fs) ++ " occurrences."
608 return Nothing
609 where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)
611#endif