cc35585 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #688 from david-christiansen/haddock-on-test

cc35585Edwin Brady13 years ago

Makefile+1−1

compare with master

unifiedsplit

@@ -13,7 +13,7 @@ pinstall: dist/setup-config

13build: dist/setup-config

14 $(CABAL) build $(CABALFLAGS)

16−test:

16+test: doc

17 $(MAKE) -C test IDRIS=../dist/build/idris

19test_java:

src/Core/Evaluate.hs+1−1

@@ -767,7 +767,7 @@ addCasedef n ci@(CaseInfo alwaysInline tcdict)

767 OK (CaseDef args_ct sc_ct _),

768 OK (CaseDef args_inl sc_inl _),

769 OK (CaseDef args_rt sc_rt _)) ->

770− let inl = alwaysInline -- || tcdict

770+ let inl = alwaysInline -- tcdict

771 inlc = (inl || small n args_ct sc_ct) && (not asserted)

772 inlr = inl || small n args_rt sc_rt

773 cdef = CaseDefs (args_tot, sc_tot)

src/Idris/CaseSplit.hs+12−12

@@ -184,10 +184,10 @@ replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)

184

185replaceVar ctxt n t pat = pat

186

187−splitOnLine :: Int -- ^ line number

187+splitOnLine :: Int -- ^ line number

188− -> Name -- ^ variable

188+ -> Name -- ^ variable

189− -> FilePath -- ^ name of file

189+ -> FilePath -- ^ name of file

190− -> Idris [[(Name, PTerm)]]

190+ -> Idris [[(Name, PTerm)]]

191splitOnLine l n fn = do

192-- let (before, later) = splitAt (l-1) (lines inp)

193-- i <- getIState

@@ -263,10 +263,10 @@ nameRoot acc nm =

263 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after

264 _ -> showSep "_" (acc ++ [nm])

265

266−getClause :: Int -> -- ^ Line type is declared on

266+getClause :: Int -- ^ line number that the type is declared on

267− Name -> -- ^ Function name

267+ -> Name -- ^ Function name

268− FilePath -> -- ^ Source file name

268+ -> FilePath -- ^ Source file name

269− Idris String

269+ -> Idris String

270getClause l fn fp = do ty <- getInternalApp fp l

271 let ap = mkApp ty [1..]

272 return (show fn ++ " " ++ ap ++

@@ -278,10 +278,10 @@ getClause l fn fp = do ty <- getInternalApp fp l

278 mkApp (PPi _ _ _ sc) ns = mkApp sc ns

279 mkApp _ _ = ""

280

281−getProofClause :: Int -> -- ^ Line type is declared on

281+getProofClause :: Int -- ^ line number that the type is declared

282− Name -> -- ^ Function name

282+ -> Name -- ^ Function name

283− FilePath -> -- ^ Source file name

283+ -> FilePath -- ^ Source file name

284− Idris String

284+ -> Idris String

285getProofClause l fn fp

286 = do ty <- getInternalApp fp l

287 return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")

src/Idris/ElabDecls.hs+1−1

@@ -888,7 +888,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

888 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats

889 _ -> return ()

890

891− let optpdef = map debind optpats -- $ map (simple_lhs (tt_ctxt ist)) optpats

891+ let optpdef = map debind optpats -- \$ map (simple_lhs (tt_ctxt ist)) optpats

892 tree@(CaseDef scargs sc _) <- tclift $

893 simpleCase tcase False reflect CompileTime fc pdef

894 cov <- coverage

src/Idris/ParseExpr.hs+124−37

@@ -42,8 +42,10 @@ allowImp syn = syn { implicitAllowed = True }

42disallowImp :: SyntaxInfo -> SyntaxInfo

43disallowImp syn = syn { implicitAllowed = False }

45−{- | Parses an expression as a whole

45+{-| Parses an expression as a whole

46+@

46 FullExpr ::= Expr EOF_t;

47 FullExpr ::= Expr EOF_t;

48+@

47 -}

49 -}

48fullExpr :: SyntaxInfo -> IdrisParser PTerm

50fullExpr :: SyntaxInfo -> IdrisParser PTerm

49fullExpr syn = do x <- expr syn

51fullExpr syn = do x <- expr syn

@@ -53,7 +55,9 @@ fullExpr syn = do x <- expr syn

55{- |Parses an expression

57{- |Parses an expression

58+@

56 Expr ::= Expr';

59 Expr ::= Expr';

60+@

57-}

61-}

58expr :: SyntaxInfo -> IdrisParser PTerm

62expr :: SyntaxInfo -> IdrisParser PTerm

59expr syn = do i <- get

63expr syn = do i <- get

@@ -61,10 +65,10 @@ expr syn = do i <- get

62{- | Parses either an internally defined expression or

66{- | Parses either an internally defined expression or

63 a user-defined one

67 a user-defined one

64−

68+@

65Expr' ::= "External (User-defined) Syntax"

69Expr' ::= "External (User-defined) Syntax"

66 | InternalExpr;

70 | InternalExpr;

67−

71+@

68 -}

72 -}

69expr' :: SyntaxInfo -> IdrisParser PTerm

73expr' :: SyntaxInfo -> IdrisParser PTerm

70expr' syn = try (externalExpr syn)

74expr' syn = try (externalExpr syn)

@@ -92,7 +96,7 @@ simpleExternalExpr syn = do i <- get

92 _ -> False

96 _ -> False

93 isSimple _ = False

97 isSimple _ = False

95−{- | Tries to parse a user-defined expression given a list of syntactic extensions -}

99+{- | Tries to parse a user-defined expression given a list of syntactic extensions -}

96extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm

100extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm

97extensions syn rules = choice (map (try . extension syn) (filter isValid rules))

101extensions syn rules = choice (map (try . extension syn) (filter isValid rules))

98 <?> "user-defined expression"

102 <?> "user-defined expression"

@@ -160,8 +164,8 @@ extension syn (Rule ssym ptm _)

160 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)

