idris-1.3.0: Functional Programming Language with Dependent Types

LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

Idris.Parser

Description

 

Synopsis

Documentation

type IdrisParser = Parser IState Source #

Idris parser with state used during parsing

moduleName :: Parsing m => m Name Source #

Parses module definition

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

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

Like addSyntax, but no effect on the IBC.

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

name :: (Parsing m, MonadState IState m) => m Name Source #

Parses a name

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

parseExpr :: IState -> String -> Either ParseError PTerm Source #

Parses an expression from 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