License | BSD3 |
---|---|
Maintainer | The Idris Community. |
Safe Haskell | None |
Language | Haskell2010 |
- type IdrisParser = Parser IState
- data ImportInfo = ImportInfo {}
- 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 #
ImportInfo | |
|
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 #
parseErrorDoc :: ParseError -> Doc Source #