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

[Ian MacLarty]

On Mon, Oct 08, 2007 at 10:49:25AM +1000, Ralph Becket wrote:
> Ian MacLarty, Monday,  8 October 2007:
> > On Fri, Oct 05, 2007 at 02:52:11PM +1000, Ralph Becket wrote:
> > > I'm trying to debug the new LP interface.
> > > The debugger uses the new pretty_printer module.
> > > The pretty_printer module uses deconstruct(..., canonicalize, ...) to
> > > decide what to do with each subterm.
> > > The canonicalize form just returns the type name for non-canonical
> > > values, rather than any structural information.
> > > This is most unhelpful for debugging.
> > > Using deconstruct(..., include_details_cc, ...) does the right thing,
> > > but is cc_multi.
> > > I want the include_details_cc behavious, but I don't want to propagate
> > > the cc_multi aspect into the interface to the pretty printer, because
> > > that could make using it rather awkward in many circumstances.
> > > 
> > > Is there any objection to me using include_details_cc wrapped in a
> > > promise_equivalent_solutions scope, even though the promise is a lie?
> > > 
> > 
> > Why not add a predicate like the following:
> > 
> > :- pred format_io(S::in, doc::in, formatter_map::in, int::in, int::in,
> >     formatting_limit::in, io::di, io::uo) is det <= stream.writer(S,
> >     string, io).
> > 
> > in which you do the required promise.  The promise is okay under a
> > suitable interpretation of the IO state.
> 
> Which interpretation do you have in mind?  I don't see it.
> 

Suppose the implementation of format_io didn't actually look at its
second argument.  Suppose instead that it simulated the current program
up to the nth call and then looked at the representation of the
second argument of the nth call in the simulated heap (assuming
that the current call to format_io is the nth call).

To initialize the simulator one has to read in all the source code and
know all the results of all the IO actions up to the nth call.

Reading in the source is deterministic.  The original program could be
easily transformed to record all its IO actions in another file and this
file could be read in by the simulator.  This would have no impact on
the determinism of the original program.  The simulator could
deterministically read in this file too.

So this simulator could be set up and run deterministically.  Looking at
the heap of the simulator is also deterministic.  Hence format_io can be
regarded as deterministic, since all it does is initialise the
simulator, run it to the Nth call, and look at the heap.

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

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