0 | module Parser.Rule.Source

  2 | import public Parser.Lexer.Source

  3 | import public Parser.Support

  5 | import Core.Metadata

  6 | import Data.List1

  7 | import Data.SnocList

  8 | import Data.String

  9 | import Idris.Syntax

 11 | %hide Core.Core.(>>)

 12 | %hide Core.Core.(>>=)

 14 | %default total

 20 | public export

 21 | record ParserState (container : Type -> Type) where

 22 |   constructor MkState

 23 |   decorations : container ASemanticDecoration

 24 |   holeNames : List String

 27 | public export

 28 | ParsingState : Type

 29 | ParsingState = ParserState SnocList

 33 | public export

 34 | State : Type

 35 | State = ParserState List

 38 | toState : ParsingState -> State

 39 | toState (MkState decs hs) = MkState (cast decs) hs

 45 | Semigroup ParsingState where

 46 |   MkState decs1 hs1 <+> MkState decs2 hs2

 47 |     = MkState (decs1 <+> decs2) (hs1 ++ hs2)

 50 | Monoid ParsingState where

 51 |   neutral = MkState [<] []

 53 | public export

 54 | BRule : Bool -> Type -> Type

 55 | BRule = Grammar ParsingState Token

 57 | public export

 58 | Rule : Type -> Type

 59 | Rule = BRule True

 61 | public export

 62 | EmptyRule : Type -> Type

 63 | EmptyRule = BRule False

 66 | actD : ASemanticDecoration -> EmptyRule ()

 67 | actD s = act (MkState [<s] [])

 70 | actH : String -> EmptyRule ()

 71 | actH s = act (MkState [<] [s])

 74 | debugInfo : Rule DebugInfo

 75 | debugInfo = terminal "Expected a magic debug info directive" $ \case

 76 |   MagicDebugInfo di => Just di

 77 |   _ => Nothing

 80 | eoi : EmptyRule ()

 81 | eoi = ignore $ nextIs "Expected end of input" isEOI

 82 |   where

 83 |     isEOI : Token -> Bool

 84 |     isEOI EndInput = True

 85 |     isEOI _ = False

 88 | constant : Rule Constant

 90 |     = terminal "Expected constant" $ \case

 91 |         CharLit c    => Ch <$> getCharLit c

 92 |         DoubleLit d  => Just (Db d)

 93 |         IntegerLit i => Just (BI i)

 94 |         Ident s      => isConstantType (UN $ Basic s) >>=

 95 |                              \case WorldType => Nothing

 96 |                                    c         => Just $ PrT c

 97 |         _            => Nothing

 99 | documentation' : Rule String

100 | documentation' = terminal "Expected documentation comment" $

101 |                           \case

102 |                             DocComment d => Just d

103 |                             _ => Nothing

106 | decorationFromBounded : {a : Type} -> OriginDesc -> Decoration -> WithBounds a -> ASemanticDecoration

107 | decorationFromBounded {a = Name} fname decor bnds

108 |    = ((fname, start bnds, end bnds), decor, Just bnds.val)

109 | decorationFromBounded fname decor bnds

110 |    = ((fname, start bnds, end bnds), decor, Nothing)

112 | documentation : OriginDesc -> Rule String

113 | documentation fname

