docs/reference/syntax-reference.rst · Idris-dev

git.iko.soy/Idris-dev

Idris-dev/docs/reference/syntax-reference.rst

422 lines 14 kB history raw

1*****************

2Syntax Reference

3*****************

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

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

8=========

9Notation

10=========

12Grammar shortcut notation::

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

22=============

23Main Grammar

24=============

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` ;

50--------------------

51Syntax Declarations

52--------------------

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`;

67----------

68Functions

69----------

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` ;

91--------------------

92Blocks & Namespaces

93--------------------

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

106Interfaces & 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-------

120Bodies

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

143Directives

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===========

187Expressions

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

208Bodies

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

276Pies

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

301Do 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----------

318Constants

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

339Tactics

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

372Misc

373----

374

375.. productionlist::

376 Imp : "?" | "_" ;

377 Static : "%static" ;

378

379=====

380Data

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=========

400Operators

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==============

413Documentation

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` ;