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

git.iko.soy/Idris-dev

on 385dcbf help sign in

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

711 lines 28 kB history raw

1{-|

2Module : Idris.Parser.Helpers

3Description : Utilities for Idris' parser.

4Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8{-# LANGUAGE CPP, ConstraintKinds, GeneralizedNewtypeDeriving, PatternGuards,

9 StandaloneDeriving #-}

10module Idris.Parser.Helpers where

12import Idris.AbsSyntax

13import Idris.Core.Evaluate

14import Idris.Core.TT

15import Idris.Delaborate (pprintErr)

16import Idris.Docstrings

17import Idris.Options

18import Idris.Output (iWarn)

20import qualified Util.Pretty as Pretty (text)

22import Prelude hiding (pi)

24import Control.Applicative

25import Control.Monad

26import Control.Monad.State.Strict

27import qualified Data.ByteString.UTF8 as UTF8

28import Data.Char

29import qualified Data.HashSet as HS

30import Data.List

31import qualified Data.List.Split as Spl

32import qualified Data.Map as M

33import Data.Maybe

34import Data.Monoid

35import qualified Data.Text as T

36import Debug.Trace

37import System.FilePath

38import qualified Text.Parser.Char as Chr

39import Text.Parser.Expression

40import Text.Parser.LookAhead

41import qualified Text.Parser.Token as Tok

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

43import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,

44 stringLiteral, symbol, whiteSpace)

45import Text.Trifecta.Delta

47-- | Idris parser with state used during parsing

48type IdrisParser = StateT IState IdrisInnerParser

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

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

53deriving instance Parsing IdrisInnerParser

55#if MIN_VERSION_base(4,9,0)

56instance {-# OVERLAPPING #-} DeltaParsing IdrisParser where

57 line = lift line

58 {-# INLINE line #-}

59 position = lift position

60 {-# INLINE position #-}

61 slicedWith f (StateT m) = StateT $ \s -> slicedWith (\(a,s') b -> (f a b, s')) $ m s

62 {-# INLINE slicedWith #-}

63 rend = lift rend

64 {-# INLINE rend #-}

65 restOfLine = lift restOfLine

66 {-# INLINE restOfLine #-}

68#endif

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

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

72 token p = do s <- get

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

74 -- See Issue #1594

75 r <- p

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

77 whiteSpace

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

79 return r

80-- | Generalized monadic parsing constraint type

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

83class HasLastTokenSpan m where

84 getLastTokenSpan :: m (Maybe FC)

86instance HasLastTokenSpan IdrisParser where

87 getLastTokenSpan = lastTokenSpan <$> get

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

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

91runparser p i inputname =

92 parseString (runInnerParser (evalStateT p i))

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

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

96highlightP fc annot = do ist <- get

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

99noDocCommentHere :: String -> IdrisParser ()

100noDocCommentHere msg =

101 optional (do fc <- getFC

102 docComment

103 ist <- get

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

105 pure ()

106

107clearParserWarnings :: Idris ()

108clearParserWarnings = do ist <- getIState

109 putIState ist { parserWarnings = [] }

110

111reportParserWarnings :: Idris ()

112reportParserWarnings = do ist <- getIState

113 mapM_ (uncurry iWarn)

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

115 reverse .

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

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

118 parserWarnings ist)

119 clearParserWarnings

120

121

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

123parserWarning fc warnOpt warnErr = do

124 ist <- get

125 let cmdline = opt_cmdline (idris_options ist)

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

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

128

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

130

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

132simpleWhiteSpace :: MonadicParsing m => m ()

133simpleWhiteSpace = satisfy isSpace *> pure ()

134

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

136isEol :: Char -> Bool

137isEol '\n' = True

138isEol _ = False

139

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

141eol :: MonadicParsing m => m ()

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

143

144{- | Consumes a single-line comment

145

146@

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

148@

149 -}

150singleLineComment :: MonadicParsing m => m ()

151singleLineComment = (string "--" *>

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

153 eol *> pure ())

154 <?> ""

155

156{- | Consumes a multi-line comment

157

158@

159 MultiLineComment_t ::=

160 '{ -- }'

161 | '{ -' InCommentChars_t

162 ;

163@

164

165@

166 InCommentChars_t ::=

167 '- }'

168 | MultiLineComment_t InCommentChars_t

169 | ~'- }'+ InCommentChars_t

170 ;

171@

172-}

173multiLineComment :: MonadicParsing m => m ()

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

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

176 <?> ""

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

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

179 <|> try (multiLineComment) *> inCommentChars

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

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

182 <|> oneOf startEnd *> inCommentChars

183 <?> "end of comment"

184 startEnd :: String

185 startEnd = "{}-"

186

187{-| Parses a documentation comment

188

189@

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

191 ;

192@

193 -}

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

195docComment = do dc <- pushIndent *> docCommentLine

196 rest <- many (indented docCommentLine)

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

198 rest <- many (indented docCommentLine)

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

200 popIndent

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

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

203

204 where docCommentLine :: MonadicParsing m => m String

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

206 many (satisfy (==' '))

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

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

209 return $ first:res)

210 eol ; someSpace

211 return contents)-- ++ concat rest))

212 <?> ""

213

214 argDocCommentLine = do string "|||"

215 many (satisfy isSpace)

216 char '@'

217 many (satisfy isSpace)

218 n <- fst <$> name

219 many (satisfy isSpace)

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

221 eol ; someSpace

222 return (n, docs)

223

224-- | Parses some white space

225whiteSpace :: MonadicParsing m => m ()

226whiteSpace = Tok.whiteSpace

227

228-- | Parses a string literal

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

230stringLiteral = do str <- Tok.stringLiteral

231 fc <- getLastTokenSpan

232 return (str, fromMaybe NoFC fc)

233

234-- | Parses a char literal

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

236charLiteral = do ch <- Tok.charLiteral

237 fc <- getLastTokenSpan

238 return (ch, fromMaybe NoFC fc)

239

240-- | Parses a natural number

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

242natural = do n <- Tok.natural

243 fc <- getLastTokenSpan

244 return (n, fromMaybe NoFC fc)

245

246-- | Parses an integral number

247integer :: MonadicParsing m => m Integer

248integer = Tok.integer

249

250-- | Parses a floating point number

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

252float = do f <- Tok.double

253 fc <- getLastTokenSpan

254 return (f, fromMaybe NoFC fc)

255

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

257

258

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

260idrisStyle :: MonadicParsing m => IdentifierStyle m

261idrisStyle = IdentifierStyle {

262 _styleName = "Idris"

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

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

265 , _styleReserved = HS.fromList

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

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

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

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

270 "interface", "implementation", "parameters", "public", "private",

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

272 "then", "else"]

273 , _styleHighlight = Hi.Identifier

274 , _styleReservedHighlight = Hi.ReservedIdentifier }

275

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

277char = Chr.char

278

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

280string = Chr.string

281

282-- | Parses a character as a token

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

284lchar = token . char

285

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

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

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

289 _ <- token (char ch)

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

291

292-- | Parses string as a token

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

294symbol = Tok.symbol

295

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

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

298 Tok.symbol str

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

300

301-- | Parses a reserved identifier

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

303reserved = Tok.reserve idrisStyle

304

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

306-- reserved identifiers never contain line breaks.

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

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

309 reserved str

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

311

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

313reservedHL :: String -> IdrisParser ()

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

315

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

317-- | Parses a reserved operator

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

319reservedOp name = token $ try $

320 do string name

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

322

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

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

325 reservedOp name

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

327

328-- | Parses an identifier as a token

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

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

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

332 i <- Tok.ident idrisStyle

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

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

335 return (i, fc))

336

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

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

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

340 return (n, fc)

341 <?> "name"

342

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

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

345maybeWithNS parser ascend bad = do

346 fc <- getFC

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

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

349 let transf = if ascend then id else reverse

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

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

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

353 parserNoNS parser = do startFC <- getFC

354 (x, nameFC) <- parser

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

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

357 parserNS parser ns = do startFC <- getFC

358 xs <- string ns

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

360 return (x, xs, spanFC startFC nameFC)

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

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

363

364-- | Parses a name

365name :: IdrisParser (Name, FC)

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

367 keywords <- syntax_keywords <$> get

368 aliases <- module_aliases <$> get

369 (n, fc) <- iName keywords

370 return (unalias aliases n, fc)

371 where

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

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

374 unalias aliases name = name

375

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

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

378condition.

379-}

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

