22546bc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

:r and :e at the REPL.

22546bcEdwin Brady15 years ago

interp.idr+1−1

compare with master

unifiedsplit

@@ -67,7 +67,7 @@ test : Int;

67test = interp Empty eProg 2 2;

69testFac : Int;

70−testFac = interp Empty eFac 3;

70+testFac = interp Empty eFac 4;

72intToStr : Int -> String;

73intToStr 0 = "O";

src/Idris/AbsSyntax.hs+14−3

@@ -38,11 +38,12 @@ data IState = IState { tt_ctxt :: Context,

38 syntax_rules :: [Syntax],

39 syntax_keywords :: [String],

40 imported :: [FilePath],

41− idris_prims :: [(Name, ([E.Name], E.Term))]

41+ idris_prims :: [(Name, ([E.Name], E.Term))],

42+ errLine :: Maybe Int

42 }

43 }

44idrisInit = IState emptyContext [] emptyContext emptyContext

45idrisInit = IState emptyContext [] emptyContext emptyContext

45− "" defaultOpts 6 [] [] [] [] []

46+ "" defaultOpts 6 [] [] [] [] [] Nothing

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

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

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

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

@@ -51,6 +52,16 @@ type Idris a = StateT IState IO a

51getContext :: Idris Context

52getContext :: Idris Context

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

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

55+setErrLine :: Int -> Idris ()

56+setErrLine x = do i <- get;

57+ case (errLine i) of

58+ Nothing -> put (i { errLine = Just x })

59+ Just _ -> return ()

60+

61+clearErr :: Idris ()

62+clearErr = do i <- get

63+ put (i { errLine = Nothing })

64+

54getIState :: Idris IState

65getIState :: Idris IState

55getIState = get

66getIState = get

@@ -124,7 +135,7 @@ setTypeCase t = do i <- get

124

135

125-- Commands in the REPL

136-- Commands in the REPL

126

137

127−data Command = Quit | Help | Eval PTerm

138+data Command = Quit | Help | Eval PTerm | Reload | Edit

128 | Compile String

139 | Compile String

129 | Metavars | Prove Name

140 | Metavars | Prove Name

130 | TTShell

141 | TTShell

src/Idris/ElabDecls.hs+4−1

@@ -303,7 +303,10 @@ pvars ist _ = []

303-- TODO: Also build a 'binary' version of each declaration for fast reloading

304

305elabDecl :: ElabInfo -> PDecl -> Idris ()

