Email Gateway (Aug 22 2022 at 17:25): Email Gateway (Aug 22 2022 at 17:25):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
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:
http://hackage.haskell.org/package/pretty-tree-0.1.0.0/docs/Data-Tree-Pretty.html
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 before?
Best,
Andreas
Email Gateway (Aug 22 2022 at 17:25):From: Tobias Nipkow <nipkow@in.tum.de>
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.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 17:27):From: Manuel Eberl <eberlm@in.tum.de>
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
possible.
– 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.
Manuel
ex1.pdf
ex2.pdf
ex3.pdf
Tree_Visualization.thy
Email Gateway (Aug 22 2022 at 17:27):From: Tobias Nipkow <nipkow@in.tum.de>
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
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 17:27):From: Makarius <makarius@sketis.net>
Incidently, the Isabelle Workshop 2018 at Oxford has a contribution
about a verified tree layout algorithm:
https://files.sketis.net/Isabelle_Workshop_2018/Isabelle_2018_paper_7.pdf
The paper cites this paper from 1996:
https://www.microsoft.com/en-us/research/publication/functional-pearl-drawing-trees
(with SML implementation).
There might be better tree layout algorithms now, but I am not an expert
on this. I only recall experts saying that there are different problem
classes:
(1) general graph layout (very difficult)
(2) DAG layout (difficult)
(3) tree layout (easy)
Makarius
Email Gateway (Aug 22 2022 at 17:27):From: Makarius <makarius@sketis.net>
On 24/06/18 12:43, Manuel Eberl wrote:
– 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
possible.
Generally, only a PIDE front-end (Isabelle/Scala) can display things,
not the back-end (Isabelle/ML). E.g. see the @{doc} antiquotation.
– 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.
Both Graphviz and Isabelle Graphview are for DAG layout, not
specifically for trees.
It might be better to integrate a decent tree layout algorithm into
Isabelle/Scala, and thus avoid the usual problems with external tools:
manual tinkering with installation that "works for me" but not for everyone.
Makarius
Email Gateway (Aug 22 2022 at 17:27):From: Manuel Eberl <eberlm@in.tum.de>
On 24/06/18 16:52, Makarius wrote:
Generally, only a PIDE front-end (Isabelle/Scala) can display things,
not the back-end (Isabelle/ML). E.g. see the @{doc} antiquotation.
Well, yes, I was thinking of something similar to what
thy_deps/code_deps does: Display some markup that one can click on to
get to the PDF file. Or some kind of jEdit popup.
Both Graphviz and Isabelle Graphview are for DAG layout, not
specifically for trees.
That is true, but dot attempts to keep the lexicographic ordering of
children, and in a tree, I think it always does, since there are no real
constraints that prevent it from doing that. People do use Graphviz to
visualise ordered trees a lot.
It might be better to integrate a decent tree layout algorithm into
Isabelle/Scala, and thus avoid the usual problems with external tools:
manual tinkering with installation that "works for me" but not for everyone.
Yes, one could do that. But the GUI would have to support quite a few
things in order to reach the same kind of versatility w.r.t. diffferent
node shapes that Graphviz provides. I took advantage of that a lot and I
think the results speak for themselves.
In any case, I do agree that having Isabelle talk to Graphviz is a
suboptimal solution unless possibly if we want to integrate Graphviz as
a component (which we probably don't).
I do think that offering Graphviz code as one possible output format is
a good idea though; that way people can easily produce PDFs/LaTeX, e.g.
for slides.
Manuel
Email Gateway (Aug 22 2022 at 17:27):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
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_)")
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.
Best,
Andreas
Email Gateway (Aug 22 2022 at 17:27):From: Makarius <makarius@sketis.net>
I am still doing Isabelle PDF presentations myself, but the coming
release is hopefully the last one where this is the usual way to do it:
the general plan is to move towards high-quality HTML presentations;
details still need to be determined.
Some weeks ago I actually intended to get something of this into the
Isabelle2018 release, but I have already switched into strict release
mode where only essential things are to be flushed from the pending
pipeline.
While such new things are waiting in the queue, I find myself doing
presentations directly from the Isabelle/jEdit view more and more often.
Makarius
Last updated: Apr 20 2024 at 08:16 UTC