164 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)

161 update ns t = t

165 update ns t = t

162

166

163−{- |Parses a (normal) built-in expression

167+{- | Parses a (normal) built-in expression

164−

168+@

165InternalExpr ::=

169InternalExpr ::=

166 App

170 App

167 | MatchApp

171 | MatchApp

@@ -173,8 +177,9 @@ InternalExpr ::=

173 | Let

177 | Let

174 | RewriteTerm

178 | RewriteTerm

175 | Pi

179 | Pi

176− | DoBlock

180+ | DoBlock

177 ;

181 ;

182+@

178-}

183-}

179internalExpr :: SyntaxInfo -> IdrisParser PTerm

184internalExpr :: SyntaxInfo -> IdrisParser PTerm

180internalExpr syn =

185internalExpr syn =

@@ -193,8 +198,10 @@ internalExpr syn =

193 <?> "expression"

198 <?> "expression"

194

199

195{- | Parses a case expression

200{- | Parses a case expression

201+@

196CaseExpr ::=

202CaseExpr ::=

197 'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;

203 'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;

204+@

198-}

205-}

199caseExpr :: SyntaxInfo -> IdrisParser PTerm

206caseExpr :: SyntaxInfo -> IdrisParser PTerm

200caseExpr syn = do reserved "case"; fc <- getFC

207caseExpr syn = do reserved "case"; fc <- getFC

@@ -204,9 +211,11 @@ caseExpr syn = do reserved "case"; fc <- getFC

204 <?> "case expression"

211 <?> "case expression"

205

212

206{- | Parses a case in a case expression

213{- | Parses a case in a case expression

214+@

207CaseOption ::=

215CaseOption ::=

208 Expr '=>' Expr Terminator

216 Expr '=>' Expr Terminator

209 ;

217 ;

218+@

210-}

219-}

211caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)

220caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)

212caseOption syn = do lhs <- expr (syn { inPattern = True })

221caseOption syn = do lhs <- expr (syn { inPattern = True })

@@ -215,9 +224,11 @@ caseOption syn = do lhs <- expr (syn { inPattern = True })

215 <?> "case option"

224 <?> "case option"

216

225

217{- | Parses a proof block

226{- | Parses a proof block

227+@

218ProofExpr ::=

228ProofExpr ::=

219 'proof' OpenBlock Tactic'* CloseBlock

229 'proof' OpenBlock Tactic'* CloseBlock

220 ;

230 ;

231+@

221-}

232-}

222proofExpr :: SyntaxInfo -> IdrisParser PTerm

233proofExpr :: SyntaxInfo -> IdrisParser PTerm

223proofExpr syn = do reserved "proof"

234proofExpr syn = do reserved "proof"

@@ -225,10 +236,12 @@ proofExpr syn = do reserved "proof"

225 return $ PProof ts

236 return $ PProof ts

226 <?> "proof block"

237 <?> "proof block"

227

238

228−{- | Parses a tactics block

239+{- | Parses a tactics block

240+@

229TacticsExpr :=

241TacticsExpr :=

230 'tactics' OpenBlock Tactic'* CloseBlock

242 'tactics' OpenBlock Tactic'* CloseBlock

231;

243;

244+@

232-}

245-}

233tacticsExpr :: SyntaxInfo -> IdrisParser PTerm

246tacticsExpr :: SyntaxInfo -> IdrisParser PTerm

234tacticsExpr syn = do reserved "tactics"

247tacticsExpr syn = do reserved "tactics"

@@ -236,7 +249,8 @@ tacticsExpr syn = do reserved "tactics"

