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.

Tobias

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:

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


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



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