5afcedb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fixed malformed haddock comments

5afcedbJan de Muijnck-Hughes13 years ago

src/Core/Evaluate.hs+1−1

compare with master

unifiedsplit

@@ -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

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

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

639 _ -> return ()

640

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

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

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

643 simpleCase tcase False reflect CompileTime fc pdef

644 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 =

@@ -295,7 +310,8 @@ simpleExpr syn =

295 <?> "expression"

310 <?> "expression"

296

311

297

312

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

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

314+@

299Bracketed ::=

315Bracketed ::=

300 ')'

316 ')'

301 | Expr ')'

317 | Expr ')'

@@ -305,6 +321,7 @@ Bracketed ::=

305 | Expr Operator ')'

321 | Expr Operator ')'

306 | Name ':' Expr '**' Expr ')'

322 | Name ':' Expr '**' Expr ')'

307 ;

323 ;

324+@

308-}

325-}

309bracketed :: SyntaxInfo -> IdrisParser PTerm

326bracketed :: SyntaxInfo -> IdrisParser PTerm

310bracketed syn =

327bracketed syn =

@@ -377,15 +394,17 @@ modifyConst syn fc (PConstant (BI x))

377modifyConst syn fc x = x

394modifyConst syn fc x = x

378

395

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

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

397+@

380ListExpr ::=

398ListExpr ::=

381 '[' ExprList? ']'

399 '[' ExprList? ']'

382;

400;

383−

401+@

402+@

384ExprList ::=

403ExprList ::=

385 Expr

404 Expr

386 | Expr ',' ExprList

405 | Expr ',' ExprList

387 ;

406 ;

388−

407+@

389 -}

408 -}

390listExpr :: SyntaxInfo -> IdrisParser PTerm

409listExpr :: SyntaxInfo -> IdrisParser PTerm

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

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

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

398

417

399

418

400{- | Parses an alternative expression

419{- | Parses an alternative expression

420+@

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

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

402

422

403 Expr_List ::=

423 Expr_List ::=

404 Expr'

424 Expr'

405 | Expr' ',' Expr_List

425 | Expr' ',' Expr_List

406 ;

426 ;

427+@

407-}

428-}

408alt :: SyntaxInfo -> IdrisParser PTerm

429alt :: SyntaxInfo -> IdrisParser PTerm

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

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

410 return (PAlternative False alts)

431 return (PAlternative False alts)

411

432

412{- | Parses a possibly hidden simple expression

433{- | Parses a possibly hidden simple expression

434+@

413HSimpleExpr ::=

435HSimpleExpr ::=

414 '.' SimpleExpr

436 '.' SimpleExpr

415 | SimpleExpr

437 | SimpleExpr

416 ;

438 ;

439+@

417-}

440-}

418hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm

441hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm

419hsimpleExpr syn =

442hsimpleExpr syn =

@@ -424,9 +447,11 @@ hsimpleExpr syn =

424 <?> "expression"

447 <?> "expression"

425

448

426{- | Parses a matching application expression

449{- | Parses a matching application expression

450+@

427MatchApp ::=

451MatchApp ::=

428 SimpleExpr '<==' FnName

452 SimpleExpr '<==' FnName

429 ;

453 ;

454+@

430-}

455-}

431matchApp :: SyntaxInfo -> IdrisParser PTerm

456matchApp :: SyntaxInfo -> IdrisParser PTerm

432matchApp syn = do ty <- simpleExpr syn

457matchApp syn = do ty <- simpleExpr syn

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

451 <?> "unification log expression"

476 <?> "unification log expression"

452

477

453{- | Parses a no implicits expression

478{- | Parses a no implicits expression

479+@

454NoImplicits ::=

480NoImplicits ::=

455 '%' 'noImplicits' SimpleExpr

481 '%' 'noImplicits' SimpleExpr

456 ;

482 ;

483+@

457-}

484-}

