0 | module TTImp.Parser

  2 | import Core.Context

  3 | import Parser.Source

  4 | import TTImp.TTImp

  6 | import public Libraries.Text.Parser

  7 | import Libraries.Data.WithDefault

  9 | withFC : (fname : OriginDesc) => Rule a -> Rule (WithFC a)

 10 | withFC parser = do

 11 |   start <- location

 12 |   parsed <- parser

 13 |   end <- location

 14 |   pure (Mk [MkFC fname start end] parsed)

 16 | topDecl : OriginDesc -> IndentInfo -> Rule ImpDecl

 20 | collectDefs : List ImpDecl -> List ImpDecl

 22 | %default covering

 24 | %hide Prelude.(>>=)

 25 | %hide Prelude.(>>)

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

 27 | %hide Prelude.pure

 28 | %hide Core.Core.pure

 30 | %hide Lexer.Core.(<|>)

 31 | %hide Prelude.(<|>)

 33 | atom : OriginDesc -> Rule RawImp

 34 | atom fname

 35 |     = do start <- location

 36 |          x <- constant

 37 |          end <- location

 38 |          pure (IPrimVal (MkFC fname start end) x)

 39 |   <|> do start <- location

 40 |          str <- simpleStr

 41 |          end <- location

 42 |          pure (IPrimVal (MkFC fname start end) (Str str))

 43 |   <|> do start <- location

 44 |          exactIdent "Type"

 45 |          end <- location

 46 |          pure (IType (MkFC fname start end))

 47 |   <|> do start <- location

 48 |          symbol "_"

 49 |          end <- location

 50 |          pure (Implicit (MkFC fname start end) True)

 51 |   <|> do start <- location

 52 |          symbol "?"

 53 |          end <- location

 54 |          pure (Implicit (MkFC fname start end) False)

 55 |   <|> do start <- location

 56 |          pragma "search"

 57 |          end <- location

 58 |          pure (ISearch (MkFC fname start end) 1000)

 59 |   <|> do start <- location

 60 |          x <- name

 61 |          end <- location

 62 |          pure (IVar (MkFC fname start end) x)

 63 |   <|> do start <- location

 64 |          symbol "$"

 65 |          x <- userName

 66 |          end <- location

 67 |          pure (IBindVar (MkFC fname start end) x)

 68 |   <|> do start <- location

 69 |          x <- holeName

 70 |          end <- location

 71 |          pure (IHole (MkFC fname start end) x)

 73 | visOption : Rule Visibility

 75 |     = do keyword "public"

 76 |          keyword "export"

 77 |          pure Public

 78 |   <|> do keyword "export"

 79 |          pure Export

 80 |   <|> do keyword "private"

 81 |          pure Private

 83 | visibility : EmptyRule (WithDefault Visibility Private)

 85 |     = (specified <$> visOption)

 86 |   <|> pure defaulted

 88 | totalityOpt : Rule TotalReq

 90 |     = do keyword "partial"

 91 |          pure PartialOK

 92 |   <|> do keyword "total"

 93 |          pure Total

 94 |   <|> do keyword "covering"

 95 |          pure CoveringOnly

 97 | dataVisOpt : EmptyRule (WithDefault Visibility Private, Maybe TotalReq)

 99 |     = do { vis <- visOption   ; mbtot <- optional totalityOpt ; pure (specified vis, mbtot) }

100 |   <|> do { tot <- totalityOpt ; vis <- visibility ; pure (vis, Just tot) }

101 |   <|> pure (defaulted, Nothing)

103 | fnOpt : Rule FnOpt

104 | fnOpt = do x <- totalityOpt

105 |            pure $ Totality x

107 | fnDirectOpt : Rule FnOpt

109 |     = do pragma "hint"

110 |          pure (Hint True)

111 |   <|> do pragma "chaser"

112 |          pure (Hint False)

113 |   <|> do pragma "globalhint"

114 |          pure (GlobalHint True)

