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

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #797 from jfdm/documentation

961f9b4Edwin Brady13 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

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

33import System.FilePath

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

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

36type IdrisParser = StateT IState IdrisInnerParser

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

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

41instance TokenParsing IdrisInnerParser where

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

44−-- | Generalized monadic parsing constraint type

44+-- | Generalized monadic parsing constraint type

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

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

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

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

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

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

54simpleWhiteSpace :: MonadicParsing m => m ()

55simpleWhiteSpace = satisfy isSpace *> pure ()

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

69isDocCommentMarker _ = False

71{- | Consumes a single-line comment

72+

73+@

72 SingleLineComment_t ::= '--' EOL_t

74 SingleLineComment_t ::= '--' EOL_t

73 | '--' ~DocCommentMarker_t ~EOL_t* EOL_t

75 | '--' ~DocCommentMarker_t ~EOL_t* EOL_t

74 ;

76 ;

77+@

75 -}

78 -}

76singleLineComment :: MonadicParsing m => m ()

79singleLineComment :: MonadicParsing m => m ()

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

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

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

79 <?> ""

82 <?> ""

81{- | Consumes a multi-line comment

84{- | Consumes a multi-line comment

85+

86+@

82 MultiLineComment_t ::=

87 MultiLineComment_t ::=

83 '{ -- }'

88 '{ -- }'

84 | '{ -' ~DocCommentMarker_t InCommentChars_t

89 | '{ -' ~DocCommentMarker_t InCommentChars_t

85 ;

90 ;

91+@

93+@

87 InCommentChars_t ::=

94 InCommentChars_t ::=

88 '- }'

95 '- }'

89 | MultiLineComment_t InCommentChars_t

96 | MultiLineComment_t InCommentChars_t

90 | ~'- }'+ InCommentChars_t

97 | ~'- }'+ InCommentChars_t

91 ;

98 ;

99+@

92− -}

100+-}

93−

94multiLineComment :: MonadicParsing m => m ()

101multiLineComment :: MonadicParsing m => m ()

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

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

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

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

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

107 startEnd = "{}-"

114 startEnd = "{}-"

108

115

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

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

117+

118+@

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

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

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

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

112 ;

121 ;

122+@

113 -}

123 -}

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

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

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

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

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

139integer :: MonadicParsing m => m Integer

149integer :: MonadicParsing m => m Integer

140integer = Tok.integer

150integer = Tok.integer

141

151

142−-- | Parses a floating point number

152+-- | Parses a floating point number

143float :: MonadicParsing m => m Double

153float :: MonadicParsing m => m Double

144float = Tok.double

154float = Tok.double

145

155

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

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

147

157

148

158

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

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

150idrisStyle :: MonadicParsing m => IdentifierStyle m

160idrisStyle :: MonadicParsing m => IdentifierStyle m

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

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

152 where _styleName = "Idris"

162 where _styleName = "Idris"

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

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

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

221 unalias aliases name = name

231 unalias aliases name = name

222

232

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

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

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

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

225− condition.

235+condition.

226-}

236-}

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

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

228initsEndAt p [] = []

238initsEndAt p [] = []

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

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

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

232

242

233

243

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

235 namespace.

245 namespace.

236-}

246-}

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

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

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

309 (x : xs) -> return x

319 (x : xs) -> return x

310 _ -> return 1

320 _ -> return 1

311

321

312−-- | Applies parser in an indented position

322+-- | Applies parser in an indented position

313indented :: IdrisParser a -> IdrisParser a

323indented :: IdrisParser a -> IdrisParser a

314indented p = notEndBlock *> p <* keepTerminator

324indented p = notEndBlock *> p <* keepTerminator

315

325

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

331 closeBlock

341 closeBlock

332 return res

342 return res

333

343

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

335indentedBlockS :: IdrisParser a -> IdrisParser a

345indentedBlockS :: IdrisParser a -> IdrisParser a

336indentedBlockS p = do openBlock

346indentedBlockS p = do openBlock

337 pushIndent