236 return $ PTactics ts

249 return $ PTactics ts

237 <?> "tactics block"

250 <?> "tactics block"

238

251

239−{- | Parses a simple expresion

252+{- | Parses a simple expression

253+@

240SimpleExpr ::=

254SimpleExpr ::=

241 '![' Term ']'

255 '![' Term ']'

242 | '?' Name

256 | '?' Name

@@ -257,6 +271,7 @@ SimpleExpr ::=

257 | '_'

271 | '_'

258 | {- External (User-defined) Simple Expression -}

272 | {- External (User-defined) Simple Expression -}

259 ;

273 ;

274+@

260-}

275-}

261simpleExpr :: SyntaxInfo -> IdrisParser PTerm

276simpleExpr :: SyntaxInfo -> IdrisParser PTerm

262simpleExpr syn =

277simpleExpr syn =

@@ -296,7 +311,8 @@ simpleExpr syn =

296 <?> "expression"

311 <?> "expression"

297

312

298

313

299−{- |Parses the rest of an expression in braces

314+{- |Parses the rest of an expression in braces

315+@

300Bracketed ::=

316Bracketed ::=

301 ')'

317 ')'

302 | Expr ')'

318 | Expr ')'

@@ -306,6 +322,7 @@ Bracketed ::=

306 | Expr Operator ')'

322 | Expr Operator ')'

307 | Name ':' Expr '**' Expr ')'

323 | Name ':' Expr '**' Expr ')'

308 ;

324 ;

325+@

309-}

326-}

310bracketed :: SyntaxInfo -> IdrisParser PTerm

327bracketed :: SyntaxInfo -> IdrisParser PTerm

311bracketed syn =

328bracketed syn =

@@ -378,15 +395,17 @@ modifyConst syn fc (PConstant (BI x))

378modifyConst syn fc x = x

395modifyConst syn fc x = x

379

396

380{- | Parses a list literal expression e.g. [1,2,3]

397{- | Parses a list literal expression e.g. [1,2,3]

398+@

381ListExpr ::=

399ListExpr ::=

382 '[' ExprList? ']'

400 '[' ExprList? ']'

383;

401;

384−

402+@

403+@

385ExprList ::=

404ExprList ::=

386 Expr

405 Expr

387 | Expr ',' ExprList

406 | Expr ',' ExprList

388 ;

407 ;

389−

408+@

390 -}

409 -}

391listExpr :: SyntaxInfo -> IdrisParser PTerm

410listExpr :: SyntaxInfo -> IdrisParser PTerm

392listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lchar ']'

411listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lchar ']'

@@ -399,22 +418,26 @@ listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lc

399

418

400

419

401{- | Parses an alternative expression

420{- | Parses an alternative expression

421+@

402 Alt ::= '(|' Expr_List '|)';

422 Alt ::= '(|' Expr_List '|)';

403

423

404 Expr_List ::=

424 Expr_List ::=

405 Expr'

425 Expr'

406 | Expr' ',' Expr_List

426 | Expr' ',' Expr_List

407 ;

427 ;

428+@

408-}

429-}

409alt :: SyntaxInfo -> IdrisParser PTerm

430alt :: SyntaxInfo -> IdrisParser PTerm