115 |   <|> do pragma "defaulthint"

116 |          pure (GlobalHint False)

117 |   <|> do pragma "inline"

118 |          pure Inline

119 |   <|> do pragma "noinline"

120 |          pure NoInline

121 |   <|> do pragma "deprecate"

122 |          pure Deprecate

123 |   <|> do pragma "extern"

124 |          pure ExternFn

126 | visOpt : Rule (Either Visibility FnOpt)

128 |     = do vis <- visOption

129 |          pure (Left vis)

130 |   <|> do tot <- fnOpt

131 |          pure (Right tot)

132 |   <|> do opt <- fnDirectOpt

133 |          pure (Right opt)

135 | getVisibility : Maybe Visibility -> List (Either Visibility FnOpt) ->

136 |                 EmptyRule Visibility

137 | getVisibility Nothing [] = pure Private

138 | getVisibility (Just vis) [] = pure vis

139 | getVisibility Nothing (Left x :: xs) = getVisibility (Just x) xs

140 | getVisibility (Just vis) (Left x :: xs)

141 |    = fatalError "Multiple visibility modifiers"

142 | getVisibility v (_ :: xs) = getVisibility v xs

144 | getRight : Either a b -> Maybe b

145 | getRight (Left _) = Nothing

146 | getRight (Right v) = Just v

148 | bindSymbol : Rule (PiInfo RawImp)

150 |     = do symbol "->"

151 |          pure Explicit

152 |   <|> do symbol "=>"

153 |          pure AutoImplicit

156 |   appExpr : OriginDesc -> IndentInfo -> Rule RawImp

157 |   appExpr fname indents

158 |       = case_ fname indents

159 |     <|> lazy fname indents

160 |     <|> do start <- location

161 |            f <- simpleExpr fname indents

162 |            args <- many (argExpr fname indents)

163 |            end <- location

164 |            pure (applyExpImp start end f args)

165 |     where

166 |       applyExpImp : FilePos -> FilePos ->

167 |                     RawImp -> List (Either RawImp (Maybe Name, RawImp)) ->

168 |                     RawImp

169 |       applyExpImp start end f [] = f

170 |       applyExpImp start end f (Left exp :: args)

171 |           = applyExpImp start end (IApp (MkFC fname start end) f exp) args

172 |       applyExpImp start end f (Right (Just n, imp) :: args)

173 |           = applyExpImp start end (INamedApp (MkFC fname start end) f n imp) args

174 |       applyExpImp start end f (Right (Nothing, imp) :: args)

175 |           = applyExpImp start end (IAutoApp (MkFC fname start end) f imp) args

177 |   argExpr : OriginDesc -> IndentInfo ->

178 |             Rule (Either RawImp (Maybe Name, RawImp))

179 |   argExpr fname indents

180 |       = do continue indents

181 |            arg <- simpleExpr fname indents

182 |            pure (Left arg)

183 |     <|> do continue indents

184 |            arg <- implicitArg fname indents

185 |            pure (Right arg)

187 |   implicitArg : OriginDesc -> IndentInfo -> Rule (Maybe Name, RawImp)

188 |   implicitArg fname indents

189 |       = do start <- location

190 |            symbol "{"

191 |            x <- userName

192 |            (do symbol "="

193 |                commit

194 |                tm <- expr fname indents

195 |                symbol "}"

196 |                pure (Just x, tm))

197 |              <|> (do symbol "}"

198 |                      end <- location

199 |                      pure (Just x, IVar (MkFC fname start end) x))

200 |     <|> do symbol "@{"

201 |            commit

202 |            tm <- expr fname indents

203 |            symbol "}"

204 |            pure (Nothing, tm)

206 |   as : OriginDesc -> IndentInfo -> Rule RawImp

207 |   as fname indents

208 |       = do start <- location

209 |            x <- userName

210 |            nameEnd <- location

211 |            symbol "@"

