idris-0.9.19: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.ParseHelpers

Contents

Synopsis

Documentation

type IdrisParser = StateT IState IdrisInnerParser Source

Idris parser with state used during parsing

newtype IdrisInnerParser a Source

Constructors

IdrisInnerParser 

Fields

runInnerParser :: Parser a
 

Instances

type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m) Source

Generalized monadic parsing constraint type

class HasLastTokenSpan m where Source

Methods

getLastTokenSpan :: m (Maybe FC) Source

Instances

runparser :: StateT st IdrisInnerParser res -> st -> String -> String -> Result res Source

Helper to run Idris inner parser based stateT parsers

highlightP :: FC -> OutputAnnotation -> IdrisParser () Source

noDocCommentHere :: String -> IdrisParser () Source

clearParserWarnings :: Idris () Source

reportParserWarnings :: Idris () Source

Space, comments and literals (token/lexing like parsers)

simpleWhiteSpace :: MonadicParsing m => m () Source

Consumes any simple whitespace (any character which satisfies Char.isSpace)

isEol :: Char -> Bool Source

Checks if a charcter is end of line

eol :: MonadicParsing m => m () Source

A parser that succeeds at the end of the line

singleLineComment :: MonadicParsing m => m () Source

Consumes a single-line comment

     SingleLineComment_t ::= '--' ~EOL_t* EOL_t ;

multiLineComment :: MonadicParsing m => m () Source

Consumes a multi-line comment

  MultiLineComment_t ::=
     '{ -- }'
   | '{ -' InCommentChars_t
  ;

  InCommentChars_t ::=
   '- }'
   | MultiLineComment_t InCommentChars_t
   | ~'- }'+ InCommentChars_t
  ;

docComment :: IdrisParser (Docstring (), [(Name, Docstring ())]) Source

Parses a documentation comment

  DocComment_t ::=   ||| ~EOL_t* EOL_t
                 ;

whiteSpace :: MonadicParsing m => m () Source

Parses some white space

stringLiteral :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC) Source

Parses a string literal

charLiteral :: (MonadicParsing m, HasLastTokenSpan m) => m (Char, FC) Source

Parses a char literal

natural :: (MonadicParsing m, HasLastTokenSpan m) => m (Integer, FC) Source

Parses a natural number

integer :: MonadicParsing m => m Integer Source

Parses an integral number

float :: (MonadicParsing m, HasLastTokenSpan m) => m (Double, FC) Source

Parses a floating point number

Symbols, identifiers, names and operators

idrisStyle :: MonadicParsing m => IdentifierStyle m Source

Idris Style for parsing identifiers/reserved keywords

char :: MonadicParsing m => Char -> m Char Source

string :: MonadicParsing m => String -> m String Source

lchar :: MonadicParsing m => Char -> m Char Source

Parses a character as a token

lcharFC :: MonadicParsing m => Char -> m FC Source

Parses a character as a token, returning the source span of the character

symbol :: MonadicParsing m => String -> m String Source

Parses string as a token

symbolFC :: MonadicParsing m => String -> m FC Source

reserved :: MonadicParsing m => String -> m () Source

Parses a reserved identifier

reservedFC :: MonadicParsing m => String -> m FC Source

Parses a reserved identifier, computing its span. Assumes that reserved identifiers never contain line breaks.

reservedHL :: String -> IdrisParser () Source

Parse a reserved identfier, highlighting its span as a keyword

reservedOp :: MonadicParsing m => String -> m () Source

Parses a reserved operator

reservedOpFC :: MonadicParsing m => String -> m FC Source

identifier :: MonadicParsing m => m (String, FC) Source

Parses an identifier as a token

iName :: (MonadicParsing m, HasLastTokenSpan m) => [String] -> m (Name, FC) Source

Parses an identifier with possible namespace as a name

maybeWithNS :: (MonadicParsing m, HasLastTokenSpan m) => m (String, FC) -> Bool -> [String] -> m (Name, FC) Source

