| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Parse
Synopsis
- class Inputable a where
- type Parser = StateT PState (Parsec Void String)
- reserved :: String -> Parser ()
- reservedOp :: String -> Parser ()
- locReserved :: String -> Parser (Located String)
- parens :: Parser a -> Parser a
- brackets :: Parser a -> Parser a
- angles :: Parser a -> Parser a
- braces :: Parser a -> Parser a
- 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
- locStringLiteral :: Parser (Located String)
- lowerIdP :: Parser Symbol
- upperIdP :: Parser Symbol
- symbolP :: Parser Symbol
- locSymbolP :: Parser LocSymbol
- constantP :: Parser Constant
- natural :: Parser Integer
- locNatural :: Parser (Located Integer)
- bindP :: Parser Symbol
- sortP :: Parser Sort
- mkQual :: Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
- infixSymbolP :: Parser Symbol
- locInfixSymbolP :: Parser (Located Symbol)
- exprP :: Parser Expr
- predP :: Parser Expr
- funAppP :: Parser Expr
- qualifierP :: Parser Sort -> Parser Qualifier
- refaP :: Parser Expr
- refP :: Parser (Reft -> a) -> Parser a
- refDefP :: Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
- refBindP :: Parser Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
- defineP :: Parser Equation
- matchP :: Parser Rewrite
- indentedBlock :: Parser a -> Parser [a]
- indentedLine :: Parser a -> Parser a
- indentedOrExplicitBlock :: Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
- explicitBlock :: Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
- explicitCommaBlock :: Parser a -> Parser [a]
- block :: Parser a -> Parser [a]
- spaces :: Parser ()
- setLayout :: Parser ()
- popLayout :: Parser ()
- condIdR :: Parser Char -> (Char -> Bool) -> (String -> Bool) -> String -> Parser Symbol
- lexeme :: Parser a -> Parser a
- located :: Parser a -> Parser (Located a)
- locLexeme :: Parser a -> Parser (Located a)
- locLowerIdP :: Parser LocSymbol
- locUpperIdP :: Parser LocSymbol
- freshIntP :: Parser Integer
- doParse' :: Parser a -> SourceName -> String -> a
- parseTest' :: Show a => Parser a -> String -> IO ()
- parseFromFile :: Parser b -> SourceName -> IO b
- parseFromStdIn :: Parser a -> IO a
- remainderP :: Parser a -> Parser (a, String, SourcePos)
- isSmall :: Char -> Bool
- isNotReserved :: String -> Bool
- initPState :: Maybe Expr -> PState
- data PState = PState {}
- data LayoutStack
- data Fixity
- data Assoc
- addOperatorP :: Fixity -> Parser ()
- addNumTyCon :: Symbol -> Parser ()
- expr0P :: Parser Expr
- dataFieldP :: Parser DataField
- dataCtorP :: Parser DataCtor
- dataDeclP :: Parser DataDecl
Top Level Class for Parseable Values
class Inputable a where Source #
Minimal complete definition
Nothing
Instances
| Inputable Command Source # | |
| Inputable Symbol Source # | |
| Inputable Constant Source # | |
| Inputable Expr Source # | |
| Inputable (FInfo ()) Source # | |
| Inputable (FInfoWithOpts ()) Source # | |
Defined in Language.Fixpoint.Parse | |
| Inputable (FixResult Integer) Source # | |
| Inputable [Command] Source # | |
| Inputable (FixResult Integer, FixSolution) Source # | |
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)
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
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.
infixSymbolP :: Parser Symbol Source #
Parses any of the known infix operators.
locInfixSymbolP :: Parser (Located Symbol) Source #
Located version of infixSymbolP.
Parsing recursive entities
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
BareTypes -----------------------------------------------------------------
Refa
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.
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.
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
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.
parseFromFile :: Parser b -> SourceName -> IO b Source #
parseFromStdIn :: Parser a -> IO a Source #
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?
isNotReserved :: String -> Bool 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.
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
| Show LayoutStack Source # | |
Defined in Language.Fixpoint.Parse Methods showsPrec :: Int -> LayoutStack -> ShowS # show :: LayoutStack -> String # showList :: [LayoutStack] -> ShowS # | |
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 -------------------------------------------------