Idris.Parser

Main grammar

moduleHeader :: IdrisParser (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])

Parses module definition

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

data ImportInfo

Constructors

ImportInfo

Fields

• import_reexport :: Bool
• import_path :: FilePath
• import_rename :: Maybe (String, FC)
• import_namespace :: [Text]
• import_location :: FC
• import_modname_location :: FC

import_ :: IdrisParser ImportInfo

Parses an import statement

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

prog :: SyntaxInfo -> IdrisParser [PDecl]

Parses program source

     Prog ::= Decl* EOF;

decl :: SyntaxInfo -> IdrisParser [PDecl]

Parses a top-level declaration

Decl ::=
    Decl'
  | Using
  | Params
  | Mutual
  | Namespace
  | Interface
  | Implementation
  | DSL
  | Directive
  | Provider
  | Transform
  | Import!
  | RunElabDecl
  ;

internalDecl :: SyntaxInfo -> IdrisParser [PDecl]

decl' :: SyntaxInfo -> IdrisParser PDecl

Parses a top-level declaration with possible syntax sugar

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

externalDecl :: SyntaxInfo -> IdrisParser [PDecl]

declExtensions :: SyntaxInfo -> [Syntax] -> IdrisParser [PDecl]

declExtension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser [PDecl]

syntaxDecl :: SyntaxInfo -> IdrisParser PDecl

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

  SyntaxDecl ::= SyntaxRule;

addSyntax :: IState -> Syntax -> IState

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

addReplSyntax :: IState -> Syntax -> IState

Like addSyntax, but no effect on the IBC.

syntaxRule :: SyntaxInfo -> IdrisParser Syntax

Parses a syntax extension declaration

SyntaxRuleOpts ::= term | pattern;

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

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

syntaxSym :: IdrisParser SSymbol

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

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

fnDecl :: SyntaxInfo -> IdrisParser [PDecl]

Parses a function declaration with possible syntax sugar

  FunDecl ::= FunDecl';

fnDecl' :: SyntaxInfo -> IdrisParser PDecl

Parses a function declaration

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

fnOpts :: IdrisParser ([FnOpt], Accessibility)

Parses a series of function and accessbility options

FnOpts ::= FnOpt* Accessibility FnOpt*

fnOpt :: IdrisParser 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
  ;

postulate :: SyntaxInfo -> IdrisParser PDecl

Parses a postulate

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

using_ :: SyntaxInfo -> IdrisParser [PDecl]

Parses a using declaration

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

params :: SyntaxInfo -> IdrisParser [PDecl]

Parses a parameters declaration

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

openInterface :: SyntaxInfo -> IdrisParser [PDecl]

Parses an open block

mutual :: SyntaxInfo -> IdrisParser [PDecl]

Parses a mutual declaration (for mutually recursive functions)

Mutual ::=
  mutual OpenBlock Decl* CloseBlock
  ;

namespace :: SyntaxInfo -> IdrisParser [PDecl]

Parses a namespace declaration

Namespace ::=
  namespace identifier OpenBlock Decl+ CloseBlock
  ;

implementationBlock :: SyntaxInfo -> IdrisParser [PDecl]

Parses a methods block (for implementations)

  ImplementationBlock ::= 'where' OpenBlock FnDecl* CloseBlock

interfaceBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])

Parses a methods and implementations block (for interfaces)

MethodOrImplementation ::=
   FnDecl
   | Implementation
   ;

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

interface_ :: SyntaxInfo -> IdrisParser [PDecl]

Parses an interface declaration

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

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

implementation :: Bool -> SyntaxInfo -> IdrisParser [PDecl]

Parses an interface implementation declaration

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

ImplementationName ::= '[' Name ']';

docstring :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))])

Parse a docstring

usingDeclList :: SyntaxInfo -> IdrisParser [Using]

Parses a using declaration list

UsingDeclList ::=
  UsingDeclList'
  | NameList TypeSig
  ;

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

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

usingDecl :: SyntaxInfo -> IdrisParser Using

Parses a using declaration

UsingDecl ::=
  FnName TypeSig
  | FnName FnName+
  ;

pattern :: SyntaxInfo -> IdrisParser PDecl

Parse a clause with patterns

Pattern ::= Clause;

caf :: SyntaxInfo -> IdrisParser PDecl

Parse a constant applicative form declaration

CAF ::= 'let' FnName '=' Expr Terminator;

argExpr :: SyntaxInfo -> IdrisParser PTerm

Parse an argument expression

ArgExpr ::= HSimpleExpr | ;

rhs :: SyntaxInfo -> Name -> IdrisParser PTerm

Parse a right hand side of a function

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

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

clause :: SyntaxInfo -> IdrisParser PClause

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;

wExpr :: SyntaxInfo -> IdrisParser PTerm

Parses with pattern

WExpr ::= '|' Expr';

whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])

Parses a where block

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

codegen_ :: IdrisParser Codegen

Parses a code generation target language name

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

directive :: SyntaxInfo -> IdrisParser [PDecl]

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
           ;

pLangExt :: IdrisParser LanguageExt

totality :: IdrisParser DefaultTotality

Parses a totality

Totality ::= partial | total | covering

provider :: SyntaxInfo -> IdrisParser [PDecl]

Parses a type provider

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

transform :: SyntaxInfo -> IdrisParser [PDecl]

Parses a transform

Transform ::= % transform Expr ==> Expr

runElabDecl :: SyntaxInfo -> IdrisParser PDecl

Parses a top-level reflected elaborator script

RunElabDecl ::= % runElab Expr

Loading and parsing

parseExpr :: IState -> String -> Result PTerm

Parses an expression from input

parseConst :: IState -> String -> Result Const

Parses a constant form input

parseTactic :: IState -> String -> Result PTactic

Parses a tactic from input

parseElabShellStep :: IState -> String -> Result (Either ElabShellCmd PDo)

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

parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Delta)

Parse module header and imports

findFC :: Doc -> (FC, String)

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

fixColour :: Bool -> Doc -> Doc

Check if the coloring matches the options and corrects if necessary

parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta -> Idris [PDecl]

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

loadModule :: FilePath -> IBCPhase -> Idris (Maybe String)

Load idris module and show error if something wrong happens

loadModule' :: FilePath -> IBCPhase -> Idris (Maybe String)

Load idris module

loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()

Load idris code from file

loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()

Load idris source code and show error if something wrong happens

loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()

Load Idris source code

addHides :: Ctxt Accessibility -> Idris ()

Adds names to hide list

module Idris.Parser.Expr

module Idris.Parser.Data

module Idris.Parser.Helpers

module Idris.Parser.Ops