idris

Safe HaskellNone

Idris.Parser

Contents

Synopsis

Main grammar

moduleHeader :: IdrisParser [String]Source

Parses module definition

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

import_ :: IdrisParser StringSource

Parses an import statement

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

prog :: SyntaxInfo -> IdrisParser [PDecl]Source

Parses program source

     Prog ::= Decl* EOF;

decl :: SyntaxInfo -> IdrisParser [PDecl]Source

Parses a top-level declaration

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

decl' :: SyntaxInfo -> IdrisParser PDeclSource

Parses a top-level declaration with possible syntax sugar

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

syntaxDecl :: SyntaxInfo -> IdrisParser PDeclSource

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

  SyntaxDecl ::= SyntaxRule;

syntaxRule :: SyntaxInfo -> IdrisParser SyntaxSource

Parses a syntax extension declaration

SyntaxRuleOpts ::= termpattern;
SyntaxRule ::=
  SyntaxRuleOpts? syntax SyntaxSym+ '=' TypeExpr Terminator;
SyntaxSym ::=   '[' Name_t ']'
             |  '{' Name_t '}'
             |  Name_t
             |  StringLiteral_t
             ;

syntaxSym :: IdrisParser SSymbolSource

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

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

fnDecl :: SyntaxInfo -> IdrisParser [PDecl]Source

Parses a function declaration with possible syntax sugar

  FunDecl ::= FunDecl';

fnDecl' :: SyntaxInfo -> IdrisParser PDeclSource

Parses a function declaration

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

fnOpts :: [FnOpt] -> IdrisParser [FnOpt]Source

Parses function options given initial options

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

postulate :: SyntaxInfo -> IdrisParser PDeclSource

Parses a postulate

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

using_ :: SyntaxInfo -> IdrisParser [PDecl]Source

Parses a using declaration

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

params :: SyntaxInfo -> IdrisParser [PDecl]Source

Parses a parameters declaration

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

mutual :: SyntaxInfo -> IdrisParser [PDecl]Source

Parses a mutual declaration (for mutually recursive functions)

Mutual ::=
  mutual OpenBlock Decl* CloseBlock
  ;

namespace :: SyntaxInfo -> IdrisParser [PDecl]Source

Parses a namespace declaration

Namespace ::=
  namespace identifier OpenBlock Decl+ CloseBlock
  ;

methodsBlock :: SyntaxInfo -> IdrisParser [PDecl]Source

Parses a methods block (for type classes and instances)

  MethodsBlock ::= 'where' OpenBlock FnDecl* CloseBlock

class_ :: SyntaxInfo -> IdrisParser [PDecl]Source

Parses a type class declaration

ClassArgument ::=
   Name
   | '(' Name : Expr ')'
   ;
Class ::=
  DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* MethodsBlock?
  ;

instance_ :: SyntaxInfo -> IdrisParser [PDecl]Source

Parses a type class instance declaration

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

usingDeclList :: SyntaxInfo -> IdrisParser [Using]Source

Parses a using declaration list

UsingDeclList ::=
  UsingDeclList'
  | NameList TypeSig
  ;
UsingDeclList' ::=
  UsingDecl
  | UsingDecl ',' UsingDeclList'
  ;
NameList ::=
  Name
  | Name ',' NameList
  ;

usingDecl :: SyntaxInfo -> IdrisParser UsingSource

Parses a using declaration

UsingDecl ::=
  FnName TypeSig
  | FnName FnName+
  ;

pattern :: SyntaxInfo -> IdrisParser PDeclSource

Parse a clause with patterns

Pattern ::= Clause;

caf :: SyntaxInfo -> IdrisParser PDeclSource

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

argExpr :: SyntaxInfo -> IdrisParser PTermSource

Parse an argument expression

ArgExpr ::= HSimpleExpr | ;

rhs :: SyntaxInfo -> Name -> IdrisParser PTermSource

Parse a right hand side of a function

RHS ::= '='            Expr
     |  ?=  RHSName? Expr
     |  impossible
     ;
RHSName ::= '{' FnName '}';

clause :: SyntaxInfo -> IdrisParser PClauseSource

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 PTermSource

Parses with pattern

 WExpr ::= '|' Expr';

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

Parses a where block

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

codegen_ :: IdrisParser CodegenSource

Parses a code generation target language name

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

directive :: SyntaxInfo -> IdrisParser [PDecl]Source

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
           ;

totality :: IdrisParser BoolSource

Parses a totality

Totality ::= partial | total

provider :: SyntaxInfo -> IdrisParser [PDecl]Source

Parses a type provider

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

transform :: SyntaxInfo -> IdrisParser [PDecl]Source

Parses a transform

Transform ::= % transform Expr ==> Expr

Loading and parsing

parseExpr :: IState -> String -> Result PTermSource

Parses an expression from input

parseTactic :: IState -> String -> Result PTacticSource

Parses a tactic from input

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

Parse module header and imports

findFC :: Doc -> (FC, String)Source

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

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

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

loadModule :: Handle -> FilePath -> Idris StringSource

Load idris module and show error if something wrong happens

loadModule' :: Handle -> FilePath -> Idris StringSource

Load idris module

loadFromIFile :: Handle -> IFileType -> Idris ()Source

Load idris code from file

loadSource' :: Handle -> Bool -> FilePath -> Idris ()Source

Load idris source code and show error if something wrong happens

loadSource :: Handle -> Bool -> FilePath -> Idris ()Source

Load Idris source code

addHides :: [(Name, Maybe Accessibility)] -> Idris ()Source

Adds names to hide list