212 |            pat <- simpleExpr fname indents

213 |            end <- location

214 |            pure (IAs (MkFC fname start end) (MkFC fname start nameEnd) UseRight x pat)

216 |   simpleExpr : OriginDesc -> IndentInfo -> Rule RawImp

217 |   simpleExpr fname indents

218 |       = as fname indents

219 |     <|> atom fname

220 |     <|> binder fname indents

221 |     <|> rewrite_ fname indents

222 |     <|> record_ fname indents

223 |     <|> do symbol "("

224 |            e <- expr fname indents

225 |            symbol ")"

226 |            pure e

228 |   multiplicity : EmptyRule (Maybe Integer)

229 |   multiplicity

230 |       = do c <- intLit

231 |            pure (Just c)

232 |     <|> pure Nothing

234 |   getMult : Maybe Integer -> EmptyRule RigCount

235 |   getMult (Just 0) = pure erased

236 |   getMult (Just 1) = pure linear

237 |   getMult Nothing = pure top

238 |   getMult _ = fatalError "Invalid multiplicity (must be 0 or 1)"

240 |   pibindAll : FC -> PiInfo RawImp -> List (WithRig $ WithMName RawImp) ->

241 |               RawImp -> RawImp

242 |   pibindAll fc p [] scope = scope

243 |   pibindAll fc p (ty :: rest) scope

244 |            = IPi fc ty.rig p (map val ty.mName) ty.val (pibindAll fc p rest scope)

246 |   bindList : OriginDesc -> FilePos -> IndentInfo ->

247 |              Rule (List (RigCount, Name, RawImp))

248 |   bindList fname start indents

249 |       = forget <$> sepBy1 (symbol ",")

250 |                           (do rigc <- multiplicity

251 |                               n <- userName

252 |                               end <- location

253 |                               ty <- option

254 |                                        (Implicit (MkFC fname start end) False)

255 |                                        (do symbol ":"

256 |                                            appExpr fname indents)

257 |                               rig <- getMult rigc

258 |                               pure (rig, n, ty))

261 |   pibindListName : OriginDesc -> FilePos -> IndentInfo ->

262 |                    Rule (List (WithRig $ WithName RawImp))

263 |   pibindListName fname start indents

264 |        = do rigc <- multiplicity

265 |             ns <- sepBy1 (symbol ",") (withFC userName)

266 |             symbol ":"

267 |             ty <- expr fname indents

268 |             atEnd indents

269 |             rig <- getMult rigc

270 |             pure (map (\n => Mk [rig, n] ty) (forget ns))

271 |      <|> forget <$> sepBy1 (symbol ",")

272 |                            (do rigc <- multiplicity

273 |                                n <- withFC name

274 |                                symbol ":"

275 |                                ty <- expr fname indents

276 |                                rig <- getMult rigc

277 |                                pure (Mk [rig, n] ty))

279 |   pibindList : OriginDesc -> FilePos -> IndentInfo ->

280 |                Rule (List (WithRig $ WithMName RawImp))

281 |   pibindList fname start indents

282 |     = do params <- pibindListName fname start indents

283 |          pure $ map (\ty => Mk [ty.rig, Just ty.name] ty.val) params

286 |   autoImplicitPi : OriginDesc -> IndentInfo -> Rule RawImp

287 |   autoImplicitPi fname indents

288 |       = do start <- location

289 |            symbol "{"

290 |            keyword "auto"

291 |            commit

292 |            binders <- pibindList fname start indents

293 |            symbol "}"

294 |            symbol "->"

295 |            scope <- typeExpr fname indents

296 |            end <- location

297 |            pure (pibindAll (MkFC fname start end) AutoImplicit binders scope)

299 |   forall_ : OriginDesc -> IndentInfo -> Rule RawImp

300 |   forall_ fname indents

301 |       = do start <- location

302 |            keyword "forall"

303 |            commit

304 |            nstart <- location

