Bugs with non-linear unification

Authoring Dialog
1

It seems there are bugs with unification when a term has a variable used several times, but that variable isn’t used afterwards. The root cause seems to be in the definition of the would_unify function of the Å-machine specification, but happens with z-code as well. A minimal example is as follows:

(test $A)	($A = [0 1])

(program entry point)
	(test [$X $X])
	Unification is possible. (line)
	(test [$Y $Y])
	Value of Y: $Y.

Here, “Unification is possible.” is printed, but the value of $Y isn’t. Besides, if we do not move the unification to its own rule but instead write this:

(program entry point)
	([$X $X] = [0 1])
	Value of X: $X.

Here we get “Value of X: 0.” which is printed, so unification seems to be incorrectly simplified by the compiler in this case.

Also, thanks a lot Linus for your work, Dialog is really awesome!

4 Likes