410alt syn = do symbol "(|"; alts <- sepBy1 (expr' syn) (lchar ','); symbol "|)"

431alt syn = do symbol "(|"; alts <- sepBy1 (expr' syn) (lchar ','); symbol "|)"

411 return (PAlternative False alts)

432 return (PAlternative False alts)

412

433

413{- | Parses a possibly hidden simple expression

434{- | Parses a possibly hidden simple expression

435+@

414HSimpleExpr ::=

436HSimpleExpr ::=

415 '.' SimpleExpr

437 '.' SimpleExpr

416 | SimpleExpr

438 | SimpleExpr

417 ;

439 ;

440+@

418-}

441-}

419hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm

442hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm

420hsimpleExpr syn =

443hsimpleExpr syn =

@@ -425,9 +448,11 @@ hsimpleExpr syn =

425 <?> "expression"

448 <?> "expression"

426

449

427{- | Parses a matching application expression

450{- | Parses a matching application expression

451+@

428MatchApp ::=

452MatchApp ::=

429 SimpleExpr '<==' FnName

453 SimpleExpr '<==' FnName

430 ;

454 ;

455+@

431-}

456-}

432matchApp :: SyntaxInfo -> IdrisParser PTerm

457matchApp :: SyntaxInfo -> IdrisParser PTerm

433matchApp syn = do ty <- simpleExpr syn

458matchApp syn = do ty <- simpleExpr syn

@@ -452,9 +477,11 @@ unifyLog syn = do lchar '%'; reserved "unifyLog";

452 <?> "unification log expression"

477 <?> "unification log expression"

453

478

454{- | Parses a no implicits expression

479{- | Parses a no implicits expression

480+@

455NoImplicits ::=

481NoImplicits ::=

456 '%' 'noImplicits' SimpleExpr

482 '%' 'noImplicits' SimpleExpr

457 ;

483 ;

484+@

458-}

485-}

459noImplicits :: SyntaxInfo -> IdrisParser PTerm

486noImplicits :: SyntaxInfo -> IdrisParser PTerm

460noImplicits syn = do lchar '%'; reserved "noImplicits";

487noImplicits syn = do lchar '%'; reserved "noImplicits";

@@ -463,10 +490,12 @@ noImplicits syn = do lchar '%'; reserved "noImplicits";

463 <?> "no implicits expression"

490 <?> "no implicits expression"

464

491

465{- | Parses a function application expression

492{- | Parses a function application expression

493+@

466App ::=

494App ::=

467 'mkForeign' Arg Arg*

495 'mkForeign' Arg Arg*

468 | SimpleExpr Arg+

496 | SimpleExpr Arg+

469 ;

497 ;

498+@

470-}

499-}

471app :: SyntaxInfo -> IdrisParser PTerm

500app :: SyntaxInfo -> IdrisParser PTerm

472app syn = do f <- reserved "mkForeign"

501app syn = do f <- reserved "mkForeign"

@@ -500,12 +529,14 @@ app syn = do f <- reserved "mkForeign"

500 = desugar (syn { dsl_info = d }) i (getTm a)

529 = desugar (syn { dsl_info = d }) i (getTm a)

501 dslify i t = t

530 dslify i t = t

502

531

503−{- |Parses a function argument

532+{-| Parses a function argument

533+@

504Arg ::=

534Arg ::=

505 ImplicitArg

535 ImplicitArg

506 | ConstraintArg

536 | ConstraintArg

507 | SimpleExpr

537 | SimpleExpr

508 ;

538 ;

539+@

509-}

540-}

510arg :: SyntaxInfo -> IdrisParser PArg

541arg :: SyntaxInfo -> IdrisParser PArg

511arg syn = implicitArg syn

542arg syn = implicitArg syn

@@ -514,10 +545,12 @@ arg syn = implicitArg syn

514 return (pexp e)

545 return (pexp e)

515 <?> "function argument"

546 <?> "function argument"

516

547

517−{- |Parses an implicit function argument

548+{-| Parses an implicit function argument

549+@

518ImplicitArg ::=

550ImplicitArg ::=

519 '{' Name ('=' Expr)? '}'

551 '{' Name ('=' Expr)? '}'

520 ;

552 ;

553+@

521-}

554-}

522implicitArg :: SyntaxInfo -> IdrisParser PArg

555implicitArg :: SyntaxInfo -> IdrisParser PArg

523implicitArg syn = do lchar '{'

556implicitArg syn = do lchar '{'

@@ -529,10 +562,12 @@ implicitArg syn = do lchar '{'

529 return (pimp n v False)

562 return (pimp n v False)

530 <?> "implicit function argument"

563 <?> "implicit function argument"

531

564

532−{- |Parses a constraint argument (for selecting a named type class instance)

565+{-| Parses a constraint argument (for selecting a named type class instance)

566+

533−ConstraintArg ::=

567+> ConstraintArg ::=

534− '@{' Expr '}'

568+> '@{' Expr '}'

535− ;

569+> ;

570+

536-}

571-}

537constraintArg :: SyntaxInfo -> IdrisParser PArg

572constraintArg :: SyntaxInfo -> IdrisParser PArg

538constraintArg syn = do symbol "@{"

573constraintArg syn = do symbol "@{"

@@ -542,18 +577,22 @@ constraintArg syn = do symbol "@{"

542 <?> "constraint argument"

577 <?> "constraint argument"

543

578

544

579

545−{- |Parses a record field setter expression

580+{-| Parses a record field setter expression

581+@

546RecordType ::=

582RecordType ::=

547 'record' '{' FieldTypeList '}';

583 'record' '{' FieldTypeList '}';

548−

584+@

585+@

549FieldTypeList ::=

586FieldTypeList ::=

550 FieldType

587 FieldType

551 | FieldType ',' FieldTypeList

588 | FieldType ',' FieldTypeList

552 ;

589 ;

553−

590+@

591+@

554FieldType ::=

592FieldType ::=

555 FnName '=' Expr

593 FnName '=' Expr

556 ;

594 ;

595+@

557-}

596-}

558recordType :: SyntaxInfo -> IdrisParser PTerm

597recordType :: SyntaxInfo -> IdrisParser PTerm

559recordType syn

598recordType syn

@@ -580,17 +619,21 @@ recordType syn

580 applyAll fc ((n, e) : es) x

619 applyAll fc ((n, e) : es) x

581 = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])

