Skip to content

Commit

Permalink
Fix cut in libreif
Browse files Browse the repository at this point in the history
Then_0 is wrapped with call(_) if it contains unsafe cuts.
  • Loading branch information
hurufu committed Jan 2, 2025
1 parent 016df05 commit 041f429
Show file tree
Hide file tree
Showing 3 changed files with 93 additions and 7 deletions.
9 changes: 3 additions & 6 deletions src/lib/reif.pl
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@
*/

:- use_module(library(dif)).
:- use_module(library(loader), [cut_contained/2]).

:- meta_predicate(if_(1, 0, 0)).
:- meta_predicate(cond_t(1, 0, ?)).
Expand Down Expand Up @@ -91,19 +92,15 @@
sameargs(0, _, _).


/*
no !s that cut outside.
no variables in place of goals
no malformed goals like integers
*/


/* 2do: unqualified If_1: error
*/

%
user:goal_expansion(if_(If_1, Then_0, Else_0), G_0) :-
ugoal_expansion(if_(If_1, Then_0, Else_0), G_0).
cut_contained(Then_0, SanitizedThen_0),
ugoal_expansion(if_(If_1, SanitizedThen_0, Else_0), G_0).

%
%
Expand Down
59 changes: 58 additions & 1 deletion src/loader.pl
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,8 @@
strip_module/3,
use_module/1,
use_module/2,
current_module/1
current_module/1,
cut_contained/2
]).

:- use_module(library(error)).
Expand Down Expand Up @@ -43,6 +44,62 @@
nl,
'$fail'.


%% cut_contained(?G_0, ?S_0).
%
% Both `G_0` and `S_0` are valid callable terms having the same meaning, but
% additionally `S_0` is safe to be called in combination with surrounding
% goals, without worrying that cut side-effect will escape and contaminate
% outer goals. `S_0 = call(G_0)` when it contains callable !s that cut outside,
% and `S_0 = G_0` otherwise.
%
% For example: given `G_0 = (a,!)` then compound goal `b,a,!` will remove
% choice points generated by `b`, but since `S_0 = call((a,!))` then
% `b, call((a,!))` is safe.
%
% TODO: Should it be marked with meta_predicate(cut_contained(:,-))?
%
cut_contained(G, S) :-
catch(cut_contained_aux(G, S), stop(_), false).

cut_contained_aux(G, call(G)) :- cuts_outside(G).
cut_contained_aux(G, G ) :- \+ cuts_outside(G).


%% cuts_outside(?G_0).
%
% `G_0` is a goal for which side-effects of a cut may spill out to the
% surrounding goals. Throws `stop(_)` when it doesn't represent a valid goal.
%
% For example it succeeds for terms `a, (!, b)` and `a, b -> !` where cut
% removes choice points generated by `a`, but fails for `a, (! -> b)` and
% `a, \+ \+ !`.
%
cuts_outside(G) :-
callable_term(G),
cuts_outside_aux(G).

cuts_outside_aux(!).
cuts_outside_aux(M:A) :- module_name(M), cuts_outside(A).
cuts_outside_aux((A,B)) :- cuts_outside(B); cuts_outside(A).
cuts_outside_aux((A;B)) :- cuts_outside(B); cuts_outside(A).
% FIXME: There is an issue with `C, (! -> B)` construct, see #2739
cuts_outside_aux((_->B)) :- cuts_outside(B).


module_name(M) :-
atom(M) -> true; throw(stop(type_error(atom,M))).


callable_term(T) :-
callable(T) ->
( acyclic_term(T) ->
true
; throw(stop(type_error(acyclic_term,T)))
)
; throw(stop(type_error(callable,T))).


expand_term(Term, ExpandedTerm) :-
( '$predicate_defined'(user, term_expansion, 2),
catch(user:term_expansion(Term, ExpandedTerm0),
Expand Down
32 changes: 32 additions & 0 deletions src/tests/reif.pl
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,38 @@
Solutions == [if_(1=1,a=a,2), error(type_error(callable,2),call/1)]
)).

test(W, loader:call(T)) :-
member(T, [
cuts_outside(!),
cuts_outside(foo:!),
cuts_outside((a,!)),
cuts_outside((!;b(_))),
cuts_outside(((a;b(_,_);c),!,d)),
\+ cuts_outside(call((a,!))),
\+ cuts_outside(((a;b;c),\+ !,d)),
\+ cuts_outside((! -> a; b)),
\+ cuts_outside(((x,!;y) -> a; b)),
catch((cuts_outside(_),false), E0, E0 = stop(type_error(callable,_))),
catch((cuts_outside(2),false), E1, E1 == stop(type_error(callable,2))),
catch((cuts_outside(1:!),false), E2, E2 == stop(type_error(atom,1))),
catch((cuts_outside(_:!),false), E3, E3 = stop(type_error(atom,_))),
(G0 = a(G0), catch((cuts_outside(G0),false), E4, E4 = stop(type_error(acyclic_term,_)))),
(G1 = m:G1, catch((cuts_outside(G1),false), E5, E5 = stop(type_error(acyclic_term,_)))),
(cut_contained(a, X0), X0 == a),
(cut_contained(!, X1), X1 == call(!)),
(cut_contained((a,b;c,d), X2), X2 == (a,b;c,d)),
(cut_contained((\+ \+ a), X3), X3 == (\+ \+ a)),
% Questionable test case, see #2739
(cut_contained((!,a->c;d), X4), X4 == (!,a->c;d)),
(cut_contained((x,a->!;d), X5), X5 == call((x,a->!;d))),
(cut_contained((a,b,c,!), X6), X6 == call((a,b,c,!))),
\+ cut_contained(0, _),
\+ cut_contained(_, _),
\+ cut_contained((a,_), _),
\+ cut_contained((a,b;1), _)
]),
phrase(format_("callable cut: ~q", [T]), W).

result_or_exception(Goal, Result) :-
catch((Goal,Result=Goal), Result, true).

Expand Down

0 comments on commit 041f429

Please sign in to comment.