306−elabDecl info d = idrisCatch (elabDecl' info d) (\e -> iputStrLn (report e))

306+elabDecl info d = idrisCatch (elabDecl' info d)

307+ (\e -> do let msg = report e

308+ setErrLine (getErrLine msg)

309+ iputStrLn msg)

307

310

308elabDecl' info (PFix _ _ _) = return () -- nothing to elaborate

311elabDecl' info (PFix _ _ _) = return () -- nothing to elaborate

309elabDecl' info (PSyntax _ p) = return () -- nothing to elaborate

312elabDecl' info (PSyntax _ p) = return () -- nothing to elaborate

src/Idris/Error.hs+10

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

9import Control.Monad.State

10import System.IO.Error

11+import Data.Char

12report :: IOError -> String

13report :: IOError -> String

13report e

14report e

@@ -27,5 +28,14 @@ tclift :: Show a => TC a -> Idris a

27tclift tc = case tc of

28tclift tc = case tc of

28 OK v -> return v

29 OK v -> return v

29 Error err -> do i <- get

30 Error err -> do i <- get

31+ case err of

32+ At (FC f l) e -> setErrLine l

33+ _ -> return ()

30 fail (pshow i err)

34 fail (pshow i err)

36+getErrLine str

37+ = case span (/=':') str of

38+ (_, ':':rest) -> case span isDigit rest of

39+ (num, _) -> read num

40+ _ -> 0

41+

src/Idris/Parser.hs+28−14

@@ -2,14 +2,16 @@ module Idris.Parser where

3import Idris.AbsSyntax

4import Idris.Imports

5−import Paths_miniidris

5+import Idris.Error

6import Idris.ElabDecls

7+import Paths_miniidris

8import Core.CoreParser

9import Core.CoreParser

9import Core.TT

10import Core.TT

10import Core.Evaluate

11import Core.Evaluate

12import Text.ParserCombinators.Parsec

13import Text.ParserCombinators.Parsec

14+import Text.ParserCombinators.Parsec.Error

13import Text.ParserCombinators.Parsec.Expr

15import Text.ParserCombinators.Parsec.Expr

14import Text.ParserCombinators.Parsec.Language

16import Text.ParserCombinators.Parsec.Language

15import qualified Text.ParserCombinators.Parsec.Token as PTok

17import qualified Text.ParserCombinators.Parsec.Token as PTok

@@ -47,17 +49,22 @@ lchar = lexeme.char

47-- Loading modules

49-- Loading modules

49loadModule :: FilePath -> Idris String

51loadModule :: FilePath -> Idris String

52+loadModule f

50−loadModule f = do datadir <- lift $ getDataDir

53+ = idrisCatch (do datadir <- lift $ getDataDir

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

54+ fp <- lift $ findImport [".", datadir] f

52− i <- getIState

55+ i <- getIState

53− if (f `elem` imported i)

56+ if (f `elem` imported i)

54− then iLOG $ "Already read " ++ f

57+ then iLOG $ "Already read " ++ f

55− else do putIState (i { imported = f : imported i })

58+ else do putIState (i { imported = f : imported i })

56− case fp of

59+ case fp of

57− IDR fn -> loadSource fn

60+ IDR fn -> loadSource fn

58− IBC fn -> error "Not implemented"

61+ IBC fn -> error "Not implemented"

59− let (dir, fh) = splitFileName f

62+ let (dir, fh) = splitFileName f

60− return (dropExtension fh)

63+ return (dropExtension fh))

64+ (\e -> do let msg = report e

65+ setErrLine (getErrLine msg)

66+ iputStrLn msg

67+ return "")

62loadSource :: FilePath -> Idris ()

69loadSource :: FilePath -> Idris ()

63loadSource f = do iLOG ("Reading " ++ f)

70loadSource f = do iLOG ("Reading " ++ f)

@@ -84,9 +91,13 @@ parseImports fname input

84 rest <- getInput

91 rest <- getInput

85 pos <- getPosition

92 pos <- getPosition

86 return ((ps, rest, pos), i)) i fname input) of

93 return ((ps, rest, pos), i)) i fname input) of

87− Left err -> fail (show err)

94+ Left err -> fail (ishow err)

88 Right (x, i) -> do put i

95 Right (x, i) -> do put i

89 return x

96 return x

97+ where ishow err = let ln = sourceLine (errorPos err) in

98+ fname ++ ":" ++ show ln ++ ":parse error"

99+-- show (map messageString (errorMessages err))

100+

101

91pfc :: IParser FC

102pfc :: IParser FC

92pfc = do s <- getPosition

103pfc = do s <- getPosition

@@ -111,9 +122,12 @@ parseProg syn fname input pos

111 eof

122 eof

112 i' <- getState

123 i' <- getState

