Re: [isabelle] Pretty-printing for trees in 2D

Hi Manuel,

Thanks a lot for the implementation. That's definitely useful, especially since I also need this for pretty-printing evaluation results.

I got something similar to the vertical tree ASCII art using just notation, where indentation replaces lines. This needs less vertical space, but more horizontal space:

abbreviation (output) Node' where "Node' x l r ≡ Node l x r"
notation (output) Node' ("[(2_)](//❙l❙: (_)//❙r❙: (_))")

I'll have to see whether I have more vertical or horizontal space available. The generated PDFs definitely look much nicer than the ASCII art, but constantly switching between Isabelle/jEdit and the PDF viewer also has its drawbacks in a demo. Moreover, the ASCII art preserves all the nice hovering tool tips, e.g., type information. This is lost in a PDF.


On 24/06/18 12:43, Manuel Eberl wrote:
I'm not sure if this is possible with a print translation in a
reasonable way.

However, it is quite simple to implement something like this with a
command. In fact, one can go even further: Why only ASCII art?

In a fit of over-engineering, I hacked a small bit of code together to
visualize a tree. It currently only works for binary trees (Tree.tree
from HOL-Library), but it can easily be extended to other tree-like
types with a little bit of boilerplate.

I implemented renderers for Tree.tree in three modes:
– ASCII art (like drawTree form Haskell's Data.Tree)
– GraphViz .dot format
– Isabelle/jEdit GraphView

The following things could be improved:
– Nicer ASCII art (e.g. Haskell's Data.Tree.Pretty, and additionally if
we had nice box-drawing characters in the Isabelle symbols, one could
use those to get nicer lines/boxes)
– Automatic rendering of .dot files to PDF and displaying the PDF. This
would be easy if GraphViz is installed on the machine and if I knew how
to launch a PDF viewer from Isabelle. But perhaps something better is
– Isabelle's GraphView sorts the children of each node ascendingly,
which means that binary trees are often not printed faithfully. It also
has very few styling option for the nodes, so the GraphViz output looks
much nicer.

I attached the theory and the PDFs corresponding to the GraphViz output
of the examples in it. Note that subtrees are also supported and
rendered differently from normal nodes.


On 23/06/18 20:43, Tobias Nipkow wrote:
Hi Andreas,

I would like the very same thing. I will only need it to visiualize the
result of some computation. That can (in principle) be dealt with by

value "tree2D(...)"

However, the result is a char list and the newline character is printed
as ⏎ and not as a new line. There are also the '' delimiters around it.
If we can fix that, we are in business.


On 23/06/2018 16:32, Andreas Lochbihler wrote:
Dear list,

For an Isabelle demo, I'd like to pretty-print a binary tree in a 2D
layout, say given by the datatype

datatype tree = Leaf nat | Node tree tree

The output should be 2-dimensional, e.g., what drawVerticalTree in
Haskell does:

I'm happy to write a print translation for the tree constructors to do
that, but I have no clue how I could achieve this with Isabelle's
syntax AST. Is this possible at all? Has anyone done something similar


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.