Safe Haskell | None |
---|---|
Language | Haskell98 |
- moduleHeader :: IdrisParser (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
- data ImportInfo = ImportInfo {}
- import_ :: IdrisParser ImportInfo
- prog :: SyntaxInfo -> IdrisParser [PDecl]
- decl :: SyntaxInfo -> IdrisParser [PDecl]
- internalDecl :: SyntaxInfo -> IdrisParser [PDecl]
- decl' :: SyntaxInfo -> IdrisParser PDecl
- externalDecl :: SyntaxInfo -> IdrisParser [PDecl]
- declExtensions :: SyntaxInfo -> [Syntax] -> IdrisParser [PDecl]
- declExtension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser [PDecl]
- syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
- addSyntax :: IState -> Syntax -> IState
- addReplSyntax :: IState -> Syntax -> IState
- syntaxRule :: SyntaxInfo -> IdrisParser Syntax
- syntaxSym :: IdrisParser SSymbol
- fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
- fnDecl' :: SyntaxInfo -> IdrisParser PDecl
- fnOpts :: IdrisParser ([FnOpt], Accessibility)
- fnOpt :: IdrisParser FnOpt
- postulate :: SyntaxInfo -> IdrisParser PDecl
- using_ :: SyntaxInfo -> IdrisParser [PDecl]
- params :: SyntaxInfo -> IdrisParser [PDecl]
- openInterface :: SyntaxInfo -> IdrisParser [PDecl]
- mutual :: SyntaxInfo -> IdrisParser [PDecl]
- namespace :: SyntaxInfo -> IdrisParser [PDecl]
- instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
- classBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])
- class_ :: SyntaxInfo -> IdrisParser [PDecl]
- instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl]
- docstring :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))])
- usingDeclList :: SyntaxInfo -> IdrisParser [Using]
- usingDecl :: SyntaxInfo -> IdrisParser Using
- pattern :: SyntaxInfo -> IdrisParser PDecl
- caf :: SyntaxInfo -> IdrisParser PDecl
- argExpr :: SyntaxInfo -> IdrisParser PTerm
- rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
- clause :: SyntaxInfo -> IdrisParser PClause
- wExpr :: SyntaxInfo -> IdrisParser PTerm
- whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
- codegen_ :: IdrisParser Codegen
- directive :: SyntaxInfo -> IdrisParser [PDecl]
- pLangExt :: IdrisParser LanguageExt
- totality :: IdrisParser DefaultTotality
- provider :: SyntaxInfo -> IdrisParser [PDecl]
- transform :: SyntaxInfo -> IdrisParser [PDecl]
- runElabDecl :: SyntaxInfo -> IdrisParser PDecl
- parseExpr :: IState -> String -> Result PTerm
- parseConst :: IState -> String -> Result Const
- parseTactic :: IState -> String -> Result PTactic
- parseElabShellStep :: IState -> String -> Result (Either ElabShellCmd PDo)
- parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Delta)
- findFC :: Doc -> (FC, String)
- fixColour :: Bool -> Doc -> Doc
- parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta -> Idris [PDecl]
- loadModule :: FilePath -> IBCPhase -> Idris (Maybe String)
- loadModule' :: FilePath -> IBCPhase -> Idris (Maybe String)
- loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()
- loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
- loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
- addHides :: Ctxt Accessibility -> Idris ()
- module Idris.Parser.Expr
- module Idris.Parser.Data
- module Idris.Parser.Helpers
- module Idris.Parser.Ops
Main grammar
moduleHeader :: IdrisParser (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)]) Source
Parses module definition
ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;
data ImportInfo Source
ImportInfo | |
|
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 | Class | Instance | DSL | Directive | Provider | Transform | Import! | RunElabDecl ;
internalDecl :: SyntaxInfo -> IdrisParser [PDecl] Source
decl' :: SyntaxInfo -> IdrisParser PDecl Source
Parses a top-level declaration with possible syntax sugar
Decl' ::= Fixity | FunDecl' | Data | Record | SyntaxDecl ;
externalDecl :: SyntaxInfo -> IdrisParser [PDecl] Source
declExtensions :: SyntaxInfo -> [Syntax] -> IdrisParser [PDecl] Source
declExtension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser [PDecl] Source
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
.
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
;
instanceBlock :: SyntaxInfo -> IdrisParser [PDecl] Source
Parses a methods block (for instances)
InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
classBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl]) Source
Parses a methods and instances block (for type classes)
MethodOrInstance ::= FnDecl | Instance ;
ClassBlock ::= 'where' OpenBlock Constructor? MethodOrInstance* CloseBlock ;
class_ :: SyntaxInfo -> IdrisParser [PDecl] Source
Parses a type class declaration
ClassArgument ::=
Name
| '(' Name :
Expr ')'
;
Class ::= DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock? ;
instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl] Source
Parses a type class instance declaration
Instance ::= DocComment_t? 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock? ;
InstanceName ::= '[' Name ']';
docstring :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))]) Source
Parse a docstring
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 |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
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
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
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
addHides :: Ctxt Accessibility -> Idris () Source
Adds names to hide list
module Idris.Parser.Expr
module Idris.Parser.Data
module Idris.Parser.Helpers
module Idris.Parser.Ops