PAKCS
Exported names: Imported modules:

Module XFD.SMTLib.NDParser

This module implements a parser for programs and formulas in the SMT-LIB2 syntax. It is based on the system library Parser which defines functional logic parsing combinators.

Summary of exported operations:

parse :: String -> Either String CmdResponse   
parseCmdResult :: CmdResponse -> [Token] -> [Token]   
parseCmdCheckSatResponse :: CmdResponse -> [Token] -> [Token]   
parseCheckSatResponse :: CheckSatResponse -> [Token] -> [Token]   
parseCmdGetValueResponse :: CmdResponse -> [Token] -> [Token]   
parseGetValueResponse :: [ValuationPair] -> [Token] -> [Token]   
parseValuePair :: ValuationPair -> [Token] -> [Token]   
parseTerm :: Term -> [Token] -> [Token]   
parseTSPC :: Term -> [Token] -> [Token]   
parseTQId :: Term -> [Token] -> [Token]   
parseCmdGenResponse :: CmdResponse -> [Token] -> [Token]   
parseGenResponse :: GenResponse -> [Token] -> [Token]   
parseErrorResponse :: GenResponse -> [Token] -> [Token]   
parseString :: String -> [Token] -> [Token]   
mStar :: (() -> a -> [b] -> [b]) -> [a] -> [b] -> [b]   
mSome :: (() -> a -> [b] -> [b]) -> [a] -> [b] -> [b]   
parseCmdGetModelResponse :: CmdResponse -> [Token] -> [Token]   
parseGetModelResponse :: [ModelResponse] -> [Token] -> [Token]   
parseModelResponse :: ModelResponse -> [Token] -> [Token]   
parseFunDef :: FunDef -> [Token] -> [Token]   

Exported datatypes:

ParseError

Type synonym: ParseError = String

Exported operations:

parse :: String -> Either String CmdResponse   

parseCmdResult :: CmdResponse -> [Token] -> [Token]   

parseTerm :: Term -> [Token] -> [Token]   

parseTSPC :: Term -> [Token] -> [Token]   

parseTQId :: Term -> [Token] -> [Token]   

parseString :: String -> [Token] -> [Token]   

mStar :: (() -> a -> [b] -> [b]) -> [a] -> [b] -> [b]   

mSome :: (() -> a -> [b] -> [b]) -> [a] -> [b] -> [b]   

parseFunDef :: FunDef -> [Token] -> [Token]