How to use freeze/2 or when/2 to for more pure Prolog code

196 Views Asked by At

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.
0

There are 0 best solutions below