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

This is great! I even managed to install graphviz and run one of your examples. The dot format clearly produces the nicest output. It would indeed be good if that could be integrated a bit more.

Many thanks

On 24/06/2018 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


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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