liquid-fixpoint-0.9.2.5: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Fixpoint.Parse

Synopsis

Top Level Class for Parseable Values

class Inputable a where Source #

Minimal complete definition

Nothing

Methods

rr :: String -> a Source #

rr' :: String -> String -> a Source #

Instances

Instances details
Inputable Command Source # 
Instance details

Defined in Language.Fixpoint.Parse

Inputable Symbol Source # 
Instance details

Defined in Language.Fixpoint.Parse

Inputable Constant Source # 
Instance details

Defined in Language.Fixpoint.Parse

Inputable Expr Source # 
Instance details

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> Expr Source #

rr' :: String -> String -> Expr Source #

Inputable (FInfo ()) Source # 
Instance details

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> FInfo () Source #

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

Inputable (FInfoWithOpts ()) Source # 
Instance details

Defined in Language.Fixpoint.Parse

Inputable (FixResult Integer) Source # 
Instance details

Defined in Language.Fixpoint.Parse

Inputable [Command] Source # 
Instance details

Defined in Language.Fixpoint.Parse

Methods

rr :: String -> [Command] Source #

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

Inputable (FixResult Integer, FixSolution) Source # 
Instance details

Defined in Language.Fixpoint.Parse

Top Level Class for Parseable Values

Some Important keyword and parsers

reserved :: String -> Parser () Source #

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

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.

parens :: Parser a -> Parser a Source #

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 Source #

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 Source #

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 Source #

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)

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

stringLiteral :: Parser String Source #

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.

Parsing basic entities

lowerIdP :: Parser Symbol Source #

Lexeme version of lowerIdR.

upperIdP :: Parser Symbol Source #

Lexeme version of upperIdR.

symbolP :: Parser Symbol Source #

Unconstrained identifier, lower- or uppercase.

Must not be a reserved word.

Lexeme version of symbolR.

constantP :: Parser Constant Source #

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

natural :: Parser Integer Source #

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.

bindP :: Parser Symbol Source #

Binder (lowerIdP <* colon)

sortP :: Parser Sort Source #

Parser for sorts (types).

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

constructing qualifiers

infixSymbolP :: Parser Symbol Source #

Parses any of the known infix operators.

Parsing recursive entities

exprP :: Parser Expr Source #

Expressions

predP :: Parser Expr Source #

Parses a predicate.

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

funAppP :: Parser Expr Source #

Parser for function applications.

Andres, TODO: Why is this so complicated?

qualifierP :: Parser Sort -> Parser Qualifier Source #

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

Qualifiers

refaP :: Parser Expr Source #

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

Refa

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

(Sorted) Refinements

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

(Sorted) Refinements with default binder

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

(Sorted) Refinements with configurable sub-parsers

Layout

indentedBlock :: Parser a -> Parser [a] Source #

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 Source #

Parse a single line that may be continued via layout.

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

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] Source #

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] Source #

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

block :: Parser a -> Parser [a] Source #

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

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

Start a new layout block at the current indentation level.

popLayout :: Parser () Source #

Remove the topmost element from the layout stack.

Raw identifiers

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

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 Source #

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) Source #

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) Source #

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.

Getting a Fresh Integer while parsing

freshIntP :: Parser Integer Source #

Obtain a fresh integer during the parsing process.

Parsing Function

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

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

Function to test parsers interactively.

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

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

Utilities

isSmall :: Char -> Bool Source #

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

TODO: What is this needed for?

initPState :: Maybe Expr -> PState Source #

Initial parser state.

data PState Source #

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 

data LayoutStack Source #

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

Instances details
Show LayoutStack Source # 
Instance details

Defined in Language.Fixpoint.Parse

data Fixity Source #

Constructors

FInfix 

Fields

FPrefix 

Fields

FPostfix 

Fields

addOperatorP :: Fixity -> Parser () Source #

Add an operator to the parsing state.

addNumTyCon :: Symbol -> Parser () Source #

Add a new numeric FTyCon (symbol) to the parsing state.

For testing

expr0P :: Parser Expr Source #

Parser for "atomic" expressions.

This parser is reused by Liquid Haskell.

dataFieldP :: Parser DataField Source #

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