aee8f60 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Parsing a REPL command may now result in a custom error message.

aee8f60Michael Maloney12 years ago

src/Idris/REPL.hs+25−21

compare with master

unifiedsplit

@@ -170,7 +170,8 @@ processNetCmd :: IState -> IState -> Handle -> FilePath -> String ->

170processNetCmd orig i h fn cmd

171 = do res <- case parseCmd i "(net)" cmd of

172 Failure err -> return (Left (Msg " invalid command"))

173− Success c -> runErrorT $ evalStateT (processNet fn c) i

173+ Success (Right c) -> runErrorT $ evalStateT (processNet fn c) i

174+ Success (Left err) -> return (Left (Msg err))

174 case res of

175 case res of

175 Right x -> return x

176 Right x -> return x

176 Left err -> do hPutStrLn h (show err)

177 Left err -> do hPutStrLn h (show err)

@@ -274,7 +275,7 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.Interpret cmd) =

274 i <- getIState

275 i <- getIState

275 case parseCmd i "(input)" cmd of

276 case parseCmd i "(input)" cmd of

276 Failure err -> iPrintError $ show (fixColour False err)

277 Failure err -> iPrintError $ show (fixColour False err)

277− Success (Prove n') ->

278+ Success (Right (Prove n')) ->

278 idrisCatch

279 idrisCatch

279 (do process fn (Prove n')

280 (do process fn (Prove n')

280 isetPrompt (mkPrompt mods)

281 isetPrompt (mkPrompt mods)

@@ -293,7 +294,7 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.Interpret cmd) =

293 IdeSlave.convSExp "abandon-proof" "Abandoned" n

294 IdeSlave.convSExp "abandon-proof" "Abandoned" n

294 _ -> return ()

295 _ -> return ()

295 iRenderError $ pprintErr ist e)

296 iRenderError $ pprintErr ist e)

296− Success cmd -> idrisCatch

297+ Success (Right cmd) -> idrisCatch

297 (ideslaveProcess fn cmd)

298 (ideslaveProcess fn cmd)

298 (\e -> getIState >>= iRenderError . flip pprintErr e)

299 (\e -> getIState >>= iRenderError . flip pprintErr e)

299runIdeSlaveCommand h id orig fn mods (IdeSlave.REPLCompletions str) =

300runIdeSlaveCommand h id orig fn mods (IdeSlave.REPLCompletions str) =

@@ -600,36 +601,38 @@ processInput cmd orig inputs

600 _ -> ""

601 _ -> ""

601 c <- colourise

602 c <- colourise

602 case parseCmd i "(input)" cmd of

603 case parseCmd i "(input)" cmd of

603− Failure err -> do runIO $ print (fixColour c err)

604+ Failure err -> do runIO $ putStrLn "Command not recognized."

604 return (Just inputs)

605 return (Just inputs)

605− Success Reload ->

606+ Success (Right Reload) ->

606 do putIState $ orig { idris_options = idris_options i

607 do putIState $ orig { idris_options = idris_options i

607 , idris_colourTheme = idris_colourTheme i

608 , idris_colourTheme = idris_colourTheme i

608 }

609 }

609 clearErr

610 clearErr

610 mods <- loadInputs inputs Nothing

611 mods <- loadInputs inputs Nothing

611 return (Just inputs)

612 return (Just inputs)

612− Success (Load f toline) ->

613+ Success (Right (Load f toline)) ->

613 do putIState orig { idris_options = idris_options i

614 do putIState orig { idris_options = idris_options i

614 , idris_colourTheme = idris_colourTheme i

615 , idris_colourTheme = idris_colourTheme i

615 }

616 }

616 clearErr

617 clearErr

617 mod <- loadInputs [f] toline

618 mod <- loadInputs [f] toline

618 return (Just [f])

619 return (Just [f])

619− Success (ModImport f) ->

620+ Success (Right (ModImport f)) ->

620 do clearErr

621 do clearErr

621 fmod <- loadModule f

622 fmod <- loadModule f

622 return (Just (inputs ++ [fmod]))

623 return (Just (inputs ++ [fmod]))

623− Success Edit -> do -- takeMVar stvar

624+ Success (Right Edit) -> do -- takeMVar stvar

624 edit fn orig

625 edit fn orig

625 return (Just inputs)

626 return (Just inputs)

626− Success Proofs -> do proofs orig

627+ Success (Right Proofs) -> do proofs orig

627− return (Just inputs)

628+ return (Just inputs)

628− Success Quit -> do when (not quiet) (iputStrLn "Bye bye")

629+ Success (Right Quit) -> do when (not quiet) (iputStrLn "Bye bye")

629− return Nothing

630+ return Nothing

630− Success cmd -> do idrisCatch (process fn cmd)

631+ Success (Right cmd ) -> do idrisCatch (process fn cmd)

631 (\e -> do msg <- showErr e ; iputStrLn msg)

632 (\e -> do msg <- showErr e ; iputStrLn msg)

633+ return (Just inputs)

634+ Success (Left err) -> do runIO $ putStrLn err

632− return (Just inputs)

635+ return (Just inputs)

633

636

634resolveProof :: Name -> Idris Name

637resolveProof :: Name -> Idris Name

635resolveProof n'

638resolveProof n'

@@ -1582,13 +1585,14 @@ initScript = do script <- getInitScript

1582 processLine i cmd input clr =

1585 processLine i cmd input clr =

1583 case parseCmd i input cmd of

1586 case parseCmd i input cmd of

1584 Failure err -> runIO $ print (fixColour clr err)

1587 Failure err -> runIO $ print (fixColour clr err)

1585− Success Reload -> iPrintError "Init scripts cannot reload the file"

1588+ Success (Right Reload) -> iPrintError "Init scripts cannot reload the file"

1586− Success (Load f _) -> iPrintError "Init scripts cannot load files"

1589+ Success (Right (Load f _)) -> iPrintError "Init scripts cannot load files"

1587− Success (ModImport f) -> iPrintError "Init scripts cannot import modules"

1590+ Success (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"

1588− Success Edit -> iPrintError "Init scripts cannot invoke the editor"

1591+ Success (Right Edit) -> iPrintError "Init scripts cannot invoke the editor"

1589− Success Proofs -> proofs i

1592+ Success (Right Proofs) -> proofs i

1590− Success Quit -> iPrintError "Init scripts cannot quit Idris"

1593+ Success (Right Quit) -> iPrintError "Init scripts cannot quit Idris"

1591− Success cmd -> process [] cmd

1594+ Success (Right cmd ) -> process [] cmd

1595+ Success (Left err) -> runIO $ print err

1592

1596

1593getFile :: Opt -> Maybe String

1597getFile :: Opt -> Maybe String

1594getFile (Filename str) = Just str

1598getFile (Filename str) = Just str

src/Idris/REPLParser.hs+60−61

@@ -23,7 +23,7 @@ import Data.List.Split(splitOn)

23import Data.Char(toLower)

24import qualified Data.ByteString.UTF8 as UTF8

26−parseCmd :: IState -> String -> String -> Result Command

26+parseCmd :: IState -> String -> String -> Result (Either String Command)

27parseCmd i inputname = P.runparser pCmd i inputname

29cmd :: [String] -> P.IdrisParser ()

@@ -31,109 +31,108 @@ cmd xs = try (do P.lchar ':'; docmd (sortBy (\x y -> compare (length y) (length

31 where docmd [] = fail "No such command"

32 docmd (x:xs) = try (discard (P.reserved x)) <|> docmd xs

34−pCmd :: P.IdrisParser Command

34+pCmd :: P.IdrisParser (Either String Command)

35−

36−pCmd = do P.whiteSpace; do cmd ["q", "quit"]; eof; return Quit

35+pCmd = do P.whiteSpace; do cmd ["q", "quit"]; eof; return (Right Quit)

37− <|> do cmd ["h", "?", "help"]; eof; return Help

36+ <|> do cmd ["h", "?", "help"]; eof; return (Right Help)

38− <|> do cmd ["w", "warranty"]; eof; return Warranty

37+ <|> do cmd ["w", "warranty"]; eof; return (Right Warranty)

39− <|> do cmd ["r", "reload"]; eof; return Reload

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

40 <|> do cmd ["module"]; f <- P.identifier; eof;

39 <|> do cmd ["module"]; f <- P.identifier; eof;

41− return (ModImport (toPath f))

40+ return (Right (ModImport (toPath f)))

42− <|> do cmd ["e", "edit"]; eof; return Edit

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

43− <|> do cmd ["exec", "execute"]; eof; return Execute

42+ <|> do cmd ["exec", "execute"]; ((try $ eof >> return (Right Execute)) <|> return (Left "exec(ute) does not take any parameters"))

44 <|> try (do cmd ["c", "compile"]

43 <|> try (do cmd ["c", "compile"]

45 i <- get

44 i <- get

46 f <- P.identifier

45 f <- P.identifier

47 eof

46 eof

48− return (Compile (Via "c") f))

47+ return (Right (Compile (Via "c") f)))

49 <|> do cmd ["c", "compile"]

48 <|> do cmd ["c", "compile"]

50 i <- get

49 i <- get

51 c <- codegenOption

50 c <- codegenOption

52 f <- P.identifier

51 f <- P.identifier

53 eof

52 eof

54− return (Compile c f)

53+ return (Right (Compile c f))

55− <|> do cmd ["proofs"]; eof; return Proofs

54+ <|> do cmd ["proofs"]; eof; return (Right Proofs)

56− <|> do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n)

55+ <|> do cmd ["rmproof"]; n <- P.name; eof; return (Right (RmProof n))

57− <|> do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n)

56+ <|> do cmd ["showproof"]; n <- P.name; eof; return (Right (ShowProof n))

58− <|> do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i))

57+ <|> do cmd ["log"]; i <- P.natural; eof; return (Right (LogLvl (fromIntegral i)))

59 <|> do cmd ["let"]

58 <|> do cmd ["let"]

60 defn <- concat <$> many (P.decl defaultSyntax)

59 defn <- concat <$> many (P.decl defaultSyntax)

61− return (NewDefn defn)

60+ return (Right (NewDefn defn))

62 <|> do cmd ["unlet","undefine"]

61 <|> do cmd ["unlet","undefine"]

63− Undefine `fmap` many P.name

62+ (Right . Undefine) `fmap` many P.name

64 <|> do cmd ["lto", "loadto"];

63 <|> do cmd ["lto", "loadto"];

65 toline <- P.natural

64 toline <- P.natural

66 f <- many anyChar;

65 f <- many anyChar;

67− return (Load f (Just (fromInteger toline)))

66+ return (Right (Load f (Just (fromInteger toline))))

68 <|> do cmd ["l", "load"]; f <- many anyChar;

67 <|> do cmd ["l", "load"]; f <- many anyChar;

69− return (Load f Nothing)

68+ return (Right (Load f Nothing))

70− <|> do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f)

69+ <|> do cmd ["cd"]; f <- many anyChar; return (Right (ChangeDirectory f))

71− <|> do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t)

70+ <|> do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Right (Spec t))

72− <|> do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t)

71+ <|> do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Right (HNF t))

