git.iko.soy/Idris-dev
on master help sign in
Better laziness behavior, still a bit off with IO
173e357David Christiansen
src/Core/Execute.hs+34−12
compare with master
unifiedsplit
@@ -49,7 +49,17 @@ data ExecVal = EP NameType Name ExecVal
49-- | ETmp Int
49-- | ETmp Int
50 | EThunk Int
50 | EThunk Int
51 | EHandle Int
51 | EHandle Int
52− deriving Show
52+
53+instance Show ExecVal where
54+ show (EP _ n _) = show n
55+ show (EV i) = "!!V" ++ show i ++ "!!"
56+ show (EBind n b body) = "EBind " ++ show b ++ " <<fn>> "
57+ show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"
58+ show (EType _) = "Type"
59+ show EErased = "[__]"
60+ show (EConstant c) = show c
61+ show (EThunk i) = "<<thunk " ++ show i ++ ">>"
62+ show (EHandle i) = "<<handle " ++ show i ++ ">>"
53
63
54toTT :: ExecVal -> Exec Term
64toTT :: ExecVal -> Exec Term
55toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
65toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
@@ -138,13 +148,15 @@ tryForce tm = return tm
138execute :: Term -> Idris Term
148execute :: Term -> Idris Term
139execute tm = do est <- initState
149execute tm = do est <- initState
140 ctxt <- getContext
150 ctxt <- getContext
141− res <- lift $ runExec (doExec [] ctxt tm >>= toTT) est
151+ res <- lift $ flip runExec est $ do res <- doExec [] ctxt tm
152+ trace ("Result: " ++ show res) $ return ()
153+ toTT res
142 case res of
154 case res of
143 Left err -> fail err
155 Left err -> fail err
144 Right tm' -> return tm'
156 Right tm' -> return tm'
145
157
146ioWrap :: ExecVal -> ExecVal
158ioWrap :: ExecVal -> ExecVal
147−ioWrap tm = mkEApp (EP Ref (UN "prim__IO") EErased) [EErased, tm]
159+ioWrap tm = mkEApp (EP (DCon 0 2) (UN "prim__IO") EErased) [EErased, tm]
148
160
149ioUnit :: ExecVal
161ioUnit :: ExecVal
150ioUnit = ioWrap (EP Ref unitCon EErased)
162ioUnit = ioWrap (EP Ref unitCon EErased)
@@ -193,7 +205,6 @@ execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal
193execApp env ctxt (f, args) = do newF <- doExec env ctxt f
205execApp env ctxt (f, args) = do newF <- doExec env ctxt f
194 laziness <- (getLaziness newF) >>= return . (++ repeat False)
206 laziness <- (getLaziness newF) >>= return . (++ repeat False)
195 newArgs <- mapM argExec (zip args laziness)
207 newArgs <- mapM argExec (zip args laziness)
196− trace (take 1000 (show newF) ++ " " ++ take 2000 (show newArgs)) $ return ()
197 execApp' env ctxt newF newArgs
208 execApp' env ctxt newF newArgs
198 where getLaziness (EP _ (UN "lazy") _) = return [True]
209 where getLaziness (EP _ (UN "lazy") _) = return [True]
199 getLaziness (EP _ n _) = do est <- getExecState
210 getLaziness (EP _ n _) = do est <- getExecState
@@ -210,11 +221,16 @@ execApp env ctxt (f, args) = do newF <- doExec env ctxt f
210
221
211execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
222execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
212execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
223execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
213−execApp' env ctxt (EP _ (UN "unsafePerformIO") _) (ty:action:rest) | (prim__IO, [ty', v]) <- unApplyV action =
224+execApp' env ctxt (EP _ (UN "unsafePerformIO") _) (ty:action:rest) | (prim__IO, [_, v]) <- unApplyV action =
214 execApp' env ctxt v rest
225 execApp' env ctxt v rest
215
226
216−-- Special cases arising from not having access to the C RTS in the interpreter
227+execApp' env ctxt (EP _ (UN "io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =
228+ trace ("io_bind " ++ take 1000 (show args)) $
229+ do res <- execApp' env ctxt k [v'] >>= tryForce
230+ trace ("io_bind result was " ++ take 1000 (show res)) $ return ()
231+ execApp' env ctxt res rest
217
232
233+-- Special cases arising from not having access to the C RTS in the interpreter
218execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str arg):rest)
234execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str arg):rest)
219 | Just (FFun "putStr" _ _) <- foreignFromTT fn = do execIO (putStr arg)
235 | Just (FFun "putStr" _ _) <- foreignFromTT fn = do execIO (putStr arg)
220 execApp' env ctxt ioUnit rest
236 execApp' env ctxt ioUnit rest
@@ -235,9 +251,13 @@ execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:fh:rest)
235 | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do h <- unHandle fh
251 | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do h <- unHandle fh
236 eofp <- execIO $ hIsEOF h
252 eofp <- execIO $ hIsEOF h
237 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
253 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
238− trace ("feof was " ++ show eofp) $ return ()
239 execApp' env ctxt res rest
254 execApp' env ctxt res rest
240
255
256+execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:fh:rest)
257+ | Just (FFun "fileClose" _ _) <- foreignFromTT fn = do h <- unHandle fh
258+ execIO $ hClose h
259+ execApp' env ctxt ioUnit rest
260+
241
261
242execApp' env ctxt f@(EP _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun _ argTs retT) <- foreignFromTT fn
262execApp' env ctxt f@(EP _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun _ argTs retT) <- foreignFromTT fn
243 , length xs >= length argTs =
263 , length xs >= length argTs =
@@ -282,8 +302,10 @@ execApp' env ctxt f@(EP _ n _) args =
282 return $ ioWrap (EConstant (Str contents))
302 return $ ioWrap (EConstant (Str contents))
283 getOp _ _ = Nothing
303 getOp _ _ = Nothing
284execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
304execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
285− execApp' env ctxt ret args
305+ let (f', as) = unApplyV ret
286−
306+ execApp' env ctxt f' (as ++ args)
307+execApp' env ctxt (EThunk i) args = do f <- force i
308+ execApp' env ctxt f args
287execApp' env ctxt f args = return (mkEApp f args)
309execApp' env ctxt f args = return (mkEApp f args)
288
310
289
311
@@ -303,7 +325,7 @@ execCase env ctxt ns sc args =
303
325
304-- | Take bindings and a case tree and examines them, executing the matching case if possible.
326-- | Take bindings and a case tree and examines them, executing the matching case if possible.
305execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
327execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
306−execCase' env ctxt amap (UnmatchedCase _) = trace "Unmatched" $ return Nothing
328+execCase' env ctxt amap (UnmatchedCase _) = return Nothing
307execCase' env ctxt amap (STerm tm) =
329execCase' env ctxt amap (STerm tm) =
308 Just <$> doExec (map (\(n, v) -> (n, Let EErased v)) amap ++ env) ctxt tm
330 Just <$> doExec (map (\(n, v) -> (n, Let EErased v)) amap ++ env) ctxt tm
309execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
331execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
@@ -342,7 +364,7 @@ ptrCon = MN 0 "__Ptr"
342
364
343-- | Convert a Haskell pointer to a Ptr term in TT
365-- | Convert a Haskell pointer to a Ptr term in TT
344ptr :: Ptr a -> ExecVal
366ptr :: Ptr a -> ExecVal
345−ptr p = EApp (EP (DCon 1 0) ptrCon EErased) (EConstant (I (addr p)))
367+ptr p = EApp (EP (DCon 0 1) ptrCon EErased) (EConstant (I (addr p)))
346 where addr p = p `minusPtr` nullPtr
368 where addr p = p `minusPtr` nullPtr
347
369
348-- | Convert a Ptr term in TT to a Haskell pointer
370-- | Convert a Ptr term in TT to a Haskell pointer
@@ -377,7 +399,7 @@ call (FFun name argTypes retType) args =
377 case fn of
399 case fn of
378 Nothing -> return Nothing
400 Nothing -> return Nothing
379 Just f -> do res <- call' f args retType
401 Just f -> do res <- call' f args retType
380− return . Just $ mkEApp (EP Ref (UN "prim__IO") EErased) [idrisType retType, res]
402+ return . Just . ioWrap $ res
381 where call' :: ForeignFun -> [ExecVal] -> FTy -> Exec ExecVal
403 where call' :: ForeignFun -> [ExecVal] -> FTy -> Exec ExecVal
382 call' (Fun _ h) args FInt = do res <- execIO $ callFFI h retCInt (prepArgs args)
404 call' (Fun _ h) args FInt = do res <- execIO $ callFFI h retCInt (prepArgs args)
383 return (EConstant (I (fromIntegral res)))
405 return (EConstant (I (fromIntegral res)))