src/Idris/Parser/Helpers.hs · Idris-dev

git.iko.soy/Idris-dev

on fd6898e help sign in

Idris-dev/src/Idris/Parser/Helpers.hs

697 lines 27 kB history raw

1{-# LANGUAGE CPP, GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards, StandaloneDeriving #-}

2#if !(MIN_VERSION_base(4,8,0))

3{-# LANGUAGE OverlappingInstances #-}

4#endif

5module Idris.Parser.Helpers where

7import Prelude hiding (pi)

9import Text.Trifecta.Delta

10import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace, Err)

11import Text.Parser.LookAhead

12import Text.Parser.Expression

13import qualified Text.Parser.Token as Tok

14import qualified Text.Parser.Char as Chr

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

17import Idris.AbsSyntax

19import Idris.Core.TT

20import Idris.Core.Evaluate

21import Idris.Delaborate (pprintErr)

22import Idris.Docstrings

23import Idris.Output (iWarn)

25import qualified Util.Pretty as Pretty (text)

27import Control.Applicative

28import Control.Monad

29import Control.Monad.State.Strict

31import Data.Maybe

32import qualified Data.List.Split as Spl

33import Data.List

34import Data.Monoid

35import Data.Char

36import qualified Data.Map as M

37import qualified Data.HashSet as HS

38import qualified Data.Text as T

39import qualified Data.ByteString.UTF8 as UTF8

41import System.FilePath

43import Debug.Trace

45-- | Idris parser with state used during parsing

46type IdrisParser = StateT IState IdrisInnerParser

48newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

49 deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing, DeltaParsing, MarkParsing Delta, Monoid, TokenParsing)

51deriving instance Parsing IdrisInnerParser

53#if MIN_VERSION_base(4,8,0)

54instance {-# OVERLAPPING #-} TokenParsing IdrisParser where

55#else

56instance TokenParsing IdrisParser where

57#endif

58 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

59 token p = do s <- get

60 (FC fn (sl, sc) _) <- getFC --TODO: Update after fixing getFC

61 -- See Issue #1594

62 r <- p

63 (FC fn _ (el, ec)) <- getFC

64 whiteSpace

65 put (s { lastTokenSpan = Just (FC fn (sl, sc) (el, ec)) })

66 return r

67-- | Generalized monadic parsing constraint type

68type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)

70class HasLastTokenSpan m where

71 getLastTokenSpan :: m (Maybe FC)

73instance HasLastTokenSpan IdrisParser where

74 getLastTokenSpan = lastTokenSpan <$> get

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

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

78runparser p i inputname =

79 parseString (runInnerParser (evalStateT p i))

80 (Directed (UTF8.fromString inputname) 0 0 0 0)

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

83highlightP fc annot = do ist <- get

84 put ist { idris_parserHighlights = (fc, annot) : idris_parserHighlights ist}

86noDocCommentHere :: String -> IdrisParser ()

87noDocCommentHere msg =

88 optional (do fc <- getFC

89 docComment

90 ist <- get

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

92 pure ()

94clearParserWarnings :: Idris ()

95clearParserWarnings = do ist <- getIState

96 putIState ist { parserWarnings = [] }

98reportParserWarnings :: Idris ()

99reportParserWarnings = do ist <- getIState

100 mapM_ (uncurry iWarn)

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

102 reverse .

103 nubBy (\(fc, err) (fc', err') ->

104 FC' fc == FC' fc' && err == err') $

105 parserWarnings ist)

106 clearParserWarnings

107

108

109parserWarning :: FC -> Maybe Opt -> Err -> IdrisParser ()

110parserWarning fc warnOpt warnErr = do

111 ist <- get

112 let cmdline = opt_cmdline (idris_options ist)

113 unless (maybe False (`elem` cmdline) warnOpt) $

114 put ist { parserWarnings = (fc, warnErr) : parserWarnings ist }

115

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

117

118-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)

