/* File:      singleton.P
** Author(s): Kostis F. Sagonas
** Contact:   xsb-contact@cs.sunysb.edu
** 
** Copyright (C) The Research Foundation of SUNY, 1986, 1993-1998
** 
** XSB is free software; you can redistribute it and/or modify it under the
** terms of the GNU Library General Public License as published by the Free
** Software Foundation; either version 2 of the License, or (at your option)
** any later version.
** 
** XSB is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
** FOR A PARTICULAR PURPOSE.  See the GNU Library General Public License for
** more details.
** 
** You should have received a copy of the GNU Library General Public License
** along with XSB; if not, write to the Free Software Foundation,
** Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
**
** $Id: singlton.P,v 1.3 1999/08/18 22:05:23 warren Exp $
** 
*/



/*======================================================================*/
/*  singleton_check(+Clause, +VariableList).				*/
/*======================================================================*/

singleton_check(X, _) :- var(X), !.
singleton_check([], _) :- !.
singleton_check([Cl|Cls], VariableList) :- !,
	singleton_check(Cl, VariableList),
	singleton_check(Cls, VariableList).
singleton_check(Clause, VariableList) :-
	( Clause = (_ :- _)  ->	'singleton check'(Clause, VariableList)
	; Clause = (H --> B),nonvar(H) ->
			( H =.. HL, append(HL, [[],[]], NHL), NH =.. NHL,
			  'singleton check'((NH :- B), VariableList), fail
			; true
			)
	; Clause = (':-'(_)) ->	true
	; Clause = ('?-'(_)) ->	true
	; /* FACT */		'singleton check'((Clause :- true),VariableList)
	).

'singleton check'(_, []) :- 
	!.	% This captures clauses with no variables to be checked, 
		% (for example ground clauses, or clauses that contain
		% only underscores as variables), where VariableList is
		% variable and no singleton test is needed.
'singleton check'(Clause, VariableList) :-
	singleton_warnings(Clause, VariableList),
	fail.	% Undo numbervars' side-effects and reclaim all space used.
'singleton check'(_, _).


singleton_warnings(Clause, VariableList) :-
	numbervars(Clause, 1, NumberOfVars),
	N is NumberOfVars - 1,
	functor(Occurences, occ, N),
	calculate_occurences(Clause, Occurences),
	Clause = (Head :- _),
	hilog_functor(Head, P, A),
	write_singleton_warnings(VariableList, Occurences, P, A).


calculate_occurences(Term, Occurences) :-
	functor(Term, _, Arity),
	'calculate occurences'(Term, 0, Arity, Occurences).


'calculate occurences'(_, N, N, _) :- 
	!.
'calculate occurences'(Term, N, Arity, Occurences) :-
	NewN is N + 1,
	arg(NewN, Term, Arg),	% We cannot use ll_arg/3 here (Term may be a list)
	( Arg = '$VAR'(Number) ->
		( integer(Number) ->
			ll_arg(Number, Occurences, OccCount),
			( var(OccCount) -> OccCount = found(_)
			; OccCount = found(Times) -> 
				( var(Times) -> Times = 'at least twice'
				; true
				)
			)
		; functor(Arg, _, ArgArity),
		  'calculate occurences'(Arg, 0, ArgArity, Occurences)
		)
	; atomic(Arg) -> 
		true
	; functor(Arg, _, ArgArity),
	  'calculate occurences'(Arg, 0, ArgArity, Occurences)
	),
	'calculate occurences'(Term, NewN, Arity, Occurences).


write_singleton_warnings([], _, _, _) :-
	!.	% This captures the open-end of VariableList.
write_singleton_warnings([vv(VarName,'$VAR'(N))|Rest], Occurences, P, A) :-
	atom_codes(VarName, CharList),
	( CharList = [95|_] ->	% variable Var begins with an "_"
		true		% (underscore), so its OK, ignore it!.
	; ll_arg(N, Occurences, OccCount),
	  ( OccCount == found('at least twice') -> true
	  ; warning(('Singleton variable ', VarName,
		     ' in a clause of ', P, '/', A))
	  )
	),
	write_singleton_warnings(Rest, Occurences, P, A).