I'm trying to write a parser for the propositional calculus using Parsec. The parser uses the buildExpressionParser
function from Text.Parsec.Expr. Here's the code where I define the logical operators.
operators = [ [Prefix (string "~" >> return Negation)]
, [binary "&" Conjunction]
, [binary "|" Disjunction]
, [binary "->" Conditional]
, [binary "<->" Biconditional]
]
binary n c = Infix (spaces >> string n >> spaces >> return c) AssocRight
expr = buildExpressionParser operators term
<?> "compound expression"
I've omitted the parsers for variables, terms and parenthesised expressions, but if you think they may be relevant to the problem you can read the full source for the parser.
The parser succeeds for expressions which use only negation and conjunction, i.e. the only prefix operator and the first infix operator.
*Data.Logic.Propositional.Parser2> runPT expr () "" "p & ~q"
Right (p ∧ ¬q)
Expressions using any other operators fail on the first character of the operator, with an error like the following:
*Data.Logic.Propositional.Parser2> runPT expr () "" "p | q"
Left (line 1, column 3):
unexpected "|"
expecting space or "&"
If I comment out the line defining the parser for conjunctions, then the parser for disjunction will work (but the rest will still fail). Putting them all into a single list (i.e. of the same precedence) doesn't work either: the same problem still manifests itself.
Can anyone point out what I'm doing wrong? Many thanks.
Thanks to Daniel Fischer for such a prompt and helpful answer.
In order to finish making this parser work correctly, I also needed to handle repeated applications of the negation symbol, so that e.g. ~~p
would parse correctly. This SO answer showed me how to do it, and the change I made to the parser can be found here.
Your problem is that
binary n c = Infix (spaces >> string n >> spaces >> return c) AssocRight
the first tried infix operator consumes a space before it fails, so the later possibilities are not tried. (Parsec favours consuming parsers, and <|>
only tries to run the second parser if the first failed without consuming any input.)
To have the other infix operators tried if the first fails, you could either wrap the binary
parsers in a try
binary n c = Infix (try $ ...) AssocRight
so that when such a parser fails, it does not consume any input, or, better, and the conventional solution to that problem, remove the initial spaces
from it,
binary n c = Infix (string n >> spaces >> return c) AssocRight
and have all your parsers consume spaces after the token they parsed
variable = do c <- letter
spaces
return $ Variable (Var c)
<?> "variable"
parens p = do char '('
spaces
x <- p
char ')'
spaces
return x
<?> "parens"
Of course, if you have parsers that can parse operators with a common prefix, you would still need to wrap those in a try
so that if e.g parsing >=
fails, >>=
can still be tried.
Mocking up a datatype for the propositions and changing the space-consuming behaviour as indicated above,
*PropositionalParser Text.Parsec> head $ runPT expr () "" "p | q -> r & s"
Right (Conditional (Disjunction (Variable (Var 'p')) (Variable (Var 'q'))) (Conjunction (Variable (Var 'r')) (Variable (Var 's'))))
even a more complicated expression is parsed.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With