Parses module definition

ModuleHeader ::= 'module' Identifier_t ';'?;

Parses an import statement

  Import ::= 'import' Identifier_t ';'?;

Parses program source

     Prog ::= Decl* EOF;

Parses a top-level declaration

Decl ::=
    Decl'
  | Using
  | Params
  | Mutual
  | Namespace
  | Class
  | Instance
  | DSL
  | Directive
  | Provider
  | Transform
  | Import!
  ;

Parses a top-level declaration with possible syntax sugar

Decl' ::=
    Fixity
  | FunDecl'
  | Data
  | Record
  | SyntaxDecl
  ;

Parses a syntax extension declaration (and adds the rule to parser state)

  SyntaxDecl ::= SyntaxRule;

Parses a syntax extension declaration

SyntaxRuleOpts ::= term | pattern;

SyntaxRule ::=
  SyntaxRuleOpts? syntax SyntaxSym+ '=' TypeExpr Terminator;

SyntaxSym ::=   '[' Name_t ']'
             |  '{' Name_t '}'
             |  Name_t
             |  StringLiteral_t
             ;

Parses a syntax symbol (either binding variable, keyword or expression)

SyntaxSym ::=   '[' Name_t ']'
             |  '{' Name_t '}'
             |  Name_t
             |  StringLiteral_t
             ;

Parses a function declaration with possible syntax sugar

  FunDecl ::= FunDecl';

Parses a function declaration

 FunDecl' ::=
  DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
  | Postulate
  | Pattern
  | CAF
  ;

Parses function options given initial options

FnOpts ::= total
  | partial
  | implicit
  | % assert_total
  | % reflection
  | % specialise '[' NameTimesList? ']'
  ;

NameTimes ::= FnName Natural?;

NameTimesList ::=
  NameTimes
  | NameTimes ',' NameTimesList
  ;

Parses a postulate

Postulate ::=
  DocComment_t? postulate FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
  ;

Parses a using declaration

Using ::=
  using '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
  ;

Parses a parameters declaration

Params ::=
  parameters '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
  ;

Parses a mutual declaration (for mutually recursive functions)

Mutual ::=
  mutual OpenBlock Decl* CloseBlock
  ;

Parses a namespace declaration

Namespace ::=
  namespace identifier OpenBlock Decl+ CloseBlock
  ;

Parses a methods block (for type classes and instances)

  MethodsBlock ::= 'where' OpenBlock FnDecl* CloseBlock

Parses a type class declaration

ClassArgument ::=
   Name
   | '(' Name : Expr ')'
   ;

Class ::=
  DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* MethodsBlock?
  ;

Parses a type class instance declaration

  Instance ::=
    'instance' InstanceName? ConstraintList? Name SimpleExpr* MethodsBlock?
    ;

InstanceName ::= '[' Name ']';

Parses a using declaration list

UsingDeclList ::=
  UsingDeclList'
  | NameList TypeSig
  ;

UsingDeclList' ::=
  UsingDecl
  | UsingDecl ',' UsingDeclList'
  ;

NameList ::=
  Name
  | Name ',' NameList
  ;

Parses a using declaration

UsingDecl ::=
  FnName TypeSig
  | FnName FnName+
  ;

Parse a clause with patterns

Pattern ::= Clause;

Parse a constant applicative form declaration CAF ::= 'let' FnName '=' Expr Terminator;

Parse an argument expression

ArgExpr ::= HSimpleExpr | ;

Parse a right hand side of a function

RHS ::= '='            Expr
     |  ?=  RHSName? Expr
     |  impossible
     ;

RHSName ::= '{' FnName '}';

Parses a function clause

RHSOrWithBlock ::= RHS WhereOrTerminator
               | with SimpleExpr OpenBlock FnDecl+ CloseBlock
               ;

Clause ::=                                                               WExpr+ RHSOrWithBlock
       |   SimpleExpr <==  FnName                                             RHS WhereOrTerminator
       |   ArgExpr Operator ArgExpr                                      WExpr* RHSOrWithBlock 
       |                     FnName ConstraintArg* ImplicitOrArgExpr*    WExpr* RHSOrWithBlock
       ;

ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;

WhereOrTerminator ::= WhereBlock | Terminator;

Parses with pattern

 WExpr ::= '|' Expr';

Parses a where block

WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;

Parses a code generation target language name

Codegen ::= C
        |   Java
        |   JavaScript
        |   Node
        |   LLVM
        |   Bytecode
        ;

Parses a compiler directive

StringList ::=
  String
  | String ',' StringList
  ;

Directive ::= % Directive';

Directive' ::= lib      CodeGen String_t
           |   link     CodeGen String_t
           |   flag     CodeGen String_t
           |   include  CodeGen String_t
           |   hide     Name
           |   freeze   Name
           |   access   Accessibility
           |   'default'  Totality
           |   logging  Natural
           |   dynamic  StringList
           |   language TypeProviders
           |   language ErrorReflection
           ;

Parses a totality

Totality ::= partial | total

Parses a type provider

Provider ::= % provide '(' FnName TypeSig ')' with Expr;

Parses a transform

Transform ::= % transform Expr ==> Expr

Parses an expression from input

Parses a tactic from input

Parse module header and imports

There should be a better way of doing this...

A program is a list of declarations, possibly with associated documentation strings.

Load idris module and show error if something wrong happens

Load idris module

Load idris code from file

Load idris source code and show error if something wrong happens

Load Idris source code

Adds names to hide list