305 |            ns <- sepBy1 (symbol ",") (withFC userName)

306 |            nend <- location

307 |            let nfc = MkFC fname nstart nend

308 |            let binders = map (\n => Mk [erased {a=RigCount}, Just n]

309 |                                        (Implicit nfc False))

310 |                              (forget ns)

311 |            symbol "."

312 |            scope <- typeExpr fname indents

313 |            end <- location

314 |            pure (pibindAll (MkFC fname start end) Implicit binders scope)

316 |   implicitPi : OriginDesc -> IndentInfo -> Rule RawImp

317 |   implicitPi fname indents

318 |       = do start <- location

319 |            symbol "{"

320 |            binders <- pibindList fname start indents

321 |            symbol "}"

322 |            symbol "->"

323 |            scope <- typeExpr fname indents

324 |            end <- location

325 |            pure (pibindAll (MkFC fname start end) Implicit binders scope)

327 |   explicitPi : OriginDesc -> IndentInfo -> Rule RawImp

328 |   explicitPi fname indents

329 |       = do start <- location

330 |            symbol "("

331 |            binders <- pibindList fname start indents

332 |            symbol ")"

333 |            exp <- bindSymbol

334 |            scope <- typeExpr fname indents

335 |            end <- location

336 |            pure (pibindAll (MkFC fname start end) exp binders scope)

338 |   lam : OriginDesc -> IndentInfo -> Rule RawImp

339 |   lam fname indents

340 |       = do start <- location

341 |            symbol "\\"

342 |            binders <- bindList fname start indents

343 |            symbol "=>"

344 |            mustContinue indents Nothing

345 |            scope <- expr fname indents

346 |            end <- location

347 |            pure (bindAll (MkFC fname start end) binders scope)

348 |      where

349 |        bindAll : FC -> List (RigCount, Name, RawImp) -> RawImp -> RawImp

350 |        bindAll fc [] scope = scope

351 |        bindAll fc ((rig, n, ty) :: rest) scope

352 |            = ILam fc rig Explicit (Just n) ty (bindAll fc rest scope)

354 |   let_ : OriginDesc -> IndentInfo -> Rule RawImp

355 |   let_ fname indents

356 |       = do start <- location

357 |            keyword "let"

358 |            rigc <- multiplicity

359 |            rig <- getMult rigc

360 |            n <- bounds name

361 |            symbol "="

362 |            commit

363 |            val <- expr fname indents

364 |            continue indents

365 |            keyword "in"

366 |            scope <- typeExpr fname indents

367 |            end <- location

368 |            pure (let fc = MkFC fname start end in

369 |                      ILet fc (boundToFC fname n) rig n.val (Implicit fc False) val scope)

370 |     <|> do start <- location

371 |            keyword "let"

372 |            ds <- block (topDecl fname)

373 |            continue indents

374 |            keyword "in"

375 |            scope <- typeExpr fname indents

376 |            end <- location

377 |            pure (ILocal (MkFC fname start end) (collectDefs ds) scope)

379 |   case_ : OriginDesc -> IndentInfo -> Rule RawImp

380 |   case_ fname indents

381 |       = do start <- location

382 |            opts <- many fnOpt

383 |            keyword "case"

384 |            scr <- expr fname indents

385 |            keyword "of"

386 |            alts <- block (caseAlt fname)

387 |            end <- location

388 |            pure (let fc = MkFC fname start end in

389 |                      ICase fc opts scr (Implicit fc False) alts)

391 |   caseAlt : OriginDesc -> IndentInfo -> Rule ImpClause

392 |   caseAlt fname indents

393 |       = do start <- location

394 |            lhs <- appExpr fname indents

395 |            caseRHS fname indents start lhs

397 |   caseRHS : OriginDesc -> IndentInfo -> (Int, Int) -> RawImp ->

398 |             Rule ImpClause

399 |   caseRHS fname indents start lhs

400 |       = do symbol "=>"