119simpleWhiteSpace :: MonadicParsing m => m ()

120simpleWhiteSpace = satisfy isSpace *> pure ()

121

122-- | Checks if a charcter is end of line

123isEol :: Char -> Bool

124isEol '\n' = True

125isEol _ = False

126

127-- | A parser that succeeds at the end of the line

128eol :: MonadicParsing m => m ()

129eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"

130

131{- | Consumes a single-line comment

132

133@

134 SingleLineComment_t ::= '--' ~EOL_t* EOL_t ;

135@

136 -}

137singleLineComment :: MonadicParsing m => m ()

138singleLineComment = (string "--" *>

139 many (satisfy (not . isEol)) *>

140 eol *> pure ())

141 <?> ""

142

143{- | Consumes a multi-line comment

144

145@

146 MultiLineComment_t ::=

147 '{ -- }'

148 | '{ -' InCommentChars_t

149 ;

150@

151

152@

153 InCommentChars_t ::=

154 '- }'

155 | MultiLineComment_t InCommentChars_t

156 | ~'- }'+ InCommentChars_t

157 ;

158@

159-}

160multiLineComment :: MonadicParsing m => m ()

161multiLineComment = try (string "{-" *> (string "-}") *> pure ())

162 <|> string "{-" *> inCommentChars

163 <?> ""

164 where inCommentChars :: MonadicParsing m => m ()

165 inCommentChars = string "-}" *> pure ()

166 <|> try (multiLineComment) *> inCommentChars

167 <|> string "|||" *> many (satisfy (not . isEol)) *> eol *> inCommentChars

168 <|> skipSome (noneOf startEnd) *> inCommentChars

169 <|> oneOf startEnd *> inCommentChars

170 <?> "end of comment"

171 startEnd :: String

172 startEnd = "{}-"

173

174{-| Parses a documentation comment

175

176@

177 DocComment_t ::= '|||' ~EOL_t* EOL_t

178 ;

179@

180 -}

181docComment :: IdrisParser (Docstring (), [(Name, Docstring ())])

182docComment = do dc <- pushIndent *> docCommentLine

183 rest <- many (indented docCommentLine)

184 args <- many $ do (name, first) <- indented argDocCommentLine

185 rest <- many (indented docCommentLine)

186 return (name, concat (intersperse "\n" (first:rest)))

187 popIndent

188 return (parseDocstring $ T.pack (concat (intersperse "\n" (dc:rest))),

189 map (\(n, d) -> (n, parseDocstring (T.pack d))) args)

190

191 where docCommentLine :: MonadicParsing m => m String

192 docCommentLine = try (do string "|||"

193 many (satisfy (==' '))

194 contents <- option "" (do first <- satisfy (\c -> not (isEol c || c == '@'))

195 res <- many (satisfy (not . isEol))

196 return $ first:res)

197 eol ; someSpace

198 return contents)-- ++ concat rest))

199 <?> ""

200

201 argDocCommentLine = do string "|||"

202 many (satisfy isSpace)

203 char '@'

204 many (satisfy isSpace)

205 n <- fst <$> name

206 many (satisfy isSpace)

207 docs <- many (satisfy (not . isEol))

208 eol ; someSpace

209 return (n, docs)

210

211-- | Parses some white space

212whiteSpace :: MonadicParsing m => m ()

213whiteSpace = Tok.whiteSpace

214

215-- | Parses a string literal

216stringLiteral :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC)

217stringLiteral = do str <- Tok.stringLiteral

218 fc <- getLastTokenSpan

219 return (str, fromMaybe NoFC fc)

220

221-- | Parses a char literal

222charLiteral :: (MonadicParsing m, HasLastTokenSpan m) => m (Char, FC)

223charLiteral = do ch <- Tok.charLiteral

224 fc <- getLastTokenSpan

225 return (ch, fromMaybe NoFC fc)

226

227-- | Parses a natural number

