Simulating occurs_check=error in SICStus Prolog

66 views Asked by At

It turns out that SICStus Prolog doesn't have an occurs_check Prolog flag. At least we couldn't find one, and this here gives an error message:

/* SICStus 4.6.0 (x86_64-win32-nt-4) */

?- set_prolog_flag(occurs_check, true).
Domain error in argument 1 of set_prolog_flag/2 

It seems the value "true" is not so much a problem, the crictical unifications can be realized via the existing built-in unify_with_occurs_check/2. An interesting value of an occurs_check Prolog flag is the value "error".

How would one implement a predicate unify_with_occurs_check_and_error/2 ? Please note, the solution for unify_with_occurs_check_and_error/2 should behave like unify_with_occurs_check/2, i.e. not trigger attributed variables.

Here is an example usage of the Prolog flag where present:

?- set_prolog_flag(occurs_check, error).
true.

?- X = f(X).
ERROR: ...

And this is what one would do in SICStus Prolog:

?- unify_with_occurs_check_and_error(X, f(X)).
ERROR: ...
1

There are 1 answers

0
AudioBubble On

Was adapting the code from here and got the following solution:

unify_with_error(X, Y) :- var(X), var(Y), !, X = Y.
unify_with_error(X, Y) :- var(X), !, must_notin(X, Y), X = Y.
unify_with_error(X, Y) :- var(Y), !, must_notin(Y, X), X = Y.
unify_with_error(X, Y) :- functor(X, F, A), functor(Y, G, B),
   F/A = G/B,
   X =.. [_|L],
   Y =.. [_|R],
   maplist(unify_with_error, L, R).

must_notin(X, Y) :-
   term_variables(Y, L),
   maplist(\==(X), L), !.
must_notin(X, Y) :-
   throw(error(occurs_check(X, Y),_)).

Seems to work and no interference with attributed variables:

/* SICStus 4.6.0 (x86_64-win32-nt-4) */

?- unify_with_error(X, f(X)). 
error(occurs_check(_413,f(_413)),_409)

?- freeze(X, throw(ball)), unify_with_error(X, f(X)).
error(occurs_check(_413,f(_413)),_409)