58bfb08 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Initial transfer of {AS} grammar to Sphinx Documtation.

58bfb08Jan de Muijnck-Hughes8 years ago

docs/reference/index.rst+1

compare with master

unifiedsplit

@@ -26,6 +26,7 @@ This will tell you how Idris works, for using it you should read the Idris Tutor

26 uniqueness-types

27 ffi

28 syntax-guide

29+ syntax-reference

29 erasure

30 erasure

30 ide-protocol

31 ide-protocol

31 semantic-highlighting

32 semantic-highlighting

docs/reference/syntax-reference.rstnew file+422

@@ -0,0 +1,422 @@

1+*****************

2+Syntax Reference

3+*****************

5+Here we present a rough description of Idris' surface syntax as an eBNF grammar.

6+This presentend grammar may differ from syntax that Idris' parser can handle due to the parser and grammar description not being in sync.

8+=========

9+Notation

10+=========

11+

12+Grammar shortcut notation::

13+

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

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

16+ RULE* = repeated rule (i.e. RULE zero or more times)

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

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

19+ RULE{n} = rule repeated n times

20+

21+

22+=============

23+Main Grammar

24+=============

25+

26+.. productionlist::

27+ ModuleHeader : `DocComment_t`? "module" `Identifier_t` ";"? ;

28+ Import : "import" `Identifier_t` ";"? ;

29+ Prog : `Decl`* `EOF`;

30+ Decl : `DeclP`

31+ : | `Using`

32+ : | `Params`

33+ : | `Mutual`

34+ : | `Namespace`

35+ : | `Interface`

36+ : | `Implementation`

37+ : | `DSL`

38+ : | `Directive`

39+ : | `Provider`

40+ : | `Transform`

41+ : | `Import`!

42+ : | `RunElabDecl` ;

43+ DeclP : `Fixity`

44+ : | `FunDecl`

45+ : | `Data`

46+ : | `Record`

47+ : | `SyntaxDecl` ;

48+

49+

50+--------------------

51+Syntax Declarations

52+--------------------

53+

54+.. productionlist::

55+ SyntaxDecl : `SyntaxRule` ;

56+ SyntaxRuleOpts : "term" | "pattern" ;

57+ SyntaxRule : `SyntaxRuleOpts`? "syntax" `SyntaxSym`+ "=" `TypeExpr` `Terminator`;

58+ SyntaxSym : '[' `Name_t` ']'

59+ : | '{' `Name_t` '}'

60+ : | `Name_t`

61+ : | `StringLiteral_t`;

62+ SyntaxSym : '[' `Name_t` ']'

63+ : | '{' `Name_t` '}'

64+ : | `Name_t`

65+ : | `StringLiteral_t`;

66+

67+----------

68+Functions

69+----------

70+

71+.. productionlist::

72+ FunDecl : `FunDeclP`;

73+ FunDeclP : `DocComment_t`? `FnOpts`* `Accessibility`? `FnOpts`* `FnName` `TypeSig` `Terminator`

74+ : | `Postulate`

75+ : | `Pattern`

76+ : | `CAF` ;

77+ FnOpts : `FnOpt`* `Accessibility` `FnOpt`* ;

78+ FnOpt : 'total'

79+ : | 'partial'

80+ : | 'covering'

81+ : | 'implicit'

82+ : | '%' 'no_implicit'

83+ : | '%' 'assert_total'

84+ : | '%' 'error_handler'

85+ : | '%' 'reflection'

86+ : | '%' 'specialise' '[' `NameTimesList`? ']' ;

87+ NameTimes : `FnName` `Natural`?;

88+ NameTimesList : `NameTimes` | `NameTimes` ',' `NameTimesList` ;

89+ Postulate : `DocComment_t`? 'postulate' `FnOpts`* `Accesibility`? `FnOpts`* `FnName` `TypeSig` `Terminator` ;

90+

91+--------------------

92+Blocks & Namespaces

93+--------------------

94+

95+.. productionlist::

96+ Using : 'using' '(' `UsingDeclList` ')' `OpenBlock` `Decl`* `CloseBlock` ;

97+ UsingDeclList : `UsingDeclListP` | `NameList TypeSig`;

98+ UsingDeclListP : `UsingDecl` | `UsingDecl` ',' `UsingDeclListP` ;

