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