347 pushIndent

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

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

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

458 <?> "accessibility modifier"

468 <?> "accessibility modifier"

459

469

460−-- | Adds accessibility option for function

470+-- | Adds accessibility option for function

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

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

462addAcc n a = do i <- get

472addAcc n a = do i <- get

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

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

src/Idris/Parser.hs+152−24

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

65import System.IO

67{-

68+@

68 grammar shortcut notation:

69 grammar shortcut notation:

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

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

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

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

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

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

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

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

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

74 RULE{n} = rule repeated n times

75 RULE{n} = rule repeated n times

76+@

75-}

77-}

77{- * Main grammar -}

79{- * Main grammar -}

79{- | Parses module definition

81{- | Parses module definition

82+

83+@

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

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

85+@

81-}

86-}

82moduleHeader :: IdrisParser [String]

87moduleHeader :: IdrisParser [String]

83moduleHeader = try (do reserved "module"

88moduleHeader = try (do reserved "module"

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

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

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

94{- | Parses an import statement

99{- | Parses an import statement

100+

101+@

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

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

103+@

96 -}

104 -}

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

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

98import_ = do fc <- getFC

106import_ = do fc <- getFC

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

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

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

106

114

107{- | Parses program source

115{- | Parses program source

116+

117+@

108 Prog ::= Decl* EOF;

118 Prog ::= Decl* EOF;

119+@

109 -}

120 -}

110prog :: SyntaxInfo -> IdrisParser [PDecl]

121prog :: SyntaxInfo -> IdrisParser [PDecl]

111prog syn = do whiteSpace

122prog syn = do whiteSpace

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

115 let c = (concat decls)

126 let c = (concat decls)

116 return c

127 return c

117

128

118−{- | Parses a top-level declaration

129+{-| Parses a top-level declaration

130+

131+@

119Decl ::=

132Decl ::=

120 Decl'

133 Decl'

121 | Using

134 | Using

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

130 | Transform

143 | Transform

131 | Import!

144 | Import!

132 ;

145 ;

146+@

133-}

147-}

134decl :: SyntaxInfo -> IdrisParser [PDecl]

148decl :: SyntaxInfo -> IdrisParser [PDecl]

135decl syn = do notEndBlock

149decl syn = do notEndBlock

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

155 return [d']

169 return [d']

156

170

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

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

172+

173+@

158Decl' ::=

174Decl' ::=

159 Fixity

175 Fixity

160 | FunDecl'

176 | FunDecl'

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

162 | Record

178 | Record

163 | SyntaxDecl

179 | SyntaxDecl

164 ;

180 ;

181+@

165-}

182-}

166decl' :: SyntaxInfo -> IdrisParser PDecl

183decl' :: SyntaxInfo -> IdrisParser PDecl

167decl' syn = fixity

184decl' syn = fixity

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

172 <?> "declaration"

189 <?> "declaration"

173

190

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

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

192+

193+@

175 SyntaxDecl ::= SyntaxRule;

194 SyntaxDecl ::= SyntaxRule;

195+@

176-}

196-}

177syntaxDecl :: SyntaxInfo -> IdrisParser PDecl

197syntaxDecl :: SyntaxInfo -> IdrisParser PDecl

178syntaxDecl syn = do s <- syntaxRule syn

198syntaxDecl syn = do s <- syntaxRule syn

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

190 ename (Keyword n) = Just n

210 ename (Keyword n) = Just n

191 ename _ = Nothing

211 ename _ = Nothing

192

212

193−{- | Parses a syntax extension declaration

213+{- | Parses a syntax extension declaration

214+

215+@

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

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

217+@

195

218

219+@

196SyntaxRule ::=

220SyntaxRule ::=

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

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

222+@

198

223

224+@

199SyntaxSym ::= '[' Name_t ']'

225SyntaxSym ::= '[' Name_t ']'

200 | '{' Name_t '}'

226 | '{' Name_t '}'

201 | Name_t

227 | Name_t

202 | StringLiteral_t

228 | StringLiteral_t

203 ;

229 ;

230+@

204-}

231-}

