| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Parse
Contents
Synopsis
- class Inputable a where
- 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 {}
- data Fixity
- data Assoc
- 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
Instances
| Inputable Symbol Source # | |
| Inputable Expr Source # | |
| Inputable Constant Source # | |
| Inputable Command Source # | |
| Inputable [Command] Source # | |
| Inputable (FixResult Integer) Source # | |
| Inputable (FInfo ()) Source # | |
| Inputable (FInfoWithOpts ()) Source # | |
Defined in Language.Fixpoint.Parse | |
| Inputable (FixResult Integer, FixSolution) Source # | |
Top Level Class for Parseable Values
Lexer to add new tokens
Some Important keyword and parsers
reservedOp :: String -> Parser () Source #
whiteSpace :: Parser () Source #
Parsing basic entities
Parsing recursive entities
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
Some Combinators
Add a Location to a parsed value
Getting a Fresh Integer while parsing
Parsing Function
parseFromFile :: Parser b -> SourceName -> IO b Source #
Utilities
isNotReserved :: String -> Bool Source #
This data type specifies the associativity of operators: left, right or none.
Constructors
| AssocNone | |
| AssocLeft | |
| AssocRight |
addOperatorP :: Fixity -> Parser () Source #
For testing
dataFieldP :: Parser DataField Source #
Parsing Data Declarations -------------------------------------------------