22587b2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Make ParseError a newtype

commit22587b2ad3a45aa01e219bf153e77b3ebffe3bab authorJason Felice <jason.m.felice@gmail.com> dateThu 26 Oct 2017, 15:57 (9 years ago) parent5048ad4

8 files changed+17−16

compare with master

unifiedsplit

src/Idris/Main.hs+4−3 src/Idris/Package/Parser.hs+1−1 src/Idris/Parser.hs+3−3 src/Idris/Parser/Expr.hs+1−1 src/Idris/Parser/Helpers.hs+2−2 src/Idris/Prover.hs+3−3 src/Idris/REPL.hs+3−2 src/Idris/REPL/Parser.hs−1

src/Idris/Main.hs+4−3

@@ -25,6 +25,7 @@ import Idris.ModeCommon

2525import Idris.Options

2626import Idris.Output

2727import Idris.Parser hiding (indent)

28+import Idris.Parser.Helpers (parseErrorDoc)

2829import Idris.REPL

2930import Idris.REPL.Commands

3031import Idris.REPL.Parser

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

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

196197 c <- colourise

197198 case parseExpr ist str of

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

199+ Left err -> do iputStrLn . show . fixColour c . parseErrorDoc $ err

199200 runIO $ exitWith (ExitFailure 1)

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

201202 exprs

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

272273execScript expr = do i <- getIState

273274 c <- colourise

274275 case parseExpr i expr of

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

276+ Left err -> do iputStrLn . show . fixColour c . parseErrorDoc $ err

276277 runIO $ exitWith (ExitFailure 1)

277278 Right term -> do ctxt <- getContext

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

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

299300 runInit h

300301 processLine i cmd input clr =

301302 case parseCmd i input cmd of

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

303+ Left err -> runIO . print . fixColour clr . parseErrorDoc $ err

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

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

305306 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 err -> fail (show $ PP.plain err)

59+ Left err -> fail (show $ PP.plain $ parseErrorDoc 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+3−3

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

15781578parseProg syn fname input mrk

15791579 = do i <- getIState

15801580 case runparser mainProg i fname input of

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

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

15821582 -- this can't be the solution!

15831583 -- Issue #1575 on the issue tracker.

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

1585− let (fc, msg) = findFC doc

1585+ let (fc, msg) = findFC $ parseErrorDoc err

15861586 i <- getIState

15871587 case idris_outputmode i of

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

1588+ RawOutput h -> iputStrLn (show . fixColour (idris_colourRepl i) . parseErrorDoc $ err)

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

15901590 putIState (i { errSpan = Just fc })

15911591 return []

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

@@ -59,7 +59,7 @@ fullExpr syn = do x <- expr syn

5959 return $ debindApp syn (desugar syn i x)

6060

6161tryFullExpr :: SyntaxInfo -> IState -> String -> Either Err PTerm

62−tryFullExpr syn st = left (Msg . show) . runparser (fullExpr syn) st ""

62+tryFullExpr syn st = left (Msg . show . parseErrorDoc) . runparser (fullExpr syn) st ""

6363

6464{- | Parses an expression

6565@

src/Idris/Parser/Helpers.hs+2−2

@@ -82,14 +82,14 @@ class HasLastTokenSpan m where

8282instance HasLastTokenSpan IdrisParser where

8383 getLastTokenSpan = lastTokenSpan <$> get

8484

85−type ParseError = PP.Doc

85+newtype ParseError = ParseError { parseErrorDoc :: PP.Doc }

8686

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

8888runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> Either ParseError res

8989runparser p i inputname s =

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

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

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

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

9393 P.Success value -> Right value

9494

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

src/Idris/Prover.hs+3−3

@@ -34,6 +34,7 @@ import qualified Idris.IdeMode as IdeMode

3434import Idris.Options

3535import Idris.Output

3636import Idris.Parser hiding (params)

37+import Idris.Parser.Helpers (parseErrorDoc)

3738import Idris.TypeSearch (searchByType)

3839

3940import Util.Pretty

@@ -43,7 +44,6 @@ import Control.Monad.State.Strict

4344import System.Console.Haskeline

4445import System.Console.Haskeline.History

4546import System.IO (Handle, hPutStrLn, stdin, stdout)

46−import qualified Text.Trifecta.Result as P

4747

4848-- | Launch the proof shell

4949prover :: ElabInfo -> Bool -> Bool -> Name -> Idris ()

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

319319 idrisCatch

320320 (case cmd of

321321 Left err ->

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

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

323323 Right (Left cmd') ->

324324 case cmd' of

325325 EQED -> do hs <- lifte e get_holes

@@ -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 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) . parseErrorDoc $ 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−2

@@ -72,6 +72,7 @@ import Idris.ModeCommon

7272import Idris.Options

7373import Idris.Output

7474import Idris.Parser hiding (indent)

75+import Idris.Parser.Helpers (parseErrorDoc)

7576import Idris.Prover

7677import Idris.REPL.Browse (namesInNS, namespacesInNS)

7778import Idris.REPL.Commands

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

294295 do c <- colourise

295296 i <- getIState

296297 case parseCmd i "(input)" cmd of

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

298+ Left err -> iPrintError . show . fixColour False . parseErrorDoc $ err

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

299300 idrisCatch

300301 (do process fn (Prove mode n')

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

726727 let fn = fromMaybe "" (listToMaybe inputs)

727728 c <- colourise

728729 case parseCmd i "(input)" cmd of

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

730+ Left err -> Just inputs <$ iputStrLn (show . fixColour c . parseErrorDoc $ err)

730731 Right (Right Reload) ->

731732 reload orig inputs

732733 Right (Right Watch) ->

src/Idris/REPL/Parser.hs−1

@@ -33,7 +33,6 @@ import System.Console.ANSI (Color(..))

3333import System.FilePath ((</>))

3434import Text.Parser.Char (anyChar, oneOf)

3535import Text.Parser.Combinators

36−import qualified Text.Trifecta as P

3736

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

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