Parses module definition

      ModuleHeader ::= DocComment_t? '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;

Extend an IState with a new syntax extension. See also addReplSyntax.

Like addSyntax, but no effect on the IBC.

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
  | % no_implicit
  | % assert_total
  | % error_handler
  | % 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 instances)

  InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock

Parses a methods and instances block (for type classes)

MethodOrInstance ::=
   FnDecl
   | Instance
   ;

ClassBlock ::=
  'where' OpenBlock MethodOrInstance* CloseBlock
  ;

Parses a type class declaration

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

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

Parses a type class instance declaration

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

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

Parse a docstring

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
           |   name           Name NameList
           |   error_handlers Name NameList
           |   language       TypeProviders
           |   language       ErrorReflection
           ;

Parses a totality

Totality ::= partial | total

Parses a type provider

Provider ::= DocComment_t? % provide Provider_What? '(' FnName TypeSig ')' with Expr;
ProviderWhat ::= proof | term | 'type' | postulate

Parses a transform

Transform ::= % transform Expr ==> Expr

Parses an expression from input

Parses a constant form input

Parses a tactic from input

Parse module header and imports

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

Check if the coloring matches the options and corrects if necessary

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