% Prolog term manipulation as constraints % 931127 ECRC, thom fruehwirth based on ideas from 9203 and 9104 % 980207, 980312 thom fruehwirth LMU adapted for Sicstus CHR :- use_module(library(chr)). handler term. option(already_in_store, off). option(already_in_heads, off). option(check_guard_bindings, off). operator(100,xfx,unif). T unif [F|L] :- chr_unif(T,F,L). constraints chr_functor/3, chr_arg/3, chr_unif/3. chr_functor(T,F,N) <=> (nonvar(T);nonvar(F),nonvar(N)) | functor(T,F,N). chr_functor(T,T,N) ==> N=0. chr_functor(T,F,0) ==> T=F. chr_functor(T,F,N) ==> chr_nonvar(T). chr_functor(T,F,N) \ chr_functor(T,F1,N1) <=> F1=F,N1=N. chr_functor(T,F,N), chr_arg(M,T,A) ==> nonvar(N),nonvar(M) | N>=M,N>0. chr_arg(0,T,A) <=> fail. chr_arg(N,T,A) <=> nonvar(N),nonvar(T) | arg(N,T,A). chr_arg(N,T,A) \ chr_arg(N,T,A1) <=> A1=A. chr_unif(T,F,L) <=> (nonvar(T);nonvar(F),islist(L)) | T=..[F|L]. chr_unif(T,T,L) ==> L=[]. chr_unif(T,F,[]) ==> T=F. chr_unif(T,F,L) ==> chr_nonvar(T),chr_nonvar(L). chr_unif(T,F,L) \ chr_unif(T,F1,L1) <=> F1=F,L1=L. chr_unif(T,F,L) \ chr_unif(T1,F,L) <=> T1=T. chr_unif(T,F,L) \ chr_functor(T,F1,N) <=> (nonvar(N);islist(L)) | F1=F,length(L,N). chr_unif(T,F,L) \ chr_arg(M,T,A) <=> nonvar(M) | nth_member(M,L,A). nth_member(1,[X|_],X). nth_member(N,[_|L],X):- gt(N,1), plus(M,1,N), nth_member(M,L,X). islist([]) ?- true. islist([X|L]) ?- islist(L). constraints chr_var/1, chr_nonvar/1. chr_var(X) <=> nonvar(X) | fail. chr_nonvar(X) <=> nonvar(X) | true. chr_nonvar(X), chr_var(X) <=> fail. chr_var(X) \ chr_var(X) <=> true. chr_nonvar(X) \ chr_nonvar(X) <=> true. constraints plus/3, gt/2. plus(A,B,C) <=> nonvar(A),nonvar(B) | C is A+B. plus(A,B,C) <=> nonvar(A),nonvar(C) | B is C-A. plus(A,B,C) <=> nonvar(B),nonvar(C) | A is C-B. gt(A,B) <=> nonvar(A),nonvar(B) | A>B. % Examples ================================================================= % these standard predicates using term manipulation run now backwards as well % but sometimes this causes nontermination % constraints needed in the examples constraints diff/2, diff_list/2. diff(X,X) <=> fail. diff_list(V,[]) <=> true. diff_list(V,L) <=> member(X,L),V==X | fail. member(X,[Y|L]):- X=Y ; member(X,L). % two variants of unification by sterling/shapiro unify1(X,Y):- chr_var(X),chr_var(Y), X=Y. unify1(X,Y):- chr_var(X),chr_nonvar(Y), X=Y. unify1(X,Y):- chr_nonvar(X),chr_var(Y), X=Y. unify1(X,Y):- % chr_nonvar(X),chr_nonvar(Y), chr_functor(X,F,N),chr_functor(Y,F,N), unify_args(N,X,Y). unify_args(0,X,Y). unify_args(N,X,Y):- gt(N,0), plus(N1,1,N), chr_arg(N,X,A),chr_arg(N,Y,B), unify1(A,B), unify_args(N1,X,Y). /* | ?- unify1(a,b). no | ?- unify1(A,B). B = A, chr_var(A) ? ; B = A, chr_nonvar(A), chr_functor(A,A,0) ? ; chr_nonvar(A), chr_nonvar(B), chr_var(_A), chr_functor(A,_B,1), chr_functor(B,_B,1), chr_arg(1,A,_A), chr_arg(1,B,_A) ? | ?- unify1(f(a,B),f(B,C)). B = a, C = a ? ; % nontermination */ unify2(X,Y):- chr_var(X),chr_var(Y), X=Y. unify2(X,Y):- chr_var(X),chr_nonvar(Y), X=Y. unify2(X,Y):- chr_nonvar(X),chr_var(Y), Y=X. unify2(X,Y):- % chr_nonvar(X),chr_nonvar(Y), X unif [F|As],Y unif [F|Bs], unify_list(As,Bs). unify_list([],[]). unify_list([A|As],[B|Bs]):- unify2(A,B), unify_list(As,Bs). /* | ?- unify2(A,B). B = A, chr_var(A) ? ; B = A, chr_nonvar(A), chr_unif(A,A,[]) ? ; B = A, chr_nonvar(A), chr_var(_A), chr_unif(A,_B,[_A]) ? ; B = A, chr_nonvar(A), chr_var(_A), chr_var(_B), chr_unif(A,_C,[_A,_B]) ? | ?- unify2(f(a,B),f(B,C)). B = a, C = a ? ; no */ % collecting the variables of a term into a list, groundness and more varlist(A,Vars):- varlist(A,[],Vars). varlist(V,L,[V|L]):- chr_var(V),diff_list(V,L). varlist(V,L,L):- chr_var(V),member(V,L). varlist(T,L1,L2):- %chr_nonvar(T), chr_functor(T,_,N), varlist(N,T,L1,L2). varlist(0,T,L,L). varlist(N,T,L1,L3) :- gt(N,0), plus(K,1,N), chr_arg(N,T,TK), varlist(TK,L1,L2), varlist(K,T,L2,L3). /* | ?- varlist(f(a,B),L). L = [B], chr_var(B) ? ; L = [], chr_nonvar(B), chr_functor(B,B,0) ? ; L = [_A], chr_nonvar(B), chr_var(_A), chr_functor(B,_B,1), chr_arg(1,B,_A) ? | ?- varlist(X,[A,B]). chr_nonvar(X), chr_var(B), chr_var(A), diff_list(A,[B]), chr_functor(X,_A,2), chr_arg(2,X,B), chr_arg(1,X,A) ? ; % nontermination */ common_var(A,K,V1):- varlist(A,AV), varlist(K,KV), member(V,AV), member(V,KV). ground0(A):- varlist(A,[]). /* % termination problems */ ground1(T):- %chr_nonvar(T), chr_functor(T, _, N), ground1(N, T). ground1(0, _). ground1(N, T):- gt(N,0), plus(N1,1,N), chr_arg(N, T, A), ground1(A), ground1(N1, T). /* | ?- ground1(h(A,b,C)). chr_nonvar(C), chr_nonvar(A), chr_functor(C,C,0), chr_functor(A,A,0) ? ; chr_nonvar(C), chr_nonvar(A), chr_nonvar(_A), chr_functor(C,C,0), chr_functor(A,_B,1), chr_arg(1,A,_A), chr_functor(_A,_A,0) ? */ ground2(T) :- %chr_nonvar(T), T unif [_|Args], ground2l(Args). ground2l([]). ground2l([H|L]) :- ground2(H), ground2l(L). /* | ?- ground2(A). chr_nonvar(A), chr_unif(A,A,[]) ? ; chr_nonvar(A), chr_nonvar(_A), chr_unif(A,_B,[_A]), chr_unif(_A,_A,[]) ? */ number_vars(Term,N0,N1) :- var(Term), % chr_var(Term) would fail later plus(N0,1,N1), name(N0,Digits), name('V',[C]), name(Term,[C|Digits]). number_vars(Term,N0,N1) :- %chr_nonvar(Term), Term unif [_|Args], number_list(Args,N0,N1). number_list([],N0,N0). number_list([H|T],N0,N2) :- number_vars(H,N0,N1), number_list(T,N1,N2). undupvar(A,B,R,L):- undupvar(A,B,[],R,[],L). undupvar(V,V,R,[V|R],L,L):- chr_var(V),diff_list(V,R). undupvar(V,W,R,R,L,[W=V|L]):- chr_var(V),member(V,R). undupvar(T,S,R1,R3,L1,L3):- %chr_nonvar(T),chr_nonvar(S), chr_functor(T,F,N),chr_functor(S,F,N), undupvar(N,T,S,R1,R3,L1,L3). undupvar(0,T,S,R,R,L,L). undupvar(N,T,S,R1,R3,L1,L3):- gt(N,0), plus(M,1,N), chr_arg(N,T,TK), chr_arg(N,S,TS), undupvar(TK,TS,R1,R2,L1,L2), undupvar(M,T,S,R2,R3,L2,L3). % from comp.lang.prolog on a sequent calculus implementation % substitute(P, X, Y, Q) substitutes instances of X in P with Y, producing Q. substitute(P1, K1, K2, P2) :- P1 = K1, P2 = K2 ; diff(P1,K1), %chr_nonvar(P1),chr_nonvar(P2), P1 unif [F|Args1], P2 unif [F|Args2], substitute_list(Args1, K1, K2, Args2). substitute_list([], _, _, []). substitute_list([H1|T1], K1, K2, [H2|T2]) :- substitute(H1, K1, K2, H2), substitute_list(T1, K1, K2, T2). % from comp.lang.prolog on heaps and trees % uses is/2 %pos(Head,t(Head,Rel,L,[],0)-[], Nc, N0-N2):- /* leaf node */ % atomic(Head), % !, % string_length1(Head,L), % N2 is N0+L, % Rel is L//2, /* middle of the node */ % Nc is (N0+N2)//2. /* center over node */ pos(X,t(Head,Rel,L,Centers,Adj)-A, Nc, N0-N2):- /* non-leaf node */ %chr_nonvar(X), X unif [Head|Args], pos_list(Args,A,Centers,N0-N1), string_length1(Head,L), posdiff(N1-N0,L,Error), Adj is (Error+((N1-N0) mod 2))//2, N2 is N1+Error, Rel is L//2, /* middle of the node */ Nc is (N0+N2)//2. pos_list([], [], [], N-N). %pos_list([H], [A], [Center], N-N1) :- !, % pos(H,A,Center,N-N1). pos_list([H|T],[A|Args],[C|Centers],N0-Nn):- pos( H, A, C, N0-N1), plus(N1,2,N2), %N2 is N1+2, pos_list(T,Args,Centers,N2-Nn). string_length1(X,L):- atomic(X), name(X,S), length(S,L). posdiff(Expr,L,0):- Adj is L-Expr, Adj =< 0. posdiff(Expr,L,Adj):- Adj is L-Expr, Adj > 0. % lsu(A,B,G): the least specific unifier of A and B is G % joachims schimpfs code modified by thom lsu(A, B, G) :- map(A, B, G, [], Map), sort(0, =<, Map, SortedMap), unify_duplicates(SortedMap). map(A, B, G, Map, NewMap) :- %chr_nonvar(A),chr_nonvar(B), chr_functor(A, Name, Arity), chr_functor(B, Name, Arity), chr_functor(G, Name, Arity), map_arg(A, B, G, Map, NewMap, Arity-0). map(A, B, G, Map, [subst(A, B, G)| Map]):- chr_var(A) ; chr_var(B) ; %chr_nonvar(A),chr_nonvar(B), chr_functor(A, Name1, Arity1), chr_functor(B, Name2, Arity2), (diff(Name1,Name2);diff(Arity1,Arity2)). map_arg(A, B, G, Map, NewMap, Ar-N) :- Ar=N, Map = NewMap. map_arg(A, B, G, Map0, NewMap, Ar-N) :- gt(Ar,N), plus(N,1,N1), chr_arg(N1, A, An), chr_arg(N1, B, Bn), chr_arg(N1, G, Gn), map(An, Bn, Gn, Map0, Map1), map_arg(A, B, G, Map1, NewMap, Ar-N1). unify_duplicates([subst(A1, B1, G1)|T]) :- T = [subst(A2, B2, G2)|_], ( A1 = A2, B1 = B2, G1 = G2 ; diff(A1,A2) ; diff(B1,B2)), unify_duplicates(T). unify_duplicates([T]). unify_duplicates([]). % end of handler term