git.iko.soy/Idris-dev
on de2011f help sign in
Idris-dev/src/Idris/Core/Execute.hs
650 lines 29 kB history raw
1{-# LANGUAGE PatternGuards, ExistentialQuantification, CPP #-}
2module Idris.Core.Execute (execute) where
4import Idris.AbsSyntax
5import Idris.AbsSyntaxTree
6import IRTS.Lang(FDesc(..), 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.Except (ExceptT, runExceptT, throwE)
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 i t k) = Pi i <$> 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 = ExceptT Err (StateT ExecState IO)
131runExec :: Exec a -> ExecState -> IO (Either Err a)
132runExec ex st = fst <$> runStateT (runExceptT ex) st
134getExecState :: Exec ExecState
135getExecState = lift get
137putExecState :: ExecState -> Exec ()
138putExecState = lift . put
140execFail :: Err -> Exec a
141execFail = throwE
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 f@(EP _ fp _) args@(xs:_:_:_:args')
235 | fp == mkfprim,
236 (ty : fn : w : rest) <- reverse args' =
237 execForeign env ctxt getArity ty fn rest (mkEApp f args)
238 where getArity = case unEList xs of
239 Just as -> length as
240 _ -> 0
242execApp env ctxt c@(EP (DCon _ arity _) n _) args =
243 do let args' = take arity args
244 let restArgs = drop arity args
245 execApp env ctxt (mkEApp c args') restArgs
247execApp env ctxt c@(EP (TCon _ arity) n _) args =
248 do let args' = take arity args
249 let restArgs = drop arity args
250 execApp env ctxt (mkEApp c args') restArgs
252execApp env ctxt f@(EP _ n _) args =
253 do let val = lookupDef n ctxt
254 case val of
255 [Function _ tm] -> fail "should already have been eval'd"
256 [TyDecl nt ty] -> return $ mkEApp f args
257 [Operator tp arity op] ->
258 if length args >= arity
259 then let args' = take arity args in
260 case getOp n args' of
261 Just res -> do r <- res
262 execApp env ctxt r (drop arity args)
263 Nothing -> return (mkEApp f args)
264 else return (mkEApp f args)
265 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
266 do rhs <- doExec env ctxt tm
267 execApp env ctxt rhs args
268 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->
269 do res <- execCase env ctxt ns sc args
270 return $ fromMaybe (mkEApp f args) res
271 thing -> return $ mkEApp f args
272execApp env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
273 let (f', as) = unApplyV ret
274 execApp env ctxt f' (as ++ args)
275execApp env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp env ctxt f (args1 ++ args2)
276execApp env ctxt f args = return (mkEApp f args)
278execForeign env ctxt arity ty fn xs onfail
279 | Just (FFun "putStr" [(_, str)] _) <- foreignFromTT arity ty fn xs
280 = case str of
281 EConstant (Str arg) -> do execIO (putStr arg)
282 execApp env ctxt ioUnit (drop arity xs)
283 _ -> execFail . Msg $
284 "The argument to putStr should be a constant string, but it was " ++
285 show str ++
286 ". Are all cases covered?"
287 | Just (FFun "putchar" [(_, ch)] _) <- foreignFromTT arity ty fn xs
288 = case ch of
289 EConstant (Ch c) -> do execIO (putChar c)
290 execApp env ctxt ioUnit (drop arity xs)
291 EConstant (I i) -> do execIO (putChar (toEnum i))
292 execApp env ctxt ioUnit (drop arity xs)
293 _ -> execFail . Msg $
294 "The argument to putchar should be a constant character, but it was " ++
295 show str ++
296 ". Are all cases covered?"
297 | Just (FFun "idris_readStr" [_, (_, handle)] _) <- foreignFromTT arity ty fn xs
298 = case handle of
299 EHandle h -> do contents <- execIO $ hGetLine h
300 execApp env ctxt (EConstant (Str (contents ++ "\n"))) (drop arity xs)
301 _ -> execFail . Msg $
302 "The argument to idris_readStr should be a handle, but it was " ++
303 show handle ++
304 ". Are all cases covered?"
305 | Just (FFun "getchar" _ _) <- foreignFromTT arity ty fn xs
306 = do -- The C API returns an Int which Idris library code
307 -- converts; thus, we must make an int here.
308 ch <- execIO $ fmap (ioWrap . EConstant . I . fromEnum) getChar
309 execApp env ctxt ch xs
310 | Just (FFun "idris_time" _ _) <- foreignFromTT arity ty fn xs
311 = do execIO $ fmap (ioWrap . EConstant . I . round) getPOSIXTime
312 | Just (FFun "fileOpen" [(_,fileStr), (_,modeStr)] _) <- foreignFromTT arity ty fn xs
313 = case (fileStr, modeStr) of
314 (EConstant (Str f), EConstant (Str mode)) ->
315 do f <- execIO $
316 catch (do let m = case mode of
317 "r" -> Right ReadMode
318 "w" -> Right WriteMode
319 "a" -> Right AppendMode
320 "rw" -> Right ReadWriteMode
321 "wr" -> Right ReadWriteMode
322 "r+" -> Right ReadWriteMode
323 _ -> Left ("Invalid mode for " ++ f ++ ": " ++ mode)
324 case fmap (openFile f) m of
325 Right h -> do h' <- h
326 hSetBinaryMode h' True
327 return $ Right (ioWrap (EHandle h'), drop arity xs)
328 Left err -> return $ Left err)
329 (\e -> let _ = ( e::SomeException)
330 in return $ Right (ioWrap (EPtr nullPtr), drop arity xs))
331 case f of
332 Left err -> execFail . Msg $ err
333 Right (res, rest) -> execApp env ctxt res rest
334 _ -> execFail . Msg $
335 "The arguments to fileOpen should be constant strings, but they were " ++
336 show fileStr ++ " and " ++ show modeStr ++
337 ". Are all cases covered?"
338 | Just (FFun "fileEOF" [(_,handle)] _) <- foreignFromTT arity ty fn xs
339 = case handle of
340 EHandle h -> do eofp <- execIO $ hIsEOF h
341 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
342 execApp env ctxt res (drop arity xs)
343 _ -> execFail . Msg $
344 "The argument to fileEOF should be a file handle, but it was " ++
345 show handle ++
346 ". Are all cases covered?"
347 | Just (FFun "fileClose" [(_,handle)] _) <- foreignFromTT arity ty fn xs
348 = case handle of
349 EHandle h -> do execIO $ hClose h
350 execApp env ctxt ioUnit (drop arity xs)
351 _ -> execFail . Msg $
352 "The argument to fileClose should be a file handle, but it was " ++
353 show handle ++
354 ". Are all cases covered?"
356 | Just (FFun "isNull" [(_, ptr)] _) <- foreignFromTT arity ty fn xs
357 = case ptr of
358 EPtr p -> let res = ioWrap . EConstant . I $
359 if p == nullPtr then 1 else 0
360 in execApp env ctxt res (drop arity xs)
361 -- Handles will be checked as null pointers sometimes - but if we got a
362 -- real Handle, then it's valid, so just return 1.
363 EHandle h -> let res = ioWrap . EConstant . I $ 0
364 in execApp env ctxt res (drop arity xs)
365 -- A foreign-returned char* has to be tested for NULL sometimes
366 EConstant (Str s) -> let res = ioWrap . EConstant . I $ 0
367 in execApp env ctxt res (drop arity xs)
368 _ -> execFail . Msg $
369 "The argument to isNull should be a pointer or file handle or string, but it was " ++
370 show ptr ++
371 ". Are all cases covered?"
373-- Right now, there's no way to send command-line arguments to the executor,
374-- so just return 0.
375execForeign env ctxt arity ty fn xs onfail
376 | Just (FFun "idris_numArgs" _ _) <- foreignFromTT arity ty fn xs
377 = let res = ioWrap . EConstant . I $ 0
378 in execApp env ctxt res (drop arity xs)
380execForeign env ctxt arity ty fn xs onfail
381 = case foreignFromTT arity ty fn xs of
382 Just ffun@(FFun f argTs retT) | length xs >= arity ->
383 do let (args', xs') = (take arity xs, -- foreign args
384 drop arity xs) -- rest
385 res <- call ffun (map snd argTs)
386 case res of
387 Nothing -> fail $ "Could not call foreign function \"" ++ f ++
388 "\" with args " ++ show (map snd argTs)
389 Just r -> return (mkEApp r xs')
390 Nothing -> return onfail
393splitArg tm | (_, [_,_,l,r]) <- unApplyV tm -- pair, two implicits
394 = Just (toFDesc l, r)
395splitArg _ = Nothing
397toFDesc tm
398 | (EP _ n _, []) <- unApplyV tm = FCon (deNS n)
399 | (EP _ n _, as) <- unApplyV tm = FApp (deNS n) (map toFDesc as)
400toFDesc _ = FUnknown
402deNS (NS n _) = n
403deNS n = n
405prf = sUN "prim__readFile"
406pwf = sUN "prim__writeFile"
407prs = sUN "prim__readString"
408pws = sUN "prim__writeString"
409pbm = sUN "prim__believe_me"
410pstdin = sUN "prim__stdin"
411pstdout = sUN "prim__stdout"
412mkfprim = sUN "mkForeignPrim"
413pioret = sUN "prim_io_return"
414piobind = sUN "prim_io_bind"
415upio = sUN "unsafePerformPrimIO"
416delay = sUN "Delay"
417force = sUN "Force"
419-- | Look up primitive operations in the global table and transform them into ExecVal functions
420getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
421getOp fn [_, _, x] | fn == pbm = Just (return x)
422getOp fn [_, EConstant (Str n)]
423 | fn == pws =
424 Just $ do execIO $ putStr n
425 return (EConstant (I 0))
426getOp fn [_]
427 | fn == prs =
428 Just $ do line <- execIO getLine
429 return (EConstant (Str line))
430getOp fn [_, EP _ fn' _, EConstant (Str n)]
431 | fn == pwf && fn' == pstdout =
432 Just $ do execIO $ putStr n
433 return (EConstant (I 0))
434getOp fn [_, EP _ fn' _]
435 | fn == prf && fn' == pstdin =
436 Just $ do line <- execIO getLine
437 return (EConstant (Str line))
438getOp fn [_, EHandle h, EConstant (Str n)]
439 | fn == pwf =
440 Just $ do execIO $ hPutStr h n
441 return (EConstant (I 0))
442getOp fn [_, EHandle h]
443 | fn == prf =
444 Just $ do contents <- execIO $ hGetLine h
445 return (EConstant (Str (contents ++ "\n")))
446getOp n args = getPrim n primitives >>= flip applyPrim args
447 where getPrim :: Name -> [Prim] -> Maybe ([ExecVal] -> Maybe ExecVal)
448 getPrim n [] = Nothing
449 getPrim n ((Prim pn _ arity def _ _) : prims) | n == pn = Just $ execPrim def
450 | otherwise = getPrim n prims
452 execPrim :: ([Const] -> Maybe Const) -> [ExecVal] -> Maybe ExecVal
453 execPrim f args = EConstant <$> (mapM getConst args >>= f)
455 getConst (EConstant c) = Just c
456 getConst _ = Nothing
458 applyPrim :: ([ExecVal] -> Maybe ExecVal) -> [ExecVal] -> Maybe (Exec ExecVal)
459 applyPrim fn args = return <$> fn args
464-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
465-- evaluates them, then begins the checks for matching cases.
466execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
467execCase env ctxt ns sc args =
468 let arity = length ns in
469 if arity <= length args
470 then do let amap = zip ns args
471-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()
472 caseRes <- execCase' env ctxt amap sc
473 case caseRes of
474 Just res -> Just <$> execApp (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)
475 Nothing -> return Nothing
476 else return Nothing
478-- | Take bindings and a case tree and examines them, executing the matching case if possible.
479execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
480execCase' env ctxt amap (UnmatchedCase _) = return Nothing
481execCase' env ctxt amap (STerm tm) =
482 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm
483execCase' env ctxt amap (Case sh n alts) | Just tm <- lookup n amap =
484 case chooseAlt tm alts of
485 Just (newCase, newBindings) ->
486 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
487 execCase' env ctxt amap' newCase
488 Nothing -> return Nothing
490chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
491chooseAlt tm (DefaultCase sc : alts) | ok tm = Just (sc, [])
492 | otherwise = Nothing
493 where -- Default cases should only work on applications of constructors or on constants
494 ok (EApp f x) = ok f
495 ok (EP Bound _ _) = False
496 ok (EP Ref _ _) = False
497 ok _ = True
500chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
501chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm
502 , cn == n = Just (sc, zip ns args)
503 | otherwise = chooseAlt tm alts
504chooseAlt tm (_:alts) = chooseAlt tm alts
505chooseAlt _ [] = Nothing
510idrisType :: FType -> ExecVal
511idrisType FUnit = EP Ref unitTy EErased
512idrisType ft = EConstant (idr ft)
513 where idr (FArith ty) = AType ty
514 idr FString = StrType
515 idr FPtr = PtrType
517data Foreign = FFun String [(FDesc, ExecVal)] FDesc deriving Show
519toFType :: FDesc -> FType
520toFType (FCon c)
521 | c == sUN "C_Str" = FString
522 | c == sUN "C_Float" = FArith ATFloat
523 | c == sUN "C_Ptr" = FPtr
524 | c == sUN "C_MPtr" = FManagedPtr
525 | c == sUN "C_Unit" = FUnit
526toFType (FApp c [_,ity])
527 | c == sUN "C_IntT" = FArith (toAType ity)
528 where toAType (FCon i)
529 | i == sUN "C_IntChar" = ATInt ITChar
530 | i == sUN "C_IntNative" = ATInt ITNative
531 | i == sUN "C_IntBits8" = ATInt (ITFixed IT8)
532 | i == sUN "C_IntBits16" = ATInt (ITFixed IT16)
533 | i == sUN "C_IntBits32" = ATInt (ITFixed IT32)
534 | i == sUN "C_IntBits64" = ATInt (ITFixed IT64)
535 toAType t = error (show t ++ " not defined in toAType")
537toFType (FApp c [_])
538 | c == sUN "C_Any" = FAny
539toFType t = error (show t ++ " not defined in toFType")
541call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
542call (FFun name argTypes retType) args =
543 do fn <- findForeign name
544 maybe (return Nothing)
545 (\f -> Just . ioWrap <$> call' f args (toFType retType)) fn
546 where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal
547 call' (Fun _ h) args (FArith (ATInt ITNative)) = do
548 res <- execIO $ callFFI h retCInt (prepArgs args)
549 return (EConstant (I (fromIntegral res)))
550 call' (Fun _ h) args (FArith (ATInt (ITFixed IT8))) = do
551 res <- execIO $ callFFI h retCChar (prepArgs args)
552 return (EConstant (B8 (fromIntegral res)))
553 call' (Fun _ h) args (FArith (ATInt (ITFixed IT16))) = do
554 res <- execIO $ callFFI h retCWchar (prepArgs args)
555 return (EConstant (B16 (fromIntegral res)))
556 call' (Fun _ h) args (FArith (ATInt (ITFixed IT32))) = do
557 res <- execIO $ callFFI h retCInt (prepArgs args)
558 return (EConstant (B32 (fromIntegral res)))
559 call' (Fun _ h) args (FArith (ATInt (ITFixed IT64))) = do
560 res <- execIO $ callFFI h retCLong (prepArgs args)
561 return (EConstant (B64 (fromIntegral res)))
562 call' (Fun _ h) args (FArith ATFloat) = do
563 res <- execIO $ callFFI h retCDouble (prepArgs args)
564 return (EConstant (Fl (realToFrac res)))
565 call' (Fun _ h) args (FArith (ATInt ITChar)) = do
566 res <- execIO $ callFFI h retCChar (prepArgs args)
567 return (EConstant (Ch (castCCharToChar res)))
568 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
569 if res == nullPtr
570 then return (EPtr res)
571 else do hStr <- execIO $ peekCString res
572 return (EConstant (Str hStr))
574 call' (Fun _ h) args FPtr = EPtr <$> (execIO $ callFFI h (retPtr retVoid) (prepArgs args))
575 call' (Fun _ h) args FUnit = do _ <- execIO $ callFFI h retVoid (prepArgs args)
576 return $ EP Ref unitCon EErased
579 prepArgs = map prepArg
580 prepArg (EConstant (I i)) = argCInt (fromIntegral i)
581 prepArg (EConstant (B8 i)) = argCChar (fromIntegral i)
582 prepArg (EConstant (B16 i)) = argCWchar (fromIntegral i)
583 prepArg (EConstant (B32 i)) = argCInt (fromIntegral i)
584 prepArg (EConstant (B64 i)) = argCLong (fromIntegral i)
585 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)
586 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
587 -- Issue #1720 on the issue tracker.
588 -- https://github.com/idris-lang/Idris-dev/issues/1720
589 prepArg (EConstant (Str s)) = argString s
590 prepArg (EPtr p) = argPtr p
591 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined
594foreignFromTT :: Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
595foreignFromTT arity ty (EConstant (Str name)) args
596 = do argFTyVals <- mapM splitArg (take arity args)
597 return $ FFun name argFTyVals (toFDesc ty)
598foreignFromTT arity ty fn args = trace ("failed to construct ffun from " ++ show (ty,fn,args)) Nothing
600getFTy :: ExecVal -> Maybe FType
601getFTy (EApp (EP _ (UN fi) _) (EP _ (UN intTy) _))
602 | fi == txt "FIntT" =
603 case str intTy of
604 "ITNative" -> Just (FArith (ATInt ITNative))
605 "ITChar" -> Just (FArith (ATInt ITChar))
606 "IT8" -> Just (FArith (ATInt (ITFixed IT8)))
607 "IT16" -> Just (FArith (ATInt (ITFixed IT16)))
608 "IT32" -> Just (FArith (ATInt (ITFixed IT32)))
609 "IT64" -> Just (FArith (ATInt (ITFixed IT64)))
610 _ -> Nothing
611getFTy (EP _ (UN t) _) =
612 case str t of
613 "FFloat" -> Just (FArith ATFloat)
614 "FString" -> Just FString
615 "FPtr" -> Just FPtr
616 "FUnit" -> Just FUnit
617 _ -> Nothing
618getFTy _ = Nothing
620unEList :: ExecVal -> Maybe [ExecVal]
621unEList tm = case unApplyV tm of
622 (nil, [_]) -> Just []
623 (cons, ([_, x, xs])) ->
624 do rest <- unEList xs
625 return $ x:rest
626 (f, args) -> Nothing
629toConst :: Term -> Maybe Const
630toConst (Constant c) = Just c
631toConst _ = Nothing
633mapMaybeM :: (Functor m, Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]
634mapMaybeM f [] = return []
635mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
636 maybe rest (:rest) <$> f x
637findForeign :: String -> Exec (Maybe ForeignFun)
638findForeign fn = do est <- getExecState
639 let libs = exec_dynamic_libs est
640 fns <- mapMaybeM getFn libs
641 case fns of
642 [f] -> return (Just f)
643 [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"
644 return Nothing
645 fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
646 show (length fs) ++ " occurrences."
647 return Nothing
648 where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)
650#endif