{-
  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 Data.Char
import Data.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'