[m-dev.] Pretty printing non-canonical types

[Mark Brown]

On 08-Oct-2007, Ian MacLarty <maclarty at csse.unimelb.edu.au> wrote:
> On Mon, Oct 08, 2007 at 10:49:25AM +1000, Ralph Becket wrote:
> > I think Mark's justification is probably sufficient: the viewer of a
> > different representations of the same non-canonical values will give
> > them the same denotation, which means the results from deconstruct
> > are semantically equivalent in the sense intended by
> > promise_equivalent_solutions.
> > 
> 
> I'm not convinced.  You could easily create a function that generated a
> string from a T using format/8.  Say you called this function str.  Then
> you might have the goal 'str(X) = str(Y)' failing, even though X and Y
> are equal.  The problem is that the "viewer" of str(X) and str(Y) is not
> necessarily a person.  It might be the program.  The program won't give
> str(X) and str(Y) the same denotation, even though a human viewer might.

Under my interpretation, the doc type technically should have a user
defined equality, which means format/8 should be cc_multi.  So this would
put some committed choice stuff in the interface of pretty_printer, which
admittedly is what Ralph wanted to avoid.  But because the committed
choice part is only when you write to a stream, it won't be anywhere
near as awkward -- if the stream is io.state then a promise can be made
immediately.  In particular, format/{3,4} would be det.  The awkwardness
was the real issue, I think.

I don't think we should try to implement the user defined equality, but
format/8 should still be cc_multi.

In the case of a string stream (or any stream with equality) the promise
won't be able to be made without extra consideration.  And in your example,
if that promise was added it would be a lie.

(Incidentally, I find it confusing that the pretty_printer module exports
procedures named format* for things that consume docs to create the final
output, as well as for things that produce/transform docs.  Is "formatting"
the process of going from term->doc or doc->stream?  The latter ones should
be renamed, IMHO.)

Cheers,
Mark.

--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at csse.unimelb.edu.au
Administrative Queries: owner-mercury-developers at csse.unimelb.edu.au
Subscriptions:          mercury-developers-request at csse.unimelb.edu.au
--------------------------------------------------------------------------