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

git.iko.soy/Idris-dev

on master help sign in

Switch from readline to haskeline

49e426aMathnerd31415 years ago

idris.cabal+1−1

compare with master

unifiedsplit

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

38 Paths_idris

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

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

41 containers, process, transformers, filepath, directory,

42 binary, bytestring, epic>=0.9.2

src/Core/ProofShell.hs+7−8

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

9import Core.Elaborate

11import Control.Monad.State

12−import System.Console.Readline

12+import System.Console.Haskeline

14data ShellState = ShellState

15 { ctxt :: Context,

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

53 err -> (state, show err)

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

56−runShell :: ShellState -> IO ShellState

56+runShell :: ShellState -> InputT IO ShellState

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

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

59− (\st -> do print st

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

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

61 (prf st)

62− x <- readline prompt

62+ x <- getInputLine prompt

63 cmd <- case x of

64 Nothing -> return $ Right Quit

65− Just input -> do addHistory input

66− return (parser input)

65+ Just input -> return (parser input)

67 case cmd of

66 case cmd of

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

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

69 runShell st

68 runShell st

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

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

71− putStrLn r

70+ outputStrLn r

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

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

73 else return st'

72 else return st'

src/Idris/AbsSyntax.hs+5−4

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

8import Core.Elaborate

9import Core.Typecheck

11+import System.Console.Haskeline

11import Control.Monad.State

12import Control.Monad.State

12import Data.List

13import Data.List

13import Data.Char

14import Data.Char

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

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

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

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

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

81−type Idris a = StateT IState IO a

82+type Idris = StateT IState (InputT IO)

83getContext :: Idris Context

84getContext :: Idris Context

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

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

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

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

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

176

177

177iputStrLn :: String -> Idris ()

178iputStrLn :: String -> Idris ()

178−iputStrLn = lift.putStrLn

179+iputStrLn = liftIO . putStrLn

179

180

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

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

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

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

182

183

183setLogLevel :: Int -> Idris ()

184setLogLevel :: Int -> Idris ()

184setLogLevel l = do i <- get

185setLogLevel l = do i <- get

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

224logLvl l str = do i <- get

225logLvl l str = do i <- get

225 let lvl = opt_logLevel (idris_options i)

226 let lvl = opt_logLevel (idris_options i)

226 when (lvl >= l)

227 when (lvl >= l)

227− $ do lift (putStrLn str)

228+ $ do liftIO (putStrLn str)

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

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

229

230

230iLOG :: String -> Idris ()

231iLOG :: String -> Idris ()

src/Idris/Compiler.hs+2−2

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

23 libs <- getLibs

24 hdrs <- getHdrs

25 let incs = map Include hdrs

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

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

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

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

28 where checkMVs = do i <- get

29 case idris_metavars i \\ primDefs of

30 [] -> return ()

src/Idris/Error.hs+4−8

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

1module Idris.Error where

3+import Prelude hiding (catch)

3import Idris.AbsSyntax

4import Idris.AbsSyntax

4import Idris.Delaborate

5import Idris.Delaborate

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

7import Core.Typecheck

8import Core.Typecheck

8import Core.Constraints

9import Core.Constraints

11+import System.Console.Haskeline

10import Control.Monad.State

12import Control.Monad.State

11−import System.IO.Error

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

12import Data.Char

14import Data.Char

14iucheck :: Idris ()

16iucheck :: Idris ()

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

25 | isUserError e = ioeGetErrorString e

27 | isUserError e = ioeGetErrorString e

26 | otherwise = show e

28 | otherwise = show e

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−

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

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

35−idrisCatch op handler = liftCatch catch op handler

31+idrisCatch = catch

37tclift :: TC a -> Idris a

33tclift :: TC a -> Idris a

38tclift tc = case tc of

34tclift tc = case tc of

src/Idris/IBC.hs+5−5

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

47loadIBC :: FilePath -> Idris ()

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

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

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

50 process ibcf fp

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

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

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

58 [] -> return ()

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

60− lift $ encodeFile f ibcf

60+ liftIO $ encodeFile f ibcf

61 iLOG $ "Written"

62 return ()

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

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

97 fail "Incorrect ibc version"

98 | otherwise =

99− do lift $ timestampOlder (sourcefile i) fn

99+ do liftIO $ timestampOlder (sourcefile i) fn

100 pImports (ibc_imports i)

101 pImps (ibc_implicits i)

102 pFixes (ibc_fixes i)

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

121

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

123pImports fs

124− = do datadir <- lift $ getDataDir

124+ = do datadir <- liftIO $ getDataDir

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

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

126 i <- getIState

127 if (f `elem` imported i)

128 then iLOG $ "Already read " ++ f

src/Idris/Parser.hs+5−5

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

54loadModule :: FilePath -> Idris String

55loadModule f

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

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

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

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

58 i <- getIState

59 if (f `elem` imported i)

60 then iLOG $ "Already read " ++ f

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

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

79loadSource lidr f

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

81− file_in <- lift $ readFile f

81+ file_in <- liftIO $ readFile f

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

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

84 mapM_ loadModule modules

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

1099 return [PDirective (do addLib lib

1100 addIBC (IBCLib lib))])

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

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

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

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

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

1104 addIBC (IBCObj o)

1105 addObjectFile o)])

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