401 |            continue indents

402 |            rhs <- expr fname indents

403 |            atEnd indents

404 |            end <- location

405 |            pure (PatClause (MkFC fname start end) lhs rhs)

406 |     <|> do keyword "impossible"

407 |            atEnd indents

408 |            end <- location

409 |            pure (ImpossibleClause (MkFC fname start end) lhs)

411 |   record_ : OriginDesc -> IndentInfo -> Rule RawImp

412 |   record_ fname indents

413 |       = do start <- location

414 |            keyword "record"

415 |            symbol "{"

416 |            commit

417 |            fs <- sepBy1 (symbol ",") (field fname indents)

418 |            symbol "}"

419 |            sc <- expr fname indents

420 |            end <- location

421 |            pure (IUpdate (MkFC fname start end) (forget fs) sc)

423 |   field : OriginDesc -> IndentInfo -> Rule IFieldUpdate

424 |   field fname indents

425 |       = do path <- sepBy1 (symbol "->") unqualifiedName

426 |            upd <- (do symbol "="; pure ISetField)

427 |                       <|>

428 |                   (do symbol "$="; pure ISetFieldApp)

429 |            val <- appExpr fname indents

430 |            pure (upd (forget path) val)

432 |   rewrite_ : OriginDesc -> IndentInfo -> Rule RawImp

433 |   rewrite_ fname indents

434 |       = do start <- location

435 |            keyword "rewrite"

436 |            rule <- expr fname indents

437 |            keyword "in"

438 |            tm <- expr fname indents

439 |            end <- location

440 |            pure (IRewrite (MkFC fname start end) rule tm)

442 |   lazy : OriginDesc -> IndentInfo -> Rule RawImp

443 |   lazy fname indents

444 |       = do start <- location

445 |            exactIdent "Lazy"

446 |            tm <- simpleExpr fname indents

447 |            end <- location

448 |            pure (IDelayed (MkFC fname start end) LLazy tm)

449 |     <|> do start <- location

450 |            exactIdent "Inf"

451 |            tm <- simpleExpr fname indents

452 |            end <- location

453 |            pure (IDelayed (MkFC fname start end) LInf tm)

454 |     <|> do start <- location

455 |            exactIdent "Delay"

456 |            tm <- simpleExpr fname indents

457 |            end <- location

458 |            pure (IDelay (MkFC fname start end) tm)

459 |     <|> do start <- location

460 |            exactIdent "Force"

461 |            tm <- simpleExpr fname indents

462 |            end <- location

463 |            pure (IForce (MkFC fname start end) tm)

466 |   binder : OriginDesc -> IndentInfo -> Rule RawImp

467 |   binder fname indents

468 |       = autoImplicitPi fname indents

469 |     <|> forall_ fname indents

470 |     <|> implicitPi fname indents

471 |     <|> explicitPi fname indents

472 |     <|> lam fname indents

473 |     <|> let_ fname indents

475 |   typeExpr : OriginDesc -> IndentInfo -> Rule RawImp

476 |   typeExpr fname indents

477 |       = do start <- location

478 |            arg <- appExpr fname indents

479 |            (do continue indents

480 |                rest <- some (do exp <- bindSymbol

481 |                                 op <- appExpr fname indents

482 |                                 pure (exp, op))

483 |                end <- location

484 |                pure (mkPi start end arg (forget rest)))

485 |              <|> pure arg

486 |     where

487 |       mkPi : FilePos -> FilePos -> RawImp -> List (PiInfo RawImp, RawImp) -> RawImp

488 |       mkPi start end arg [] = arg

489 |       mkPi start end arg ((exp, a) :: as)

490 |             = IPi (MkFC fname start end) top exp Nothing arg

491 |                   (mkPi start end a as)

493 |   export

494 |   expr : OriginDesc -> IndentInfo -> Rule RawImp

495 |   expr = typeExpr

497 | tyDecl : OriginDesc -> IndentInfo -> Rule ImpTy

