Как использовать freeze/2 или когда / 2 для более чистого кода Пролога

Question

Я написал предикат term_ctx_subterm/3, который представляет собой связь между термином, контекстом с одним отверстием для этого термина и подтермом, который заполняет дыру. По большей части предикат работает так, как я хочу. Смотрите код и примеры его использования ниже. Однако я использовал два предложения для определения предиката, по одному для каждого из двух его режимов. В первом режиме термин является составным, и он деконструируется в контексты с одним отверстием и соответствующие подтермы. Во втором режиме задается контекст с одним отверстием, и термин восстанавливается с использованием подтерма для заполнения отверстия.

Я пытался написать term_ctx_subterm как предикат с одним предложением, используя когда /2, и я думаю, что я близок, но а) это довольно уродливо и б) это не совсем правильно работает. Как я могу использовать сопутствующие предикаты для реализации term_ctx_subterm, используя одно предложение?

Сначала вот версия 1, с двумя пунктами:

Версия 1

%!    term_ctx_subterm(+Term, ?CtxHole, ?SubTerm) is nondet
%!    term_ctx_subterm(?Term, +CtxHole, ?SubTerm) is det
%
%     True when =Term= is equal to =CtxHole= if the hole is equal to
%     SubTerm. =CtxHole= is a pair =Ctx-Hole= where =Ctx= is a term
%     containing variable =Hole=. 
%
term_ctx_subterm(Term, Ctx-Hole, SubTerm) :-
    nonvar(Term),
    !,    
    Term =.. [F|Args],
    append(Left, [R|Right], Args),
    append(Left, [R1|Right], CtxArgs),
    Ctx  =.. [F|CtxArgs],
    (SubTerm = R,
     Hole = R1
    ;
    term_ctx_subterm(R, Ctx1-Hole, SubTerm),
    R1 = Ctx1
    ),
    Ctx  =.. [F|CtxArgs].
term_ctx_subterm(Term, Ctx-Hole, SubTerm) :-
    nonvar(Ctx),    
    !,
    Term = Ctx,
    Hole = SubTerm.


test1 :-
    term_ctx_subterm(a(b, c(d)), Ctx-Hole, SubTerm).

% ?- term_ctx_subterm(a(b, c(d)), Ctx-Hole, SubTerm),
% Ctx = a(Hole, c(d)),
% SubTerm = b ;
% Ctx = a(b, Hole),
% SubTerm = c(d) ;
% Ctx = a(b, c(Hole)),
% SubTerm = d ;
% false


test2 :-
    term_ctx_subterm(Term, a(b, c(Hole))-Hole, 'HERE').

% ?- term_ctx_subterm(Term, a(b, c(Hole))-Hole, 'HERE').
% Term = a(b, c('HERE')),
% Hole = 'HERE'.

test3 :- % should probably throw an instantiation error here
    term_ctx_subterm(A, B, C).

% ?- term_ctx_subterm(A, B, C).
% false
%

Версия 2

В этой версии я пытаюсь использовать, когда /2:

term_ctx_subterm_v2(Term, Ctx-Hole, SubTerm) :-
    when((nonvar(Term); nonvar(F), ?=(Args, CtxArgs)),
         (Term =.. [F|Args])),

    when((nonvar(Ctx); nonvar(F), ?=(Args, CtxArgs)),
           (Ctx  =.. [F|CtxArgs])),

    when((nonvar(Left);nonvar(Args)),
         append(Left, [R|Right], Args)
        ),
    when((nonvar(Left);nonvar(CtxArgs)),
         append(Left, [R1|Right], CtxArgs)
        ),

    (SubTerm = R,
     Hole = R1
    ;
    term_ctx_subterm_v2(R, Ctx1-Hole, SubTerm),
    R1 = Ctx1
    ),
    Ctx  =.. [F|CtxArgs].

Но следующий случай не работает:

[debug]  ?- term_ctx_subterm_v2(Term, a(X)-X, 1).
when((nonvar(Term);nonvar(a), ?=([1], [X])), Term=..[a, 1]) ;
ERROR: Arguments are not sufficiently instantiated
ERROR: In:
ERROR:    [9] _7658=..[_7664|_7666]
ERROR:    [8] term_ctx_subterm_v2(_7690,_7698-_7700,1) at /Users/edechter/Dropbox/Projects/scratch/term_ctx_subterm.pl:52
ERROR:    [7] term_ctx_subterm_v2(_7724,... - _7734,1) at /Users/edechter/Dropbox/Projects/scratch/term_ctx_subterm.pl:49
   Exception: (9) _6952{when = ...}=..[_6840{when = ...}|_7228{when = ...}] ? ;

тогда как в первой версии он работает нормально:

[debug]  ?-     term_ctx_subterm(Term, a(X)-X, 1).
Term = a(1),
X = 1.