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
  | Interface
  | Implementation
  | DSL
  | Directive
  | Provider
  | Transform
  | Import!
  | RunElabDecl
  ;

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 a series of function and accessbility options

FnOpts ::= FnOpt* Accessibility FnOpt*

Parses a function option

FnOpt ::= total
  | partial
  | covering
  | 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 an open block

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 implementations)

  ImplementationBlock ::= 'where' OpenBlock FnDecl* CloseBlock

Parses a methods and implementations block (for interfaces)

MethodOrImplementation ::=
   FnDecl
   | Implementation
   ;

InterfaceBlock ::=
  'where' OpenBlock Constructor? MethodOrImplementation* CloseBlock
  ;

Parses an interface declaration

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

Interface ::=
  DocComment_t? Accessibility? interface ConstraintList? Name InterfaceArgument* InterfaceBlock?
  ;

Parses an interface implementation declaration

  Implementation ::=
    DocComment_t? implementation ImplementationName? ConstraintList? Name SimpleExpr* ImplementationBlock?
    ;

ImplementationName ::= '[' 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
           |   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
           ;

Parses a totality

Totality ::= partial | total | covering

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 a top-level reflected elaborator script

RunElabDecl ::= % runElab Expr

Parses an expression from input

Parses a constant form input

Parses a tactic from input

Parses a do-step from input (used in the elab shell)

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