498 | tyDecl fname indents

499 |     = do start <- location

500 |          n <- withFC name

501 |          nameEnd <- location

502 |          symbol ":"

503 |          ty <- expr fname indents

504 |          end <- location

505 |          atEnd indents

506 |          let fc = MkFC fname start end

507 |          pure (Mk [fc, n] ty)

510 |   parseRHS : (withArgs : Nat) ->

511 |              OriginDesc -> IndentInfo -> (Int, Int) -> RawImp ->

512 |              Rule (Name, ImpClause)

513 |   parseRHS withArgs fname indents start lhs

514 |       = do symbol "="

515 |            commit

516 |            rhs <- expr fname indents

517 |            atEnd indents

518 |            end <- location

519 |            let fc = MkFC fname start end

520 |            pure (!(getFn lhs), PatClause fc lhs rhs)

521 |     <|> do keyword "with"

522 |            m <- multiplicity

523 |            rig <- getMult m

524 |            wstart <- location

525 |            symbol "("

526 |            wval <- expr fname indents

527 |            symbol ")"

528 |            prf <- optional $ do

529 |                     keyword "proof"

530 |                     pure (!(getMult !multiplicity), !name)

531 |            ws <- nonEmptyBlock (clause (S withArgs) fname)

532 |            end <- location

533 |            let fc = MkFC fname start end

534 |            pure (MkPair !(getFn lhs) $ WithClause fc lhs rig wval prf [] (forget $ map snd ws))

536 |     <|> do keyword "impossible"

537 |            atEnd indents

538 |            end <- location

539 |            let fc = MkFC fname start end

540 |            pure (!(getFn lhs), ImpossibleClause fc lhs)

541 |     where

542 |       getFn : RawImp -> EmptyRule Name

543 |       getFn (IVar _ n) = pure n

544 |       getFn (IApp _ f a) = getFn f

545 |       getFn (IAutoApp _ f a) = getFn f

546 |       getFn (INamedApp _ f _ a) = getFn f

547 |       getFn _ = fail "Not a function application"

549 |   clause : Nat -> OriginDesc -> IndentInfo -> Rule (Name, ImpClause)

550 |   clause withArgs fname indents

551 |       = do start <- location

552 |            lhs <- expr fname indents

553 |            extra <- many parseWithArg

554 |            ifThenElse (withArgs /= length extra)

555 |               (fatalError "Wrong number of 'with' arguments")

556 |               (parseRHS withArgs fname indents start (applyArgs lhs extra))

557 |     where

558 |       applyArgs : RawImp -> List (FC, RawImp) -> RawImp

559 |       applyArgs f [] = f

560 |       applyArgs f ((fc, a) :: args) = applyArgs (IApp fc f a) args

562 |       parseWithArg : Rule (FC, RawImp)

563 |       parseWithArg

564 |           = do symbol "|"

565 |                start <- location

566 |                tm <- expr fname indents

567 |                end <- location

568 |                pure (MkFC fname start end, tm)

570 | definition : OriginDesc -> IndentInfo -> Rule ImpDecl

571 | definition fname indents

572 |     = do start <- location

573 |          nd <- clause 0 fname indents

574 |          end <- location

575 |          pure (IDef (MkFC fname start end) (fst nd) [snd nd])

577 | dataOpt : Rule DataOpt

579 |     = do exactIdent "noHints"

580 |          pure NoHints

581 |   <|> do exactIdent "uniqueSearch"

582 |          pure UniqueSearch

583 |   <|> do exactIdent "search"

584 |          ns <- some name

585 |          pure (SearchBy ns)

587 | dataOpts : EmptyRule (List DataOpt)

588 | dataOpts = option [] $ do

589 |   symbol "["

590 |   dopts <- sepBy1 (symbol ",") dataOpt

591 |   symbol "]"

592 |   pure $ forget dopts

