1{-# LANGUAGE PatternGuards, ExistentialQuantification #-}
2module Core.Execute (execute) where
5import Idris.AbsSyntaxTree
6import IRTS.Lang( IntTy(..)
10import Idris.Primitives(Prim(..), primitives)
18import Util.DynamicLinker
21import Control.Applicative hiding (Const)
22import Control.Monad.Trans
23import Control.Monad.Trans.State.Strict
24import Control.Monad.Trans.Error
28import qualified Data.Map as M
31import Foreign.C.String
32import Foreign.Marshal.Alloc (free)
37readMay :: (Read a) => String -> Maybe a
38readMay s = case reads s of
42data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show
44data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the result of evaluating "lazy" or calling lazy funcs
45 , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness
46 , exec_implicits :: Ctxt [PArg] -- ^ Necessary info on laziness from idris monad
47 , exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
50data ExecVal = EP NameType Name ExecVal
52 | EBind Name (Binder ExecVal) (ExecVal -> Exec ExecVal)
53 | EApp ExecVal ExecVal
57 | forall a. EPtr (Ptr a)
61instance Show ExecVal where
62 show (EP _ n _) = show n
63 show (EV i) = "!!V" ++ show i ++ "!!"
64 show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"
65 show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
66 show (EType _) = "Type"
68 show (EConstant c) = show c
69 show (EPtr p) = "<<ptr " ++ show p ++ ">>"
70 show (EThunk i) = "<<thunk " ++ show i ++ ">>"
71 show (EHandle h) = "<<handle " ++ show h ++ ">>"
73toTT :: ExecVal -> Exec Term
74toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
75toTT (EV i) = return $ V i
76toTT (EBind n b body) = do body' <- body $ EP Bound n EErased
78 Bind n b' <$> toTT body'
79 where fixBinder (Lam t) = Lam <$> toTT t
80 fixBinder (Pi t) = Pi <$> toTT t
81 fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2
82 fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2
83 fixBinder (Hole t) = Hole <$> toTT t
84 fixBinder (GHole t) = GHole <$> toTT t
85 fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2
86 fixBinder (PVar t) = PVar <$> toTT t
87 fixBinder (PVTy t) = PVTy <$> toTT t
88toTT (EApp e1 e2) = do e1' <- toTT e1
91toTT (EType u) = return $ TType u
92toTT EErased = return Erased
93toTT (EConstant c) = return (Constant c)
94toTT (EThunk i) = return (P (DCon 0 0) (MN i "THUNK") Erased) --(force i) >>= toTT
95toTT (EHandle _) = return Erased
97unApplyV :: ExecVal -> (ExecVal, [ExecVal])
99 where ua args (EApp f a) = ua (a:args) f
100 ua args t = (t, args)
102mkEApp :: ExecVal -> [ExecVal] -> ExecVal
104mkEApp f (a:args) = mkEApp (EApp f a) args
106initState :: Idris ExecState
107initState = do ist <- getIState
108 return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)
110type Exec = ErrorT String (StateT ExecState IO)
112runExec :: Exec a -> ExecState -> IO (Either String a)
113runExec ex st = fst <$> runStateT (runErrorT ex) st
115getExecState :: Exec ExecState
116getExecState = lift get
118putExecState :: ExecState -> Exec ()
119putExecState = lift . put
121execFail :: String -> Exec a
124execIO :: IO a -> Exec a
127delay :: ExecEnv -> Context -> Term -> Exec ExecVal
129 do st <- getExecState
130 let i = exec_next_thunk st
131 putExecState $ st { exec_thunks = M.insert i (Delayed env ctxt tm) (exec_thunks st)
132 , exec_next_thunk = exec_next_thunk st + 1
136force :: Int -> Exec ExecVal
137force i = do st <- getExecState
138 case M.lookup i (exec_thunks st) of
139 Just (Delayed env ctxt tm) -> do tm' <- doExec env ctxt tm
147 Just (Forced tm) -> return tm
148 Nothing -> execFail "Tried to exec non-existing thunk. This is a bug!"
149 where update :: ExecVal -> Int -> Exec ()
150 update tm i = do est <- getExecState
151 putExecState $ est { exec_thunks = M.insert i (Forced tm) (exec_thunks est) }
153tryForce :: ExecVal -> Exec ExecVal
154tryForce (EThunk i) = force i
155tryForce tm = return tm
157debugThunks :: Exec ()
158debugThunks = do st <- getExecState
159 execIO $ putStrLn (take 4000 (show (exec_thunks st)))
161execute :: Term -> Idris Term
162execute tm = do est <- initState
164 res <- lift $ flip runExec est $ do res <- doExec [] ctxt tm
168 Right tm' -> return tm'
170ioWrap :: ExecVal -> ExecVal
171ioWrap tm = mkEApp (EP (DCon 0 2) (UN "prim__IO") EErased) [EErased, tm]
174ioUnit = ioWrap (EP Ref unitCon EErased)
176type ExecEnv = [(Name, ExecVal)]
178doExec :: ExecEnv -> Context -> Term -> Exec ExecVal
179doExec env ctxt p@(P Ref n ty) | Just v <- lookup n env = return v
180doExec env ctxt p@(P Ref n ty) =
181 do let val = lookupDef n ctxt
183 [Function _ tm] -> doExec env ctxt tm
184 [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def
185 [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later
186 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
188 [CaseOp _ _ _ _ _ ns sc _ _] -> return (EP Ref n EErased)
189 [] -> execFail $ "Could not find " ++ show n ++ " in definitions."
190 thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined
191doExec env ctxt p@(P Bound n ty) =
193 Nothing -> execFail "not found"
195doExec env ctxt (P (DCon a b) n _) = return (EP (DCon a b) n EErased)
196doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)
197doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))
198 | otherwise = execFail "env too small"
199doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v
200 doExec ((n, v'):env) ctxt body
201doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
202doExec env ctxt tm@(Bind n b body) = return $
203 EBind n (fmap (\_->EErased) b)
204 (\arg -> doExec ((n, arg):env) ctxt body)
205doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)
206doExec env ctxt (Constant c) = return (EConstant c)
207doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
208 doExec env ctxt ((x:xs) !! i)
209doExec env ctxt Erased = return EErased
210doExec env ctxt Impossible = fail "Tried to execute an impossible case"
211doExec env ctxt (TType u) = return (EType u)
213execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal
214execApp env ctxt (f, args) = do newF <- doExec env ctxt f
215 laziness <- (++ repeat False) <$> (getLaziness newF)
216 newArgs <- mapM argExec (zip args laziness)
217 execApp' env ctxt newF newArgs
218 where getLaziness (EP _ (UN "lazy") _) = return [False, True]
219 getLaziness (EP _ n _) = do est <- getExecState
220 let argInfo = exec_implicits est
221 case lookupCtxtName n argInfo of
222 [] -> return (repeat False)
223 [ps] -> return $ map lazyarg (snd ps)
224 many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)
225 getLaziness _ = return (repeat False) -- ok due to zip above
226 argExec :: (Term, Bool) -> Exec ExecVal
227 argExec (tm, False) = doExec env ctxt tm
228 argExec (tm, True) = delay env ctxt tm
231execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
232execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
233execApp' env ctxt (EP _ (UN "unsafePerformIO") _) (ty:action:rest) | (prim__IO, [_, v]) <- unApplyV action =
234 execApp' env ctxt v rest
236execApp' env ctxt (EP _ (UN "io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =
237 do v'' <- tryForce v'
238 res <- execApp' env ctxt k [v''] >>= tryForce
239 execApp' env ctxt res rest
240execApp' env ctxt con@(EP _ (UN "io_return") _) args@(tp:v:rest) =
242 execApp' env ctxt (mkEApp con [tp, v']) rest
244-- Special cases arising from not having access to the C RTS in the interpreter
245execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str arg):rest)
246 | Just (FFun "putStr" _ _) <- foreignFromTT fn = do execIO (putStr arg)
247 execApp' env ctxt ioUnit rest
248execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
249 | Just (FFun "fileOpen" _ _) <- foreignFromTT fn = do m <- case mode of
250 "r" -> return ReadMode
251 "w" -> return WriteMode
252 "a" -> return AppendMode
253 "rw" -> return ReadWriteMode
254 "wr" -> return ReadWriteMode
255 "r+" -> return ReadWriteMode
256 _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)
257 h <- execIO $ openFile f m
258 execApp' env ctxt (ioWrap (EHandle h)) rest
260execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)
261 | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do eofp <- execIO $ hIsEOF h
262 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
263 execApp' env ctxt res rest
265execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)
266 | Just (FFun "fileClose" _ _) <- foreignFromTT fn = do execIO $ hClose h
267 execApp' env ctxt ioUnit rest
269execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EPtr p):rest)
270 | Just (FFun "isNull" _ _) <- foreignFromTT fn = let res = ioWrap . EConstant . I $
271 if p == nullPtr then 1 else 0
272 in execApp' env ctxt res rest
274execApp' env ctxt f@(EP _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun f argTs retT) <- foreignFromTT fn
275 , length xs >= length argTs =
276 do res <- stepForeign (ty:fn:take (length argTs) xs)
278 Nothing -> fail $ "Could not call foreign function \"" ++ f ++
279 "\" with args " ++ show (take (length argTs) xs)
280 Just r -> return (mkEApp r (drop (length argTs) xs))
281 | otherwise = return (mkEApp f args)
283execApp' env ctxt c@(EP (DCon _ arity) n _) args =
284 do args' <- mapM tryForce (take arity args)
285 let restArgs = drop arity args
286 execApp' env ctxt (mkEApp c args') restArgs
288execApp' env ctxt c@(EP (TCon _ arity) n _) args =
289 do args' <- mapM tryForce (take arity args)
290 let restArgs = drop arity args
291 execApp' env ctxt (mkEApp c args') restArgs
293execApp' env ctxt f@(EP _ n _) args =
294 do let val = lookupDef n ctxt
296 [Function _ tm] -> fail "should already have been eval'd"
297 [TyDecl nt ty] -> return $ mkEApp f args
298 [Operator tp arity op] ->
299 if length args >= arity
300 then do args' <- mapM tryForce $ take arity args
301 case getOp n args' of
302 Just res -> do r <- res
303 execApp' env ctxt r (drop arity args)
304 Nothing -> return (mkEApp f args)
305 else return (mkEApp f args)
306 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun
307 do rhs <- doExec env ctxt tm
308 execApp' env ctxt rhs args
309 [CaseOp _ _ _ _ _ ns sc _ _] ->
310 do res <- execCase env ctxt ns sc args
311 return $ fromMaybe (mkEApp f args) res
312 thing -> return $ mkEApp f args
313execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
314 let (f', as) = unApplyV ret
315 execApp' env ctxt f' (as ++ args)
316execApp' env ctxt (EThunk i) args = do f <- force i
317 execApp' env ctxt f args
318execApp' env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp' env ctxt f (args1 ++ args2)
319execApp' env ctxt f args = return (mkEApp f args)
321-- | Look up primitive operations in the global table and transform them into ExecVal functions
322getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)
323getOp (UN "prim__believe_me") [_, _, x] = Just (return x)
324getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =
325 Just $ do line <- execIO getLine
326 return (EConstant (Str line))
327getOp (UN "prim__readString") [EHandle h] =
328 Just $ do contents <- execIO $ hGetLine h
329 return (EConstant (Str (contents ++ "\n")))
330getOp n args = getPrim n primitives >>= flip applyPrim args
331 where getPrim :: Name -> [Prim] -> Maybe ([ExecVal] -> Maybe ExecVal)
332 getPrim n [] = Nothing
333 getPrim n ((Prim pn _ arity def _ _) : prims) | n == pn = Just $ execPrim def
334 | otherwise = getPrim n prims
336 execPrim :: ([Const] -> Maybe Const) -> [ExecVal] -> Maybe ExecVal
337 execPrim f args = EConstant <$> (mapM getConst args >>= f)
339 getConst (EConstant c) = Just c
342 applyPrim :: ([ExecVal] -> Maybe ExecVal) -> [ExecVal] -> Maybe (Exec ExecVal)
343 applyPrim fn args = return <$> fn args
348-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
349-- evaluates them, then begins the checks for matching cases.
350execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
351execCase env ctxt ns sc args =
352 let arity = length ns in
353 if arity <= length args
354 then do let amap = zip ns args
355-- trace ("Case " ++ show sc ++ "\n in " ++ show amap ++"\n in env " ++ show env ++ "\n\n" ) $ return ()
356 caseRes <- execCase' env ctxt amap sc
358 Just res -> Just <$> execApp' (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)
359 Nothing -> return Nothing
362-- | Take bindings and a case tree and examines them, executing the matching case if possible.
363execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
364execCase' env ctxt amap (UnmatchedCase _) = return Nothing
365execCase' env ctxt amap (STerm tm) =
366 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm
367execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
368 do tm' <- tryForce tm
369 case chooseAlt tm' alts of
370 Just (newCase, newBindings) ->
371 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
372 execCase' env ctxt amap' newCase
373 Nothing -> return Nothing
375chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
376chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])
377chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
378chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm
379 , cn == n = Just (sc, zip ns args)
380 | otherwise = chooseAlt tm alts
381chooseAlt tm (_:alts) = chooseAlt tm alts
382chooseAlt _ [] = Nothing
387idrisType :: FType -> ExecVal
388idrisType FUnit = EP Ref unitTy EErased
389idrisType ft = EConstant (idr ft)
390 where idr (FInt ty) = intTyToConst ty
393 idr FString = StrType
396data Foreign = FFun String [FType] FType deriving Show
399call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
400call (FFun name argTypes retType) args =
401 do fn <- findForeign name
403 Nothing -> return Nothing
404 Just f -> do res <- call' f args retType
405 return . Just . ioWrap $ res
406 where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal
407 call' (Fun _ h) args (FInt ITNative) = do res <- execIO $ callFFI h retCInt (prepArgs args)
408 return (EConstant (I (fromIntegral res)))
409 call' (Fun _ h) args (FInt IT8) = do res <- execIO $ callFFI h retCChar (prepArgs args)
410 return (EConstant (B8 (fromIntegral res)))
411 call' (Fun _ h) args (FInt IT16) = do res <- execIO $ callFFI h retCWchar (prepArgs args)
412 return (EConstant (B16 (fromIntegral res)))
413 call' (Fun _ h) args (FInt IT32) = do res <- execIO $ callFFI h retCInt (prepArgs args)
414 return (EConstant (B32 (fromIntegral res)))
415 call' (Fun _ h) args (FInt IT64) = do res <- execIO $ callFFI h retCLong (prepArgs args)
416 return (EConstant (B64 (fromIntegral res)))
417 call' (Fun _ h) args FDouble = do res <- execIO $ callFFI h retCDouble (prepArgs args)
418 return (EConstant (Fl (realToFrac res)))
419 call' (Fun _ h) args FChar = do res <- execIO $ callFFI h retCChar (prepArgs args)
420 return (EConstant (Ch (castCCharToChar res)))
421 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
422 hStr <- execIO $ peekCString res
424 return (EConstant (Str hStr))
426 call' (Fun _ h) args FPtr = do res <- execIO $ callFFI h (retPtr retVoid) (prepArgs args)
428 call' (Fun _ h) args FUnit = do res <- execIO $ callFFI h retVoid (prepArgs args)
429 return (EP Ref unitCon EErased)
430-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)
433 prepArgs = map prepArg
434 prepArg (EConstant (I i)) = argCInt (fromIntegral i)
435 prepArg (EConstant (B8 i)) = argCChar (fromIntegral i)
436 prepArg (EConstant (B16 i)) = argCWchar (fromIntegral i)
437 prepArg (EConstant (B32 i)) = argCInt (fromIntegral i)
438 prepArg (EConstant (B64 i)) = argCLong (fromIntegral i)
439 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)
440 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
441 prepArg (EConstant (Str s)) = argString s
442 prepArg (EPtr p) = argPtr p
443 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined
447foreignFromTT :: ExecVal -> Maybe Foreign
448foreignFromTT t = case (unApplyV t) of
449 (_, [(EConstant (Str name)), args, ret]) ->
450 do argTy <- unEList args
451 argFTy <- sequence $ map getFTy argTy
453 return $ FFun name argFTy retFTy
454 _ -> trace "failed to construct ffun" Nothing
456getFTy :: ExecVal -> Maybe FType
457getFTy (EApp (EP _ (UN "FIntT") _) (EP _ (UN intTy) _)) =
459 "ITNative" -> Just $ FInt ITNative
460 "IT8" -> Just $ FInt IT8
461 "IT16" -> Just $ FInt IT16
462 "IT32" -> Just $ FInt IT32
463 "IT64" -> Just $ FInt IT64
465getFTy (EP _ (UN t) _) =
467 "FFloat" -> Just FDouble
468 "FChar" -> Just FChar
469 "FString" -> Just FString
471 "FUnit" -> Just FUnit
475unList :: Term -> Maybe [Term]
476unList tm = case unApply tm of
477 (nil, [_]) -> Just []
478 (cons, ([_, x, xs])) ->
483unEList :: ExecVal -> Maybe [ExecVal]
484unEList tm = case unApplyV tm of
485 (nil, [_]) -> Just []
486 (cons, ([_, x, xs])) ->
487 do rest <- unEList xs
492toConst :: Term -> Maybe Const
493toConst (Constant c) = Just c
496stepForeign :: [ExecVal] -> Exec (Maybe ExecVal)
497stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn
498 f' <- case (call <$> ffun) of
500 Nothing -> return Nothing
502stepForeign _ = fail "Tried to call foreign function that wasn't mkForeign"
504mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
505mapMaybeM f [] = return []
506mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
509 Just x'' -> return (x'':rest)
510 Nothing -> return rest
512findForeign :: String -> Exec (Maybe ForeignFun)
513findForeign fn = do est <- getExecState
514 let libs = exec_dynamic_libs est
515 fns <- mapMaybeM getFn libs
517 [f] -> return (Just f)
518 [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"
520 fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
521 show (length fs) ++ " occurrences."
523 where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list