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.
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
