AeneasVerif
Compute short names of items
Items in the pretty output have fully-qualitied names that are hard to read. We could compute for each item a shorter name that is guaranteed to be unique across the whole llbc output, and use that shorter name when displaying to the user.
As discussed: I believe this is a good idea. There is just one thing which is not clear to me: do you intend to compute a short name for all names, or only for a small selection of the most common ones (such as Box)?
As a side remark: of course, we will need an option to print the full names - in my case, I often write name patterns by looking at the debugging output, but those can only be derived by looking at the full names.
I intend this for all names. I also intend for the name matcher to optionally work on short names (and raise an error if there could be ambiguity).
We can also easily add an option to print full names, or add a map from short to full names in the llbc output.
I intend this for all names. I also intend for the name matcher to optionally work on short names (and raise an error if there could be ambiguity).
Ok, understood. A small remark for the name matcher: I think it would be good if the patterns are stable, which would not be the case if we allow matching by using short names (as adding a dependency to a crate might introduce ambiguities, making some previously succeeding patterns suddenly fail).
Agreed, hence why "optional". I also think short names are a lot more convenient when prototyping so it's a good option to have.