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

[Ian MacLarty]

On Mon, Oct 08, 2007 at 02:18:32PM +1000, Mark Brown wrote:
> 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.

Ah, that's okay then.  I thought you were trying to bury the
promise_equivalent_solutions inside format/8.

> 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.
> 

Yes, I agree format/8 should be cc_multi if it's going to have a
polymorphic !State argument.  

> 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.)
> 

What about write_doc?

Ian.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------