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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Parse

Contents

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
Inputable Symbol 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 Constant Source # 
Instance details

Defined in Language.Fixpoint.Parse

Inputable Command 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) Source # 
Instance details

Defined in Language.Fixpoint.Parse

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, FixSolution) Source # 
Instance details

Defined in Language.Fixpoint.Parse

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

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 -> [QualParam] -> 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 PState Source #

Constructors

PState 

Fields

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