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

git.iko.soy/Idris-dev

on master help sign in

Updated Haddock Documentation.

878653bJan de Muijnck-Hughes13 years ago

src/Idris/ParseExpr.hs+3−1

compare with master

unifiedsplit

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

757 <?> "quote goal expression"

758

759{- | Parses a dependent type signature

760+

760@

761@

761Pi ::=

762Pi ::=

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

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

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

1030 <?> "constant or literal"

1031 <?> "constant or literal"

1031

1032

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

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

1034+

1033@

1035@

1034VerbatimString_t ::=

1036VerbatimString_t ::=

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

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

1036@

1038@

1037 -}

1039 -}

1038verbatimStringLiteral :: MonadicParsing m => m String

1040verbatimStringLiteral :: MonadicParsing m => m String

src/Idris/ParseHelpers.hs+24−14

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

32import System.FilePath

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

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

35type IdrisParser = StateT IState IdrisInnerParser

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

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

40instance TokenParsing IdrisInnerParser where

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

43−-- | Generalized monadic parsing constraint type

43+-- | Generalized monadic parsing constraint type

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

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

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

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

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

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

53simpleWhiteSpace :: MonadicParsing m => m ()

54simpleWhiteSpace = satisfy isSpace *> pure ()

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

68isDocCommentMarker _ = False

70{- | Consumes a single-line comment

71+

72+@

71 SingleLineComment_t ::= '--' EOL_t

73 SingleLineComment_t ::= '--' EOL_t

72 | '--' ~DocCommentMarker_t ~EOL_t* EOL_t

74 | '--' ~DocCommentMarker_t ~EOL_t* EOL_t

73 ;

75 ;

76+@

74 -}

77 -}

75singleLineComment :: MonadicParsing m => m ()

78singleLineComment :: MonadicParsing m => m ()

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

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

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

78 <?> ""

81 <?> ""

80{- | Consumes a multi-line comment

83{- | Consumes a multi-line comment

84+

85+@

81 MultiLineComment_t ::=

86 MultiLineComment_t ::=

82 '{ -- }'

87 '{ -- }'

83 | '{ -' ~DocCommentMarker_t InCommentChars_t

88 | '{ -' ~DocCommentMarker_t InCommentChars_t

84 ;

89 ;

90+@

92+@

86 InCommentChars_t ::=

93 InCommentChars_t ::=

87 '- }'

94 '- }'

88 | MultiLineComment_t InCommentChars_t

95 | MultiLineComment_t InCommentChars_t

89 | ~'- }'+ InCommentChars_t

96 | ~'- }'+ InCommentChars_t

90 ;

97 ;

98+@

91− -}

99+-}

92−

93multiLineComment :: MonadicParsing m => m ()

100multiLineComment :: MonadicParsing m => m ()

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

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

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

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

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

106 startEnd = "{}-"

113 startEnd = "{}-"

107

114

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

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

116+

117+@

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

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

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

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

111 ;

120 ;

121+@

112 -}

122 -}

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

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

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

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

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

138integer :: MonadicParsing m => m Integer

148integer :: MonadicParsing m => m Integer

139integer = Tok.integer

149integer = Tok.integer

140

150

141−-- | Parses a floating point number

151+-- | Parses a floating point number

142float :: MonadicParsing m => m Double

152float :: MonadicParsing m => m Double

143float = Tok.double

153float = Tok.double

144

154

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

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

146

156

147

157

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

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

149idrisStyle :: MonadicParsing m => IdentifierStyle m

159idrisStyle :: MonadicParsing m => IdentifierStyle m

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

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

151 where _styleName = "Idris"

161 where _styleName = "Idris"

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

215 <?> "name"

225 <?> "name"

216

226

217

227

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

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

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

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

220− condition.

230+condition.

221-}

231-}

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

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

223initsEndAt p [] = []

233initsEndAt p [] = []

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

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

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

227

237

228

238

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

230 namespace.

240 namespace.

231-}

241-}

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

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

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

304 (x : xs) -> return x

314 (x : xs) -> return x

305 _ -> return 1

315 _ -> return 1

306

316

307−-- | Applies parser in an indented position

317+-- | Applies parser in an indented position