620 = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])

582

621

583−{- |Creates setters for record types on necessary functions -}

622+-- | Creates setters for record types on necessary functions

584mkType :: Name -> Name

623mkType :: Name -> Name

585mkType (UN n) = UN ("set_" ++ n)

624mkType (UN n) = UN ("set_" ++ n)

586mkType (MN 0 n) = MN 0 ("set_" ++ n)

625mkType (MN 0 n) = MN 0 ("set_" ++ n)

587mkType (NS n s) = NS (mkType n) s

626mkType (NS n s) = NS (mkType n) s

588

627

589−{- |Parses a type signature

628+{- | Parses a type signature

629+@

590TypeSig ::=

630TypeSig ::=

591 ':' Expr

631 ':' Expr

592 ;

632 ;

633+@

634+@

593TypeExpr ::= ConstraintList? Expr;

635TypeExpr ::= ConstraintList? Expr;

636+@

594 -}

637 -}

595typeExpr :: SyntaxInfo -> IdrisParser PTerm

638typeExpr :: SyntaxInfo -> IdrisParser PTerm

596typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []

639typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []

@@ -598,15 +641,19 @@ typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else retu

598 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)

641 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)

599 <?> "type signature"

642 <?> "type signature"

600

643

601−{- |Parses a lambda expression

644+{- | Parses a lambda expression

645+@

602Lambda ::=

646Lambda ::=

603 '\\' TypeOptDeclList '=>' Expr

647 '\\' TypeOptDeclList '=>' Expr

604 | '\\' SimpleExprList '=>' Expr

648 | '\\' SimpleExprList '=>' Expr

605 ;

649 ;

650+@

651+@

606SimpleExprList ::=

652SimpleExprList ::=

607 SimpleExpr

653 SimpleExpr

608 | SimpleExpr ',' SimpleExprList

654 | SimpleExpr ',' SimpleExprList

609 ;

655 ;

656+@

610-}

657-}

611lambda :: SyntaxInfo -> IdrisParser PTerm

658lambda :: SyntaxInfo -> IdrisParser PTerm

612lambda syn = do lchar '\\'

659lambda syn = do lchar '\\'

@@ -628,10 +675,12 @@ lambda syn = do lchar '\\'

628 (PCase fc (PRef fc (MN i "lamp"))

675 (PCase fc (PRef fc (MN i "lamp"))

629 [(x, pmList xs sc)])

676 [(x, pmList xs sc)])

630

677

631−{- |Parses a term rewrite expression

678+{- | Parses a term rewrite expression

679+@

632RewriteTerm ::=

680RewriteTerm ::=

633 'rewrite' Expr ('==>' Expr)? 'in' Expr

681 'rewrite' Expr ('==>' Expr)? 'in' Expr

634 ;

682 ;

683+@

635-}

684-}

636rewriteTerm :: SyntaxInfo -> IdrisParser PTerm

685rewriteTerm :: SyntaxInfo -> IdrisParser PTerm

637rewriteTerm syn = do reserved "rewrite"

686rewriteTerm syn = do reserved "rewrite"

@@ -645,6 +694,7 @@ rewriteTerm syn = do reserved "rewrite"

645 <?> "term rewrite expression"

694 <?> "term rewrite expression"

646

695

647{- |Parses a let binding

696{- |Parses a let binding

697+@

648Let ::=

698Let ::=

649 'let' Name TypeSig'? '=' Expr 'in' Expr

699 'let' Name TypeSig'? '=' Expr 'in' Expr

650| 'let' Expr' '=' Expr' 'in' Expr

700| 'let' Expr' '=' Expr' 'in' Expr

@@ -652,6 +702,7 @@ Let ::=

652TypeSig' ::=

702TypeSig' ::=

653 ':' Expr'

703 ':' Expr'

654 ;

704 ;

705+@

655 -}

706 -}

656let_ :: SyntaxInfo -> IdrisParser PTerm

707let_ :: SyntaxInfo -> IdrisParser PTerm

