961f9b4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #797 from jfdm/documentation

Updated Haddock Documentation.

commit961f9b4119e93238ed1cf65d1404c877c34752d4 authorEdwin Brady <edwin.brady@gmail.com> dateThu 30 Jan 2014, 02:17 (13 years ago) parentfee6a00 878653b

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

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

3232

3333import System.FilePath

3434

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

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

3636type IdrisParser = StateT IState IdrisInnerParser

3737

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

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

4141instance TokenParsing IdrisInnerParser where

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

4343

44−-- | Generalized monadic parsing constraint type

44+-- | Generalized monadic parsing constraint type

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

4646

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

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

5050

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

5252

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

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

5454simpleWhiteSpace :: MonadicParsing m => m ()

5555simpleWhiteSpace = satisfy isSpace *> pure ()

5656

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

6969isDocCommentMarker _ = False

7070

7171{- | Consumes a single-line comment

72+

73+@

7274 SingleLineComment_t ::= '--' EOL_t

7375 | '--' ~DocCommentMarker_t ~EOL_t* EOL_t

7476 ;

77+@

7578 -}

7679singleLineComment :: MonadicParsing m => m ()

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

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

7982 <?> ""

8083

8184{- | Consumes a multi-line comment

85+

86+@

8287 MultiLineComment_t ::=

8388 '{ -- }'

8489 | '{ -' ~DocCommentMarker_t InCommentChars_t

8590 ;

91+@

8692

93+@

8794 InCommentChars_t ::=

8895 '- }'

8996 | MultiLineComment_t InCommentChars_t

9097 | ~'- }'+ InCommentChars_t

9198 ;

92− -}

93−

99+@

100+-}

94101multiLineComment :: MonadicParsing m => m ()

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

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

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

107114 startEnd = "{}-"

108115

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

117+

118+@

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

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

112121 ;

122+@

113123 -}

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

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

@@ -139,14 +149,14 @@ natural = Tok.natural

139149integer :: MonadicParsing m => m Integer

140150integer = Tok.integer

141151

142−-- | Parses a floating point number

152+-- | Parses a floating point number

143153float :: MonadicParsing m => m Double

144154float = Tok.double

145155

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

147157

148158

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

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

150160idrisStyle :: MonadicParsing m => IdentifierStyle m

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

152162 where _styleName = "Idris"

@@ -220,9 +230,9 @@ name = (<?> "name") $ do

220230 unalias aliases (NS n ns) | Just ns' <- M.lookup ns aliases = NS n ns'

221231 unalias aliases name = name

222232

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

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

225− condition.

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

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

235+condition.

226236-}

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

228238initsEndAt p [] = []

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

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

232242

233243

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

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

235245 namespace.

236246-}

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

@@ -309,7 +319,7 @@ lastIndent = do ist <- get

309319 (x : xs) -> return x

310320 _ -> return 1

311321

312−-- | Applies parser in an indented position

322+-- | Applies parser in an indented position

313323indented :: IdrisParser a -> IdrisParser a

314324indented p = notEndBlock *> p <* keepTerminator

315325

@@ -331,7 +341,7 @@ indentedBlock1 p = do openBlock

331341 closeBlock

332342 return res

333343

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

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

335345indentedBlockS :: IdrisParser a -> IdrisParser a

336346indentedBlockS p = do openBlock

337347 pushIndent

@@ -457,7 +467,7 @@ accessibility = do reserved "public"; return Public

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

458468 <?> "accessibility modifier"

459469

460−-- | Adds accessibility option for function

470+-- | Adds accessibility option for function

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

462472addAcc n a = do i <- get

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

src/Idris/Parser.hs+152−24

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

6565import System.IO

6666

6767{-

68+@

6869 grammar shortcut notation:

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

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

@@ -72,12 +73,16 @@ import System.IO

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

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

7475 RULE{n} = rule repeated n times

76+@

7577-}

7678

7779{- * Main grammar -}

7880

7981{- | Parses module definition

82+

83+@

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

85+@

8186-}

8287moduleHeader :: IdrisParser [String]