205syntaxRule :: SyntaxInfo -> IdrisParser Syntax

232syntaxRule :: SyntaxInfo -> IdrisParser Syntax

206syntaxRule syn

233syntaxRule syn

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

236

263

237

264

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

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

266+

267+@

239SyntaxSym ::= '[' Name_t ']'

268SyntaxSym ::= '[' Name_t ']'

240 | '{' Name_t '}'

269 | '{' Name_t '}'

241 | Name_t

270 | Name_t

242 | StringLiteral_t

271 | StringLiteral_t

243 ;

272 ;

273+@

244 -}

274 -}

245syntaxSym :: IdrisParser SSymbol

275syntaxSym :: IdrisParser SSymbol

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

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

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

254 <?> "syntax symbol"

284 <?> "syntax symbol"

255

285

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

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

287+

288+@

257 FunDecl ::= FunDecl';

289 FunDecl ::= FunDecl';

290+@

258-}

291-}

259fnDecl :: SyntaxInfo -> IdrisParser [PDecl]

292fnDecl :: SyntaxInfo -> IdrisParser [PDecl]

260fnDecl syn = try (do notEndBlock

293fnDecl syn = try (do notEndBlock

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

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

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

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

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

265

298

266−{- Parses a function declaration

299+{-| Parses a function declaration

300+

301+@

267 FunDecl' ::=

302 FunDecl' ::=

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

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

269 | Postulate

304 | Postulate

270 | Pattern

305 | Pattern

271 | CAF

306 | CAF

272 ;

307 ;

308+@

273-}

309-}

274fnDecl' :: SyntaxInfo -> IdrisParser PDecl

310fnDecl' :: SyntaxInfo -> IdrisParser PDecl

275fnDecl' syn = checkFixity $

311fnDecl' syn = checkFixity $

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

313 | otherwise = return True

349 | otherwise = return True

314 fixityOK _ = return True

350 fixityOK _ = return True

315

351

316−{- Parses function options given initial options

352+{-| Parses function options given initial options

353+

354+@

317FnOpts ::= 'total'

355FnOpts ::= 'total'

318 | 'partial'

356 | 'partial'

319 | 'implicit'

357 | 'implicit'

320 | '%' 'assert_total'

358 | '%' 'assert_total'

321 | '%' 'error_handler'

359 | '%' 'error_handler'

322− | '%' 'reflection'

360+ | '%' 'reflection'

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

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

324 ;

362 ;

363+@

325

364

365+@

326NameTimes ::= FnName Natural?;

366NameTimes ::= FnName Natural?;

367+@

327

368

369+@

328NameTimesList ::=

370NameTimesList ::=

329 NameTimes

371 NameTimes

330 | NameTimes ',' NameTimesList

372 | NameTimes ',' NameTimesList

331 ;

373 ;

332−

374+@

333-}

375-}

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

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

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

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

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

360

402

361{- | Parses a postulate

403{- | Parses a postulate

362

404

405+@

363Postulate ::=

406Postulate ::=

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

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

365 ;

408 ;

409+@

366-}

410-}

367postulate :: SyntaxInfo -> IdrisParser PDecl

411postulate :: SyntaxInfo -> IdrisParser PDecl

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

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

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

388

432

389{- | Parses a using declaration

433{- | Parses a using declaration

390

434

435+@

391Using ::=

436Using ::=

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

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

393 ;

438 ;

439+@

394 -}

440 -}

395using_ :: SyntaxInfo -> IdrisParser [PDecl]

441using_ :: SyntaxInfo -> IdrisParser [PDecl]

396using_ syn =

442using_ syn =

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

402 return (concat ds)

448 return (concat ds)

403 <?> "using declaration"

449 <?> "using declaration"

404

450

405−{- | Parses a parameters declaration

451+{- | Parses a parameters declaration

406

452

453+@

407Params ::=

454Params ::=

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

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

409 ;

456 ;

457+@

410 -}

458 -}

411params :: SyntaxInfo -> IdrisParser [PDecl]

459params :: SyntaxInfo -> IdrisParser [PDecl]

412params syn =

460params syn =

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

421

469

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

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

423

471

472+@

424Mutual ::=

473Mutual ::=

425 'mutual' OpenBlock Decl* CloseBlock

474 'mutual' OpenBlock Decl* CloseBlock

426 ;

475 ;

476+@

427-}

477-}

