49e426a · Idris-dev · git.iko.soy

idris.cabal+1−1

@@ -37,7 +37,7 @@ Executable idris

3737

3838 Paths_idris

3939

40− Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,

40+ Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline,

4141 containers, process, transformers, filepath, directory,

4242 binary, bytestring, epic>=0.9.2

4343

src/Core/ProofShell.hs+7−8

@@ -9,7 +9,7 @@ import Core.ShellParser

99import Core.Elaborate

1010

1111import Control.Monad.State

12−import System.Console.Readline

12+import System.Console.Haskeline

1313

1414data ShellState = ShellState

1515 { ctxt :: Context,

@@ -53,22 +53,21 @@ processCommand (Tac e) state

5353 err -> (state, show err)

5454 | otherwise = (state, "No proof in progress")

5555

56−runShell :: ShellState -> IO ShellState

56+runShell :: ShellState -> InputT IO ShellState

5757runShell st = do (prompt, parser) <-

5858 maybe (return ("TT# ", parseCommand))

59− (\st -> do print st

59+ (\st -> do outputStrLn (show st)

6060 return (show (thname st) ++ "# ", parseTactic))

6161 (prf st)

62− x <- readline prompt

62+ x <- getInputLine prompt

6363 cmd <- case x of

6464 Nothing -> return $ Right Quit

65− Just input -> do addHistory input

66− return (parser input)

65+ Just input -> return (parser input)

6766 case cmd of

68− Left err -> do putStrLn (show err)

67+ Left err -> do outputStrLn (show err)

6968 runShell st

7069 Right cmd -> do let (st', r) = processCommand cmd st

71− putStrLn r

70+ outputStrLn r

7271 if (not (exitNow st')) then runShell st'

7372 else return st'

7473

src/Idris/AbsSyntax.hs+5−4

@@ -8,6 +8,7 @@ import Core.Evaluate

88import Core.Elaborate

99import Core.Typecheck

1010

11+import System.Console.Haskeline

1112import Control.Monad.State

1213import Data.List

1314import Data.Char

@@ -78,7 +79,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

7879

7980-- The monad for the main REPL - reading and processing files and updating

8081-- global state (hence the IO inner monad).

81−type Idris a = StateT IState IO a

82+type Idris = StateT IState (InputT IO)

8283

8384getContext :: Idris Context

8485getContext = do i <- get; return (tt_ctxt i)

@@ -175,10 +176,10 @@ solveDeferred n = do i <- get

175176 put (i { idris_metavars = idris_metavars i \\ [n] })

176177

177178iputStrLn :: String -> Idris ()

178−iputStrLn = lift.putStrLn

179+iputStrLn = liftIO . putStrLn

179180

180181iWarn :: FC -> String -> Idris ()

181−iWarn fc err = do lift $ putStrLn (show fc ++ ":" ++ err)

182+iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)

182183

183184setLogLevel :: Int -> Idris ()

184185setLogLevel l = do i <- get

@@ -224,7 +225,7 @@ logLvl :: Int -> String -> Idris ()

224225logLvl l str = do i <- get

225226 let lvl = opt_logLevel (idris_options i)

226227 when (lvl >= l)

227− $ do lift (putStrLn str)

228+ $ do liftIO (putStrLn str)

228229 put (i { idris_log = idris_log i ++ str ++ "\n" } )

229230

230231iLOG :: String -> Idris ()

src/Idris/Compiler.hs+2−2

@@ -23,8 +23,8 @@ compile f = do checkMVs

2323 libs <- getLibs

2424 hdrs <- getHdrs

2525 let incs = map Include hdrs

26− lift $ compileObjWith [Debug] (mkProgram (incs ++ ds)) (f ++ ".o")

27− lift $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f

26+ liftIO $ compileObjWith [Debug] (mkProgram (incs ++ ds)) (f ++ ".o")

27+ liftIO $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f

2828 where checkMVs = do i <- get

2929 case idris_metavars i \\ primDefs of

3030 [] -> return ()

src/Idris/Error.hs+4−8

@@ -1,5 +1,6 @@

11module Idris.Error where

22

3+import Prelude hiding (catch)

34import Idris.AbsSyntax

45import Idris.Delaborate

56

@@ -7,8 +8,9 @@ import Core.TT

78import Core.Typecheck

89import Core.Constraints

910

11+import System.Console.Haskeline

1012import Control.Monad.State

11−import System.IO.Error

13+import System.IO.Error(isUserError, ioeGetErrorString)

1214import Data.Char

1315

1416iucheck :: Idris ()

@@ -25,14 +27,8 @@ report e

2527 | isUserError e = ioeGetErrorString e

2628 | otherwise = show e

2729

28−-- Taken from the library source code - for ghc 6.12/7 compatibility

29−liftCatch :: (m (a,s) -> (e -> m (a,s)) -> m (a,s)) ->

30− StateT s m a -> (e -> StateT s m a) -> StateT s m a

31−liftCatch catchError m h =

32− StateT $ \s -> runStateT m s `catchError` \e -> runStateT (h e) s

33−

3430idrisCatch :: Idris a -> (IOError -> Idris a) -> Idris a

35−idrisCatch op handler = liftCatch catch op handler

31+idrisCatch = catch

3632

3733tclift :: TC a -> Idris a

3834tclift tc = case tc of

src/Idris/IBC.hs+5−5

@@ -46,7 +46,7 @@ initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] []

4646

4747loadIBC :: FilePath -> Idris ()

4848loadIBC fp = do iLOG $ "Loading ibc " ++ fp

49− ibcf <- lift $ (decodeFile fp :: IO IBCFile)

49+ ibcf <- liftIO $ (decodeFile fp :: IO IBCFile)

5050 process ibcf fp

5151

5252writeIBC :: FilePath -> FilePath -> Idris ()

@@ -57,7 +57,7 @@ writeIBC src f

5757 (_:_) -> fail "Can't write ibc when there are unsolved metavariables"

5858 [] -> return ()

5959 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

60− lift $ encodeFile f ibcf

60+ liftIO $ encodeFile f ibcf

6161 iLOG $ "Written"

6262 return ()

6363

@@ -96,7 +96,7 @@ process i fn

9696 | ver i /= ibcVersion = do iLOG "ibc out of date"

9797 fail "Incorrect ibc version"

9898 | otherwise =

99− do lift $ timestampOlder (sourcefile i) fn

99+ do liftIO $ timestampOlder (sourcefile i) fn

100100 pImports (ibc_imports i)

101101 pImps (ibc_implicits i)

102102 pFixes (ibc_fixes i)

@@ -121,8 +121,8 @@ timestampOlder src ibc = do srcok <- doesFileExist src

121121

122122pImports :: [FilePath] -> Idris ()

123123pImports fs

124− = do datadir <- lift $ getDataDir

125− mapM_ (\f -> do fp <- lift $ findImport [".", datadir] f

124+ = do datadir <- liftIO $ getDataDir

125+ mapM_ (\f -> do fp <- liftIO $ findImport [".", datadir] f

126126 i <- getIState

127127 if (f `elem` imported i)

128128 then iLOG $ "Already read " ++ f

src/Idris/Parser.hs+5−5

@@ -53,8 +53,8 @@ lchar = lexeme.char

5353

5454loadModule :: FilePath -> Idris String

5555loadModule f

56− = idrisCatch (do datadir <- lift $ getDataDir

57− fp <- lift $ findImport [".", datadir] f

56+ = idrisCatch (do datadir <- liftIO $ getDataDir

57+ fp <- liftIO $ findImport [".", datadir] f

5858 i <- getIState

5959 if (f `elem` imported i)

6060 then iLOG $ "Already read " ++ f

@@ -78,7 +78,7 @@ loadModule f

7878loadSource :: Bool -> FilePath -> Idris ()

7979loadSource lidr f

8080 = do iLOG ("Reading " ++ f)

81− file_in <- lift $ readFile f

81+ file_in <- liftIO $ readFile f

8282 file <- if lidr then tclift $ unlit f file_in else return file_in

8383 (mname, modules, rest, pos) <- parseImports f file

8484 mapM_ loadModule modules

@@ -1099,8 +1099,8 @@ pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;

10991099 return [PDirective (do addLib lib

11001100 addIBC (IBCLib lib))])

11011101 <|> try (do lchar '%'; reserved "link"; obj <- strlit;

1102− return [PDirective (do datadir <- lift $ getDataDir

1103− o <- lift $ findInPath [".", datadir] obj

1102+ return [PDirective (do datadir <- liftIO $ getDataDir

1103+ o <- liftIO $ findInPath [".", datadir] obj

11041104 addIBC (IBCObj o)

11051105 addObjectFile o)])

11061106 <|> try (do lchar '%'; reserved "include"; hdr <- strlit;

src/Idris/Prover.hs+4−5

@@ -13,7 +13,7 @@ import Idris.ElabTerm

1313import Idris.Parser

1414import Idris.Error

1515

16−import System.Console.Readline

16+import System.Console.Haskeline

1717import Control.Monad.State

1818

1919prover :: Name -> Idris ()

@@ -82,12 +82,11 @@ lifte st e = do (v, _) <- elabStep st e

8282ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Idris (Term, [String])

8383ploop d prompt prf e

8484 = do i <- get

85− when d $ lift $ dumpState i (proof e)

86− x <- lift $ readline (prompt ++ "> ")

85+ when d $ liftIO $ dumpState i (proof e)

86+ x <- lift $ getInputLine (prompt ++ "> ")

8787 (cmd, step) <- case x of

8888 Nothing -> fail "Abandoned"

89− Just input -> do lift $ addHistory input

90− return (parseTac i input, input)

89+ Just input -> do return (parseTac i input, input)

9190 (d, st, done, prf') <- idrisCatch

9291 (case cmd of

9392 Left err -> do iputStrLn (show err)

src/Idris/REPL.hs+12−13

@@ -19,7 +19,7 @@ import Core.ProofShell

1919import Core.TT

2020import Core.Constraints

2121

22−import System.Console.Readline

22+import System.Console.Haskeline

2323import System.FilePath

2424import System.Environment

2525import System.Process

@@ -33,12 +33,11 @@ import Data.Version

3333repl :: IState -> [FilePath] -> Idris ()

3434repl orig mods

3535 = do let prompt = mkPrompt mods

36− x <- lift $ readline (prompt ++ "> ")

36+ x <- lift $ getInputLine (prompt ++ "> ")

3737 case x of

3838 Nothing -> do iputStrLn "Bye bye"

3939 return ()

40− Just input -> do lift $ addHistory input

41− ms <- processInput input orig mods

40+ Just input -> do ms <- processInput input orig mods

4241 case ms of

4342 Just mods -> repl orig mods

4443 Nothing -> return ()

@@ -54,7 +53,7 @@ processInput cmd orig inputs

5453 (f:_) -> f

5554 _ -> ""

5655 case parseCmd i cmd of

57− Left err -> do lift $ print err

56+ Left err -> do liftIO $ print err

5857 return (Just inputs)

5958 Right Reload -> do put (orig { idris_options = idris_options i })

6059 clearErr

@@ -75,13 +74,13 @@ edit :: FilePath -> IState -> Idris ()

7574edit "" orig = iputStrLn "Nothing to edit"

7675edit f orig

7776 = do i <- get

78− env <- lift $ getEnvironment

77+ env <- liftIO $ getEnvironment

7978 let editor = getEditor env

8079 let line = case errLine i of

8180 Just l -> " +" ++ show l ++ " "

8281 Nothing -> " "

8382 let cmd = editor ++ line ++ f

84− lift $ system cmd

83+ liftIO $ system cmd

8584 clearErr

8685 put (orig { idris_options = idris_options i })

8786 loadModule f

@@ -95,13 +94,13 @@ addProof :: FilePath -> IState -> Idris ()

9594addProof "" orig = iputStrLn "Nothing to add to"

9695addProof f orig

9796 = do let fb = f ++ "~"

98− lift $ copyFile f fb -- make a backup in case something goes wrong!

99− prog <- lift $ readFile fb

97+ liftIO $ copyFile f fb -- make a backup in case something goes wrong!

98+ prog <- liftIO $ readFile fb

10099 i <- get

101100 case last_proof i of

102101 Nothing -> iputStrLn "No proof to add"

103102 Just (n, p) -> do let prog' = insertScript (showProof n p) (lines prog)

104− lift $ writeFile f (unlines prog')

103+ liftIO $ writeFile f (unlines prog')

105104 iputStrLn $ "Added proof " ++ show n

106105 put (i { last_proof = Nothing })

107106 -- lift $ removeFile fb -- uncomment when less scared :)

@@ -141,14 +140,14 @@ process (Check t) = do (tm, ty) <- elabVal toplevel False t

141140process Universes = do i <- get

142141 let cs = idris_constraints i

143142-- iputStrLn $ showSep "\n" (map show cs)

144− lift $ print (map fst cs)

143+ liftIO $ print (map fst cs)

145144 let n = length cs

146145 iputStrLn $ "(" ++ show n ++ " constraints)"

147146 case ucheck cs of

148147 Error e -> iputStrLn $ pshow i e

149148 OK _ -> iputStrLn "Universes OK"

150149process (Defn n) = do ctxt <- getContext

151− lift $ print (lookupDef Nothing n ctxt)

150+ liftIO $ print (lookupDef Nothing n ctxt)

152151process (Spec t) = do (tm, ty) <- elabVal toplevel False t

153152 ctxt <- getContext

154153 ist <- get

@@ -165,7 +164,7 @@ process TTShell = do ist <- get

165164 shst' <- lift $ runShell shst

166165 return ()

167166process (Execute f) = do compile f

168− lift $ system ("./" ++ f)

167+ liftIO $ system ("./" ++ f)

169168 return ()

170169process (Compile f) = do compile f

171170process (LogLvl i) = setLogLevel i

src/Main.hs+5−5

@@ -1,6 +1,6 @@

11module Main where

22

3−import System.Console.Readline

3+import System.Console.Haskeline

44import System.IO

55import System.Environment

66import System.Exit

@@ -42,15 +42,15 @@ data Opt = Filename String

4242

4343main = do xs <- getArgs

4444 opts <- parseArgs xs

45− execStateT (runIdris opts) idrisInit

45+ runInputT defaultSettings $ execStateT (runIdris opts) idrisInit

4646

4747runIdris :: [Opt] -> Idris ()

4848runIdris opts =

4949 do let inputs = opt getFile opts

5050 let runrepl = not (NoREPL `elem` opts)

5151 let output = opt getOutput opts

52− when (Ver `elem` opts) $ lift showver

53− when (Usage `elem` opts) $ lift usage

52+ when (Ver `elem` opts) $ liftIO showver

53+ when (Usage `elem` opts) $ liftIO usage

5454 setREPL runrepl

5555 mapM_ makeOption opts

5656 elabPrims

@@ -65,7 +65,7 @@ runIdris opts =

6565 (o:_) -> process (Compile o)

6666 when runrepl $ repl ist inputs

6767 ok <- noErrors

68− when (not ok) $ lift (exitWith (ExitFailure 1))

68+ when (not ok) $ liftIO (exitWith (ExitFailure 1))

6969 where

7070 makeOption (OLogging i) = setLogLevel i

7171 makeOption TypeCase = setTypeCase True