657let_ syn = try (do reserved "let"; n <- name;

708let_ syn = try (do reserved "let"; n <- name;

@@ -666,10 +717,13 @@ let_ syn = try (do reserved "let"; n <- name;

666 return (PCase fc v [(pat, sc)]))

717 return (PCase fc v [(pat, sc)]))

667 <?> "let binding"

718 <?> "let binding"

668

719

669−{- |Parses a quote goal

720+{- | Parses a quote goal

721+

722+@

670QuoteGoal ::=

723QuoteGoal ::=

671 'quoteGoal' Name 'by' Expr 'in' Expr

724 'quoteGoal' Name 'by' Expr 'in' Expr

672 ;

725 ;

726+@

673 -}

727 -}

674quoteGoal :: SyntaxInfo -> IdrisParser PTerm

728quoteGoal :: SyntaxInfo -> IdrisParser PTerm

675quoteGoal syn = do reserved "quoteGoal"; n <- name;

729quoteGoal syn = do reserved "quoteGoal"; n <- name;

@@ -681,13 +735,15 @@ quoteGoal syn = do reserved "quoteGoal"; n <- name;

681 return (PGoal fc r n sc)

735 return (PGoal fc r n sc)

682 <?> "quote goal expression"

736 <?> "quote goal expression"

683

737

684−{- |Parses a dependent type signature

738+{- | Parses a dependent type signature

739+@

685Pi ::=

740Pi ::=

686 '|'? Static? '(' TypeDeclList ')' DocComment '->' Expr

741 '|'? Static? '(' TypeDeclList ')' DocComment '->' Expr

687 | '|'? Static? '{' TypeDeclList '}' '->' Expr

742 | '|'? Static? '{' TypeDeclList '}' '->' Expr

688 | '{' 'auto' TypeDeclList '}' '->' Expr

743 | '{' 'auto' TypeDeclList '}' '->' Expr

689 | '{' 'default' TypeDeclList '}' '->' Expr

744 | '{' 'default' TypeDeclList '}' '->' Expr

690 ;

745 ;

746+@

691 -}

747 -}

692

748

693pi :: SyntaxInfo -> IdrisParser PTerm

749pi :: SyntaxInfo -> IdrisParser PTerm

@@ -729,10 +785,13 @@ pi syn =

729 <?> "dependent type signature"

785 <?> "dependent type signature"

730

786

731{- | Parses a type constraint list

787{- | Parses a type constraint list

788+

789+@

732ConstraintList ::=

790ConstraintList ::=

733 '(' Expr_List ')' '=>'

791 '(' Expr_List ')' '=>'

734 | Expr '=>'

792 | Expr '=>'

735 ;

793 ;

794+@

736-}

795-}

737constraintList :: SyntaxInfo -> IdrisParser [PTerm]

796constraintList :: SyntaxInfo -> IdrisParser [PTerm]

738constraintList syn = try (do lchar '('

797constraintList syn = try (do lchar '('

@@ -746,16 +805,20 @@ constraintList syn = try (do lchar '('

746 <|> return []

805 <|> return []

747 <?> "type constraint list"

806 <?> "type constraint list"

748

807

749−{- |Parses a type declaration list

808+{- | Parses a type declaration list

809+@

750TypeDeclList ::=

810TypeDeclList ::=

751 FunctionSignatureList

811 FunctionSignatureList

752 | NameList TypeSig

812 | NameList TypeSig

753 ;

813 ;

814+@

754

815

816+@

755FunctionSignatureList ::=

817FunctionSignatureList ::=

756 Name TypeSig

818 Name TypeSig

757 | Name TypeSig ',' FunctionSignatureList

819 | Name TypeSig ',' FunctionSignatureList

758 ;

820 ;

821+@

759-}

822-}

760typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

823typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

761typeDeclList syn = try (sepBy1 (do x <- fnName

824typeDeclList syn = try (sepBy1 (do x <- fnName

@@ -769,13 +832,17 @@ typeDeclList syn = try (sepBy1 (do x <- fnName

769 return (map (\x -> (x, t)) ns)

832 return (map (\x -> (x, t)) ns)

770 <?> "type declaration list"

833 <?> "type declaration list"

771

834

772−{- |Parses a type declaration list with optional parameters

835+{- | Parses a type declaration list with optional parameters

836+@

773TypeOptDeclList ::=

837TypeOptDeclList ::=

774 NameOrPlaceholder TypeSig?

838 NameOrPlaceholder TypeSig?

775 | NameOrPlaceholder TypeSig? ',' TypeOptDeclList

839 | NameOrPlaceholder TypeSig? ',' TypeOptDeclList

776 ;

840 ;

841+@

777

842

843+@

778NameOrPlaceHolder ::= Name | '_';

844NameOrPlaceHolder ::= Name | '_';

845+@

779-}

846-}

780tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

847tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

781tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder

848tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder

@@ -790,13 +857,17 @@ tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder

790 return (MN 0 "underscore")

857 return (MN 0 "underscore")

791 <?> "name or placeholder"

858 <?> "name or placeholder"

792

859

793−{- |Parses a list comprehension

860+{- | Parses a list comprehension

861+@

794Comprehension ::= '[' Expr '|' DoList ']';

862Comprehension ::= '[' Expr '|' DoList ']';

863+@

795

864

865+@

796DoList ::=

866DoList ::=

797 Do

867 Do

798 | Do ',' DoList

868 | Do ',' DoList

799 ;

869 ;

870+@

800-}

871-}

801comprehension :: SyntaxInfo -> IdrisParser PTerm

872comprehension :: SyntaxInfo -> IdrisParser PTerm

802comprehension syn

873comprehension syn

@@ -815,12 +886,16 @@ comprehension syn

815 [pexp e])

886 [pexp e])

816 addGuard x = x

887 addGuard x = x

817

888

818−{- |Parses a do-block

889+{- | Parses a do-block

890+@

819Do' ::= Do KeepTerminator;

891Do' ::= Do KeepTerminator;

892+@

820

893

894+@

821DoBlock ::=

895DoBlock ::=

822 'do' OpenBlock Do'+ CloseBlock

896 'do' OpenBlock Do'+ CloseBlock

823 ;

897 ;

898+@

824 -}

899 -}

825doBlock :: SyntaxInfo -> IdrisParser PTerm

900doBlock :: SyntaxInfo -> IdrisParser PTerm

826doBlock syn

901doBlock syn

@@ -829,7 +904,8 @@ doBlock syn

829 return (PDoBlock ds)

904 return (PDoBlock ds)

830 <?> "do block"

905 <?> "do block"

831

906

832−{- |Parses an expression inside a do block

907+{- | Parses an expression inside a do block

908+@

833Do ::=

909Do ::=

834 'let' Name TypeSig'? '=' Expr

910 'let' Name TypeSig'? '=' Expr

835 | 'let' Expr' '=' Expr

911 | 'let' Expr' '=' Expr

@@ -837,6 +913,7 @@ Do ::=

837 | Expr' '<-' Expr

913 | Expr' '<-' Expr

838 | Expr

914 | Expr

839 ;

915 ;

916+@

840-}

917-}

841do_ :: SyntaxInfo -> IdrisParser PDo

918do_ :: SyntaxInfo -> IdrisParser PDo

842do_ syn

919do_ syn

@@ -869,8 +946,10 @@ do_ syn

869 return (DoExp fc e)

946 return (DoExp fc e)

870 <?> "do block expression"

947 <?> "do block expression"

871

948

872−{- |Parses an expression in idiom brackets

949+{- | Parses an expression in idiom brackets

950+@

873Idiom ::= '[|' Expr '|]';

951Idiom ::= '[|' Expr '|]';

952+@

874-}

953-}

875idiom :: SyntaxInfo -> IdrisParser PTerm

954idiom :: SyntaxInfo -> IdrisParser PTerm

876idiom syn

955idiom syn

@@ -882,6 +961,8 @@ idiom syn

882 <?> "expression in idiom brackets"

961 <?> "expression in idiom brackets"

883

962

884{- |Parses a constant or literal expression

963{- |Parses a constant or literal expression

964+

965+@

885Constant ::=

966Constant ::=

886 'Integer'

967 'Integer'

887 | 'Int'

968 | 'Int'

@@ -902,6 +983,7 @@ Constant ::=

902 | String_t

983 | String_t

903 | Char_t

984 | Char_t

904 ;

985 ;

986+@

905-}

987-}

906constant :: IdrisParser Core.TT.Const

988constant :: IdrisParser Core.TT.Const

907constant = do reserved "Integer";return (AType (ATInt ITBig))

989constant = do reserved "Integer";return (AType (ATInt ITBig))

@@ -924,17 +1006,22 @@ constant = do reserved "Integer";return (AType (ATInt ITBig))

924 <|> try (do c <- charLiteral; return $ Ch c)

1006 <|> try (do c <- charLiteral; return $ Ch c)

925 <?> "constant or literal"

1007 <?> "constant or literal"

926

1008

927−{- |Parses a static modifier

1009+{- | Parses a static modifier

1010+

1011+@

928Static ::=

1012Static ::=

929 '[' static ']'

1013 '[' static ']'

930;

1014;

1015+@

931-}

1016-}

932static :: IdrisParser Static

1017static :: IdrisParser Static

933static = do lchar '['; reserved "static"; lchar ']'; return Static

1018static = do lchar '['; reserved "static"; lchar ']'; return Static

934 <|> return Dynamic

1019 <|> return Dynamic

935 <?> "static modifier"

1020 <?> "static modifier"

936

1021

937−{- | Parses a tactic script

1022+{- | Parses a tactic script

1023+

1024+@

938Tactic ::= 'intro' NameList?

1025Tactic ::= 'intro' NameList?

939 | 'intros'

1026 | 'intros'

940 | 'refine' Name Imp+

1027 | 'refine' Name Imp+

@@ -968,7 +1055,7 @@ TacticSeq ::=

968 Tactic ';' Tactic

1055 Tactic ';' Tactic

969 | Tactic ';' TacticSeq

1056 | Tactic ';' TacticSeq

970 ;

1057 ;

971−

1058+@

972-}

1059-}

973

1060

974tactic :: SyntaxInfo -> IdrisParser PTactic

1061tactic :: SyntaxInfo -> IdrisParser PTactic

@@ -1041,7 +1128,7 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (

1041 mergeSeq [t] = t

1128 mergeSeq [t] = t

1042 mergeSeq (t:ts) = TSeq t (mergeSeq ts)

1129 mergeSeq (t:ts) = TSeq t (mergeSeq ts)

1043

1130

1044−{- | Parses a tactic as a whole -}

1131+-- | Parses a tactic as a whole

1045fullTactic :: SyntaxInfo -> IdrisParser PTactic

1132fullTactic :: SyntaxInfo -> IdrisParser PTactic

1046fullTactic syn = do t <- tactic syn

1133fullTactic syn = do t <- tactic syn

1047 eof

1134 eof

src/Idris/ParseOps.hs+23−14

@@ -29,8 +29,8 @@ import qualified Data.HashSet as HS

29import qualified Data.Text as T

30import qualified Data.ByteString.UTF8 as UTF8

32−{- |Creates table for fixity declarations to build expression parser using

32+-- | Creates table for fixity declarations to build expression parser

33− pre-build and user-defined operator/fixity declarations -}

33+-- using pre-build and user-defined operator/fixity declarations

34table :: [FixDecl] -> OperatorTable IdrisParser PTerm

35table fixes

36 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))

@@ -40,7 +40,7 @@ table fixes

40 [binary "=" PEq AssocLeft],

41 [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]

43−{- |Calculates table for fixtiy declarations -}

43+-- | Calculates table for fixtiy declarations

44toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

45toTable fs = map (map toBin)

46 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)

@@ -52,20 +52,20 @@ toTable fs = map (map toBin)

52 assoc (Infixr _) = AssocRight

53 assoc (InfixN _) = AssocNone

55−{- |Binary operator -}

55+-- | Binary operator

56binary :: String -> (FC -> PTerm -> PTerm -> PTerm) -> Assoc -> Operator IdrisParser PTerm

57binary name f = Infix (do fc <- getFC

58 reservedOp name

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

60 return (f fc))

62−{- |Prefix operator -}

62+-- | Prefix operator

63prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm

64prefix name f = Prefix (do reservedOp name

65 fc <- getFC

66 return (f fc))

68−{- |Backtick operator -}

68+-- | Backtick operator

69backtick :: Operator IdrisParser PTerm

70backtick = Infix (do lchar '`'; n <- fnName

71 lchar '`'

@@ -75,22 +75,29 @@ backtick = Infix (do lchar '`'; n <- fnName

75{- | Parses an operator in function position i.e. enclosed by `()', with an

76 optional namespace

78+@

78 OperatorFront ::= (Identifier_t '.')? '(' Operator_t ')';

79 OperatorFront ::= (Identifier_t '.')? '(' Operator_t ')';

80+@

81+

79-}

82-}

80operatorFront :: IdrisParser Name

83operatorFront :: IdrisParser Name

81operatorFront = maybeWithNS (lchar '(' *> operator <* lchar ')') False []

84operatorFront = maybeWithNS (lchar '(' *> operator <* lchar ')') False []

83{- | Parses a function (either normal name or operator)

86{- | Parses a function (either normal name or operator)

87+

88+@

84− FnName ::= Name | OperatorFront;

89+ FnName ::= Name | OperatorFront;

90+@

85-}

91-}

86fnName :: IdrisParser Name

92fnName :: IdrisParser Name

87fnName = try operatorFront <|> name <?> "function name"

93fnName = try operatorFront <|> name <?> "function name"

89{- | Parses a fixity declaration

95{- | Parses a fixity declaration

90−

96+@

91Fixity ::=

97Fixity ::=

92 FixityType Natural_t OperatorList Terminator

98 FixityType Natural_t OperatorList Terminator

93 ;

99 ;

100+@

94-}

101-}

95fixity :: IdrisParser PDecl

102fixity :: IdrisParser PDecl

96fixity = do pushIndent

103fixity = do pushIndent

@@ -121,12 +128,14 @@ fixity = do pushIndent

121 extractName (Fix _ n) = n

128 extractName (Fix _ n) = n

122

129

123{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)

130{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)

131+@

124−FixityType ::=

132+ FixityType ::=

125− 'infixl'

133+ 'infixl'

126− | 'infixr'

134+ | 'infixr'

127− | 'infix'

135+ | 'infix'

128− | 'prefix'

136+ | 'prefix'

129− ;

137+ ;

138+@

130 -}

139 -}

131fixityType :: IdrisParser (Int -> Fixity)

140fixityType :: IdrisParser (Int -> Fixity)

132fixityType = do reserved "infixl"; return Infixl

141fixityType = do reserved "infixl"; return Infixl