73− <|> do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t)

72+ <|> do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Right (TestInline t))

74− <|> do c <- try (cmd ["doc"] *> P.constant); eof; return (DocStr (Right c))

73+ <|> do c <- try (cmd ["doc"] *> P.constant); eof; return (Right (DocStr (Right c)))

75− <|> do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr (Left n))

74+ <|> do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (Right (DocStr (Left n)))

76− <|> do cmd ["d", "def"]; P.whiteSpace; n <- P.fnName; eof; return (Defn n)

75+ <|> do cmd ["d", "def"]; P.whiteSpace; n <- P.fnName; eof; return (Right (Defn n))

77− <|> do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n)

76+ <|> do cmd ["total"]; do n <- P.fnName; eof; return (Right (TotCheck n))

78− <|> do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t)

77+ <|> do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Right (Check t))

79− <|> do cmd ["u", "universes"]; eof; return Universes

78+ <|> do cmd ["u", "universes"]; eof; return (Right Universes)

80− <|> do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (DebugInfo n)

79+ <|> do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (Right (DebugInfo n))

81− <|> do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Missing n)

80+ <|> do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Right (Missing n))

82− <|> try (do cmd ["dynamic"]; eof; return ListDynamic)

81+ <|> try (do cmd ["dynamic"]; eof; return (Right ListDynamic))

