idris-1.1.0: Functional Programming Language with Dependent Types

CopyrightLicense : BSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

Idris.Parser

Contents

Description

 

Synopsis

Main grammar

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

Parses module definition

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

import_ :: IdrisParser ImportInfo Source #

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

decl' :: SyntaxInfo -> IdrisParser PDecl Source #

Parses a top-level declaration with possible syntax sugar

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

syntaxDecl :: SyntaxInfo -> IdrisParser PDecl Source #

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

  SyntaxDecl ::= SyntaxRule;

addSyntax :: IState -> Syntax -> IState Source #

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

addReplSyntax :: IState -> Syntax -> IState Source #

Like addSyntax, but no effect on the IBC.

syntaxRule :: SyntaxInfo -> IdrisParser Syntax Source #

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 Source #

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 PDecl Source #

Parses a function declaration

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

fnOpts :: IdrisParser ([FnOpt], Accessibility) Source #

Parses a series of function and accessbility options

FnOpts ::= FnOpt* Accessibility FnOpt*

fnOpt :: IdrisParser FnOpt Source #

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 Source #

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
  ;

openInterface :: SyntaxInfo -> IdrisParser [PDecl] Source #

Parses an open block

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
  ;

implementationBlock :: SyntaxInfo -> IdrisParser [PDecl] Source #

Parses a methods block (for implementations)

  ImplementationBlock ::= 'where' OpenBlock FnDecl* CloseBlock

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

Parses a methods and implementations block (for interfaces)

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

interface_ :: SyntaxInfo -> IdrisParser [PDecl] Source #

Parses an interface declaration

InterfaceArgument ::=
   Name
   | '(' Name : Expr ')'
   ;
Interface ::=
  DocComment_t? Accessibility? interface ConstraintList? Name InterfaceArgument* InterfaceBlock?
  ;

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

Parses an interface implementation declaration

  Implementation ::=
    DocComment_t? implementation ImplementationName? ConstraintList? Name SimpleExpr* ImplementationBlock?
    ;
ImplementationName ::= '[' 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 Using Source #

Parses a using declaration

UsingDecl ::=
  FnName TypeSig
  | FnName FnName+
  ;

pattern :: SyntaxInfo -> IdrisParser PDecl Source #

Parse a clause with patterns

Pattern ::= Clause;

caf :: SyntaxInfo -> IdrisParser PDecl Source #

Parse a constant applicative form declaration

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

argExpr :: SyntaxInfo -> IdrisParser PTerm Source #

Parse an argument expression

ArgExpr ::= HSimpleExpr | ;

rhs :: SyntaxInfo -> Name -> IdrisParser PTerm Source #

Parse a right hand side of a function

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

clause :: SyntaxInfo -> IdrisParser PClause Source #

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 Source #

Parses with pattern

WExpr ::= '|' Expr';

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

Parses a where block

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

codegen_ :: IdrisParser Codegen Source #

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
           |   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
           ;

totality :: IdrisParser DefaultTotality Source #

Parses a totality

Totality ::= partial | total | covering

provider :: SyntaxInfo -> IdrisParser [PDecl] Source #

Parses a type provider

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

transform :: SyntaxInfo -> IdrisParser [PDecl] Source #

Parses a transform

Transform ::= % transform Expr ==> Expr

runElabDecl :: SyntaxInfo -> IdrisParser PDecl Source #

Parses a top-level reflected elaborator script

RunElabDecl ::= % runElab Expr

Loading and parsing

parseExpr :: IState -> String -> Result PTerm Source #

Parses an expression from input

parseConst :: IState -> String -> Result Const Source #

Parses a constant form input

parseTactic :: IState -> String -> Result PTactic Source #

Parses a tactic from input

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

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

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

Parse module header and imports

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

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

fixColour :: Bool -> Doc -> Doc Source #

Check if the coloring matches the options and corrects if necessary

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

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

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

Load idris module and show error if something wrong happens

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

Load idris module

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

Load idris code from file

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

Load idris source code and show error if something wrong happens

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

Load Idris source code

addHides :: Ctxt Accessibility -> Idris () Source #

Adds names to hide list