Syntax Reference
Here we present a rough description of Idris’ surface syntax as an eBNF grammar. This presentend grammar may differ from syntax that Idris’ parser can handle due to the parser and grammar description not being in sync.
Notation
Grammar shortcut notation:
~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)
RULE? = optional rule (i.e. RULE or nothing)
RULE* = repeated rule (i.e. RULE zero or more times)
RULE+ = repeated rule with at least one match (i.e. RULE one or more times)
RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)
RULE{n} = rule repeated n times
Main Grammar
ModuleHeader ::=DocComment_t
? "module"Identifier_t
";"? ; Import ::= "import"Identifier_t
";"? ; Prog ::=Decl
*EOF
; Decl ::=DeclP
|Using
|Params
|Mutual
|Namespace
|Interface
|Implementation
|DSL
|Directive
|Provider
|Transform
|Import
! |RunElabDecl
; DeclP ::=Fixity
|FunDecl
|Data
|Record
|SyntaxDecl
;
Syntax Declarations
SyntaxDecl ::=SyntaxRule
; SyntaxRuleOpts ::= "term" | "pattern" ; SyntaxRule ::=SyntaxRuleOpts
? "syntax"SyntaxSym
+ "="TypeExpr
Terminator
; SyntaxSym ::= '['Name_t
']' | '{'Name_t
'}' |Name_t
|StringLiteral_t
; SyntaxSym ::= '['Name_t
']' | '{'Name_t
'}' |Name_t
|StringLiteral_t
;
Functions
FunDecl ::=FunDeclP
; FunDeclP ::=DocComment_t
?FnOpts
*Accessibility
?FnOpts
*FnName
TypeSig
Terminator
|Postulate
|Pattern
|CAF
; FnOpts ::=FnOpt
*Accessibility
FnOpt
* ; FnOpt ::= 'total' | 'partial' | 'covering' | 'implicit' | '%' 'no_implicit' | '%' 'assert_total' | '%' 'error_handler' | '%' 'reflection' | '%' 'specialise' '['NameTimesList
? ']' ; NameTimes ::=FnName
Natural
?; NameTimesList ::=NameTimes
|NameTimes
','NameTimesList
; Postulate ::=DocComment_t
? 'postulate'FnOpts
*Accesibility
?FnOpts
*FnName
TypeSig
Terminator
;
Blocks & Namespaces
Using ::= 'using' '('UsingDeclList
')'OpenBlock
Decl
*CloseBlock
; UsingDeclList ::=UsingDeclListP
| `NameList TypeSig`; UsingDeclListP ::=UsingDecl
|UsingDecl
','UsingDeclListP
; NameList ::=Name
|Name
','NameList
; UsingDecl ::=FnName
TypeSig
|FnName
FnName
+ ; Params ::= 'parameters' '('TypeDeclList
')'OpenBlock
Decl
*CloseBlock
; Mutual ::= 'mutual'OpenBlock
Decl
*CloseBlock
; Namespace ::= 'namespace'identifier
OpenBlock
Decl
+CloseBlock
;
Interfaces & Implementation
ImplementationBlock ::= 'where'OpenBlock
FnDecl
*CloseBlock
; MethodOrImplementation ::=FnDecl
|Implementation
; InterfaceBlock ::= 'where'OpenBlock
Constructor
?MethodOrImplementation
*CloseBlock
; InterfaceArgument ::=Name
| '('Name
':'Expr
')'; Interface ::= :=DocComment_t
?Accessibility
? 'interface'ConstraintList
?Name
InterfaceArgument
*InterfaceBlock
?; Implementation ::=DocComment_t
? 'implementation'ImplementationName
?ConstraintList
?Name
SimpleExpr
*ImplementationBlock
? ; ImplementationName ::= '['Name
']';
Bodies
Pattern ::=Clause
; CAF ::= 'let'FnName
'='Expr
Terminator
; ArgExpr ::=HSimpleExpr
| "In Pattern External (User-defined) Expression"; RHS ::= '='Expr
| '?='RHSName
?Expr
|Impossible
; RHSName ::= '{'FnName
'}' ; RHSOrWithBlock ::=RHS
WhereOrTerminator
| 'with'SimpleExpr
OpenBlock
FnDecl
+CloseBlock
; Clause ::=WExpr
+RHSOrWithBlock
|SimpleExpr
'<=='FnName
RHS
WhereOrTerminator
|ArgExpr
Operator
ArgExpr
WExpr
*RHSOrWithBlock
{- Except "=" and "?=" operators to avoid ambiguity -} |FnName
ConstraintArg
*ImplicitOrArgExpr
*WExpr
*RHSOrWithBlock
; ImplicitOrArgExpr ::= :=ImplicitArg
|ArgExpr
; WhereOrTerminator ::= :=WhereBlock
|Terminator
; WExpr ::= := '|'Expr
'; WhereBlock ::= 'where'OpenBlock
Decl
+CloseBlock
;
Directives
Codegen ::= 'C' | 'Java' | 'JavaScript' | 'Node' | 'LLVM' | 'Bytecode' ; StringList ::=String
|String
','StringList
; Directive ::= '%'DirectiveP
; DirectiveP ::= 'lib'CodeGen
String_t
| 'link'CodeGen
String_t
| 'flag'CodeGen
String_t
| 'include'CodeGen
String_t
| 'hide'Name
| 'freeze'Name
| 'thaw'Name
| 'access'Accessibility
| 'default'Totality
| 'logging'Natural
| 'dynamic'StringList
| 'name'Name
NameList
| 'error_handlers'Name
NameList
| 'language' 'TypeProviders' | 'language' 'ErrorReflection' | 'deprecated'Name
String
| 'fragile'Name
Reason
; LangExt ::= "TypeProviders" | "ErrorReflection" | "UniquenessTypes" | "LinearTypes" | "DSLNotation" | "ElabReflection" | "FirstClassReflection" ; Totality ::= 'partial' | 'total' | 'covering' Provider ::=DocComment_t
? '%' 'provide'Provider_What
? '('FnName
TypeSig
')' 'with'Expr
; ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate' Transform ::= '%' 'transform'Expr
'==>'Expr
; RunElabDecl ::= '%' 'runElab'Expr
;
Expressions
FullExpr ::=Expr
EOF_t
; Expr ::=Pi
; OpExpr ::= "Expression Parser with Operators based on ExprP" ; ExprP ::= "External (User-defined) Syntax" |InternalExpr
; InternalExpr ::=UnifyLog
|RecordType
|SimpleExpr
|Lambda
|QuoteGoal
|Let
|If
|RewriteTerm
|CaseExpr
|DoBlock
|App
;
Bodies
Impossible ::=impossible
; CaseExpr ::= "case"Expr
"of"OpenBlock
CaseOption
+CloseBlock
; CaseOption ::=Expr
(Impossible
| "=>"Expr
)Terminator
; ProofExpr ::= "proof"OpenBlock
`Tactic'`*CloseBlock
; TacticsExpr ::= "tactics"OpenBlock
`Tactic'`*CloseBlock
; SimpleExpr ::= "External (User-defined) Simple Expression" | "?"Name
| "%" "implementation" | "Refl" ("{"Expr
"}")? |ProofExpr
|TacticsExpr
|FnName
|Idiom
|List
|Alt
|Bracketed
|Constant
|Type
| "Void" |Quasiquote
|NameQuote
|Unquote
| "_" ; Bracketed ::= "("BracketedP
; BracketedP ::= ")" |Expr
")" |ExprList
")" |DependentPair
")" |Operator
Expr
")" |Expr
Operator
")" ; Alt ::= "(|"Expr_List
"|)" ; Expr_List ::= `Expr'` | `Expr'` ","Expr_List
; HSimpleExpr ::= "."SimpleExpr
|SimpleExpr
; UnifyLog ::= "%" "unifyLog"SimpleExpr
; RunTactics ::= "%" "runElab"SimpleExpr
; Disamb ::= "with"NameList
Expr
; NoImplicits ::= "%" "noImplicits"SimpleExpr
; App ::= "mkForeign"Arg
Arg
* |MatchApp
|SimpleExpr
Arg
* ; MatchApp ::=SimpleExpr
"<=="FnName
; Arg ::= ` ImplicitArg` |ConstraintArg
|SimpleExpr
; ImplicitArg ::= "{"Name
("="Expr
)? "}" ; ConstraintArg ::= "@{"Expr
"}" ; Quasiquote ::= "`("Expr
")" ; Unquote ::= ","Expr
; RecordType ::= "record" "{"FieldTypeList
"}" ; FieldTypeList ::=FieldType
|FieldType
","FieldTypeList
; FieldType ::=FnName
"="Expr
; TypeSig ::= ":"Expr
; TypeExpr ::=ConstraintList
?Expr
; Lambda ::= "\\"TypeOptDeclList
LambdaTail
| "\\"SimpleExprList
LambdaTail
; SimpleExprList ::=SimpleExpr
|SimpleExpr
","SimpleExprList
; LambdaTail ::=Impossible
| "=>"Expr
; RewriteTerm ::= "rewrite"Expr
("==>"Expr
)? "in"Expr
; RigCount ::= "1" : "0" ; Let ::= "let"Name
TypeSig
"? "="Expr
"in"Expr
| "let" `Expr'` "=" `Expr'` "in"Expr
; TypeSig' ::= ":" `Expr'` ; If ::= "if"Expr
"then"Expr
"else"Expr
; QuoteGoal ::= "quoteGoal"Name
"by"Expr
"in"Expr
;
Pies
Pi ::=PiOpts
Static
?PiP
; PiP ::=OpExpr
("->"Pi
)? | "("TypeDeclList
")" "->"Pi
| "{"TypeDeclList
"}" "->"Pi
| "{" "auto"TypeDeclList
"}" "->"Pi
| "{" "default"SimpleExpr
TypeDeclList
"}" "->"Pi
; PiOpts ::= "."? ; ConstraintList ::= "("Expr_List
")" "=>" |Expr
"=>" ; TypeDeclList ::=FunctionSignatureList
|NameList
TypeSig
; FunctionSignatureList ::=Name
TypeSig
|Name
TypeSig
","FunctionSignatureList
; TypeOptDeclList ::=NameOrPlaceholder
TypeSig
? |NameOrPlaceholder
TypeSig
? ","TypeOptDeclList
; NameOrPlaceHolder ::=Name
: "_" ; ListExpr ::= "[" "]" | "["Expr
"|"DoList
"]" | "["ExprList
"]" ; ExprList ::=Expr
|Expr
","ExprList
;
Do Blocks & Idioms
DoList ::=Do
:Do
","DoList
; Do' ::=Do
KeepTerminator
; DoBlock ::= "do"OpenBlock
`Do'`+CloseBlock
; Do ::= "let"Name
TypeSig
"? "="Expr
| "let" `Expr'` "="Expr
| "rewrite"Expr
|Name
"<-"Expr
| `Expr'` "<-"Expr
|Expr
; Idiom ::= "[|"Expr
"|]" ;
Constants
Constant ::= | "Integer" | "Int" | "Char" | "Double" | "String" | "Bits8" | "Bits16" | "Bits32" | "Bits64" |Float_t
|Natural_t
|VerbatimString_t
|String_t
|Char_t
; VerbatimString_t ::= "\"\"\"" ~"\"\"\"" "\""* "\"\"\"" ;
Tactics
Tactic ::= "intro"NameList
? | "intros" | "refine"Name
Imp
+ | "mrefine"Name
| "rewrite"Expr
| "induction"Expr
| "equiv"Expr
| "let"Name
":" `Expr'` "="Expr
| "let"Name
"="Expr
| "focus"Name
| "exact"Expr
| "applyTactic"Expr
| "reflect"Expr
| "fill"Expr
| "try"Tactic
"|"Tactic
| "{"TacticSeq
"}" | "compute" | "trivial" | "solve" | "attack" | "state" | "term" | "undo" | "qed" | "abandon" | ":" "q" ; TacticSeq ::=Tactic
";"Tactic
|Tactic
";"TacticSeq
;
Misc
Imp ::= "?" | "_" ; Static ::= "%static" ;
Data
Record ::=DocComment
Accessibility
? "record"FnName
TypeSig
"where"OpenBlock
Constructor
KeepTerminator
CloseBlock
; DataI ::= "data" | "codata"; Data ::=DocComment
?Accessibility
?DataI
FnName
TypeSig
ExplicitTypeDataRest
?DocComment
?Accessibility
?DataI
FnName
Name
*DataRest
? ; Constructor' ::=Constructor
KeepTerminator
; ExplicitTypeDataRest ::= "where"OpenBlock
`Constructor'`*CloseBlock
; DataRest ::= "="SimpleConstructorList
Terminator
| "where"!; SimpleConstructorList ::=SimpleConstructor
|SimpleConstructor
"|"SimpleConstructorList
; Constructor ::=DocComment
?FnName
TypeSig
; SimpleConstructor ::=FnName
SimpleExpr
*DocComment
?; DSL ::= "dsl"FnName
OpenBlock
`Overload'`+CloseBlock
; OverloadIdentifier ::= "let" |Identifier
; Overload ::=OverloadIdentifier
"="Expr
;
Operators
BacktickOperator ::=Name
; OperatorName ::=SymbolicOperator
:BacktickOperator
; OperatorFront ::= "(" "=" ")" | (Identifier_t
".")? "("Operator_t
")" ; FnName ::=Name
|OperatorFront
; Fixity ::=FixityType
Natural_t
OperatorList
Terminator
; FixityType ::= "infixl" | "infixr" | "infix" | "prefix";
Documentation
SingleLineComment_t ::= "--" ~EOL_t
*EOL_t
; MultiLineComment_t ::= "{" .. "}" | "{ -"InCommentChars_t
; InCommentChars_t ::= "- }" |MultiLineComment_t
InCommentChars_t
| ~"- }"+InCommentChars_t
; DocComment_t ::=DocCommentLine
(ArgCommentLine
DocCommentLine
*)* ; DocCommentLine ::= "|||" ~EOL_t
*EOL_t
; ArgCommentLine ::= "|||" "@" ~EOL_t
*EOL_t
;