Agda-2.5.1.2: A dependently typed functional programming language and proof assistant

Synopsis

data Parser a Source #

The parse monad. Equivalent to StateT ParseState (Either ParseError) except for the definition of fail, which builds a suitable ParseError object.

Instances

 Source # Methods(>>=) :: Parser a -> (a -> Parser b) -> Parser b #(>>) :: Parser a -> Parser b -> Parser b #return :: a -> Parser a #fail :: String -> Parser a # Source # Methodsfmap :: (a -> b) -> Parser a -> Parser b #(<\$) :: a -> Parser b -> Parser a # Source # Methodspure :: a -> Parser a #(<*>) :: Parser (a -> b) -> Parser a -> Parser b #(*>) :: Parser a -> Parser b -> Parser b #(<*) :: Parser a -> Parser b -> Parser a # Source # MethodscatchError :: Parser a -> (ParseError -> Parser a) -> Parser a # Source # Methodsput :: ParseState -> Parser () #state :: (ParseState -> (a, ParseState)) -> Parser a #

data ParseResult a Source #

The result of parsing something.

Constructors

 ParseOk ParseState a ParseFailed ParseError

The parser state. Contains everything the parser and the lexer could ever need.

Constructors

 PState FieldsparseSrcFile :: !SrcFile parsePos :: !PositionWithoutFileposition at current input locationparseLastPos :: !PositionWithoutFileposition of last tokenparseInp :: Stringthe current inputparsePrevChar :: !Charthe character before the inputparsePrevToken :: Stringthe previous tokenparseLayout :: [LayoutContext]the stack of layout contextsparseLexState :: [LexState]the state of the lexer (states can be nested so we need a stack)parseFlags :: ParseFlagscurrently there are no flags

Instances

 Source # MethodsshowList :: [ParseState] -> ShowS # Source # Methodsput :: ParseState -> Parser () #state :: (ParseState -> (a, ParseState)) -> Parser a #

What you get if parsing fails.

Constructors

 ParseError FieldserrSrcFile :: !SrcFileThe file in which the error occurred.errPos :: !PositionWithoutFileWhere the error occurred.errInput :: StringThe remaining input.errPrevToken :: StringThe previous token.errMsg :: StringHopefully an explanation of what happened.

Instances

 Source # MethodsshowList :: [ParseError] -> ShowS # Source # Methods Source # Methods Source # Methods Source # MethodscatchError :: Parser a -> (ParseError -> Parser a) -> Parser a #

type LexState = Int Source #

To do context sensitive lexing alex provides what is called start codes in the Alex documentation. It is really an integer representing the state of the lexer, so we call it LexState instead.

We need to keep track of the context to do layout. The context specifies the indentation (if any) of a layout block. See Agda.Syntax.Parser.Layout for more informaton.

Constructors

 NoLayout no layout Layout Int32 layout at specified column

Instances

 Source # MethodsshowList :: [LayoutContext] -> ShowS #

There aren't any parser flags at the moment.

Constructors

 ParseFlags FieldsparseKeepComments :: BoolShould comment tokens be returned by the lexer?

Instances

 Source # MethodsshowList :: [ParseFlags] -> ShowS #

# Running the parser

Constructs the initial state of the parser. The string argument is the input string, the file path is only there because it's part of a position.

The default flags.

parse :: ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a Source #

The most general way of parsing a string. The Agda.Syntax.Parser will define more specialised functions that supply the ParseFlags and the LexState.

parsePosString :: Position -> ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a Source #

The even more general way of parsing a string.

parseFile :: ParseFlags -> [LexState] -> Parser a -> AbsolutePath -> IO (ParseResult a) Source #

The most general way of parsing a file. The Agda.Syntax.Parser will define more specialised functions that supply the ParseFlags and the LexState.

Note that Agda source files always use the UTF-8 character encoding.

# Manipulating the state

The parse interval is between the last position and the current position.

## Layout

Return the current layout context.

Should only be used at the beginning of a file. When we start parsing we should be in layout mode. Instead of forcing zero indentation we use the indentation of the first token.

## Errors

parseError = fail

Fake a parse error at the specified position. Used, for instance, when lexing nested comments, which when failing will always fail at the end of the file. A more informative position is the beginning of the failing comment.

Use parseErrorAt or parseError as appropriate.

For lexical errors we want to report the current position as the site of the error, whereas for parse errors the previous position is the one we're interested in (since this will be the position of the token we just lexed). This function does parseErrorAt the current position.