| License | BSD3 |
|---|---|
| Maintainer | The Idris Community. |
| Safe Haskell | None |
| Language | Haskell2010 |
Idris.Parser
Description
- type IdrisParser = Parser IState
- data ImportInfo = ImportInfo {}
- moduleName :: Parsing m => m Name
- addReplSyntax :: IState -> Syntax -> IState
- clearParserWarnings :: Idris ()
- decl :: SyntaxInfo -> IdrisParser [PDecl]
- fixColour :: Bool -> Doc -> Doc
- loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()
- loadModule :: FilePath -> IBCPhase -> Idris (Maybe String)
- name :: (Parsing m, MonadState IState m) => m Name
- opChars :: String
- parseElabShellStep :: IState -> String -> Either ParseError (Either ElabShellCmd PDo)
- parseConst :: IState -> String -> Either ParseError Const
- parseExpr :: IState -> String -> Either ParseError PTerm
- parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark)
- parseTactic :: IState -> String -> Either ParseError PTactic
- runparser :: Parser st res -> st -> String -> String -> Either ParseError res
- data ParseError
- parseErrorDoc :: ParseError -> Doc
Documentation
type IdrisParser = Parser IState Source #
Idris parser with state used during parsing
data ImportInfo Source #
Constructors
| ImportInfo | |
Fields
| |
moduleName :: Parsing m => m Name Source #
Parses module definition
ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;
clearParserWarnings :: Idris () Source #
decl :: SyntaxInfo -> IdrisParser [PDecl] Source #
Parses a top-level declaration
Decl ::=
Decl'
| Using
| Params
| Mutual
| Namespace
| Interface
| Implementation
| DSL
| Directive
| Provider
| Transform
| Import!
| RunElabDecl
;
fixColour :: Bool -> Doc -> Doc Source #
Check if the coloring matches the options and corrects if necessary
loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris () Source #
Load idris code from file
loadModule :: FilePath -> IBCPhase -> Idris (Maybe String) Source #
Load idris module and show error if something wrong happens
parseElabShellStep :: IState -> String -> Either ParseError (Either ElabShellCmd PDo) Source #
Parses a do-step from input (used in the elab shell)
parseConst :: IState -> String -> Either ParseError Const Source #
Parses a constant form input
parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark) Source #
Parse module header and imports
parseTactic :: IState -> String -> Either ParseError PTactic Source #
Parses a tactic from input
runparser :: Parser st res -> st -> String -> String -> Either ParseError res Source #
Run the Idris parser stack
data ParseError Source #
Instances
parseErrorDoc :: ParseError -> Doc Source #