228natural :: (MonadicParsing m, HasLastTokenSpan m) => m (Integer, FC)

229natural = do n <- Tok.natural

230 fc <- getLastTokenSpan

231 return (n, fromMaybe NoFC fc)

232

233-- | Parses an integral number

234integer :: MonadicParsing m => m Integer

235integer = Tok.integer

236

237-- | Parses a floating point number

238float :: (MonadicParsing m, HasLastTokenSpan m) => m (Double, FC)

239float = do f <- Tok.double

240 fc <- getLastTokenSpan

241 return (f, fromMaybe NoFC fc)

242

243{- * Symbols, identifiers, names and operators -}

244

245

246-- | Idris Style for parsing identifiers/reserved keywords

247idrisStyle :: MonadicParsing m => IdentifierStyle m

248idrisStyle = IdentifierStyle {

249 _styleName = "Idris"

250 , _styleStart = satisfy isAlpha <|> oneOf "_"

251 , _styleLetter = satisfy isAlphaNum <|> oneOf "_'."

252 , _styleReserved = HS.fromList

253 ["let", "in", "data", "codata", "record", "corecord", "Type", "do", "dsl",

254 "import", "impossible", "case", "of", "total", "partial", "mutual",

255 "infix", "infixl", "infixr", "rewrite", "where", "with", "syntax",

256 "proof", "postulate", "using", "namespace", "class", "instance",

257 "interface", "implementation", "parameters", "public", "private",

258 "export", "abstract", "implicit", "quoteGoal", "constructor", "if",

259 "then", "else"]

260 , _styleHighlight = Hi.Identifier

261 , _styleReservedHighlight = Hi.ReservedIdentifier }

262

263char :: MonadicParsing m => Char -> m Char

264char = Chr.char

265

266string :: MonadicParsing m => String -> m String

267string = Chr.string

268

269-- | Parses a character as a token

270lchar :: MonadicParsing m => Char -> m Char

271lchar = token . char

272

273-- | Parses a character as a token, returning the source span of the character

274lcharFC :: MonadicParsing m => Char -> m FC

275lcharFC ch = do (FC file (l, c) _) <- getFC

276 _ <- token (char ch)

277 return $ FC file (l, c) (l, c+1)

278

279-- | Parses string as a token

280symbol :: MonadicParsing m => String -> m String

281symbol = Tok.symbol

282

283symbolFC :: MonadicParsing m => String -> m FC

284symbolFC str = do (FC file (l, c) _) <- getFC

285 Tok.symbol str

286 return $ FC file (l, c) (l, c + length str)

287

288-- | Parses a reserved identifier

289reserved :: MonadicParsing m => String -> m ()

290reserved = Tok.reserve idrisStyle

291

292-- | Parses a reserved identifier, computing its span. Assumes that

293-- reserved identifiers never contain line breaks.

294reservedFC :: MonadicParsing m => String -> m FC

295reservedFC str = do (FC file (l, c) _) <- getFC

296 reserved str

297 return $ FC file (l, c) (l, c + length str)

298

299-- | Parse a reserved identfier, highlighting its span as a keyword

300reservedHL :: String -> IdrisParser ()

301reservedHL str = reservedFC str >>= flip highlightP AnnKeyword

302

303-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007

304-- | Parses a reserved operator

305reservedOp :: MonadicParsing m => String -> m ()

306reservedOp name = token $ try $

307 do string name

308 notFollowedBy (operatorLetter) <?> ("end of " ++ show name)

309

310reservedOpFC :: MonadicParsing m => String -> m FC

311reservedOpFC name = do (FC f (l, c) _) <- getFC

312 reservedOp name

313 return (FC f (l, c) (l, c + length name))

314

315-- | Parses an identifier as a token

316identifier :: (MonadicParsing m) => m (String, FC)

317identifier = try(do (i, fc) <-

318 token $ do (FC f (l, c) _) <- getFC

319 i <- Tok.ident idrisStyle

320 return (i, FC f (l, c) (l, c + length i))

321 when (i == "_") $ unexpected "wildcard"

322 return (i, fc))