594 | dataDecl : OriginDesc -> IndentInfo -> Rule ImpData

595 | dataDecl fname indents

596 |     = do start <- location

597 |          keyword "data"

598 |          n <- name

599 |          symbol ":"

600 |          ty <- expr fname indents

601 |          keyword "where"

602 |          opts <- dataOpts

603 |          cs <- block (tyDecl fname)

604 |          end <- location

605 |          pure (MkImpData (MkFC fname start end) n (Just ty) opts cs)

607 | recordParam : OriginDesc -> IndentInfo -> Rule (List (ImpParameter' RawImp))

608 | recordParam fname indents

609 |     = do symbol "("

610 |          start <- location

611 |          params <- pibindListName fname start indents

612 |          symbol ")"

613 |          pure (map (map (MkPiBindData Explicit)) params)

614 |   <|> do symbol "{"

615 |          commit

616 |          start <- location

617 |          info <- (pure AutoImplicit <* keyword "auto"

618 |               <|>(do

619 |                   keyword "default"

620 |                   t <- simpleExpr fname indents

621 |                   pure $ DefImplicit t)

622 |               <|> pure      Implicit)

623 |          params <- pibindListName fname start indents

624 |          symbol "}"

625 |          pure (map (map (MkPiBindData info)) params)

626 |   <|> do n <- withFC name

627 |          pure [ Mk [top, n] (MkPiBindData Explicit (Implicit n.fc False)) ]

629 | fieldDecl : OriginDesc -> IndentInfo -> Rule (List IField)

630 | fieldDecl fname indents

631 |       = do symbol "{"

632 |            commit

633 |            fs <- fieldBody Implicit

634 |            symbol "}"

635 |            atEnd indents

636 |            pure fs

637 |     <|> do fs <- fieldBody Explicit

638 |            atEnd indents

639 |            pure fs

640 |   where

641 |     fieldBody : PiInfo RawImp -> Rule (List IField)

642 |     fieldBody p

643 |         = do start <- location

644 |              ns <- sepBy1 (symbol ",") (withFC userName)

645 |              symbol ":"

646 |              ty <- expr fname indents

647 |              end <- location

648 |              pure (map (\n => Mk [MkFC fname start end, linear, n]

649 |                                        (MkPiBindData p ty)) (forget ns))

651 | recordDecl : OriginDesc -> IndentInfo -> Rule ImpDecl

652 | recordDecl fname indents

653 |     = do start <- location

654 |          (vis,mbtot) <- dataVisOpt

655 |          col <- column

656 |          keyword "record"

657 |          commit

658 |          n <- withFC name

659 |          paramss <- many (recordParam fname indents)

660 |          let params = concat paramss

661 |          keyword "where"

662 |          opts <- dataOpts

663 |          exactIdent "constructor"

664 |          dc <- withFC name

665 |          flds <- assert_total (blockAfter col (fieldDecl fname))

666 |          end <- location

667 |          pure (let fc = MkFC fname start end

668 |                 in IRecord fc Nothing vis mbtot

669 |                            (Mk [fc] $ MkImpRecord (Mk [n] params) (Mk [dc, opts] (concat flds))))

671 | namespaceDecl : Rule Namespace

673 |     = do keyword "namespace"

674 |          commit

675 |          namespaceId

677 | logLevel : Rule (Maybe (List String, Nat))

679 |   = (Nothing <$ exactIdent "off")

680 |     <|> do topic <- option [] ((::) <$> unqualifiedName <*> many aDotIdent)

681 |            lvl <- intLit

682 |            pure (Just (topic, fromInteger lvl))

684 | directive : OriginDesc -> IndentInfo -> Rule ImpDecl

685 | directive fname indents

686 |     = do pragma "logging"

687 |          commit

688 |          lvl <- logLevel

689 |          atEnd indents

690 |          pure (ILog lvl)

691 |   <|> do b <- bounds (do pragma "builtin"

692 |                          commit

693 |                          t <- builtinType

694 |                          n <- name

695 |                          pure (t, n))

696 |          (t, n) <- pure b.val

697 |          pure $ IBuiltin (boundToFC fname b) t n

699 |          {- Can't do IPragma due to lack of Ref Ctxt. Should we worry about this?

720 | topDecl fname indents

721 |     = do start <- location

722 |          (vis,mbtot) <- dataVisOpt

723 |          dat <- dataDecl fname indents

724 |          end <- location

725 |          pure (IData (MkFC fname start end) vis mbtot dat)

726 |   <|> do start <- location

727 |          ns <- namespaceDecl

728 |          ds <- assert_total (nonEmptyBlock (topDecl fname))

729 |          end <- location

730 |          pure (INamespace (MkFC fname start end) ns (forget ds))

731 |   <|> do start <- location

732 |          visOpts <- many visOpt

733 |          vis <- getVisibility Nothing visOpts

734 |          let opts = mapMaybe getRight visOpts

735 |          m <- multiplicity

736 |          rig <- getMult m

737 |          claim <- tyDecl fname indents

738 |          end <- location

739 |          pure (IClaim (MkFCVal (MkFC fname start end) $ MkIClaimData  rig vis opts claim))

740 |   <|> recordDecl fname indents

741 |   <|> directive fname indents

742 |   <|> definition fname indents

746 | collectDefs [] = []

747 | collectDefs (IDef loc fn cs :: ds)

748 |     = let (cs', rest) = spanMap (isClause fn) ds in

749 |           IDef loc fn (cs ++ cs') :: assert_total (collectDefs rest)

750 |   where

751 |     spanMap : (a -> Maybe (List b)) -> List a -> (List b, List a)

752 |     spanMap f [] = ([], [])

753 |     spanMap f (x :: xs) = case f x of

754 |                                Nothing => ([], x :: xs)

755 |                                Just y => case spanMap f xs of

756 |                                               (ys, zs) => (y ++ ys, zs)

758 |     isClause : Name -> ImpDecl -> Maybe (List ImpClause)

759 |     isClause n (IDef _ n' cs)

760 |         = if n == n' then Just cs else Nothing

761 |     isClause n _ = Nothing

762 | collectDefs (INamespace loc ns nds :: ds)

763 |     = INamespace loc ns (collectDefs nds) :: collectDefs ds

764 | collectDefs (IFail loc msg nds :: ds)

765 |     = IFail loc msg (collectDefs nds) :: collectDefs ds

766 | collectDefs (d :: ds)

767 |     = d :: collectDefs ds

771 | prog : OriginDesc -> Rule (List ImpDecl)

772 | prog fname

773 |     = do ds <- nonEmptyBlock (topDecl fname)

774 |          pure (collectDefs $ forget ds)

778 | command : Rule ImpREPL

780 |     = do symbol ":"; exactIdent "t"

781 |          tm <- expr (Virtual Interactive) init

782 |          pure (Check tm)

783 |   <|> do symbol ":"; exactIdent "s"

784 |          n <- name

785 |          pure (ProofSearch n)

786 |   <|> do symbol ":"; exactIdent "es"

787 |          n <- name

788 |          pure (ExprSearch n)

789 |   <|> do symbol ":"; exactIdent "gd"

790 |          l <- intLit

791 |          n <- name

792 |          pure (GenerateDef (fromInteger l) n)

793 |   <|> do symbol ":"; exactIdent "missing"

794 |          n <- name

795 |          pure (Missing n)

796 |   <|> do symbol ":"; keyword "total"

797 |          n <- name

798 |          pure (CheckTotal n)

799 |   <|> do symbol ":"; exactIdent "di"

800 |          n <- name

801 |          pure (DebugInfo n)

802 |   <|> do symbol ":"; exactIdent "q"

803 |          pure Quit

804 |   <|> do tm <- expr (Virtual Interactive) init

805 |          pure (Eval tm)