458noImplicits :: SyntaxInfo -> IdrisParser PTerm

485noImplicits :: SyntaxInfo -> IdrisParser PTerm

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

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

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

462 <?> "no implicits expression"

489 <?> "no implicits expression"

463

490

464{- | Parses a function application expression

491{- | Parses a function application expression

492+@

465App ::=

493App ::=

466 'mkForeign' Arg Arg*

494 'mkForeign' Arg Arg*

467 | SimpleExpr Arg+

495 | SimpleExpr Arg+

468 ;

496 ;

497+@

469-}

498-}

470app :: SyntaxInfo -> IdrisParser PTerm

499app :: SyntaxInfo -> IdrisParser PTerm

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

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

@@ -499,12 +528,14 @@ app syn = do f <- reserved "mkForeign"

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

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

500 dslify i t = t

529 dslify i t = t

501

530

502−{- |Parses a function argument

531+{-| Parses a function argument

532+@

503Arg ::=

533Arg ::=

504 ImplicitArg

534 ImplicitArg

505 | ConstraintArg

535 | ConstraintArg

506 | SimpleExpr

536 | SimpleExpr

507 ;

537 ;

538+@

508-}

539-}

509arg :: SyntaxInfo -> IdrisParser PArg

540arg :: SyntaxInfo -> IdrisParser PArg

510arg syn = implicitArg syn

541arg syn = implicitArg syn

@@ -513,10 +544,12 @@ arg syn = implicitArg syn

513 return (pexp e)

544 return (pexp e)

514 <?> "function argument"

545 <?> "function argument"

515

546

516−{- |Parses an implicit function argument

547+{-| Parses an implicit function argument

548+@

517ImplicitArg ::=

549ImplicitArg ::=

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

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

519 ;

551 ;

552+@

520-}

553-}

521implicitArg :: SyntaxInfo -> IdrisParser PArg

554implicitArg :: SyntaxInfo -> IdrisParser PArg

522implicitArg syn = do lchar '{'

555implicitArg syn = do lchar '{'

@@ -528,10 +561,12 @@ implicitArg syn = do lchar '{'

528 return (pimp n v False)

561 return (pimp n v False)

529 <?> "implicit function argument"

562 <?> "implicit function argument"

530

563

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

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

565+

532−ConstraintArg ::=

566+> ConstraintArg ::=

533− '@{' Expr '}'

567+> '@{' Expr '}'

534− ;

568+> ;

569+

535-}

570-}

536constraintArg :: SyntaxInfo -> IdrisParser PArg

571constraintArg :: SyntaxInfo -> IdrisParser PArg

537constraintArg syn = do symbol "@{"

572constraintArg syn = do symbol "@{"

@@ -541,18 +576,22 @@ constraintArg syn = do symbol "@{"

541 <?> "constraint argument"

576 <?> "constraint argument"

542

577

543

578

544−{- |Parses a record field setter expression

579+{-| Parses a record field setter expression

580+@

545RecordType ::=

581RecordType ::=

546 'record' '{' FieldTypeList '}';

582 'record' '{' FieldTypeList '}';

547−

583+@

584+@

548FieldTypeList ::=

585FieldTypeList ::=

549 FieldType

586 FieldType

550 | FieldType ',' FieldTypeList

587 | FieldType ',' FieldTypeList

551 ;

588 ;

552−

589+@

590+@

553FieldType ::=

591FieldType ::=

554 FnName '=' Expr

592 FnName '=' Expr

555 ;

593 ;

594+@

556-}

595-}

557recordType :: SyntaxInfo -> IdrisParser PTerm

596recordType :: SyntaxInfo -> IdrisParser PTerm

558recordType syn

597recordType syn

@@ -579,17 +618,21 @@ recordType syn

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

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

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

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

581

620

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

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

583mkType :: Name -> Name

622mkType :: Name -> Name

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

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

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

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

