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