git.iko.soy/Idris-dev
on 449089d help sign in
Idris-dev/src/Idris/Core/Execute.hs
667 lines 30 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 ns t) = GHole i ns <$> 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 Complete 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 "fileError" [(_,handle)] _) <- foreignFromTT arity ty fn xs
353 = case handle of
354 -- errors handled differently in Haskell than in C, so if
355 -- there's been an error we'll have had an exception already.
356 -- Therefore, assume we're okay.
357 EHandle h -> do let res = ioWrap (EConstant (I 0))
358 execApp env ctxt res (drop arity xs)
359 _ -> execFail . Msg $
360 "The argument to fileError should be a file handle, but it was " ++
361 show handle ++
362 ". Are all cases covered?"
363 | Just (FFun "fileClose" [(_,handle)] _) <- foreignFromTT arity ty fn xs
364 = case handle of
365 EHandle h -> do execIO $ hClose h
366 execApp env ctxt ioUnit (drop arity xs)
367 _ -> execFail . Msg $
368 "The argument to fileClose should be a file handle, but it was " ++
369 show handle ++
370 ". Are all cases covered?"
372 | Just (FFun "isNull" [(_, ptr)] _) <- foreignFromTT arity ty fn xs
373 = case ptr of
374 EPtr p -> let res = ioWrap . EConstant . I $
375 if p == nullPtr then 1 else 0
376 in execApp env ctxt res (drop arity xs)
377 -- Handles will be checked as null pointers sometimes - but if we got a
378 -- real Handle, then it's valid, so just return 1.
379 EHandle h -> let res = ioWrap . EConstant . I $ 0
380 in execApp env ctxt res (drop arity xs)
381 -- A foreign-returned char* has to be tested for NULL sometimes
382 EConstant (Str s) -> let res = ioWrap . EConstant . I $ 0
383 in execApp env ctxt res (drop arity xs)
384 _ -> execFail . Msg $
385 "The argument to isNull should be a pointer or file handle or string, but it was " ++
386 show ptr ++
387 ". Are all cases covered?"
389-- Right now, there's no way to send command-line arguments to the executor,
390-- so just return 0.
391execForeign env ctxt arity ty fn xs onfail
392 | Just (FFun "idris_numArgs" _ _) <- foreignFromTT arity ty fn xs
393 = let res = ioWrap . EConstant . I $ 0
394 in execApp env ctxt res (drop arity xs)
396execForeign env ctxt arity ty fn xs onfail
397 = case foreignFromTT arity ty fn xs of
398 Just ffun@(FFun f argTs retT) | length xs >= arity ->
399 do let (args', xs') = (take arity xs, -- foreign args
400 drop arity xs) -- rest
401 res <- call ffun (map snd argTs)
402 case res of
403 Nothing -> fail $ "Could not call foreign function \"" ++ f ++
404 "\" with args " ++ show (map snd argTs)
405 Just r -> return (mkEApp r xs')
406 _ -> return onfail
409splitArg tm | (_, [_,_,l,r]) <- unApplyV tm -- pair, two implicits
410 = Just (toFDesc l, r)
411splitArg _ = Nothing
413toFDesc tm
414 | (EP _ n _, []) <- unApplyV tm = FCon (deNS n)
415 | (EP _ n _, as) <- unApplyV tm = FApp (deNS n) (map toFDesc as)
416toFDesc _ = FUnknown
418deNS (NS n _) = n
419deNS n = n
421prf = sUN "prim__readFile"
422pwf = sUN "prim__writeFile"
423prs = sUN "prim__readString"
424pws = sUN "prim__writeString"
425pbm = sUN "prim__believe_me"
426pstdin = sUN "prim__stdin"
427pstdout = sUN "prim__stdout"
428mkfprim = sUN "mkForeignPrim"
429pioret = sUN "prim_io_return"
430piobind = sUN "prim_io_bind"
431upio = sUN "unsafePerformPrimIO"
432delay = sUN "Delay"
433force = sUN "Force"
435-- | Look up primitive operations in the global table and transform
436-- them into ExecVal functions
437getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal, [ExecVal])
438getOp fn (_ : _ : x : xs) | fn == pbm = Just (return x, xs)
439getOp fn (_ : EConstant (Str n) : xs)
440 | fn == pws =
441 Just (do execIO $ putStr n
442 return (EConstant (I 0)), xs)
443getOp fn (_:xs)
444 | fn == prs =
445 Just (do line <- execIO getLine
446 return (EConstant (Str line)), xs)
447getOp fn (_ : EP _ fn' _ : EConstant (Str n) : xs)
448 | fn == pwf && fn' == pstdout =
449 Just (do execIO $ putStr n
450 return (EConstant (I 0)), xs)
451getOp fn (_ : EP _ fn' _ : xs)
452 | fn == prf && fn' == pstdin =
453 Just (do line <- execIO getLine
454 return (EConstant (Str line)), xs)
455getOp fn (_ : EHandle h : EConstant (Str n) : xs)
456 | fn == pwf =
457 Just (do execIO $ hPutStr h n
458 return (EConstant (I 0)), xs)
459getOp fn (_ : EHandle h : xs)
460 | fn == prf =
461 Just (do contents <- execIO $ hGetLine h
462 return (EConstant (Str (contents ++ "\n"))), xs)
463getOp fn (_ : arg : xs)
464 | fn == prf =
465 Just $ (execFail (Msg "Can't use prim__readFile on a raw pointer in the executor."), xs)
466getOp n args = do (arity, prim) <- getPrim n primitives
467 if (length args >= arity)
468 then do res <- applyPrim prim (take arity args)
469 Just (res, drop arity args)
470 else Nothing
471 where getPrim :: Name -> [Prim] -> Maybe (Int, [ExecVal] -> Maybe ExecVal)
472 getPrim n [] = Nothing
473 getPrim n ((Prim pn _ arity def _ _) : prims)
474 | n == pn = Just (arity, execPrim def)
475 | otherwise = getPrim n prims
477 execPrim :: ([Const] -> Maybe Const) -> [ExecVal] -> Maybe ExecVal
478 execPrim f args = EConstant <$> (mapM getConst args >>= f)
480 getConst (EConstant c) = Just c
481 getConst _ = Nothing
483 applyPrim :: ([ExecVal] -> Maybe ExecVal) -> [ExecVal] -> Maybe (Exec ExecVal)
484 applyPrim fn args = return <$> fn args
489-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
490-- evaluates them, then begins the checks for matching cases.
491execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
492execCase env ctxt ns sc args =
493 let arity = length ns in
494 if arity <= length args
495 then do let amap = zip ns args
496-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()
497 caseRes <- execCase' env ctxt amap sc
498 case caseRes of
499 Just res -> Just <$> execApp (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)
500 Nothing -> return Nothing
501 else return Nothing
503-- | Take bindings and a case tree and examines them, executing the matching case if possible.
504execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
505execCase' env ctxt amap (UnmatchedCase _) = return Nothing
506execCase' env ctxt amap (STerm tm) =
507 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm
508execCase' env ctxt amap (Case sh n alts) | Just tm <- lookup n amap =
509 case chooseAlt tm alts of
510 Just (newCase, newBindings) ->
511 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
512 execCase' env ctxt amap' newCase
513 Nothing -> return Nothing
514execCase' _ _ _ cse = fail $ "The impossible happened: tried to exec " ++ show cse
516chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
517chooseAlt tm (DefaultCase sc : alts) | ok tm = Just (sc, [])
518 | otherwise = Nothing
519 where -- Default cases should only work on applications of constructors or on constants
520 ok (EApp f x) = ok f
521 ok (EP Bound _ _) = False
522 ok (EP Ref _ _) = False
523 ok _ = True
526chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
527chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm
528 , cn == n = Just (sc, zip ns args)
529 | otherwise = chooseAlt tm alts
530chooseAlt tm (_:alts) = chooseAlt tm alts
531chooseAlt _ [] = Nothing
534data Foreign = FFun String [(FDesc, ExecVal)] FDesc deriving Show
536toFType :: FDesc -> FType
537toFType (FCon c)
538 | c == sUN "C_Str" = FString
539 | c == sUN "C_Float" = FArith ATFloat
540 | c == sUN "C_Ptr" = FPtr
541 | c == sUN "C_MPtr" = FManagedPtr
542 | c == sUN "C_Unit" = FUnit
543toFType (FApp c [_,ity])
544 | c == sUN "C_IntT" = FArith (toAType ity)
545 where toAType (FCon i)
546 | i == sUN "C_IntChar" = ATInt ITChar
547 | i == sUN "C_IntNative" = ATInt ITNative
548 | i == sUN "C_IntBits8" = ATInt (ITFixed IT8)
549 | i == sUN "C_IntBits16" = ATInt (ITFixed IT16)
550 | i == sUN "C_IntBits32" = ATInt (ITFixed IT32)
551 | i == sUN "C_IntBits64" = ATInt (ITFixed IT64)
552 toAType t = error (show t ++ " not defined in toAType")
554toFType (FApp c [_])
555 | c == sUN "C_Any" = FAny
556toFType t = error (show t ++ " not defined in toFType")
558call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
559call (FFun name argTypes retType) args =
560 do fn <- findForeign name
561 maybe (return Nothing)
562 (\f -> Just . ioWrap <$> call' f args (toFType retType)) fn
563 where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal
564 call' (Fun _ h) args (FArith (ATInt ITNative)) = do
565 res <- execIO $ callFFI h retCInt (prepArgs args)
566 return (EConstant (I (fromIntegral res)))
567 call' (Fun _ h) args (FArith (ATInt (ITFixed IT8))) = do
568 res <- execIO $ callFFI h retCChar (prepArgs args)
569 return (EConstant (B8 (fromIntegral res)))
570 call' (Fun _ h) args (FArith (ATInt (ITFixed IT16))) = do
571 res <- execIO $ callFFI h retCWchar (prepArgs args)
572 return (EConstant (B16 (fromIntegral res)))
573 call' (Fun _ h) args (FArith (ATInt (ITFixed IT32))) = do
574 res <- execIO $ callFFI h retCInt (prepArgs args)
575 return (EConstant (B32 (fromIntegral res)))
576 call' (Fun _ h) args (FArith (ATInt (ITFixed IT64))) = do
577 res <- execIO $ callFFI h retCLong (prepArgs args)
578 return (EConstant (B64 (fromIntegral res)))
579 call' (Fun _ h) args (FArith ATFloat) = do
580 res <- execIO $ callFFI h retCDouble (prepArgs args)
581 return (EConstant (Fl (realToFrac res)))
582 call' (Fun _ h) args (FArith (ATInt ITChar)) = do
583 res <- execIO $ callFFI h retCChar (prepArgs args)
584 return (EConstant (Ch (castCCharToChar res)))
585 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
586 if res == nullPtr
587 then return (EPtr res)
588 else do hStr <- execIO $ peekCString res
589 return (EConstant (Str hStr))
591 call' (Fun _ h) args FPtr = EPtr <$> (execIO $ callFFI h (retPtr retVoid) (prepArgs args))
592 call' (Fun _ h) args FUnit = do _ <- execIO $ callFFI h retVoid (prepArgs args)
593 return $ EP Ref unitCon EErased
594 call' _ _ _ = fail "the impossible happened in call' in Execute.hs"
596 prepArgs = map prepArg
597 prepArg (EConstant (I i)) = argCInt (fromIntegral i)
598 prepArg (EConstant (B8 i)) = argCChar (fromIntegral i)
599 prepArg (EConstant (B16 i)) = argCWchar (fromIntegral i)
600 prepArg (EConstant (B32 i)) = argCInt (fromIntegral i)
601 prepArg (EConstant (B64 i)) = argCLong (fromIntegral i)
602 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)
603 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
604 -- Issue #1720 on the issue tracker.
605 -- https://github.com/idris-lang/Idris-dev/issues/1720
606 prepArg (EConstant (Str s)) = argString s
607 prepArg (EPtr p) = argPtr p
608 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined
611foreignFromTT :: Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
612foreignFromTT arity ty (EConstant (Str name)) args
613 = do argFTyVals <- mapM splitArg (take arity args)
614 return $ FFun name argFTyVals (toFDesc ty)
615foreignFromTT arity ty fn args = trace ("failed to construct ffun from " ++ show (ty,fn,args)) Nothing
617getFTy :: ExecVal -> Maybe FType
618getFTy (EApp (EP _ (UN fi) _) (EP _ (UN intTy) _))
619 | fi == txt "FIntT" =
620 case str intTy of
621 "ITNative" -> Just (FArith (ATInt ITNative))
622 "ITChar" -> Just (FArith (ATInt ITChar))
623 "IT8" -> Just (FArith (ATInt (ITFixed IT8)))
624 "IT16" -> Just (FArith (ATInt (ITFixed IT16)))
625 "IT32" -> Just (FArith (ATInt (ITFixed IT32)))
626 "IT64" -> Just (FArith (ATInt (ITFixed IT64)))
627 _ -> Nothing
628getFTy (EP _ (UN t) _) =
629 case str t of
630 "FFloat" -> Just (FArith ATFloat)
631 "FString" -> Just FString
632 "FPtr" -> Just FPtr
633 "FUnit" -> Just FUnit
634 _ -> Nothing
635getFTy _ = Nothing
637unEList :: ExecVal -> Maybe [ExecVal]
638unEList tm = case unApplyV tm of
639 (nil, [_]) -> Just []
640 (cons, ([_, x, xs])) ->
641 do rest <- unEList xs
642 return $ x:rest
643 (f, args) -> Nothing
646toConst :: Term -> Maybe Const
647toConst (Constant c) = Just c
648toConst _ = Nothing
650mapMaybeM :: (Functor m, Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]
651mapMaybeM f [] = return []
652mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
653 maybe rest (:rest) <$> f x
654findForeign :: String -> Exec (Maybe ForeignFun)
655findForeign fn = do est <- getExecState
656 let libs = exec_dynamic_libs est
657 fns <- mapMaybeM getFn libs
658 case fns of
659 [f] -> return (Just f)
660 [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"
661 return Nothing
662 fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
663 show (length fs) ++ " occurrences."
664 return Nothing
665 where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)
667#endif