878653b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Updated Haddock Documentation.

Fixed some outstanding malformed documentation strings.

commit878653b0787d3eb452fe71cf3466707a18b8619f authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateFri 24 Jan 2014, 21:00 (13 years ago) parent5080735

4 files changed+181−41

compare with master

unifiedsplit

src/Idris/ParseExpr.hs+3−1 src/Idris/ParseHelpers.hs+24−14 src/Idris/Parser.hs+152−24 src/Pkg/Package.hs+2−2

src/Idris/ParseExpr.hs+3−1

@@ -757,6 +757,7 @@ quoteGoal syn = do reserved "quoteGoal"; n <- name;

757757 <?> "quote goal expression"

758758

759759{- | Parses a dependent type signature

760+

760761@

761762Pi ::=

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

@@ -1030,9 +1031,10 @@ constant = do reserved "Integer";return (AType (ATInt ITBig))

10301031 <?> "constant or literal"

10311032

10321033{- | Parses a verbatim multi-line string literal (triple-quoted)

1034+

10331035@

10341036VerbatimString_t ::=

1035− '"""' ~'"""' '"""'

1037+ '\"\"\"' ~'\"\"\"' '\"\"\"'

10361038@

10371039 -}

10381040verbatimStringLiteral :: MonadicParsing m => m String

src/Idris/ParseHelpers.hs+24−14

@@ -31,7 +31,7 @@ import qualified Data.ByteString.UTF8 as UTF8

3131

3232import System.FilePath

3333

34−-- | Idris parser with state used during parsing

34+-- | Idris parser with state used during parsing

3535type IdrisParser = StateT IState IdrisInnerParser

3636

3737newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

@@ -40,7 +40,7 @@ newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

4040instance TokenParsing IdrisInnerParser where

4141 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

4242

43−-- | Generalized monadic parsing constraint type

43+-- | Generalized monadic parsing constraint type

4444type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)

4545

4646-- | Helper to run Idris inner parser based stateT parsers

@@ -49,7 +49,7 @@ runparser p i inputname = parseString (runInnerParser (evalStateT p i)) (Directe

4949

5050{- * Space, comments and literals (token/lexing like parsers) -}

5151

52−-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)

52+-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)

5353simpleWhiteSpace :: MonadicParsing m => m ()

5454simpleWhiteSpace = satisfy isSpace *> pure ()

5555

@@ -68,9 +68,12 @@ isDocCommentMarker '^' = True

6868isDocCommentMarker _ = False

6969

7070{- | Consumes a single-line comment

71+

72+@

7173 SingleLineComment_t ::= '--' EOL_t

7274 | '--' ~DocCommentMarker_t ~EOL_t* EOL_t

7375 ;

76+@

7477 -}

7578singleLineComment :: MonadicParsing m => m ()

7679singleLineComment = try (string "--" *> eol *> pure ())

@@ -78,18 +81,22 @@ singleLineComment = try (string "--" *> eol *> pure ())

7881 <?> ""

7982

8083{- | Consumes a multi-line comment

84+

85+@

8186 MultiLineComment_t ::=

8287 '{ -- }'

8388 | '{ -' ~DocCommentMarker_t InCommentChars_t

8489 ;

90+@

8591

92+@

8693 InCommentChars_t ::=

8794 '- }'

8895 | MultiLineComment_t InCommentChars_t

8996 | ~'- }'+ InCommentChars_t

9097 ;

91− -}

92−

98+@

99+-}

93100multiLineComment :: MonadicParsing m => m ()

94101multiLineComment = try (string "{-" *> (string "-}") *> pure ())

95102 <|> string "{-" *> satisfy (not . isDocCommentMarker) *> inCommentChars

@@ -106,9 +113,12 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())

106113 startEnd = "{}-"

107114

108115{-| Parses a documentation comment (similar to haddoc) given a marker character

116+

117+@

109118 DocComment_t ::= '--' DocCommentMarker_t ~EOL_t* EOL_t

110119 | '{ -' DocCommentMarket_t ~'- }'* '- }'

111120 ;

121+@

112122 -}

113123docComment :: MonadicParsing m => Char -> m String

114124docComment marker | isDocCommentMarker marker = do dc <- docComment' marker; return (T.unpack $ T.strip $ T.pack dc)