586mkType (NS n s) = NS (mkType n) s

625mkType (NS n s) = NS (mkType n) s

587

626

588−{- |Parses a type signature

627+{- | Parses a type signature

628+@

589TypeSig ::=

629TypeSig ::=

590 ':' Expr

630 ':' Expr

591 ;

631 ;

632+@

633+@

592TypeExpr ::= ConstraintList? Expr;

634TypeExpr ::= ConstraintList? Expr;

635+@

593 -}

636 -}

594typeExpr :: SyntaxInfo -> IdrisParser PTerm

637typeExpr :: SyntaxInfo -> IdrisParser PTerm

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

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

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

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

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

598 <?> "type signature"

641 <?> "type signature"

599

642

600−{- |Parses a lambda expression

643+{- | Parses a lambda expression

644+@

601Lambda ::=

645Lambda ::=

602 '\\' TypeOptDeclList '=>' Expr

646 '\\' TypeOptDeclList '=>' Expr

603 | '\\' SimpleExprList '=>' Expr

647 | '\\' SimpleExprList '=>' Expr

604 ;

648 ;

649+@

650+@

605SimpleExprList ::=

651SimpleExprList ::=

606 SimpleExpr

652 SimpleExpr

607 | SimpleExpr ',' SimpleExprList

653 | SimpleExpr ',' SimpleExprList

608 ;

654 ;

655+@

609-}

656-}

610lambda :: SyntaxInfo -> IdrisParser PTerm

657lambda :: SyntaxInfo -> IdrisParser PTerm

611lambda syn = do lchar '\\'

658lambda syn = do lchar '\\'

@@ -627,10 +674,12 @@ lambda syn = do lchar '\\'

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

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

628 [(x, pmList xs sc)])

675 [(x, pmList xs sc)])

629

676

630−{- |Parses a term rewrite expression

677+{- | Parses a term rewrite expression

678+@

631RewriteTerm ::=

679RewriteTerm ::=

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

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

633 ;

681 ;

682+@

634-}

683-}

635rewriteTerm :: SyntaxInfo -> IdrisParser PTerm

684rewriteTerm :: SyntaxInfo -> IdrisParser PTerm

636rewriteTerm syn = do reserved "rewrite"

685rewriteTerm syn = do reserved "rewrite"

@@ -644,6 +693,7 @@ rewriteTerm syn = do reserved "rewrite"

644 <?> "term rewrite expression"

693 <?> "term rewrite expression"

645

694

646{- |Parses a let binding

695{- |Parses a let binding

696+@

647Let ::=

697Let ::=

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

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

649| 'let' Expr' '=' Expr' 'in' Expr

699| 'let' Expr' '=' Expr' 'in' Expr

@@ -651,6 +701,7 @@ Let ::=

651TypeSig' ::=

701TypeSig' ::=

652 ':' Expr'

702 ':' Expr'

653 ;

703 ;

704+@

654 -}

705 -}

655let_ :: SyntaxInfo -> IdrisParser PTerm

706let_ :: SyntaxInfo -> IdrisParser PTerm

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

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

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

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

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

666 <?> "let binding"

717 <?> "let binding"

667

718

668−{- |Parses a quote goal

719+{- | Parses a quote goal

720+

721+@

669QuoteGoal ::=

722QuoteGoal ::=

670 'quoteGoal' Name 'by' Expr 'in' Expr

723 'quoteGoal' Name 'by' Expr 'in' Expr

671 ;

724 ;

725+@

672 -}

726 -}

673quoteGoal :: SyntaxInfo -> IdrisParser PTerm

727quoteGoal :: SyntaxInfo -> IdrisParser PTerm

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

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

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

680 return (PGoal fc r n sc)

734 return (PGoal fc r n sc)

681 <?> "quote goal expression"

735 <?> "quote goal expression"

682

736