8388moduleHeader = try (do reserved "module"

@@ -92,7 +97,10 @@ moduleHeader = try (do reserved "module"

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

9398

9499{- | Parses an import statement

100+

101+@

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

103+@

96104 -}

97105import_ :: IdrisParser (String, Maybe String, FC)

98106import_ = do fc <- getFC

@@ -105,7 +113,10 @@ import_ = do fc <- getFC

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

106114

107115{- | Parses program source

116+

117+@

108118 Prog ::= Decl* EOF;

119+@

109120 -}

110121prog :: SyntaxInfo -> IdrisParser [PDecl]

111122prog syn = do whiteSpace

@@ -115,7 +126,9 @@ prog syn = do whiteSpace

115126 let c = (concat decls)

116127 return c

117128

118−{- | Parses a top-level declaration

129+{-| Parses a top-level declaration

130+

131+@

119132Decl ::=

120133 Decl'

121134 | Using

@@ -130,6 +143,7 @@ Decl ::=

130143 | Transform

131144 | Import!

132145 ;

146+@

133147-}

134148decl :: SyntaxInfo -> IdrisParser [PDecl]

135149decl syn = do notEndBlock

@@ -155,6 +169,8 @@ decl syn = do notEndBlock

155169 return [d']

156170

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

172+

173+@

158174Decl' ::=

159175 Fixity

160176 | FunDecl'

@@ -162,6 +178,7 @@ Decl' ::=

162178 | Record

163179 | SyntaxDecl

164180 ;

181+@

165182-}

166183decl' :: SyntaxInfo -> IdrisParser PDecl

167184decl' syn = fixity

@@ -172,7 +189,10 @@ decl' syn = fixity

172189 <?> "declaration"

173190

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

192+

193+@

175194 SyntaxDecl ::= SyntaxRule;

195+@

176196-}

177197syntaxDecl :: SyntaxInfo -> IdrisParser PDecl

178198syntaxDecl syn = do s <- syntaxRule syn

@@ -190,17 +210,24 @@ syntaxDecl syn = do s <- syntaxRule syn

190210 ename (Keyword n) = Just n

191211 ename _ = Nothing

192212

193−{- | Parses a syntax extension declaration

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

213+{- | Parses a syntax extension declaration

214+

215+@

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

217+@

195218

219+@

196220SyntaxRule ::=

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

222+@

198223

224+@

199225SyntaxSym ::= '[' Name_t ']'

200226 | '{' Name_t '}'

201227 | Name_t

202228 | StringLiteral_t

203229 ;

230+@

204231-}

205232syntaxRule :: SyntaxInfo -> IdrisParser Syntax

206233syntaxRule syn

@@ -236,11 +263,14 @@ syntaxRule syn

236263

237264

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

266+

267+@

239268SyntaxSym ::= '[' Name_t ']'

240269 | '{' Name_t '}'

241270 | Name_t

242271 | StringLiteral_t

243272 ;

273+@

244274 -}

245275syntaxSym :: IdrisParser SSymbol

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

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

254284 <?> "syntax symbol"

255285

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

287+

288+@

257289 FunDecl ::= FunDecl';

290+@

258291-}

259292fnDecl :: SyntaxInfo -> IdrisParser [PDecl]

260293fnDecl syn = try (do notEndBlock

@@ -263,13 +296,16 @@ fnDecl syn = try (do notEndBlock

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

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

265298

266−{- Parses a function declaration

299+{-| Parses a function declaration

300+

301+@

267302 FunDecl' ::=

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

269304 | Postulate

270305 | Pattern

271306 | CAF

272307 ;

308+@

273309-}

274310fnDecl' :: SyntaxInfo -> IdrisParser PDecl

275311fnDecl' syn = checkFixity $

@@ -313,23 +349,29 @@ fnDecl' syn = checkFixity $

313349 | otherwise = return True

314350 fixityOK _ = return True

315351

316−{- Parses function options given initial options

352+{-| Parses function options given initial options

353+

354+@

317355FnOpts ::= 'total'

318356 | 'partial'

319357 | 'implicit'

320358 | '%' 'assert_total'

321359 | '%' 'error_handler'

322− | '%' 'reflection'

360+ | '%' 'reflection'

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

324362 ;

363+@

325364

365+@

326366NameTimes ::= FnName Natural?;

367+@

327368

369+@

328370NameTimesList ::=

329371 NameTimes

330372 | NameTimes ',' NameTimesList

331373 ;

332−

374+@

333375-}

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

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

@@ -360,9 +402,11 @@ fnOpts opts

360402

361403{- | Parses a postulate

362404

405+@

363406Postulate ::=

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

365408 ;

409+@

366410-}

367411postulate :: SyntaxInfo -> IdrisParser PDecl

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

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

388432

389433{- | Parses a using declaration

390434

435+@

391436Using ::=

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

393438 ;

439+@

394440 -}

395441using_ :: SyntaxInfo -> IdrisParser [PDecl]

396442using_ syn =

@@ -402,11 +448,13 @@ using_ syn =

402448 return (concat ds)

403449 <?> "using declaration"

404450

405−{- | Parses a parameters declaration

451+{- | Parses a parameters declaration

406452

453+@

407454Params ::=

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

409456 ;

457+@

410458 -}

411459params :: SyntaxInfo -> IdrisParser [PDecl]

412460params syn =

@@ -421,9 +469,11 @@ params syn =

421469

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

423471

472+@

424473Mutual ::=

425474 'mutual' OpenBlock Decl* CloseBlock

426475 ;

476+@

427477-}

428478mutual :: SyntaxInfo -> IdrisParser [PDecl]

429479mutual syn =

@@ -436,11 +486,13 @@ mutual syn =

436486 return [PMutual fc (concat ds)]

437487 <?> "mutual block"

438488

439−{- | Parses a namespace declaration

489+{-| Parses a namespace declaration

440490

491+@

441492Namespace ::=

442493 'namespace' identifier OpenBlock Decl+ CloseBlock

443494 ;

495+@

444496-}

445497namespace :: SyntaxInfo -> IdrisParser [PDecl]

446498namespace syn =

@@ -451,9 +503,12 @@ namespace syn =

451503 return [PNamespace n (concat ds)]

452504 <?> "namespace declaration"

453505

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

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

507+

508+@

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

456− -}

510+@

511+-}

457512instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]

458513instanceBlock syn = do reserved "where"

459514 openBlock

@@ -462,16 +517,20 @@ instanceBlock syn = do reserved "where"

462517 return (concat ds)

463518 <?> "instance block"

464519

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

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

466521

522+@

467523MethodOrInstance ::=

468524 FnDecl

469525 | Instance

470526 ;

527+@

471528

529+@

472530ClassBlock ::=

473531 'where' OpenBlock MethodOrInstance* CloseBlock

474532 ;

533+@

475534-}

476535classBlock :: SyntaxInfo -> IdrisParser [PDecl]

477536classBlock syn = do reserved "where"

@@ -481,16 +540,20 @@ classBlock syn = do reserved "where"

481540 return (concat ds)

482541 <?> "class block"

483542

484−{- |Parses a type class declaration

543+{-| Parses a type class declaration

485544

545+@

486546ClassArgument ::=

487547 Name

488548 | '(' Name ':' Expr ')'

489549 ;

550+@

490551

552+@

491553Class ::=

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

493555 ;

556+@

494557-}

495558class_ :: SyntaxInfo -> IdrisParser [PDecl]

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

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

511574 <|> do i <- name;

512575 return (i, PType)

513576

514−{- |Parses a type class instance declaration

577+{- | Parses a type class instance declaration

515578

579+@

516580 Instance ::=

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

518582 ;

583+@

519584

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

585+@

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

587+@

521588-}

522589instance_ :: SyntaxInfo -> IdrisParser [PDecl]

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

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

538605

539606

540607{- | Parses a using declaration list

608+

609+@

541610UsingDeclList ::=

542611 UsingDeclList'

543612 | NameList TypeSig

544613 ;

614+@

545615

616+@

546617UsingDeclList' ::=

547618 UsingDecl

548619 | UsingDecl ',' UsingDeclList'

549620 ;

621+@

550622

623+@

551624NameList ::=

552625 Name

553626 | Name ',' NameList

554627 ;

628+@

555629-}

556630usingDeclList :: SyntaxInfo -> IdrisParser [Using]

557631usingDeclList syn

@@ -563,10 +637,13 @@ usingDeclList syn

563637 <?> "using declaration list"

564638

565639{- |Parses a using declaration

640+

641+@

566642UsingDecl ::=

567643 FnName TypeSig

568644 | FnName FnName+

569645 ;

646+@

570647-}

571648usingDecl :: SyntaxInfo -> IdrisParser Using

572649usingDecl syn = try (do x <- fnName

@@ -578,8 +655,11 @@ usingDecl syn = try (do x <- fnName

578655 return (UConstraint c xs)

579656 <?> "using declaration"

580657

581−{- | Parse a clause with patterns

658+{- | Parse a clause with patterns

659+

660+@

582661Pattern ::= Clause;

662+@

583663-}

584664pattern :: SyntaxInfo -> IdrisParser PDecl

585665pattern syn = do fc <- getFC

@@ -588,7 +668,10 @@ pattern syn = do fc <- getFC

588668 <?> "pattern"

589669

590670{- | Parse a constant applicative form declaration

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

671+

672+@

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

674+@

592675-}

593676caf :: SyntaxInfo -> IdrisParser PDecl

594677caf syn = do reserved "let"

@@ -601,7 +684,10 @@ caf syn = do reserved "let"

601684 <?> "constant applicative form declaration"

602685

603686{- | Parse an argument expression

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

687+

688+@

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

690+@

605691-}

606692argExpr :: SyntaxInfo -> IdrisParser PTerm

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

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

609695 <?> "argument expression"

610696

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

698+

699+@

612700RHS ::= '=' Expr

613701 | '?=' RHSName? Expr

614702 | 'impossible'

615703 ;

704+@

616705

706+@

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

708+@

618709-}

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

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

@@ -637,16 +728,28 @@ rhs syn n = do lchar '='; expr syn

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

638729

639730{- |Parses a function clause

731+

732+@

640733RHSOrWithBlock ::= RHS WhereOrTerminator

641734 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock

642735 ;

736+@

737+

738+@

643739Clause ::= WExpr+ RHSOrWithBlock

644740 | SimpleExpr '<==' FnName RHS WhereOrTerminator

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

646742 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock

647743 ;

744+@

745+

746+@

648747ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;

649−WhereOrTerminator ::= WhereBlock | Terminator;

748+@

749+

750+@

751+WhereOrTerminator ::= WhereBlock | Terminator;

752+@

650753-}

651754clause :: SyntaxInfo -> IdrisParser PClause

652755clause syn

@@ -775,17 +878,23 @@ clause syn

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

776879 fillLHSD n c a x = x

777880

778−{- |Parses with pattern

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

881+{-| Parses with pattern

882+

883+@

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

885+@

780886-}

781887wExpr :: SyntaxInfo -> IdrisParser PTerm

782888wExpr syn = do lchar '|'

783889 expr' syn

784890 <?> "with pattern"

785891

786−{- |Parses a where block

892+{- | Parses a where block

893+

894+@

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

788− -}

896+@

897+-}

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

790899whereBlock n syn

791900 = do reserved "where"

@@ -795,6 +904,8 @@ whereBlock n syn

795904 <?> "where block"

796905

797906{- |Parses a code generation target language name

907+

908+@

798909Codegen ::= 'C'

799910 | 'Java'

800911 | 'JavaScript'

@@ -802,6 +913,7 @@ Codegen ::= 'C'

802913 | 'LLVM'

803914 | 'Bytecode'

804915 ;

916+@

805917-}

806918codegen_ :: IdrisParser Codegen

807919codegen_ = do reserved "C"; return ViaC

@@ -813,13 +925,18 @@ codegen_ = do reserved "C"; return ViaC

813925 <?> "code generation language"

814926

815927{- |Parses a compiler directive

928+@

816929StringList ::=

817930 String

818931 | String ',' StringList

819932 ;

933+@

820934

935+@

821936Directive ::= '%' Directive';

937+@

822938

939+@

823940Directive' ::= 'lib' CodeGen String_t

824941 | 'link' CodeGen String_t

825942 | 'flag' CodeGen String_t

@@ -834,6 +951,7 @@ Directive' ::= 'lib' CodeGen String_t

834951 | 'language' 'TypeProviders'

835952 | 'language' 'ErrorReflection'

836953 ;

954+@

837955-}

838956directive :: SyntaxInfo -> IdrisParser [PDecl]

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

@@ -893,15 +1011,22 @@ pLangExt = (reserved "TypeProviders" >> return TypeProviders)

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

8941012

8951013{- | Parses a totality

1014+

1015+@

8961016Totality ::= 'partial' | 'total'

1017+@

1018+

8971019-}

8981020totality :: IdrisParser Bool

8991021totality

9001022 = do reserved "total"; return True

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

9021024

903−{- | Parses a type provider

1025+{- | Parses a type provider

1026+

1027+@

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

1029+@

9051030 -}

9061031provider :: SyntaxInfo -> IdrisParser [PDecl]

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

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

9131038 <?> "type provider"

9141039

9151040{- | Parses a transform

1041+

1042+@

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

1044+@

9171045-}

9181046transform :: SyntaxInfo -> IdrisParser [PDecl]

9191047transform 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