308indented :: IdrisParser a -> IdrisParser a

318indented :: IdrisParser a -> IdrisParser a

309indented p = notEndBlock *> p <* keepTerminator

319indented p = notEndBlock *> p <* keepTerminator

310

320

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

326 closeBlock

336 closeBlock

327 return res

337 return res

328

338

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

330indentedBlockS :: IdrisParser a -> IdrisParser a

340indentedBlockS :: IdrisParser a -> IdrisParser a

331indentedBlockS p = do openBlock

341indentedBlockS p = do openBlock

332 pushIndent

342 pushIndent

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

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

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

453 <?> "accessibility modifier"

463 <?> "accessibility modifier"

454

464

455−-- | Adds accessibility option for function

465+-- | Adds accessibility option for function

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

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

457addAcc n a = do i <- get

467addAcc n a = do i <- get

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

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

src/Idris/Parser.hs+152−24

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

62import System.IO

64{-

65+@

65 grammar shortcut notation:

66 grammar shortcut notation:

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

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

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

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

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

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

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

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

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

71 RULE{n} = rule repeated n times

72 RULE{n} = rule repeated n times

73+@

72-}

74-}

74{- * Main grammar -}

76{- * Main grammar -}

76{- | Parses module definition

78{- | Parses module definition

79+

80+@

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

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

82+@

78-}

83-}

79moduleHeader :: IdrisParser [String]

84moduleHeader :: IdrisParser [String]

80moduleHeader = try (do reserved "module"

85moduleHeader = try (do reserved "module"

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

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

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

91{- | Parses an import statement

96{- | Parses an import statement

97+

98+@

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

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

100+@

93 -}

101 -}

94import_ :: IdrisParser String

102import_ :: IdrisParser String

95import_ = do reserved "import"

103import_ = do reserved "import"

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

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

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

101

109

102{- | Parses program source

110{- | Parses program source

111+

112+@

103 Prog ::= Decl* EOF;

113 Prog ::= Decl* EOF;

114+@

104 -}

115 -}

105prog :: SyntaxInfo -> IdrisParser [PDecl]

116prog :: SyntaxInfo -> IdrisParser [PDecl]

106prog syn = do whiteSpace

117prog syn = do whiteSpace

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

110 let c = (concat decls)

121 let c = (concat decls)

111 return c

122 return c

112

123

113−{- | Parses a top-level declaration

124+{-| Parses a top-level declaration

125+

126+@

114Decl ::=

127Decl ::=

115 Decl'

128 Decl'

116 | Using

129 | Using

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

125 | Transform

138 | Transform

126 | Import!

139 | Import!

127 ;

140 ;

141+@

128-}

142-}

129decl :: SyntaxInfo -> IdrisParser [PDecl]

143decl :: SyntaxInfo -> IdrisParser [PDecl]

130decl syn = do notEndBlock

144decl syn = do notEndBlock

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

150 return [d']

164 return [d']

151

165

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

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

167+

168+@

153Decl' ::=

169Decl' ::=

154 Fixity

170 Fixity

155 | FunDecl'

171 | FunDecl'

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

157 | Record

173 | Record

158 | SyntaxDecl

174 | SyntaxDecl

159 ;

175 ;

176+@

160-}

177-}

161decl' :: SyntaxInfo -> IdrisParser PDecl

178decl' :: SyntaxInfo -> IdrisParser PDecl

162decl' syn = fixity

179decl' syn = fixity

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

167 <?> "declaration"

184 <?> "declaration"

168

185

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

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

187+

188+@

170 SyntaxDecl ::= SyntaxRule;

189 SyntaxDecl ::= SyntaxRule;

190+@

171-}

191-}

172syntaxDecl :: SyntaxInfo -> IdrisParser PDecl

192syntaxDecl :: SyntaxInfo -> IdrisParser PDecl

173syntaxDecl syn = do s <- syntaxRule syn

193syntaxDecl syn = do s <- syntaxRule syn

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

185 ename (Keyword n) = Just n

205 ename (Keyword n) = Just n

186 ename _ = Nothing

206 ename _ = Nothing

187

207

