Agfdhyk

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.

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.

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.