428mutual :: SyntaxInfo -> IdrisParser [PDecl]

478mutual :: SyntaxInfo -> IdrisParser [PDecl]

429mutual syn =

479mutual syn =

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

436 return [PMutual fc (concat ds)]

486 return [PMutual fc (concat ds)]

437 <?> "mutual block"

487 <?> "mutual block"

438

488

439−{- | Parses a namespace declaration

489+{-| Parses a namespace declaration

440

490

491+@

441Namespace ::=

492Namespace ::=

442 'namespace' identifier OpenBlock Decl+ CloseBlock

493 'namespace' identifier OpenBlock Decl+ CloseBlock

443 ;

494 ;

495+@

444-}

496-}

445namespace :: SyntaxInfo -> IdrisParser [PDecl]

497namespace :: SyntaxInfo -> IdrisParser [PDecl]

446namespace syn =

498namespace syn =

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

451 return [PNamespace n (concat ds)]

503 return [PNamespace n (concat ds)]

452 <?> "namespace declaration"

504 <?> "namespace declaration"

453

505

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

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

507+

508+@

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

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

510+@

456− -}

511+-}

457instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]

512instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]

458instanceBlock syn = do reserved "where"

513instanceBlock syn = do reserved "where"

459 openBlock

514 openBlock

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

462 return (concat ds)

517 return (concat ds)

463 <?> "instance block"

518 <?> "instance block"

464

519

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

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

466

521

522+@

467MethodOrInstance ::=

523MethodOrInstance ::=

468 FnDecl

524 FnDecl

469 | Instance

525 | Instance

470 ;

526 ;

527+@

471

528

529+@

472ClassBlock ::=

530ClassBlock ::=

473 'where' OpenBlock MethodOrInstance* CloseBlock

531 'where' OpenBlock MethodOrInstance* CloseBlock

474 ;

532 ;

533+@

475-}

534-}

476classBlock :: SyntaxInfo -> IdrisParser [PDecl]

535classBlock :: SyntaxInfo -> IdrisParser [PDecl]

477classBlock syn = do reserved "where"

536classBlock syn = do reserved "where"

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

481 return (concat ds)

540 return (concat ds)

482 <?> "class block"

541 <?> "class block"

483

542

484−{- |Parses a type class declaration

543+{-| Parses a type class declaration

485

544

545+@

486ClassArgument ::=

546ClassArgument ::=

487 Name

547 Name

488 | '(' Name ':' Expr ')'

548 | '(' Name ':' Expr ')'

489 ;

549 ;

550+@

490

551

552+@

491Class ::=

553Class ::=

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

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

493 ;

555 ;

556+@

494-}

557-}

495class_ :: SyntaxInfo -> IdrisParser [PDecl]

558class_ :: SyntaxInfo -> IdrisParser [PDecl]

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

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

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

511 <|> do i <- name;

574 <|> do i <- name;

512 return (i, PType)

575 return (i, PType)

513

576

514−{- |Parses a type class instance declaration

577+{- | Parses a type class instance declaration

515

578

579+@

516 Instance ::=

580 Instance ::=

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

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

518 ;

582 ;

583+@

519

584

585+@

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

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

587+@

521-}

588-}

522instance_ :: SyntaxInfo -> IdrisParser [PDecl]

589instance_ :: SyntaxInfo -> IdrisParser [PDecl]

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

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

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

538

605

539

606

