[m-dev.] call for opinions on promise_same_solutions syntax

[Peter Schachte]

OK, with an understanding of the motivating example, here's a new
proposal, rather similar to Zoltan's proposal 2 (but avoiding the use
of the 'deconstruct' keyword and still trying to make this a general
facility):

        promise_equivalent_solution_sets [Vars] (
                whichever [Vars1] Goal1,
                whichever [Vars2] Goal2,
		...
		Goal
        )

This is semantically equivalent to (Goal1, Goal2, ..., Goal).  But it
makes the promise that for each Vars1 satisfying Goal1, the set of
solutions for Vars satisfying Goal2,Goal is equivalent.  Similarly, it
promises that for each Vars2 satisfying Goal2, the set of solutions
for Vars satisfying Goal1,Goal is equivalent.  The compiler must
verify that no variables other than those on Vars are generated by
Goal and used outside the promise_equivalent_solution_sets, and
similarly that no variables other than those on the quantified list
are generated inside and used outside a 'whichever' context.  This
justifies independently committing to the first solution to each
'whichever' goal.

The goal within a 'whichever' context should be permitted to be
compound, and to contain goals of any determinism.  It should also be
permitted to put any goals before, among, or after after all
'whichever' contexts.  However, in the case where Goal1 is cc_multi
and Goal2 is cc_nondet, they must appear in separate 'whichever'
contexts.

Actually, I wouldn't mind dropping the [Vars] part of the
promise_equivalent_solution_sets goal.  It's easy enough to think of
this as saying the choice of solutions for Vars1 and Vars2 satisfying
Goal1 and Goal2 are immaterial to the solutions to Goal.  But I think
it's important to list the variables for which all solutions generate
equivalent solution sets for Goal.

-- 
Peter Schachte              Even if you are a minority of one, the truth is
schachte at cs.mu.OZ.AU        the truth.
www.cs.mu.oz.au/~schachte/      -- Mahatma Gandhi 
Phone: +61 3 8344 1338      
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------