Parsing a Formal Logic in Haskell

Question

I have the following language I am trying to parse.

formula ::=  true  
         |  false  
         |  var  
         |  formula & formula  
         |  ∀ var . formula
         |  (formula)

    var ::=  letter { letter | digit }*

I have been following this article on the Haskell wiki and have used Parsec combinators to create the following parser.

module LogicParser where

import System.IO
import Control.Monad
import Text.ParserCombinators.Parsec
import Text.ParserCombinators.Parsec.Expr
import Text.ParserCombinators.Parsec.Language
import qualified Text.ParserCombinators.Parsec.Token as Token

-- Data Structures
data Formula = Var String
             | TT
             | FF
             | Con Formula Formula
             | Forall String Formula
               deriving (Show)

-- Language Definition
lang :: LanguageDef st
lang =
    emptyDef{ Token.identStart      = letter
            , Token.identLetter     = alphaNum
            , Token.opStart         = oneOf "&."
            , Token.opLetter        = oneOf "&."
            , Token.reservedOpNames = ["&", "."]
            , Token.reservedNames   = ["tt", "ff", "forall"]
            }


-- Lexer for langauge
lexer = 
    Token.makeTokenParser lang


-- Trivial Parsers
identifier     = Token.identifier lexer
keyword        = Token.reserved lexer
op             = Token.reservedOp lexer
roundBrackets  = Token.parens lexer
whiteSpace     = Token.whiteSpace lexer

-- Main Parser, takes care of trailing whitespaces
formulaParser :: Parser Formula
formulaParser = whiteSpace >> formula

-- Parsing Formulas
formula :: Parser Formula
formula = conFormula
        <|> formulaTerm
        <|> forallFormula

-- Term in a Formula
formulaTerm :: Parser Formula
formulaTerm = roundBrackets formula
            <|> ttFormula
            <|> ffFormula
            <|> varFormula

-- Conjunction
conFormula :: Parser Formula
conFormula = 
    buildExpressionParser [[Infix (op "&" >> return Con) AssocLeft]] formula

-- Truth
ttFormula :: Parser Formula
ttFormula = keyword "tt" >> return TT

-- Falsehood
ffFormula :: Parser Formula
ffFormula = keyword "ff" >> return FF

-- Variable
varFormula :: Parser Formula
varFormula =
    do  var <- identifier
        return $ Var var

-- Universal Statement 
forallFormula :: Parser Formula
forallFormula = 
    do  keyword "forall"
        x <- identifier
        op "."
        phi <- formulaTerm
        return $ Forall x phi

-- For running runghc
calculate :: String -> String
calculate s = 
    case ret of
        Left e ->  "Error: " ++ (show e)
        Right n -> "Interpreted as: " ++ (show n)
    where 
        ret = parse formulaParser "" s

main :: IO ()
main = interact (unlines . (map calculate) . lines)

The problem is the & operator, I am trying to model it on how the article parses expressions, using the Infix function and passing it a list of operators and a parser to parse terms. However, the parser is not behaving as desired and I can't work out why. Here are some examples of desired behaviour:

true                         -- parsing -->      TT
true & false                 -- parsing -->      Con TT FF
true & (true & false)        -- parsing -->      Con TT (Con TT FF)
forall x . false & true      -- parsing -->      Con (Forall "x" FF) TT

However currently the parser is producing no output. I appreciate any assistance.

Answer 1

I think I managed to fix the problem by rephrasing the grammar, and conjunction is still left-associative:

formula :: Parser Formula
formula = conFormula
        <|> formulaTerm

formulaTerm :: Parser Formula
formulaTerm = roundBrackets formula
            <|> ttFormula
            <|> ffFormula
            <|> varFormula
            <|> forallFormula

conFormula :: Parser Formula
conFormula = 
    buildExpressionParser [[Infix (op "&" >> return Con) AssocLeft]] formulaTerm

This parsed the following successfully.

Answer 2

The problem in your code is, that you try to parse a formula for which the first attempt is to parse a formulaCon. This then first tries to parse a formula, i.e. you create an infinite recursion without consuming any input.

To resolve this, you have to structure your grammar. Define your terms like this (note that all these terms consume some input before doing a recursion back to formula):

formulaTerm = ttFormula
          <|> ffFormula
          <|> varFormula
          <|> forallFormula
          <|> roundBrackets formula

forallFormula = do
  keyword "forall"
  x <- identifier
  op "."
  phi <- formula
  return $ Forall x phi

A formula is then either a single term or a conjunction consisting of term, an operator, and another formula. To ensure that all input is parsed, first try to parse a conjunction and - if that fails - parse a single term:

formula = (try formulaCon) <|> formulaTerm

Finally a formulaCon can be parsed like this:

formulaCon = do
  f1 <- formulaTerm
  op "&"
  f2 <- formula
  return $ Con f1 f2

The drawback with this solution is that conjunctions are now right associative.