src/Idris/Prover.hs+4−5

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

13import Idris.Parser

14import Idris.Error

16−import System.Console.Readline

16+import System.Console.Haskeline

17import Control.Monad.State

19prover :: Name -> Idris ()

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

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

83ploop d prompt prf e

84 = do i <- get

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

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

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

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

87 (cmd, step) <- case x of

88 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)

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

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

92 (case cmd of

91 (case cmd of

93 Left err -> do iputStrLn (show err)

92 Left err -> do iputStrLn (show err)

src/Idris/REPL.hs+12−13

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

19import Core.TT

20import Core.Constraints

22−import System.Console.Readline

22+import System.Console.Haskeline

23import System.FilePath

24import System.Environment

25import System.Process

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

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

34repl orig mods

35 = do let prompt = mkPrompt mods

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

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

37 case x of

38 Nothing -> do iputStrLn "Bye bye"

39 return ()

40− Just input -> do lift $ addHistory input

41− ms <- processInput input orig mods

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

42 case ms of

41 case ms of

43 Just mods -> repl orig mods

42 Just mods -> repl orig mods

44 Nothing -> return ()

43 Nothing -> return ()

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

54 (f:_) -> f

53 (f:_) -> f

55 _ -> ""

54 _ -> ""

56 case parseCmd i cmd of

55 case parseCmd i cmd of

57− Left err -> do lift $ print err

56+ Left err -> do liftIO $ print err

58 return (Just inputs)

57 return (Just inputs)

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

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

60 clearErr

59 clearErr

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

75edit "" orig = iputStrLn "Nothing to edit"

74edit "" orig = iputStrLn "Nothing to edit"

76edit f orig

75edit f orig

77 = do i <- get

76 = do i <- get

78− env <- lift $ getEnvironment

77+ env <- liftIO $ getEnvironment

79 let editor = getEditor env

78 let editor = getEditor env

80 let line = case errLine i of

79 let line = case errLine i of

81 Just l -> " +" ++ show l ++ " "

80 Just l -> " +" ++ show l ++ " "

82 Nothing -> " "

81 Nothing -> " "

83 let cmd = editor ++ line ++ f

82 let cmd = editor ++ line ++ f

84− lift $ system cmd

83+ liftIO $ system cmd

85 clearErr

84 clearErr

86 put (orig { idris_options = idris_options i })

85 put (orig { idris_options = idris_options i })

87 loadModule f

86 loadModule f

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

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

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

96addProof f orig

95addProof f orig

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

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

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

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

99− prog <- lift $ readFile fb

98+ prog <- liftIO $ readFile fb

100 i <- get

99 i <- get

101 case last_proof i of

100 case last_proof i of

102 Nothing -> iputStrLn "No proof to add"

101 Nothing -> iputStrLn "No proof to add"

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

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

104− lift $ writeFile f (unlines prog')

103+ liftIO $ writeFile f (unlines prog')

105 iputStrLn $ "Added proof " ++ show n

104 iputStrLn $ "Added proof " ++ show n

106 put (i { last_proof = Nothing })

105 put (i { last_proof = Nothing })

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

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

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

141process Universes = do i <- get

140process Universes = do i <- get

142 let cs = idris_constraints i

141 let cs = idris_constraints i

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

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

144− lift $ print (map fst cs)

143+ liftIO $ print (map fst cs)

145 let n = length cs

144 let n = length cs

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

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

147 case ucheck cs of

146 case ucheck cs of

148 Error e -> iputStrLn $ pshow i e

147 Error e -> iputStrLn $ pshow i e

149 OK _ -> iputStrLn "Universes OK"

148 OK _ -> iputStrLn "Universes OK"

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

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

151− lift $ print (lookupDef Nothing n ctxt)

150+ liftIO $ print (lookupDef Nothing n ctxt)

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

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

153 ctxt <- getContext

152 ctxt <- getContext

154 ist <- get

153 ist <- get

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

165 shst' <- lift $ runShell shst

164 shst' <- lift $ runShell shst

166 return ()

165 return ()

167process (Execute f) = do compile f

166process (Execute f) = do compile f

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

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

169 return ()

168 return ()

170process (Compile f) = do compile f

169process (Compile f) = do compile f

171process (LogLvl i) = setLogLevel i

170process (LogLvl i) = setLogLevel i

src/Main.hs+5−5

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

1module Main where

3−import System.Console.Readline

3+import System.Console.Haskeline

4import System.IO

5import System.Environment

6import System.Exit

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

43main = do xs <- getArgs

44 opts <- parseArgs xs

45− execStateT (runIdris opts) idrisInit

45+ runInputT defaultSettings $ execStateT (runIdris opts) idrisInit

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

48runIdris opts =

49 do let inputs = opt getFile opts

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

51 let output = opt getOutput opts

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

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

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

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

54 setREPL runrepl

55 mapM_ makeOption opts

56 elabPrims

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

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

66 when runrepl $ repl ist inputs

67 ok <- noErrors

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

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

69 where

70 makeOption (OLogging i) = setLogLevel i

71 makeOption TypeCase = setTypeCase True