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