idris-0.12.3: Functional Programming Language with Dependent Types

CopyrightLicense : BSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell98

Idris.Parser.Helpers

Contents

Description

 

Synopsis

Documentation

type IdrisParser = StateT IState IdrisInnerParser Source #

Idris parser with state used during parsing

newtype IdrisInnerParser a Source #

Constructors

IdrisInnerParser 

Fields

Instances

Monad IdrisInnerParser Source # 
Functor IdrisInnerParser Source # 

Methods

fmap :: (a -> b) -> IdrisInnerParser a -> IdrisInnerParser b #

(<$) :: a -> IdrisInnerParser b -> IdrisInnerParser a #

Applicative IdrisInnerParser Source # 
Alternative IdrisInnerParser Source # 
MonadPlus IdrisInnerParser Source # 
TokenParsing IdrisInnerParser Source # 
TokenParsing IdrisParser Source # 
CharParsing IdrisInnerParser Source # 
LookAheadParsing IdrisInnerParser Source # 
Parsing IdrisInnerParser Source # 
DeltaParsing IdrisInnerParser Source # 
DeltaParsing IdrisParser Source # 
HasLastTokenSpan IdrisParser Source # 
MarkParsing Delta IdrisInnerParser Source # 
Monoid a => Monoid (IdrisInnerParser a) Source # 

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

Generalized monadic parsing constraint type

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

Helper to run Idris inner parser based stateT parsers

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

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

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

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.

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 -> Accessibility -> IdrisParser () Source #

Adds accessibility option for function

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

Add accessbility option for data declarations (works for interfaces too - abstract means the data/interface 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