323

324-- | Parses an identifier with possible namespace as a name

325iName :: (MonadicParsing m, HasLastTokenSpan m) => [String] -> m (Name, FC)

326iName bad = do (n, fc) <- maybeWithNS identifier False bad

327 return (n, fc)

328 <?> "name"

329

330-- | Parses an string possibly prefixed by a namespace

331maybeWithNS :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC) -> Bool -> [String] -> m (Name, FC)

332maybeWithNS parser ascend bad = do

333 fc <- getFC

334 i <- option "" (lookAhead (fst <$> identifier))

335 when (i `elem` bad) $ unexpected "reserved identifier"

336 let transf = if ascend then id else reverse

337 (x, xs, fc) <- choice (transf (parserNoNS parser : parsersNS parser i))

338 return (mkName (x, xs), fc)

339 where parserNoNS :: MonadicParsing m => m (String, FC) -> m (String, String, FC)

340 parserNoNS parser = do startFC <- getFC

341 (x, nameFC) <- parser

342 return (x, "", spanFC startFC nameFC)

343 parserNS :: MonadicParsing m => m (String, FC) -> String -> m (String, String, FC)

344 parserNS parser ns = do startFC <- getFC

345 xs <- string ns

346 lchar '.'; (x, nameFC) <- parser

347 return (x, xs, spanFC startFC nameFC)

348 parsersNS :: MonadicParsing m => m (String, FC) -> String -> [m (String, String, FC)]

349 parsersNS parser i = [try (parserNS parser ns) | ns <- (initsEndAt (=='.') i)]

350

351-- | Parses a name

352name :: IdrisParser (Name, FC)

353name = (<?> "name") $ do

354 keywords <- syntax_keywords <$> get

355 aliases <- module_aliases <$> get

356 (n, fc) <- iName keywords

357 return (unalias aliases n, fc)

358 where

359 unalias :: M.Map [T.Text] [T.Text] -> Name -> Name

360 unalias aliases (NS n ns) | Just ns' <- M.lookup ns aliases = NS n ns'

361 unalias aliases name = name

362

363{- | List of all initial segments in ascending order of a list. Every

364such initial segment ends right before an element satisfying the given

365condition.

366-}

367initsEndAt :: (a -> Bool) -> [a] -> [[a]]

368initsEndAt p [] = []

369initsEndAt p (x:xs) | p x = [] : x_inits_xs

370 | otherwise = x_inits_xs

371 where x_inits_xs = [x : cs | cs <- initsEndAt p xs]

372

373

