liquid-fixpoint-0.7.0.2: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Parse

Contents

Synopsis

Top Level Class for Parseable Values

Top Level Class for Parseable Values

Lexer to add new tokens

Some Important keyword and parsers

parens :: ParserT u a -> ParserT u a Source #

brackets :: ParserT u a -> ParserT u a Source #

angles :: ParserT u a -> ParserT u a Source #

braces :: ParserT u a -> ParserT u a Source #

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

Parsing basic entities

lowerIdP :: Parser Symbol Source #

Lower-case identifiers

upperIdP :: Parser Symbol Source #

Lower-case identifiers

infixIdP :: Parser String Source #

String Haskell infix Id

symbolP :: Parser Symbol Source #

Arbitrary Symbols

constantP :: Parser Constant Source #

(Integer) Constants

bindP :: Parser Symbol Source #

Binder (lowerIdP <* colon)

mkQual :: Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier Source #

constructing qualifiers

Parsing recursive entities

exprP :: Parser Expr Source #

Expressions

funAppP :: Parser Expr Source #

Function Applications

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

bvSortP :: Parser Sort Source #

Bit-Vector Sort

Some Combinators

Add a Location to a parsed value

Getting a Fresh Integer while parsing

Parsing Function

Utilities

data Fixity Source #

Constructors

FInfix 

Fields

FPrefix 

Fields

FPostfix 

Fields

data Assoc :: * #

This data type specifies the associativity of operators: left, right or none.

For testing

dataFieldP :: Parser DataField Source #

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