Pretty Printing Syntax Tree with Operator Precedence and Associativity in Haskell

Question

Is there any commonly used method or even a library for pretty printing (and parsing) a syntax tree with (binary) operators that have an associativity and a precedence level assigned, so that the result uses as few brackets as possible?

---

Take the formulas of propositional calculus as an example:

data Formula
    = Atom String
    | Not (Formula)
    | And (Formula) (Formula)
    | Or (Formula) (Formula)
    | Imp (Formula) (Formula) 

Assume that the precedence is Imp < Or < And < Not (so Not binds the most) and that And, Or and Imp should associate to the right; so for example Imp (And (Imp (Atom "A") (Atom "B")) (Atom "A")) (Atom "B") should print something like (A -> B) /\ A -> B.

---

Of course this could be achieved by pattern matching but this is tedious and very unpleasant; I'm looking for something similarly simple to this notation from the Coq proof assistant:

Notation "A /\ B" := (and A B) (at level 80, right associativity).

which generates a parser and a pretty printer.

Pereyra

There is no such language feature in Haskell as there is Coq - you are likely stuck writing a parser yourself. The standard parsec can handle this use case quite easily. Some libraries allow you to define both a parser and pretty printer from some specification of the grammar. – Magnusson

Answer 1

A Show instance for Formula might look like this:

instance Show Formula where
  showsPrec _ (Atom name) = showString name
  showsPrec p (Not formula) = showParen (p > 3) $
    showString "\\+ " . showsPrec 3 formula
  showsPrec p (And lhs rhs) = showParen (p > 2) $
    showsPrec 3 lhs . showString " /\\ " . showsPrec 2 rhs
  showsPrec p (Or lhs rhs) = showParen (p > 1) $
    showsPrec 2 lhs . showString " \\/ " . showsPrec 1 rhs
  showsPrec p (Imp lhs rhs) = showParen (p > 0) $
    showsPrec 1 lhs . showString " -> " . showsPrec 0 rhs

Which will allow any Formula to be shown with appropriate parens:

main = print $ Imp (And (Imp (Atom "A") (Atom "B")) (Atom "A")) (Atom "B")

Prints (print is putStrLn . show):

(A -> B) /\ A -> B

Neese