mozart / mozart2

Mozart Programming System v2
http://mozart.github.io/
BSD 2-Clause "Simplified" License
566 stars 96 forks source link

Fix error message on failed unification #315

Closed layus closed 6 years ago

layus commented 6 years ago

Sometimes, unification fails with a nonsensical error message like this.

%***************************** failure **************************
%**
%** Tell: [1] = [1]

It appears that rebinding is not properly undone, and the two values are still aliased when producing the error message. Hence the confusing output.

XXX: This fix works but I have no idea why.

Closes #312. /cc @sjrd

sjrd commented 6 years ago

I looks like this is only pushing the issue into a smaller corner. What if both nodes are unstable?

layus commented 6 years ago

I looks like this is only pushing the issue into a smaller corner. What if both nodes are unstable?

Then

void StableNode::init(VM vm, UnstableNode& from) {
  std::cout << BOOST_CURRENT_FUNCTION << "\n";
  set(from);
  if (!isCopyable())
    from.make<Reference>(vm, this);
}

is not called. And

void UnstableNode::copy(VM vm, UnstableNode& from) {
  if (from.isCopyable()) {
    set(from);
  } else {
    StableNode* stable = new (vm) StableNode;
    stable->set(from);
    make<Reference>(vm, stable);
    from.make<Reference>(vm, stable);
  }
}

gets called instead, which probably breaks alike.

That being said, it never happened on all the tests in the test suite. So I just assume this does not occur.

layus commented 6 years ago

What would be a good way to implement rollback in that case ?

layus commented 6 years ago

Well, no, in that case it works, but one of the stable nodes is not reverted, and remains a reference to the stable node created in void UnstableNode::copy(VM vm, UnstableNode& from). This is however okay because from references the correct value as the stable node was initialized with from. It leaves a new stable node behind, but that is not a big deal I think.

layus commented 6 years ago

So the only case where it is annoying is the wkEqual of two unstable nodes. Smarter rollback would need to undo the creation of the stable node, which would require deleting it. That seems far too complex, just leave the stable node around. the reference will be resolved sooner or later.

sjrd commented 6 years ago

Well, no, in that case it works, but one of the stable nodes is not reverted, and remains a reference to the stable node created in void UnstableNode::copy(VM vm, UnstableNode& from). This is however okay because from references the correct value as the stable node was initialized with from. It leaves a new stable node behind, but that is not a big deal I think.

Ah yes, that seems to be a reasonable analysis. Yes, then I believe it should work fine. Perhaps include that as a comment in the C++ code?

undo the creation of the stable node, which would require deleting it

No, never delete anything allocated on the VM heap. You can never be sure its reference hasn't been transferred somewhere else. Just let it stay there, and it will be garbage-collected.

layus commented 6 years ago

Perhaps include that as a comment in the C++ code?

I would be glad to do that, but where ? It belongs to both UnstableNode::copy and StructuralDualWalk::rebind. More generally, this pertains to the reinit/init/copy interface of nodes. I propose to comment both in RichNode::reinit(VM vm, RichNode from) and StructuralDualWalk::rebind. Do we have a deal ? ;)

sjrd commented 6 years ago

Yes, sounds good.