cc35585 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

Haddock on test

commitcc355856c844befd6c7a8a2e4edc72229e600b9d authorEdwin Brady <edwin.brady@gmail.com> dateSat 30 Nov 2013, 06:04 (13 years ago) parentb881bff 985fe52

6 files changed+162−66

compare with master

unifiedsplit

Makefile+1−1 src/Core/Evaluate.hs+1−1 src/Idris/CaseSplit.hs+12−12 src/Idris/ElabDecls.hs+1−1 src/Idris/ParseExpr.hs+124−37 src/Idris/ParseOps.hs+23−14

Makefile+1−1

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

1313build: dist/setup-config

1414 $(CABAL) build $(CABALFLAGS)

1515

16−test:

16+test: doc

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

1818

1919test_java:

src/Core/Evaluate.hs+1−1

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

767767 OK (CaseDef args_ct sc_ct _),

768768 OK (CaseDef args_inl sc_inl _),

769769 OK (CaseDef args_rt sc_rt _)) ->

770− let inl = alwaysInline -- || tcdict

770+ let inl = alwaysInline -- tcdict

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

772772 inlr = inl || small n args_rt sc_rt

773773 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)

184184

185185replaceVar ctxt n t pat = pat

186186

187−splitOnLine :: Int -- ^ line number

188− -> Name -- ^ variable

189− -> FilePath -- ^ name of file

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

187+splitOnLine :: Int -- ^ line number

188+ -> Name -- ^ variable

189+ -> FilePath -- ^ name of file

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

191191splitOnLine l n fn = do

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

193193-- i <- getIState

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

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

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

265265

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

267− Name -> -- ^ Function name

268− FilePath -> -- ^ Source file name

269− Idris String

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

267+ -> Name -- ^ Function name

268+ -> FilePath -- ^ Source file name

269+ -> Idris String

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

271271 let ap = mkApp ty [1..]