83− <|> do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l)

82+ <|> do cmd ["dynamic"]; l <- many anyChar; return (Right (DynamicLink l))

84− <|> do cmd ["color", "colour"]; pSetColourCmd

83+ <|> do cmd ["color", "colour"]; pSetColourCmd >>= return . Right

85− <|> do cmd ["set"]; o <- pOption; return (SetOpt o)

84+ <|> do cmd ["set"]; o <- pOption; return (Right (SetOpt o))

86− <|> do cmd ["unset"]; o <- pOption; return (UnsetOpt o)

85+ <|> do cmd ["unset"]; o <- pOption; return (Right (UnsetOpt o))

87 <|> do cmd ["s", "search"]; P.whiteSpace;

86 <|> do cmd ["s", "search"]; P.whiteSpace;

88− t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Search t)

87+ t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Right (Search t))

89 <|> do cmd ["cs", "casesplit"]; P.whiteSpace;

88 <|> do cmd ["cs", "casesplit"]; P.whiteSpace;

90 upd <- option False (do P.lchar '!'; return True)

89 upd <- option False (do P.lchar '!'; return True)

91 l <- P.natural; n <- P.name;

90 l <- P.natural; n <- P.name;

92− return (CaseSplitAt upd (fromInteger l) n)

91+ return (Right (CaseSplitAt upd (fromInteger l) n))