99+ NameList : `Name` | `Name` ',' `NameList` ;

100+ UsingDecl : `FnName` `TypeSig` | `FnName` `FnName`+ ;

101+ Params : 'parameters' '(' `TypeDeclList` ')' `OpenBlock` `Decl`* `CloseBlock`;

102+ Mutual : 'mutual' `OpenBlock` `Decl`* `CloseBlock` ;

103+ Namespace : 'namespace' `identifier` `OpenBlock` `Decl`+ `CloseBlock` ;

104+

105+----------------------------

106+Interfaces & Implementation

107+----------------------------

108+

109+.. productionlist::

110+ ImplementationBlock : 'where' `OpenBlock` `FnDecl`* `CloseBlock` ;

111+ MethodOrImplementation : `FnDecl` | `Implementation`;

112+ InterfaceBlock : 'where' `OpenBlock` `Constructor`? `MethodOrImplementation`* `CloseBlock` ;

113+ InterfaceArgument : `Name` | '(' `Name` ':' `Expr` ')';

114+ Interface ::= `DocComment_t`? `Accessibility`? 'interface' `ConstraintList`? `Name` `InterfaceArgument`* `InterfaceBlock`?;

115+ Implementation : `DocComment_t`? 'implementation' `ImplementationName`? `ConstraintList`? `Name` `SimpleExpr`* `ImplementationBlock`? ;

116+ ImplementationName : '[' `Name` ']';

117+

118+

119+-------

120+Bodies

121+-------

122+

123+.. productionlist::

124+ Pattern : `Clause`;

125+ CAF : 'let' `FnName` '=' `Expr` `Terminator`;

126+ ArgExpr : `HSimpleExpr` | "In Pattern External (User-defined) Expression";

127+ RHS : '=' `Expr`

128+ : | '?=' `RHSName`? `Expr`

129+ : | `Impossible` ;

130+ RHSName : '{' `FnName` '}' ;

131+ RHSOrWithBlock : `RHS` `WhereOrTerminator`

132+ : | 'with' `SimpleExpr` `OpenBlock` `FnDecl`+ `CloseBlock`;

133+ Clause : `WExpr`+ `RHSOrWithBlock`

134+ : | `SimpleExpr` '<==' `FnName` `RHS` `WhereOrTerminator`

135+ : | `ArgExpr` `Operator` `ArgExpr` `WExpr`* `RHSOrWithBlock` {- Except "=" and "?=" operators to avoid ambiguity -}

136+ : | `FnName` `ConstraintArg`* `ImplicitOrArgExpr`* `WExpr`* `RHSOrWithBlock`;

137+ ImplicitOrArgExpr ::= `ImplicitArg` | `ArgExpr`;

138+ WhereOrTerminator ::= `WhereBlock` | `Terminator`;

139+ WExpr ::= '|' `Expr`';

140+ WhereBlock : 'where' `OpenBlock` `Decl`+ `CloseBlock`;

141+

142+----------

143+Directives

144+----------

145+

146+.. productionlist::

147+ Codegen: 'C'

148+ : | 'Java'

149+ : | 'JavaScript'

150+ : | 'Node'

151+ : | 'LLVM'

152+ : | 'Bytecode' ;

153+ StringList : `String` | `String` ',' `StringList` ;

154+ Directive : '%' `DirectiveP`;

155+ DirectiveP : 'lib' `CodeGen` `String_t`

156+ : | 'link' `CodeGen` `String_t`

157+ : | 'flag' `CodeGen` `String_t`

158+ : | 'include' `CodeGen` `String_t`

159+ : | 'hide' `Name`

160+ : | 'freeze' `Name`

161+ : | 'thaw' `Name`

162+ : | 'access' `Accessibility`

163+ : | 'default' `Totality`

164+ : | 'logging' `Natural`

165+ : | 'dynamic' `StringList`

166+ : | 'name' `Name` `NameList`

167+ : | 'error_handlers' `Name` `NameList`

168+ : | 'language' 'TypeProviders'

169+ : | 'language' 'ErrorReflection'

170+ : | 'deprecated' `Name` `String`

171+ : | 'fragile' `Name` `Reason` ;

172+ LangExt : "TypeProviders"

173+ : | "ErrorReflection"

