@@ -0,0 +1,422 @@
1+*****************
2+Syntax Reference
3+*****************
4+
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.
7+
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` ;