%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Show Bound Terms -- Variable binding term printer
% Shows internal bindings in a term.
%
% by David Reitter, reitter at mle dot mit.media.edu
% Version dated July 28, 2003
% Updated versions likely to be found at http://www.david-reitter.com/
% licensed under the GNU General Public License
%
% WHAT DOES THIS DO?
% 	In term(D, D), the two arguments are co-bound.
% 	Normally, if D is instantiated, the value of D will be printed twice:
% 	T=term(D,D), D=bound(a,X), write(T) 
% 	will print "term(bound(a,_G100),bound(a,_G100))". This does not reveal the binding, 
% 	and leads to large output, especially when working with unification-based
% 	mechanisms where bindings occur frequently and contain large structures.
% 	The predicate sbt/2 converts the above example as follows:
% 	T=term(D,D), D=bound(a,b), sbt(T, T2), write(T2)
% 	yields "term(<V1> =bound(a, b), <V1>)".
% 	This attempts to show the intensional description of the term rather than the extensional one.
%
% REQUIREMENTS:
%	Tested with SWI-Prolog. Other Prolog implementations should run, but you might
%     have to replace the call to flag/3 at the end of this file.
%
% EXAMPLES:
%     Run ex/0 to view the effect.
%     Run ex2/0 to see that things don't work perfectly. this_term(1,2) shouldn't be bound.
%
% NOTE: 
% 	Bindings are only shown for complex terms like lists or a(b,c) or a/b, but not
% 	for single atoms.  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% USAGE EXAMPLE
ex :-
 	Term = p(p,B,fine:B,fine:C,good(B,A/D),[some,things, like,C,or,A,or,D,are,bound,and,thats,fine:B]),
	B=[a,b|_], 
	A=this_atom,
	D=this_term(1,2),
	sbt(Term,New),
	format('Original:\n ~w\n\nSBT:\n ~w\n\n', [Term, New]). 

ex2 :- 
	Term = p(this_term(1,2), hello:D),
	D=this_term(1,2),
	sbt(Term,New),
	format('Original:\n ~w\n\nSBT:\n ~w\n\n', [Term, New]). 		
		
% CONFIGURATION
% declare a clause of sbt_ignorefunctor/1 for each functor that is supposed to be ignored.
% sbt/2 will only display bindings of compound terms. It will, however, not analyze bound terms
% that have an ignored functor. In the above example (call ex/0), you will get a "fine: <V1>" binding with
% the sbt_ignorefunctor enabled. Without it, you will get a "<V3> = fine: xxx" binding. 

sbt_ignorefunctor(':').
	

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
	
	
%%%%%%%%%%%%%%%%
%sbt(T,N) :-
%	display_cache_get(sbt, T, N),!.

sbt(T,N) :-
	sbt_init_gensym(Session),
	sbt(T, Session, Hole-Hole,_,N),  
	sbt_instantiate_singleterms(Hole). 

sbt(V, _Session, _Acc-AccH, AccH, V) :-
	(var(V);atom(V);integer(V)), !. 

sbt(T, Session, Acc-AccH, AccH, VarPrefix) :- 
	% check if double term
	identmember(v(T,VarPrefix/FirstOccurrence/NewTerm), Acc),
	!, 
	(var(VarPrefix) -> 
		(
	  		sbt_gensym(Session, 'V', NewName),
 			concat_atom(['<', NewName, '>'], VarPrefix), 
 			!
 		);
 		true
 	),
 	% set label in first occurrence
	FirstOccurrence = (VarPrefix=NewTerm).
	
% in the new term, we just see a new variable
% ('Firstoccurrence'). This will later be instantiated
% correctly as V3:Term or as term, depending on 
% whether the thing was referenced again or not. 
	
sbt(T, Session, Acc-AccH, AccNH2, FirstOccurrence) :-
	T =.. [First|Rest],
	% add to difflist
	(sbt_ignorefunctor(First)
	-> AccNH1=AccH, 
	    FirstOccurrence=Result
	;   AccH = [v(T,_VarPrefix/FirstOccurrence/Result)|AccNH1]
	),
	sbtf(Rest, Session, Acc-AccNH1, AccNH2, Result1),
	Result =.. [First|Result1].


% for lists
sbtf([], _Session, _Acc-AccH, AccH, []) :- !.
sbtf([First|Rest], Session, Acc-AccH, AccNH2,[Res1|Res2]) :- !,
	sbt(First, Session, Acc-AccH, AccNH, Res1),  
	 sbtf(Rest, Session, Acc-AccNH, AccNH2, Res2).
	  

% post-processing: instantiate terms that occur only once -- do not show a label
sbt_instantiate_singleterms(V) :- var(V),!.
sbt_instantiate_singleterms([]) :- !.
% binding if binding possible
sbt_instantiate_singleterms([v(_, _/SO/SO)|R]):- !,
	sbt_instantiate_singleterms(R).
sbt_instantiate_singleterms([_|R]):- !,
	sbt_instantiate_singleterms(R).

identmember(Entry, Var) :-
%	not(not(memberchk(Entry, Var))),  % speed optimization??
	identmember2(Entry, Var).

identmember2(Entry, Var) :-  
	var(Var),	% end of open list -- fail unless identical
	!,
	v(Elem,Parm)=Entry,
	not(not((Var=v(F,_),Elem==F))),
	Var=v(_,Parm). 
	
	
identmember2(v(Elem,Parm), [v(F,Parm)|_]) :- 
	Elem==F, !.
identmember2(_, []) :- !, fail.   % empty list - fail
	
identmember2(Elem, [_|R]) :-
	identmember2(Elem, R).
	
% GENSYM WRAPPER
% might need modification for other Prologs. Works with SWI-Prolog

sbt_init_gensym(Session) :-
	gensym('sbt_session_', Session),
	flag(Session, _, 1).
	
sbt_gensym(Session, Prefix, Value) :-
	flag(Session, Curr, Curr+1),
	atom_concat(Prefix, Curr, Value).

%%% DOCUMENTATION

% Acc, AccHole is a DIFFERENCE LIST
% Acc = [a,b,c|Hole]

% each element of this diff list contains v(OrigTerm, Name/FirstOcc/NewTerm)
% OrigTerm -- the exact Term as it was originally
% Name -- the name we assigned to this term
% FirstOcc -- unified with the first Occurrence of this Term, but in the target Structure.
%                  initially, this is an unbound variable. When a second occurrence of the term
%                  (i.e. a binding) is encountered, it is bound to a variable label:NewTerm. 
%                  In the end, sbt_instantiate_singleterms/1 will bind all remaining FirstOcc to
%                  NewTerm, so that Terms that are not referenced are not labeled.
% NewTerm -- this is the new term replacement as calculated recursively