188−{- | Parses a syntax extension declaration

208+{- | Parses a syntax extension declaration

209+

210+@

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

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

212+@

190

213

214+@

191SyntaxRule ::=

215SyntaxRule ::=

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

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

217+@

193

218

219+@

194SyntaxSym ::= '[' Name_t ']'

220SyntaxSym ::= '[' Name_t ']'

195 | '{' Name_t '}'

221 | '{' Name_t '}'

196 | Name_t

222 | Name_t

197 | StringLiteral_t

223 | StringLiteral_t

198 ;

224 ;

225+@

199-}

226-}

200syntaxRule :: SyntaxInfo -> IdrisParser Syntax

227syntaxRule :: SyntaxInfo -> IdrisParser Syntax

201syntaxRule syn

228syntaxRule syn

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

231

258

232

259

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

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

261+

262+@

234SyntaxSym ::= '[' Name_t ']'

263SyntaxSym ::= '[' Name_t ']'

235 | '{' Name_t '}'

264 | '{' Name_t '}'

236 | Name_t

265 | Name_t

237 | StringLiteral_t

266 | StringLiteral_t

238 ;

267 ;

268+@

239 -}

269 -}

240syntaxSym :: IdrisParser SSymbol

270syntaxSym :: IdrisParser SSymbol

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

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

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

249 <?> "syntax symbol"

279 <?> "syntax symbol"

250

280

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

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

282+

283+@

252 FunDecl ::= FunDecl';

284 FunDecl ::= FunDecl';

285+@

253-}

286-}

254fnDecl :: SyntaxInfo -> IdrisParser [PDecl]

287fnDecl :: SyntaxInfo -> IdrisParser [PDecl]

255fnDecl syn = try (do notEndBlock

288fnDecl syn = try (do notEndBlock

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

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

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

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

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

260

293

261−{- Parses a function declaration

294+{-| Parses a function declaration

295+

296+@

262 FunDecl' ::=

297 FunDecl' ::=

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

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

264 | Postulate

299 | Postulate

265 | Pattern

300 | Pattern

266 | CAF

301 | CAF

267 ;

302 ;

303+@

268-}

304-}

269fnDecl' :: SyntaxInfo -> IdrisParser PDecl

305fnDecl' :: SyntaxInfo -> IdrisParser PDecl

270fnDecl' syn = checkFixity $

306fnDecl' syn = checkFixity $

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

308 | otherwise = return True

344 | otherwise = return True

309 fixityOK _ = return True

345 fixityOK _ = return True

310

346

311−{- Parses function options given initial options

347+{-| Parses function options given initial options

348+

349+@

312FnOpts ::= 'total'

350FnOpts ::= 'total'

313 | 'partial'

351 | 'partial'

314 | 'implicit'

352 | 'implicit'

315 | '%' 'assert_total'

353 | '%' 'assert_total'

316 | '%' 'error_handler'

354 | '%' 'error_handler'

317− | '%' 'reflection'

355+ | '%' 'reflection'

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

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

319 ;

357 ;

358+@

320

359

360+@

321NameTimes ::= FnName Natural?;

361NameTimes ::= FnName Natural?;

362+@

322

363

364+@

323NameTimesList ::=

365NameTimesList ::=

324 NameTimes

366 NameTimes

325 | NameTimes ',' NameTimesList

367 | NameTimes ',' NameTimesList

326 ;

368 ;

327−

369+@

328-}

370-}

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

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

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

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

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

353

395

354{- | Parses a postulate

396{- | Parses a postulate

355

397

398+@

356Postulate ::=

399Postulate ::=

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

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

358 ;

401 ;

402+@

359-}

403-}

360postulate :: SyntaxInfo -> IdrisParser PDecl

404postulate :: SyntaxInfo -> IdrisParser PDecl

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

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

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

381

425

382{- | Parses a using declaration

426{- | Parses a using declaration

383

427

428+@

384Using ::=

429Using ::=

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

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

386 ;

431 ;

432+@

387 -}

433 -}

388using_ :: SyntaxInfo -> IdrisParser [PDecl]

434using_ :: SyntaxInfo -> IdrisParser [PDecl]

389using_ syn =

435using_ syn =

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

395 return (concat ds)

441 return (concat ds)

396 <?> "using declaration"

442 <?> "using declaration"

397

443

398−{- | Parses a parameters declaration

444+{- | Parses a parameters declaration

399

445

446+@

400Params ::=

447Params ::=

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

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

402 ;

449 ;

450+@

403 -}

451 -}

404params :: SyntaxInfo -> IdrisParser [PDecl]

452params :: SyntaxInfo -> IdrisParser [PDecl]

405params syn =

453params syn =

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

414

462

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

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

416

464

465+@

417Mutual ::=

466Mutual ::=

418 'mutual' OpenBlock Decl* CloseBlock

467 'mutual' OpenBlock Decl* CloseBlock

419 ;

468 ;

469+@

420-}

470-}

