module Smtlib.Parsers.CommonParsers where
import Control.Applicative as Ctr hiding ((<|>))
import Data.Functor.Identity
import Text.Parsec.Prim as Prim
import Text.ParserCombinators.Parsec as Pc
import Smtlib.Syntax.Syntax
import Control.Monad
(<:>) :: Applicative f => f a -> f [a] -> f [a]
(<:>) a b = (:) <$> a <*> b
(<++>) :: Applicative f => f [a] -> f [a] -> f [a]
(<++>) a b = (++) <$> a <*> b
parseBool :: ParsecT String u Identity Bool
parseBool = (true *> return True) <|> (false *> return False)
numeral :: ParsecT String u Identity String
numeral = many1 digit
num :: ParsecT String u Identity String
num = Pc.many digit
decimal :: ParsecT String u Identity String
decimal = numeral <++> dot <++> Pc.try zeros <++> num
zeros :: ParsecT String u Identity String
zeros = Pc.many $ char '0'
dot :: ParsecT String u Identity String
dot = string "."
hexadecimal :: ParsecT String u Identity String
hexadecimal = string "#x" *> many1 hexDigit
binary :: ParsecT String u Identity String
binary = string "#b" *> many1 bin
bin :: ParsecT String u Identity Char
bin = char '0' <|> char '1'
str :: ParsecT String u Identity String
str = string "\"" <++> Pc.many strChar <++> string "\""
strChar :: ParsecT String u Identity Char
strChar = alphaNum
<|> char ' '
<|> char ':'
<|> char ','
symbol :: ParsecT String u Identity String
symbol = simpleSymbol <|> quotedSymbol
quotedSymbol :: ParsecT String u Identity String
quotedSymbol = char '|' *> Pc.many (noneOf "|") <* char '|'
simpleSymbol :: ParsecT String u Identity String
simpleSymbol = (letter <|> spcSymb) <:> sq
where sq = Pc.many (alphaNum <|> spcSymb)
spcSymb :: ParsecT String u Identity Char
spcSymb = oneOf "+-/*=%?!.$_~^&<>@"
keyword :: ParsecT String u Identity String
keyword = char ':' <:> Pc.many (alphaNum<|> spcSymb)
aspO :: ParsecT String u Identity Char
aspO = char '('
aspC :: ParsecT String u Identity Char
aspC = char ')'
aspUS :: ParsecT String u Identity Char
aspUS = char '_'
true :: ParsecT String u Identity String
true = string "true"
false :: ParsecT String u Identity String
false = string "false"
emptySpace :: ParsecT String u Identity String
emptySpace = Pc.try $ Pc.many $
char ' ' <|> char '\n' <|> char '\t' <|> char '\r'
reservedWords :: ParsecT String u Identity String
reservedWords = string "let"
<|> string "par"
<|> string "_"
<|> string "!"
<|> string "as"
<|> string "forall"
<|> string "exists"
<|> string "NUMERAL"
<|> string "DECIMAL"
<|> string "STRING"
parseTerm :: ParsecT String u Identity Term
parseTerm = parseTSPC
<|> Pc.try parseTQID
<|> Pc.try parseTQIT
<|> Pc.try parseTermLet
<|> Pc.try parseTermFA
<|> Pc.try parseTermEX
<|> parseTermAnnot
parseTSPC :: ParsecT String u Identity Term
parseTSPC = liftM TermSpecConstant parseSpecConstant
parseTQID :: ParsecT String u Identity Term
parseTQID = liftM TermQualIdentifier parseQualIdentifier
parseTQIT :: ParsecT String u Identity Term
parseTQIT = do
_ <- aspO
_ <- emptySpace
iden <- parseQualIdentifier
_ <- emptySpace
terms <- Pc.many $ parseTerm <* Pc.try emptySpace
_ <- aspC
return $ TermQualIdentifierT iden terms
parseTermLet :: ParsecT String u Identity Term
parseTermLet = do
_ <- aspO
_ <- emptySpace
_ <- string "let"
_ <- emptySpace
_ <- aspO
_ <- emptySpace
vb <- Pc.many $ parseVarBinding <* Pc.try emptySpace
_ <- aspC
_ <- emptySpace
term <- parseTerm
_ <- emptySpace
_ <- aspC
return $ TermLet vb term
parseTermFA :: ParsecT String u Identity Term
parseTermFA = do
_ <- aspO
_ <- emptySpace
_ <- string "forall"
_ <- emptySpace
_ <- aspO
sv <- Pc.many $ parseSortedVar <* Pc.try emptySpace
_ <- aspC
_ <- emptySpace
term <- parseTerm
_ <- emptySpace
_ <- aspC
return $ TermForall sv term
parseTermEX :: ParsecT String u Identity Term
parseTermEX = do
_ <- aspO
_ <- emptySpace
_ <- string "exists"
_ <- emptySpace
_ <- aspO
sv <- Pc.many $ parseSortedVar <* Pc.try emptySpace
_ <- aspC
_ <- emptySpace
term <- parseTerm
_ <- emptySpace
_ <- aspC
return $ TermExists sv term
parseTermAnnot :: ParsecT String u Identity Term
parseTermAnnot = do
_ <- aspO
_ <- emptySpace
_ <- char '!'
_ <- emptySpace
term <- parseTerm
_ <- emptySpace
attr <- Pc.many $ parseAttribute <* Pc.try emptySpace
_ <- aspC
return $ TermAnnot term attr
parseSortedVar :: ParsecT String u Identity SortedVar
parseSortedVar = do
_ <- aspO
_ <- emptySpace
symb <- symbol
_ <- emptySpace
sort <- parseSort
_ <- emptySpace
_ <- aspC
return $ SV symb sort
parseQualIdentifier :: ParsecT String u Identity QualIdentifier
parseQualIdentifier = Pc.try parseQID <|> parseQIAs
parseQID :: ParsecT String u Identity QualIdentifier
parseQID = liftM QIdentifier parseIdentifier
parseQIAs :: ParsecT String u Identity QualIdentifier
parseQIAs = do
_ <- aspO
_ <- emptySpace
_ <- string "as"
_ <- emptySpace
ident <- parseIdentifier
_ <- emptySpace
sort <- parseSort
_ <- emptySpace
_ <- aspC
return $ QIdentifierAs ident sort
parseVarBinding :: ParsecT String u Identity VarBinding
parseVarBinding = do
_ <- aspO
_ <- emptySpace
symb <- symbol
_ <- emptySpace
term <- parseTerm
_ <- emptySpace
_ <- aspC
return $ VB symb term
parseAttributeValue :: ParsecT String u Identity AttrValue
parseAttributeValue = parseAVSC <|> parseAVS <|> parseAVSexpr
parseAVSC :: ParsecT String u Identity AttrValue
parseAVSC = liftM AttrValueConstant parseSpecConstant
parseAVS :: ParsecT String u Identity AttrValue
parseAVS = liftM AttrValueSymbol symbol
parseAVSexpr :: ParsecT String u Identity AttrValue
parseAVSexpr = do
_ <- aspO
_ <- emptySpace
expr <- Pc.many $ parseSexpr <* Pc.try emptySpace
_ <- aspC
return $ AttrValueSexpr expr
parseAttribute :: ParsecT String u Identity Attribute
parseAttribute = Pc.try parseKeyAttAttribute <|> parseKeyAttribute
parseKeyAttribute :: ParsecT String u Identity Attribute
parseKeyAttribute = liftM Attribute keyword
parseKeyAttAttribute :: ParsecT String u Identity Attribute
parseKeyAttAttribute = do
kw <- keyword
_ <- emptySpace
atr <- parseAttributeValue
return $ AttributeVal kw atr
parseSort :: ParsecT String u Identity Sort
parseSort = Pc.try parseIdentifierS <|> parseIdentifierSort
parseIdentifierS :: ParsecT String u Identity Sort
parseIdentifierS = liftM SortId parseIdentifier
parseIdentifierSort :: ParsecT String u Identity Sort
parseIdentifierSort = do
_ <- aspO
_ <- emptySpace
identifier <- parseIdentifier
_ <- emptySpace
sorts <- many1 (parseSort <* Pc.try emptySpace)
_ <- aspC
return $ SortIdentifiers identifier sorts
parseIdentifier :: ParsecT String u Identity Identifier
parseIdentifier = parseOnlySymbol <|> parseNSymbol
parseOnlySymbol :: ParsecT String u Identity Identifier
parseOnlySymbol = liftM ISymbol symbol
parseNSymbol :: ParsecT String u Identity Identifier
parseNSymbol = do
_ <- aspO
_ <- emptySpace
_ <- aspUS
_ <- emptySpace
symb <- symbol
_ <- emptySpace
nume <- many1 (numeral <* Pc.try spaces)
_ <- aspC
return $ I_Symbol symb (fmap (read) nume)
parseSexprConstant :: ParsecT String u Identity Sexpr
parseSexprConstant = liftM SexprSpecConstant parseSpecConstant
parseSexprSymbol :: ParsecT String u Identity Sexpr
parseSexprSymbol = liftM SexprSymbol symbol
parseSexprKeyword :: ParsecT String u Identity Sexpr
parseSexprKeyword = liftM SexprSymbol keyword
parseAtomSexpr :: ParsecT String u Identity Sexpr
parseAtomSexpr = parseSexprConstant
<|> parseSexprSymbol
<|> parseSexprKeyword
parseListSexpr :: ParsecT String u Identity Sexpr
parseListSexpr = do
_ <- aspO
list <- Pc.many parseSexpr
_ <- aspC
return $ SexprSxp list
parseSexpr :: ParsecT String u Identity Sexpr
parseSexpr = do
_ <- emptySpace
expr <- parseAtomSexpr <|> parseListSexpr
_ <- emptySpace
return expr
parseSpecConstant :: ParsecT String u Identity SpecConstant
parseSpecConstant = Pc.try parseDecimal
<|> parseNumeral
<|> Pc.try parseHexadecimal
<|> parseBinary
<|> parseString
parseNumeral :: ParsecT String u Identity SpecConstant
parseNumeral = liftM SpecConstantNumeral (read <$> numeral)
parseDecimal :: ParsecT String u Identity SpecConstant
parseDecimal = liftM SpecConstantDecimal decimal
parseHexadecimal :: ParsecT String u Identity SpecConstant
parseHexadecimal = liftM SpecConstantHexadecimal hexadecimal
parseBinary :: ParsecT String u Identity SpecConstant
parseBinary = liftM SpecConstantBinary binary
parseString :: ParsecT String u Identity SpecConstant
parseString = liftM SpecConstantString str