5048ad4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Introduce ParseError type alias

5048ad4Jason Felice9 years ago

src/Idris/Main.hs+5−6

compare with master

unifiedsplit

@@ -47,7 +47,6 @@ import System.Exit

47import System.FilePath

48import System.IO

49import System.IO.CodePage (withCP65001)

50−import qualified Text.Trifecta.Result as P

52-- | How to run Idris programs.

51-- | How to run Idris programs.

53runMain :: Idris () -> IO ()

52runMain :: Idris () -> IO ()

@@ -196,8 +195,8 @@ idrisMain opts =

196 mapM_ (\str -> do ist <- getIState

195 mapM_ (\str -> do ist <- getIState

197 c <- colourise

196 c <- colourise

198 case parseExpr ist str of

197 case parseExpr ist str of

199− Left (P.ErrInfo err _) -> do iputStrLn $ show (fixColour c err)

198+ Left err -> do iputStrLn $ show (fixColour c err)

200− runIO $ exitWith (ExitFailure 1)

199+ runIO $ exitWith (ExitFailure 1)

201 Right e -> process "" (Eval e))

200 Right e -> process "" (Eval e))

202 exprs

201 exprs

203 runIO exitSuccess

202 runIO exitSuccess

@@ -273,8 +272,8 @@ execScript :: String -> Idris ()

273execScript expr = do i <- getIState

272execScript expr = do i <- getIState

274 c <- colourise

273 c <- colourise

275 case parseExpr i expr of

274 case parseExpr i expr of

276− Left (P.ErrInfo err _) -> do iputStrLn $ show (fixColour c err)

275+ Left err -> do iputStrLn $ show (fixColour c err)

277− runIO $ exitWith (ExitFailure 1)

276+ runIO $ exitWith (ExitFailure 1)

278 Right term -> do ctxt <- getContext

277 Right term -> do ctxt <- getContext

