7
8:-module(ccopy,[ccopy/2]). 9
10:- use_module(quantif). 11
13
22
23get_substituted_variable([(X1,Y1)|_],X2,Y2):-
24 X1==X2,
25 !,
26 Y1=Y2.
27get_substituted_variable([_|T],X,Y):-
28 get_substituted_variable(T,X,Y).
29
30
31ccopy(X,Y):-
32 ccopy(X,Y,[],Substitutions),
33 copy_restrictions(Substitutions).
34
35ccopy(X,Y,Substitutions,Substitutions) :-
36 var(X), get_quant(X,existsf),
37 !, X=Y.
38ccopy(X,Y,_,_):-
39 var(X), nonvar(Y), !,
40 writeln("Error: ccopy invoked with 2nd argument non var"),
41 halt.
42
43ccopy(X,Y,Substitutions,Substitutions):-
44 var(X),
45 get_substituted_variable(Substitutions,X,Y),
46 !.
47ccopy(X,Y,OldSubstitutions,[(X,Y)|OldSubstitutions]) :-
48 var(X),!,
49 ((get_quant(X,QX),nonvar(QX))
50 -> 51 set_quant(Y,QX)
52 ; true).
55ccopy(X,Y,OldSubstitutions,NewSubstitutions) :-
56 functor(X,F,N),
57 functor(Y,F,N),
58 ccopy_arg(N,X,Y,OldSubstitutions,NewSubstitutions).
59
60ccopy_arg(0,_,_,Substitutions,Substitutions):-!. 61ccopy_arg(N,X,Y,OldSubstitutions,NewSubstitutions):-
62 63 arg(N,X,Xn),
64 arg(N,Y,Yn),
65 ccopy(Xn,Yn,OldSubstitutions,IntSubstitutions),
66 N1 is N-1,
67 ccopy_arg(N1,X,Y,IntSubstitutions,NewSubstitutions).
68
69copy_restrictions(R):- copy_restrictions(R,R).
70copy_restrictions([],_).
71copy_restrictions([(X,Y)|T],Subs):-
72 get_restrictions(X,Rx),
73 74 75 76 77 substitute_vars(Rx,[(X,Y)|Subs],Ry),
78 79 set_restriction_list(Ry,Y),
80 copy_restrictions(T,Subs).
81
82substitute_vars(X,Subs,Z):-
83 var(X),!,
84 (get_substituted_variable(Subs,X,Y)
85 -> Z=Y
86 ; Z=X).
89substitute_vars(X,Subs,Y):-
90 functor(X,F,N),
91 functor(Y,F,N),
92 substitute_vars_arg(N,X,Y,Subs).
93
94substitute_vars_arg(0,_,_,_):- !.
95substitute_vars_arg(N,X,Y,Subs):-
96 arg(N,X,Xn),
97 arg(N,Y,Yn),
98 substitute_vars(Xn,Subs,Yn),
99 N1 is N-1,
100 substitute_vars_arg(N1,X,Y,Subs)