Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Parse

Contents

Top Level Class for Parseable Values
Top Level Class for Parseable Values
Lexer to add new tokens
Some Important keyword and parsers
Parsing basic entities
Parsing recursive entities
Some Combinators
Add a Location to a parsed value
Getting a Fresh Integer while parsing
Parsing Function
Utilities
For testing

Synopsis

class Inputable a where
- rr :: String -> a
- rr' :: String -> String -> a
type Parser = ParsecT String Integer (State PState)
lexer :: Monad m => GenTokenParser String u m
reserved :: String -> Parser ()
reservedOp :: String -> Parser ()
parens :: ParserT u a -> ParserT u a
brackets :: ParserT u a -> ParserT u a
angles :: ParserT u a -> ParserT u a
braces :: ParserT u a -> ParserT u a
semi :: Parser String
comma :: Parser String
colon :: Parser String
dcolon :: Parser String
whiteSpace :: Parser ()
blanks :: Parser String
pairP :: Parser a -> Parser z -> Parser b -> Parser (a, b)
stringLiteral :: Parser String
lowerIdP :: Parser Symbol
upperIdP :: Parser Symbol
infixIdP :: Parser String
symbolP :: Parser Symbol
constantP :: Parser Constant
integer :: Parser Integer
bindP :: Parser Symbol
sortP :: Parser Sort
mkQual :: Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
infixSymbolP :: Parser 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
bvSortP :: Parser Sort
condIdP :: Parser Char -> HashSet Char -> (String -> Bool) -> Parser Symbol
locParserP :: Parser a -> Parser (Located a)
locLowerIdP :: Parser LocSymbol
locUpperIdP :: Parser LocSymbol
freshIntP :: Parser Integer
doParse' :: Parser a -> SourceName -> String -> a
parseFromFile :: Parser b -> SourceName -> IO b
remainderP :: Parser a -> Parser (a, String, SourcePos)
isSmall :: Char -> Bool
isNotReserved :: String -> Bool
initPState :: Maybe Expr -> PState
data PState = PState {
- fixityTable :: OpTable
- fixityOps :: [Fixity]
- empList :: Maybe Expr
- singList :: Maybe (Expr -> Expr)
}
data Fixity
- = FInfix {
  - fpred :: Maybe Int
  - fname :: String
  - fop2 :: Maybe (Expr -> Expr -> Expr)
  - fassoc :: Assoc
  }
- | FPrefix {
  - fpred :: Maybe Int
  - fname :: String
  - fop1 :: Maybe (Expr -> Expr)
  }
- | FPostfix {
  - fpred :: Maybe Int
  - fname :: String
  - fop1 :: Maybe (Expr -> Expr)
  }
data Assoc
- = AssocNone
- | AssocLeft
- | AssocRight
addOperatorP :: Fixity -> 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

Methods

rr :: String -> a Source #

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

Instances

Inputable Symbol Source #
Instance details Defined in Language.Fixpoint.Parse Methods rr :: String -> Symbol Source # rr' :: String -> String -> Symbol Source #
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 Methods rr :: String -> Constant Source # rr' :: String -> String -> Constant Source #
Inputable Command Source #
Instance details Defined in Language.Fixpoint.Parse Methods rr :: String -> Command Source # rr' :: String -> String -> Command Source #
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 Methods rr :: String -> FixResult Integer Source # rr' :: String -> String -> FixResult Integer 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 Methods rr :: String -> FInfoWithOpts () Source # rr' :: String -> String -> FInfoWithOpts () Source #
Inputable (FixResult Integer, FixSolution) Source #
Instance details Defined in Language.Fixpoint.Parse Methods rr :: String -> (FixResult Integer, FixSolution) Source # rr' :: String -> String -> (FixResult Integer, FixSolution) Source #

Top Level Class for Parseable Values

type Parser = ParsecT String Integer (State PState) Source #

Lexer to add new tokens

lexer :: Monad m => GenTokenParser String u m Source #

Some Important keyword and parsers

reserved :: String -> Parser () Source #

reservedOp :: String -> Parser () Source #

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 #

semi :: Parser String Source #

comma :: Parser String Source #

colon :: Parser String Source #

dcolon :: Parser String Source #

whiteSpace :: Parser () Source #

blanks :: Parser String Source #

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

stringLiteral :: Parser String Source #

Parsing basic entities

lowerIdP :: Parser Symbol Source #

upperIdP :: Parser Symbol Source #

infixIdP :: Parser String Source #

String Haskell infix Id

symbolP :: Parser Symbol Source #

Arbitrary Symbols

constantP :: Parser Constant Source #

(Integer) Constants

integer :: Parser Integer Source #

Integer

bindP :: Parser Symbol Source #

Binder (lowerIdP <* colon)

sortP :: Parser Sort Source #

Sort

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

constructing qualifiers

infixSymbolP :: Parser Symbol Source #

Parsing recursive entities

exprP :: Parser Expr Source #

Expressions

predP :: Parser Expr Source #

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

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

Add a Location to a parsed value

locParserP :: Parser a -> Parser (Located a) Source #

locLowerIdP :: Parser LocSymbol Source #

locUpperIdP :: Parser LocSymbol Source #

Getting a Fresh Integer while parsing

freshIntP :: Parser Integer Source #

Parsing Function

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

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

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

Utilities

isSmall :: Char -> Bool Source #

isNotReserved :: String -> Bool Source #

initPState :: Maybe Expr -> PState Source #

data PState Source #

Constructors

PState
Fields fixityTable :: OpTable fixityOps :: [Fixity] empList :: Maybe Expr singList :: Maybe (Expr -> Expr)

data Fixity Source #

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 #

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

Constructors

AssocNone
AssocLeft
AssocRight

addOperatorP :: Fixity -> Parser () Source #

For testing

expr0P :: Parser Expr Source #

dataFieldP :: Parser DataField Source #

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

dataCtorP :: Parser DataCtor Source #

dataDeclP :: Parser DataDecl Source #