1%-------------------------------------------------------------
    2% Implementation of ccopy
    3% Marco Gavanelli
    4% Ver 3
    5% Considers also the quantifier restrictions
    6%-------------------------------------------------------------
    7
    8:-module(ccopy,[ccopy/2]).    9
   10:- use_module(quantif).   11
   12% ccopy(+Term,-CopiedTerm)
   13
   14/*
   15
   16Marco Alberti:
   17
   18This version replaces all multiple occurrences of the same "old"
   19variable with the same "new" variable.
   20
   21*/
   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	  -> 	%set_term_quantification(Y,QX)
   51            set_quant(Y,QX) 
   52	  ; 	true).
   53% Uncomment the following clause if you want to save memory (at the cost of speed)
   54% ccopy(X,Y,Old,New):- ground(X),!,X=Y,Old=New.
   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):-!. % SICStus non ottimizza questo se tolgo il cut e metto N>0
   61ccopy_arg(N,X,Y,OldSubstitutions,NewSubstitutions):-
   62	%N>0,
   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	%(X,Y) is already a member of Subs; however, we are
   74	%renaming the restrictions on variable X, so it is
   75	%handy to have the couple (X,Y) as first element
   76	%of the list.
   77	substitute_vars(Rx,[(X,Y)|Subs],Ry),
   78	%set_restriction_list(Ry), MG 27 jul 2007: This gives a strong speedup in block world, where many restrictions are imposed
   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).
   87%substitute_vars(X,_Subs,X):- Without this clause is slightly faster
   88%	ground(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)