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

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 before?


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

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