[m-dev.] Suggestion for a new "where" operator

[Fergus Henderson]

On 05-Aug-2003, Peter Schachte <schachte at cs.mu.OZ.AU> wrote:
> On Tue, Aug 05, 2003 at 11:58:50AM +1000, Fergus Henderson wrote:
> > This determinism requirement is necessary for consistency with the way
> > we treat functions.  Unfortunately, however, it will make the proposal
> > a bit more difficult to implement.  In particular, we will need to keep
> > track in the HLDS of which goals came from a `where' expression, so that
> > determinism analysis can check their determinism.
> > 
> > That in turn also means that we should not allow mode reordering to
> > break up where expressions.
> 
> Maybe the best way to ensure consistency of the 'where' syntax with
> function application would be to transform
> 
> 	(E where G)
> 
> into
> 
> 	f(vars)
> 
> where f is defined as
> 
> 	f(vars) = E :- G
> 
> and vars = the intersection of the sets of variables appearing in the
> clause outside the where expression and the variables appearing in
> either E or G.  And the compiler should be encouraged to inline f.

There seems to be little point in outlining this function in order
to almost immediately inline it again.

Also, treating it as a separate function would unnecessarily constrain
the modes.  Even if mode inference was used, rather than just assuming
the default function mode, this would not be as general as treating
the goal as an inline goal for the purpose of mode analysis, since mode
inference is not capable of inferring some complicated modes -- it makes
some approximations to ensure termination.

Instead, I think `E1 = (E2 where G)' should be transformed by make_hlds.m
to
	V1 = E1,
	V2 = E2,
	some [] (G),
	V1 = V2

where V1 and V2 are fresh variables.

Wrapping G up in a "some" like this would ensure that mode reordering
won't break G up by reordering goals into or out of the where expression,
which is important for checking the determinism of G.

The "some [] (G)" goal would need to be annotated with a
"from_where_goal(E2Vars)" annotation, where E2Vars are the non-local
variables of E2.  Determinism analysis could then look at "some" goals
with the "from_where_goal" annotation, and could enforce determinism
restrictions analagous to those that we use for functions: if all the
non-local variables of the goal apart from those in the result (E2Vars)
are input, then the "some" goal must have at most one solution.

The transformation shown above is for the case where E1 and E2 are
compound expressions.  If E1 is just a variable, then the unification
V1 = E1 should be omitted, and the other occurrence of V1 replaced with E1.
Likewise for E2 and V2.

Note that the specific order of expansion -- first E1, then E2, then G,
then V1 = V2 -- is chosen to match Mercury's normal depth-first
left-to-right evaluation order.  (The order may change after mode
reordering, of course, or if --no-reorder-conj is not specified.)

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------