tableaux-0.1: src/Parser.hs
{-
Parser & pretty-printer for first order logic formulas
Built using the Parsec Haskell library
Pedro Vasconcelos, 2009--2010
-}
module Parser where
import FOL
import Text.ParserCombinators.Parsec
import Text.ParserCombinators.Parsec.Char
import Text.ParserCombinators.Parsec.Expr
import qualified Text.ParserCombinators.Parsec.Token as P
import Text.ParserCombinators.Parsec.Language
import Control.Monad
import Char
import List (intersperse)
import Test.QuickCheck
-- setup a tokenizer
lexer :: P.TokenParser ()
lexer = P.makeTokenParser
(emptyDef {reservedNames=["forall", "exist", "true", "false"]})
-- tokens (using Parsec tokenizer)
identifier = P.identifier lexer
reserved = P.reserved lexer
whiteSpace = P.whiteSpace lexer
parens = P.parens lexer
comma = P.comma lexer
natural = P.natural lexer
operator n = string n >> whiteSpace
lexeme = P.lexeme lexer
-- parse formulas (entry function)
parseFormula txt
= parse (do {f<-connectives; whiteSpace; eof; return f}) "stdin" txt
-- a formula built from connectives
connectives :: Parser Formula
connectives = buildExpressionParser table formula
where table = [[unary "~" Not],
[binary "&" And AssocLeft,
binary "/\\" And AssocLeft],
[binary "|" Or AssocLeft,
binary "\\/" Or AssocLeft,
binary "->" Implies AssocRight]]
unary name fun
= Prefix (do {operator name; return fun})
binary name fun assoc
= Infix (do {operator name; return fun}) assoc
formula :: Parser Formula
formula = do { reserved "forall"
; x<-variable
; f<-formula
; return (Forall x f)
}
<|> do { reserved "exist"
; x<-variable
; f<-formula
; return (Exist x f)
}
<|> do { operator "~"; f<-formula; return (Not f) }
<|> parens connectives
<|> atomic
-- an atom is either a literal or true/false constant
atomic :: Parser Formula
atomic = do { reserved "true"; return TT }
<|> do { reserved "false"; return FF }
<|> do { r<-constant
; do { ts<-parens (term`sepBy`comma)
; return (Rel r ts)
} <|>
return (Rel r [])
}
<?> "atomic formula"
term :: Parser Term
term = do { id<-constant
; parens (do { ts<-term`sepBy`comma
; return (Fun id ts)
})
<|> return (Fun id [])
}
<|> do { x<-variable; return (Var x) }
<?> "term"
constant :: Parser Funsym
constant = lexeme (do { c<-lower
; cs<-many alphaNum
; return (c:cs)
})
<|> do { n<-natural
; return (show n)
}
<?> "constant"
variable :: Parser Var
variable = lexeme (do { c<-upper
; cs<-many alphaNum
; return (c:cs)
}) <?> "variable"
-- formula pretty printer
showFormula f = showsFormula 0 f ""
showsFormula :: Int -> Formula -> ShowS
showsFormula _ TT = ("true"++)
showsFormula _ FF = ("false"++)
showsFormula _ (Rel r ts) = showsTerm (Fun r ts)
showsFormula p (Forall x f)
= showParen (p>10) $ ("forall "++).(x++).(' ':) .showsFormula 10 f
showsFormula p (Exist x f)
= showParen (p>10) $ ("exist "++).(x++).(' ':) .showsFormula 10 f
showsFormula p (Not f)
= showParen (p>10) $ ('~':) . showsFormula 10 f
showsFormula p (And f1 f2)
= showParen (p>=5) $ showsFormula 5 f1 . ("/\\"++) . showsFormula 5 f2
showsFormula p (Or f1 f2)
= showParen (p>=5) $ showsFormula 5 f1 . ("\\/"++) . showsFormula 5 f2
showsFormula p (Implies f1 f2)
= showParen (p>=5) $ showsFormula 5 f1 . ("->"++) . showsFormula 5 f2
showsTerm :: Term -> ShowS
showsTerm (Var x) = (x++)
showsTerm (Fun c []) = (c++)
showsTerm (Fun f ts) = (f++).('(':).s.(')':)
where s = foldl (.) id $ intersperse (',':) (map showsTerm ts)
----------------------------------------------------------------------
-- QuickCheck generators for formulas and terms
----------------------------------------------------------------------
instance Arbitrary Formula where
arbitrary = sized genFormula
shrink = shrinkFormula
instance Arbitrary Term where
arbitrary = sized genTerm
shrink = shrinkTerm
shrinkTerm (Fun f ts) = ts ++ [Fun f ts' | ts'<-shrink ts]
shrinkTerm (Var x) = [Var x]
shrinkFormula (Implies f1 f2) = [f1,f2]
shrinkFormula (And f1 f2) = [f1,f2]
shrinkFormula (Or f1 f2) = [f1,f2]
shrinkFormula (Not f) = [f]
shrinkFormula (Exist x f)= [f]
shrinkFormula (Forall x f) = [f]
shrinkFormula (Rel r ts) = [Rel r ts' | ts'<-shrink ts]
-- a sized generator for formulas
genFormula :: Int -> Gen Formula
genFormula 0 = elements [TT, FF]
genFormula n | n>0 = frequency [(1, arity 1), (1, arity 2),
(2, liftM2 And f' f'),
(2, liftM2 Or f' f'),
(2, liftM2 Implies f' f'),
(2, liftM2 Forall variables f''),
(2, liftM2 Exist variables f'')
]
where
f' = genFormula (n`div`2)
f'' = genFormula (n-1)
arity k = do r<-relsyms
ts<-sequence [genTerm (n`div`k -1) | _<-[1..k]]
return (Rel r ts)
relsyms = elements ["p", "q", "r", "s"]
variables = elements ["X", "Y", "Z"]
-- a sized generator for terms
genTerm :: Int -> Gen Term
genTerm n | n<=0 = frequency [(1, liftM (\f -> Fun f []) constants),
(2, liftM Var variables)]
| otherwise = oneof [arity 1, arity 2]
where
arity k = do f<- funsyms
ts <- sequence [genTerm (n`div`k - 1) | _<-[1..k]]
return (Fun f ts)
funsyms = elements ["f", "g", "h"]
constants = elements ["a", "b", "c", "e"]
variables = elements ["X", "Y", "Z"]
------------------------------------------------------------------
-- Quickcheck properties follow
------------------------------------------------------------------
-- relation between parsing & pretty-printting
-- parseFromula is the left-inverse of showFormula
prop_parseRoundtrip f = case parseFormula (showFormula f) of
Left err -> False
Right f' -> f==f'