dbbdbb2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #662 from hannesm/error-cleanup

Error cleanup

commitdbbdbb24a2ab195f01256024089439c864d3aa65 authorEdwin Brady <edwin.brady@gmail.com> dateSat 23 Nov 2013, 11:30 (13 years ago) parent1c19fcc 365d64f

5 files changed+108−96

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+7−16 src/Idris/ElabDecls.hs+1−5 src/Idris/Error.hs+8−3 src/Idris/Parser.hs+41−23 src/Idris/REPL.hs+51−49

src/Idris/AbsSyntax.hs+7−16

@@ -325,21 +325,12 @@ ihputStrLn :: Handle -> String -> Idris ()

325325ihputStrLn h s = do i <- getIState

326326 case idris_outputmode i of

327327 RawOutput -> runIO $ hPutStrLn h s

328− IdeSlave n ->

329− case span (/=':') s of

330− (fn, ':':rest) -> case span isDigit rest of

331− ([], ':':msg) -> write

332− ([], msg) -> write

333− (row, ':':rest') ->

334− case span isDigit rest' of

335− ([], msg) -> iWarn (FC fn (read row) 0) msg

336− (col, ':':msg) -> iWarn (FC fn (read row) (read col)) msg

337− _ -> write

338− where write = runIO . hPutStrLn h $ convSExp "write-string" s n

328+ IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n

339329

340330iputStrLn = ihputStrLn stdout

341331iPrintError = ihPrintError stdout

342332iPrintResult = ihPrintResult stdout

333+iWarn = ihWarn stdout

343334

344335ideslavePutSExp :: SExpable a => String -> a -> Idris ()

345336ideslavePutSExp cmd info = do i <- getIState

@@ -359,11 +350,11 @@ isetPrompt p = do i <- getIState

359350 case idris_outputmode i of

360351 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n

361352

362−iWarn :: FC -> String -> Idris ()

363−iWarn fc err = do i <- getIState

364− case idris_outputmode i of

365− RawOutput -> runIO $ putStrLn (show fc ++ ":" ++ err)

366− IdeSlave n -> runIO . putStrLn $ convSExp "warning" (fc_fname fc, fc_line fc, err) n

353+ihWarn :: Handle -> FC -> String -> Idris ()

354+ihWarn h fc err = do i <- getIState

355+ case idris_outputmode i of

356+ RawOutput -> runIO $ hPutStrLn h (show fc ++ ":" ++ err)

357+ IdeSlave n -> runIO $ hPutStrLn h $ convSExp "warning" (fc_fname fc, fc_line fc, err) n

367358

368359setLogLevel :: Int -> Idris ()

369360setLogLevel l = do i <- getIState

src/Idris/ElabDecls.hs+1−5

@@ -1612,11 +1612,7 @@ elabDecls info ds = do mapM_ (elabDecl EAll info) ds

16121612

16131613elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()

16141614elabDecl what info d

1615− = idrisCatch (elabDecl' what info d)

1616− (\e -> do setErrLine (getErrLine e)

1617− ist <- getIState

1618− let h = idris_outh ist

1619− ihputStrLn h $ pshow ist e)

1615+ = idrisCatch (elabDecl' what info d) (setAndReport)

16201616

16211617elabDecl' _ info (PFix _ _ _)

16221618 = return () -- nothing to elaborate

src/Idris/Error.hs+8−3

@@ -35,12 +35,17 @@ report e

3535 | isUserError e = ioeGetErrorString e

3636 | otherwise = show e

3737

38−--idrisCatch :: Idris a -> (SomeException -> Idris a) -> Idris a

39−--idrisCatch = catch

40−

4138idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a

4239idrisCatch = catchError

4340

41+setAndReport :: Err -> Idris ()

42+setAndReport e = do ist <- getIState

43+ let h = idris_outh ist

44+ case e of

45+ At fc@(FC f l c) e -> do setErrLine l

46+ ihWarn h fc $ pshow ist e

47+ _ -> do setErrLine (getErrLine e)

48+ ihputStrLn h $ pshow ist e

4449

4550ifail :: String -> Idris a

4651ifail = throwError . Msg

src/Idris/Parser.hs+41−23

@@ -15,6 +15,8 @@ import qualified Text.Parser.Token as Tok

1515import qualified Text.Parser.Char as Chr

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

1717

18+import Text.PrettyPrint.ANSI.Leijen (Doc, plain)

19+

1820import Idris.AbsSyntax

1921import Idris.DSL

2022import Idris.Imports

@@ -911,6 +913,13 @@ parseImports fname input

911913 i <- get

912914 return ((mname, ps, mrk'), i)

913915

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

917+findFC :: Doc -> (FC, String)

918+findFC x = let s = show (plain x) in

919+ case span (/= ':') s of

920+ (failname, ':':rest) -> case span isDigit rest of

921+ (line, ':':rest') -> (FC failname (read line) 0, drop 2 (dropWhile (/= ':') rest'))

922+

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

915924-- documentation strings.

916925parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->

@@ -919,10 +928,13 @@ parseProg syn fname input mrk

919928 = do i <- getIState

920929 case runparser mainProg i fname input of

921930 Failure doc -> do -- FIXME: Get error location from trifecta

922− --let errl = sourceLine (errorPos err)

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

932+ let (fc, msg) = findFC doc

923933 i <- getIState

924− ihputStrLn (idris_outh i) (show doc)

925− putIState (i { errLine = Just 0 }) -- Just errl })

934+ case idris_outputmode i of

935+ RawOutput -> ihputStrLn (idris_outh i) (show doc)

936+ IdeSlave n -> ihWarn (idris_outh i) fc msg

937+ putIState (i { errLine = Just (fc_line fc) }) -- Just errl })

