e680962 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Return parse results using Either

commite6809620f6d917799cd26eba0c70038a15b3cea3 authorJason Felice <jason.m.felice@gmail.com> dateThu 26 Oct 2017, 15:21 (9 years ago) parent1f8db23

8 files changed+82−82

compare with master

unifiedsplit

src/Idris/Main.hs+18−18 src/Idris/Package/Parser.hs+2−2 src/Idris/Parser.hs+9−9 src/Idris/Parser/Expr.hs+2−4 src/Idris/Parser/Helpers.hs+6−4 src/Idris/Prover.hs+22−22 src/Idris/REPL.hs+22−22 src/Idris/REPL/Parser.hs+1−1

src/Idris/Main.hs+18−18

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

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

197197 c <- colourise

198198 case parseExpr ist str of

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

200− runIO $ exitWith (ExitFailure 1)

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

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

200+ runIO $ exitWith (ExitFailure 1)

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

202202 exprs

203203 runIO exitSuccess

204204

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

273273execScript expr = do i <- getIState

274274 c <- colourise

275275 case parseExpr i expr of

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

277− runIO $ exitWith (ExitFailure 1)

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

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

280− res <- execute tm

281− runIO $ exitSuccess

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

277+ runIO $ exitWith (ExitFailure 1)

278+ Right term -> do ctxt <- getContext

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

280+ res <- execute tm

281+ runIO $ exitSuccess

282282

283283-- | Run the initialisation script

284284initScript :: Idris ()

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

300300 runInit h

301301 processLine i cmd input clr =

302302 case parseCmd i input cmd of

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

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

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

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

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

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

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

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

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

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

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

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

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

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

308+ Right (Right Proofs) -> proofs i

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

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

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

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

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

5656 then do

5757 p <- readFile fp

5858 case runparser pPkg defaultPkg fp p of

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

60− P.Success x -> return x

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

60+ Right x -> return x

6161 else do

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

6363 exitWith (ExitFailure 1)

src/Idris/Parser.hs+9−9

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

14781478

14791479{- * Loading and parsing -}

14801480{-| Parses an expression from input -}

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

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

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

14831483

14841484{-| Parses a constant form input -}

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

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

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

14871487

14881488{-| Parses a tactic from input -}

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

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

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

14911491

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

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

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

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

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

14951495 where elabShellCmd = char ':' >>

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

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

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

15791579parseProg syn fname input mrk

15801580 = do i <- getIState

15811581 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

15831583 -- this can't be the solution!

15841584 -- Issue #1575 on the issue tracker.

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

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

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

15911591 putIState (i { errSpan = Just fc })

15921592 return []

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

1594− reportParserWarnings

1595− return $ collect x

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

1594+ reportParserWarnings

1595+ return $ collect x

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

15971597 mainProg = case mrk of

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

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

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

1818

1919import Prelude hiding (pi)

2020

21+import Control.Arrow (left)

2122import Control.Applicative

2223import Control.Monad

2324import Control.Monad.State.Strict

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

5859 return $ debindApp syn (desugar syn i x)

5960

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

61−tryFullExpr syn st input =

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

63− P.Success tm -> Right tm

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

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

6563

6664{- | Parses an expression

6765@

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

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

8282 getLastTokenSpan = lastTokenSpan <$> get

8383

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

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

86−runparser p i inputname =

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

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

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

86+runparser p i inputname s =

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

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

89+ P.Failure errInfo -> Left errInfo

90+ P.Success result -> Right result

8991

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

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

312312

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

314314 case cmd of

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

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

316316 _ -> return ()

317317

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

319319 idrisCatch

320320 (case cmd of

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

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

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

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

323+ Right (Left cmd') ->

324324 case cmd' of

325325 EQED -> do hs <- lifte e get_holes

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

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

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

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

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

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

348+ Right (Right cmd') ->

349349 case cmd' of

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

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

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

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

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

432432 case cmd of

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

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

434434 _ -> return ()

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

436436 (case cmd of

437− P.Failure (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

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

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

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

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

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

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

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

446− iputStrLn "Proof completed!"

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

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

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

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

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

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

453− P.Success tac ->

437+ Left (P.ErrInfo 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 "")

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

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

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

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

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

446+ iputStrLn "Proof completed!"

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

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

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

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

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

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

453+ Right tac ->

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

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

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

src/Idris/REPL.hs+22−22

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

177177 IO (IState, FilePath)

178178processNetCmd orig i h fn cmd

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

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

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

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

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

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

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

183183 case res of

184184 Right x -> return x

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

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

295295 do c <- colourise

296296 i <- getIState

297297 case parseCmd i "(input)" cmd of

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

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

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

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

300300 idrisCatch

301301 (do process fn (Prove mode n')

302302 isetPrompt (mkPrompt mods)

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

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

316316 _ -> return ()

317317 iRenderError $ pprintErr ist e)

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

318+ Right (Right cmd) -> idrisCatch

319319 (idemodeProcess fn cmd)

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

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

321+ Right (Left err) -> iPrintError err

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

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

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

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

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

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

355355 case parseConst orig name of

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

357− P.Failure _ ->

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

357+ Left _ ->

358358 case splitName name of

359359 Left err -> iPrintError err

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

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

727727 let fn = fromMaybe "" (listToMaybe inputs)

728728 c <- colourise

729729 case parseCmd i "(input)" cmd of

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

731− P.Success (Right Reload) ->

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

731+ Right (Right Reload) ->

732732 reload orig inputs

733− P.Success (Right Watch) ->

733+ Right (Right Watch) ->

734734 if null inputs then

735735 do iputStrLn "No loaded files to watch."

736736 return (Just inputs)

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

738738 do iputStrLn efile

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

740740 watch orig inputs

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

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

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

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

744744 -- See issue #2386

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

748748 clearErr

749749 mod <- loadInputs [f] toline

750750 return (Just mod)

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

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

752752 do clearErr

753753 fmod <- loadModule f (IBC_REPL True)

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

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

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

756756 edit efile orig

757757 return (Just inputs)

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

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

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

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

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

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

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

762− return (Just inputs)

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

764− return (Just inputs)

762+ return (Just inputs)

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

764+ return (Just inputs)

765765

766766resolveProof :: Name -> Idris Name

767767resolveProof n'

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

14261426process fn (MakeDoc s) =

14271427 do istate <- getIState

14281428 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

14301430 parse n = Left n

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

14321432 cd <- runIO getCurrentDirectory

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

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

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

4040 where trim = f . f

4141 where f = reverse . dropWhile isSpace