114 |   = do b <- bounds (some documentation')

115 |        actD (decorationFromBounded fname Comment b)

116 |        pure (unlines $ forget b.val)

119 | optDocumentation : OriginDesc -> EmptyRule String

120 | optDocumentation fname = option "" (documentation fname)

123 | intLit : Rule Integer

125 |     = terminal "Expected integer literal" $

126 |                \case

127 |                  IntegerLit i => Just i

128 |                  _ => Nothing

131 | onOffLit : Rule Bool

133 |     = terminal "Expected on or off" $

134 |                \case

135 |                  Ident "on" => Just True

136 |                  Ident "off" => Just False

137 |                  _ => Nothing

140 | simpleStrLit : Rule String

142 |     = terminal "Expected string literal" $

143 |                \case

144 |                  StringLit s => unescape 0 s

145 |                  _ => Nothing

149 | strLitLines : Rule (List1 String)

151 |     = terminal "Expected string literal" $

152 |                \case

153 |                  StringLit s => Just $ map pack (linesHelp [] (unpack s))

154 |                  _ => Nothing

155 |   where

156 |   linesHelp : List Char -> List Char -> List1 (List Char)

157 |   linesHelp [] [] = List1.singleton []

158 |   linesHelp acc [] = List1.singleton (reverse acc)

159 |   linesHelp acc ('\n' :: xs) = reverse ('\n' :: acc) `List1.cons` linesHelp [] xs

160 |   linesHelp acc ('\r' :: '\n' :: xs) = reverse ('\n' :: '\r' :: acc) `List1.cons` linesHelp [] xs

161 |   linesHelp acc ('\r' :: xs) = reverse ('\r' :: acc) `List1.cons` linesHelp [] xs

162 |   linesHelp acc (c :: xs) = linesHelp (c :: acc) xs

165 | strBegin : Rule Nat

166 | strBegin = terminal "Expected string begin" $

167 |                     \case

168 |                       StringBegin hashtag Single => Just hashtag

169 |                       _ => Nothing

172 | multilineBegin : Rule Nat

173 | multilineBegin = terminal "Expected multiline string begin" $

174 |                           \case

175 |                             StringBegin hashtag Multi => Just hashtag

176 |                             _ => Nothing

179 | strEnd : Rule ()

180 | strEnd = terminal "Expected string end" $

181 |                   \case

182 |                     StringEnd => Just ()

183 |                     _ => Nothing

186 | interpBegin : Rule ()

187 | interpBegin = terminal "Expected string interp begin" $

188 |                        \case

189 |                          InterpBegin => Just ()

190 |                          _ => Nothing

193 | interpEnd : Rule ()

194 | interpEnd = terminal "Expected string interp end" $

195 |                      \case

196 |                        InterpEnd => Just ()

197 |                        _ => Nothing

200 | simpleStr : Rule String

201 | simpleStr = strBegin *> commit *> (option "" simpleStrLit) <* strEnd

204 | simpleMultiStr : Rule String

205 | simpleMultiStr = multilineBegin *> commit *> (option "" simpleStrLit) <* strEnd

208 | aDotIdent : Rule String

209 | aDotIdent = terminal "Expected dot+identifier" $

210 |                      \case

211 |                        DotIdent s => Just s

212 |                        _ => Nothing

215 | postfixProj : Rule Name

216 | postfixProj = UN . Field <$> aDotIdent

219 | symbol : String -> Rule ()

220 | symbol req

221 |     = terminal ("Expected '" ++ req ++ "'") $

222 |                \case

223 |                  Symbol s => guard (s == req)

224 |                  _ => Nothing

227 | anyReservedSymbol : Rule String

229 |   = terminal ("Expected a reserved symbol") $

230 |                \case

231 |                  Symbol s => s <$ guard (s `elem` reservedSymbols)

232 |                  _ => Nothing

235 | anyKeyword : Rule String

237 |   = terminal ("Expected a keyword") $

238 |              \case

239 |                Keyword s => Just s

240 |                _ => Nothing

243 | keyword : String -> Rule ()

244 | keyword req

245 |     = terminal ("Expected '" ++ req ++ "'") $

246 |                \case

247 |                  Keyword s => guard (s == req)

248 |                  _ => Nothing

251 | exactIdent : String -> Rule ()

252 | exactIdent req

253 |     = terminal ("Expected " ++ req) $

254 |                \case

255 |                  Ident s => guard (s == req)

256 |                  _ => Nothing

259 | pragma : String -> Rule ()

260 | pragma n =

261 |   terminal ("Expected pragma " ++ n) $

262 |     \case

263 |       Pragma s => guard (s == n)

264 |       _ => Nothing

267 | cgDirective : Rule String

268 | cgDirective =

269 |   terminal "Expected CG directive" $

270 |     \case

271 |       CGDirective d => Just d

272 |       _ => Nothing

275 | builtinType : Rule BuiltinType

276 | builtinType =

277 |     BuiltinNatural <$ exactIdent "Natural"

278 |     <|> NaturalToInteger <$ exactIdent "NaturalToInteger"

279 |     <|> IntegerToNatural <$ exactIdent "IntegerToNatural"

281 | operatorCandidate : Rule Name

283 |     = terminal "Expected operator" $

284 |                \case

285 |                  Symbol s => Just (UN $ Basic s) -- TODO: have an operator construct?

286 |                  _ => Nothing

289 | unqualifiedOperatorName : Rule String

291 |     = terminal "Expected operator" $

292 |                \case

293 |                  Symbol s => s <$ guard (not $ s `elem` reservedSymbols)

294 |                  _ => Nothing

297 | operator : Rule Name

298 | operator = UN . Basic <$> unqualifiedOperatorName

299 |                -- ^ TODO: add an operator constructor?

301 | identPart : Rule String

303 |     = terminal "Expected name" $

304 |                \case

305 |                  Ident str => Just str

306 |                  _ => Nothing

309 | namespacedIdent : Rule (Maybe Namespace, String)

311 |     = terminal "Expected namespaced name" $

312 |                \case

313 |                  DotSepIdent ns n => Just (Just ns, n)

314 |                  Ident i => Just (Nothing, i)

315 |                  _ => Nothing

317 | isCapitalisedIdent : WithBounds String -> EmptyRule ()

318 | isCapitalisedIdent str =

319 |   let val = str.val

320 |       loc = str.bounds

321 |       err : EmptyRule ()

322 |           = failLoc loc ("Expected a capitalised identifier, got: \{val}")

323 |   in case strM val of

324 |        StrNil => err

325 |        StrCons c _ => if (isUpper c || c > chr 160) then pure () else err

328 | namespaceId : Rule Namespace

329 | namespaceId = do

330 |   nsid <- bounds namespacedIdent

331 |   isCapitalisedIdent (snd <$> nsid)

332 |   pure (uncurry mkNestedNamespace nsid.val)

335 | namespacedSymbol : String -> Rule (Maybe Namespace)

336 | namespacedSymbol req = do

337 |   (symbol req $> Nothing) <|> do

338 |     ns <- namespaceId

339 |     symbol ("." ++ req)

340 |     pure (Just ns)

343 | moduleIdent : Rule ModuleIdent

344 | moduleIdent = nsAsModuleIdent <$> namespaceId

347 | unqualifiedName : Rule String

348 | unqualifiedName = identPart

351 | userName : Rule Name

352 | userName = UN . Basic <$> unqualifiedName

355 | holeName : Rule String

357 |     = terminal "Expected hole name" $

358 |                \case

359 |                  HoleIdent str => Just str

360 |                  _ => Nothing

362 | reservedNames : List String

364 |     = [ "Type", "Int", "Int8", "Int16", "Int32", "Int64", "Integer"

365 |       , "Bits8", "Bits16", "Bits32", "Bits64"

366 |       , "String", "Char", "Double", "Lazy", "Inf", "Force", "Delay"

367 |       ]

370 | anyReservedIdent : Rule (WithBounds String)

371 | anyReservedIdent = do

372 |     id <- bounds identPart

373 |     unless (id.val `elem` reservedNames) $ failLoc id.bounds "Expected reserved identifier"

374 |     pure id

376 | isNotReservedName : WithBounds String -> EmptyRule ()

377 | isNotReservedName x

378 |     = when (x.val `elem` reservedNames) $

379 |         failLoc x.bounds $ "Can't use reserved name \{x.val}"

381 | isNotReservedSymbol : WithBounds String -> EmptyRule ()

382 | isNotReservedSymbol x

383 |     = when (x.val `elem` reservedSymbols) $

384 |         failLoc x.bounds $ "Can't use reserved symbol \{x.val}"

387 | opNonNS : Rule Name

388 | opNonNS = do

389 |   symbol "("

390 |   commit

391 |   id <- bounds (operatorCandidate <|> postfixProj)

392 |   isNotReservedSymbol (nameRoot <$> id)

393 |   symbol ")"

394 |   pure id.val

396 | identWithCapital : (capitalised : Bool) -> WithBounds String ->

397 |                    EmptyRule ()

398 | identWithCapital b x = when b (isCapitalisedIdent x)

400 | nameWithCapital : (capitalised : Bool) -> Rule Name

401 | nameWithCapital b = opNonNS <|> do

402 |   nsx <- bounds namespacedIdent

403 |   opNS nsx <|> nameNS nsx

404 |  where

406 |   nameNS : WithBounds (Maybe Namespace, String) -> EmptyRule Name

407 |   nameNS nsx = do

408 |     let id = snd <$> nsx

409 |     identWithCapital b id

410 |     isNotReservedName id

411 |     pure $ uncurry mkNamespacedName (map Basic nsx.val)

413 |   opNS : WithBounds (Maybe Namespace, String) -> Rule Name

414 |   opNS nsx = do

415 |     isCapitalisedIdent (snd <$> nsx)

416 |     let ns = uncurry mkNestedNamespace nsx.val

417 |     symbol ".("

418 |     n <- (operator <|> postfixProj)

419 |     symbol ")"

420 |     pure (NS ns n)

423 | fixityNS : Rule HidingDirective

424 | fixityNS = do

425 |   namespacePrefix <- bounds namespacedIdent

426 |   let nsVal = namespacePrefix.val

427 |   fx <- checkFixity (snd nsVal) namespacePrefix.bounds

428 |   symbol ".("

429 |   n <- unqualifiedOperatorName

430 |   symbol ")"

431 |   pure (HideFixity fx (NS (uncurry mkNestedNamespace nsVal) $ UN $ Basic n))

432 |   where

433 |     checkFixity : String -> Bounds -> EmptyRule Fixity

434 |     checkFixity "infixl" _ = pure InfixL

435 |     checkFixity "infixr" _ = pure InfixR

436 |     checkFixity "infix"  _ = pure Infix

437 |     checkFixity "prefix" _ = pure Prefix

438 |     checkFixity _ loc =  failLoc loc ""

441 | name : Rule Name

442 | name = nameWithCapital False

445 | capitalisedName : Rule Name

446 | capitalisedName = nameWithCapital True

449 | capitalisedIdent : Rule String

450 | capitalisedIdent = do

451 |   id <- bounds identPart

452 |   isCapitalisedIdent id

453 |   isNotReservedName id

454 |   pure id.val

457 | dataConstructorName : Rule Name

458 | dataConstructorName = opNonNS <|> (UN . Basic) <$> capitalisedIdent

460 | export %inline

461 | dataTypeName : Rule Name

462 | dataTypeName = opNonNS <|> capitalisedName

465 | IndentInfo : Type

466 | IndentInfo = Int

469 | init : IndentInfo

470 | init = 0

472 | continueF : EmptyRule () -> (indent : IndentInfo) -> EmptyRule ()

473 | continueF err indent

474 |     = do eoi; err

475 |   <|> do keyword "where"; err

476 |   <|> do col <- column

477 |          when (col <= indent)

478 |             err

482 | continue : (indent : IndentInfo) -> EmptyRule ()

483 | continue = continueF (fail "Unexpected end of expression")

487 | mustContinue : (indent : IndentInfo) -> Maybe String -> EmptyRule ()

488 | mustContinue indent Nothing

489 |    = continueF (fatalError "Unexpected end of expression") indent

490 | mustContinue indent (Just req)

491 |    = continueF (fatalError ("Expected '" ++ req ++ "'")) indent

493 | data ValidIndent =

494 |   |||  In {}, entries can begin in any column

495 |   AnyIndent |

496 |   ||| Entry must begin in a specific column

497 |   AtPos Int |

498 |   ||| Entry can begin in this column or later

499 |   AfterPos Int |

500 |   ||| Block is finished

501 |   EndOfBlock

503 | Show ValidIndent where

504 |   show AnyIndent = "[any]"

505 |   show (AtPos i) = "[col " ++ show i ++ "]"

506 |   show (AfterPos i) = "[after " ++ show i ++ "]"

507 |   show EndOfBlock = "[EOB]"

509 | checkValid : ValidIndent -> Int -> EmptyRule ()

510 | checkValid AnyIndent c = pure ()

511 | checkValid (AtPos x) c = unless (c == x) $ fail "Invalid indentation"

512 | checkValid (AfterPos x) c = unless (c >= x) $ fail "Invalid indentation"

513 | checkValid EndOfBlock c = fail "End of block"

516 | isTerminator : Token -> Bool

517 | isTerminator (Symbol ",") = True

518 | isTerminator (Symbol "]") = True

519 | isTerminator (Symbol ";") = True

520 | isTerminator (Symbol "}") = True

521 | isTerminator (Symbol ")") = True

522 | isTerminator (Symbol "|") = True

523 | isTerminator (Symbol "**") = True

524 | isTerminator (Keyword "in") = True

525 | isTerminator (Keyword "then") = True

526 | isTerminator (Keyword "else") = True

527 | isTerminator (Keyword "where") = True

528 | isTerminator InterpEnd = True

529 | isTerminator EndInput = True

530 | isTerminator _ = False

537 | atEnd : (indent : IndentInfo) -> EmptyRule ()

538 | atEnd indent

539 |     = eoi

540 |   <|> do ignore $ nextIs "Expected end of block" isTerminator

541 |   <|> do col <- column

542 |          when (not (col <= indent))

543 |             $ fail "Not the end of a block entry"

547 | atEndIndent : (indent : IndentInfo) -> EmptyRule ()

548 | atEndIndent indent

549 |     = eoi

550 |   <|> do col <- column

551 |          when (not (col <= indent))

552 |             $ fail "Not the end of a block entry"

557 | terminator : ValidIndent -> Int -> EmptyRule ValidIndent

558 | terminator valid laststart

559 |     = do eoi

560 |          pure EndOfBlock

561 |   <|> do symbol ";"

562 |          pure (afterSemi valid)

563 |   <|> do col <- column

564 |          afterDedent valid col

565 |   <|> pure EndOfBlock

566 |  where

567 |    -- Expected indentation for the next token can either be anything (if

568 |    -- we're inside a brace delimited block) or anywhere after the initial

569 |    -- column (if we're inside an indentation delimited block)

570 |    afterSemi : ValidIndent -> ValidIndent

571 |    afterSemi AnyIndent = AnyIndent -- in braces, anything goes

572 |    afterSemi (AtPos c) = AfterPos c -- not in braces, after the last start position

573 |    afterSemi (AfterPos c) = AfterPos c

574 |    afterSemi EndOfBlock = EndOfBlock

576 |    -- Expected indentation for the next token can either be anything (if

577 |    -- we're inside a brace delimited block) or in exactly the initial column

578 |    -- (if we're inside an indentation delimited block)

579 |    afterDedent : ValidIndent -> Int -> EmptyRule ValidIndent

580 |    afterDedent AnyIndent col

581 |        = if col <= laststart

582 |             then pure AnyIndent

583 |             else fail "Not the end of a block entry"

584 |    afterDedent (AfterPos c) col

585 |        = if col <= laststart

586 |             then pure (AtPos c)

587 |             else fail "Not the end of a block entry"

588 |    afterDedent (AtPos c) col

589 |        = if col <= laststart

590 |             then pure (AtPos c)

591 |             else fail "Not the end of a block entry"

592 |    afterDedent EndOfBlock col = pure EndOfBlock

595 | blockEntry : ValidIndent -> (IndentInfo -> Rule ty) ->

596 |              Rule (ty, ValidIndent)

597 | blockEntry valid rule

598 |     = do col <- column

599 |          checkValid valid col

600 |          p <- rule col

601 |          valid' <- terminator valid col

602 |          pure (p, valid')

604 | blockEntries : ValidIndent -> (IndentInfo -> Rule ty) ->

605 |                EmptyRule (List ty)

606 | blockEntries valid rule

607 |      = do eoi; pure []

608 |    <|> do res <- blockEntry valid rule

609 |           ts <- blockEntries (snd res) rule

610 |           pure (fst res :: ts)

611 |    <|> pure []

614 | block : (IndentInfo -> Rule ty) -> EmptyRule (List ty)

615 | block item

616 |     = do symbol "{"

617 |          commit

618 |          ps <- blockEntries AnyIndent item

619 |          symbol "}"

620 |          pure ps

621 |   <|> do col <- column

622 |          blockEntries (AtPos col) item

630 | blockAfter : Int -> (IndentInfo -> Rule ty) -> EmptyRule (List ty)

631 | blockAfter mincol item

632 |     = do symbol "{"

633 |          commit

634 |          ps <- blockEntries AnyIndent item

635 |          symbol "}"

636 |          pure ps

637 |   <|> do col <- column

638 |          ifThenElse (col <= mincol)

639 |             (pure [])

640 |             $ blockEntries (AtPos col) item

643 | blockWithOptHeaderAfter :

644 |    (column : Int) ->

645 |    (header : IndentInfo -> Rule hd) ->

646 |    (item : IndentInfo -> Rule ty) ->

647 |    EmptyRule (Maybe hd, List ty)

648 | blockWithOptHeaderAfter {ty} mincol header item

649 |     = do symbol "{"

650 |          commit

651 |          hidt <- optional $ blockEntry AnyIndent header

652 |          restOfBlock hidt

653 |   <|> do col <- column

654 |          ifThenElse (col <= mincol)

655 |             (pure (Nothing, []))

656 |             $ do hidt <- optional $ blockEntry (AtPos col) header

657 |                  ps <- blockEntries (AtPos col) item

658 |                  pure (map fst hidt, ps)

659 |   where

660 |   restOfBlock : Maybe (hd, ValidIndent) -> Rule (Maybe hd, List ty)

661 |   restOfBlock (Just (h, idt)) = do ps <- blockEntries idt item

662 |                                    symbol "}"

663 |                                    pure (Just h, ps)

664 |   restOfBlock Nothing = do ps <- blockEntries AnyIndent item

665 |                            symbol "}"

666 |                            pure (Nothing, ps)

669 | nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List1 ty)

670 | nonEmptyBlock item

671 |     = do symbol "{"

672 |          commit

673 |          res <- blockEntry AnyIndent item

674 |          ps <- blockEntries (snd res) item

675 |          symbol "}"

676 |          pure (fst res ::: ps)

677 |   <|> do col <- column

678 |          res <- blockEntry (AtPos col) item

679 |          ps <- blockEntries (snd res) item

680 |          pure (fst res ::: ps)

687 | nonEmptyBlockAfter : Int -> (IndentInfo -> Rule ty) -> Rule (List1 ty)

688 | nonEmptyBlockAfter mincol item

689 |     = do symbol "{"

690 |          commit

691 |          res <- blockEntry AnyIndent item

692 |          ps <- blockEntries (snd res) item

693 |          symbol "}"

694 |          pure (fst res ::: ps)

695 |   <|> do col <- column

696 |          let False = col <= mincol

697 |             | True => fatalError "Expected an indented non-empty block"

698 |          res <- blockEntry (AtPos col) item

699 |          ps <- blockEntries (snd res) item

700 |          pure (fst res ::: ps)