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



On 23/06/18 16:32, Andreas Lochbihler wrote:
> 
> 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

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




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