git.iko.soy/Idris-dev
on master help sign in
Convert IO errors into erros in the Idris monad
b5eee09David Christiansen
src/IRTS/Compiler.hs+17−18
compare with master
unifiedsplit
@@ -67,31 +67,30 @@ compile codegen f tm
67 dumpDefun <- getDumpDefun
67 dumpDefun <- getDumpDefun
68 case dumpCases of
68 case dumpCases of
69 Nothing -> return ()
69 Nothing -> return ()
70− Just f -> liftIO $ writeFile f (showCaseTrees tagged)
70+ Just f -> runIO $ writeFile f (showCaseTrees tagged)
71 case dumpDefun of
71 case dumpDefun of
72 Nothing -> return ()
72 Nothing -> return ()
73− Just f -> liftIO $ writeFile f (dumpDefuns defuns)
73+ Just f -> runIO $ writeFile f (dumpDefuns defuns)
74 triple <- targetTriple
74 triple <- targetTriple
75 cpu <- targetCPU
75 cpu <- targetCPU
76 optimize <- optLevel
76 optimize <- optLevel
77 iLOG "Building output"
77 iLOG "Building output"
78 case checked of
78 case checked of
79− OK c -> liftIO $ case codegen of
79+ OK c -> runIO $ case codegen of
80− ViaC ->
80+ ViaC ->
81− codegenC c f outty hdrs
81+ codegenC c f outty hdrs
82− (concatMap mkObj objs)
82+ (concatMap mkObj objs)
83− (concatMap mkLib libs)
83+ (concatMap mkLib libs)
84− (concatMap mkFlag flags ++
84+ (concatMap mkFlag flags ++
85− concatMap incdir impdirs) NONE
85+ concatMap incdir impdirs) NONE
86− ViaJava ->
86+ ViaJava ->
87− codegenJava [] c f hdrs libs outty
87+ codegenJava [] c f hdrs libs outty
88− ViaJavaScript ->
88+ ViaJavaScript ->
89− codegenJavaScript JavaScript c f outty
89+ codegenJavaScript JavaScript c f outty
90− ViaNode ->
90+ ViaNode ->
91− codegenJavaScript Node c f outty
91+ codegenJavaScript Node c f outty
92− ViaLLVM -> codegenLLVM c triple cpu optimize f outty
92+ ViaLLVM -> codegenLLVM c triple cpu optimize f outty
93−
94− Bytecode -> dumpBC c f
93+ Bytecode -> dumpBC c f
95 Error e -> ierror e
94 Error e -> ierror e
96 where checkMVs = do i <- getIState
95 where checkMVs = do i <- getIState
97 case idris_metavars i \\ primDefs of
96 case idris_metavars i \\ primDefs of
src/Idris/AbsSyntax.hs+21−13
@@ -27,6 +27,9 @@ import Data.Word (Word)
27
27
28import Debug.Trace
28import Debug.Trace
29
29
30+import Control.Monad.Error (throwError, catchError)
31+import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)
32+
30import Util.Pretty
33import Util.Pretty
31import Util.System
34import Util.System
32
35
@@ -221,6 +224,11 @@ getIState = get
221putIState :: IState -> Idris ()
224putIState :: IState -> Idris ()
222putIState = put
225putIState = put
223
226
227+-- | A version of liftIO that puts errors into the exception type of the Idris monad
228+runIO :: IO a -> Idris a
229+runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
230+-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
231+
224getName :: Idris Int
232getName :: Idris Int
225getName = do i <- getIState;
233getName = do i <- getIState;
226 let idx = idris_name i;
234 let idx = idris_name i;
@@ -282,25 +290,25 @@ iPrintResult s = do i <- getIState
282 case idris_outputmode i of
290 case idris_outputmode i of
283 RawOutput -> case s of
291 RawOutput -> case s of
284 "" -> return ()
292 "" -> return ()
285− s -> liftIO $ putStrLn s
293+ s -> runIO $ putStrLn s
286 IdeSlave n ->
294 IdeSlave n ->
287 let good = SexpList [SymbolAtom "ok", toSExp s] in
295 let good = SexpList [SymbolAtom "ok", toSExp s] in
288− liftIO $ putStrLn $ convSExp "return" good n
296+ runIO $ putStrLn $ convSExp "return" good n
289
297
290iPrintError :: String -> Idris ()
298iPrintError :: String -> Idris ()
291iPrintError s = do i <- getIState
299iPrintError s = do i <- getIState
292 case idris_outputmode i of
300 case idris_outputmode i of
293 RawOutput -> case s of
301 RawOutput -> case s of
294 "" -> return ()
302 "" -> return ()
295− s -> liftIO $ putStrLn s
303+ s -> runIO $ putStrLn s
296 IdeSlave n ->
304 IdeSlave n ->
297 let good = SexpList [SymbolAtom "error", toSExp s] in
305 let good = SexpList [SymbolAtom "error", toSExp s] in
298− liftIO . putStrLn $ convSExp "return" good n
306+ runIO . putStrLn $ convSExp "return" good n
299
307
300iputStrLn :: String -> Idris ()
308iputStrLn :: String -> Idris ()
301iputStrLn s = do i <- getIState
309iputStrLn s = do i <- getIState
302 case idris_outputmode i of
310 case idris_outputmode i of
303− RawOutput -> liftIO $ putStrLn s
311+ RawOutput -> runIO $ putStrLn s
304 IdeSlave n ->
312 IdeSlave n ->
305 case span (/=':') s of
313 case span (/=':') s of
306 (fn, ':':rest) -> case span isDigit rest of
314 (fn, ':':rest) -> case span isDigit rest of
@@ -308,31 +316,31 @@ iputStrLn s = do i <- getIState
308 ([], msg) -> write
316 ([], msg) -> write
309 (num, ':':msg) -> iWarn (FC fn (read num)) msg
317 (num, ':':msg) -> iWarn (FC fn (read num)) msg
310 _ -> write
318 _ -> write
311− where write = liftIO . putStrLn $ convSExp "write-string" s n
319+ where write = runIO . putStrLn $ convSExp "write-string" s n
312
320
313ideslavePutSExp :: SExpable a => String -> a -> Idris ()
321ideslavePutSExp :: SExpable a => String -> a -> Idris ()
314ideslavePutSExp cmd info = do i <- getIState
322ideslavePutSExp cmd info = do i <- getIState
315 case idris_outputmode i of
323 case idris_outputmode i of
316− IdeSlave n -> liftIO . putStrLn $ convSExp cmd info n
324+ IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
317 _ -> return ()
325 _ -> return ()
318
326
319-- this needs some typing magic and more structured output towards emacs
327-- this needs some typing magic and more structured output towards emacs
320iputGoal :: String -> Idris ()
328iputGoal :: String -> Idris ()
321iputGoal s = do i <- getIState
329iputGoal s = do i <- getIState
322 case idris_outputmode i of
330 case idris_outputmode i of
323− RawOutput -> liftIO $ putStrLn s
331+ RawOutput -> runIO $ putStrLn s
324− IdeSlave n -> liftIO . putStrLn $ convSExp "write-goal" s n
332+ IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" s n
325
333
326isetPrompt :: String -> Idris ()
334isetPrompt :: String -> Idris ()
327isetPrompt p = do i <- getIState
335isetPrompt p = do i <- getIState
328 case idris_outputmode i of
336 case idris_outputmode i of
329− IdeSlave n -> liftIO . putStrLn $ convSExp "set-prompt" p n
337+ IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
330
338
331iWarn :: FC -> String -> Idris ()
339iWarn :: FC -> String -> Idris ()
332iWarn fc err = do i <- getIState
340iWarn fc err = do i <- getIState
333 case idris_outputmode i of
341 case idris_outputmode i of
334− RawOutput -> liftIO $ putStrLn (show fc ++ ":" ++ err)
342+ RawOutput -> runIO $ putStrLn (show fc ++ ":" ++ err)
335− IdeSlave n -> liftIO . putStrLn $ convSExp "warning" (fc_fname fc, fc_line fc, err) n
343+ IdeSlave n -> runIO . putStrLn $ convSExp "warning" (fc_fname fc, fc_line fc, err) n
336
344
337setLogLevel :: Int -> Idris ()
345setLogLevel :: Int -> Idris ()
338setLogLevel l = do i <- getIState
346setLogLevel l = do i <- getIState
@@ -543,7 +551,7 @@ logLvl :: Int -> String -> Idris ()
543logLvl l str = do i <- getIState
551logLvl l str = do i <- getIState
544 let lvl = opt_logLevel (idris_options i)
552 let lvl = opt_logLevel (idris_options i)
545 when (lvl >= l)
553 when (lvl >= l)
546− $ do liftIO (putStrLn str)
554+ $ do runIO (putStrLn str)
547 putIState $ i { idris_log = idris_log i ++ str ++ "\n" }
555 putIState $ i { idris_log = idris_log i ++ str ++ "\n" }
548
556
549cmdOptType :: Opt -> Idris Bool
557cmdOptType :: Opt -> Idris Bool
src/Idris/Chaser.hs+13−13
@@ -71,7 +71,7 @@ getIModTime (LIDR i) = getModificationTime i
71buildTree :: [FilePath] -> -- already guaranteed built
71buildTree :: [FilePath] -> -- already guaranteed built
72 FilePath -> Idris [ModuleTree]
72 FilePath -> Idris [ModuleTree]
73buildTree built fp = idrisCatch (btree [] fp)
73buildTree built fp = idrisCatch (btree [] fp)
74− (\e -> do now <- liftIO $ getCurrentTime
74+ (\e -> do now <- runIO $ getCurrentTime
75 return [MTree (IDR fp) True now []])
75 return [MTree (IDR fp) True now []])
76 where
76 where
77 btree done f =
77 btree done f =
@@ -80,8 +80,8 @@ buildTree built fp = idrisCatch (btree [] fp)
80 iLOG $ "CHASING " ++ show file
80 iLOG $ "CHASING " ++ show file
81 ibcsd <- valIBCSubDir i
81 ibcsd <- valIBCSubDir i
82 ids <- allImportDirs
82 ids <- allImportDirs
83− fp <- liftIO $ findImport ids ibcsd file
83+ fp <- runIO $ findImport ids ibcsd file
84− mt <- liftIO $ getIModTime fp
84+ mt <- runIO $ getIModTime fp
85 if (file `elem` built)
85 if (file `elem` built)
86 then return [MTree fp False mt []]
86 then return [MTree fp False mt []]
87 else if file `elem` done
87 else if file `elem` done
@@ -89,19 +89,19 @@ buildTree built fp = idrisCatch (btree [] fp)
89 else mkChildren fp
89 else mkChildren fp
90
90
91 where mkChildren (LIDR fn) = do ms <- children True fn (f:done)
91 where mkChildren (LIDR fn) = do ms <- children True fn (f:done)
92− mt <- liftIO $ getModificationTime fn
92+ mt <- runIO $ getModificationTime fn
93 return [MTree (LIDR fn) True mt ms]
93 return [MTree (LIDR fn) True mt ms]
94 mkChildren (IDR fn) = do ms <- children False fn (f:done)
94 mkChildren (IDR fn) = do ms <- children False fn (f:done)
95− mt <- liftIO $ getModificationTime fn
95+ mt <- runIO $ getModificationTime fn
96 return [MTree (IDR fn) True mt ms]
96 return [MTree (IDR fn) True mt ms]
97 mkChildren (IBC fn src)
97 mkChildren (IBC fn src)
98− = do srcexist <- liftIO $ doesFileExist (getSrcFile src)
98+ = do srcexist <- runIO $ doesFileExist (getSrcFile src)
99 ms <- if srcexist then
99 ms <- if srcexist then
100 do [MTree _ _ _ ms'] <- mkChildren src
100 do [MTree _ _ _ ms'] <- mkChildren src
101 return ms'
101 return ms'
102 else return []
102 else return []
103− mt <- idrisCatch (liftIO $ getModificationTime fn)
103+ mt <- idrisCatch (runIO $ getModificationTime fn)
104− (\c -> liftIO $ getIModTime src)
104+ (\c -> runIO $ getIModTime src)
105 ok <- checkIBCUpToDate fn src
105 ok <- checkIBCUpToDate fn src
106 return [MTree (IBC fn src) ok mt ms]
106 return [MTree (IBC fn src) ok mt ms]
107
107
@@ -115,18 +115,18 @@ buildTree built fp = idrisCatch (btree [] fp)
115 checkIBCUpToDate fn (LIDR src) = older fn src
115 checkIBCUpToDate fn (LIDR src) = older fn src
116 checkIBCUpToDate fn (IDR src) = older fn src
116 checkIBCUpToDate fn (IDR src) = older fn src
117
117
118− older ibc src = do exist <- liftIO $ doesFileExist src
118+ older ibc src = do exist <- runIO $ doesFileExist src
119 if exist then do
119 if exist then do
120− ibct <- liftIO $ getModificationTime ibc
120+ ibct <- runIO $ getModificationTime ibc
121− srct <- liftIO $ getModificationTime src
121+ srct <- runIO $ getModificationTime src
122 return (srct > ibct)
122 return (srct > ibct)
123 else return False
123 else return False
124
124
125 children :: Bool -> FilePath -> [FilePath] -> Idris [ModuleTree]
125 children :: Bool -> FilePath -> [FilePath] -> Idris [ModuleTree]
126 children lit f done = idrisCatch
126 children lit f done = idrisCatch
127− (do exist <- liftIO $ doesFileExist f
127+ (do exist <- runIO $ doesFileExist f
128 if exist then do
128 if exist then do
129− file_in <- liftIO $ readFile f
129+ file_in <- runIO $ readFile f
130 file <- if lit then tclift $ unlit f file_in else return file_in
130 file <- if lit then tclift $ unlit f file_in else return file_in
131 (_, modules, _) <- parseImports f file
131 (_, modules, _) <- parseImports f file
132 ms <- mapM (btree done) modules
132 ms <- mapM (btree done) modules
src/Idris/IBC.hs+7−7
@@ -62,7 +62,7 @@ initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []
62
62
63loadIBC :: FilePath -> Idris ()
63loadIBC :: FilePath -> Idris ()
64loadIBC fp = do iLOG $ "Loading ibc " ++ fp
64loadIBC fp = do iLOG $ "Loading ibc " ++ fp
65− ibcf <- liftIO $ (decodeFile fp :: IO IBCFile)
65+ ibcf <- runIO $ (decodeFile fp :: IO IBCFile)
66 process ibcf fp
66 process ibcf fp
67
67
68writeIBC :: FilePath -> FilePath -> Idris ()
68writeIBC :: FilePath -> FilePath -> Idris ()
@@ -73,8 +73,8 @@ writeIBC src f
73 (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"
73 (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"
74 [] -> return ()
74 [] -> return ()
75 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })
75 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })
76− idrisCatch (do liftIO $ createDirectoryIfMissing True (dropFileName f)
76+ idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)
77− liftIO $ encodeFile f ibcf
77+ runIO $ encodeFile f ibcf
78 iLOG "Written")
78 iLOG "Written")
79 (\c -> do iLOG $ "Failed " ++ show c)
79 (\c -> do iLOG $ "Failed " ++ show c)
80 return ()
80 return ()
@@ -140,8 +140,8 @@ process i fn
140 | ver i /= ibcVersion = do iLOG "ibc out of date"
140 | ver i /= ibcVersion = do iLOG "ibc out of date"
141 ifail "Incorrect ibc version --- please rebuild"
141 ifail "Incorrect ibc version --- please rebuild"
142 | otherwise =
142 | otherwise =
143− do srcok <- liftIO $ doesFileExist (sourcefile i)
143+ do srcok <- runIO $ doesFileExist (sourcefile i)
144− when srcok $ liftIO $ timestampOlder (sourcefile i) fn
144+ when srcok $ runIO $ timestampOlder (sourcefile i) fn
145 v <- verbose
145 v <- verbose
146 quiet <- getQuiet
146 quiet <- getQuiet
147-- when (v && srcok && not quiet) $ iputStrLn $ "Skipping " ++ sourcefile i
147-- when (v && srcok && not quiet) $ iputStrLn $ "Skipping " ++ sourcefile i
@@ -181,7 +181,7 @@ pImports fs
181 = do mapM_ (\f -> do i <- getIState
181 = do mapM_ (\f -> do i <- getIState
182 ibcsd <- valIBCSubDir i
182 ibcsd <- valIBCSubDir i
183 ids <- allImportDirs
183 ids <- allImportDirs
184− fp <- liftIO $ findImport ids ibcsd f
184+ fp <- runIO $ findImport ids ibcsd f
185 if (f `elem` imported i)
185 if (f `elem` imported i)
186 then iLOG $ "Already read " ++ f
186 then iLOG $ "Already read " ++ f
187 else do putIState (i { imported = f : imported i })
187 else do putIState (i { imported = f : imported i })
@@ -259,7 +259,7 @@ pKeywords k = do i <- getIState
259
259
260pObjs :: [(Codegen, FilePath)] -> Idris ()
260pObjs :: [(Codegen, FilePath)] -> Idris ()
261pObjs os = mapM_ (\ (cg, obj) -> do dirs <- allImportDirs
261pObjs os = mapM_ (\ (cg, obj) -> do dirs <- allImportDirs
262− o <- liftIO $ findInPath dirs obj
262+ o <- runIO $ findInPath dirs obj
263 addObjectFile cg o) os
263 addObjectFile cg o) os
264
264
265pLibs :: [(Codegen, String)] -> Idris ()
265pLibs :: [(Codegen, String)] -> Idris ()
src/Idris/Parser.hs+1−1
@@ -975,7 +975,7 @@ loadSource lidr f
975 = do iLOG ("Reading " ++ f)
975 = do iLOG ("Reading " ++ f)
976 i <- getIState
976 i <- getIState
977 let def_total = default_total i
977 let def_total = default_total i
978− file_in <- liftIO $ readFile f
978+ file_in <- runIO $ readFile f
979 file <- if lidr then tclift $ unlit f file_in else return file_in
979 file <- if lidr then tclift $ unlit f file_in else return file_in
980 (mname, modules, pos) <- parseImports f file
980 (mname, modules, pos) <- parseImports f file
981 i <- getIState
981 i <- getIState
src/Idris/Prover.hs+1−1
@@ -136,7 +136,7 @@ lifte st e = do (v, _) <- elabStep st e
136receiveInput :: ElabState [PDecl] -> Idris (Maybe String)
136receiveInput :: ElabState [PDecl] -> Idris (Maybe String)
137receiveInput e =
137receiveInput e =
138 do i <- getIState
138 do i <- getIState
139− l <- liftIO $ getLine
139+ l <- runIO $ getLine
140 let (sexp, id) = parseMessage l
140 let (sexp, id) = parseMessage l
141 putIState $ i { idris_outputmode = (IdeSlave id) }
141 putIState $ i { idris_outputmode = (IdeSlave id) }
142 case sexpToCommand sexp of
142 case sexpToCommand sexp of
src/Idris/REPL.hs+31−31
@@ -58,7 +58,7 @@ import System.IO
58import Control.Monad
58import Control.Monad
59import Control.Monad.Trans.Error (ErrorT(..))
59import Control.Monad.Trans.Error (ErrorT(..))
60import Control.Monad.Trans.State.Strict ( StateT, execStateT, get, put )
60import Control.Monad.Trans.State.Strict ( StateT, execStateT, get, put )
61−import Control.Monad.Trans ( liftIO, lift )
61+import Control.Monad.Trans ( lift )
62import Data.Maybe
62import Data.Maybe
63import Data.List
63import Data.List
64import Data.Char
64import Data.Char
@@ -111,7 +111,7 @@ ideslaveStart orig mods
111ideslave :: IState -> [FilePath] -> Idris ()
111ideslave :: IState -> [FilePath] -> Idris ()
112ideslave orig mods
112ideslave orig mods
113 = do idrisCatch
113 = do idrisCatch
114− (do l <- liftIO $ getLine
114+ (do l <- runIO $ getLine
115 let (sexp, id) = parseMessage l
115 let (sexp, id) = parseMessage l
116 i <- getIState
116 i <- getIState
117 putIState $ i { idris_outputmode = (IdeSlave id) }
117 putIState $ i { idris_outputmode = (IdeSlave id) }
@@ -134,7 +134,7 @@ ideslave orig mods
134 Just (REPLCompletions str) ->
134 Just (REPLCompletions str) ->
135 do (unused, compls) <- replCompletion (reverse str, "")
135 do (unused, compls) <- replCompletion (reverse str, "")
136 let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]
136 let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]
137− liftIO $ putStrLn $ convSExp "return" good id
137+ runIO $ putStrLn $ convSExp "return" good id
138 Just (LoadFile filename) ->
138 Just (LoadFile filename) ->
139 do clearErr
139 do clearErr
140 putIState (orig { idris_options = idris_options i,
140 putIState (orig { idris_options = idris_options i,
@@ -224,7 +224,7 @@ processInput cmd orig inputs
224 _ -> ""
224 _ -> ""
225 c <- colourise
225 c <- colourise
226 case parseCmd i "(input)" cmd of
226 case parseCmd i "(input)" cmd of
227− Failure err -> do liftIO $ print (fixColour c err)
227+ Failure err -> do runIO $ print (fixColour c err)
228 return (Just inputs)
228 return (Just inputs)
229 Success Reload ->
229 Success Reload ->
230 do putIState $ orig { idris_options = idris_options i
230 do putIState $ orig { idris_options = idris_options i
@@ -275,13 +275,13 @@ edit :: FilePath -> IState -> Idris ()
275edit "" orig = iputStrLn "Nothing to edit"
275edit "" orig = iputStrLn "Nothing to edit"
276edit f orig
276edit f orig
277 = do i <- getIState
277 = do i <- getIState
278− env <- liftIO $ getEnvironment
278+ env <- runIO $ getEnvironment
279 let editor = getEditor env
279 let editor = getEditor env
280 let line = case errLine i of
280 let line = case errLine i of
281 Just l -> " +" ++ show l ++ " "
281 Just l -> " +" ++ show l ++ " "
282 Nothing -> " "
282 Nothing -> " "
283 let cmd = editor ++ line ++ f
283 let cmd = editor ++ line ++ f
284− liftIO $ system cmd
284+ runIO $ system cmd
285 clearErr
285 clearErr
286 putIState $ orig { idris_options = idris_options i
286 putIState $ orig { idris_options = idris_options i
287 , idris_colourTheme = idris_colourTheme i
287 , idris_colourTheme = idris_colourTheme i
@@ -311,7 +311,7 @@ insertScript prf (x : xs) = x : insertScript prf xs
311process :: FilePath -> Command -> Idris ()
311process :: FilePath -> Command -> Idris ()
312process fn Help = iPrintResult displayHelp
312process fn Help = iPrintResult displayHelp
313process fn (ChangeDirectory f)
313process fn (ChangeDirectory f)
314− = do liftIO $ setCurrentDirectory f
314+ = do runIO $ setCurrentDirectory f
315 return ()
315 return ()
316process fn (Eval t)
316process fn (Eval t)
317 = do (tm, ty) <- elabVal toplevel False t
317 = do (tm, ty) <- elabVal toplevel False t
@@ -443,17 +443,17 @@ process fn (RmProof n')
443
443
444process fn' (AddProof prf)
444process fn' (AddProof prf)
445 = do fn <- do
445 = do fn <- do
446− ex <- liftIO $ doesFileExist fn'
446+ ex <- runIO $ doesFileExist fn'
447 let fnExt = fn' <.> "idr"
447 let fnExt = fn' <.> "idr"
448− exExt <- liftIO $ doesFileExist fnExt
448+ exExt <- runIO $ doesFileExist fnExt
449 if ex
449 if ex
450 then return fn'
450 then return fn'
451 else if exExt
451 else if exExt
452 then return fnExt
452 then return fnExt
453 else ifail $ "Neither \""++fn'++"\" nor \""++fnExt++"\" exist"
453 else ifail $ "Neither \""++fn'++"\" nor \""++fnExt++"\" exist"
454 let fb = fn ++ "~"
454 let fb = fn ++ "~"
455− liftIO $ copyFile fn fb -- make a backup in case something goes wrong!
455+ runIO $ copyFile fn fb -- make a backup in case something goes wrong!
456− prog <- liftIO $ readFile fb
456+ prog <- runIO $ readFile fb
457 i <- getIState
457 i <- getIState
458 let proofs = proof_list i
458 let proofs = proof_list i
459 n' <- case prf of
459 n' <- case prf of
@@ -465,7 +465,7 @@ process fn' (AddProof prf)
465 case lookup n proofs of
465 case lookup n proofs of
466 Nothing -> iputStrLn "No proof to add"
466 Nothing -> iputStrLn "No proof to add"
467 Just p -> do let prog' = insertScript (showProof (lit fn) n p) ls
467 Just p -> do let prog' = insertScript (showProof (lit fn) n p) ls
468− liftIO $ writeFile fn (unlines prog')
468+ runIO $ writeFile fn (unlines prog')
469 removeProof n
469 removeProof n
470 iputStrLn $ "Added proof " ++ show n
470 iputStrLn $ "Added proof " ++ show n
471 where ls = (lines prog)
471 where ls = (lines prog)
@@ -513,11 +513,11 @@ process fn Execute = do (m, _) <- elabVal toplevel False
513 (PRef fc (UN "run__IO"))
513 (PRef fc (UN "run__IO"))
514 [pexp $ PRef fc (NS (UN "main") ["Main"])])
514 [pexp $ PRef fc (NS (UN "main") ["Main"])])
515-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))
515-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))
516− (tmpn, tmph) <- liftIO tempfile
516+ (tmpn, tmph) <- runIO tempfile
517− liftIO $ hClose tmph
517+ runIO $ hClose tmph
518 t <- codegen
518 t <- codegen
519 compile t tmpn m
519 compile t tmpn m
520− liftIO $ system tmpn
520+ runIO $ system tmpn
521 return ()
521 return ()
522 where fc = FC "main" 0
522 where fc = FC "main" 0
523process fn (Compile codegen f)
523process fn (Compile codegen f)
@@ -774,10 +774,10 @@ idrisMain opts =
774 [] -> 2
774 [] -> 2
775 xs -> last xs
775 xs -> last xs
776 trpl <- case opt getTriple opts of
776 trpl <- case opt getTriple opts of
777− [] -> liftIO $ getDefaultTargetTriple
777+ [] -> runIO $ getDefaultTargetTriple
778 xs -> return (last xs)
778 xs -> return (last xs)
779 tcpu <- case opt getCPU opts of
779 tcpu <- case opt getCPU opts of
780− [] -> liftIO $ getHostCPUName
780+ [] -> runIO $ getHostCPUName
781 xs -> return (last xs)
781 xs -> return (last xs)
782 let outty = case opt getOutputTy opts of
782 let outty = case opt getOutputTy opts of
783 [] -> Executable
783 [] -> Executable
@@ -788,7 +788,7 @@ idrisMain opts =
788 script <- case opt getExecScript opts of
788 script <- case opt getExecScript opts of
789 [] -> return Nothing
789 [] -> return Nothing
790 x:y:xs -> do iputStrLn "More than one interpreter expression found."
790 x:y:xs -> do iputStrLn "More than one interpreter expression found."
791− liftIO $ exitWith (ExitFailure 1)
791+ runIO $ exitWith (ExitFailure 1)
792 [expr] -> return (Just expr)
792 [expr] -> return (Just expr)
793 when (DefaultTotal `elem` opts) $ do i <- getIState
793 when (DefaultTotal `elem` opts) $ do i <- getIState
794 putIState (i { default_total = True })
794 putIState (i { default_total = True })
@@ -809,11 +809,11 @@ idrisMain opts =
809 -- if we have the --fovm flag, drop into the first order VM testing
809 -- if we have the --fovm flag, drop into the first order VM testing
810 case vm of
810 case vm of
811 [] -> return ()
811 [] -> return ()
812− xs -> liftIO $ mapM_ (fovm cgn outty) xs
812+ xs -> runIO $ mapM_ (fovm cgn outty) xs
813 -- if we have the --bytecode flag, drop into the bytecode assembler
813 -- if we have the --bytecode flag, drop into the bytecode assembler
814 case bcs of
814 case bcs of
815 [] -> return ()
815 [] -> return ()
816− xs -> return () -- liftIO $ mapM_ bcAsm xs
816+ xs -> return () -- runIO $ mapM_ bcAsm xs
817 case ibcsubdir of
817 case ibcsubdir of
818 [] -> setIBCSubDir ""
818 [] -> setIBCSubDir ""
819 (d:_) -> setIBCSubDir d
819 (d:_) -> setIBCSubDir d
@@ -829,7 +829,7 @@ idrisMain opts =
829
829
830 loadInputs inputs
830 loadInputs inputs
831
831
832− liftIO $ hSetBuffering stdout LineBuffering
832+ runIO $ hSetBuffering stdout LineBuffering
833
833
834 ok <- noErrors
834 ok <- noErrors
835 when ok $ case output of
835 when ok $ case output of
@@ -845,7 +845,7 @@ idrisMain opts =
845 when (runrepl && not idesl) $ runInputT (replSettings (Just historyFile)) $ repl ist inputs
845 when (runrepl && not idesl) $ runInputT (replSettings (Just historyFile)) $ repl ist inputs
846 when (idesl) $ ideslaveStart ist inputs
846 when (idesl) $ ideslaveStart ist inputs
847 ok <- noErrors
847 ok <- noErrors
848− when (not ok) $ liftIO (exitWith (ExitFailure 1))
848+ when (not ok) $ runIO (exitWith (ExitFailure 1))
849 where
849 where
850 makeOption (OLogging i) = setLogLevel i
850 makeOption (OLogging i) = setLogLevel i
851 makeOption TypeCase = setTypeCase True
851 makeOption TypeCase = setTypeCase True
@@ -855,7 +855,7 @@ idrisMain opts =
855 makeOption _ = return ()
855 makeOption _ = return ()
856
856
857 addPkgDir :: String -> Idris ()
857 addPkgDir :: String -> Idris ()
858− addPkgDir p = do ddir <- liftIO $ getDataDir
858+ addPkgDir p = do ddir <- runIO $ getDataDir
859 addImportDir (ddir </> p)
859 addImportDir (ddir </> p)
860
860
861execScript :: String -> Idris ()
861execScript :: String -> Idris ()
@@ -863,11 +863,11 @@ execScript expr = do i <- getIState
863 c <- colourise
863 c <- colourise
864 case parseExpr i expr of
864 case parseExpr i expr of
865 Failure err -> do iputStrLn $ show (fixColour c err)
865 Failure err -> do iputStrLn $ show (fixColour c err)
866− liftIO $ exitWith (ExitFailure 1)
866+ runIO $ exitWith (ExitFailure 1)
867 Success term -> do ctxt <- getContext
867 Success term -> do ctxt <- getContext
868 (tm, _) <- elabVal toplevel False term
868 (tm, _) <- elabVal toplevel False term
869 res <- execute tm
869 res <- execute tm
870− liftIO $ exitWith ExitSuccess
870+ runIO $ exitWith ExitSuccess
871
871
872-- | Check if the coloring matches the options and corrects if necessary
872-- | Check if the coloring matches the options and corrects if necessary
873fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
873fixColour :: Bool -> ANSI.Doc -> ANSI.Doc
@@ -876,7 +876,7 @@ fixColour True doc = doc
876
876
877-- | Get the platform-specific, user-specific Idris dir
877-- | Get the platform-specific, user-specific Idris dir
878getIdrisUserDataDir :: Idris FilePath
878getIdrisUserDataDir :: Idris FilePath
879−getIdrisUserDataDir = liftIO $ getAppUserDataDirectory "idris"
879+getIdrisUserDataDir = runIO $ getAppUserDataDirectory "idris"
880
880
881-- | Locate the platform-specific location for the init script
881-- | Locate the platform-specific location for the init script
882getInitScript :: Idris FilePath
882getInitScript :: Idris FilePath
@@ -886,24 +886,24 @@ getInitScript = do idrisDir <- getIdrisUserDataDir
886-- | Run the initialisation script
886-- | Run the initialisation script
887initScript :: Idris ()
887initScript :: Idris ()
888initScript = do script <- getInitScript
888initScript = do script <- getInitScript
889− idrisCatch (do go <- liftIO $ doesFileExist script
889+ idrisCatch (do go <- runIO $ doesFileExist script
890 when go $ do
890 when go $ do
891− h <- liftIO $ openFile script ReadMode
891+ h <- runIO $ openFile script ReadMode
892 runInit h
892 runInit h
893− liftIO $ hClose h)
893+ runIO $ hClose h)
894 (\e -> iPrintError $ "Error reading init file: " ++ show e)
894 (\e -> iPrintError $ "Error reading init file: " ++ show e)
895 where runInit :: Handle -> Idris ()
895 where runInit :: Handle -> Idris ()
896 runInit h = do eof <- lift . lift $ hIsEOF h
896 runInit h = do eof <- lift . lift $ hIsEOF h
897 ist <- getIState
897 ist <- getIState
898 unless eof $ do
898 unless eof $ do
899− line <- liftIO $ hGetLine h
899+ line <- runIO $ hGetLine h
900 script <- getInitScript
900 script <- getInitScript
901 c <- colourise
901 c <- colourise
902 processLine ist line script c
902 processLine ist line script c
903 runInit h
903 runInit h
904 processLine i cmd input clr =
904 processLine i cmd input clr =
905 case parseCmd i input cmd of
905 case parseCmd i input cmd of
906− Failure err -> liftIO $ print (fixColour clr err)
906+ Failure err -> runIO $ print (fixColour clr err)
907 Success Reload -> iPrintError "Init scripts cannot reload the file"
907 Success Reload -> iPrintError "Init scripts cannot reload the file"
908 Success (Load f) -> iPrintError "Init scripts cannot load files"
908 Success (Load f) -> iPrintError "Init scripts cannot load files"
909 Success (ModImport f) -> iPrintError "Init scripts cannot import modules"
909 Success (ModImport f) -> iPrintError "Init scripts cannot import modules"
src/Main.hs+8−9
@@ -10,7 +10,6 @@ import Data.Maybe
10import Data.Version
10import Data.Version
11import Control.Monad.Trans.Error ( ErrorT(..) )
11import Control.Monad.Trans.Error ( ErrorT(..) )
12import Control.Monad.Trans.State.Strict ( execStateT, get, put )
12import Control.Monad.Trans.State.Strict ( execStateT, get, put )
13−import Control.Monad.Trans ( liftIO )
14import Control.Monad ( when )
13import Control.Monad ( when )
15
14
16import Core.CoreParser
15import Core.CoreParser
@@ -45,18 +44,18 @@ main = do xs <- getArgs
45
44
46runIdris :: [Opt] -> Idris ()
45runIdris :: [Opt] -> Idris ()
47runIdris opts = do
46runIdris opts = do
48− when (Ver `elem` opts) $ liftIO showver
47+ when (Ver `elem` opts) $ runIO showver
49− when (Usage `elem` opts) $ liftIO usage
48+ when (Usage `elem` opts) $ runIO usage
50− when (ShowIncs `elem` opts) $ liftIO showIncs
49+ when (ShowIncs `elem` opts) $ runIO showIncs
51− when (ShowLibs `elem` opts) $ liftIO showLibs
50+ when (ShowLibs `elem` opts) $ runIO showLibs
52− when (ShowLibdir `elem` opts) $ liftIO showLibdir
51+ when (ShowLibdir `elem` opts) $ runIO showLibdir
53 case opt getPkgClean opts of
52 case opt getPkgClean opts of
54 [] -> return ()
53 [] -> return ()
55− fs -> do liftIO $ mapM_ cleanPkg fs
54+ fs -> do runIO $ mapM_ cleanPkg fs
56− liftIO $ exitWith ExitSuccess
55+ runIO $ exitWith ExitSuccess
57 case opt getPkg opts of
56 case opt getPkg opts of
58 [] -> idrisMain opts -- in Idris.REPL
57 [] -> idrisMain opts -- in Idris.REPL
59− fs -> liftIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs
58+ fs -> runIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs
60
59
61usage = do putStrLn usagemsg
60usage = do putStrLn usagemsg
62 exitWith ExitSuccess
61 exitWith ExitSuccess