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

git.iko.soy/Idris-dev

Introduce ParseError type alias

commit5048ad4099f395464d3f6b7b82d86f374b6c0678 authorJason Felice <jason.m.felice@gmail.com> dateThu 26 Oct 2017, 15:42 (9 years ago) parente680962

7 files changed+38−38

compare with master

unifiedsplit

src/Idris/Main.hs+5−6 src/Idris/Package/Parser.hs+1−1 src/Idris/Parser.hs+20−21 src/Idris/Parser/Helpers.hs+6−3 src/Idris/Prover.hs+2−2 src/Idris/REPL.hs+3−4 src/Idris/REPL/Parser.hs+1−1

src/Idris/Main.hs+5−6

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

4747import System.FilePath

4848import System.IO

4949import System.IO.CodePage (withCP65001)

50−import qualified Text.Trifecta.Result as P

5150

5251-- | How to run Idris programs.

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

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

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

197196 c <- colourise

198197 case parseExpr ist str of

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

200− runIO $ exitWith (ExitFailure 1)

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

199+ runIO $ exitWith (ExitFailure 1)

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

202201 exprs

203202 runIO exitSuccess

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

273272execScript expr = do i <- getIState

274273 c <- colourise

275274 case parseExpr i expr of

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

277− runIO $ exitWith (ExitFailure 1)

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

276+ runIO $ exitWith (ExitFailure 1)

278277 Right term -> do ctxt <- getContext

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

280279 res <- execute tm

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

300299 runInit h

301300 processLine i cmd input clr =

302301 case parseCmd i input cmd of

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

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

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

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

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

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

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

5656 then do

5757 p <- readFile fp

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

6060 Right x -> return x

6161 else do

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

src/Idris/Parser.hs+20−21

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

5757import qualified Data.Text as T

5858import qualified System.Directory as Dir (makeAbsolute)

5959import 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

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

6362import qualified Text.Trifecta as P

6463import qualified Text.Trifecta.Delta as P

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

14781477

14791478{- * Loading and parsing -}

14801479{-| Parses an expression from input -}

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

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

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

14831482

14841483{-| Parses a constant form input -}

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

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

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

14871486

14881487{-| Parses a tactic from input -}

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

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

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

14911490

14921491{-| 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)

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

14951494 where elabShellCmd = char ':' >>

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

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

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

15541553

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

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

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

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

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

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

15591558 -- Horrid kludge to prevent crashes on Windows

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

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

15681567 (FC failname pos pos, msg)

15691568

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

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

1572−fixColour False doc = ANSI.plain doc

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

1571+fixColour False doc = PP.plain doc

15731572fixColour True doc = doc

15741573

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

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

15791578parseProg syn fname input mrk

15801579 = do i <- getIState

15811580 case runparser mainProg i fname input of

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

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

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

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

1586− let (fc, msg) = findFC doc

1587− i <- getIState

1588− case idris_outputmode i of

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

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

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

1592− return []

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

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

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

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

1585+ let (fc, msg) = findFC doc

1586+ i <- getIState

1587+ case idris_outputmode i of

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

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

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

1591+ return []

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

15941593 reportParserWarnings

15951594 return $ collect x

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

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

3535import Text.Parser.LookAhead

3636import qualified Text.Parser.Token as Tok

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

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

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

3940import qualified Text.Trifecta as P

4041import qualified Text.Trifecta.Delta as P

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

8182instance HasLastTokenSpan IdrisParser where

8283 getLastTokenSpan = lastTokenSpan <$> get

8384

85+type ParseError = PP.Doc

86+

8487-- | 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

8689runparser p i inputname s =

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

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

89− P.Failure errInfo -> Left errInfo

90− P.Success result -> Right result

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

93+ P.Success value -> Right value

9194

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

9396highlightP 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

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

319319 idrisCatch

320320 (case cmd of

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

321+ Left err ->

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

323323 Right (Left cmd') ->

324324 case cmd' of

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

434434 _ -> return ()

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

436436 (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)

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

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

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

src/Idris/REPL.hs+3−4

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

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

9494import System.IO

9595import System.Process

96−import qualified Text.Trifecta.Result as P

9796import Util.DynamicLinker

9897import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)

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

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

177176 IO (IState, FilePath)

178177processNetCmd orig i h fn cmd

179178 = 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"))

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

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

183182 case res of

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

295294 do c <- colourise

296295 i <- getIState

297296 case parseCmd i "(input)" cmd of

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

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

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

300299 idrisCatch

301300 (do process fn (Prove mode n')

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

727726 let fn = fromMaybe "" (listToMaybe inputs)

728727 c <- colourise

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

731730 Right (Right Reload) ->

732731 reload orig inputs

733732 Right (Right Watch) ->

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

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

3535import Text.Parser.Combinators

3636import qualified Text.Trifecta as P

3737

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

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

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

4040 where trim = f . f

4141 where f = reverse . dropWhile isSpace