683−{- |Parses a dependent type signature

737+{- | Parses a dependent type signature

738+@

684Pi ::=

739Pi ::=

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

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

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

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

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

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

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

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

689 ;

744 ;

745+@

690 -}

746 -}

691

747

692pi :: SyntaxInfo -> IdrisParser PTerm

748pi :: SyntaxInfo -> IdrisParser PTerm

@@ -728,10 +784,13 @@ pi syn =

728 <?> "dependent type signature"

784 <?> "dependent type signature"

729

785

730{- | Parses a type constraint list

786{- | Parses a type constraint list

787+

788+@

731ConstraintList ::=

789ConstraintList ::=

732 '(' Expr_List ')' '=>'

790 '(' Expr_List ')' '=>'

733 | Expr '=>'

791 | Expr '=>'

734 ;

792 ;

793+@

735-}

794-}

736constraintList :: SyntaxInfo -> IdrisParser [PTerm]

795constraintList :: SyntaxInfo -> IdrisParser [PTerm]

737constraintList syn = try (do lchar '('

796constraintList syn = try (do lchar '('

@@ -745,16 +804,20 @@ constraintList syn = try (do lchar '('

745 <|> return []

804 <|> return []

746 <?> "type constraint list"

805 <?> "type constraint list"

747

806

748−{- |Parses a type declaration list

807+{- | Parses a type declaration list

808+@

749TypeDeclList ::=

809TypeDeclList ::=

750 FunctionSignatureList

810 FunctionSignatureList

751 | NameList TypeSig

811 | NameList TypeSig

752 ;

812 ;

813+@

753

814

815+@

754FunctionSignatureList ::=

816FunctionSignatureList ::=

755 Name TypeSig

817 Name TypeSig

756 | Name TypeSig ',' FunctionSignatureList

818 | Name TypeSig ',' FunctionSignatureList

757 ;

819 ;

820+@

758-}

821-}

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

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

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

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

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

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

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

769 <?> "type declaration list"

832 <?> "type declaration list"

770

833

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

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

835+@

772TypeOptDeclList ::=

836TypeOptDeclList ::=

773 NameOrPlaceholder TypeSig?

837 NameOrPlaceholder TypeSig?

774 | NameOrPlaceholder TypeSig? ',' TypeOptDeclList

838 | NameOrPlaceholder TypeSig? ',' TypeOptDeclList

775 ;

839 ;

840+@

776

841

842+@

777NameOrPlaceHolder ::= Name | '_';

843NameOrPlaceHolder ::= Name | '_';

844+@

778-}

845-}

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

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

780tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder

847tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder

@@ -789,13 +856,17 @@ tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder

789 return (MN 0 "underscore")

856 return (MN 0 "underscore")

790 <?> "name or placeholder"

857 <?> "name or placeholder"

791

858

792−{- |Parses a list comprehension

859+{- | Parses a list comprehension

860+@

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

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

862+@

794

863

864+@

795DoList ::=

865DoList ::=

796 Do

866 Do

797 | Do ',' DoList

867 | Do ',' DoList

798 ;

868 ;

869+@

799-}

870-}

800comprehension :: SyntaxInfo -> IdrisParser PTerm

871comprehension :: SyntaxInfo -> IdrisParser PTerm

801comprehension syn

872comprehension syn

@@ -814,12 +885,16 @@ comprehension syn

814 [pexp e])

885 [pexp e])

815 addGuard x = x

886 addGuard x = x

816

887

817−{- |Parses a do-block

888+{- | Parses a do-block

889+@

818Do' ::= Do KeepTerminator;

890Do' ::= Do KeepTerminator;

891+@

819

892

893+@

820DoBlock ::=

894DoBlock ::=

821 'do' OpenBlock Do'+ CloseBlock

895 'do' OpenBlock Do'+ CloseBlock

822 ;

896 ;

897+@

823 -}

898 -}

824doBlock :: SyntaxInfo -> IdrisParser PTerm

