문법 참조
문법 참조 (Syntax Reference)
여기에서는 Idris의 표면 문법(surface syntax)을 eBNF 문법으로 대략적으로 설명할게요. 이 문서가 제시하는 문법은 파서(parser)와 문법 설명이 서로 동기화되어 있지 않기 때문에, Idris 파서가 실제로 처리할 수 있는 문법과 다를 수 있어요.
출처: 문서
본문
표기법 (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 블록과 관용구 (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 ;