c733a8f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Parser warnings; especially for invalid doc comments

This patch adds: * A facility for non-fatal parser warnings * A convenient way to add specific warnings for invalid documentation comments * Warnings for module doc comments (which are not currently supported)

commitc733a8f556e7477fb7ce2f537bb6645dffc577b8 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSat 22 Feb 2014, 09:55 (13 years ago) parentecfb293

5 files changed+38−9

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/Chaser.hs+2 src/Idris/ParseExpr.hs+4−4 src/Idris/ParseHelpers.hs+25−1 src/Idris/Parser.hs+5−3

src/Idris/AbsSyntaxTree.hs+2−1

@@ -133,6 +133,7 @@ data IState = IState {

133133 idris_hdrs :: [(Codegen, String)],

134134 proof_list :: [(Name, [String])],

135135 errLine :: Maybe Int,

136+ parserWarnings :: [(FC, Err)],

136137 lastParse :: Maybe Name,

137138 indent_stack :: [Int],

138139 brace_stack :: [Maybe Int],

@@ -219,7 +220,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

219220 emptyContext emptyContext emptyContext emptyContext

220221 emptyContext emptyContext

221222 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

222− [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

223+ [] Nothing [] Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

223224 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

224225 AutomaticWidth

225226

src/Idris/Chaser.hs+2

@@ -132,6 +132,8 @@ buildTree built fp = btree [] fp

132132 file_in <- runIO $ readFile f

133133 file <- if lit then tclift $ unlit f file_in else return file_in

134134 (_, modules, _) <- parseImports f file

135+ -- The chaser should never report warnings from sub-modules

136+ clearParserWarnings

135137 ms <- mapM (btree done) [realName | (realName, alias, fc) <- modules]

136138 return (concat ms)

137139 else return [] -- IBC with no source available

src/Idris/ParseExpr.hs+4−4

@@ -78,8 +78,8 @@ expr' syn = doexpr' syn

7878

7979doexpr' :: SyntaxInfo -> IdrisParser PTerm

8080doexpr' syn = try (externalExpr syn)

81− <|> internalExpr syn

82− <?> "expression"

81+ <|> internalExpr syn

82+ <?> "expression"

8383

8484{- | Parses a user-defined expression -}

8585externalExpr :: SyntaxInfo -> IdrisParser PTerm

@@ -204,7 +204,7 @@ internalExpr syn =

204204 <|> quoteGoal syn

205205 <|> let_ syn

206206 <|> rewriteTerm syn

207− <|> try(pi syn)

207+ <|> try (pi syn)

208208 <|> doBlock syn

209209 <|> caseExpr syn

210210 <|> simpleExpr syn

@@ -785,7 +785,7 @@ pi syn =

785785 -- else return []

786786 return []

787787 st <- static

788− (do try(lchar '('); xt <- typeDeclList syn; lchar ')'

788+ (do try (lchar '('); xt <- typeDeclList syn; lchar ')'

789789 doc <- option "" (docComment '^')

790790 symbol "->"

791791 sc <- expr syn

src/Idris/ParseHelpers.hs+25−1

@@ -15,6 +15,7 @@ import Idris.AbsSyntax

1515

1616import Idris.Core.TT

1717import Idris.Core.Evaluate

18+import Idris.Delaborate (pprintErr)

1819

1920import Control.Applicative

2021import Control.Monad

@@ -46,7 +47,30 @@ type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Mon

4647

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

4849runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> Result res

49−runparser p i inputname = parseString (runInnerParser (evalStateT p i)) (Directed (UTF8.fromString inputname) 0 0 0 0)

50+runparser p i inputname =

51+ parseString (runInnerParser (evalStateT p i))

52+ (Directed (UTF8.fromString inputname) 0 0 0 0)

53+

54+noDocCommentHere :: Char -> String -> IdrisParser ()

55+noDocCommentHere c msg =

56+ optional (do fc <- getFC

57+ docComment c

58+ ist <- get

59+ put ist { parserWarnings = (fc, Msg msg) : parserWarnings ist}) *>

60+ pure ()

61+

62+clearParserWarnings :: Idris ()

63+clearParserWarnings = do ist <- getIState

64+ putIState ist { parserWarnings = [] }

65+

66+reportParserWarnings :: Idris ()

67+reportParserWarnings = do ist <- getIState

68+ mapM_ (uncurry $ ihWarn (idris_outh ist))

69+ (map (\ (fc, err) -> (fc, pprintErr ist err)) .

70+ reverse .

71+ nub $

72+ parserWarnings ist)

73+ clearParserWarnings

5074

5175{- * Space, comments and literals (token/lexing like parsers) -}

5276

src/Idris/Parser.hs+5−3

@@ -87,7 +87,8 @@ import System.IO

8787@

8888-}

8989moduleHeader :: IdrisParser [String]

90−moduleHeader = try (do reserved "module"

90+moduleHeader = try (do noDocCommentHere '|' "Modules cannot have documentation comments"

91+ reserved "module"

9192 i <- identifier

9293 option ';' (lchar ';')

9394 return (moduleName i))

@@ -1085,8 +1086,7 @@ parseImports fname input

10851086 = do i <- getIState

10861087 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of

10871088 Failure err -> fail (show err)

1088− Success (x, i) -> do -- Discard state updates (there should be

1089− -- none anyway)

1089+ Success (x, i) -> do putIState i

10901090 return x

10911091 where imports :: IdrisParser (([String], [(String, Maybe String, FC)], Maybe Delta), IState)

10921092 imports = do whiteSpace

@@ -1125,6 +1125,7 @@ parseProg syn fname input mrk

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

11261126 return []

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

1128+ reportParserWarnings

11281129 return $ collect x

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

11301131 mainProg = case mrk of

@@ -1200,6 +1201,7 @@ loadSource h lidr f

12001201 file_in <- runIO $ readFile f

12011202 file <- if lidr then tclift $ unlit f file_in else return file_in

12021203 (mname, imports, pos) <- parseImports f file

1204+ reportParserWarnings

12031205

12041206 -- process and check module aliases

12051207 let modAliases = M.fromList