421mutual :: SyntaxInfo -> IdrisParser [PDecl]

471mutual :: SyntaxInfo -> IdrisParser [PDecl]

422mutual syn =

472mutual syn =

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

429 return [PMutual fc (concat ds)]

479 return [PMutual fc (concat ds)]

430 <?> "mutual block"

480 <?> "mutual block"

431

481

432−{- | Parses a namespace declaration

482+{-| Parses a namespace declaration

433

483

484+@

434Namespace ::=

485Namespace ::=

435 'namespace' identifier OpenBlock Decl+ CloseBlock

486 'namespace' identifier OpenBlock Decl+ CloseBlock

436 ;

487 ;

488+@

437-}

489-}

438namespace :: SyntaxInfo -> IdrisParser [PDecl]

490namespace :: SyntaxInfo -> IdrisParser [PDecl]

439namespace syn =

491namespace syn =

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

444 return [PNamespace n (concat ds)]

496 return [PNamespace n (concat ds)]

445 <?> "namespace declaration"

497 <?> "namespace declaration"

446

498

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

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

500+

501+@

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

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

503+@

449− -}

504+-}

450instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]

505instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]

451instanceBlock syn = do reserved "where"

506instanceBlock syn = do reserved "where"

452 openBlock

507 openBlock

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

455 return (concat ds)

510 return (concat ds)

456 <?> "instance block"

511 <?> "instance block"

457

512

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

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

459

514

515+@

460MethodOrInstance ::=

516MethodOrInstance ::=

461 FnDecl

517 FnDecl

462 | Instance

518 | Instance

463 ;

519 ;

520+@

464

521

522+@

465ClassBlock ::=

523ClassBlock ::=

466 'where' OpenBlock MethodOrInstance* CloseBlock

524 'where' OpenBlock MethodOrInstance* CloseBlock

467 ;

525 ;

526+@

468-}

527-}

469classBlock :: SyntaxInfo -> IdrisParser [PDecl]

528classBlock :: SyntaxInfo -> IdrisParser [PDecl]

470classBlock syn = do reserved "where"

529classBlock syn = do reserved "where"

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

474 return (concat ds)

533 return (concat ds)

475 <?> "class block"

534 <?> "class block"

476

535

477−{- |Parses a type class declaration

536+{-| Parses a type class declaration

478

537

538+@

479ClassArgument ::=

539ClassArgument ::=

480 Name

540 Name

481 | '(' Name ':' Expr ')'

541 | '(' Name ':' Expr ')'

482 ;

542 ;

543+@

483

544

545+@

484Class ::=

546Class ::=

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

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

486 ;

548 ;

549+@

487-}

550-}

488class_ :: SyntaxInfo -> IdrisParser [PDecl]

551class_ :: SyntaxInfo -> IdrisParser [PDecl]

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

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

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

504 <|> do i <- name;

567 <|> do i <- name;

505 return (i, PType)

568 return (i, PType)

506

569

507−{- |Parses a type class instance declaration

570+{- | Parses a type class instance declaration

508

571

572+@

509 Instance ::=

573 Instance ::=

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

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

511 ;

575 ;

576+@

512

577

578+@

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

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

580+@

514-}

581-}

515instance_ :: SyntaxInfo -> IdrisParser [PDecl]

582instance_ :: SyntaxInfo -> IdrisParser [PDecl]

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

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

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

531

598

532

599

