How to safely temporarily change the occurs check flag?

Question

I am using the following code to temporarily change the occurs check flag, where G is a goal that doesn't create any delayed goals:

with_occurs_check(G) :-
   current_prolog_flag(occurs_check, F),
   setup_call_cleanup(
      set_prolog_flag(occurs_check, true),
      G,
      set_prolog_flag(occurs_check, F)).

The below is a desired aspect of with_occurs_check/1, since we want all backtracking into the goal G work with the occurs check flag set to true. Also preferably only once a choice point is created, this is seen in SWI-Prolog that ";" is only asked once and not twice:

?- with_occurs_check((X=1;current_prolog_flag(occurs_check, F), X=2)).
X = 1 ;
X = 2,
F = true.   %%% desired

But there is a caveat. The above doesn't really work when G is non-deterministic. If G has an exit port with remaining choice points, setup_call_cleanup/3 will not call its cleanup. So the occurs check flag change will leak into the continuation:

?- with_occurs_check((X=1;X=2)), current_prolog_flag(occurs_check, F).
X = 1,
F = true ;   %%% not desired, update leaking
X = 2,
F = false.   %%% desired

Is there a safer way to change the occurs check temporarily?

You want the occurs check to be "on" for a proof subtree. But a Prolog Processor with the occurs flag on is actually a "different engine" (in particular arbitrary delayed goals could run in the context of the occurs check being on). In SWI-Prolog you could maybe start a [Prolog engine](https://eu.swi-prolog.org/pldoc/man?section=engines) ... but I'm still not sure that the occurs flag would be restricted to that. — David Tonhofer, Feb 04 '21 at 12:52

gusbro · Answer 1 · 2021-02-04T17:52:18.203

Maybe revert the occurs check also after G succeeds ?

with_occurs_check(G) :-
   current_prolog_flag(occurs_check, F),
   setup_call_cleanup(
      set_prolog_flag(occurs_check, true),
      (G, set_prolog_flag(occurs_check, F)),
      set_prolog_flag(occurs_check, F)).

test run:

?- with_occurs_check((X=1;X=2)), current_prolog_flag(occurs_check, F).
X = 1,
F = false ;
X = 2,
F = false.

Update after reading comments so that occurs_check continue to be true upon backtracking:

with_occurs_check(G) :-
   current_prolog_flag(occurs_check, F),
   setup_call_cleanup(
      set_prolog_flag(occurs_check, true),
      (G, with_occurs_check1(F)),
      set_prolog_flag(occurs_check, F)).

with_occurs_check1(F):-
  set_prolog_flag(occurs_check, F).
with_occurs_check1(_):-
  set_prolog_flag(occurs_check, true),
  fail.

Sample run:

?- with_occurs_check((X=1;current_prolog_flag(occurs_check, F), X=2)), current_prolog_flag(occurs_check, F2).
X = 1,
F2 = false ;
X = 2,
F = true,
F2 = false ;
false.

How to safely temporarily change the occurs check flag?

1 Answers1