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