PR#1314: kost moved PR#1314 from incoming to engine

[Raphael Collet]

Konstantin Popov wrote:
> 
> > > While this is legitimate behaviour from the language point of view,
> >
> > ???  Why would this be legitimate behavior?  I disagree with this.
> if I remember right, the state of the store after a failure is not
> defined. Partially because of that "incremental tell", right?

No, the "incremental tell" behavior is more precise than that.  It
decomposes a unification into elementary constraints.  If a failure
occurs, a subset of those constraints might have been told to the
store.  But this subset never makes the store inconsistent, nor does it
remove existing information (which is the case with the bug above).

Here is an example.  Suppose that variable Z is free, and you try to
unify X=foo(1 2) with Y=foo(Z 4).  The unification fails, though Z=1
might be told to the store.  What unification does looks like
 - check record labels ('foo' and 'foo') -> ok
 - check arities ([1 2] and [1 2]) -> ok
 - unify X.1 with Y.1 -> successfully tell Z=1
 - unify X.2 with Y.2 -> failure

The procedure must be similar for open records.  The unification of
a(b:1 c:2) with j(...) should fail at the very first step.  The record
labels are incompatible, so no binding should happen at all.

I will have a look at this (not immediately, but in a few days).


Cheers,

raph