540{- | Parses a using declaration list

607{- | Parses a using declaration list

608+

609+@

541UsingDeclList ::=

610UsingDeclList ::=

542 UsingDeclList'

611 UsingDeclList'

543 | NameList TypeSig

612 | NameList TypeSig

544 ;

613 ;

614+@

545

615

616+@

546UsingDeclList' ::=

617UsingDeclList' ::=

547 UsingDecl

618 UsingDecl

548 | UsingDecl ',' UsingDeclList'

619 | UsingDecl ',' UsingDeclList'

549 ;

620 ;

621+@

550

622

623+@

551NameList ::=

624NameList ::=

552 Name

625 Name

553 | Name ',' NameList

626 | Name ',' NameList

554 ;

627 ;

628+@

555-}

629-}

556usingDeclList :: SyntaxInfo -> IdrisParser [Using]

630usingDeclList :: SyntaxInfo -> IdrisParser [Using]

557usingDeclList syn

631usingDeclList syn

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

563 <?> "using declaration list"

637 <?> "using declaration list"

564

638

565{- |Parses a using declaration

639{- |Parses a using declaration

640+

641+@

566UsingDecl ::=

642UsingDecl ::=

567 FnName TypeSig

643 FnName TypeSig

568 | FnName FnName+

644 | FnName FnName+

569 ;

645 ;

646+@

570-}

647-}

571usingDecl :: SyntaxInfo -> IdrisParser Using

648usingDecl :: SyntaxInfo -> IdrisParser Using

572usingDecl syn = try (do x <- fnName

649usingDecl syn = try (do x <- fnName

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

578 return (UConstraint c xs)

655 return (UConstraint c xs)

579 <?> "using declaration"

656 <?> "using declaration"

580

657

581−{- | Parse a clause with patterns

658+{- | Parse a clause with patterns

659+

660+@

582Pattern ::= Clause;

661Pattern ::= Clause;

662+@

583-}

663-}

584pattern :: SyntaxInfo -> IdrisParser PDecl

664pattern :: SyntaxInfo -> IdrisParser PDecl

585pattern syn = do fc <- getFC

665pattern syn = do fc <- getFC

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

588 <?> "pattern"

668 <?> "pattern"

589

669

590{- | Parse a constant applicative form declaration

670{- | Parse a constant applicative form declaration

671+

672+@

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

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

674+@

592-}

675-}

593caf :: SyntaxInfo -> IdrisParser PDecl

676caf :: SyntaxInfo -> IdrisParser PDecl

594caf syn = do reserved "let"

677caf syn = do reserved "let"

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

601 <?> "constant applicative form declaration"

684 <?> "constant applicative form declaration"

602

685

603{- | Parse an argument expression

686{- | Parse an argument expression

687+

688+@

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

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

690+@

605-}

691-}

606argExpr :: SyntaxInfo -> IdrisParser PTerm

692argExpr :: SyntaxInfo -> IdrisParser PTerm

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

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

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

609 <?> "argument expression"

695 <?> "argument expression"

610

696

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

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

698+

699+@

612RHS ::= '=' Expr

700RHS ::= '=' Expr

613 | '?=' RHSName? Expr

701 | '?=' RHSName? Expr

614 | 'impossible'

702 | 'impossible'

615 ;

703 ;

704+@

616

705

706+@

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

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

708+@

618-}

709-}

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

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

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

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

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

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

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

638

729

639{- |Parses a function clause

730{- |Parses a function clause

731+

732+@

640RHSOrWithBlock ::= RHS WhereOrTerminator

733RHSOrWithBlock ::= RHS WhereOrTerminator

641 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock

734 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock

642 ;

735 ;

736+@

737+

738+@

643Clause ::= WExpr+ RHSOrWithBlock

739Clause ::= WExpr+ RHSOrWithBlock

644 | SimpleExpr '<==' FnName RHS WhereOrTerminator

740 | SimpleExpr '<==' FnName RHS WhereOrTerminator

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

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

646 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock

742 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock

647 ;

743 ;

744+@

745+

746+@

648ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;

747ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;

748+@

749+

750+@

649−WhereOrTerminator ::= WhereBlock | Terminator;

751+WhereOrTerminator ::= WhereBlock | Terminator;

752+@

650-}

753-}