381initsEndAt p [] = []

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

383 | otherwise = x_inits_xs

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

385

386

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

388 namespace.

389-}

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

391mkName (n, "") = sUN n

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

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

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

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

396

397opChars :: String

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

399

400operatorLetter :: MonadicParsing m => m Char

401operatorLetter = oneOf opChars

402

403

404commentMarkers :: [String]

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

406

407invalidOperators :: [String]

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

409

410-- | Parses an operator

411operator :: MonadicParsing m => m String

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

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

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

415 return op

416

417-- | Parses an operator

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

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

420 op <- operator

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

422

423{- * Position helpers -}

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

425fileName :: Delta -> String

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

427fileName _ = "(interactive)"

428

429{- | Get line number from position -}

430lineNum :: Delta -> Int

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

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

433lineNum _ = 0

434

435{- | Get column number from position -}

436columnNum :: Delta -> Int

437columnNum pos = fromIntegral (column pos) + 1

438

439

440{- | Get file position as FC -}

441getFC :: MonadicParsing m => m FC

442getFC = do s <- position

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

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

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

446 -- Issue #1594 on the Issue Tracker.

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

448

449

450{-* Syntax helpers-}

451-- | Bind constraints to term

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

453bindList b [] sc = sc

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

455

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

457 separated by commas and optional whitespace. -}

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

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

460

461{- * Layout helpers -}

462

463-- | Push indentation to stack

464pushIndent :: IdrisParser ()

465pushIndent = do pos <- position

466 ist <- get

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

468

469-- | Pops indentation from stack

470popIndent :: IdrisParser ()

471popIndent = do ist <- get

472 case indent_stack ist of

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

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

475

476

477-- | Gets current indentation

478indent :: IdrisParser Int

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

480

481-- | Gets last indentation

