I have written a predicate called term_ctx_subterm/3 which is a relation between term, a one-hole context for that term, and a subterm that fills the hole. For the most part the predicate works as I desire. See the code and examples of its use below. However, I used two clauses to define the predicate, one for each of its two modes. In the first mode the term is a compound, and it is deconstructed into one-hole contexts and the corresponding subterms. In the second mode, the one-hole context is given, and the term is reconstructed using the subterm to fill the hole.
I've been trying to write term_ctx_subterm as a one clause predicate using when/2, and I think I'm close but a) it's pretty ugly and b) it doesn't work quite right. How can I use the coroutining predicates to implement term_ctx_subterm using a single clause?
First here's version 1, with two clauses:
Version 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
%
Version 2
In this version, I try to use when/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].
But the following case does not work:
[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 = ...}] ? ;
whereas it works fine in the first version:
[debug] ?- term_ctx_subterm(Term, a(X)-X, 1).
Term = a(1),
X = 1.