@@ -49,7 +49,17 @@ data ExecVal = EP NameType Name ExecVal
4949-- | ETmp Int
5050 | EThunk Int
5151 | 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 ++ ">>"
5363
5464toTT :: ExecVal -> Exec Term
5565toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
@@ -138,13 +148,15 @@ tryForce tm = return tm
138148execute :: Term -> Idris Term
139149execute tm = do est <- initState
140150 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
142154 case res of
143155 Left err -> fail err
144156 Right tm' -> return tm'
145157
146158ioWrap :: 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]
148160
149161ioUnit :: ExecVal
150162ioUnit = ioWrap (EP Ref unitCon EErased)
@@ -193,7 +205,6 @@ execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal
193205execApp env ctxt (f, args) = do newF <- doExec env ctxt f
194206 laziness <- (getLaziness newF) >>= return . (++ repeat False)
195207 newArgs <- mapM argExec (zip args laziness)
196− trace (take 1000 (show newF) ++ " " ++ take 2000 (show newArgs)) $ return ()
197208 execApp' env ctxt newF newArgs
198209 where getLaziness (EP _ (UN "lazy") _) = return [True]
199210 getLaziness (EP _ n _) = do est <- getExecState
@@ -210,11 +221,16 @@ execApp env ctxt (f, args) = do newF <- doExec env ctxt f
210221
211222execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
212223execApp' 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 =
214225 execApp' env ctxt v rest
215226
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
217232
233+-- Special cases arising from not having access to the C RTS in the interpreter
218234execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str arg):rest)
219235 | Just (FFun "putStr" _ _) <- foreignFromTT fn = do execIO (putStr arg)
220236 execApp' env ctxt ioUnit rest
@@ -235,9 +251,13 @@ execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:fh:rest)
235251 | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do h <- unHandle fh
236252 eofp <- execIO $ hIsEOF h
237253 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
238− trace ("feof was " ++ show eofp) $ return ()
239254 execApp' env ctxt res rest
240255
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+
241261
242262execApp' env ctxt f@(EP _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun _ argTs retT) <- foreignFromTT fn
243263 , length xs >= length argTs =
@@ -282,8 +302,10 @@ execApp' env ctxt f@(EP _ n _) args =
282302 return $ ioWrap (EConstant (Str contents))
283303 getOp _ _ = Nothing
284304execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
285− execApp' env ctxt ret args
286−
305+ let (f', as) = unApplyV ret
306+ execApp' env ctxt f' (as ++ args)
307+execApp' env ctxt (EThunk i) args = do f <- force i
308+ execApp' env ctxt f args
287309execApp' env ctxt f args = return (mkEApp f args)
288310
289311
@@ -303,7 +325,7 @@ execCase env ctxt ns sc args =
303325
304326-- | Take bindings and a case tree and examines them, executing the matching case if possible.
305327execCase' :: 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
307329execCase' env ctxt amap (STerm tm) =
308330 Just <$> doExec (map (\(n, v) -> (n, Let EErased v)) amap ++ env) ctxt tm
309331execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
@@ -342,7 +364,7 @@ ptrCon = MN 0 "__Ptr"
342364
343365-- | Convert a Haskell pointer to a Ptr term in TT
344366ptr :: 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)))
346368 where addr p = p `minusPtr` nullPtr
347369
348370-- | Convert a Ptr term in TT to a Haskell pointer
@@ -377,7 +399,7 @@ call (FFun name argTypes retType) args =
377399 case fn of
378400 Nothing -> return Nothing
379401 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
381403 where call' :: ForeignFun -> [ExecVal] -> FTy -> Exec ExecVal
382404 call' (Fun _ h) args FInt = do res <- execIO $ callFFI h retCInt (prepArgs args)
383405 return (EConstant (I (fromIntegral res)))