533{- | Parses a using declaration list

600{- | Parses a using declaration list

601+

602+@

534UsingDeclList ::=

603UsingDeclList ::=

535 UsingDeclList'

604 UsingDeclList'

536 | NameList TypeSig

605 | NameList TypeSig

537 ;

606 ;

607+@

538

608

609+@

539UsingDeclList' ::=

610UsingDeclList' ::=

540 UsingDecl

611 UsingDecl

541 | UsingDecl ',' UsingDeclList'

612 | UsingDecl ',' UsingDeclList'

542 ;

613 ;

614+@

543

615

616+@

544NameList ::=

617NameList ::=

545 Name

618 Name

546 | Name ',' NameList

619 | Name ',' NameList

547 ;

620 ;

621+@

548-}

622-}

549usingDeclList :: SyntaxInfo -> IdrisParser [Using]

623usingDeclList :: SyntaxInfo -> IdrisParser [Using]

550usingDeclList syn

624usingDeclList syn

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

556 <?> "using declaration list"

630 <?> "using declaration list"

557

631

558{- |Parses a using declaration

632{- |Parses a using declaration

633+

634+@

559UsingDecl ::=

635UsingDecl ::=

560 FnName TypeSig

636 FnName TypeSig

561 | FnName FnName+

637 | FnName FnName+

562 ;

638 ;

639+@

563-}

640-}

564usingDecl :: SyntaxInfo -> IdrisParser Using

641usingDecl :: SyntaxInfo -> IdrisParser Using

565usingDecl syn = try (do x <- fnName

642usingDecl syn = try (do x <- fnName

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

571 return (UConstraint c xs)

648 return (UConstraint c xs)

572 <?> "using declaration"

649 <?> "using declaration"

573

650

574−{- | Parse a clause with patterns

651+{- | Parse a clause with patterns

652+

653+@

575Pattern ::= Clause;

654Pattern ::= Clause;

655+@

576-}

656-}

577pattern :: SyntaxInfo -> IdrisParser PDecl

657pattern :: SyntaxInfo -> IdrisParser PDecl

578pattern syn = do fc <- getFC

658pattern syn = do fc <- getFC

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

581 <?> "pattern"

661 <?> "pattern"

582

662

583{- | Parse a constant applicative form declaration

663{- | Parse a constant applicative form declaration

664+

665+@

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

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

667+@

585-}

668-}

586caf :: SyntaxInfo -> IdrisParser PDecl

669caf :: SyntaxInfo -> IdrisParser PDecl

587caf syn = do reserved "let"

670caf syn = do reserved "let"

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

594 <?> "constant applicative form declaration"

677 <?> "constant applicative form declaration"

595

678

596{- | Parse an argument expression

679{- | Parse an argument expression

680+

681+@

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

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

683+@

598-}

684-}

599argExpr :: SyntaxInfo -> IdrisParser PTerm

685argExpr :: SyntaxInfo -> IdrisParser PTerm

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

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

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

602 <?> "argument expression"

688 <?> "argument expression"

603

689

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

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

691+

692+@

605RHS ::= '=' Expr

693RHS ::= '=' Expr

606 | '?=' RHSName? Expr

694 | '?=' RHSName? Expr

607 | 'impossible'

695 | 'impossible'

608 ;

696 ;

697+@

609

698

699+@

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

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

701+@

611-}

702-}

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

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

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

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

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

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

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

631

722

632{- |Parses a function clause

723{- |Parses a function clause

724+

725+@

633RHSOrWithBlock ::= RHS WhereOrTerminator

726RHSOrWithBlock ::= RHS WhereOrTerminator

634 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock

727 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock

635 ;

728 ;

729+@

730+

731+@

636Clause ::= WExpr+ RHSOrWithBlock

732Clause ::= WExpr+ RHSOrWithBlock

637 | SimpleExpr '<==' FnName RHS WhereOrTerminator

733 | SimpleExpr '<==' FnName RHS WhereOrTerminator

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

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

639 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock

735 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock

640 ;

736 ;

737+@

738+

739+@

641ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;

740ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;

741+@

742+

743+@

642−WhereOrTerminator ::= WhereBlock | Terminator;

744+WhereOrTerminator ::= WhereBlock | Terminator;

745+@

643-}

746-}

644clause :: SyntaxInfo -> IdrisParser PClause

747clause :: SyntaxInfo -> IdrisParser PClause