174+ : | "UniquenessTypes"

175+ : | "LinearTypes"

176+ : | "DSLNotation"

177+ : | "ElabReflection"

178+ : | "FirstClassReflection" ;

179+ Totality : 'partial' | 'total' | 'covering'

180+ Provider : `DocComment_t`? '%' 'provide' `Provider_What`? '(' `FnName` `TypeSig` ')' 'with' `Expr`;

181+ ProviderWhat : 'proof' | 'term' | 'type' | 'postulate'

182+ Transform : '%' 'transform' `Expr` '==>' `Expr`;

183+ RunElabDecl : '%' 'runElab' `Expr`;

184+

185+

186+===========

187+Expressions

188+===========

189+

190+.. productionlist::

191+ FullExpr : `Expr` `EOF_t` ;

192+ Expr : `Pi` ;

193+ OpExpr : "Expression Parser with Operators based on ExprP" ;

194+ ExprP : "External (User-defined) Syntax" | `InternalExpr` ;

195+ InternalExpr : `UnifyLog`

196+ : | `RecordType`

197+ : | `SimpleExpr`

198+ : | `Lambda`

199+ : | `QuoteGoal`

200+ : | `Let`

201+ : | `If`

202+ : | `RewriteTerm`

203+ : | `CaseExpr`

204+ : | `DoBlock`

205+ : | `App` ;

206+

207+-------

208+Bodies

209+-------

210+

211+.. productionlist::

212+ Impossible : `impossible` ;

213+ CaseExpr : "case" `Expr` "of" `OpenBlock` `CaseOption`+ `CloseBlock` ;

214+ CaseOption : `Expr` (`Impossible` | "=>" `Expr`) `Terminator` ;

215+ ProofExpr : "proof" `OpenBlock` `Tactic'`* `CloseBlock` ;

216+ TacticsExpr : "tactics" `OpenBlock` `Tactic'`* `CloseBlock` ;

217+ SimpleExpr : "External (User-defined) Simple Expression"

218+ : | "?" `Name`

219+ : | "%" "implementation"

220+ : | "Refl" ("{" `Expr` "}")?

221+ : | `ProofExpr`

222+ : | `TacticsExpr`

223+ : | `FnName`

224+ : | `Idiom`

225+ : | `List`

226+ : | `Alt`

227+ : | `Bracketed`

228+ : | `Constant`

229+ : | `Type`

230+ : | "Void"

231+ : | `Quasiquote`

232+ : | `NameQuote`

233+ : | `Unquote`

234+ : | "_" ;

235+ Bracketed : "(" `BracketedP` ;

236+ BracketedP : ")"

237+ : | `Expr` ")"

238+ : | `ExprList` ")"

239+ : | `DependentPair` ")"

240+ : | `Operator` `Expr` ")"

241+ : | `Expr` `Operator` ")" ;

242+ Alt : "(|" `Expr_List` "|)" ;

243+ Expr_List : `Expr'` | `Expr'` "," `Expr_List` ;

244+ HSimpleExpr : "." `SimpleExpr` | `SimpleExpr` ;

245+ UnifyLog : "%" "unifyLog" `SimpleExpr` ;

246+ RunTactics : "%" "runElab" `SimpleExpr` ;

247+ Disamb : "with" `NameList` `Expr` ;

248+ NoImplicits : "%" "noImplicits" `SimpleExpr` ;

249+ App : "mkForeign" `Arg` `Arg`*

250+ : | `MatchApp`

251+ : | `SimpleExpr` `Arg`* ;

252+ MatchApp : `SimpleExpr` "<==" `FnName` ;

253+ Arg :` ImplicitArg` | `ConstraintArg` | `SimpleExpr` ;

254+ ImplicitArg : "{" `Name` ("=" `Expr`)? "}" ;

255+ ConstraintArg : "@{" `Expr` "}" ;

256+ Quasiquote : "`(" `Expr` ")" ;

257+ Unquote : "," `Expr` ;

258+ RecordType : "record" "{" `FieldTypeList` "}" ;

259+ FieldTypeList : `FieldType` | `FieldType` "," `FieldTypeList` ;

260+ FieldType : `FnName` "=" `Expr` ;

261+ TypeSig : ":" `Expr` ;

