985fe52 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge remote-tracking branch 'jfdm/haddock' into haddock-on-test

commit985fe52d0403a81372c615b5bcc41f27d509dded authorDavid Christiansen <david@davidchristiansen.dk> dateFri 29 Nov 2013, 11:28 (13 years ago) parent08eb2e2 5afcedb

5 files changed+161−65

compare with master

unifiedsplit

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

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

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

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

639639 _ -> return ()

640640

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

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

643643 simpleCase tcase False reflect CompileTime fc pdef

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

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

295310 <?> "expression"

296311

297312

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

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

314+@

299315Bracketed ::=

300316 ')'

301317 | Expr ')'

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

305321 | Expr Operator ')'

306322 | Name ':' Expr '**' Expr ')'

307323 ;

324+@

308325-}

309326bracketed :: SyntaxInfo -> IdrisParser PTerm

310327bracketed syn =

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

377394modifyConst syn fc x = x

378395

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

397+@

380398ListExpr ::=

381399 '[' ExprList? ']'

382400;

383−

401+@

402+@

384403ExprList ::=

385404 Expr

386405 | Expr ',' ExprList

387406 ;

388−

407+@

389408 -}

390409listExpr :: SyntaxInfo -> IdrisParser PTerm

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

398417

399418

400419{- | Parses an alternative expression

420+@

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

402422

403423 Expr_List ::=

404424 Expr'

405425 | Expr' ',' Expr_List

406426 ;

427+@

407428-}

408429alt :: SyntaxInfo -> IdrisParser PTerm

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

410431 return (PAlternative False alts)

411432

412433{- | Parses a possibly hidden simple expression

434+@

413435HSimpleExpr ::=

414436 '.' SimpleExpr

415437 | SimpleExpr

416438 ;

439+@

417440-}

418441hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm

419442hsimpleExpr syn =

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

424447 <?> "expression"

425448

426449{- | Parses a matching application expression

450+@

427451MatchApp ::=

428452 SimpleExpr '<==' FnName

429453 ;

454+@

430455-}

431456matchApp :: SyntaxInfo -> IdrisParser PTerm

432457matchApp syn = do ty <- simpleExpr syn

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

451476 <?> "unification log expression"

452477

453478{- | Parses a no implicits expression

479+@

454480NoImplicits ::=

455481 '%' 'noImplicits' SimpleExpr

456482 ;

483+@

457484-}

458485noImplicits :: SyntaxInfo -> IdrisParser PTerm

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

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

462489 <?> "no implicits expression"

463490

464491{- | Parses a function application expression

492+@

465493App ::=

466494 'mkForeign' Arg Arg*

467495 | SimpleExpr Arg+

468496 ;

497+@

469498-}

470499app :: SyntaxInfo -> IdrisParser PTerm

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

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

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

500529 dslify i t = t

501530