113 return (concat ps, i')) i fname input) of

124 return (concat ps, i')) i fname input) of

114− Left err -> fail (show err)

125+ Left err -> fail (ishow err)

115 Right (x, i) -> do put i

126 Right (x, i) -> do put i

116 return (collect x)

127 return (collect x)

128+ where ishow err = let ln = sourceLine (errorPos err) in

129+ fname ++ ":" ++ show ln ++ ":parse error"

130+-- show (map messageString (errorMessages err))

117

131

118-- Collect PClauses with the same function name

132-- Collect PClauses with the same function name

119

133

src/Idris/REPL.hs+79−46

@@ -9,69 +9,102 @@ import Idris.Error

9import Idris.Delaborate

10import Idris.Compiler

11import Idris.Prover

12+import Idris.Parser

13import Core.Evaluate

14import Core.Evaluate

14import Core.ProofShell

15import Core.ProofShell

15import Core.TT

16import Core.TT

17import System.Console.Readline

18import System.Console.Readline

19+import System.FilePath

20+import System.Environment

21+import System.Process

18import Control.Monad

22import Control.Monad

19import Control.Monad.State

23import Control.Monad.State

20import Data.List

24import Data.List

25+import Data.Char

22−repl :: String -> Idris ()

27+repl :: IState -> [FilePath] -> Idris ()

23−repl prompt

28+repl orig mods

29+ = do let prompt = mkPrompt mods

24− = do x <- lift $ readline (prompt ++ "> ")

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

25 case x of

31 case x of

26− Nothing -> repl prompt

32+ Nothing -> repl orig mods

27 Just input -> do lift $ addHistory input

33 Just input -> do lift $ addHistory input

28− continue <- processInput input

34+ ms <- processInput input orig mods

29− when continue (repl prompt)

35+ case ms of

36+ Just mods -> repl orig mods

37+ Nothing -> return ()

39+mkPrompt [] = "Idris"

40+mkPrompt [x] = "*" ++ dropExtension x

41+mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs

42+

31−processInput :: String -> Idris Bool

43+processInput :: String -> IState -> [FilePath] -> Idris (Maybe [FilePath])

32−processInput cmd

44+processInput cmd orig inputs

33 = do i <- get

45 = do i <- get

46+ let fn = case inputs of

47+ (f:_) -> f

48+ _ -> ""

34 case parseCmd i cmd of

49 case parseCmd i cmd of

35 Left err -> do lift $ print err

50 Left err -> do lift $ print err

36− return True

51+ return (Just inputs)

52+ Right Reload -> do put orig

53+ clearErr

54+ mods <- mapM loadModule inputs

55+ return (Just inputs)

37 Right Quit -> do iputStrLn "Bye bye"

56 Right Quit -> do iputStrLn "Bye bye"

38− return False

57+ return Nothing

39− Right cmd -> do idrisCatch (process cmd)

58+ Right cmd -> do idrisCatch (process fn cmd)

40 (\e -> iputStrLn (report e))

59 (\e -> iputStrLn (report e))

41− return True

60+ return (Just inputs)

42−

61+

43−process :: Command -> Idris ()

62+process :: FilePath -> Command -> Idris ()

44−process Help

63+process _ Help

45 = iputStrLn "At some point I'll write some help text. Thanks for asking though."

64 = iputStrLn "At some point I'll write some help text. Thanks for asking though."

65+process "" Edit = iputStrLn "Nothing to edit"

66+process f Edit

67+ = do i <- get

68+ env <- lift $ getEnvironment

69+ let editor = getEditor env

70+ let line = case errLine i of

71+ Just l -> " +" ++ show l ++ " "

72+ Nothing -> " "

73+ let cmd = editor ++ line ++ f

74+ lift $ system cmd

75+ return ()

76+ where getEditor env | Just ed <- lookup "EDITOR" env = ed

77+ | Just ed <- lookup "VISUAL" env = ed

78+ | otherwise = "vi"

46−process (Eval t) = do (tm, ty) <- elabVal toplevel t

79+process _ (Eval t) = do (tm, ty) <- elabVal toplevel t

47− ctxt <- getContext

80+ ctxt <- getContext

48− ist <- get

81+ ist <- get

49− let tm' = normaliseC ctxt [] tm

82+ let tm' = normaliseC ctxt [] tm

50− let ty' = normaliseC ctxt [] ty

83+ let ty' = normaliseC ctxt [] ty

51− logLvl 3 $ "Raw: " ++ show (tm', ty')

84+ logLvl 3 $ "Raw: " ++ show (tm', ty')

52− iputStrLn (show (delab ist tm') ++ " : " ++

85+ iputStrLn (show (delab ist tm') ++ " : " ++

53− show (delab ist ty'))

86+ show (delab ist ty'))

54−process (Spec t) = do (tm, ty) <- elabVal toplevel t

87+process _ (Spec t) = do (tm, ty) <- elabVal toplevel t

55− ctxt <- getContext

88+ ctxt <- getContext

56− ist <- get

89+ ist <- get

57− let tm' = specialise ctxt (idris_statics ist) tm

90+ let tm' = specialise ctxt (idris_statics ist) tm

58− iputStrLn (show (delab ist tm'))

91+ iputStrLn (show (delab ist tm'))

59−process (Prove n) = prover n

92+process _ (Prove n) = prover n

60−process (HNF t) = do (tm, ty) <- elabVal toplevel t

93+process _ (HNF t) = do (tm, ty) <- elabVal toplevel t

61− ctxt <- getContext

94+ ctxt <- getContext

62− ist <- get

95+ ist <- get

63− let tm' = hnf ctxt [] tm

96+ let tm' = hnf ctxt [] tm

64− iputStrLn (show (delab ist tm'))

97+ iputStrLn (show (delab ist tm'))

65−process TTShell = do ist <- get

98+process _ TTShell = do ist <- get

66− let shst = initState (tt_ctxt ist)

99+ let shst = initState (tt_ctxt ist)

67− shst' <- lift $ runShell shst

100+ shst' <- lift $ runShell shst

68− return ()

101+ return ()

69−process (Compile f) = do compile f

102+process _ (Compile f) = do compile f

70−process (LogLvl i) = setLogLevel i

103+process _ (LogLvl i) = setLogLevel i

71−process Metavars = do ist <- get

104+process _ Metavars = do ist <- get

72− let mvs = idris_metavars ist \\ primDefs

105+ let mvs = idris_metavars ist \\ primDefs

73− case mvs of

106+ case mvs of

74− [] -> iputStrLn "No global metavariables to solve"

107+ [] -> iputStrLn "No global metavariables to solve"

75− _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs

108+ _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs

76−process NOP = return ()

109+process _ NOP = return ()

110

src/Idris/REPLParser.hs+2

@@ -22,6 +22,8 @@ cmd xs = do lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)

22pCmd :: IParser Command

23pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

24 <|> try (do cmd ["h", "?", "help"]; eof; return Help)

25+ <|> try (do cmd ["r", "reload"]; eof; return Reload)

26+ <|> try (do cmd ["e", "edit"]; eof; return Edit)

25 <|> try (do cmd ["ttshell"]; eof; return TTShell)

27 <|> try (do cmd ["ttshell"]; eof; return TTShell)

26 <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile f))

28 <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile f))

27 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)

29 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)

src/Main.hs+2−5

@@ -48,17 +48,14 @@ runIdris opts =

48 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"

49 return ()

50 when runrepl $ iputStrLn banner

51+ ist <- get

51 mods <- mapM loadModule inputs

52 mods <- mapM loadModule inputs

52− when runrepl $ repl (mkPrompt mods)

53+ when runrepl $ repl ist inputs

53 where

54 where

54 makeOption (OLogging i) = setLogLevel i

55 makeOption (OLogging i) = setLogLevel i

55 makeOption TypeCase = setTypeCase True

56 makeOption TypeCase = setTypeCase True

56 makeOption _ = return ()

57 makeOption _ = return ()

58−mkPrompt [] = "Idris"

59−mkPrompt [x] = "*" ++ x

60−mkPrompt (x:xs) = "*" ++ x ++ " " ++ mkPrompt xs

61−

62getFile :: Opt -> Maybe String

59getFile :: Opt -> Maybe String

63getFile (Filename str) = Just str

60getFile (Filename str) = Just str

64getFile _ = Nothing

61getFile _ = Nothing