Language.Fixpoint.Parse

Top Level Class for Parseable Values

class Inputable a where

Minimal complete definition

Nothing

Methods

rr :: String -> a

rr' :: String -> String -> a

Instances

Inputable Command

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> Command

rr' :: String -> String -> Command

Inputable Symbol

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> Symbol

rr' :: String -> String -> Symbol

Inputable Constant

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> Constant

rr' :: String -> String -> Constant

Inputable Expr

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> Expr

rr' :: String -> String -> Expr

Inputable (FInfo ())

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> FInfo ()

rr' :: String -> String -> FInfo ()

Inputable (FInfoWithOpts ())

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> FInfoWithOpts ()

rr' :: String -> String -> FInfoWithOpts ()

Inputable (FixResult Integer)

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> FixResult Integer

rr' :: String -> String -> FixResult Integer

Inputable [Command]

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> [Command]

rr' :: String -> String -> [Command]

Inputable (FixResult Integer, FixSolution)

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> (FixResult Integer, FixSolution)

rr' :: String -> String -> (FixResult Integer, FixSolution)

Top Level Class for Parseable Values

type Parser = StateT PState (Parsec Void String)

Some Important keyword and parsers

reserved :: String -> Parser ()

Parser that consumes the given reserved word.

The input token cannot be longer than the given name.

NOTE: we currently don't double-check that the reserved word is in the list of reserved words.

reservedOp :: String -> Parser ()

Parser that consumes the given reserved operator.

The input token cannot be longer than the given name.

NOTE: we currently don't double-check that the reserved operator is in the list of reserved operators.

locReserved :: String -> Parser (Located String)

parens :: Parser a -> Parser a

Parser that consumes the given symbol.

The difference with reservedOp is that the given symbol is seen as a token of its own, so the next character that follows does not matter.

symbol :: String -> Parser String symbol x = L.symbol spaces (string x)

brackets :: Parser a -> Parser a

Parser that consumes the given symbol.

The difference with reservedOp is that the given symbol is seen as a token of its own, so the next character that follows does not matter.

symbol :: String -> Parser String symbol x = L.symbol spaces (string x)

angles :: Parser a -> Parser a

Parser that consumes the given symbol.

The difference with reservedOp is that the given symbol is seen as a token of its own, so the next character that follows does not matter.

symbol :: String -> Parser String symbol x = L.symbol spaces (string x)

braces :: Parser a -> Parser a

Parser that consumes the given symbol.

The difference with reservedOp is that the given symbol is seen as a token of its own, so the next character that follows does not matter.

symbol :: String -> Parser String symbol x = L.symbol spaces (string x)

semi :: Parser String

comma :: Parser String

colon :: Parser String

dcolon :: Parser String

dot :: Parser String

pairP :: Parser a -> Parser z -> Parser b -> Parser (a, b)

stringLiteral :: Parser String

Parses a string literal as a lexeme. This is based on megaparsec's charLiteral parser, which claims to handle all the single-character escapes defined by the Haskell grammar.

locStringLiteral :: Parser (Located String)

Parsing basic entities

lowerIdP :: Parser Symbol

Lexeme version of lowerIdR.

upperIdP :: Parser Symbol

Lexeme version of upperIdR.

symbolP :: Parser Symbol

Unconstrained identifier, lower- or uppercase.

Must not be a reserved word.

Lexeme version of symbolR.

locSymbolP :: Parser LocSymbol

constantP :: Parser Constant

Parser for literal numeric constants: floats or integers without sign.

natural :: Parser Integer

Consumes a natural number literal lexeme, which can be in decimal, octal and hexadecimal representation.

This does not parse negative integers. Unary minus is available as an operator in the expression language.

locNatural :: Parser (Located Integer)

bindP :: Parser Symbol

Binder (lowerIdP <* colon)

sortP :: Parser Sort

Parser for sorts (types).

mkQual :: Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier

constructing qualifiers

infixSymbolP :: Parser Symbol

Parses any of the known infix operators.

locInfixSymbolP :: Parser (Located Symbol)

Located version of infixSymbolP.

Parsing recursive entities

exprP :: Parser Expr

Expressions

predP :: Parser Expr

Parses a predicate.

Unlike for expressions, there is a built-in operator list.

funAppP :: Parser Expr

Parser for function applications.

Andres, TODO: Why is this so complicated?

qualifierP :: Parser Sort -> Parser Qualifier

Parsing Qualifiers --------------------------------------------------------

Qualifiers

refaP :: Parser Expr

BareTypes -----------------------------------------------------------------

Refa

refP :: Parser (Reft -> a) -> Parser a

(Sorted) Refinements

refDefP :: Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a

(Sorted) Refinements with default binder

refBindP :: Parser Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a

(Sorted) Refinements with configurable sub-parsers

bvSortP :: Parser Sort

Bit-Vector Sort

defineP :: Parser Equation

matchP :: Parser Rewrite

Layout

indentedBlock :: Parser a -> Parser [a]

Parse a block delimited by layout. The block must be indented more than the surrounding blocks, otherwise we return an empty list.

Assumes that the parser for items does not accept the empty string.

