git.iko.soy/Idris-dev
on 2b258db help sign in
Idris-dev/src/Idris/Core/Execute.hs
656 lines 29 kB history raw
1{-# LANGUAGE PatternGuards, ExistentialQuantification, CPP #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3module Idris.Core.Execute (execute) where
5import Idris.AbsSyntax
6import Idris.AbsSyntaxTree
7import IRTS.Lang(FDesc(..), FType(..))
9import Idris.Primitives(Prim(..), primitives)
11import Idris.Core.TT
12import Idris.Core.Evaluate
13import Idris.Core.CaseTree
15import Idris.Error
17import Debug.Trace
19import Util.DynamicLinker
20import Util.System
22import Control.Applicative hiding (Const)
23import Control.Exception
24import Control.Monad.Trans
25import Control.Monad.Trans.State.Strict
26import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE)
27import Control.Monad hiding (forM)
28import Data.Maybe
29import Data.Bits
30import Data.Traversable (forM)
31import Data.Time.Clock.POSIX (getPOSIXTime)
32import qualified Data.Map as M
34#ifdef IDRIS_FFI
35import Foreign.LibFFI
36import Foreign.C.String
37import Foreign.Marshal.Alloc (free)
38import Foreign.Ptr
39#endif
41import System.IO
43#ifndef IDRIS_FFI
44execute :: Term -> Idris Term
45execute tm = fail "libffi not supported, rebuild Idris with -f FFI"
46#else
47-- else is rest of file
48readMay :: (Read a) => String -> Maybe a
49readMay s = case reads s of
50 [(x, "")] -> Just x
51 _ -> Nothing
53data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show
55data ExecState = ExecState { exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
56 , binderNames :: [Name] -- ^ Used to uniquify binders when converting to TT
57 }
59data ExecVal = EP NameType Name ExecVal
60 | EV Int
61 | EBind Name (Binder ExecVal) (ExecVal -> Exec ExecVal)
62 | EApp ExecVal ExecVal
63 | EType UExp
64 | EUType Universe
65 | EErased
66 | EConstant Const
67 | forall a. EPtr (Ptr a)
68 | EThunk Context ExecEnv Term
69 | EHandle Handle
71instance Show ExecVal where
72 show (EP _ n _) = show n
73 show (EV i) = "!!V" ++ show i ++ "!!"
74 show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"
75 show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
76 show (EType _) = "Type"
77 show (EUType _) = "UType"
78 show EErased = "[__]"
79 show (EConstant c) = show c
80 show (EPtr p) = "<<ptr " ++ show p ++ ">>"
81 show (EThunk _ env tm) = "<<thunk " ++ show env ++ "||||" ++ show tm ++ ">>"
82 show (EHandle h) = "<<handle " ++ show h ++ ">>"
84toTT :: ExecVal -> Exec Term
85toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
86toTT (EV i) = return $ V i
87toTT (EBind n b body) = do n' <- newN n
88 body' <- body $ EP Bound n' EErased
89 b' <- fixBinder b
90 Bind n' b' <$> toTT body'
91 where fixBinder (Lam t) = Lam <$> toTT t
92 fixBinder (Pi i t k) = Pi i <$> toTT t <*> toTT k
93 fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
94 fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2
95 fixBinder (Hole t) = Hole <$> toTT t
96 fixBinder (GHole i t) = GHole i <$> toTT t
97 fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
98 fixBinder (PVar t) = PVar <$> toTT t
99 fixBinder (PVTy t) = PVTy <$> toTT t
100 newN n = do (ExecState hs ns) <- lift get
101 let n' = uniqueName n ns
102 lift (put (ExecState hs (n':ns)))
103 return n'
104toTT (EApp e1 e2) = do e1' <- toTT e1
105 e2' <- toTT e2
106 return $ App e1' e2'
107toTT (EType u) = return $ TType u
108toTT (EUType u) = return $ UType u
109toTT EErased = return Erased
110toTT (EConstant c) = return (Constant c)
111toTT (EThunk ctxt env tm) = do env' <- mapM toBinder env
112 return $ normalise ctxt env' tm
113 where toBinder (n, v) = do v' <- toTT v
114 return (n, Let Erased v')
115toTT (EHandle _) = execFail $ Msg "Can't convert handles back to TT after execution."
116toTT (EPtr ptr) = execFail $ Msg "Can't convert pointers back to TT after execution."
118unApplyV :: ExecVal -> (ExecVal, [ExecVal])
119unApplyV tm = ua [] tm
120 where ua args (EApp f a) = ua (a:args) f
121 ua args t = (t, args)
123mkEApp :: ExecVal -> [ExecVal] -> ExecVal
124mkEApp f [] = f
125mkEApp f (a:args) = mkEApp (EApp f a) args
127initState :: Idris ExecState
128initState = do ist <- getIState
129 return $ ExecState (idris_dynamic_libs ist) []
131type Exec = ExceptT Err (StateT ExecState IO)
133runExec :: Exec a -> ExecState -> IO (Either Err a)
134runExec ex st = fst <$> runStateT (runExceptT ex) st
136getExecState :: Exec ExecState
137getExecState = lift get
139putExecState :: ExecState -> Exec ()
140putExecState = lift . put
142execFail :: Err -> Exec a
143execFail = throwE
145execIO :: IO a -> Exec a
146execIO = lift . lift
149execute :: Term -> Idris Term
150execute tm = do est <- initState
151 ctxt <- getContext
152 res <- lift . lift . flip runExec est $
153 do res <- doExec [] ctxt tm
154 toTT res
155 case res of
156 Left err -> ierror err
157 Right tm' -> return tm'
159ioWrap :: ExecVal -> ExecVal
160ioWrap tm = mkEApp (EP (DCon 0 2 False) (sUN "prim__IO") EErased) [EErased, tm]
162ioUnit :: ExecVal
163ioUnit = ioWrap (EP Ref unitCon EErased)
165type ExecEnv = [(Name, ExecVal)]
167doExec :: ExecEnv -> Context -> Term -> Exec ExecVal
168doExec env ctxt p@(P Ref n ty) | Just v <- lookup n env = return v
169doExec env ctxt p@(P Ref n ty) =
170 do let val = lookupDef n ctxt
171 case val of
172 [Function _ tm] -> doExec env ctxt tm
173 [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def
174 [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later
175 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
176 doExec env ctxt tm
177 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] -> return (EP Ref n EErased)
178 [] -> execFail . Msg $ "Could not find " ++ show n ++ " in definitions."
179 other | length other > 1 -> execFail . Msg $ "Multiple definitions found for " ++ show n
180 | otherwise -> execFail . Msg . take 500 $ "got to " ++ show other ++ " lookup up " ++ show n
181doExec env ctxt p@(P Bound n ty) =
182 case lookup n env of
183 Nothing -> execFail . Msg $ "not found"
184 Just tm -> return tm
185doExec env ctxt (P (DCon a b u) n _) = return (EP (DCon a b u) n EErased)
186doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)
187doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))
188 | otherwise = execFail . Msg $ "env too small"
189doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v
190 doExec ((n, v'):env) ctxt body
191doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
192doExec env ctxt tm@(Bind n b body) = do b' <- forM b (doExec env ctxt)
193 return $
194 EBind n b' (\arg -> doExec ((n, arg):env) ctxt body)
195doExec env ctxt a@(App _ _) =
196 do let (f, args) = unApply a
197 f' <- doExec env ctxt f
198 args' <- case f' of
199 (EP _ d _) | d == delay ->
200 case args of
201 [t,a,tm] -> do t' <- doExec env ctxt t
202 a' <- doExec env ctxt a
203 return [t', a', EThunk ctxt env tm]
204 _ -> mapM (doExec env ctxt) args -- partial applications are fine to evaluate
205 fun' -> do mapM (doExec env ctxt) args
206 execApp env ctxt f' args'
207doExec env ctxt (Constant c) = return (EConstant c)
208doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
209 doExec env ctxt ((x:xs) !! i)
210doExec env ctxt Erased = return EErased
211doExec env ctxt Impossible = fail "Tried to execute an impossible case"
212doExec env ctxt (TType u) = return (EType u)
213doExec env ctxt (UType u) = return (EUType u)
215execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
216execApp env ctxt v [] = return v -- no args is just a constant! can result from function calls
217execApp env ctxt (EP _ f _) (t:a:delayed:rest)
218 | f == force
219 , (_, [_, _, EThunk tmCtxt tmEnv tm]) <- unApplyV delayed =
220 do tm' <- doExec tmEnv tmCtxt tm
221 execApp env ctxt tm' rest
222execApp env ctxt (EP _ fp _) (ty:action:rest)
223 | fp == upio,
224 (prim__IO, [_, v]) <- unApplyV action
225 = execApp env ctxt v rest
227execApp env ctxt (EP _ fp _) args@(_:_:v:k:rest)
228 | fp == piobind,
229 (prim__IO, [_, v']) <- unApplyV v =
230 do res <- execApp env ctxt k [v']
231 execApp env ctxt res rest
232execApp env ctxt con@(EP _ fp _) args@(tp:v:rest)
233 | fp == pioret = execApp env ctxt (mkEApp con [tp, v]) rest
235-- Special cases arising from not having access to the C RTS in the interpreter
236execApp env ctxt f@(EP _ fp _) args@(xs:_:_:_:args')
237 | fp == mkfprim,
238 (ty : fn : w : rest) <- reverse args' =
239 execForeign env ctxt getArity ty fn rest (mkEApp f args)
240 where getArity = case unEList xs of
241 Just as -> length as
242 _ -> 0
244execApp env ctxt c@(EP (DCon _ arity _) n _) args =
245 do let args' = take arity args
246 let restArgs = drop arity args
247 execApp env ctxt (mkEApp c args') restArgs
249execApp env ctxt c@(EP (TCon _ arity) n _) args =
250 do let args' = take arity args
251 let restArgs = drop arity args
252 execApp env ctxt (mkEApp c args') restArgs
254execApp env ctxt f@(EP _ n _) args
255 | Just (res, rest) <- getOp n args = do r <- res
256 execApp env ctxt r rest
257execApp env ctxt f@(EP _ n _) args =
258 do let val = lookupDef n ctxt
259 case val of
260 [Function _ tm] -> fail "should already have been eval'd"
261 [TyDecl nt ty] -> return $ mkEApp f args
262 [Operator tp arity op] ->
263 if length args >= arity
264 then let args' = take arity args in
265 case getOp n args' of
266 Just (res, []) -> do r <- res
267 execApp env ctxt r (drop arity args)
268 _ -> return (mkEApp f args)
269 else return (mkEApp f args)
270 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
271 do rhs <- doExec env ctxt tm
272 execApp env ctxt rhs args
273 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] ->
274 do res <- execCase env ctxt ns sc args
275 return $ fromMaybe (mkEApp f args) res
276 thing -> return $ mkEApp f args
277execApp env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
278 let (f', as) = unApplyV ret
279 execApp env ctxt f' (as ++ args)
280execApp env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp env ctxt f (args1 ++ args2)
281execApp env ctxt f args = return (mkEApp f args)
283execForeign env ctxt arity ty fn xs onfail
284 | Just (FFun "putStr" [(_, str)] _) <- foreignFromTT arity ty fn xs
285 = case str of
286 EConstant (Str arg) -> do execIO (putStr arg)
287 execApp env ctxt ioUnit (drop arity xs)
288 _ -> execFail . Msg $
289 "The argument to putStr should be a constant string, but it was " ++
290 show str ++
291 ". Are all cases covered?"
292 | Just (FFun "putchar" [(_, ch)] _) <- foreignFromTT arity ty fn xs
293 = case ch of
294 EConstant (Ch c) -> do execIO (putChar c)
295 execApp env ctxt ioUnit (drop arity xs)
296 EConstant (I i) -> do execIO (putChar (toEnum i))
297 execApp env ctxt ioUnit (drop arity xs)
298 _ -> execFail . Msg $
299 "The argument to putchar should be a constant character, but it was " ++
300 show str ++
301 ". Are all cases covered?"
302 | Just (FFun "idris_readStr" [_, (_, handle)] _) <- foreignFromTT arity ty fn xs
303 = case handle of
304 EHandle h -> do contents <- execIO $ hGetLine h
305 execApp env ctxt (EConstant (Str (contents ++ "\n"))) (drop arity xs)
306 _ -> execFail . Msg $
307 "The argument to idris_readStr should be a handle, but it was " ++
308 show handle ++
309 ". Are all cases covered?"
310 | Just (FFun "getchar" _ _) <- foreignFromTT arity ty fn xs
311 = do -- The C API returns an Int which Idris library code
312 -- converts; thus, we must make an int here.
313 ch <- execIO $ fmap (ioWrap . EConstant . I . fromEnum) getChar
314 execApp env ctxt ch xs
315 | Just (FFun "idris_time" _ _) <- foreignFromTT arity ty fn xs
316 = do execIO $ fmap (ioWrap . EConstant . I . round) getPOSIXTime
317 | Just (FFun "fileOpen" [(_,fileStr), (_,modeStr)] _) <- foreignFromTT arity ty fn xs
318 = case (fileStr, modeStr) of
319 (EConstant (Str f), EConstant (Str mode)) ->
320 do f <- execIO $
321 catch (do let m = case mode of
322 "r" -> Right ReadMode
323 "w" -> Right WriteMode
324 "a" -> Right AppendMode
325 "rw" -> Right ReadWriteMode
326 "wr" -> Right ReadWriteMode
327 "r+" -> Right ReadWriteMode
328 _ -> Left ("Invalid mode for " ++ f ++ ": " ++ mode)
329 case fmap (openFile f) m of
330 Right h -> do h' <- h
331 hSetBinaryMode h' True
332 return $ Right (ioWrap (EHandle h'), drop arity xs)
333 Left err -> return $ Left err)
334 (\e -> let _ = ( e::SomeException)
335 in return $ Right (ioWrap (EPtr nullPtr), drop arity xs))
336 case f of
337 Left err -> execFail . Msg $ err
338 Right (res, rest) -> execApp env ctxt res rest
339 _ -> execFail . Msg $
340 "The arguments to fileOpen should be constant strings, but they were " ++
341 show fileStr ++ " and " ++ show modeStr ++
342 ". Are all cases covered?"
343 | Just (FFun "fileEOF" [(_,handle)] _) <- foreignFromTT arity ty fn xs
344 = case handle of
345 EHandle h -> do eofp <- execIO $ hIsEOF h
346 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
347 execApp env ctxt res (drop arity xs)
348 _ -> execFail . Msg $
349 "The argument to fileEOF should be a file handle, but it was " ++
350 show handle ++
351 ". Are all cases covered?"
352 | Just (FFun "fileClose" [(_,handle)] _) <- foreignFromTT arity ty fn xs
353 = case handle of
354 EHandle h -> do execIO $ hClose h
355 execApp env ctxt ioUnit (drop arity xs)
356 _ -> execFail . Msg $
357 "The argument to fileClose should be a file handle, but it was " ++
358 show handle ++
359 ". Are all cases covered?"
361 | Just (FFun "isNull" [(_, ptr)] _) <- foreignFromTT arity ty fn xs
362 = case ptr of
363 EPtr p -> let res = ioWrap . EConstant . I $
364 if p == nullPtr then 1 else 0
365 in execApp env ctxt res (drop arity xs)
366 -- Handles will be checked as null pointers sometimes - but if we got a
367 -- real Handle, then it's valid, so just return 1.
368 EHandle h -> let res = ioWrap . EConstant . I $ 0
369 in execApp env ctxt res (drop arity xs)
370 -- A foreign-returned char* has to be tested for NULL sometimes
371 EConstant (Str s) -> let res = ioWrap . EConstant . I $ 0
372 in execApp env ctxt res (drop arity xs)
373 _ -> execFail . Msg $
374 "The argument to isNull should be a pointer or file handle or string, but it was " ++
375 show ptr ++
376 ". Are all cases covered?"
378-- Right now, there's no way to send command-line arguments to the executor,
379-- so just return 0.
380execForeign env ctxt arity ty fn xs onfail
381 | Just (FFun "idris_numArgs" _ _) <- foreignFromTT arity ty fn xs
382 = let res = ioWrap . EConstant . I $ 0
383 in execApp env ctxt res (drop arity xs)
385execForeign env ctxt arity ty fn xs onfail
386 = case foreignFromTT arity ty fn xs of
387 Just ffun@(FFun f argTs retT) | length xs >= arity ->
388 do let (args', xs') = (take arity xs, -- foreign args
389 drop arity xs) -- rest
390 res <- call ffun (map snd argTs)
391 case res of
392 Nothing -> fail $ "Could not call foreign function \"" ++ f ++
393 "\" with args " ++ show (map snd argTs)
394 Just r -> return (mkEApp r xs')
395 _ -> return onfail
398splitArg tm | (_, [_,_,l,r]) <- unApplyV tm -- pair, two implicits
399 = Just (toFDesc l, r)
400splitArg _ = Nothing
402toFDesc tm
403 | (EP _ n _, []) <- unApplyV tm = FCon (deNS n)
404 | (EP _ n _, as) <- unApplyV tm = FApp (deNS n) (map toFDesc as)
405toFDesc _ = FUnknown
407deNS (NS n _) = n
408deNS n = n
410prf = sUN "prim__readFile"
411pwf = sUN "prim__writeFile"
412prs = sUN "prim__readString"
413pws = sUN "prim__writeString"
414pbm = sUN "prim__believe_me"
415pstdin = sUN "prim__stdin"
416pstdout = sUN "prim__stdout"
417mkfprim = sUN "mkForeignPrim"
418pioret = sUN "prim_io_return"
419piobind = sUN "prim_io_bind"
420upio = sUN "unsafePerformPrimIO"
421delay = sUN "Delay"
422force = sUN "Force"
424-- | Look up primitive operations in the global table and transform
425-- them into ExecVal functions
426getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal, [ExecVal])
427getOp fn (_ : _ : x : xs) | fn == pbm = Just (return x, xs)
428getOp fn (_ : EConstant (Str n) : xs)
429 | fn == pws =
430 Just (do execIO $ putStr n
431 return (EConstant (I 0)), xs)
432getOp fn (_:xs)
433 | fn == prs =
434 Just (do line <- execIO getLine
435 return (EConstant (Str line)), xs)
436getOp fn (_ : EP _ fn' _ : EConstant (Str n) : xs)
437 | fn == pwf && fn' == pstdout =
438 Just (do execIO $ putStr n
439 return (EConstant (I 0)), xs)
440getOp fn (_ : EP _ fn' _ : xs)
441 | fn == prf && fn' == pstdin =
442 Just (do line <- execIO getLine
443 return (EConstant (Str line)), xs)
444getOp fn (_ : EHandle h : EConstant (Str n) : xs)
445 | fn == pwf =
446 Just (do execIO $ hPutStr h n
447 return (EConstant (I 0)), xs)
448getOp fn (_ : EHandle h : xs)
449 | fn == prf =
450 Just (do contents <- execIO $ hGetLine h
451 return (EConstant (Str (contents ++ "\n"))), xs)
452getOp fn (_ : arg : xs)
453 | fn == prf =
454 Just $ (execFail (Msg "Can't use prim__readFile on a raw pointer in the executor."), xs)
455getOp n args = do (arity, prim) <- getPrim n primitives
456 if (length args >= arity)
457 then do res <- applyPrim prim (take arity args)
458 Just (res, drop arity args)
459 else Nothing
460 where getPrim :: Name -> [Prim] -> Maybe (Int, [ExecVal] -> Maybe ExecVal)
461 getPrim n [] = Nothing
462 getPrim n ((Prim pn _ arity def _ _) : prims)
463 | n == pn = Just (arity, execPrim def)
464 | otherwise = getPrim n prims
466 execPrim :: ([Const] -> Maybe Const) -> [ExecVal] -> Maybe ExecVal
467 execPrim f args = EConstant <$> (mapM getConst args >>= f)
469 getConst (EConstant c) = Just c
470 getConst _ = Nothing
472 applyPrim :: ([ExecVal] -> Maybe ExecVal) -> [ExecVal] -> Maybe (Exec ExecVal)
473 applyPrim fn args = return <$> fn args
478-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
479-- evaluates them, then begins the checks for matching cases.
480execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
481execCase env ctxt ns sc args =
482 let arity = length ns in
483 if arity <= length args
484 then do let amap = zip ns args
485-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()
486 caseRes <- execCase' env ctxt amap sc
487 case caseRes of
488 Just res -> Just <$> execApp (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)
489 Nothing -> return Nothing
490 else return Nothing
492-- | Take bindings and a case tree and examines them, executing the matching case if possible.
493execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
494execCase' env ctxt amap (UnmatchedCase _) = return Nothing
495execCase' env ctxt amap (STerm tm) =
496 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm
497execCase' env ctxt amap (Case sh n alts) | Just tm <- lookup n amap =
498 case chooseAlt tm alts of
499 Just (newCase, newBindings) ->
500 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
501 execCase' env ctxt amap' newCase
502 Nothing -> return Nothing
503execCase' _ _ _ cse = fail $ "The impossible happened: tried to exec " ++ show cse
505chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
506chooseAlt tm (DefaultCase sc : alts) | ok tm = Just (sc, [])
507 | otherwise = Nothing
508 where -- Default cases should only work on applications of constructors or on constants
509 ok (EApp f x) = ok f
510 ok (EP Bound _ _) = False
511 ok (EP Ref _ _) = False
512 ok _ = True
515chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
516chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm
517 , cn == n = Just (sc, zip ns args)
518 | otherwise = chooseAlt tm alts
519chooseAlt tm (_:alts) = chooseAlt tm alts
520chooseAlt _ [] = Nothing
523data Foreign = FFun String [(FDesc, ExecVal)] FDesc deriving Show
525toFType :: FDesc -> FType
526toFType (FCon c)
527 | c == sUN "C_Str" = FString
528 | c == sUN "C_Float" = FArith ATFloat
529 | c == sUN "C_Ptr" = FPtr
530 | c == sUN "C_MPtr" = FManagedPtr
531 | c == sUN "C_Unit" = FUnit
532toFType (FApp c [_,ity])
533 | c == sUN "C_IntT" = FArith (toAType ity)
534 where toAType (FCon i)
535 | i == sUN "C_IntChar" = ATInt ITChar
536 | i == sUN "C_IntNative" = ATInt ITNative
537 | i == sUN "C_IntBits8" = ATInt (ITFixed IT8)
538 | i == sUN "C_IntBits16" = ATInt (ITFixed IT16)
539 | i == sUN "C_IntBits32" = ATInt (ITFixed IT32)
540 | i == sUN "C_IntBits64" = ATInt (ITFixed IT64)
541 toAType t = error (show t ++ " not defined in toAType")
543toFType (FApp c [_])
544 | c == sUN "C_Any" = FAny
545toFType t = error (show t ++ " not defined in toFType")
547call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
548call (FFun name argTypes retType) args =
549 do fn <- findForeign name
550 maybe (return Nothing)
551 (\f -> Just . ioWrap <$> call' f args (toFType retType)) fn
552 where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal
553 call' (Fun _ h) args (FArith (ATInt ITNative)) = do
554 res <- execIO $ callFFI h retCInt (prepArgs args)
555 return (EConstant (I (fromIntegral res)))
556 call' (Fun _ h) args (FArith (ATInt (ITFixed IT8))) = do
557 res <- execIO $ callFFI h retCChar (prepArgs args)
558 return (EConstant (B8 (fromIntegral res)))
559 call' (Fun _ h) args (FArith (ATInt (ITFixed IT16))) = do
560 res <- execIO $ callFFI h retCWchar (prepArgs args)
561 return (EConstant (B16 (fromIntegral res)))
562 call' (Fun _ h) args (FArith (ATInt (ITFixed IT32))) = do
563 res <- execIO $ callFFI h retCInt (prepArgs args)
564 return (EConstant (B32 (fromIntegral res)))
565 call' (Fun _ h) args (FArith (ATInt (ITFixed IT64))) = do
566 res <- execIO $ callFFI h retCLong (prepArgs args)
567 return (EConstant (B64 (fromIntegral res)))
568 call' (Fun _ h) args (FArith ATFloat) = do
569 res <- execIO $ callFFI h retCDouble (prepArgs args)
570 return (EConstant (Fl (realToFrac res)))
571 call' (Fun _ h) args (FArith (ATInt ITChar)) = do
572 res <- execIO $ callFFI h retCChar (prepArgs args)
573 return (EConstant (Ch (castCCharToChar res)))
574 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
575 if res == nullPtr
576 then return (EPtr res)
577 else do hStr <- execIO $ peekCString res
578 return (EConstant (Str hStr))
580 call' (Fun _ h) args FPtr = EPtr <$> (execIO $ callFFI h (retPtr retVoid) (prepArgs args))
581 call' (Fun _ h) args FUnit = do _ <- execIO $ callFFI h retVoid (prepArgs args)
582 return $ EP Ref unitCon EErased
583 call' _ _ _ = fail "the impossible happened in call' in Execute.hs"
585 prepArgs = map prepArg
586 prepArg (EConstant (I i)) = argCInt (fromIntegral i)
587 prepArg (EConstant (B8 i)) = argCChar (fromIntegral i)
588 prepArg (EConstant (B16 i)) = argCWchar (fromIntegral i)
589 prepArg (EConstant (B32 i)) = argCInt (fromIntegral i)
590 prepArg (EConstant (B64 i)) = argCLong (fromIntegral i)
591 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)
592 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
593 -- Issue #1720 on the issue tracker.
594 -- https://github.com/idris-lang/Idris-dev/issues/1720
595 prepArg (EConstant (Str s)) = argString s
596 prepArg (EPtr p) = argPtr p
597 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined
600foreignFromTT :: Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
601foreignFromTT arity ty (EConstant (Str name)) args
602 = do argFTyVals <- mapM splitArg (take arity args)
603 return $ FFun name argFTyVals (toFDesc ty)
604foreignFromTT arity ty fn args = trace ("failed to construct ffun from " ++ show (ty,fn,args)) Nothing
606getFTy :: ExecVal -> Maybe FType
607getFTy (EApp (EP _ (UN fi) _) (EP _ (UN intTy) _))
608 | fi == txt "FIntT" =
609 case str intTy of
610 "ITNative" -> Just (FArith (ATInt ITNative))
611 "ITChar" -> Just (FArith (ATInt ITChar))
612 "IT8" -> Just (FArith (ATInt (ITFixed IT8)))
613 "IT16" -> Just (FArith (ATInt (ITFixed IT16)))
614 "IT32" -> Just (FArith (ATInt (ITFixed IT32)))
615 "IT64" -> Just (FArith (ATInt (ITFixed IT64)))
616 _ -> Nothing
617getFTy (EP _ (UN t) _) =
618 case str t of
619 "FFloat" -> Just (FArith ATFloat)
620 "FString" -> Just FString
621 "FPtr" -> Just FPtr
622 "FUnit" -> Just FUnit
623 _ -> Nothing
624getFTy _ = Nothing
626unEList :: ExecVal -> Maybe [ExecVal]
627unEList tm = case unApplyV tm of
628 (nil, [_]) -> Just []
629 (cons, ([_, x, xs])) ->
630 do rest <- unEList xs
631 return $ x:rest
632 (f, args) -> Nothing
635toConst :: Term -> Maybe Const
636toConst (Constant c) = Just c
637toConst _ = Nothing
639mapMaybeM :: (Functor m, Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]
640mapMaybeM f [] = return []
641mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
642 maybe rest (:rest) <$> f x
643findForeign :: String -> Exec (Maybe ForeignFun)
644findForeign fn = do est <- getExecState
645 let libs = exec_dynamic_libs est
646 fns <- mapMaybeM getFn libs
647 case fns of
648 [f] -> return (Just f)
649 [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"
650 return Nothing
651 fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
652 show (length fs) ++ " occurrences."
653 return Nothing
654 where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)
656#endif