Better display of boolean formulas

Question

I want to implement a method for showing a propositional formula in SML. The solutions that I found so far was of this type:

fun show (Atom a) = a
  | show (Neg p) = "(~ " ^ show p ^ ")"
  | show (Conj(p,q)) = "(" ^ show p ^ " & " ^ show q ^ ")"
  | show (Disj(p,q)) = "(" ^ show p ^ " | " ^ show q ^ ")";

This produces unnecessary braces:

((~p) & (q | r))

when, what I'd like to have is:

~ p & (q | r)

I saw, that Haskell has a function (display?) which does this nicely. Can someone help me out a little bit. How should I go about this?

Answer 1

If you want to eliminate redundant parentheses, you will need to pass around some precedence information. For example, in Haskell, the showsPrec function embodies this pattern; it has type

showsPrec :: Show a => Int -> a -> String -> String

where the first Int argument is the precedence of the current printing context. The extra String argument is a trick to get efficient list appending. I'll demonstrate how to write a similar function for your type, though admittedly in Haskell (since I know that language best) and without using the extra efficiency trick.

The idea is to first build a string that has no top-level parentheses -- but does have all the parentheses needed to disambiguate subterms -- then add parentheses only if necessary. The unbracketed computation below does the first step. Then the only question is: when should we put parentheses around our term? Well, the answer to that is that things should be parenthesized when a low-precedence term is an argument to a high-precedence operator. So we need to compare the precedence of our immediate "parent" -- called dCntxt in the code below -- to the precedence of the term we're currently rendering -- called dHere in the code below. The bracket function below either adds parentheses or leaves the string alone based on the result of this comparison.

data Formula
    = Atom String
    | Neg  Formula
    | Conj Formula Formula
    | Disj Formula Formula

precedence :: Formula -> Int
precedence Atom{} = 4
precedence Neg {} = 3
precedence Conj{} = 2
precedence Disj{} = 1

displayPrec :: Int -> Formula -> String
displayPrec dCntxt f = bracket unbracketed where
    dHere       = precedence f
    recurse     = displayPrec dHere
    unbracketed = case f of
        Atom s   -> s
        Neg  p   -> "~ " ++ recurse p
        Conj p q -> recurse p ++ " & " ++ recurse q
        Disj p q -> recurse p ++ " | " ++ recurse q
    bracket
        | dCntxt > dHere = \s -> "(" ++ s ++ ")"
        | otherwise      = id

display :: Formula -> String
display = displayPrec 0

Here's how it looks in action.

*Main> display (Neg (Conj (Disj (Conj (Atom "a") (Atom "b")) (Atom "c")) (Conj (Atom "d") (Atom "e"))))
"~ ((a & b | c) & d & e)"