e680962 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Return parse results using Either

e680962Jason Felice9 years ago

src/Idris/Main.hs+18−18

compare with master

unifiedsplit

@@ -196,9 +196,9 @@ idrisMain opts =

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

197 c <- colourise

198 case parseExpr ist str of

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

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

200− runIO $ exitWith (ExitFailure 1)

200+ runIO $ exitWith (ExitFailure 1)

201− P.Success e -> process "" (Eval e))

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

202 exprs

203 runIO exitSuccess

204

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

273execScript expr = do i <- getIState

274 c <- colourise

275 case parseExpr i expr of

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

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

277− runIO $ exitWith (ExitFailure 1)

277+ runIO $ exitWith (ExitFailure 1)

278− P.Success term -> do ctxt <- getContext

278+ Right term -> do ctxt <- getContext

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

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

280− res <- execute tm

280+ res <- execute tm

281− runIO $ exitSuccess

281+ runIO $ exitSuccess

282

283-- | Run the initialisation script

284initScript :: Idris ()

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

300 runInit h

301 processLine i cmd input clr =

302 case parseCmd i input cmd of

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

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

304− P.Success (Right Reload) -> iPrintError "Init scripts cannot reload the file"

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

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

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

306− P.Success (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"

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

307− P.Success (Right Edit) -> iPrintError "Init scripts cannot invoke the editor"

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

308− P.Success (Right Proofs) -> proofs i

308+ Right (Right Proofs) -> proofs i

309− P.Success (Right Quit) -> iPrintError "Init scripts cannot quit Idris"

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

310− P.Success (Right cmd ) -> process [] cmd

310+ Right (Right cmd ) -> process [] cmd

311− P.Success (Left err) -> runIO $ print err

311+ Right (Left err) -> runIO $ print err

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

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

56 then do

57 p <- readFile fp

58 case runparser pPkg defaultPkg fp p of

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

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

60− P.Success x -> return x

60+ Right x -> return x

61 else do

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

63 exitWith (ExitFailure 1)

src/Idris/Parser.hs+9−9

@@ -1478,20 +1478,20 @@ runElabDecl syn =

1478

1479{- * Loading and parsing -}

1480{-| Parses an expression from input -}

1481−parseExpr :: IState -> String -> P.Result PTerm

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

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

1483

1484{-| Parses a constant form input -}

1485−parseConst :: IState -> String -> P.Result Const

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

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

1487

1488{-| Parses a tactic from input -}

1489−parseTactic :: IState -> String -> P.Result PTactic

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

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

1491

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

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

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

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

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

1495 where elabShellCmd = char ':' >>

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

1497 (reserved "abandon" >> pure EAbandon ) <|>

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

1579parseProg syn fname input mrk

1580 = do i <- getIState

1581 case runparser mainProg i fname input of

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

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

@@ -1590,9 +1590,9 @@ parseProg syn fname input mrk

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

1591 putIState (i { errSpan = Just fc })

1592 return []

1593− P.Success (x, i) -> do putIState i

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

1594− reportParserWarnings

1594+ reportParserWarnings

1595− return $ collect x

1595+ return $ collect x

1596 where mainProg :: IdrisParser ([PDecl], IState)

1597 mainProg = case mrk of

1598 Nothing -> do i <- get; return ([], i)

src/Idris/Parser/Expr.hs+2−4

@@ -18,6 +18,7 @@ import Idris.Parser.Ops

19import Prelude hiding (pi)

21+import Control.Arrow (left)

21import Control.Applicative

22import Control.Applicative

22import Control.Monad

23import Control.Monad

23import Control.Monad.State.Strict

24import Control.Monad.State.Strict

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

58 return $ debindApp syn (desugar syn i x)

59 return $ debindApp syn (desugar syn i x)

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

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

61−tryFullExpr syn st input =

62− case runparser (fullExpr syn) st "" input of

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

63− P.Success tm -> Right tm

64− P.Failure e -> Left (Msg (show e))

66{- | Parses an expression

64{- | Parses an expression

67@

65@

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

@@ -82,10 +82,12 @@ instance HasLastTokenSpan IdrisParser where

82 getLastTokenSpan = lastTokenSpan <$> get

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

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

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

86−runparser p i inputname =

86+runparser p i inputname s =

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

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

88− (P.Directed (UTF8.fromString inputname) 0 0 0 0)

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

89+ P.Failure errInfo -> Left errInfo

90+ P.Success result -> Right result

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

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

91highlightP fc annot = do ist <- get

93highlightP fc annot = do ist <- get

src/Idris/Prover.hs+22−22

@@ -312,15 +312,15 @@ elabloop info fn d prompt prf e prev h env

312

313 -- if we're abandoning, it has to be outside the scope of the catch

314 case cmd of

315− P.Success (Left EAbandon) -> do iPrintError ""; ifail "Abandoned"

315+ Right (Left EAbandon) -> do iPrintError ""; ifail "Abandoned"

316 _ -> return ()

317

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

319 idrisCatch

320 (case cmd of

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

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

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

323− P.Success (Left cmd') ->

323+ Right (Left cmd') ->

324 case cmd' of

325 EQED -> do hs <- lifte e get_holes

326 unless (null hs) $ ifail "Incomplete proof"

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

345 return (d', prev, st', done, prf', env, go)

346 EDocStr d -> do (d', st', done, prf', go) <- docStr e prf d

347 return (d', prev, st', done, prf', env, go)

348− P.Success (Right cmd') ->

348+ Right (Right cmd') ->

349 case cmd' of

350 DoLetP {} -> ifail "Pattern-matching let not supported here"

351 DoRewrite {} -> ifail "Pattern-matching do-rewrite not supported here"

@@ -430,27 +430,27 @@ ploop fn d prompt prf e h

430 Nothing -> do iPrintError ""; ifail "Abandoned"

431 Just input -> return (parseTactic i input, input)

432 case cmd of

433− P.Success Abandon -> do iPrintError ""; ifail "Abandoned"

433+ Right Abandon -> do iPrintError ""; ifail "Abandoned"

434 _ -> return ()

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

436 (case cmd of

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

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

438− P.Success Undo -> do (_, st) <- elabStep e loadState

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

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

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

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

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

441− P.Success ProofTerm -> do tm <- lifte e get_term

441+ Right ProofTerm -> do tm <- lifte e get_term

442− iputStrLn $ "TT: " ++ show tm ++ "\n"

442+ iputStrLn $ "TT: " ++ show tm ++ "\n"

443− return (False, e, False, prf, Right $ iPrintResult "")

443+ return (False, e, False, prf, Right $ iPrintResult "")

444− P.Success Qed -> do hs <- lifte e get_holes

444+ Right Qed -> do hs <- lifte e get_holes

445− unless (null hs) $ ifail "Incomplete proof"

445+ unless (null hs) $ ifail "Incomplete proof"

446− iputStrLn "Proof completed!"

446+ iputStrLn "Proof completed!"

447− return (False, e, True, prf, Right $ iPrintResult "")

447+ return (False, e, True, prf, Right $ iPrintResult "")

448− P.Success (TCheck (PRef _ _ n)) -> checkNameType e prf n

448+ Right (TCheck (PRef _ _ n)) -> checkNameType e prf n

449− P.Success (TCheck t) -> checkType e prf t

449+ Right (TCheck t) -> checkType e prf t

450− P.Success (TEval t) -> evalTerm e prf t

450+ Right (TEval t) -> evalTerm e prf t

451− P.Success (TDocStr x) -> docStr e prf x

451+ Right (TDocStr x) -> docStr e prf x

452− P.Success (TSearch t) -> search e prf t

452+ Right (TSearch t) -> search e prf t

453− P.Success tac ->

453+ Right tac ->

454 do (_, e) <- elabStep e saveState

455 (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac)

456 return (True, st, False, prf ++ [step], Right $ iPrintResult ""))

src/Idris/REPL.hs+22−22

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

177 IO (IState, FilePath)

178processNetCmd orig i h fn cmd

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

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

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

181− P.Success (Right c) -> runExceptT $ evalStateT (processNet fn c) i

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

182− P.Success (Left err) -> return (Left (Msg err))

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

183 case res of

184 Right x -> return x

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

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

295 do c <- colourise

296 i <- getIState

297 case parseCmd i "(input)" cmd of

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

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

299− P.Success (Right (Prove mode n')) ->

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

300 idrisCatch

301 (do process fn (Prove mode n')

302 isetPrompt (mkPrompt mods)

@@ -315,10 +315,10 @@ runIdeModeCommand h id orig fn mods (IdeMode.Interpret cmd) =

315 IdeMode.convSExp "abandon-proof" "Abandoned" n

316 _ -> return ()

317 iRenderError $ pprintErr ist e)

318− P.Success (Right cmd) -> idrisCatch

318+ Right (Right cmd) -> idrisCatch

319 (idemodeProcess fn cmd)

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

321− P.Success (Left err) -> iPrintError err

321+ Right (Left err) -> iPrintError err

322runIdeModeCommand h id orig fn mods (IdeMode.REPLCompletions str) =

323 do (unused, compls) <- replCompletion (reverse str, "")

324 let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok",

@@ -353,8 +353,8 @@ runIdeModeCommand h id orig fn mods (IdeMode.TypeOf name) =

353 (Check (PRef (FC "(idemode)" (0,0) (0,0)) [] n))

354runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name w) =

355 case parseConst orig name of

356− P.Success c -> process "(idemode)" (DocStr (Right c) (howMuch w))

356+ Right c -> process "(idemode)" (DocStr (Right c) (howMuch w))

357− P.Failure _ ->

357+ Left _ ->

358 case splitName name of

359 Left err -> iPrintError err

360 Right n -> process "(idemode)" (DocStr (Left n) (howMuch w))

@@ -727,10 +727,10 @@ processInput cmd orig inputs efile

727 let fn = fromMaybe "" (listToMaybe inputs)

728 c <- colourise

729 case parseCmd i "(input)" cmd of

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

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

731− P.Success (Right Reload) ->

731+ Right (Right Reload) ->

732 reload orig inputs

733− P.Success (Right Watch) ->

733+ Right (Right Watch) ->

734 if null inputs then

735 do iputStrLn "No loaded files to watch."

736 return (Just inputs)

@@ -738,7 +738,7 @@ processInput cmd orig inputs efile

738 do iputStrLn efile

739 iputStrLn $ "Watching for .idr changes in " ++ show inputs ++ ", press enter to cancel."

740 watch orig inputs

741− P.Success (Right (Load f toline)) ->

741+ Right (Right (Load f toline)) ->

742 -- The $!! here prevents a space leak on reloading.

743 -- This isn't a solution - but it's a temporary stopgap.

744 -- See issue #2386

@@ -748,20 +748,20 @@ processInput cmd orig inputs efile

748 clearErr

749 mod <- loadInputs [f] toline

750 return (Just mod)

751− P.Success (Right (ModImport f)) ->

751+ Right (Right (ModImport f)) ->

752 do clearErr

753 fmod <- loadModule f (IBC_REPL True)

754 return (Just (inputs ++ maybe [] (:[]) fmod))

755− P.Success (Right Edit) -> do -- takeMVar stvar

755+ Right (Right Edit) -> do -- takeMVar stvar

756 edit efile orig

757 return (Just inputs)

758− P.Success (Right Proofs) -> Just inputs <$ proofs orig

758+ Right (Right Proofs) -> Just inputs <$ proofs orig

759− P.Success (Right Quit) -> Nothing <$ when (not quiet) (iputStrLn "Bye bye")

759+ Right (Right Quit) -> Nothing <$ when (not quiet) (iputStrLn "Bye bye")

760− P.Success (Right cmd ) -> do idrisCatch (process fn cmd)

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

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

762− return (Just inputs)

762+ return (Just inputs)

763− P.Success (Left err) -> do runIO $ putStrLn err

763+ Right (Left err) -> do runIO $ putStrLn err

764− return (Just inputs)

764+ return (Just inputs)

765

766resolveProof :: Name -> Idris Name

767resolveProof n'

@@ -1426,7 +1426,7 @@ process fn (Browse ns) =

1426process fn (MakeDoc s) =

1427 do istate <- getIState

1428 let names = words s

1429− parse n | P.Success x <- runparser (fmap fst name) istate fn n = Right x

1429+ parse n | Right x <- runparser (fmap fst name) istate fn n = Right x

1430 parse n = Left n

1431 (bad, nss) = partitionEithers $ map parse names

1432 cd <- runIO getCurrentDirectory

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 -> P.Result (Either String Command)

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

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

40 where trim = f . f

41 where f = reverse . dropWhile isSpace