651clause :: SyntaxInfo -> IdrisParser PClause

754clause :: SyntaxInfo -> IdrisParser PClause

652clause syn

755clause syn

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

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

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

776 fillLHSD n c a x = x

879 fillLHSD n c a x = x

777

880

778−{- |Parses with pattern

881+{-| Parses with pattern

882+

883+@

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

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

885+@

780-}

886-}

781wExpr :: SyntaxInfo -> IdrisParser PTerm

887wExpr :: SyntaxInfo -> IdrisParser PTerm

782wExpr syn = do lchar '|'

888wExpr syn = do lchar '|'

783 expr' syn

889 expr' syn

784 <?> "with pattern"

890 <?> "with pattern"

785

891

786−{- |Parses a where block

892+{- | Parses a where block

893+

894+@

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

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

896+@

788− -}

897+-}

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

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

790whereBlock n syn

899whereBlock n syn

791 = do reserved "where"

900 = do reserved "where"

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

795 <?> "where block"

904 <?> "where block"

796

905

797{- |Parses a code generation target language name

906{- |Parses a code generation target language name

907+

908+@

798Codegen ::= 'C'

909Codegen ::= 'C'

799 | 'Java'

910 | 'Java'

800 | 'JavaScript'

911 | 'JavaScript'

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

802 | 'LLVM'

913 | 'LLVM'

803 | 'Bytecode'

914 | 'Bytecode'

804 ;

915 ;

916+@

805-}

917-}

806codegen_ :: IdrisParser Codegen

918codegen_ :: IdrisParser Codegen

807codegen_ = do reserved "C"; return ViaC

919codegen_ = do reserved "C"; return ViaC

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

813 <?> "code generation language"

925 <?> "code generation language"

814

926

815{- |Parses a compiler directive

927{- |Parses a compiler directive

928+@

816StringList ::=

929StringList ::=

817 String

930 String

818 | String ',' StringList

931 | String ',' StringList

819 ;

932 ;

933+@

820

934

935+@

821Directive ::= '%' Directive';

936Directive ::= '%' Directive';

937+@

822

938

939+@

823Directive' ::= 'lib' CodeGen String_t

940Directive' ::= 'lib' CodeGen String_t

824 | 'link' CodeGen String_t

941 | 'link' CodeGen String_t

825 | 'flag' CodeGen String_t

942 | 'flag' CodeGen String_t

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

834 | 'language' 'TypeProviders'

951 | 'language' 'TypeProviders'

835 | 'language' 'ErrorReflection'

952 | 'language' 'ErrorReflection'

836 ;

953 ;

954+@

837-}

955-}

838directive :: SyntaxInfo -> IdrisParser [PDecl]

956directive :: SyntaxInfo -> IdrisParser [PDecl]

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

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

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

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

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

894

1012

895{- | Parses a totality

1013{- | Parses a totality

1014+

1015+@

896Totality ::= 'partial' | 'total'

1016Totality ::= 'partial' | 'total'

1017+@

1018+

897-}

1019-}

898totality :: IdrisParser Bool

1020totality :: IdrisParser Bool

899totality

1021totality

900 = do reserved "total"; return True

1022 = do reserved "total"; return True

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

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

902

1024

903−{- | Parses a type provider

1025+{- | Parses a type provider

1026+

1027+@

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

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

1029+@

905 -}

1030 -}

906provider :: SyntaxInfo -> IdrisParser [PDecl]

1031provider :: SyntaxInfo -> IdrisParser [PDecl]

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

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

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

913 <?> "type provider"

1038 <?> "type provider"

914

1039

915{- | Parses a transform

1040{- | Parses a transform

1041+

1042+@

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

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

1044+@

917-}

1045-}

918transform :: SyntaxInfo -> IdrisParser [PDecl]

1046transform :: SyntaxInfo -> IdrisParser [PDecl]

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

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