374{- | Create a `Name' from a pair of strings representing a base name and its

375 namespace.

376-}

377mkName :: (String, String) -> Name

378mkName (n, "") = sUN n

379mkName (n, ns) = sNS (sUN n) (reverse (parseNS ns))

380 where parseNS x = case span (/= '.') x of

381 (x, "") -> [x]

382 (x, '.':y) -> x : parseNS y

383

384opChars :: String

385opChars = ":!#$%&*+./<=>?@\\^|-~"

386

387operatorLetter :: MonadicParsing m => m Char

388operatorLetter = oneOf opChars

389

390

391commentMarkers :: [String]

392commentMarkers = [ "--", "|||" ]

393

394invalidOperators :: [String]

395invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!", "@"]

396

397-- | Parses an operator

398operator :: MonadicParsing m => m String

399operator = do op <- token . some $ operatorLetter

400 when (op `elem` (invalidOperators ++ commentMarkers)) $

401 fail $ op ++ " is not a valid operator"

402 return op

403

404-- | Parses an operator

405operatorFC :: MonadicParsing m => m (String, FC)

406operatorFC = do (FC f (l, c) _) <- getFC

407 op <- operator

408 return (op, FC f (l, c) (l, c + length op))

409

410{- * Position helpers -}

411{- | Get filename from position (returns "(interactive)" when no source file is given) -}

412fileName :: Delta -> String

413fileName (Directed fn _ _ _ _) = UTF8.toString fn

414fileName _ = "(interactive)"

415

416{- | Get line number from position -}

417lineNum :: Delta -> Int

418lineNum (Lines l _ _ _) = fromIntegral l + 1

419lineNum (Directed _ l _ _ _) = fromIntegral l + 1

420lineNum _ = 0

421

422{- | Get column number from position -}

423columnNum :: Delta -> Int

424columnNum pos = fromIntegral (column pos) + 1

425

426

427{- | Get file position as FC -}

428getFC :: MonadicParsing m => m FC

429getFC = do s <- position

430 let (dir, file) = splitFileName (fileName s)

431 let f = if dir == addTrailingPathSeparator "." then file else fileName s

432 return $ FC f (lineNum s, columnNum s) (lineNum s, columnNum s) -- TODO: Change to actual spanning

433 -- Issue #1594 on the Issue Tracker.

434 -- https://github.com/idris-lang/Idris-dev/issues/1594

435

436

437{-* Syntax helpers-}

438-- | Bind constraints to term

439bindList :: (Name -> FC -> PTerm -> PTerm -> PTerm) -> [(Name, FC, PTerm)] -> PTerm -> PTerm

440bindList b [] sc = sc

441bindList b ((n, fc, t):bs) sc = b n fc t (bindList b bs sc)

442

443{- | @commaSeparated p@ parses one or more occurences of `p`,

444 separated by commas and optional whitespace. -}

445commaSeparated :: MonadicParsing m => m a -> m [a]

446commaSeparated p = p `sepBy1` (spaces >> char ',' >> spaces)

447

448{- * Layout helpers -}

449

450-- | Push indentation to stack

451pushIndent :: IdrisParser ()

452pushIndent = do pos <- position

453 ist <- get

454 put (ist { indent_stack = (fromIntegral (column pos) + 1) : indent_stack ist })

455

456-- | Pops indentation from stack

457popIndent :: IdrisParser ()

458popIndent = do ist <- get

459 case indent_stack ist of

460 [] -> error "The impossible happened! Tried to pop an indentation level where none was pushed (underflow)."

461 (x : xs) -> put (ist { indent_stack = xs })

462

463

464-- | Gets current indentation

465indent :: IdrisParser Int

466indent = liftM ((+1) . fromIntegral . column) position

467

468-- | Gets last indentation

469lastIndent :: IdrisParser Int

470lastIndent = do ist <- get

471 case indent_stack ist of

472 (x : xs) -> return x

473 _ -> return 1

474

475-- | Applies parser in an indented position

476indented :: IdrisParser a -> IdrisParser a

477indented p = notEndBlock *> p <* keepTerminator

478

479-- | Applies parser to get a block (which has possibly indented statements)

480indentedBlock :: IdrisParser a -> IdrisParser [a]

481indentedBlock p = do openBlock

482 pushIndent

483 res <- many (indented p)

484 popIndent

485 closeBlock

486 return res

487

488-- | Applies parser to get a block with at least one statement (which has possibly indented statements)

489indentedBlock1 :: IdrisParser a -> IdrisParser [a]

490indentedBlock1 p = do openBlock

491 pushIndent

492 res <- some (indented p)

493 popIndent

494 closeBlock

495 return res

496

497-- | Applies parser to get a block with exactly one (possibly indented) statement

498indentedBlockS :: IdrisParser a -> IdrisParser a

499indentedBlockS p = do openBlock

500 pushIndent

501 res <- indented p

502 popIndent

503 closeBlock

504 return res

505

506

507-- | Checks if the following character matches provided parser

508lookAheadMatches :: MonadicParsing m => m a -> m Bool

509lookAheadMatches p = do match <- lookAhead (optional p)

510 return $ isJust match

511

512-- | Parses a start of block

513openBlock :: IdrisParser ()

514openBlock = do lchar '{'

515 ist <- get

516 put (ist { brace_stack = Nothing : brace_stack ist })

517 <|> do ist <- get

518 lvl' <- indent

519 -- if we're not indented further, it's an empty block, so

520 -- increment lvl to ensure we get to the end

521 let lvl = case brace_stack ist of

522 Just lvl_old : _ ->

523 if lvl' <= lvl_old then lvl_old+1

524 else lvl'

525 [] -> if lvl' == 1 then 2 else lvl'

526 _ -> lvl'

527 put (ist { brace_stack = Just lvl : brace_stack ist })

528 <?> "start of block"

529

530-- | Parses an end of block

531closeBlock :: IdrisParser ()

532closeBlock = do ist <- get

533 bs <- case brace_stack ist of

534 [] -> eof >> return []

535 Nothing : xs -> lchar '}' >> return xs <?> "end of block"

536 Just lvl : xs -> (do i <- indent

537 isParen <- lookAheadMatches (char ')')

538 isIn <- lookAheadMatches (reserved "in")

539 if i >= lvl && not (isParen || isIn)

540 then fail "not end of block"

541 else return xs)

542 <|> (do notOpenBraces

543 eof

544 return [])

545 put (ist { brace_stack = bs })

546

547-- | Parses a terminator

548terminator :: IdrisParser ()

549terminator = do lchar ';'; popIndent

550 <|> do c <- indent; l <- lastIndent

551 if c <= l then popIndent else fail "not a terminator"

552 <|> do isParen <- lookAheadMatches (oneOf ")}")

553 if isParen then popIndent else fail "not a terminator"

554 <|> lookAhead eof

555

556-- | Parses and keeps a terminator

557keepTerminator :: IdrisParser ()

558keepTerminator = do lchar ';'; return ()

559 <|> do c <- indent; l <- lastIndent

560 unless (c <= l) $ fail "not a terminator"

561 <|> do isParen <- lookAheadMatches (oneOf ")}|")

562 isIn <- lookAheadMatches (reserved "in")

563 unless (isIn || isParen) $ fail "not a terminator"

564 <|> lookAhead eof

565

566-- | Checks if application expression does not end

567notEndApp :: IdrisParser ()

568notEndApp = do c <- indent; l <- lastIndent

569 when (c <= l) (fail "terminator")

570

571-- | Checks that it is not end of block

572notEndBlock :: IdrisParser ()

573notEndBlock = do ist <- get

574 case brace_stack ist of

575 Just lvl : xs -> do i <- indent

576 isParen <- lookAheadMatches (char ')')

577 when (i < lvl || isParen) (fail "end of block")

578 _ -> return ()

579

580-- | Representation of an operation that can compare the current indentation with the last indentation, and an error message if it fails

581data IndentProperty = IndentProperty (Int -> Int -> Bool) String

582

583-- | Allows comparison of indent, and fails if property doesn't hold

584indentPropHolds :: IndentProperty -> IdrisParser ()

585indentPropHolds (IndentProperty op msg) = do

586 li <- lastIndent

587 i <- indent

588 when (not $ op i li) $ fail ("Wrong indention: " ++ msg)

589

590-- | Greater-than indent property

591gtProp :: IndentProperty

592gtProp = IndentProperty (>) "should be greater than context indentation"

593

594-- | Greater-than or equal to indent property

595gteProp :: IndentProperty

596gteProp = IndentProperty (>=) "should be greater than or equal context indentation"

597

598-- | Equal indent property

599eqProp :: IndentProperty

600eqProp = IndentProperty (==) "should be equal to context indentation"

601

602-- | Less-than indent property

603ltProp :: IndentProperty

604ltProp = IndentProperty (<) "should be less than context indentation"

605

606-- | Less-than or equal to indent property

607lteProp :: IndentProperty

608lteProp = IndentProperty (<=) "should be less than or equal to context indentation"

609

610

611-- | Checks that there are no braces that are not closed

612notOpenBraces :: IdrisParser ()

613notOpenBraces = do ist <- get

614 when (hasNothing $ brace_stack ist) $ fail "end of input"

615 where hasNothing :: [Maybe a] -> Bool

616 hasNothing = any isNothing

617

618{- | Parses an accessibilty modifier (e.g. public, private) -}

619accessibility' :: IdrisParser Accessibility

620accessibility'

621 = do reserved "public";

622 gotexp <- optional (reserved "export")

623 case gotexp of

624 Just _ -> return ()

625 Nothing -> do

626 ist <- get

627 fc <- getFC

628 put ist { parserWarnings =

629 (fc, Msg "'public' is deprecated. Use 'public export' instead.")

630 : parserWarnings ist }

631 return Public

632 <|> do reserved "abstract";

633 ist <- get

634 fc <- getFC

635 put ist { parserWarnings =

636 (fc, Msg "The 'abstract' keyword is deprecated. Use 'export' instead.")

637 : parserWarnings ist }

638 return Frozen

639 <|> do reserved "export"; return Frozen

640 <|> do reserved "private"; return Private

641 <?> "accessibility modifier"

642

643accessibility :: IdrisParser Accessibility

644accessibility = do acc <- optional accessibility'

645 case acc of

646 Just a -> return a

647 Nothing -> do ist <- get

648 return (default_access ist)

649

650-- | Adds accessibility option for function

651addAcc :: Name -> Accessibility -> IdrisParser ()

652addAcc n a = do i <- get

653 put (i { hide_list = addDef n a (hide_list i) })

654

655{- | Add accessbility option for data declarations

656 (works for classes too - 'abstract' means the data/class is visible but members not) -}

657accData :: Accessibility -> Name -> [Name] -> IdrisParser ()

658accData Frozen n ns = do addAcc n Public -- so that it can be used in public definitions

659 mapM_ (\n -> addAcc n Private) ns -- so that they are invisible

660accData a n ns = do addAcc n a

661 mapM_ (`addAcc` a) ns

662

663

664{- * Error reporting helpers -}

665{- | Error message with possible fixes list -}

666fixErrorMsg :: String -> [String] -> String

667fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)

668

669-- | Collect 'PClauses' with the same function name

670collect :: [PDecl] -> [PDecl]

671collect (c@(PClauses _ o _ _) : ds)

672 = clauses (cname c) [] (c : ds)

673 where clauses :: Maybe Name -> [PClause] -> [PDecl] -> [PDecl]

674 clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)

675 | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds

676 clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r pn w] : ds)

677 | n == n' = clauses j (PWith fc' n' l ws r pn (collect w) : acc) ds

678 clauses (Just n) acc xs = PClauses (fcOf c) o n (reverse acc) : collect xs

679 clauses Nothing acc (x:xs) = collect xs

680 clauses Nothing acc [] = []

681

682 cname :: PDecl -> Maybe Name

683 cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n

684 cname (PClauses fc _ _ [PWith _ n _ _ _ _ _]) = Just n

685 cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing

686 cname (PClauses fc _ _ [PWithR _ _ _ _ _]) = Nothing

687 fcOf :: PDecl -> FC

688 fcOf (PClauses fc _ _ _) = fc

689collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

690collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

691collect (PNamespace ns fc ps : ds) = PNamespace ns fc (collect ps) : collect ds

692collect (PClass doc f s cs n nfc ps pdocs fds ds cn cd : ds')

693 = PClass doc f s cs n nfc ps pdocs fds (collect ds) cn cd : collect ds'

694collect (PInstance doc argDocs f s cs acc opts n nfc ps t en ds : ds')

695 = PInstance doc argDocs f s cs acc opts n nfc ps t en (collect ds) : collect ds'

696collect (d : ds) = d : collect ds

697collect [] = []