%%%%%  Ashwin Srinivasan's Prolog code 
%%%%%  for measuring theory complexity. 


% dynamic statements are only for compiled Prologs
% (not Clocksin and Mellish standard)

:- dynamic counts/2.

% count clauses, literals and terms in file FileName
count(FileName):-
	reset_counts,
	see(FileName),
	count_clauses,
	seen,
	print_theory_counts.

count_clauses:-
	repeat,
	read(Clause),
	count_clause(Clause),
	Clause = end_of_file,
	!.

count_clause(end_of_file):- !.
count_clause((Head:-Body)):-
	!,
	inc(clauses,1),
	get_litterm_count((Head,Body)).
count_clause(UnitClause):-
	inc(clauses,1),
	get_litterm_count(UnitClause).


get_litterm_count((LitTerm;LitTerms)):-
	!,
	inc(litterms,1),		% for ';'/2
	get_litterm_count(LitTerm),
	get_litterm_count(LitTerms).
get_litterm_count((LitTerm,LitTerms)):-	% no charge for ','/2
	!,
	get_litterm_count(LitTerm),
	get_litterm_count(LitTerms).
get_litterm_count(LitTerm):-
	inc(litterms,1),		% for Lit
	functor(LitTerm,Name,Arity),
	get_arg_count(LitTerm,Arity,0,T0),
	inc(litterms,T0).

get_arg_count(_,0,LT,LT).
get_arg_count(Expr,Arg,T,LitTerms):-
	arg(Arg,Expr,Term),
	var(Term), !,
	Arg0 is Arg - 1,
	T1 is T + 1,
	get_arg_count(Expr,Arg0,T1,LitTerms).
get_arg_count(Expr,Arg,T,LitTerms):-
	arg(Arg,Expr,LitTerm),
	functor(LitTerm,LitTermName,LitTermArity),
	inc_term_count(LitTermName/LitTermArity,T,T1),
	get_arg_count(LitTerm,LitTermArity,T1,T2),
	Arg0 is Arg - 1,
	get_arg_count(Expr,Arg0,T2,LitTerms).

inc_term_count(','/2,T,T):-		% no charge for ','/2 
	!.
inc_term_count(_,T,T1):-
	T1 is T + 1.

reset_counts:-
	retractall(counts(_,_)),
	asserta(counts(clauses,0)),
	asserta(counts(litterms,0)).

print_theory_counts:-
	counts(clauses,C),
	write('clauses:'), write(C), nl,
	counts(litterms,LT),
	write('lits+terms:'), write(LT), nl, nl,
	Total is C + LT,
	write('total:'), write(Total), nl.


inc(Parse,N):-
	retract(counts(Parse,N1)),
	N0 is N1 + N,
	asserta(counts(Parse,N0)).