%   File   : DEPTH.PL
%   Author : R.A.O'Keefe
%   Updated: 12 March 1984, 23 June 1987
%   Purpose: Find or check the depth of a term.

/*  Many resolution-based theorem provers impose a Depth Bound on the
    terms they create.  Not the least of the reasons for this is to
    stop infinite loops.  This module provides two entry points:

	depth_of_term(Term, Depth)
	depth_bound(Term, Bound)

    depth_of_term calculates the depth of the term, using the definition
	depth(Var) = 0
	dpeth(Const) = 0
	depth(F(T1,...,Tn)) = 1+max(depth(T1),...,depth(Tn))

    Mostly, we couldn't care less what the depth of a term is, provided
    it is below some fixed bound.  depth_bound checks that the depth of
    the given term is below the bound (which is assumed to be an integer
    >= 1), without ever finding out what the depth actually is.
*/

% Example, given the tree
% 
% 		m
% 	       / \
% 	      /   \
% 	    f	    q
% 	   / \     / \
% 	  a   g   /   \
% 		 o      u
% 		/ \    / \
% 		n  p  s  w
% represented by
% tree(
% 	tree(m,
% 		tree(f,tree(a,[],[]),tree(g,[],[])),
% 		tree(q,
% 			tree(o,tree(n,[],[]),tree(p,[],[])),
% 			tree(u,tree(s,[],[]),tree(w,[],[]))
% 		    )
% 	    )
%     ).
% 
% test(D) :-
% 	tree(T),
% 	depth_of_term(T,D).
% 
% % ?- test(D) succeeds with D = 4
% 
% ?- tree(T), depth_bound(T,3)	Fails
% ?- tree(T), depth_bound(T,4)	Succeeds

depth_bound(Compound, Bound) :-
	nonvar(Compound),
	functor(Compound, _, Arity),
	Arity > 0,
	!,
	Bound > 0,		% this is the test!
	Limit is Bound-1,
	depth_bound(Arity, Compound, Limit).

depth_bound(_, _).


depth_bound(0, _, _) :-
	!.

depth_bound(N, Compound, Limit) :-
	arg(N, Compound, Arg),
	depth_bound(Arg, Limit),
	M is N-1,
	!,
	depth_bound(M, Compound, Limit).

depth_of_term(Compound, Depth) :-
	nonvar(Compound),
	functor(Compound, _, Arity),
	Arity > 0,
	!,
	depth_of_term(Arity, Compound, 0, ArgDepth),
	Depth is ArgDepth+1.
depth_of_term(_, 0).

depth_of_term(0, _, Depth, Depth) :- !.

depth_of_term(N, Compound, SoFar, Depth) :-
	arg(N, Compound, Arg),
	depth_of_term(Arg, ArgDepth),
	ArgDepth > SoFar,
	M is N-1,
	!,
	depth_of_term(M, Compound, ArgDepth, Depth).

depth_of_term(N, Compound, SoFar, Depth) :-
	M is N-1,
	depth_of_term(M, Compound, SoFar, Depth).