645clause syn

748clause syn

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

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

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

769 fillLHSD n c a x = x

872 fillLHSD n c a x = x

770

873

771−{- |Parses with pattern

874+{-| Parses with pattern

875+

876+@

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

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

878+@

773-}

879-}

774wExpr :: SyntaxInfo -> IdrisParser PTerm

880wExpr :: SyntaxInfo -> IdrisParser PTerm

775wExpr syn = do lchar '|'

881wExpr syn = do lchar '|'

776 expr' syn

882 expr' syn

777 <?> "with pattern"

883 <?> "with pattern"

778

884

779−{- |Parses a where block

885+{- | Parses a where block

886+

887+@

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

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

889+@

781− -}

890+-}

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

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

783whereBlock n syn

892whereBlock n syn

784 = do reserved "where"

893 = do reserved "where"

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

788 <?> "where block"

897 <?> "where block"

789

898

790{- |Parses a code generation target language name

899{- |Parses a code generation target language name

900+

901+@

791Codegen ::= 'C'

902Codegen ::= 'C'

792 | 'Java'

903 | 'Java'

793 | 'JavaScript'

904 | 'JavaScript'

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

795 | 'LLVM'

906 | 'LLVM'

796 | 'Bytecode'

907 | 'Bytecode'

797 ;

908 ;

909+@

798-}

910-}

799codegen_ :: IdrisParser Codegen

911codegen_ :: IdrisParser Codegen

800codegen_ = do reserved "C"; return ViaC

912codegen_ = do reserved "C"; return ViaC

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

806 <?> "code generation language"

918 <?> "code generation language"

807

919

808{- |Parses a compiler directive

920{- |Parses a compiler directive

921+@

809StringList ::=

922StringList ::=

810 String

923 String

811 | String ',' StringList

924 | String ',' StringList

812 ;

925 ;

926+@

813

927

928+@

814Directive ::= '%' Directive';

929Directive ::= '%' Directive';

930+@

815

931

932+@

816Directive' ::= 'lib' CodeGen String_t

933Directive' ::= 'lib' CodeGen String_t

817 | 'link' CodeGen String_t

934 | 'link' CodeGen String_t

818 | 'flag' CodeGen String_t

935 | 'flag' CodeGen String_t

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

827 | 'language' 'TypeProviders'

944 | 'language' 'TypeProviders'

828 | 'language' 'ErrorReflection'

945 | 'language' 'ErrorReflection'

829 ;

946 ;

947+@

830-}

948-}

831directive :: SyntaxInfo -> IdrisParser [PDecl]

949directive :: SyntaxInfo -> IdrisParser [PDecl]

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

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

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

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

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

887

1005

888{- | Parses a totality

1006{- | Parses a totality

1007+

1008+@

889Totality ::= 'partial' | 'total'

1009Totality ::= 'partial' | 'total'

1010+@

1011+

890-}

1012-}

891totality :: IdrisParser Bool

1013totality :: IdrisParser Bool

892totality

1014totality

893 = do reserved "total"; return True

1015 = do reserved "total"; return True

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

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

895

1017

896−{- | Parses a type provider

1018+{- | Parses a type provider

1019+

1020+@

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

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

1022+@

898 -}

1023 -}

899provider :: SyntaxInfo -> IdrisParser [PDecl]

1024provider :: SyntaxInfo -> IdrisParser [PDecl]

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

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

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

906 <?> "type provider"

1031 <?> "type provider"

907

1032

908{- | Parses a transform

1033{- | Parses a transform

1034+

1035+@

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

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

1037+@

910-}

1038-}

911transform :: SyntaxInfo -> IdrisParser [PDecl]

1039transform :: SyntaxInfo -> IdrisParser [PDecl]

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

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

src/Pkg/Package.hs+2−2

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

25import Paths_idris (getDataDir)

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

28−--

29-- To build a package:

27-- To build a package:

30-- * read the package description

28-- * read the package description

31-- * check all the library dependencies exist

29-- * check all the library dependencies exist

32-- * invoke the makefile if there is one

30-- * invoke the makefile if there is one

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

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

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

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

33+

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

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

36buildPkg warnonly (install, fp)

37 = do pkgdesc <- parseDesc fp