262+ TypeExpr : `ConstraintList`? `Expr` ;

263+ Lambda : "\\" `TypeOptDeclList` `LambdaTail`

264+ : | "\\" `SimpleExprList` `LambdaTail` ;

265+ SimpleExprList : `SimpleExpr` | `SimpleExpr` "," `SimpleExprList` ;

266+ LambdaTail : `Impossible` | "=>" `Expr` ;

267+ RewriteTerm : "rewrite" `Expr` ("==>" `Expr`)? "in" `Expr` ;

268+ RigCount: "1" : "0" ;

269+ Let : "let" `Name` `TypeSig`"? "=" `Expr` "in" `Expr`

270+ : | "let" `Expr'` "=" `Expr'` "in" `Expr` ;

271+ TypeSig' : ":" `Expr'` ;

272+ If : "if" `Expr` "then" `Expr` "else" `Expr` ;

273+ QuoteGoal : "quoteGoal" `Name` "by" `Expr` "in" `Expr` ;

274+

275+----

276+Pies

277+----

278+

279+.. productionlist::

280+ Pi : `PiOpts` `Static`? `PiP` ;

281+ PiP : `OpExpr` ("->" `Pi`)?

282+ : | "(" `TypeDeclList` ")" "->" `Pi`

283+ : | "{" `TypeDeclList` "}" "->" `Pi`

284+ : | "{" "auto" `TypeDeclList` "}" "->" `Pi`

285+ : | "{" "default" `SimpleExpr` `TypeDeclList` "}" "->" `Pi` ;

286+ PiOpts : "."? ;

287+ ConstraintList : "(" `Expr_List` ")" "=>"

288+ : | `Expr` "=>" ;

289+ TypeDeclList : `FunctionSignatureList`

290+ : | `NameList` `TypeSig` ;

291+ FunctionSignatureList : `Name` `TypeSig`

292+ : | `Name` `TypeSig` "," `FunctionSignatureList` ;

293+ TypeOptDeclList : `NameOrPlaceholder` `TypeSig`?

294+ : | `NameOrPlaceholder` `TypeSig`? "," `TypeOptDeclList` ;

295+ NameOrPlaceHolder : `Name` : "_" ;

296+ ListExpr : "[" "]" | "[" `Expr` "|" `DoList` "]" | "[" `ExprList` "]" ;

297+ ExprList : `Expr` | `Expr` "," `ExprList` ;

298+

299+

300+-------------------

301+Do Blocks & Idioms

302+-------------------

303+

304+.. productionlist::

305+ DoList : `Do` : `Do` "," `DoList` ;

306+ Do' : `Do` `KeepTerminator` ;

307+ DoBlock : "do" `OpenBlock` `Do'`+ `CloseBlock` ;

308+ Do : "let" `Name` `TypeSig`"? "=" `Expr`

309+ : | "let" `Expr'` "=" `Expr`

310+ : | "rewrite" `Expr`

311+ : | `Name` "<-" `Expr`

312+ : | `Expr'` "<-" `Expr`

313+ : | `Expr` ;

314+ Idiom : "[|" `Expr` "|]" ;

315+

316+

317+----------

318+Constants

319+----------

320+

321+.. productionlist::

322+ Constant : | "Integer"

323+ : | "Int"

324+ : | "Char"

325+ : | "Double"

326+ : | "String"

327+ : | "Bits8"

328+ : | "Bits16"

329+ : | "Bits32"

330+ : | "Bits64"

331+ : | `Float_t`

332+ : | `Natural_t`

333+ : | `VerbatimString_t`

334+ : | `String_t`

335+ : | `Char_t` ;

336+ VerbatimString_t : "\"\"\"" ~"\"\"\"" "\""* "\"\"\"" ;

337+

338+-------

339+Tactics

340+-------

341+

342+.. productionlist::

343+ Tactic : "intro" `NameList`?

344+ : | "intros"

345+ : | "refine" `Name` `Imp`+

346+ : | "mrefine" `Name`

347+ : | "rewrite" `Expr`

348+ : | "induction" `Expr`

349+ : | "equiv" `Expr`

350+ : | "let" `Name` ":" `Expr'` "=" `Expr`

351+ : | "let" `Name` "=" `Expr`

352+ : | "focus" `Name`

