Language.Fixpoint.Parse

Top Level Class for Parseable Values

class Inputable a where

Minimal complete definition

Nothing

Methods

rr :: String -> a

rr' :: String -> String -> a

Instances

Inputable Symbol

Inputable Refa

Inputable Pred

Inputable Expr

Inputable Constant

Inputable Command

Inputable [Command]

Inputable (FInfo ())

Inputable (FixResult Integer)

Inputable (FixResult Integer, FixSolution)

Top Level Class for Parseable Values

type Parser = Parsec String Integer

Lexer to add new tokens

lexer :: GenTokenParser String u Identity

Some Important keyword and parsers

reserved :: String -> ParsecT String u Identity ()

reservedOp :: String -> ParsecT String u Identity ()

parens :: ParsecT String u Identity a -> ParsecT String u Identity a

brackets :: ParsecT String u Identity a -> ParsecT String u Identity a

angles :: ParsecT String u Identity a -> ParsecT String u Identity a

braces :: ParsecT String u Identity a -> ParsecT String u Identity a

semi :: ParsecT String u Identity String

comma :: ParsecT String u Identity String

colon :: ParsecT String u Identity String

dcolon :: Stream s m Char => ParsecT s u m String

whiteSpace :: ParsecT String u Identity ()

blanks :: Stream s m Char => ParsecT s u m [Char]

Parsing basic entities

lowerIdP :: Parser Symbol

upperIdP :: Parser Symbol

symbolP :: Parser Symbol

constantP :: Parser Constant

integer :: Stream s m Char => ParsecT s u m Integer

bindP :: ParsecT String Integer Identity Symbol

mkQual :: Symbol -> [(Symbol, Sort)] -> Pred -> SourcePos -> Qualifier

Parsing recursive entities

exprP :: Parser Expr

predP :: Parser Pred

funAppP :: ParsecT String Integer Identity Expr

qualifierP :: ParsecT String Integer Identity Sort -> ParsecT String Integer Identity Qualifier

Parsing Qualifiers ---------------------------------------------

refaP :: Parser Refa

refP :: Parser (Reft -> a) -> Parser a

refDefP :: Symbol -> Parser Refa -> Parser (Reft -> a) -> Parser a

refBindP :: Parser Symbol -> Parser Refa -> Parser (Reft -> a) -> Parser a

bvSortP :: ParsecT String u Identity Sort

Some Combinators

condIdP :: [Char] -> (String -> Bool) -> Parser Symbol

Add a Location to a parsed value

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

locLowerIdP :: Parser (Located Symbol)

locUpperIdP :: Parser (Located Symbol)

Getting a Fresh Integer while parsing

freshIntP :: Parser Integer

Parsing Function

doParse' :: Num u => ParsecT String u Identity a -> SourceName -> String -> a

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

remainderP :: Monad m => ParsecT t1 u m t -> ParsecT t1 u m (t, t1, SourcePos)