93 <|> do cmd ["apc", "addproofclause"]; P.whiteSpace;

92 <|> do cmd ["apc", "addproofclause"]; P.whiteSpace;

94 upd <- option False (do P.lchar '!'; return True)

93 upd <- option False (do P.lchar '!'; return True)

95 l <- P.natural; n <- P.name;

94 l <- P.natural; n <- P.name;

96− return (AddProofClauseFrom upd (fromInteger l) n)

95+ return (Right (AddProofClauseFrom upd (fromInteger l) n))

97 <|> do cmd ["ac", "addclause"]; P.whiteSpace;

96 <|> do cmd ["ac", "addclause"]; P.whiteSpace;

98 upd <- option False (do P.lchar '!'; return True)

97 upd <- option False (do P.lchar '!'; return True)

99 l <- P.natural; n <- P.name;

98 l <- P.natural; n <- P.name;

100− return (AddClauseFrom upd (fromInteger l) n)

99+ return (Right (AddClauseFrom upd (fromInteger l) n))

101 <|> do cmd ["am", "addmissing"]; P.whiteSpace;

100 <|> do cmd ["am", "addmissing"]; P.whiteSpace;

102 upd <- option False (do P.lchar '!'; return True)

101 upd <- option False (do P.lchar '!'; return True)

103 l <- P.natural; n <- P.name;

102 l <- P.natural; n <- P.name;

104− return (AddMissing upd (fromInteger l) n)

103+ return (Right (AddMissing upd (fromInteger l) n))

105 <|> do cmd ["mw", "makewith"]; P.whiteSpace;

104 <|> do cmd ["mw", "makewith"]; P.whiteSpace;

106 upd <- option False (do P.lchar '!'; return True)

105 upd <- option False (do P.lchar '!'; return True)

107 l <- P.natural; n <- P.name;

106 l <- P.natural; n <- P.name;

108− return (MakeWith upd (fromInteger l) n)

107+ return (Right (MakeWith upd (fromInteger l) n))

109 <|> do cmd ["ml", "makelemma"]; P.whiteSpace;

108 <|> do cmd ["ml", "makelemma"]; P.whiteSpace;

110 upd <- option False (do P.lchar '!'; return True)

109 upd <- option False (do P.lchar '!'; return True)

111 l <- P.natural; n <- P.name;

110 l <- P.natural; n <- P.name;

112− return (MakeLemma upd (fromInteger l) n)

111+ return (Right (MakeLemma upd (fromInteger l) n))

113 <|> do cmd ["ps", "proofsearch"]; P.whiteSpace;

112 <|> do cmd ["ps", "proofsearch"]; P.whiteSpace;

114 upd <- option False (do P.lchar '!'; return True)

113 upd <- option False (do P.lchar '!'; return True)

115 l <- P.natural; n <- P.name;

114 l <- P.natural; n <- P.name;