indentedLine :: Parser a -> Parser a

Parse a single line that may be continued via layout.

indentedOrExplicitBlock :: Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]

Parse a block of items which can be delimited either via layout or via explicit delimiters as specified.

Assumes that the parser for items does not accept the empty string.

explicitBlock :: Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]

Parse a block of items that are delimited via explicit delimiters. Layout is disabled/reset for the scope of this block.

explicitCommaBlock :: Parser a -> Parser [a]

Parses a block with explicit braces and commas as separator. Used for record constructors in datatypes.

block :: Parser a -> Parser [a]

Parses a block via layout or explicit braces and semicolons.

Assumes that the parser for items does not accept the empty string.

However, even in layouted mode, we are allowing semicolons to separate block contents. We also allow semicolons at the beginning, end, and multiple subsequent semicolons, so the resulting parser provides the illusion of allowing empty items.

spaces :: Parser ()

Consumes all whitespace, including LH comments.

Should not be used directly, but primarily via lexeme.

The only "valid" use case for spaces is in top-level parsing function, to consume initial spaces.

setLayout :: Parser ()

Start a new layout block at the current indentation level.

popLayout :: Parser ()

Remove the topmost element from the layout stack.

Raw identifiers

condIdR :: Parser Char -> (Char -> Bool) -> (String -> Bool) -> String -> Parser Symbol

Raw (non-whitespace) parser for an identifier adhering to certain conditions.

The arguments are as follows, in order:

• the parser for the initial character,
• a predicate indicating which subsequent characters are ok,
• a check for the entire identifier to be applied in the end,
• an error message to display if the final check fails.

Lexemes and lexemes with location

lexeme :: Parser a -> Parser a

Indentation-aware lexeme parser. Before parsing, establishes whether we are in a position permitted by the layout stack. After the token, consume whitespace and potentially change state.

located :: Parser a -> Parser (Located a)

Make a parser location-aware.

This is at the cost of an imprecise span because we still consume spaces in the end first.

locLexeme :: Parser a -> Parser (Located a)

Indentation-aware located lexeme parser.

This is defined in such a way that it determines the actual source range covered by the identifier. I.e., it consumes additional whitespace in the end, but that is not part of the source range reported for the identifier.

locLowerIdP :: Parser LocSymbol

locUpperIdP :: Parser LocSymbol

Getting a Fresh Integer while parsing

freshIntP :: Parser Integer

Obtain a fresh integer during the parsing process.

Parsing Function

doParse' :: Parser a -> SourceName -> String -> a

Entry point for parsing, for testing.

Take the top-level parser, the source file name, and the input as a string. Fails with an exception on a parse error.

parseTest' :: Show a => Parser a -> String -> IO ()

Function to test parsers interactively.

parseFromFile :: Parser b -> SourceName -> IO b

parseFromStdIn :: Parser a -> IO a

remainderP :: Parser a -> Parser (a, String, SourcePos)

Parse via the given parser, and obtain the rest of the input as well as the final source position.

Utilities

isSmall :: Char -> Bool

Predicate version to check if the characer is a valid initial character for lowerIdR.

TODO: What is this needed for?

isNotReserved :: String -> Bool

initPState :: Maybe Expr -> PState

Initial parser state.

data PState

The parser state.

We keep track of the fixities of infix operators.

We also keep track of whether empty list and singleton lists syntax is allowed (and how they are to be interpreted, if they are).

We also keep track of an integer counter that can be used to supply unique integers during the parsing process.

Finally, we keep track of the layout stack.

Constructors

PState

Fields

• fixityTable :: OpTable
• fixityOps :: [Fixity]
• empList :: Maybe Expr
• singList :: Maybe (Expr -> Expr)
• supply :: !Integer
• layoutStack :: LayoutStack

data LayoutStack

The layout stack tracks columns at which layout blocks have started.

Constructors

Empty

no layout info

Reset LayoutStack

in a block not using layout

At Pos LayoutStack

in a block at the given column

After Pos LayoutStack

past a block at the given column

Instances

Show LayoutStack

Defined in Language.Fixpoint.Parse

Methods

showsPrec :: Int -> LayoutStack -> ShowS

show :: LayoutStack -> String

showList :: [LayoutStack] -> ShowS

data Fixity

Constructors

FInfix

Fields

• fpred :: Maybe Int
• fname :: String
• fop2 :: Maybe (Expr -> Expr -> Expr)
• fassoc :: Assoc

FPrefix

Fields

• fpred :: Maybe Int
• fname :: String
• fop1 :: Maybe (Expr -> Expr)

FPostfix

Fields

• fpred :: Maybe Int
• fname :: String
• fop1 :: Maybe (Expr -> Expr)

data Assoc

Constructors

AssocNone

AssocLeft

AssocRight

addOperatorP :: Fixity -> Parser ()

Add an operator to the parsing state.

For testing

expr0P :: Parser Expr

Parser for "atomic" expressions.

This parser is reused by Liquid Haskell.

dataFieldP :: Parser DataField

Parsing Data Declarations -------------------------------------------------

dataCtorP :: Parser DataCtor

dataDeclP :: Parser DataDecl