272272 return (show fn ++ " " ++ ap ++

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

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

279279 mkApp _ _ = ""

280280

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

282− Name -> -- ^ Function name

283− FilePath -> -- ^ Source file name

284− Idris String

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

282+ -> Name -- ^ Function name

283+ -> FilePath -- ^ Source file name

284+ -> Idris String

285285getProofClause l fn fp

286286 = do ty <- getInternalApp fp l

287287 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

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

889889 _ -> return ()

890890

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

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

893893 simpleCase tcase False reflect CompileTime fc pdef

894894 cov <- coverage

src/Idris/ParseExpr.hs+124−37

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

4242disallowImp :: SyntaxInfo -> SyntaxInfo

4343disallowImp syn = syn { implicitAllowed = False }

4444

45−{- | Parses an expression as a whole

45+{-| Parses an expression as a whole

46+@

4647 FullExpr ::= Expr EOF_t;

48+@

4749 -}

4850fullExpr :: SyntaxInfo -> IdrisParser PTerm

4951fullExpr syn = do x <- expr syn

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

5355

5456

5557{- |Parses an expression

58+@

5659 Expr ::= Expr';

60+@

5761-}

5862expr :: SyntaxInfo -> IdrisParser PTerm

5963expr syn = do i <- get

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

6165

6266{- | Parses either an internally defined expression or

6367 a user-defined one

64−

68+@

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

6670 | InternalExpr;

67−

71+@

6872 -}

6973expr' :: SyntaxInfo -> IdrisParser PTerm

7074expr' syn = try (externalExpr syn)

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

9296 _ -> False

9397 isSimple _ = False

9498

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

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

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

98102 <?> "user-defined expression"

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

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

161165 update ns t = t

162166

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

164−

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

168+@

165169InternalExpr ::=

166170 App

167171 | MatchApp

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

173177 | Let

174178 | RewriteTerm

175179 | Pi

176− | DoBlock

180+ | DoBlock

177181 ;

182+@

178183-}

179184internalExpr :: SyntaxInfo -> IdrisParser PTerm

180185internalExpr syn =

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

193198 <?> "expression"

194199

195200{- | Parses a case expression

201+@

196202CaseExpr ::=

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

204+@

198205-}

199206caseExpr :: SyntaxInfo -> IdrisParser PTerm

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

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

204211 <?> "case expression"

205212

206213{- | Parses a case in a case expression

214+@

207215CaseOption ::=

208216 Expr '=>' Expr Terminator

209217 ;

218+@

210219-}

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

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

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

215224 <?> "case option"

216225

217226{- | Parses a proof block

227+@

218228ProofExpr ::=

219229 'proof' OpenBlock Tactic'* CloseBlock

220230 ;

231+@

221232-}

222233proofExpr :: SyntaxInfo -> IdrisParser PTerm

223234proofExpr syn = do reserved "proof"

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

225236 return $ PProof ts

226237 <?> "proof block"

227238

228−{- | Parses a tactics block

239+{- | Parses a tactics block

240+@

229241TacticsExpr :=

230242 'tactics' OpenBlock Tactic'* CloseBlock

231243;

244+@

232245-}

233246tacticsExpr :: SyntaxInfo -> IdrisParser PTerm

234247tacticsExpr syn = do reserved "tactics"

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

236249 return $ PTactics ts

237250 <?> "tactics block"

238251

239−{- | Parses a simple expresion

252+{- | Parses a simple expression

253+@

240254SimpleExpr ::=

241255 '![' Term ']'

242256 | '?' Name

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

257271 | '_'

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

259273 ;

274+@

260275-}

261276simpleExpr :: SyntaxInfo -> IdrisParser PTerm

262277simpleExpr syn =

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

296311 <?> "expression"

297312

298313

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

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

315+@

300316Bracketed ::=

301317 ')'

302318 | Expr ')'

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

306322 | Expr Operator ')'

307323 | Name ':' Expr '**' Expr ')'

308324 ;

325+@

309326-}

310327bracketed :: SyntaxInfo -> IdrisParser PTerm

311328bracketed syn =

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

378395modifyConst syn fc x = x

379396

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

398+@

381399ListExpr ::=

382400 '[' ExprList? ']'

383401;

384−

402+@

403+@

385404ExprList ::=

386405 Expr

387406 | Expr ',' ExprList

388407 ;

389−

408+@

390409 -}

391410listExpr :: SyntaxInfo -> IdrisParser PTerm

392411listExpr 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

399418

400419

401420{- | Parses an alternative expression

421+@

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

403423

404424 Expr_List ::=

405425 Expr'

406426 | Expr' ',' Expr_List

407427 ;

428+@

408429-}

409430alt :: SyntaxInfo -> IdrisParser PTerm

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

411432 return (PAlternative False alts)

412433

413434{- | Parses a possibly hidden simple expression

435+@

414436HSimpleExpr ::=

415437 '.' SimpleExpr

416438 | SimpleExpr

417439 ;

440+@

418441-}

419442hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm

420443hsimpleExpr syn =

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

425448 <?> "expression"

426449

427450{- | Parses a matching application expression

451+@

428452MatchApp ::=

429453 SimpleExpr '<==' FnName

430454 ;

455+@

431456-}

432457matchApp :: SyntaxInfo -> IdrisParser PTerm

433458matchApp syn = do ty <- simpleExpr syn

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

452477 <?> "unification log expression"

453478

454479{- | Parses a no implicits expression

480+@

455481NoImplicits ::=

456482 '%' 'noImplicits' SimpleExpr

457483 ;

484+@

458485-}

459486noImplicits :: SyntaxInfo -> IdrisParser PTerm

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

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

463490 <?> "no implicits expression"

464491

465492{- | Parses a function application expression

493+@

466494App ::=

467495 'mkForeign' Arg Arg*

468496 | SimpleExpr Arg+

469497 ;

498+@

470499-}

471500app :: SyntaxInfo -> IdrisParser PTerm

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

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

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

501530 dslify i t = t

502531

503−{- |Parses a function argument

532+{-| Parses a function argument

533+@

504534Arg ::=

505535 ImplicitArg

506536 | ConstraintArg

507537 | SimpleExpr

508538 ;

539+@

509540-}

510541arg :: SyntaxInfo -> IdrisParser PArg

511542arg syn = implicitArg syn

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

514545 return (pexp e)

515546 <?> "function argument"

516547

517−{- |Parses an implicit function argument

548+{-| Parses an implicit function argument

549+@

518550ImplicitArg ::=

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

520552 ;

553+@

521554-}

522555implicitArg :: SyntaxInfo -> IdrisParser PArg

523556implicitArg syn = do lchar '{'

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

529562 return (pimp n v False)

530563 <?> "implicit function argument"

531564

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

533−ConstraintArg ::=

534− '@{' Expr '}'

535− ;

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

566+

567+> ConstraintArg ::=

568+> '@{' Expr '}'

569+> ;

570+

536571-}

537572constraintArg :: SyntaxInfo -> IdrisParser PArg

538573constraintArg syn = do symbol "@{"

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

542577 <?> "constraint argument"

543578

544579

545−{- |Parses a record field setter expression

580+{-| Parses a record field setter expression

581+@

546582RecordType ::=

547583 'record' '{' FieldTypeList '}';

548−

584+@

585+@

549586FieldTypeList ::=

550587 FieldType

551588 | FieldType ',' FieldTypeList

552589 ;

553−

590+@

591+@

554592FieldType ::=

555593 FnName '=' Expr

556594 ;

595+@

557596-}

558597recordType :: SyntaxInfo -> IdrisParser PTerm

559598recordType syn

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

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

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

582621

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

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

584623mkType :: Name -> Name

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

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

587626mkType (NS n s) = NS (mkType n) s

588627

589−{- |Parses a type signature

628+{- | Parses a type signature

629+@

590630TypeSig ::=

591631 ':' Expr

592632 ;

633+@

634+@

593635TypeExpr ::= ConstraintList? Expr;

636+@

594637 -}

595638typeExpr :: SyntaxInfo -> IdrisParser PTerm

596639typeExpr 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

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

599642 <?> "type signature"

600643

601−{- |Parses a lambda expression

644+{- | Parses a lambda expression

645+@

602646Lambda ::=

603647 '\\' TypeOptDeclList '=>' Expr

604648 | '\\' SimpleExprList '=>' Expr

605649 ;

650+@

651+@

606652SimpleExprList ::=

607653 SimpleExpr

608654 | SimpleExpr ',' SimpleExprList

609655 ;

656+@

610657-}

611658lambda :: SyntaxInfo -> IdrisParser PTerm

612659lambda syn = do lchar '\\'

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

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

629676 [(x, pmList xs sc)])

630677

631−{- |Parses a term rewrite expression

678+{- | Parses a term rewrite expression

679+@

632680RewriteTerm ::=

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

634682 ;

683+@

635684-}

636685rewriteTerm :: SyntaxInfo -> IdrisParser PTerm

637686rewriteTerm syn = do reserved "rewrite"

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

645694 <?> "term rewrite expression"

646695

647696{- |Parses a let binding

697+@

648698Let ::=

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

650700| 'let' Expr' '=' Expr' 'in' Expr

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

652702TypeSig' ::=

653703 ':' Expr'

654704 ;

705+@

655706 -}

656707let_ :: SyntaxInfo -> IdrisParser PTerm

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

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

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

667718 <?> "let binding"

668719

669−{- |Parses a quote goal

720+{- | Parses a quote goal

721+

722+@

670723QuoteGoal ::=

671724 'quoteGoal' Name 'by' Expr 'in' Expr

672725 ;

726+@

673727 -}

674728quoteGoal :: SyntaxInfo -> IdrisParser PTerm

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

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

681735 return (PGoal fc r n sc)

682736 <?> "quote goal expression"

683737

684−{- |Parses a dependent type signature

738+{- | Parses a dependent type signature

739+@

685740Pi ::=

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

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

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

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

690745 ;

746+@

691747 -}

692748

693749pi :: SyntaxInfo -> IdrisParser PTerm

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

729785 <?> "dependent type signature"

730786

731787{- | Parses a type constraint list

788+

789+@

732790ConstraintList ::=

733791 '(' Expr_List ')' '=>'

734792 | Expr '=>'

735793 ;

794+@

736795-}

737796constraintList :: SyntaxInfo -> IdrisParser [PTerm]

738797constraintList syn = try (do lchar '('

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

746805 <|> return []

747806 <?> "type constraint list"

748807

749−{- |Parses a type declaration list

808+{- | Parses a type declaration list

809+@

750810TypeDeclList ::=

751811 FunctionSignatureList

752812 | NameList TypeSig

753813 ;

814+@

754815

816+@

755817FunctionSignatureList ::=

756818 Name TypeSig

757819 | Name TypeSig ',' FunctionSignatureList

758820 ;

821+@

759822-}

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

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

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

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

770833 <?> "type declaration list"

771834

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

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

836+@

773837TypeOptDeclList ::=

774838 NameOrPlaceholder TypeSig?

775839 | NameOrPlaceholder TypeSig? ',' TypeOptDeclList

776840 ;

841+@

777842

843+@

778844NameOrPlaceHolder ::= Name | '_';

845+@

779846-}

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

781848tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder

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

790857 return (MN 0 "underscore")

791858 <?> "name or placeholder"

792859

793−{- |Parses a list comprehension

860+{- | Parses a list comprehension

861+@

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

863+@

795864

865+@

796866DoList ::=

797867 Do

798868 | Do ',' DoList

799869 ;

870+@

800871-}

801872comprehension :: SyntaxInfo -> IdrisParser PTerm

802873comprehension syn

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

815886 [pexp e])

816887 addGuard x = x

817888

818−{- |Parses a do-block

889+{- | Parses a do-block

890+@

819891Do' ::= Do KeepTerminator;

892+@

820893

894+@

821895DoBlock ::=

822896 'do' OpenBlock Do'+ CloseBlock

823897 ;

898+@

824899 -}

825900doBlock :: SyntaxInfo -> IdrisParser PTerm

826901doBlock syn

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

829904 return (PDoBlock ds)

830905 <?> "do block"

831906

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

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

908+@

833909Do ::=

834910 'let' Name TypeSig'? '=' Expr

835911 | 'let' Expr' '=' Expr

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

837913 | Expr' '<-' Expr

838914 | Expr

839915 ;

916+@

840917-}

841918do_ :: SyntaxInfo -> IdrisParser PDo

842919do_ syn

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

869946 return (DoExp fc e)

870947 <?> "do block expression"

871948

872−{- |Parses an expression in idiom brackets

949+{- | Parses an expression in idiom brackets

950+@

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

952+@

874953-}

875954idiom :: SyntaxInfo -> IdrisParser PTerm

876955idiom syn

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

882961 <?> "expression in idiom brackets"

883962

884963{- |Parses a constant or literal expression

964+

965+@

885966Constant ::=

886967 'Integer'

887968 | 'Int'

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

902983 | String_t

903984 | Char_t

904985 ;

986+@

905987-}

906988constant :: IdrisParser Core.TT.Const

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

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

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

9251007 <?> "constant or literal"

9261008

927−{- |Parses a static modifier

1009+{- | Parses a static modifier

1010+

1011+@

9281012Static ::=

9291013 '[' static ']'

9301014;

1015+@

9311016-}

9321017static :: IdrisParser Static

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

9341019 <|> return Dynamic

9351020 <?> "static modifier"

9361021

937−{- | Parses a tactic script

1022+{- | Parses a tactic script

1023+

1024+@

9381025Tactic ::= 'intro' NameList?

9391026 | 'intros'

9401027 | 'refine' Name Imp+

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

9681055 Tactic ';' Tactic

9691056 | Tactic ';' TacticSeq

9701057 ;

971−

1058+@

9721059-}

9731060

9741061tactic :: SyntaxInfo -> IdrisParser PTactic

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

10411128 mergeSeq [t] = t

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

10431130

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

1131+-- | Parses a tactic as a whole

10451132fullTactic :: SyntaxInfo -> IdrisParser PTactic

10461133fullTactic syn = do t <- tactic syn

10471134 eof

src/Idris/ParseOps.hs+23−14

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

2929import qualified Data.Text as T

3030import qualified Data.ByteString.UTF8 as UTF8

3131

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

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

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

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

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

3535table fixes

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

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

4040 [binary "=" PEq AssocLeft],

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

4242

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

43+-- | Calculates table for fixtiy declarations

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

4545toTable fs = map (map toBin)

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

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

5252 assoc (Infixr _) = AssocRight

5353 assoc (InfixN _) = AssocNone

5454

55−{- |Binary operator -}

55+-- | Binary operator

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

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

5858 reservedOp name

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

6060 return (f fc))

6161

62−{- |Prefix operator -}

62+-- | Prefix operator

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

6464prefix name f = Prefix (do reservedOp name

6565 fc <- getFC

6666 return (f fc))

6767

68−{- |Backtick operator -}

68+-- | Backtick operator

6969backtick :: Operator IdrisParser PTerm

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

7171 lchar '`'

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

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

7676 optional namespace

7777

78+@

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

80+@

81+

7982-}

8083operatorFront :: IdrisParser Name

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

8285

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

84− FnName ::= Name | OperatorFront;

87+

88+@

89+ FnName ::= Name | OperatorFront;

90+@

8591-}

8692fnName :: IdrisParser Name

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

8894

8995{- | Parses a fixity declaration

90−

96+@

9197Fixity ::=

9298 FixityType Natural_t OperatorList Terminator

9399 ;

100+@

94101-}

95102fixity :: IdrisParser PDecl

96103fixity = do pushIndent

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

121128 extractName (Fix _ n) = n

122129

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

124−FixityType ::=

125− 'infixl'

126− | 'infixr'

127− | 'infix'

128− | 'prefix'

129− ;

131+@

132+ FixityType ::=

133+ 'infixl'

134+ | 'infixr'

135+ | 'infix'

136+ | 'prefix'

137+ ;

138+@

130139 -}

131140fixityType :: IdrisParser (Int -> Fixity)

132141fixityType = do reserved "infixl"; return Infixl