116 hints <- many P.fnName

115 hints <- many P.fnName

117− return (DoProofSearch upd True (fromInteger l) n hints)

116+ return (Right (DoProofSearch upd True (fromInteger l) n hints))

118 <|> do cmd ["ref", "refine"]; P.whiteSpace;

117 <|> do cmd ["ref", "refine"]; P.whiteSpace;

119 upd <- option False (do P.lchar '!'; return True)

118 upd <- option False (do P.lchar '!'; return True)

120 l <- P.natural; n <- P.name;

119 l <- P.natural; n <- P.name;

121 hint <- P.fnName

120 hint <- P.fnName

122− return (DoProofSearch upd False (fromInteger l) n [hint])

121+ return (Right (DoProofSearch upd False (fromInteger l) n [hint]))

123− <|> do cmd ["p", "prove"]; n <- P.name; eof; return (Prove n)

122+ <|> do cmd ["p", "prove"]; n <- P.name; eof; return (Right (Prove n))

124− <|> do cmd ["m", "metavars"]; eof; return Metavars

123+ <|> do cmd ["m", "metavars"]; eof; return (Right Metavars)

125 <|> do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;

124 <|> do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;

126 return (Just x))

125 return (Just x))

127− eof; return (AddProof n)

126+ eof; return (Right (AddProof n))

128− <|> do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t)

127+ <|> do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Right (ExecVal t))

129− <|> do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t)

128+ <|> do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Right (Pattelab t))

130− <|> do cmd ["errorhandlers"]; eof ; return ListErrorHandlers

129+ <|> do cmd ["errorhandlers"]; eof ; return (Right ListErrorHandlers)

131− <|> do cmd ["consolewidth"]; w <- pConsoleWidth ; return (SetConsoleWidth w)

130+ <|> do cmd ["consolewidth"]; w <- pConsoleWidth ; return (Right (SetConsoleWidth w))

132− <|> do cmd ["apropos"]; str <- many anyChar ; return (Apropos str)

131+ <|> do cmd ["apropos"]; str <- many anyChar ; return (Right (Apropos str))

133− <|> do cmd ["wc", "whocalls"]; P.whiteSpace; n <- P.fnName ; return (WhoCalls n)

132+ <|> do cmd ["wc", "whocalls"]; P.whiteSpace; n <- P.fnName ; return (Right (WhoCalls n))

134− <|> do cmd ["cw", "callswho"]; P.whiteSpace; n <- P.fnName ; return (CallsWho n)

133+ <|> do cmd ["cw", "callswho"]; P.whiteSpace; n <- P.fnName ; return (Right (CallsWho n))

135− <|> do cmd ["mkdoc"]; str <- many anyChar; return (MakeDoc str)

134+ <|> do cmd ["mkdoc"]; str <- many anyChar; return (Right (MakeDoc str))

136− <|> do cmd ["printdef"]; P.whiteSpace; n <- P.fnName; return (PrintDef n)

135+ <|> do cmd ["printdef"]; P.whiteSpace; n <- P.fnName; return (Right (PrintDef n))

137 <|> do cmd ["pp", "pprint"]

136 <|> do cmd ["pp", "pprint"]

138 P.whiteSpace

137 P.whiteSpace

139 fmt <- ppFormat

138 fmt <- ppFormat

@@ -141,9 +140,9 @@ pCmd = do P.whiteSpace; do cmd ["q", "quit"]; eof; return Quit

141 n <- fmap fromInteger P.natural

140 n <- fmap fromInteger P.natural

142 P.whiteSpace

141 P.whiteSpace

143 t <- P.fullExpr defaultSyntax

142 t <- P.fullExpr defaultSyntax

144− return (PPrint fmt n t)

143+ return (Right (PPrint fmt n t))

145− <|> do P.whiteSpace; do eof; return NOP

144+ <|> do P.whiteSpace; do eof; return (Right NOP)

146− <|> do t <- P.fullExpr defaultSyntax; return (Eval t)

145+ <|> do t <- P.fullExpr defaultSyntax; return (Right (Eval t))

147

146

148 where toPath n = foldl1' (</>) $ splitOn "." n

147 where toPath n = foldl1' (</>) $ splitOn "." n

149

148