@@ -138,14 +148,14 @@ natural = Tok.natural

138148integer :: MonadicParsing m => m Integer

139149integer = Tok.integer

140150

141−-- | Parses a floating point number

151+-- | Parses a floating point number

142152float :: MonadicParsing m => m Double

143153float = Tok.double

144154

145155{- * Symbols, identifiers, names and operators -}

146156

147157

148−-- | Idris Style for parsing identifiers/reserved keywords

158+-- | Idris Style for parsing identifiers/reserved keywords

149159idrisStyle :: MonadicParsing m => IdentifierStyle m

150160idrisStyle = IdentifierStyle _styleName _styleStart _styleLetter _styleReserved Hi.Identifier Hi.ReservedIdentifier

151161 where _styleName = "Idris"

@@ -215,9 +225,9 @@ name = do i <- get

215225 <?> "name"

216226

217227

218−{- | List of all initial segments in ascending order of a list. Every such

219− initial segment ends right before an element satisfying the given

220− condition.

228+{- | List of all initial segments in ascending order of a list. Every

229+such initial segment ends right before an element satisfying the given

230+condition.

221231-}

222232initsEndAt :: (a -> Bool) -> [a] -> [[a]]

223233initsEndAt p [] = []

@@ -226,7 +236,7 @@ initsEndAt p (x:xs) | p x = [] : x_inits_xs

226236 where x_inits_xs = [x : cs | cs <- initsEndAt p xs]

227237

228238

229−{- | Create a `Name' from a pair of strings representing a base name and its

239+{- | Create a `Name' from a pair of strings representing a base name and its

230240 namespace.

231241-}

232242mkName :: (String, String) -> Name

@@ -304,7 +314,7 @@ lastIndent = do ist <- get

304314 (x : xs) -> return x

305315 _ -> return 1

306316

307−-- | Applies parser in an indented position

317+-- | Applies parser in an indented position

308318indented :: IdrisParser a -> IdrisParser a

309319indented p = notEndBlock *> p <* keepTerminator

310320

@@ -326,7 +336,7 @@ indentedBlock1 p = do openBlock

326336 closeBlock

327337 return res

328338

329−-- | Applies parser to get a block with exactly one (possibly indented) statement

339+-- | Applies parser to get a block with exactly one (possibly indented) statement

330340indentedBlockS :: IdrisParser a -> IdrisParser a

331341indentedBlockS p = do openBlock

332342 pushIndent

@@ -452,7 +462,7 @@ accessibility = do reserved "public"; return Public

452462 <|> do reserved "private"; return Hidden

453463 <?> "accessibility modifier"

454464

455−-- | Adds accessibility option for function

465+-- | Adds accessibility option for function

456466addAcc :: Name -> Maybe Accessibility -> IdrisParser ()

457467addAcc n a = do i <- get

458468 put (i { hide_list = (n, a) : hide_list i })

src/Idris/Parser.hs+152−24

@@ -62,6 +62,7 @@ import System.FilePath

6262import System.IO

6363

6464{-

65+@

6566 grammar shortcut notation:

6667 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)

6768 RULE? = optional rule (i.e. RULE or nothing)

@@ -69,12 +70,16 @@ import System.IO

6970 RULE+ = repeated rule with at least one match (i.e. RULE one or more times)

7071 RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)

7172 RULE{n} = rule repeated n times

73+@

7274-}

7375

7476{- * Main grammar -}

7577

7678{- | Parses module definition

79+

80+@

7781 ModuleHeader ::= 'module' Identifier_t ';'?;

82+@

7883-}

7984moduleHeader :: IdrisParser [String]