926938 return []

927939 Success (x, i) -> do putIState i

928940 return $ collect x

@@ -935,34 +947,40 @@ parseProg syn fname input mrk

935947 i' <- get

936948 return (ds, i')

937949

938−{- | Load idris module -}

950+{- | Load idris module and show error if something wrong happens -}

939951loadModule :: Handle -> FilePath -> Idris String

940952loadModule outh f

941− = idrisCatch (do i <- getIState

942− let file = takeWhile (/= ' ') f

943− ibcsd <- valIBCSubDir i

944− ids <- allImportDirs

945− fp <- liftIO $ findImport ids ibcsd file

946− if file `elem` imported i

947− then iLOG $ "Already read " ++ file

948− else do putIState (i { imported = file : imported i })

949− case fp of

950− IDR fn -> loadSource outh False fn

951− LIDR fn -> loadSource outh True fn

952− IBC fn src ->

953− idrisCatch (loadIBC fn)

954− (\c -> do iLOG $ fn ++ " failed " ++ show c

955− case src of

956− IDR sfn -> loadSource outh False sfn

957− LIDR sfn -> loadSource outh True sfn)

958− let (dir, fh) = splitFileName file

959− return (dropExtension fh))

953+ = idrisCatch (loadModule' outh f)

960954 (\e -> do setErrLine (getErrLine e)

961955 ist <- getIState

962956 msg <- showErr e

963957 ihputStrLn outh msg

964958 return "")

965959

960+{- | Load idris module -}

961+loadModule' :: Handle -> FilePath -> Idris String

962+loadModule' outh f

963+ = do i <- getIState

964+ let file = takeWhile (/= ' ') f

965+ ibcsd <- valIBCSubDir i

966+ ids <- allImportDirs

967+ fp <- liftIO $ findImport ids ibcsd file

968+ if file `elem` imported i

969+ then iLOG $ "Already read " ++ file

970+ else do putIState (i { imported = file : imported i })

971+ case fp of

972+ IDR fn -> loadSource outh False fn

973+ LIDR fn -> loadSource outh True fn

974+ IBC fn src ->

975+ idrisCatch (loadIBC fn)

976+ (\c -> do iLOG $ fn ++ " failed " ++ show c

977+ case src of

978+ IDR sfn -> loadSource outh False sfn

979+ LIDR sfn -> loadSource outh True sfn)

980+ let (dir, fh) = splitFileName file

981+ return (dropExtension fh)

982+

983+

966984{- | Load idris code from file -}

967985loadFromIFile :: Handle -> IFileType -> Idris ()

968986loadFromIFile h i@(IBC fn src)

src/Idris/REPL.hs+51−49

@@ -199,55 +199,57 @@ ideslave orig mods

199199 Right (sexp, id) -> return (sexp, id)

200200 i <- getIState

201201 putIState $ i { idris_outputmode = (IdeSlave id) }

202− let fn = case mods of

203− (f:_) -> f

204− _ -> ""

205− case IdeSlave.sexpToCommand sexp of

206− Just (IdeSlave.Interpret cmd) ->

207− do c <- colourise

208− case parseCmd i "(input)" cmd of

209− Failure err -> iPrintError $ show (fixColour c err)

210− Success (Prove n') -> do iPrintResult ""

211− idrisCatch

212− (process stdout fn (Prove n'))

213− (\e -> getIState >>= iPrintError . flip pshow e)

214− isetPrompt (mkPrompt mods)

215− Success cmd -> idrisCatch

216− (ideslaveProcess fn cmd)

217− (\e -> getIState >>= iPrintError . flip pshow e)

218− Just (IdeSlave.REPLCompletions str) ->

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

220− let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok", IdeSlave.toSExp (map replacement compls, reverse unused)]

221− runIO $ putStrLn $ IdeSlave.convSExp "return" good id

222− Just (IdeSlave.LoadFile filename) ->

223− do clearErr

224− putIState (orig { idris_options = idris_options i,

225− idris_outputmode = (IdeSlave id) })

226− loadModule stdout filename

227− iucheck

228− isetPrompt (mkPrompt [filename])

229−

230− -- Report either success or failure

231− i <- getIState

232− case (errLine i) of

233− Nothing -> iPrintResult $ "loaded " ++ filename

234− Just x -> iPrintError $ "didn't load " ++ filename

235− ideslave orig [filename]

236− Just (IdeSlave.TypeOf name) ->

237− process stdout "(ideslave)" (Check (PRef (FC "(ideslave)" 0 0) (UN name)))

238− Just (IdeSlave.CaseSplit line name) ->

239− process stdout fn (CaseSplitAt False line (UN name))

240− Just (IdeSlave.AddClause line name) ->

241− process stdout fn (AddClauseFrom False line (UN name))

242− Just (IdeSlave.AddProofClause line name) ->

243− process stdout fn (AddProofClauseFrom False line (UN name))

244− Just (IdeSlave.AddMissing line name) ->

245− process stdout fn (AddMissing False line (UN name))

246− Just (IdeSlave.MakeWithBlock line name) ->

247− process stdout fn (MakeWith False line (UN name))

248− Just (IdeSlave.ProofSearch line name hints) ->

249− process stdout fn (DoProofSearch False line (UN name) (map UN hints))

250− Nothing -> do iPrintError "did not understand")

202+ idrisCatch -- to report correct id back!

203+ (do let fn = case mods of

204+ (f:_) -> f

205+ _ -> ""

206+ case IdeSlave.sexpToCommand sexp of

207+ Just (IdeSlave.Interpret cmd) ->

208+ do c <- colourise

209+ case parseCmd i "(input)" cmd of

210+ Failure err -> iPrintError $ show (fixColour c err)

211+ Success (Prove n') -> do iPrintResult ""

212+ idrisCatch

213+ (process stdout fn (Prove n'))

214+ (\e -> getIState >>= iPrintError . flip pshow e)

215+ isetPrompt (mkPrompt mods)

216+ Success cmd -> idrisCatch

217+ (ideslaveProcess fn cmd)

218+ (\e -> getIState >>= iPrintError . flip pshow e)

219+ Just (IdeSlave.REPLCompletions str) ->

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

221+ let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok", IdeSlave.toSExp (map replacement compls, reverse unused)]

222+ runIO $ putStrLn $ IdeSlave.convSExp "return" good id

223+ Just (IdeSlave.LoadFile filename) ->

224+ do clearErr

225+ putIState (orig { idris_options = idris_options i,

226+ idris_outputmode = (IdeSlave id) })

227+ idrisCatch (do mod <- loadModule' stdout filename

228+ return ())

229+ (setAndReport)

230+ isetPrompt (mkPrompt [filename])

231+ -- Report either success or failure

232+ i <- getIState

233+ case (errLine i) of

234+ Nothing -> iPrintResult $ "loaded " ++ filename

235+ Just x -> iPrintError $ "didn't load " ++ filename

236+ ideslave orig [filename]

237+ Just (IdeSlave.TypeOf name) ->

238+ process stdout "(ideslave)" (Check (PRef (FC "(ideslave)" 0 0) (UN name)))

239+ Just (IdeSlave.CaseSplit line name) ->

240+ process stdout fn (CaseSplitAt False line (UN name))

241+ Just (IdeSlave.AddClause line name) ->

242+ process stdout fn (AddClauseFrom False line (UN name))

243+ Just (IdeSlave.AddProofClause line name) ->

244+ process stdout fn (AddProofClauseFrom False line (UN name))

245+ Just (IdeSlave.AddMissing line name) ->

246+ process stdout fn (AddMissing False line (UN name))

247+ Just (IdeSlave.MakeWithBlock line name) ->

248+ process stdout fn (MakeWith False line (UN name))

249+ Just (IdeSlave.ProofSearch line name hints) ->

250+ process stdout fn (DoProofSearch False line (UN name) (map UN hints))

251+ Nothing -> do iPrintError "did not understand")

252+ (\e -> do iPrintError $ show e))

251253 (\e -> do iPrintError $ show e)

252254 ideslave orig mods

253255