353+ : | "exact" `Expr`

354+ : | "applyTactic" `Expr`

355+ : | "reflect" `Expr`

356+ : | "fill" `Expr`

357+ : | "try" `Tactic` "|" `Tactic`

358+ : | "{" `TacticSeq` "}"

359+ : | "compute"

360+ : | "trivial"

361+ : | "solve"

362+ : | "attack"

363+ : | "state"

364+ : | "term"

365+ : | "undo"

366+ : | "qed"

367+ : | "abandon"

368+ : | ":" "q" ;

369+ TacticSeq : `Tactic` ";" `Tactic` | `Tactic` ";" `TacticSeq` ;

370+

371+----

372+Misc

373+----

374+

375+.. productionlist::

376+ Imp : "?" | "_" ;

377+ Static : "%static" ;

378+

379+=====

380+Data

381+=====

382+

383+.. productionlist::

384+ Record : `DocComment` `Accessibility`? "record" `FnName` `TypeSig` "where" `OpenBlock` `Constructor` `KeepTerminator` `CloseBlock`;

385+ DataI : "data" | "codata";

386+ Data : `DocComment`? `Accessibility`? `DataI` `FnName` `TypeSig` `ExplicitTypeDataRest`?

387+ : `DocComment`? `Accessibility`? `DataI` `FnName` `Name`* `DataRest`? ;

388+ Constructor': `Constructor` `KeepTerminator` ;

389+ ExplicitTypeDataRest : "where" `OpenBlock` `Constructor'`* `CloseBlock`;

390+ DataRest : "=" `SimpleConstructorList` `Terminator` | "where"!;

391+ SimpleConstructorList : `SimpleConstructor` | `SimpleConstructor` "|" `SimpleConstructorList`;

392+ Constructor : `DocComment`? `FnName` `TypeSig`;

393+ SimpleConstructor : `FnName` `SimpleExpr`* `DocComment`?;

394+ DSL : "dsl" `FnName` `OpenBlock` `Overload'`+ `CloseBlock`;

395+ OverloadIdentifier : "let" | `Identifier`;

396+ Overload : `OverloadIdentifier` "=" `Expr`;

397+

398+

399+=========

400+Operators

401+=========

402+

403+.. productionlist::

404+ BacktickOperator: `Name` ;

405+ OperatorName: `SymbolicOperator` : `BacktickOperator` ;

406+ OperatorFront: "(" "=" ")" | (`Identifier_t` ".")? "(" `Operator_t` ")" ;

407+ FnName: `Name` | `OperatorFront`;

408+ Fixity: `FixityType` `Natural_t` `OperatorList` `Terminator`;

409+ FixityType: "infixl" | "infixr" | "infix" | "prefix";

410+

411+

412+==============

413+Documentation

414+==============

415+

416+.. productionlist::

417+ SingleLineComment_t: "--" ~`EOL_t`* `EOL_t` ;

418+ MultiLineComment_t: "{" .. "}" | "{ -" `InCommentChars_t` ;

419+ InCommentChars_t : "- }" | `MultiLineComment_t` `InCommentChars_t` | ~"- }"+ `InCommentChars_t`;

420+ DocComment_t : `DocCommentLine` (`ArgCommentLine` `DocCommentLine`*)* ;

421+ DocCommentLine : "|||" ~`EOL_t`* `EOL_t` ;

422+ ArgCommentLine : "|||" "@" ~`EOL_t`* `EOL_t` ;

src/Idris/Parser/Helpers.hs+4−2

@@ -200,8 +200,10 @@ multiLineComment = P.hidden $ P.try (string "{-" *> string "-}" *> pure ())

200{-| Parses a documentation comment

201

202@

203+ DocComment_t ::= DocCommentLine (ArgCommentLine DocCommentLine*)* ;

204+

203− DocComment_t ::= '|||' ~EOL_t* EOL_t

205+ DocCommentLine ::= '|||' ~EOL_t* EOL_t ;

204− ;

206+ ArgCommentLine ::= '|||' '@' ~EOL_t* EOL_t ;

205@

207@

206 -}

208 -}

207docComment :: IdrisParser (Docstring (), [(Name, Docstring ())])

209docComment :: IdrisParser (Docstring (), [(Name, Docstring ())])