@@ -11,6 +11,8 @@ import Idris.Core.TT
1111import Idris.Core.Evaluate
1212import Idris.Core.CaseTree
1313
14+import Idris.Error
15+
1416import Debug.Trace
1517
1618import Util.DynamicLinker
@@ -113,9 +115,9 @@ initState :: Idris ExecState
113115initState = do ist <- getIState
114116 return $ ExecState (idris_dynamic_libs ist)
115117
116−type Exec = ErrorT String (StateT ExecState IO)
118+type Exec = ErrorT Err (StateT ExecState IO)
117119
118−runExec :: Exec a -> ExecState -> IO (Either String a)
120+runExec :: Exec a -> ExecState -> IO (Either Err a)
119121runExec ex st = fst <$> runStateT (runErrorT ex) st
120122
121123getExecState :: Exec ExecState
@@ -124,7 +126,7 @@ getExecState = lift get
124126putExecState :: ExecState -> Exec ()
125127putExecState = lift . put
126128
127−execFail :: String -> Exec a
129+execFail :: Err -> Exec a
128130execFail = throwError
129131
130132execIO :: IO a -> Exec a
@@ -138,7 +140,7 @@ execute tm = do est <- initState
138140 do res <- doExec [] ctxt tm
139141 toTT res
140142 case res of
141− Left err -> fail err
143+ Left err -> ierror err
142144 Right tm' -> return tm'
143145
144146ioWrap :: ExecVal -> ExecVal
@@ -160,16 +162,16 @@ doExec env ctxt p@(P Ref n ty) =
160162 [CaseOp _ _ _ _ _ (CaseDefs _ ([], STerm tm) _ _)] -> -- nullary fun
161163 doExec env ctxt tm
162164 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] -> return (EP Ref n EErased)
163− [] -> execFail $ "Could not find " ++ show n ++ " in definitions."
165+ [] -> execFail . Msg $ "Could not find " ++ show n ++ " in definitions."
164166 thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined
165167doExec env ctxt p@(P Bound n ty) =
166168 case lookup n env of
167− Nothing -> execFail "not found"
169+ Nothing -> execFail . Msg $ "not found"
168170 Just tm -> return tm
169171doExec env ctxt (P (DCon a b) n _) = return (EP (DCon a b) n EErased)
170172doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)
171173doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))
172− | otherwise = execFail "env too small"
174+ | otherwise = execFail . Msg $ "env too small"
173175doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v
174176 doExec ((n, v'):env) ctxt body
175177doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
@@ -216,71 +218,95 @@ execApp env ctxt con@(EP _ fp _) args@(tp:v:rest)
216218 | fp == pioret = execApp env ctxt (mkEApp con [tp, v]) rest
217219
218220-- Special cases arising from not having access to the C RTS in the interpreter
219−execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str arg):_:rest)
221+execApp env ctxt (EP _ fp _) (_:fn:str:_:rest)
220222 | fp == mkfprim,
221223 Just (FFun "putStr" _ _) <- foreignFromTT fn
222− = do execIO (putStr arg)
223− execApp env ctxt ioUnit rest
224−execApp env ctxt (EP _ fp _) (_:fn:_:EHandle h:_:rest)
224+ = case str of
225+ EConstant (Str arg) -> do execIO (putStr arg)
226+ execApp env ctxt ioUnit rest
227+ _ -> execFail . Msg $
228+ "The argument to putStr should be a constant string, but it was " ++
229+ show str ++
230+ ". Are all cases covered?"
231+execApp env ctxt (EP _ fp _) (_:fn:_:handle:_:rest)
225232 | fp == mkfprim,
226233 Just (FFun "idris_readStr" _ _) <- foreignFromTT fn
227− = do contents <- execIO $ hGetLine h
228− execApp env ctxt (EConstant (Str (contents ++ "\n"))) rest
229−execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)
234+ = case handle of
235+ EHandle h -> do contents <- execIO $ hGetLine h
236+ execApp env ctxt (EConstant (Str (contents ++ "\n"))) rest
237+ _ -> execFail . Msg $
238+ "The argument to idris_readStr should be a handle, but it was " ++
239+ show handle ++
240+ ". Are all cases covered?"
241+execApp env ctxt (EP _ fp _) (_:fn:fileStr:modeStr:rest)
230242 | fp == mkfprim,
231243 Just (FFun "fileOpen" _ _) <- foreignFromTT fn
232− = do f <- execIO $
233− catch (do let m = case mode of
234− "r" -> Right ReadMode
235− "w" -> Right WriteMode
236− "a" -> Right AppendMode
237− "rw" -> Right ReadWriteMode
238− "wr" -> Right ReadWriteMode
239− "r+" -> Right ReadWriteMode
240− _ -> Left ("Invalid mode for " ++ f ++ ": " ++ mode)
241− case fmap (openFile f) m of
242− Right h -> do h' <- h; return $ Right (ioWrap (EHandle h'), tail rest)
243− Left err -> return $ Left err)
244− (\e -> let _ = ( e::SomeException)
245− in return $ Right (ioWrap (EPtr nullPtr), tail rest))
246− case f of
247− Left err -> execFail err
248− Right (res, rest) -> execApp env ctxt res rest
249−
250−execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)
244+ = case (fileStr, modeStr) of
245+ (EConstant (Str f), EConstant (Str mode)) ->
246+ do f <- execIO $
247+ catch (do let m = case mode of
248+ "r" -> Right ReadMode
249+ "w" -> Right WriteMode
250+ "a" -> Right AppendMode
251+ "rw" -> Right ReadWriteMode
252+ "wr" -> Right ReadWriteMode
253+ "r+" -> Right ReadWriteMode
254+ _ -> Left ("Invalid mode for " ++ f ++ ": " ++ mode)
255+ case fmap (openFile f) m of
256+ Right h -> do h' <- h; return $ Right (ioWrap (EHandle h'), tail rest)
257+ Left err -> return $ Left err)
258+ (\e -> let _ = ( e::SomeException)
259+ in return $ Right (ioWrap (EPtr nullPtr), tail rest))
260+ case f of
261+ Left err -> execFail . Msg $ err
262+ Right (res, rest) -> execApp env ctxt res rest
263+ _ -> execFail . Msg $
264+ "The arguments to fileOpen should be constant strings, but they were " ++
265+ show fileStr ++ " and " ++ show modeStr ++
266+ ". Are all cases covered?"
267+
268+execApp env ctxt (EP _ fp _) (_:fn:handle:rest)
251269 | fp == mkfprim,
252270 Just (FFun "fileEOF" _ _) <- foreignFromTT fn
253− = do eofp <- execIO $ hIsEOF h
254− let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
255− execApp env ctxt res (tail rest)
256−
257−execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)
271+ = case handle of
272+ EHandle h -> do eofp <- execIO $ hIsEOF h
273+ let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
274+ execApp env ctxt res (tail rest)
275+ _ -> execFail . Msg $
276+ "The argument to fileEOF should be a file handle, but it was " ++
277+ show handle ++
278+ ". Are all cases covered?"
279+
280+execApp env ctxt (EP _ fp _) (_:fn:handle:rest)
258281 | fp == mkfprim,
259282 Just (FFun "fileClose" _ _) <- foreignFromTT fn
260− = do execIO $ hClose h
261− execApp env ctxt ioUnit (tail rest)
262−
263−execApp env ctxt (EP _ fp _) (_:fn:(EPtr p):rest)
264− | fp == mkfprim,
265− Just (FFun "isNull" _ _) <- foreignFromTT fn
266− = let res = ioWrap . EConstant . I $
267− if p == nullPtr then 1 else 0
268− in execApp env ctxt res (tail rest)
269−
270−-- Handles will be checked as null pointers sometimes - but if we got a
271−-- real Handle, then it's valid, so just return 1.
272−execApp env ctxt (EP _ fp _) (_:fn:(EHandle h):rest)
283+ = case handle of
284+ EHandle h -> do execIO $ hClose h
285+ execApp env ctxt ioUnit (tail rest)
286+ _ -> execFail . Msg $
287+ "The argument to fileClose should be a file handle, but it was " ++
288+ show handle ++
289+ ". Are all cases covered?"
290+
291+execApp env ctxt (EP _ fp _) (_:fn:ptr:rest)
273292 | fp == mkfprim,
274293 Just (FFun "isNull" _ _) <- foreignFromTT fn
275− = let res = ioWrap . EConstant . I $ 0
276− in execApp env ctxt res (tail rest)
294+ = case ptr of
295+ EPtr p -> let res = ioWrap . EConstant . I $
296+ if p == nullPtr then 1 else 0
297+ in execApp env ctxt res (tail rest)
298+ -- Handles will be checked as null pointers sometimes - but if we got a
299+ -- real Handle, then it's valid, so just return 1.
300+ EHandle h -> let res = ioWrap . EConstant . I $ 0
301+ in execApp env ctxt res (tail rest)
302+ -- A foreign-returned char* has to be tested for NULL sometimes
303+ EConstant (Str s) -> let res = ioWrap . EConstant . I $ 0
304+ in execApp env ctxt res (tail rest)
305+ _ -> execFail . Msg $
306+ "The argument to isNull should be a pointer or file handle or string, but it was " ++
307+ show ptr ++
308+ ". Are all cases covered?"
277309
278−-- A foreign-returned char* has to be tested for NULL sometimes
279−execApp env ctxt (EP _ fp _) (_:fn:EConstant (Str s):rest)
280− | fp == mkfprim,
281− Just (FFun "isNull" _ _) <- foreignFromTT fn
282− = let res = ioWrap . EConstant . I $ 0
283− in execApp env ctxt res (tail rest)
284310
285311-- Right now, there's no way to send command-line arguments to the executor,
286312-- so just return 0.
@@ -289,7 +315,6 @@ execApp env ctxt (EP _ fp _) (_:fn:rest)
289315 Just (FFun "idris_numArgs" _ _) <- foreignFromTT fn
290316 = let res = ioWrap . EConstant . I $ 0
291317 in execApp env ctxt res (tail rest)
292−-- Throw away the 'World' argument to the foreign function
293318
294319execApp env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim
295320 = case foreignFromTT fn of