899doBlock :: SyntaxInfo -> IdrisParser PTerm

825doBlock syn

900doBlock syn

@@ -828,7 +903,8 @@ doBlock syn

828 return (PDoBlock ds)

903 return (PDoBlock ds)

829 <?> "do block"

904 <?> "do block"

830

905

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

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

907+@

832Do ::=

908Do ::=

833 'let' Name TypeSig'? '=' Expr

909 'let' Name TypeSig'? '=' Expr

834 | 'let' Expr' '=' Expr

910 | 'let' Expr' '=' Expr

@@ -836,6 +912,7 @@ Do ::=

836 | Expr' '<-' Expr

912 | Expr' '<-' Expr

837 | Expr

913 | Expr

838 ;

914 ;

915+@

839-}

916-}

840do_ :: SyntaxInfo -> IdrisParser PDo

917do_ :: SyntaxInfo -> IdrisParser PDo

841do_ syn

918do_ syn

@@ -868,8 +945,10 @@ do_ syn

868 return (DoExp fc e)

945 return (DoExp fc e)

869 <?> "do block expression"

946 <?> "do block expression"

870

947

871−{- |Parses an expression in idiom brackets

948+{- | Parses an expression in idiom brackets

949+@

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

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

951+@

873-}

952-}

874idiom :: SyntaxInfo -> IdrisParser PTerm

953idiom :: SyntaxInfo -> IdrisParser PTerm

875idiom syn

954idiom syn

@@ -881,6 +960,8 @@ idiom syn

881 <?> "expression in idiom brackets"

960 <?> "expression in idiom brackets"

882

961

883{- |Parses a constant or literal expression

962{- |Parses a constant or literal expression

963+

964+@

884Constant ::=

965Constant ::=

885 'Integer'

966 'Integer'

886 | 'Int'

967 | 'Int'

@@ -901,6 +982,7 @@ Constant ::=

901 | String_t

982 | String_t

902 | Char_t

983 | Char_t

903 ;

984 ;

985+@

904-}

986-}

905constant :: IdrisParser Core.TT.Const

987constant :: IdrisParser Core.TT.Const

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

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

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

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

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

924 <?> "constant or literal"

1006 <?> "constant or literal"

925

1007

926−{- |Parses a static modifier

1008+{- | Parses a static modifier

1009+

1010+@

927Static ::=

1011Static ::=

928 '[' static ']'

1012 '[' static ']'

929;

1013;

1014+@

930-}

1015-}

931static :: IdrisParser Static

1016static :: IdrisParser Static

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

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

933 <|> return Dynamic

1018 <|> return Dynamic

934 <?> "static modifier"

1019 <?> "static modifier"

935

1020

936−{- | Parses a tactic script

1021+{- | Parses a tactic script

1022+

1023+@

937Tactic ::= 'intro' NameList?

1024Tactic ::= 'intro' NameList?

938 | 'intros'

1025 | 'intros'

939 | 'refine' Name Imp+

1026 | 'refine' Name Imp+

@@ -967,7 +1054,7 @@ TacticSeq ::=

967 Tactic ';' Tactic

1054 Tactic ';' Tactic

968 | Tactic ';' TacticSeq

1055 | Tactic ';' TacticSeq

969 ;

1056 ;

970−

1057+@

971-}

1058-}

972

1059

973tactic :: SyntaxInfo -> IdrisParser PTactic

1060tactic :: SyntaxInfo -> IdrisParser PTactic

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

1040 mergeSeq [t] = t

1127 mergeSeq [t] = t

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

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

1042

1129

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

1130+-- | Parses a tactic as a whole

1044fullTactic :: SyntaxInfo -> IdrisParser PTactic

1131fullTactic :: SyntaxInfo -> IdrisParser PTactic

1045fullTactic syn = do t <- tactic syn

1132fullTactic syn = do t <- tactic syn

1046 eof

1133 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