gprinttyp: a graphical debugging printer for types #13049
Conversation
|
This is a nice idea and I agree in principle. I would expect a review for readability (not "correctness", this is debug-only and we don't care if there is a slight issue here or there) before we can merge. I don't quite follow the actual example (as always): |
|
Oops, I picked a non-representative subgraph, here is a graph of an unification step with the two arrows present. The |
There was a problem hiding this comment.
I did a quick review (I did not read the dot-producing code in full details). This is the usual nice, slightly over-engineered Florian style and I trust it to perform above expectations at printing graphs from types. Thank you!
I think that you should split the change to match_row_field and the row_field_cell type to a separate preparatory commit.
I will be happy to approve once you have done a pass taking the review comments into account. (The most invasive one is to mass-rewrite ellide into elide.)
typing/gprinttyp.ml
Outdated
| let _index params ty = pretty_id params (repr params ty).id | ||
| let field ~name x = match x with | ||
| | Main id -> Field {id;name;synth=false} | ||
| | Field r -> Field {r with name} |
There was a problem hiding this comment.
I don't understand the logic here -- I'm not sure what field is and from a distance I would have expected that the field baz of foo.bar is foo.bar.baz, not foo.baz. No big deal, but maybe a comment. Also when reading that I wondered if we should have Field of t * string instead of your weird definition, but I'm fine with the weird definition as well.
There was a problem hiding this comment.
I have renamed the constructor to Named_subnode to make it clearer that those index are associated to a main index and that the subnode of a subnode is not really supported at this point.
Octachron
force-pushed
the
gprinttyp_core
branch
from
46c6857
to
945f87e
Compare
typing/gprinttyp.ml
Outdated
| | "p" -> "𝜋" | ||
| | "i" -> "𝜄" | ||
| | "h" -> "𝜂" | ||
| | "k" -> "k" |
There was a problem hiding this comment.
Shouldn't that be a kappa (κ or one of the other versions) ?
There was a problem hiding this comment.
Indeed (even if κ and k are quite confusable depending on the font).
typing/gprinttyp.ml
Outdated
| | "r" -> "𝜌" | ||
| | "s" -> "𝜎" | ||
| | "p" -> "𝜋" | ||
| | "i" -> "𝜄" | ||
| | "h" -> "𝜂" | ||
| | "k" -> "κ" | ||
| | "l" -> "𝜆" | ||
| | "m" -> "μ" |
There was a problem hiding this comment.
| | "r" -> "𝜌" | |
| | "s" -> "𝜎" | |
| | "p" -> "𝜋" | |
| | "i" -> "𝜄" | |
| | "h" -> "𝜂" | |
| | "k" -> "κ" | |
| | "l" -> "𝜆" | |
| | "m" -> "μ" | |
| | "r" -> "𝜌" | |
| | "s" -> "𝜎" | |
| | "p" -> "𝜋" | |
| | "i" -> "𝜄" | |
| | "h" -> "𝜂" | |
| | "k" -> "𝜅" | |
| | "l" -> "𝜆" | |
| | "m" -> "𝜇" |
If I'm not mistaken, you're using Unicode's Mathematical Bold Italic Small symbols, from U+1D736 to U+1D714. The kappa and mu were not exactly consistent…
There was a problem hiding this comment.
Indeed, this is better, thanks!
|
While squashing the history, I have added a basic description of the graph format; since I had been told that the format might be a bit too arcane to decipher without any explanation. |
This purely internal PR proposes to add a
Gprinttypmodule which can print faithfully type expressions as digraphs using the graphviz format.This module is intended as a helper for typechecker debugging session (see 71dd0d0 for an example of use case), since graph representation scales better than purely textual representation when there are more than a dozen of nodes involved.
As an illustration, the digraph representation for
is
which is still readable even with the 16 nodes of the type expressions, and the few empty universal type variable binders.
Since printing digraphs on stdout does not work that well when printing hundreds of graphs (my debugging session in #13004 typically produced between 100 and 600 graphs by execution trace), the interface of
Gprinttypis oriented toward dumping files in a directory specified bydump-dirs, with few helpers functions that helps to provide context.All feature of the type expressions are covered (type expansions, object fields and polymorphic variants included) and there are few knobs exposed for tuning the level of detail of the graph, and it should be straightforward to add more, in particular for printing levels and scopes.
I imagine that I should mention that the unicode characters in the printers can be removed if required.