502−{- |Parses a function argument

531+{-| Parses a function argument

532+@

503533Arg ::=

504534 ImplicitArg

505535 | ConstraintArg

506536 | SimpleExpr

507537 ;

538+@

508539-}

509540arg :: SyntaxInfo -> IdrisParser PArg

510541arg syn = implicitArg syn

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

513544 return (pexp e)

514545 <?> "function argument"

515546

516−{- |Parses an implicit function argument

547+{-| Parses an implicit function argument

548+@

517549ImplicitArg ::=

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

519551 ;

552+@

520553-}

521554implicitArg :: SyntaxInfo -> IdrisParser PArg

522555implicitArg syn = do lchar '{'

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

528561 return (pimp n v False)

529562 <?> "implicit function argument"

530563

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

532−ConstraintArg ::=

533− '@{' Expr '}'

534− ;

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

565+

566+> ConstraintArg ::=

567+> '@{' Expr '}'

568+> ;

569+

535570-}

536571constraintArg :: SyntaxInfo -> IdrisParser PArg

537572constraintArg syn = do symbol "@{"

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

541576 <?> "constraint argument"

542577

543578

544−{- |Parses a record field setter expression

579+{-| Parses a record field setter expression

580+@

545581RecordType ::=

546582 'record' '{' FieldTypeList '}';

547−

583+@

584+@

548585FieldTypeList ::=

549586 FieldType

550587 | FieldType ',' FieldTypeList

551588 ;

552−

589+@

590+@

553591FieldType ::=

554592 FnName '=' Expr

555593 ;

594+@

556595-}

557596recordType :: SyntaxInfo -> IdrisParser PTerm

558597recordType syn

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

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

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

581620

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

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

583622mkType :: Name -> Name

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

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

586625mkType (NS n s) = NS (mkType n) s

587626

588−{- |Parses a type signature

627+{- | Parses a type signature

628+@

589629TypeSig ::=

590630 ':' Expr

591631 ;

632+@

633+@

592634TypeExpr ::= ConstraintList? Expr;

635+@

593636 -}

594637typeExpr :: SyntaxInfo -> IdrisParser PTerm

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

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

598641 <?> "type signature"

599642

600−{- |Parses a lambda expression

643+{- | Parses a lambda expression

644+@

601645Lambda ::=

602646 '\\' TypeOptDeclList '=>' Expr

603647 | '\\' SimpleExprList '=>' Expr

604648 ;

649+@

650+@

605651SimpleExprList ::=

606652 SimpleExpr

607653 | SimpleExpr ',' SimpleExprList

608654 ;

655+@

609656-}

610657lambda :: SyntaxInfo -> IdrisParser PTerm

611658lambda syn = do lchar '\\'

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

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

628675 [(x, pmList xs sc)])

629676

630−{- |Parses a term rewrite expression

677+{- | Parses a term rewrite expression

678+@

631679RewriteTerm ::=

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

633681 ;

682+@

634683-}

635684rewriteTerm :: SyntaxInfo -> IdrisParser PTerm

636685rewriteTerm syn = do reserved "rewrite"

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

644693 <?> "term rewrite expression"

645694

646695{- |Parses a let binding

696+@

647697Let ::=

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

649699| 'let' Expr' '=' Expr' 'in' Expr

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

651701TypeSig' ::=

652702 ':' Expr'

653703 ;

704+@

654705 -}

655706let_ :: SyntaxInfo -> IdrisParser PTerm

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

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

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

666717 <?> "let binding"

667718

668−{- |Parses a quote goal

719+{- | Parses a quote goal

720+

721+@

669722QuoteGoal ::=

670723 'quoteGoal' Name 'by' Expr 'in' Expr

671724 ;

725+@

672726 -}

673727quoteGoal :: SyntaxInfo -> IdrisParser PTerm

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

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

680734 return (PGoal fc r n sc)

681735 <?> "quote goal expression"

682736

683−{- |Parses a dependent type signature

737+{- | Parses a dependent type signature

738+@

684739Pi ::=

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

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

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

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

689744 ;

745+@

690746 -}

691747

692748pi :: SyntaxInfo -> IdrisParser PTerm

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

728784 <?> "dependent type signature"

729785

730786{- | Parses a type constraint list

787+

788+@

731789ConstraintList ::=

732790 '(' Expr_List ')' '=>'

733791 | Expr '=>'

734792 ;

793+@

735794-}

736795constraintList :: SyntaxInfo -> IdrisParser [PTerm]

737796constraintList syn = try (do lchar '('

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

745804 <|> return []

746805 <?> "type constraint list"

747806

748−{- |Parses a type declaration list

807+{- | Parses a type declaration list

808+@

749809TypeDeclList ::=

750810 FunctionSignatureList

751811 | NameList TypeSig

752812 ;

813+@

753814

815+@

754816FunctionSignatureList ::=

755817 Name TypeSig

756818 | Name TypeSig ',' FunctionSignatureList

757819 ;

820+@

758821-}

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

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

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

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

769832 <?> "type declaration list"

770833

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

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

835+@

772836TypeOptDeclList ::=

773837 NameOrPlaceholder TypeSig?

774838 | NameOrPlaceholder TypeSig? ',' TypeOptDeclList

775839 ;

840+@

776841

842+@

777843NameOrPlaceHolder ::= Name | '_';

844+@

778845-}

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

780847tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder

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

789856 return (MN 0 "underscore")

790857 <?> "name or placeholder"

791858

792−{- |Parses a list comprehension

859+{- | Parses a list comprehension

860+@

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

862+@

794863

864+@

795865DoList ::=

796866 Do

797867 | Do ',' DoList

798868 ;

869+@

799870-}

800871comprehension :: SyntaxInfo -> IdrisParser PTerm

801872comprehension syn

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

814885 [pexp e])

815886 addGuard x = x

816887

817−{- |Parses a do-block

888+{- | Parses a do-block

889+@

818890Do' ::= Do KeepTerminator;

891+@

819892

893+@

820894DoBlock ::=

821895 'do' OpenBlock Do'+ CloseBlock

822896 ;

897+@

823898 -}

824899doBlock :: SyntaxInfo -> IdrisParser PTerm

825900doBlock syn

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

828903 return (PDoBlock ds)

829904 <?> "do block"

830905

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

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

907+@

832908Do ::=

833909 'let' Name TypeSig'? '=' Expr

834910 | 'let' Expr' '=' Expr

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

836912 | Expr' '<-' Expr

837913 | Expr

838914 ;

915+@

839916-}

840917do_ :: SyntaxInfo -> IdrisParser PDo

841918do_ syn

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

868945 return (DoExp fc e)

869946 <?> "do block expression"

870947

871−{- |Parses an expression in idiom brackets

948+{- | Parses an expression in idiom brackets

949+@

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

951+@

873952-}

874953idiom :: SyntaxInfo -> IdrisParser PTerm

875954idiom syn

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

881960 <?> "expression in idiom brackets"

882961

883962{- |Parses a constant or literal expression

963+

964+@

884965Constant ::=

885966 'Integer'

886967 | 'Int'

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

901982 | String_t

902983 | Char_t

903984 ;

985+@

904986-}

905987constant :: IdrisParser Core.TT.Const

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

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

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

9241006 <?> "constant or literal"

9251007

926−{- |Parses a static modifier

1008+{- | Parses a static modifier

1009+

1010+@

9271011Static ::=

9281012 '[' static ']'

9291013;

1014+@

9301015-}

9311016static :: IdrisParser Static

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

9331018 <|> return Dynamic

9341019 <?> "static modifier"

9351020

936−{- | Parses a tactic script

1021+{- | Parses a tactic script

1022+

1023+@

9371024Tactic ::= 'intro' NameList?

9381025 | 'intros'

9391026 | 'refine' Name Imp+

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

9671054 Tactic ';' Tactic

9681055 | Tactic ';' TacticSeq

9691056 ;

970−

1057+@

9711058-}

9721059

9731060tactic :: SyntaxInfo -> IdrisParser PTactic

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

10401127 mergeSeq [t] = t

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

10421129

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

1130+-- | Parses a tactic as a whole

10441131fullTactic :: SyntaxInfo -> IdrisParser PTactic

10451132fullTactic syn = do t <- tactic syn

10461133 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