c733a8f · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+2−1

compare with master

unifiedsplit

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

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

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

135 errLine :: Maybe Int,

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

136 lastParse :: Maybe Name,

137 lastParse :: Maybe Name,

137 indent_stack :: [Int],

138 indent_stack :: [Int],

138 brace_stack :: [Maybe Int],

139 brace_stack :: [Maybe Int],

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

219 emptyContext emptyContext emptyContext emptyContext

220 emptyContext emptyContext emptyContext emptyContext

220 emptyContext emptyContext

221 emptyContext emptyContext

221 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

222 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

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

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

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

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

224 AutomaticWidth

225 AutomaticWidth

225

226

src/Idris/Chaser.hs+2

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

132 file_in <- runIO $ readFile f

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

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

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

136+ clearParserWarnings

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

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

136 return (concat ms)

138 return (concat ms)

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

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

src/Idris/ParseExpr.hs+4−4

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

78

79doexpr' :: SyntaxInfo -> IdrisParser PTerm

80doexpr' syn = try (externalExpr syn)

81− <|> internalExpr syn

81+ <|> internalExpr syn

82− <?> "expression"

82+ <?> "expression"

83

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

85externalExpr :: SyntaxInfo -> IdrisParser PTerm

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

204 <|> quoteGoal syn

205 <|> let_ syn

206 <|> rewriteTerm syn

207− <|> try(pi syn)

207+ <|> try (pi syn)

208 <|> doBlock syn

209 <|> caseExpr syn

210 <|> simpleExpr syn

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

785 -- else return []

786 return []

787 st <- static

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

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

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

790 symbol "->"

791 sc <- expr syn

src/Idris/ParseHelpers.hs+25−1

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

15

16import Idris.Core.TT

17import Idris.Core.Evaluate

18+import Idris.Delaborate (pprintErr)

18

19

19import Control.Applicative

20import Control.Applicative

20import Control.Monad

21import Control.Monad

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

46

47

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

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

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

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

50+runparser p i inputname =

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

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

50

74

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

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

52

76

src/Idris/Parser.hs+5−3

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

87@

88-}

89moduleHeader :: IdrisParser [String]

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

90−moduleHeader = try (do reserved "module"

91+ reserved "module"

91 i <- identifier

92 i <- identifier

92 option ';' (lchar ';')

93 option ';' (lchar ';')

93 return (moduleName i))

94 return (moduleName i))

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

1085 = do i <- getIState

1086 = do i <- getIState

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

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

1087 Failure err -> fail (show err)

1088 Failure err -> fail (show err)

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

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

1089− -- none anyway)

1090 return x

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

1092 imports = do whiteSpace

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

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

1126 return []

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

1128+ reportParserWarnings

1128 return $ collect x

1129 return $ collect x

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

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

1130 mainProg = case mrk of

1131 mainProg = case mrk of

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

1200 file_in <- runIO $ readFile f

1201 file_in <- runIO $ readFile f

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

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

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

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

1204+ reportParserWarnings

1203

1205

1204 -- process and check module aliases

1206 -- process and check module aliases

1205 let modAliases = M.fromList

1207 let modAliases = M.fromList