@@ -61,11 +61,13 @@ data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the res
6161 , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness
6262 , exec_implicits :: Ctxt [PArg] -- ^ Necessary info on laziness from idris monad
6363 , exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
64+ , exec_handles :: M.Map Int Handle -- ^ Opened files
65+ , exec_next_handle :: Int -- ^ Ensure opened file key uniqueness
6466 }
6567
6668initState :: Idris ExecState
6769initState = do ist <- getIState
68− return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)
70+ return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist) M.empty 0
6971
7072type Exec = ErrorT String (StateT ExecState IO)
7173
@@ -111,6 +113,11 @@ execute tm = do est <- initState
111113 Left err -> fail err
112114 Right tm' -> return tm'
113115
116+ioWrap :: Term -> Term
117+ioWrap = App (P Ref (UN "prim__IO") Erased)
118+
119+ioUnit :: Term
120+ioUnit = ioWrap (P Ref unitCon Erased)
114121
115122doExec :: Env -> Context -> Term -> Exec Term
116123doExec env ctxt p@(P Ref n ty) =
@@ -130,8 +137,8 @@ doExec env ctxt p@(P Bound n ty) = case (lookupDef n ctxt) of -- bound vars must
130137 [Function ty tm] -> doExec env ctxt tm
131138 [] -> return p
132139 x -> fail ("Internal error lookup up bound var " ++ show n ++ " - found " ++ show x)
133−doExec env ctxt p@(P (DCon a b) n ty) = do { ty' <- doExec env ctxt ty; return (P (DCon a b) n ty') }
134−doExec env ctxt p@(P (TCon a b) n ty) = do { ty' <- doExec env ctxt ty; return (P (TCon a b) n ty') }
140+doExec env ctxt p@(P (DCon _ _) n _) = return p
141+doExec env ctxt p@(P (TCon _ _) n _) = return p
135142doExec env ctxt v@(V i) | i < length env = do let binder = env !! i
136143 case binder of
137144 (_, (Let t v)) -> return v
@@ -155,7 +162,7 @@ execApp :: Env -> Context -> (Term, [Term]) -> Exec Term
155162execApp env ctxt (f, args) = do newF <- doExec env ctxt f
156163 laziness <- getLaziness newF
157164 newArgs <- mapM (doExec env ctxt) args
158− trace (show newF ++ show (zip args laziness)) $ return ()
165+ -- trace (show newF ++ show (zip args laziness)) $ return ()
159166 execApp' env ctxt newF newArgs
160167 where getLaziness (P _ (UN "lazy") _) = return [True]
161168 getLaziness (P _ n _) = do est <- getExecState
@@ -170,6 +177,26 @@ execApp env ctxt (f, args) = do newF <- doExec env ctxt f
170177execApp' :: Env -> Context -> Term -> [Term] -> Exec Term
171178execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls
172179execApp' env ctxt (P _ (UN "unsafePerformIO") _) [ty, action] | (prim__IO, [ty', v]) <- unApply action = return v
180+
181+-- Special cases arising from not having access to the C RTS in the interpreter
182+
183+execApp' env ctxt (P _ (UN "mkForeign") _) [_, fn, Constant (Str arg)]
184+ | Just (FFun "putStr" _ _) <- foreignFromTT fn = execIO (putStr arg) >> return ioUnit
185+execApp' env ctxt (P _ (UN "mkForeign") _) [_, fn, Constant (Str f), Constant (Str mode)]
186+ | Just (FFun "fileOpen" _ _) <- foreignFromTT fn = do trace ("Opening " ++ f ++ " with " ++ mode) $ return ()
187+ m <- case mode of
188+ "r" -> return ReadMode
189+ "w" -> return WriteMode
190+ "a" -> return AppendMode
191+ "rw" -> return ReadWriteMode
192+ "wr" -> return ReadWriteMode
193+ "r+" -> return ReadWriteMode
194+ _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)
195+ h <- execIO $ openFile f m
196+ h' <- handle h
197+ return (ioWrap h')
198+
199+
173200execApp' env ctxt (P _ (UN "mkForeign") _) args =
174201 do res <- stepForeign args
175202 case res of
@@ -191,15 +218,7 @@ execApp' env ctxt (P _ (UN "prim__ltInt") _) [Constant (I i1), Constant (I i2)]
191218execApp' env ctxt (P _ (UN "prim__subInt") _) [Constant (I i1), Constant (I i2)] =
192219 return . Constant . I $ i1 - i2
193220
194−execApp' env ctxt (P _ (UN "prim__readString") _) [ptr] | Just p <- unPtr ptr =
195− do fn <- findForeign "freadStr"
196− case fn of
197− Just (Fun _ freadStr) -> do
198− res <- execIO $ callFFI freadStr retCString [argPtr p]
199− str <- execIO $ peekCString res
200− trace ("Found " ++ str) $ return ()
201− return $ Constant (Str str)
202− Nothing -> fail "Could not load freadStr"
221+execApp' env ctxt (P _ (UN "prim__readString") _) [ptr] = trace "readString" $ undefined
203222
204223execApp' env ctxt f@(P _ n _) args =
205224 do let val = lookupDef n ctxt
@@ -275,6 +294,22 @@ unPtr (App (P _ con _) (Constant (I addr))) | con == ptrCon = Just (unAddr addr)
275294 where unAddr a = nullPtr `plusPtr` a
276295unPtr _ = Nothing
277296
297+-- | Convert a Haskell file handle to a handle term in TT (an int)
298+handle :: Handle -> Exec Term
299+handle h = do est <- getExecState
300+ let i = exec_next_handle est
301+ putExecState $ est { exec_next_handle = exec_next_handle est + 1
302+ , exec_handles = M.insert i h (exec_handles est)
303+ }
304+ return $ Constant (I i)
305+
306+unHandle :: Term -> Exec Handle
307+unHandle (Constant (I i)) =
308+ do est <- getExecState
309+ case M.lookup i (exec_handles est) of
310+ Just h -> return h
311+ Nothing -> execFail "Bad handle ID"
312+unHandle _ = execFail "Not a handle"
278313
279314call :: Foreign -> [Term] -> Exec (Maybe Term)
280315call (FFun name argTypes retType) args =