David,
On 31 Aug 2009, at 18:26, you wrote:
Rob Arthan wrote:
I have a problem building ProofPower with the latest Poly/ML. The
build
goes into a loop at a point where it opens a certain structure.
This
will be the first time Poly/ML has had to pretty-print a value of
the
type THM that represents theorems. This type has a circularity
passing
through a ref and a certain dictionary data type. I have attached
a very
cutdown version of the failing code. The cutdown version behaves slightly differently in that I see some never-ending output,
while the
ProofPower build just goes into a silent busy hang.
The dictionary type OE_DICT that causes the problem is an amalgam
of two
simpler dictionary data types S_DICT (simple dictionaries using an association list) and E_DICT (efficient dictionaries using a hash
key
and a binary tree). Somewhat oddly the problem doesn't happen if I replace OE_DICT with either S_DICT or E_DICT even though the representation type for OE_DICT is just S_DICT * E_DICT.
I'm not sure what's happening in detail in your example but there has been a significant change in the way printing works in the latest version. A printing function (and an equality function, if appropriate) is now compiled for each type as it is created. This means that printing and type-specific equality functions are available in a wider range of cases than they used to be, particularly in functors.
Previously, the code checked whether there was circularity and just printed "..." when it detected it. That's not really possible with the current code so it relies on the print depth (PolyML.print_depth) to stop infinite looping. Setting print_depth to 10 in your example produces much more sensible output.
That works. Even better for me, if I change the order of compilation so that my user-defined pretty-printer for the circular type is installed first, that works too.
The only simple solution I can suggest is to set the default for the printer depth to something much smaller, perhaps 10. There's probably no reason for the current, essentially unconstrained, print depth.
I also noted in passing that types declared as abstypes are now
equality
types. Was this a conscious attempt to implement one of the
Successor ML
proposals?
No, it was something I noticed while working on the printing and equality code. An early draft of Standard ML explicitly said that abstypes were not equality types outside the "with...end" block and that's what Poly/ML implemented. When I looked again recently I couldn't actually see that anywhere in either the ML90 or ML97 definitions and it seems to conflict with the way equality is handled in the semantics. For that reason I took out the code which switched off equality.
Section 4.9 of the ML97 definitions describes something called Abs(TE, VE) that I think is changing the types declared between "abstype" and "with" into non-equality types and getting rid of their constructors. I think the conflict you mention is why there is a Successor ML proposal to do what you have done.
Regards,
Rob.
At 18:38 31/08/2009, Rob Arthan wrote:
Section 4.9 of the ML97 definitions describes something called Abs(TE, VE) that I think is changing the types declared between "abstype" and "with" into non-equality types and getting rid of their constructors. I think the conflict you mention is why there is a Successor ML proposal to do what you have done.
IIRC, part of the reasoning behind this is that you need some way of removing the equality attribute from types. E.g. if you are implementing sets with unordered lists, the default equality function for an int set will not give the correct result. Abstype provides a way (possibly the only way) of removing the equality attribute.
It's been a long while since I was involved with SML, so please take this with a pinch of salt.
Dave.
Rob, Rob Arthan wrote:
Previously, the code checked whether there was circularity and just printed "..." when it detected it. That's not really possible with the current code so it relies on the print depth (PolyML.print_depth) to stop infinite looping. Setting print_depth to 10 in your example produces much more sensible output.
That works. Even better for me, if I change the order of compilation so that my user-defined pretty-printer for the circular type is installed first, that works too.
I've now set the default value of print_depth to 10 rather than 100 so it shouldn't cause this problem again.
I don't know if I mentioned before that there's been a major change in the way type-specific printing is done. The old pretty-printing functions have been replaced by functions that generate the PolyML.pretty datatype: datatype pretty = PrettyBlock of int * bool * context list * pretty list | PrettyBreak of int * int | PrettyString of string
with the context type defined as datatype context = ContextLocation of location | ContextParentStructure of string * context list | ContextProperty of string * string
The context type may be extended in the future. ContextLocation and ContextParentStructure are used by the compiler when outputting information. ContextProperty isn't used or generated by the compiler and is intended for application programs which may want to pass information from a type-dependent pretty printer to a top-level printer.
PolyML.install_pp has been retained for backwards compatibility but PolyML.addPrettyPrinter is probably a better way to go.
There's also a function similar to PolyML.makestring: PolyML.prettyRepresentation: 'a * int -> pretty which takes a type-specific value and a print-depth and returns the "pretty" datatype for the value. I found it useful when writing some of the pretty printers for the basis library since it meant that a pretty-printer for a datatype that in effect extended an existing type could just be written as a function that returned prettyRepresentation of the base type.
Note that abstract types and opaque signatures no longer hide their representation when printing. There was some discussion on whether this was the best approach but it seems that the advantage of being able to install a pretty printer inside an opaque type and have it available outside outweighs the disadvantages.
Section 4.9 of the ML97 definitions describes something called Abs(TE, VE) that I think is changing the types declared between "abstype" and "with" into non-equality types and getting rid of their constructors. I think the conflict you mention is why there is a Successor ML proposal to do what you have done.
You, and Dave, are correct. Somehow I'd missed that. I've now changed it so that abstypes are no longer equality types.
David
-
dave＠berrybental.me.uk -
David.Matthews＠prolingua.co.uk -
rda＠lemma-one.com