279 (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term

278 (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term

280 res <- execute tm

279 res <- execute tm

@@ -300,7 +299,7 @@ initScript = do script <- runIO $ getIdrisInitScript

300 runInit h

299 runInit h

301 processLine i cmd input clr =

300 processLine i cmd input clr =

302 case parseCmd i input cmd of

301 case parseCmd i input cmd of

303− Left (P.ErrInfo err _) -> runIO $ print (fixColour clr err)

302+ Left err -> runIO $ print (fixColour clr err)

304 Right (Right Reload) -> iPrintError "Init scripts cannot reload the file"

303 Right (Right Reload) -> iPrintError "Init scripts cannot reload the file"

305 Right (Right (Load f _)) -> iPrintError "Init scripts cannot load files"

304 Right (Right (Load f _)) -> iPrintError "Init scripts cannot load files"

306 Right (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"

305 Right (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"

src/Idris/Package/Parser.hs+1−1

@@ -56,7 +56,7 @@ parseDesc fp = do

56 then do

57 p <- readFile fp

58 case runparser pPkg defaultPkg fp p of

59− Left (P.ErrInfo err _) -> fail (show $ PP.plain err)

59+ Left err -> fail (show $ PP.plain err)

60 Right x -> return x

61 else do

62 putStrLn $ unwords [ "The presented iPKG file does not exist:", show fp]

src/Idris/Parser.hs+20−21

@@ -57,8 +57,7 @@ import Data.Ord

57import qualified Data.Text as T

58import qualified System.Directory as Dir (makeAbsolute)

59import System.FilePath

60−import Text.PrettyPrint.ANSI.Leijen (Doc, plain)

61−import qualified Text.PrettyPrint.ANSI.Leijen as ANSI

60+import qualified Text.PrettyPrint.ANSI.Leijen as PP

62import Text.Trifecta ((<?>))

61import Text.Trifecta ((<?>))

63import qualified Text.Trifecta as P

62import qualified Text.Trifecta as P

64import qualified Text.Trifecta.Delta as P

63import qualified Text.Trifecta.Delta as P

@@ -1478,19 +1477,19 @@ runElabDecl syn =

1478

1477

1479{- * Loading and parsing -}

1478{- * Loading and parsing -}

1480{-| Parses an expression from input -}

1479{-| Parses an expression from input -}

1481−parseExpr :: IState -> String -> Either P.ErrInfo PTerm

1480+parseExpr :: IState -> String -> Either ParseError PTerm

1482parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"

1481parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"

1483

1482

1484{-| Parses a constant form input -}

1483{-| Parses a constant form input -}

1485−parseConst :: IState -> String -> Either P.ErrInfo Const

1484+parseConst :: IState -> String -> Either ParseError Const

1486parseConst st = runparser (fmap fst constant) st "(input)"

1485parseConst st = runparser (fmap fst constant) st "(input)"

1487

1486

1488{-| Parses a tactic from input -}

1487{-| Parses a tactic from input -}

1489−parseTactic :: IState -> String -> Either P.ErrInfo PTactic

1488+parseTactic :: IState -> String -> Either ParseError PTactic

1490parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"

1489parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"

1491

1490

1492{-| Parses a do-step from input (used in the elab shell) -}

1491{-| Parses a do-step from input (used in the elab shell) -}

1493−parseElabShellStep :: IState -> String -> Either P.ErrInfo (Either ElabShellCmd PDo)

1492+parseElabShellStep :: IState -> String -> Either ParseError (Either ElabShellCmd PDo)

1494parseElabShellStep ist = runparser (Right <$> do_ defaultSyntax <|> Left <$> elabShellCmd) ist "(input)"

1493parseElabShellStep ist = runparser (Right <$> do_ defaultSyntax <|> Left <$> elabShellCmd) ist "(input)"

1495 where elabShellCmd = char ':' >>

1494 where elabShellCmd = char ':' >>

1496 (reserved "qed" >> pure EQED ) <|>

1495 (reserved "qed" >> pure EQED ) <|>

@@ -1553,8 +1552,8 @@ parseImports fname input

1553 shebang = string "#!" *> many (P.satisfy $ not . isEol) *> eol *> pure ()

1552 shebang = string "#!" *> many (P.satisfy $ not . isEol) *> eol *> pure ()

1554

1553

1555-- | There should be a better way of doing this...

1554-- | There should be a better way of doing this...

1556−findFC :: Doc -> (FC, String)

1555+findFC :: PP.Doc -> (FC, String)

1557−findFC x = let s = show (plain x) in findFC' s

1556+findFC x = let s = show (PP.plain x) in findFC' s

1558 where findFC' s = case span (/= ':') s of

1557 where findFC' s = case span (/= ':') s of

1559 -- Horrid kludge to prevent crashes on Windows

1558 -- Horrid kludge to prevent crashes on Windows

1560 (prefix, ':':'\\':rest) ->

1559 (prefix, ':':'\\':rest) ->

@@ -1568,8 +1567,8 @@ findFC x = let s = show (plain x) in findFC' s

1568 (FC failname pos pos, msg)

1567 (FC failname pos pos, msg)

1569

1568

1570-- | Check if the coloring matches the options and corrects if necessary

1569-- | Check if the coloring matches the options and corrects if necessary

1571−fixColour :: Bool -> ANSI.Doc -> ANSI.Doc

1570+fixColour :: Bool -> PP.Doc -> PP.Doc

1572−fixColour False doc = ANSI.plain doc

1571+fixColour False doc = PP.plain doc

1573fixColour True doc = doc

1572fixColour True doc = doc

1574

1573

1575-- | A program is a list of declarations, possibly with associated

1574-- | A program is a list of declarations, possibly with associated

@@ -1579,17 +1578,17 @@ parseProg :: SyntaxInfo -> FilePath -> String -> Maybe P.Delta ->

1579parseProg syn fname input mrk

1578parseProg syn fname input mrk

1580 = do i <- getIState

1579 = do i <- getIState

1581 case runparser mainProg i fname input of

1580 case runparser mainProg i fname input of

1582− Left (P.ErrInfo doc _) -> do -- FIXME: Get error location from trifecta

1581+ Left doc -> do -- FIXME: Get error location from trifecta

1583− -- this can't be the solution!

1582+ -- this can't be the solution!

1584− -- Issue #1575 on the issue tracker.

1583+ -- Issue #1575 on the issue tracker.

1585− -- https://github.com/idris-lang/Idris-dev/issues/1575

1584+ -- https://github.com/idris-lang/Idris-dev/issues/1575

1586− let (fc, msg) = findFC doc

1585+ let (fc, msg) = findFC doc

1587− i <- getIState

1586+ i <- getIState

1588− case idris_outputmode i of

1587+ case idris_outputmode i of

1589− RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)

1588+ RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)

1590− IdeMode n h -> iWarn fc (Util.Pretty.text msg)

1589+ IdeMode n h -> iWarn fc (Util.Pretty.text msg)

1591− putIState (i { errSpan = Just fc })

1590+ putIState (i { errSpan = Just fc })

1592− return []

1591+ return []

1593 Right (x, i) -> do putIState i

1592 Right (x, i) -> do putIState i

1594 reportParserWarnings

1593 reportParserWarnings

1595 return $ collect x

1594 return $ collect x

src/Idris/Parser/Helpers.hs+6−3

@@ -35,6 +35,7 @@ import qualified Text.Parser.Char as Chr

35import Text.Parser.LookAhead

36import qualified Text.Parser.Token as Tok

37import qualified Text.Parser.Token.Highlight as Hi

38+import qualified Text.PrettyPrint.ANSI.Leijen as PP

38import Text.Trifecta ((<?>))

39import Text.Trifecta ((<?>))

39import qualified Text.Trifecta as P

40import qualified Text.Trifecta as P

40import qualified Text.Trifecta.Delta as P

41import qualified Text.Trifecta.Delta as P

@@ -81,13 +82,15 @@ class HasLastTokenSpan m where

81instance HasLastTokenSpan IdrisParser where

82instance HasLastTokenSpan IdrisParser where

82 getLastTokenSpan = lastTokenSpan <$> get

83 getLastTokenSpan = lastTokenSpan <$> get

85+type ParseError = PP.Doc

86+

84-- | Helper to run Idris inner parser based stateT parsers

87-- | Helper to run Idris inner parser based stateT parsers

85−runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> Either P.ErrInfo res

88+runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> Either ParseError res

86runparser p i inputname s =

89runparser p i inputname s =

87 case P.parseString (runInnerParser (evalStateT p i))

90 case P.parseString (runInnerParser (evalStateT p i))

88 (P.Directed (UTF8.fromString inputname) 0 0 0 0) s of

91 (P.Directed (UTF8.fromString inputname) 0 0 0 0) s of

89− P.Failure errInfo -> Left errInfo

92+ P.Failure (P.ErrInfo doc _) -> Left doc

90− P.Success result -> Right result

93+ P.Success value -> Right value

92highlightP :: FC -> OutputAnnotation -> IdrisParser ()

95highlightP :: FC -> OutputAnnotation -> IdrisParser ()

93highlightP fc annot = do ist <- get

96highlightP fc annot = do ist <- get

src/Idris/Prover.hs+2−2

@@ -318,7 +318,7 @@ elabloop info fn d prompt prf e prev h env

318 (d, prev', st, done, prf', env', res) <-

319 idrisCatch

320 (case cmd of

321− Left (P.ErrInfo err _) ->

321+ Left err ->

322 return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) $ err)

323 Right (Left cmd') ->

324 case cmd' of

@@ -434,7 +434,7 @@ ploop fn d prompt prf e h

434 _ -> return ()

435 (d, st, done, prf', res) <- idrisCatch

436 (case cmd of

437− Left (P.ErrInfo err _) -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)

437+ Left err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)

438 Right Undo -> do (_, st) <- elabStep e loadState

439 return (True, st, False, init prf, Right $ iPrintResult "")

440 Right ProofState -> return (True, e, False, prf, Right $ iPrintResult "")

src/Idris/REPL.hs+3−4

@@ -93,7 +93,6 @@ import System.FSNotify (watchDir, withManager)

93import System.FSNotify.Devel (allEvents, doAllEvents)

94import System.IO

95import System.Process

96−import qualified Text.Trifecta.Result as P

97import Util.DynamicLinker

96import Util.DynamicLinker

98import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)

97import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)

99import Util.Pretty hiding ((</>))

98import Util.Pretty hiding ((</>))

@@ -177,7 +176,7 @@ processNetCmd :: IState -> IState -> Handle -> FilePath -> String ->

177 IO (IState, FilePath)

176 IO (IState, FilePath)

178processNetCmd orig i h fn cmd

177processNetCmd orig i h fn cmd

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

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

180− Left (P.ErrInfo err _) -> return (Left (Msg " invalid command"))

179+ Left err -> return (Left (Msg " invalid command"))

181 Right (Right c) -> runExceptT $ evalStateT (processNet fn c) i

180 Right (Right c) -> runExceptT $ evalStateT (processNet fn c) i

182 Right (Left err) -> return (Left (Msg err))

181 Right (Left err) -> return (Left (Msg err))

183 case res of

182 case res of

@@ -295,7 +294,7 @@ runIdeModeCommand h id orig fn mods (IdeMode.Interpret cmd) =

295 do c <- colourise

294 do c <- colourise

296 i <- getIState

295 i <- getIState

297 case parseCmd i "(input)" cmd of

296 case parseCmd i "(input)" cmd of

298− Left (P.ErrInfo err _) -> iPrintError $ show (fixColour False err)

297+ Left err -> iPrintError $ show (fixColour False err)

299 Right (Right (Prove mode n')) ->

298 Right (Right (Prove mode n')) ->

300 idrisCatch

299 idrisCatch

301 (do process fn (Prove mode n')

300 (do process fn (Prove mode n')

@@ -727,7 +726,7 @@ processInput cmd orig inputs efile

727 let fn = fromMaybe "" (listToMaybe inputs)

726 let fn = fromMaybe "" (listToMaybe inputs)

728 c <- colourise

727 c <- colourise

729 case parseCmd i "(input)" cmd of

728 case parseCmd i "(input)" cmd of

730− Left (P.ErrInfo err _) -> Just inputs <$ iputStrLn (show (fixColour c err))

729+ Left err -> Just inputs <$ iputStrLn (show (fixColour c err))

731 Right (Right Reload) ->

730 Right (Right Reload) ->

732 reload orig inputs

731 reload orig inputs

733 Right (Right Watch) ->

732 Right (Right Watch) ->

src/Idris/REPL/Parser.hs+1−1

@@ -35,7 +35,7 @@ import Text.Parser.Char (anyChar, oneOf)

35import Text.Parser.Combinators

36import qualified Text.Trifecta as P

38−parseCmd :: IState -> String -> String -> Either P.ErrInfo (Either String Command)

38+parseCmd :: IState -> String -> String -> Either IP.ParseError (Either String Command)

39parseCmd i inputname = IP.runparser pCmd i inputname . trim

40 where trim = f . f

41 where f = reverse . dropWhile isSpace