8085moduleHeader = try (do reserved "module"

@@ -89,7 +94,10 @@ moduleHeader = try (do reserved "module"

8994 (x, '.':y) -> x : moduleName y

9095

9196{- | Parses an import statement

97+

98+@

9299 Import ::= 'import' Identifier_t ';'?;

100+@

93101 -}

94102import_ :: IdrisParser String

95103import_ = do reserved "import"

@@ -100,7 +108,10 @@ import_ = do reserved "import"

100108 where toPath f = foldl1' (</>) (Spl.splitOn "." f)

101109

102110{- | Parses program source

111+

112+@

103113 Prog ::= Decl* EOF;

114+@

104115 -}

105116prog :: SyntaxInfo -> IdrisParser [PDecl]

106117prog syn = do whiteSpace

@@ -110,7 +121,9 @@ prog syn = do whiteSpace

110121 let c = (concat decls)

111122 return c

112123

113−{- | Parses a top-level declaration

124+{-| Parses a top-level declaration

125+

126+@

114127Decl ::=

115128 Decl'

116129 | Using

@@ -125,6 +138,7 @@ Decl ::=

125138 | Transform

126139 | Import!

127140 ;

141+@

128142-}

129143decl :: SyntaxInfo -> IdrisParser [PDecl]

130144decl syn = do notEndBlock

@@ -150,6 +164,8 @@ decl syn = do notEndBlock

150164 return [d']

151165

152166{- | Parses a top-level declaration with possible syntax sugar

167+

168+@

153169Decl' ::=

154170 Fixity

155171 | FunDecl'

@@ -157,6 +173,7 @@ Decl' ::=

157173 | Record

158174 | SyntaxDecl

159175 ;

176+@

160177-}

161178decl' :: SyntaxInfo -> IdrisParser PDecl

162179decl' syn = fixity

@@ -167,7 +184,10 @@ decl' syn = fixity

167184 <?> "declaration"

168185

169186{- | Parses a syntax extension declaration (and adds the rule to parser state)

187+

188+@

170189 SyntaxDecl ::= SyntaxRule;

190+@

171191-}

172192syntaxDecl :: SyntaxInfo -> IdrisParser PDecl

173193syntaxDecl syn = do s <- syntaxRule syn

@@ -185,17 +205,24 @@ syntaxDecl syn = do s <- syntaxRule syn

185205 ename (Keyword n) = Just n

186206 ename _ = Nothing

187207

188−{- | Parses a syntax extension declaration

189−SyntaxRuleOpts ::= 'term' | 'pattern';

208+{- | Parses a syntax extension declaration

209+

210+@

211+SyntaxRuleOpts ::= 'term' | 'pattern';

212+@

190213

214+@

191215SyntaxRule ::=

192216 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;

217+@

193218

219+@

194220SyntaxSym ::= '[' Name_t ']'

195221 | '{' Name_t '}'

196222 | Name_t

197223 | StringLiteral_t

198224 ;

225+@

199226-}

200227syntaxRule :: SyntaxInfo -> IdrisParser Syntax

201228syntaxRule syn

@@ -231,11 +258,14 @@ syntaxRule syn

231258

232259

233260{- | Parses a syntax symbol (either binding variable, keyword or expression)

261+

262+@

234263SyntaxSym ::= '[' Name_t ']'

235264 | '{' Name_t '}'

236265 | Name_t

237266 | StringLiteral_t

238267 ;

268+@

239269 -}

240270syntaxSym :: IdrisParser SSymbol

241271syntaxSym = try (do lchar '['; n <- name; lchar ']'

@@ -249,7 +279,10 @@ syntaxSym = try (do lchar '['; n <- name; lchar ']'

249279 <?> "syntax symbol"

250280

251281{- | Parses a function declaration with possible syntax sugar

282+

283+@

252284 FunDecl ::= FunDecl';

285+@

253286-}

254287fnDecl :: SyntaxInfo -> IdrisParser [PDecl]

255288fnDecl syn = try (do notEndBlock

@@ -258,13 +291,16 @@ fnDecl syn = try (do notEndBlock

258291 let d' = fmap (desugar syn i) d

259292 return [d']) <?> "function declaration"

260293

261−{- Parses a function declaration

294+{-| Parses a function declaration

295+

296+@

262297 FunDecl' ::=

263298 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator

264299 | Postulate

265300 | Pattern

266301 | CAF

267302 ;

303+@

268304-}

269305fnDecl' :: SyntaxInfo -> IdrisParser PDecl

270306fnDecl' syn = checkFixity $

@@ -308,23 +344,29 @@ fnDecl' syn = checkFixity $

308344 | otherwise = return True

309345 fixityOK _ = return True

310346

311−{- Parses function options given initial options

347+{-| Parses function options given initial options

348+

349+@

312350FnOpts ::= 'total'

313351 | 'partial'

314352 | 'implicit'

315353 | '%' 'assert_total'

316354 | '%' 'error_handler'

317− | '%' 'reflection'

355+ | '%' 'reflection'

318356 | '%' 'specialise' '[' NameTimesList? ']'

319357 ;

358+@

320359

360+@

321361NameTimes ::= FnName Natural?;

362+@

322363

364+@

323365NameTimesList ::=

324366 NameTimes

325367 | NameTimes ',' NameTimesList

326368 ;

327−

369+@

328370-}

329371-- FIXME: Check compatability for function options (i.e. partal/total)

330372fnOpts :: [FnOpt] -> IdrisParser [FnOpt]

@@ -353,9 +395,11 @@ fnOpts opts

353395

354396{- | Parses a postulate

355397

398+@

356399Postulate ::=

357400 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator

358401 ;

402+@

359403-}

360404postulate :: SyntaxInfo -> IdrisParser PDecl

361405postulate syn = do doc <- try $ do doc <- option "" (docComment '|')

@@ -381,9 +425,11 @@ postulate syn = do doc <- try $ do doc <- option "" (docComment '|')

381425

382426{- | Parses a using declaration

383427

428+@

384429Using ::=

385430 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock

386431 ;

432+@

387433 -}

388434using_ :: SyntaxInfo -> IdrisParser [PDecl]

389435using_ syn =

@@ -395,11 +441,13 @@ using_ syn =

395441 return (concat ds)

396442 <?> "using declaration"

397443

398−{- | Parses a parameters declaration

444+{- | Parses a parameters declaration

399445

446+@

400447Params ::=

401448 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock

402449 ;

450+@

403451 -}

404452params :: SyntaxInfo -> IdrisParser [PDecl]

405453params syn =

@@ -414,9 +462,11 @@ params syn =

414462

415463{- | Parses a mutual declaration (for mutually recursive functions)

416464

465+@

417466Mutual ::=

418467 'mutual' OpenBlock Decl* CloseBlock

419468 ;

469+@

420470-}

421471mutual :: SyntaxInfo -> IdrisParser [PDecl]

422472mutual syn =

@@ -429,11 +479,13 @@ mutual syn =

429479 return [PMutual fc (concat ds)]

430480 <?> "mutual block"

431481

432−{- | Parses a namespace declaration

482+{-| Parses a namespace declaration

433483

484+@

434485Namespace ::=

435486 'namespace' identifier OpenBlock Decl+ CloseBlock

436487 ;

488+@

437489-}

438490namespace :: SyntaxInfo -> IdrisParser [PDecl]

439491namespace syn =

@@ -444,9 +496,12 @@ namespace syn =

444496 return [PNamespace n (concat ds)]

445497 <?> "namespace declaration"

446498

447−{- |Parses a methods block (for instances)

499+{- | Parses a methods block (for instances)

500+

501+@

448502 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock

449− -}

503+@

504+-}

450505instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]

451506instanceBlock syn = do reserved "where"

452507 openBlock

@@ -455,16 +510,20 @@ instanceBlock syn = do reserved "where"

455510 return (concat ds)

456511 <?> "instance block"

457512

458−{- |Parses a methods and instances block (for type classes)

513+{- | Parses a methods and instances block (for type classes)

459514

515+@

460516MethodOrInstance ::=

461517 FnDecl

462518 | Instance

463519 ;

520+@

464521

522+@

465523ClassBlock ::=

466524 'where' OpenBlock MethodOrInstance* CloseBlock

467525 ;

526+@

468527-}

469528classBlock :: SyntaxInfo -> IdrisParser [PDecl]

470529classBlock syn = do reserved "where"

@@ -474,16 +533,20 @@ classBlock syn = do reserved "where"

474533 return (concat ds)

475534 <?> "class block"

476535

477−{- |Parses a type class declaration

536+{-| Parses a type class declaration

478537

538+@

479539ClassArgument ::=

480540 Name

481541 | '(' Name ':' Expr ')'

482542 ;

543+@

483544

545+@

484546Class ::=

485547 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?

486548 ;

549+@

487550-}

488551class_ :: SyntaxInfo -> IdrisParser [PDecl]

489552class_ syn = do (doc, acc) <- try (do

@@ -504,13 +567,17 @@ class_ syn = do (doc, acc) <- try (do

504567 <|> do i <- name;

505568 return (i, PType)

506569

507−{- |Parses a type class instance declaration

570+{- | Parses a type class instance declaration

508571

572+@

509573 Instance ::=

510574 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?

511575 ;

576+@

512577

513− InstanceName ::= '[' Name ']';

578+@

579+InstanceName ::= '[' Name ']';

580+@

514581-}

515582instance_ :: SyntaxInfo -> IdrisParser [PDecl]

516583instance_ syn = do reserved "instance"; fc <- getFC

@@ -531,20 +598,27 @@ instance_ syn = do reserved "instance"; fc <- getFC

531598

532599

533600{- | Parses a using declaration list

601+

602+@

534603UsingDeclList ::=

535604 UsingDeclList'

536605 | NameList TypeSig

537606 ;

607+@

538608

609+@

539610UsingDeclList' ::=

540611 UsingDecl

541612 | UsingDecl ',' UsingDeclList'

542613 ;

614+@

543615

616+@

544617NameList ::=

545618 Name

546619 | Name ',' NameList

547620 ;

621+@

548622-}

549623usingDeclList :: SyntaxInfo -> IdrisParser [Using]

550624usingDeclList syn

@@ -556,10 +630,13 @@ usingDeclList syn

556630 <?> "using declaration list"

557631

558632{- |Parses a using declaration

633+

634+@

559635UsingDecl ::=

560636 FnName TypeSig

561637 | FnName FnName+

562638 ;

639+@

563640-}

564641usingDecl :: SyntaxInfo -> IdrisParser Using

565642usingDecl syn = try (do x <- fnName

@@ -571,8 +648,11 @@ usingDecl syn = try (do x <- fnName

571648 return (UConstraint c xs)

572649 <?> "using declaration"

573650

574−{- | Parse a clause with patterns

651+{- | Parse a clause with patterns

652+

653+@

575654Pattern ::= Clause;

655+@

576656-}

577657pattern :: SyntaxInfo -> IdrisParser PDecl

578658pattern syn = do fc <- getFC

@@ -581,7 +661,10 @@ pattern syn = do fc <- getFC

581661 <?> "pattern"

582662

583663{- | Parse a constant applicative form declaration

584− CAF ::= 'let' FnName '=' Expr Terminator;

664+

665+@

666+CAF ::= 'let' FnName '=' Expr Terminator;

667+@

585668-}

586669caf :: SyntaxInfo -> IdrisParser PDecl

587670caf syn = do reserved "let"

@@ -594,7 +677,10 @@ caf syn = do reserved "let"

594677 <?> "constant applicative form declaration"

595678

596679{- | Parse an argument expression

597− ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};

680+

681+@

682+ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};

683+@

598684-}

599685argExpr :: SyntaxInfo -> IdrisParser PTerm

600686argExpr syn = let syn' = syn { inPattern = True } in

@@ -602,12 +688,17 @@ argExpr syn = let syn' = syn { inPattern = True } in

602688 <?> "argument expression"

603689

604690{- | Parse a right hand side of a function

691+

692+@

605693RHS ::= '=' Expr

606694 | '?=' RHSName? Expr

607695 | 'impossible'

608696 ;

697+@

609698

699+@

610700RHSName ::= '{' FnName '}';

701+@

611702-}

612703rhs :: SyntaxInfo -> Name -> IdrisParser PTerm

613704rhs syn n = do lchar '='; expr syn

@@ -630,16 +721,28 @@ rhs syn n = do lchar '='; expr syn

630721 addLet nm r = (PLet (sUN "value") Placeholder r (PMetavar nm))

631722

632723{- |Parses a function clause

724+

725+@

633726RHSOrWithBlock ::= RHS WhereOrTerminator

634727 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock

635728 ;

729+@

730+

731+@

636732Clause ::= WExpr+ RHSOrWithBlock

637733 | SimpleExpr '<==' FnName RHS WhereOrTerminator

638734 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}

639735 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock

640736 ;

737+@

738+

739+@

641740ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;

642−WhereOrTerminator ::= WhereBlock | Terminator;

741+@

742+

743+@

744+WhereOrTerminator ::= WhereBlock | Terminator;

745+@

643746-}

644747clause :: SyntaxInfo -> IdrisParser PClause

645748clause syn

@@ -768,17 +871,23 @@ clause syn

768871 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)

769872 fillLHSD n c a x = x

770873

771−{- |Parses with pattern

772− WExpr ::= '|' Expr';

874+{-| Parses with pattern

875+

876+@

877+WExpr ::= '|' Expr';

878+@

773879-}

774880wExpr :: SyntaxInfo -> IdrisParser PTerm

775881wExpr syn = do lchar '|'

776882 expr' syn

777883 <?> "with pattern"

778884

779−{- |Parses a where block

885+{- | Parses a where block

886+

887+@

780888WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;

781− -}

889+@

890+-}

782891whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])

783892whereBlock n syn

784893 = do reserved "where"

@@ -788,6 +897,8 @@ whereBlock n syn

788897 <?> "where block"

789898

790899{- |Parses a code generation target language name

900+

901+@

791902Codegen ::= 'C'

792903 | 'Java'

793904 | 'JavaScript'

@@ -795,6 +906,7 @@ Codegen ::= 'C'

795906 | 'LLVM'

796907 | 'Bytecode'

797908 ;

909+@

798910-}

799911codegen_ :: IdrisParser Codegen

800912codegen_ = do reserved "C"; return ViaC

@@ -806,13 +918,18 @@ codegen_ = do reserved "C"; return ViaC

806918 <?> "code generation language"

807919

808920{- |Parses a compiler directive

921+@

809922StringList ::=

810923 String

811924 | String ',' StringList

812925 ;

926+@

813927

928+@

814929Directive ::= '%' Directive';

930+@

815931

932+@

816933Directive' ::= 'lib' CodeGen String_t

817934 | 'link' CodeGen String_t

818935 | 'flag' CodeGen String_t

@@ -827,6 +944,7 @@ Directive' ::= 'lib' CodeGen String_t

827944 | 'language' 'TypeProviders'

828945 | 'language' 'ErrorReflection'

829946 ;

947+@

830948-}

831949directive :: SyntaxInfo -> IdrisParser [PDecl]

832950directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;

@@ -886,15 +1004,22 @@ pLangExt = (reserved "TypeProviders" >> return TypeProviders)

8861004 <|> (reserved "ErrorReflection" >> return ErrorReflection)

8871005

8881006{- | Parses a totality

1007+

1008+@

8891009Totality ::= 'partial' | 'total'

1010+@

1011+

8901012-}

8911013totality :: IdrisParser Bool

8921014totality

8931015 = do reserved "total"; return True

8941016 <|> do reserved "partial"; return False

8951017

896−{- | Parses a type provider

1018+{- | Parses a type provider

1019+

1020+@

8971021Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;

1022+@

8981023 -}

8991024provider :: SyntaxInfo -> IdrisParser [PDecl]

9001025provider syn = do try (lchar '%' *> reserved "provide");

@@ -906,7 +1031,10 @@ provider syn = do try (lchar '%' *> reserved "provide");

9061031 <?> "type provider"

9071032

9081033{- | Parses a transform

1034+

1035+@

9091036Transform ::= '%' 'transform' Expr '==>' Expr

1037+@

9101038-}

9111039transform :: SyntaxInfo -> IdrisParser [PDecl]

9121040transform syn = do try (lchar '%' *> reserved "transform")

src/Pkg/Package.hs+2−2

@@ -24,14 +24,14 @@ import Pkg.PParser

2424

2525import Paths_idris (getDataDir)

2626

27−-- | Run the package through the idris compiler.

28−--

2927-- To build a package:

3028-- * read the package description

3129-- * check all the library dependencies exist

3230-- * invoke the makefile if there is one

3331-- * invoke idris on each module, with idris_opts

3432-- * install everything into datadir/pname, if install flag is set

33+

34+-- | Run the package through the idris compiler.

3535buildPkg :: Bool -> (Bool, FilePath) -> IO ()

3636buildPkg warnonly (install, fp)

3737 = do pkgdesc <- parseDesc fp