[mercury-users] Solver types and \=

[Ralph Becket]

Peter Hawkins, Friday, 12 August 2005:
> Hi...
> 
> Suppose A and B are variables of a solver type with an equality defined. 
> Then Mercury appears to transparently convert:
> A \= B
> to:
> not(A = B)

Yes, this is described in the reference manual:
http://www.mercury.cs.mu.oz.au/information/doc-latest/mercury_ref/Goals.html#Goals

	Term1 \= Term2
	    An inequality. Term1 and Term2 must be valid data-terms.
	    This is an abbreviation for not (Term1 = Term2). 

> However, since I would imagine most of the time the equality of two 
> solver types will post a constraint, and it is illegal to post a 
> constraint within a negated context, this behaviour is silly.

No, this behaviour is fine.  What is "silly" is not reporting an error.
This is on my TODO list: namely, require that any negated goals taking
non-local solver type inst any arguments be explicitly marked as impure.
I expect this will require changes in quite a lot of the solver type
applications out there.

> Perhaps it would be better to leave '\=' undefined for solver types,
> and leave the user to define a custom inequality predicate if it makes
> sense?

Hmm, that sounds horribly warty to me.  Unfortunately, I think this is
one of those situations where there is friction between Mercury's
execution model and the use of solver types.  I don't think we should
change Mercury's execution model.

-- Ralph
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------