% File : TERMIN.PL
% Author : R.A.O'Keefe
% Updated: 15 October 1984
% Purpose: Check for missing base cases.
% updated for NIP: Ken Johnson 24-6-87
/* termin(File) loads a file of Prolog clauses, which may use
disjunctions but not negations or foralls, and stores it as
recorded terms in the firm recorded(if,(pred/arity),_)
append will be stored as
if(append/3, []).
if(append/3, [append/3]).
in fact it is a little bit cleverer than that. If
the predicate symbol on the left occurs on the right,
the clause can be dropped entirely. So we just get
if(append/3, []).
It also ensures that there is a pred() fact
for each predicate defined.
termin/0 copies the if/2 clauses as fi/2, dropping (and
commenting on) any clauses that mention undefined predicates.
Termin/1 will load util:system.pl the first time it is called
so that built in p;redicates will not be lost.
Then, for each pred, it tries to prove that symbol, which
amounts to proving that it might have a terminating computation.
If this fails, it might mean that the predicate will just fail,
or it might mean that it won't terminate. (p :- fail. and
p :- p. look the same to termin.)
Note that if P fails, every pred that calls P will fail too.
This is the main thing that stops this being a practical tool.
*/
% Change the next clause when moving to a new directory
system_preds_are_in('/user1/ken/prolog/toolkit/terms/system_preds.pl').
termin(_) :-
\+ system(_),
system_preds_are_in(File),
reconsult(File),
system(Goal),
process(Goal),
fail.
termin(File) :-
see(File),
repeat,
read(Rule),
expand_term(Rule, Clause),
process(Clause),
Clause = end_of_file,
!,
seen.
process(end_of_file) :- !.
process(:-(_)) :- !.
process(:-(Head,Body)) :-
!,
note_head(Head, Pred),
flat_rule(Body, Flat, []),
sort(Flat, Sorted),
note_rule(Pred, Sorted).
process(Head) :-
note_head(Head, Pred),
note_rule(Pred, []).
note_head(Head, F/N) :-
functor(Head, F, N),
( pred(F/N)
;
record(pred,(F/N),_)
),
!.
note_rule(Pred, Body) :-
( memberchk(Pred, Body)
;
recorded(if,[Pred,Body],_)
;
record(if,[Pred,Body],_)
),
!.
flat_rule((A,B), L0, L) :- !,
flat_rule(A, L0, L1),
flat_rule(B, L1, L).
flat_rule((A;_), L0, L) :-
flat_rule(A, L0, L).
flat_rule((_;B), L0, L) :- !,
flat_rule(B, L0, L).
flat_rule(!, L, L) :- !.
flat_rule(true, L, L) :- !.
flat_rule(fail, _, _) :- !,
fail.
flat_rule(Head, [F/N|L], L) :-
functor(Head, F, N).
termin :-
(
recorded(fi,_,Key),
erase(Key),
fail
;
(
recorded(if,[Pred,Body],_),
if_to_fi(Pred, Body), fail
; pred(Pred), check(Pred), fail
; true
)
).
if_to_fi(Pred, Body) :-
member(Undef, Body),
\+ pred(Undef),
!,
writef('! %t calls %t, which is not defined.\n', [Pred,Undef]).
if_to_fi(Pred, Body) :-
record(fi,[Pred,Body],_).
check(Pred) :-
prove(Pred, []),
!.
check(Pred) :-
writef('! %t has no terminating proof.\n', [Pred]).
prove(Query, Stack) :-
\+ memberchk(Query, Stack),
recorded(fi,[Query,Body],_),
prove_body(Body, [Query|Stack]).
prove_body([], _) :- !.
prove_body([H|T], Stack) :-
prove(H, Stack),
prove_body(T, Stack).