Parses an string possibly prefixed by a namespace

name :: IdrisParser (Name, FC) Source

Parses a name

initsEndAt :: (a -> Bool) -> [a] -> [[a]] Source

List of all initial segments in ascending order of a list. Every such initial segment ends right before an element satisfying the given condition.

mkName :: (String, String) -> Name Source

Create a Name from a pair of strings representing a base name and its namespace.

opChars :: String Source

operatorLetter :: MonadicParsing m => m Char Source

commentMarkers :: [String] Source

invalidOperators :: [String] Source

operator :: MonadicParsing m => m String Source

Parses an operator

operatorFC :: MonadicParsing m => m (String, FC) Source

Parses an operator

Position helpers

fileName :: Delta -> String Source

Get filename from position (returns "(interactive)" when no source file is given)

lineNum :: Delta -> Int Source

Get line number from position

columnNum :: Delta -> Int Source

Get column number from position

getFC :: MonadicParsing m => m FC Source

Get file position as FC

Syntax helpers

bindList :: (Name -> FC -> PTerm -> PTerm -> PTerm) -> [(Name, FC, PTerm)] -> PTerm -> PTerm Source

Bind constraints to term

commaSeparated :: MonadicParsing m => m a -> m [a] Source

commaSeparated p parses one or more occurences of p, separated by commas and optional whitespace.

Layout helpers

pushIndent :: IdrisParser () Source

Push indentation to stack

popIndent :: IdrisParser () Source

Pops indentation from stack

indent :: IdrisParser Int Source

Gets current indentation

lastIndent :: IdrisParser Int Source

Gets last indentation

indented :: IdrisParser a -> IdrisParser a Source

Applies parser in an indented position

indentedBlock :: IdrisParser a -> IdrisParser [a] Source

Applies parser to get a block (which has possibly indented statements)

indentedBlock1 :: IdrisParser a -> IdrisParser [a] Source

Applies parser to get a block with at least one statement (which has possibly indented statements)

indentedBlockS :: IdrisParser a -> IdrisParser a Source

Applies parser to get a block with exactly one (possibly indented) statement

lookAheadMatches :: MonadicParsing m => m a -> m Bool Source

Checks if the following character matches provided parser

openBlock :: IdrisParser () Source

Parses a start of block

closeBlock :: IdrisParser () Source

Parses an end of block

terminator :: IdrisParser () Source

Parses a terminator

keepTerminator :: IdrisParser () Source

Parses and keeps a terminator

notEndApp :: IdrisParser () Source

Checks if application expression does not end

notEndBlock :: IdrisParser () Source

Checks that it is not end of block

data IndentProperty Source

Representation of an operation that can compare the current indentation with the last indentation, and an error message if it fails

Constructors

IndentProperty (Int -> Int -> Bool) String 

indentPropHolds :: IndentProperty -> IdrisParser () Source

Allows comparison of indent, and fails if property doesn't hold

gtProp :: IndentProperty Source

Greater-than indent property

gteProp :: IndentProperty Source

Greater-than or equal to indent property

eqProp :: IndentProperty Source

Equal indent property

ltProp :: IndentProperty Source

Less-than indent property

lteProp :: IndentProperty Source

Less-than or equal to indent property

notOpenBraces :: IdrisParser () Source

Checks that there are no braces that are not closed

accessibility :: IdrisParser Accessibility Source

Parses an accessibilty modifier (e.g. public, private)

addAcc :: Name -> Maybe Accessibility -> IdrisParser () Source

Adds accessibility option for function

accData :: Maybe Accessibility -> Name -> [Name] -> IdrisParser () Source

Add accessbility option for data declarations (works for classes too - abstract means the data/class is visible but members not)

Error reporting helpers

fixErrorMsg :: String -> [String] -> String Source

Error message with possible fixes list

collect :: [PDecl] -> [PDecl] Source

Collect PClauses with the same function name