482lastIndent :: IdrisParser Int

483lastIndent = do ist <- get

484 case indent_stack ist of

485 (x : xs) -> return x

486 _ -> return 1

487

488-- | Applies parser in an indented position

489indented :: IdrisParser a -> IdrisParser a

490indented p = notEndBlock *> p <* keepTerminator

491

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

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

494indentedBlock p = do openBlock

495 pushIndent

496 res <- many (indented p)

497 popIndent

498 closeBlock

499 return res

500

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

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

503indentedBlock1 p = do openBlock

504 pushIndent

505 res <- some (indented p)

506 popIndent

507 closeBlock

508 return res

509

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

511indentedBlockS :: IdrisParser a -> IdrisParser a

512indentedBlockS p = do openBlock

513 pushIndent

514 res <- indented p

515 popIndent

516 closeBlock

517 return res

518

519

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

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

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

523 return $ isJust match

524

525-- | Parses a start of block

526openBlock :: IdrisParser ()

527openBlock = do lchar '{'

528 ist <- get

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

530 <|> do ist <- get

531 lvl' <- indent

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

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

534 let lvl = case brace_stack ist of

535 Just lvl_old : _ ->

536 if lvl' <= lvl_old then lvl_old+1

537 else lvl'

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

539 _ -> lvl'

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

541 <?> "start of block"

542

543-- | Parses an end of block

544closeBlock :: IdrisParser ()

545closeBlock = do ist <- get

546 bs <- case brace_stack ist of

547 [] -> eof >> return []

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

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

550 isParen <- lookAheadMatches (char ')')

551 isIn <- lookAheadMatches (reserved "in")

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

553 then fail "not end of block"

554 else return xs)

555 <|> (do notOpenBraces

556 eof

557 return [])

558 put (ist { brace_stack = bs })

559

560-- | Parses a terminator

561terminator :: IdrisParser ()

562terminator = do lchar ';'; popIndent

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

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

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

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

567 <|> lookAhead eof

568

569-- | Parses and keeps a terminator

570keepTerminator :: IdrisParser ()

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

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

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

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

575 isIn <- lookAheadMatches (reserved "in")

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

577 <|> lookAhead eof

578

579-- | Checks if application expression does not end

580notEndApp :: IdrisParser ()

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

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

583

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

585notEndBlock :: IdrisParser ()

586notEndBlock = do ist <- get

587 case brace_stack ist of

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

589 isParen <- lookAheadMatches (char ')')

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

591 _ -> return ()

592

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

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

595

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

597indentPropHolds :: IndentProperty -> IdrisParser ()

598indentPropHolds (IndentProperty op msg) = do

599 li <- lastIndent

600 i <- indent

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

602

603-- | Greater-than indent property

604gtProp :: IndentProperty

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

606

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

608gteProp :: IndentProperty

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

610

611-- | Equal indent property

612eqProp :: IndentProperty

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

614

615-- | Less-than indent property

616ltProp :: IndentProperty

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

618

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

620lteProp :: IndentProperty

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

622

623

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

625notOpenBraces :: IdrisParser ()

626notOpenBraces = do ist <- get

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

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

629 hasNothing = any isNothing

630

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

632accessibility' :: IdrisParser Accessibility

633accessibility'

634 = do reserved "public";

635 gotexp <- optional (reserved "export")

636 case gotexp of

637 Just _ -> return ()

638 Nothing -> do

639 ist <- get

640 fc <- getFC

641 put ist { parserWarnings =

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

643 : parserWarnings ist }

644 return Public

645 <|> do reserved "abstract";

646 ist <- get

647 fc <- getFC

648 put ist { parserWarnings =

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

650 : parserWarnings ist }

651 return Frozen

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

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

654 <?> "accessibility modifier"

655

656accessibility :: IdrisParser Accessibility

657accessibility = do acc <- optional accessibility'

658 case acc of

659 Just a -> return a

660 Nothing -> do ist <- get

661 return (default_access ist)

662

663-- | Adds accessibility option for function

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

665addAcc n a = do i <- get

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

667

668{- | Add accessbility option for data declarations

669 (works for interfaces too - 'abstract' means the data/interface is visible but members not) -}

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

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

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

673accData a n ns = do addAcc n a

674 mapM_ (`addAcc` a) ns

675

676

677{- * Error reporting helpers -}

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

679fixErrorMsg :: String -> [String] -> String

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

681

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

683collect :: [PDecl] -> [PDecl]

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

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

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

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

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

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

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

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

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

693 clauses Nothing acc [] = []

694

695 cname :: PDecl -> Maybe Name

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

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

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

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

700 fcOf :: PDecl -> FC

701 fcOf (PClauses fc _ _ _) = fc

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

703collect (POpenInterfaces f ns ps : ds) = POpenInterfaces f ns (collect ps) : collect ds

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

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

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

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

708collect (PImplementation doc argDocs f s cs pnames acc opts n nfc ps pextra t en ds : ds')

709 = PImplementation doc argDocs f s cs pnames acc opts n nfc ps pextra t en (collect ds) : collect ds'

710collect (d : ds) = d : collect ds

711collect [] = []